Add an UnboundTypeVariable error.

client/FPrinter.ml

@@ -209,6 +209,9 @@ let print_type_error e =
   | UnboundTermVariable x ->
       str "Scope error." ++
       str "The variable %s is unbound." x
+  | UnboundTypeVariable x ->
+      str "Scope error." ++
+      str "The type variable %d is unbound." x
   | TwoOccurencesOfSameVariable x ->
       str "Scope error." ++
       str "The variable %s is bound twice in a pattern." x

client/FTypeChecker.ml

@@ -8,6 +8,7 @@ type type_error =
   | NotAForall of debruijn_type
   | NotAnEqual of debruijn_type
   | UnboundTermVariable of tevar
+  | UnboundTypeVariable of tyvar
   | TwoOccurencesOfSameVariable of string
   | ContextNotAbsurd
 
@@ -223,7 +224,14 @@ let rec translate ~inside_mu store (env : vertex list) (ty : F.debruijn_type)
   = match ty with
 
   | TyVar x ->
-      List.nth env x
+      begin
+        (* If the type is closed, then [x] was bound by a quantifier before and
+           was added to the environment. *)
+        try
+          List.nth env x
+        with Not_found ->
+          raise (TypeError (UnboundTypeVariable x))
+      end
 
   | TyMu ((), ty) ->
       (* Extend the environment with a mapping of this μ-bound variable

client/FTypeChecker.mli

@@ -10,6 +10,7 @@ type type_error =
   | NotAForall of debruijn_type
   | NotAnEqual of debruijn_type
   | UnboundTermVariable of tevar
+  | UnboundTypeVariable of tyvar
   | TwoOccurencesOfSameVariable of string
   | ContextNotAbsurd