Build an export environment into the typechecker, and add a few tests.

demos/system-F-type/FTypeChecker.ml

@@ -47,42 +47,42 @@ let extend_with_tyvar (env : env) (a : tyvar) : env =
 
 (* Destructors. *)
 
-exception NotAnArrow of nominal_typ
+exception NotAnArrow of raw_typ
 
-let as_arrow ty : nominal_typ * nominal_typ =
+let as_arrow xenv ty : nominal_typ * nominal_typ =
   match ty with
   | TyArrow (ty1, ty2) ->
       ty1, ty2
   | _ ->
-      raise (NotAnArrow ty)
+      raise (NotAnArrow (export_typ xenv ty))
 
-exception NotAProduct of nominal_typ
+exception NotAProduct of raw_typ
 
-let as_product ty : nominal_typ * nominal_typ =
+let as_product xenv ty : nominal_typ * nominal_typ =
   match ty with
   | TyProduct (ty1, ty2) ->
       ty1, ty2
   | _ ->
-      raise (NotAProduct ty)
+      raise (NotAProduct (export_typ xenv ty))
 
-exception NotAForall of nominal_typ
+exception NotAForall of raw_typ
 
-let as_forall ty : tyvar * nominal_typ =
+let as_forall xenv ty : tyvar * nominal_typ =
   match ty with
   | TyForall (a, ty) ->
       a, ty
   | _ ->
-      raise (NotAForall ty)
+      raise (NotAForall (export_typ xenv ty))
 
 (* -------------------------------------------------------------------------- *)
 
 (* An equality test. *)
 
-exception TypeMismatch of nominal_typ * nominal_typ
+exception TypeMismatch of raw_typ * raw_typ
 
-let (--) ty1 ty2 =
+let equate xenv ty1 ty2 =
   if not (equiv_typ ty1 ty2) then
-    raise (TypeMismatch (ty1, ty2))
+    raise (TypeMismatch (export_typ xenv ty1, export_typ xenv ty2))
 
 (* -------------------------------------------------------------------------- *)
 
@@ -99,7 +99,12 @@ let (--) ty1 ty2 =
 (* Postcondition: if [typeof env t] returns a type [ty], then the bound variables
    of [ty] are disjoint with [env.tyvars], and [ty] has no shadowing. *)
 
-let rec typeof env (t : nominal_term) : nominal_typ =
+(* As we go down, we build an export environment [xenv], which is used when a
+   type error is encountered. The problematic types are then exported, so that
+   a type error message can be printed. This export environment is enriched
+   when we enter a \Lambda. *)
+
+let rec typeof xenv env (t : nominal_term) : nominal_typ =
   (* Test the preconditions stated above. *)
   assert (guq_term t);
   assert (avoids_term env.tyvars t);
@@ -113,19 +118,20 @@ let rec typeof env (t : nominal_term) : nominal_typ =
   | TeVar x ->
       lookup env x
   | TeAbs (x, ty1, t) ->
-      let ty2 = typeof (extend_with_tevar env x ty1) t in
+      let ty2 = typeof xenv (extend_with_tevar env x ty1) t in
       TyArrow (ty1, ty2)
   | TeApp (t, u) ->
-      let ty1, ty2 = as_arrow (typeof env t) in
-      typeof env u -- ty1;
+      let ty1, ty2 = as_arrow xenv (typeof xenv env t) in
+      equate xenv (typeof xenv env u) ty1;
       ty2
   | TeLet (x, t, u) ->
-      let env = extend_with_tevar env x (typeof env t) in
-      typeof env u
+      let env = extend_with_tevar env x (typeof xenv env t) in
+      typeof xenv env u
   | TeTyAbs (a, t) ->
-      TyForall (a, typeof (extend_with_tyvar env a) t)
+      let _, xenv = KitExport.extend a xenv in
+      TyForall (a, typeof xenv (extend_with_tyvar env a) t)
   | TeTyApp (t, ty2) ->
-      let a, ty1 = as_forall (typeof env t) in
+      let a, ty1 = as_forall xenv (typeof xenv env t) in
       (* We need ba(ty1) # [ty2/a] for this substitution to be safe. *)
       (* We have ba(ty1) # a because the type a.ty1 satisfies no-shadowing. *)
       assert (not (Atom.Set.mem a (ba_typ ty1)));
@@ -138,10 +144,10 @@ let rec typeof env (t : nominal_term) : nominal_typ =
          [ty2] when grafting: *)
       (* subst_TyVar_typ1 (fun ty2 -> ty2) ty2 a (copy_typ ty1) *)
   | TePair (t1, t2) ->
-      TyProduct (typeof env t1, typeof env t2)
+      TyProduct (typeof xenv env t1, typeof xenv env t2)
   | TeProj (i, t) ->
       assert (i = 1 || i = 2);
-      let ty1, ty2 = as_product (typeof env t) in
+      let ty1, ty2 = as_product xenv (typeof xenv env t) in
       if i = 1 then ty1 else ty2
   in
   (* Test the postcondition stated above. *)
@@ -149,4 +155,4 @@ let rec typeof env (t : nominal_term) : nominal_typ =
   ty
 
 let typeof =
-  typeof empty
+  typeof KitExport.empty empty

demos/system-F-type/Main.ml

@@ -3,23 +3,84 @@ open AlphaLib
 open F
 open FTypeChecker
 
+(* -------------------------------------------------------------------------- *)
+
+(* Typechecking a term. *)
+
 let check (t : raw_term) =
   printf "Raw term:\n%a\n"
-    Print.term t;
+    Print.term t
+  ;
   let t : nominal_term =
     import_term KitImport.empty t
   in
   printf "Imported (and reexported) term:\n%a\n"
-    Print.term (export_term KitExport.empty t);
-  let ty : nominal_typ =
-    typeof t
-  in
-  printf "Inferred type:\n%a\n"
-    Print.typ (export_typ KitExport.empty ty)
+    Print.term (export_term KitExport.empty t)
+  ;
+  match typeof t with
+  | ty ->
+      printf "Inferred type:\n%a\n"
+        Print.typ (export_typ KitExport.empty ty)
+  | exception NotAnArrow ty ->
+      printf "Type error: this is not a function type:\n%a\n"
+        Print.typ ty
+  | exception NotAProduct ty ->
+      printf "Type error: this is not a product type:\n%a\n"
+        Print.typ ty
+  | exception NotAForall ty ->
+      printf "Type error: this is not a universal type:\n%a\n"
+        Print.typ ty
+
+(* -------------------------------------------------------------------------- *)
+
+(* Sample well-typed terms. *)
+
+let identity =
+  TeTyAbs ("A", TeAbs ("x", TyVar "A", TeVar "x"))
 
 let terms : raw_term list = [
-  TeTyAbs ("A", TeAbs ("x", TyVar "A", TeVar "x"));
+
+  identity;
+
+  TeTyAbs ("A", TeAbs ("x", TyVar "A",
+    TeApp (TeTyApp (identity, TyVar "A"), TeVar "x")
+  ));
+
+  TeTyAbs ("A", TeAbs ("x", TyVar "A",
+  TeTyAbs ("B", TeAbs ("y", TyVar "B",
+    TeLet ("id", identity,
+      TePair (
+        TeApp (TeTyApp (TeVar "id", TyVar "A"), TeVar "x"),
+        TeApp (TeTyApp (TeVar "id", TyVar "B"), TeVar "y")
+      )
+    )
+  ))));
+
 ]
 
 let () =
   List.iter check terms
+
+(* -------------------------------------------------------------------------- *)
+
+(* Sample ill-typed terms. *)
+
+let ill_typed : raw_term list = [
+
+  TeTyAbs ("A", TeAbs ("x", TyVar "A", TeApp (TeVar "x", TeVar "x")));
+
+  TeProj (1, identity);
+
+  TeTyAbs ("A",
+    TeLet ("id", TeAbs ("x", TyVar "A", TeVar "x"),
+      TeTyApp (TeVar "id", TyVar "A")
+    )
+  );
+
+]
+
+let () =
+  List.iter check ill_typed
+
+(* TEMPORARY report unbound term variables, with locations. *)
+(* TEMPORARY report unbound type variables, with locations. *)