Idris Bug 2

KindBug.idr

data Kind : Type where 
  Set : Kind -- Sets
  ProdK : Kind -> Kind -> Kind -- Product Category

data Ty : Kind -> Type where 
  -- First and Second projections from a product category
  Fst : {k1, k2 : Kind} -> Ty (ProdK k1 k2) -> Ty k1
  Snd : {k1, k2 : Kind} -> Ty (ProdK k1 k2) -> Ty k2
  -- Cartesian product of two types
  Prod : Ty k -> Ty k -> Ty k 

EvalKind : Kind -> Type 
EvalKind Set = Type -- Set is just Type
EvalKind (ProdK k1 k2) = (EvalKind k1, EvalKind k2) -- Product kind is a product of types

partial
EvalTy : (k : Kind) -> Ty k -> EvalKind k 
EvalTy (ProdK k1 k2) p = (EvalTy k1 (Fst p), EvalTy k2 (Snd p))
EvalTy s (Fst {k1=s, k2} a) = fst (EvalTy (ProdK s k2) a)
EvalTy s (Snd {k1, k2=s} a) = snd (EvalTy (ProdK k1 s) a)

-- Given a kind, we need to determine the morphisms of its category
EvalArr : (k : Kind) -> EvalKind k -> EvalKind k -> Type 
EvalArr Set a b = a -> b  -- Sets and functions
EvalArr (ProdK k1 k2) l r = -- Product category k1 k2 has a pair of morphisms from k1 and k2
  (EvalArr k1 (fst l) (fst r), EvalArr k2 (snd l) (snd r))

data Term : Ty k -> Ty k -> Type where
  MapFst : Term (Prod t b) t -> Term (Fst (Prod t b)) (Fst t)

eval : (k : Kind) -> {s, t : Ty k}  
    -> Term s t -> EvalArr k (EvalTy k s) (EvalTy k t) 
eval k (MapFst t) = ?zzz  -- this works
--eval Set (MapFst t) = ?zzz -- this breaks idris