From 934fb82b15032c67f285a01e41dc63044968a5ea Mon Sep 17 00:00:00 2001 From: Olivier Date: Sat, 21 Jan 2023 14:50:36 +0100 Subject: [PATCH] Add an UnboundTypeVariable error. --- client/FPrinter.ml | 3 +++ client/FTypeChecker.ml | 10 +++++++++- client/FTypeChecker.mli | 1 + 3 files changed, 13 insertions(+), 1 deletion(-) diff --git a/client/FPrinter.ml b/client/FPrinter.ml index 97245b9..36c56fb 100644 --- a/client/FPrinter.ml +++ b/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 diff --git a/client/FTypeChecker.ml b/client/FTypeChecker.ml index 5abb7dd..6084e76 100644 --- a/client/FTypeChecker.ml +++ b/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 diff --git a/client/FTypeChecker.mli b/client/FTypeChecker.mli index 7b21104..047252e 100644 --- a/client/FTypeChecker.mli +++ b/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