SKK

src/lang.ml

@@ -112,6 +112,7 @@ let rec has_fv x e =
   | App (t, u) -> has_fv x t || has_fv x u
   | Hole (t, a) -> has_fv x t || has_fv x a
   | Meta { contents = Some t } -> has_fv x t
+  | Meta { contents = None } -> true
   | Obj -> false
   | _ -> error ~pos:e.pos "has_fv: handle %s" (to_string e)
 
@@ -187,7 +188,7 @@ let check_ps l a =
       | App (t, u) -> mk (App (rewrite t, rewrite u))
       | Hole (t, _) -> rewrite t
       | Meta { contents = Some t } -> rewrite t
-      | _ -> failwith (Printf.sprintf "TODO: in rewrite handle %s" (to_string e))
+      | _ -> error ~pos:e.pos "TODO: in rewrite handle %s" (to_string e)
     in
     (* Orient identities on variables as rewriting rules and normalize l. *)
     let rec aux rw = function

src/test.cccatt

@@ -83,8 +83,9 @@ coh ap-K (a b : .) (x : a) (y : b) : ap b a (ap a (b -> a) (K a b) x) y = x
 
 coh ap-comp (a b c : .) (f : a -> b) (g : b -> c) (x : a) : ap a c (comp a b c f g) x = ap b c g (ap a b f x)
 
-# # I is derivable
-# coh SKK (a : .) : ap _ _ (ap _ _ (S _ _ _) (K _ _)) (K _ _) = I a
+# I is derivable
+coh SKK (a b : .) : ap (a -> b -> a) (a -> a) (ap (a -> (b -> a) -> a) ((a -> b -> a) -> a -> a) (S a (b -> a) a) (K a (b -> a))) (K a b) = I a
+coh SKK (a b : .) : ap _ _ (ap _ _ (S _ _ _) (K _ _)) (K _ b) = I a
 
 ## Church numerals with pi-types