Detailed pre- and postconditions for the typechecker. Untested.

demos/system-F-type/FTypeChecker.ml

@@ -88,8 +88,28 @@ let (--) ty1 ty2 =
 
 (* The type-checker. *)
 
+(* Precondition: the term [t] that we started with satisfies global uniqueness.
+   So, the term [t] that we are looking satisfies global uniqueness and avoids
+   the set of in-scope type variables, [env.tyvars]. *)
+
+(* Precondition: if [env] maps [x] to some type [ty], then the bound variables
+   of [ty] are disjoint with [env.tyvars] and with the bound variables of [t],
+   and [ty] has no shadowing. *)
+
+(* 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 =
-  match t with
+  (* Test the preconditions stated above. *)
+  assert (guq_term t);
+  assert (avoids_term env.tyvars t);
+  assert (
+    let bad = Atom.Set.union env.tyvars (ba_term t) in
+    TermVarMap.for_all (fun _x ty ->
+      avoids_typ bad ty
+    ) env.tevars
+  );
+  let ty = match t with
   | TeVar x ->
       lookup env x
   | TeAbs (x, ty1, t) ->
@@ -107,17 +127,26 @@ let rec typeof env (t : nominal_term) : nominal_typ =
   | TeTyApp (t, ty2) ->
       let a, ty1 = as_forall (typeof 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 is satisfies no-shadowing. *)
+      (* We have ba(ty1) # a because the type a.ty1 satisfies no-shadowing. *)
       assert (not (Atom.Set.mem a (ba_typ ty1)));
       (* We have ba(ty1) # fa(ty2) because fa(ty2) is a subset of dom(env), that is,
-         env.tyvars, and typeof has the postcondition ba(\result) # env.tyvars. *)
-      subst_TyVar_typ1 (fun ty -> ty) ty2 a ty1
+         env.tyvars, and the result of typeof avoids env.tyvars. *)
+      (* We must copy when grafting so as to ensure that the result of the
+         substitution enjoys no-shadowing. *)
+      subst_TyVar_typ1 copy_typ ty2 a ty1
+      (* Conversely, I believe that we could choose to copy [ty1] and not copy
+         [ty2] when grafting: *)
+      (* subst_TyVar_typ1 (fun ty2 -> ty2) ty2 a (copy_typ ty1) *)
   | TePair (t1, t2) ->
       TyProduct (typeof env t1, typeof env t2)
   | TeProj (i, t) ->
       assert (i = 1 || i = 2);
       let ty1, ty2 = as_product (typeof env t) in
       if i = 1 then ty1 else ty2
+  in
+  (* Test the postcondition stated above. *)
+  assert (avoids_typ env.tyvars ty);
+  ty
 
 let typeof =
   typeof empty