Making judgment type generic over the type of inner constrs.

This allows to factorize code and prevents the unnecessary use of back and
forth conversions between the various types of terms.

Note that functions from typing may now raise errors as PretypeError rather
than TypeError, because they call the proper wrapper. I think that they were
wrongly calling the kernel because of an overlook of open modules.

4 files changed, 82 insertions, 67 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 4a543f195..5688813ad 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -469,9 +469,11 @@ let lookup_modtype mp env =
 
 (*s Judgments. *)
 
-type unsafe_judgment = {
-  uj_val : constr;
-  uj_type : types }
+type ('constr, 'types) punsafe_judgment = {
+  uj_val : 'constr;
+  uj_type : 'types }
+
+type unsafe_judgment = (constr, types) punsafe_judgment
 
 let make_judge v tj =
   { uj_val = v;
@@ -480,10 +482,12 @@ let make_judge v tj =
 let j_val j = j.uj_val
 let j_type j = j.uj_type
 
-type unsafe_type_judgment = {
-  utj_val : constr;
+type 'types punsafe_type_judgment = {
+  utj_val : 'types;
   utj_type : sorts }
 
+type unsafe_type_judgment = types punsafe_type_judgment
+
 (*s Compilation of global declaration *)
 
 let compile_constant_body = Cbytegen.compile_constant_body false
diff --git a/kernel/environ.mli b/kernel/environ.mli
index ea570cb4a..b7431dbe5 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -238,18 +238,21 @@ val keep_hyps : env -> Id.Set.t -> Context.Named.t
   actually only a datatype to store a term with its type and the type of its
   type. *)
 
-type unsafe_judgment = {
-  uj_val  : constr;
-  uj_type : types }
+type ('constr, 'types) punsafe_judgment = {
+  uj_val : 'constr;
+  uj_type : 'types }
 
-val make_judge : constr -> types -> unsafe_judgment
-val j_val  : unsafe_judgment -> constr
-val j_type : unsafe_judgment -> types
+type unsafe_judgment = (constr, types) punsafe_judgment
 
-type unsafe_type_judgment = {
-  utj_val  : constr;
+val make_judge : 'constr -> 'types -> ('constr, 'types) punsafe_judgment
+val j_val  : ('constr, 'types) punsafe_judgment -> 'constr
+val j_type : ('constr, 'types) punsafe_judgment -> 'types
+
+type 'types punsafe_type_judgment = {
+  utj_val : 'types;
   utj_type : sorts }
 
+type unsafe_type_judgment = types punsafe_type_judgment
 
 (** {6 Compilation of global declaration } *)
 
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index 5071f0ad5..5e1763815 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -13,52 +13,56 @@ open Reduction
 
 (* Type errors. *)
 
-type guard_error =
+type 'constr pguard_error =
   (* Fixpoints *)
   | NotEnoughAbstractionInFixBody
-  | RecursionNotOnInductiveType of constr
-  | RecursionOnIllegalTerm of int * (env * constr) * int list * int list
+  | RecursionNotOnInductiveType of 'constr
+  | RecursionOnIllegalTerm of int * (env * 'constr) * int list * int list
   | NotEnoughArgumentsForFixCall of int
   (* CoFixpoints *)
-  | CodomainNotInductiveType of constr
+  | CodomainNotInductiveType of 'constr
   | NestedRecursiveOccurrences
-  | UnguardedRecursiveCall of constr
-  | RecCallInTypeOfAbstraction of constr
-  | RecCallInNonRecArgOfConstructor of constr
-  | RecCallInTypeOfDef of constr
-  | RecCallInCaseFun of constr
-  | RecCallInCaseArg of constr
-  | RecCallInCasePred of constr
-  | NotGuardedForm of constr
-  | ReturnPredicateNotCoInductive of constr
+  | UnguardedRecursiveCall of 'constr
+  | RecCallInTypeOfAbstraction of 'constr
+  | RecCallInNonRecArgOfConstructor of 'constr
+  | RecCallInTypeOfDef of 'constr
+  | RecCallInCaseFun of 'constr
+  | RecCallInCaseArg of 'constr
+  | RecCallInCasePred of 'constr
+  | NotGuardedForm of 'constr
+  | ReturnPredicateNotCoInductive of 'constr
+
+type guard_error = constr pguard_error
 
 type arity_error =
   | NonInformativeToInformative
   | StrongEliminationOnNonSmallType
   | WrongArity
 
-type type_error =
+type ('constr, 'types) ptype_error =
   | UnboundRel of int
   | UnboundVar of variable
-  | NotAType of unsafe_judgment
-  | BadAssumption of unsafe_judgment
-  | ReferenceVariables of identifier * constr
-  | ElimArity of pinductive * sorts_family list * constr * unsafe_judgment
+  | NotAType of ('constr, 'types) punsafe_judgment
+  | BadAssumption of ('constr, 'types) punsafe_judgment
+  | ReferenceVariables of identifier * 'constr
+  | ElimArity of pinductive * sorts_family list * 'constr * ('constr, 'types) punsafe_judgment
       * (sorts_family * sorts_family * arity_error) option
-  | CaseNotInductive of unsafe_judgment
+  | CaseNotInductive of ('constr, 'types) punsafe_judgment
   | WrongCaseInfo of pinductive * case_info
-  | NumberBranches of unsafe_judgment * int
-  | IllFormedBranch of constr * pconstructor * constr * constr
-  | Generalization of (Name.t * types) * unsafe_judgment
-  | ActualType of unsafe_judgment * types
+  | NumberBranches of ('constr, 'types) punsafe_judgment * int
+  | IllFormedBranch of 'constr * pconstructor * 'constr * 'constr
+  | Generalization of (Name.t * 'types) * ('constr, 'types) punsafe_judgment
+  | ActualType of ('constr, 'types) punsafe_judgment * 'types
   | CantApplyBadType of
-      (int * constr * constr) * unsafe_judgment * unsafe_judgment array
-  | CantApplyNonFunctional of unsafe_judgment * unsafe_judgment array
-  | IllFormedRecBody of guard_error * Name.t array * int * env * unsafe_judgment array
+      (int * 'constr * 'constr) * ('constr, 'types) punsafe_judgment * ('constr, 'types) punsafe_judgment array
+  | CantApplyNonFunctional of ('constr, 'types) punsafe_judgment * ('constr, 'types) punsafe_judgment array
+  | IllFormedRecBody of 'constr pguard_error * Name.t array * int * env * ('constr, 'types) punsafe_judgment array
   | IllTypedRecBody of
-      int * Name.t array * unsafe_judgment array * types array
+      int * Name.t array * ('constr, 'types) punsafe_judgment array * 'types array
   | UnsatisfiedConstraints of Univ.constraints
 
+type type_error = (constr, types) ptype_error
+
 exception TypeError of env * type_error
 
 let nfj env {uj_val=c;uj_type=ct} =
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index 0c3a952b8..bd6032716 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -14,52 +14,56 @@ open Environ
 
 (*i Rem: NotEnoughAbstractionInFixBody should only occur with "/i" Fix
     notation i*)
-type guard_error =
+type 'constr pguard_error =
   (** Fixpoints *)
   | NotEnoughAbstractionInFixBody
-  | RecursionNotOnInductiveType of constr
-  | RecursionOnIllegalTerm of int * (env * constr) * int list * int list
+  | RecursionNotOnInductiveType of 'constr
+  | RecursionOnIllegalTerm of int * (env * 'constr) * int list * int list
   | NotEnoughArgumentsForFixCall of int
   (** CoFixpoints *)
-  | CodomainNotInductiveType of constr
+  | CodomainNotInductiveType of 'constr
   | NestedRecursiveOccurrences
-  | UnguardedRecursiveCall of constr
-  | RecCallInTypeOfAbstraction of constr
-  | RecCallInNonRecArgOfConstructor of constr
-  | RecCallInTypeOfDef of constr
-  | RecCallInCaseFun of constr
-  | RecCallInCaseArg of constr
-  | RecCallInCasePred of constr
-  | NotGuardedForm of constr
-  | ReturnPredicateNotCoInductive of constr
+  | UnguardedRecursiveCall of 'constr
+  | RecCallInTypeOfAbstraction of 'constr
+  | RecCallInNonRecArgOfConstructor of 'constr
+  | RecCallInTypeOfDef of 'constr
+  | RecCallInCaseFun of 'constr
+  | RecCallInCaseArg of 'constr
+  | RecCallInCasePred of 'constr
+  | NotGuardedForm of 'constr
+  | ReturnPredicateNotCoInductive of 'constr
+
+type guard_error = constr pguard_error
 
 type arity_error =
   | NonInformativeToInformative
   | StrongEliminationOnNonSmallType
   | WrongArity
 
-type type_error =
+type ('constr, 'types) ptype_error =
   | UnboundRel of int
   | UnboundVar of variable
-  | NotAType of unsafe_judgment
-  | BadAssumption of unsafe_judgment
-  | ReferenceVariables of identifier * constr
-  | ElimArity of pinductive * sorts_family list * constr * unsafe_judgment
+  | NotAType of ('constr, 'types) punsafe_judgment
+  | BadAssumption of ('constr, 'types) punsafe_judgment
+  | ReferenceVariables of identifier * 'constr
+  | ElimArity of pinductive * sorts_family list * 'constr * ('constr, 'types) punsafe_judgment
       * (sorts_family * sorts_family * arity_error) option
-  | CaseNotInductive of unsafe_judgment
+  | CaseNotInductive of ('constr, 'types) punsafe_judgment
   | WrongCaseInfo of pinductive * case_info
-  | NumberBranches of unsafe_judgment * int
-  | IllFormedBranch of constr * pconstructor * constr * constr
-  | Generalization of (Name.t * types) * unsafe_judgment
-  | ActualType of unsafe_judgment * types
+  | NumberBranches of ('constr, 'types) punsafe_judgment * int
+  | IllFormedBranch of 'constr * pconstructor * 'constr * 'constr
+  | Generalization of (Name.t * 'types) * ('constr, 'types) punsafe_judgment
+  | ActualType of ('constr, 'types) punsafe_judgment * 'types
   | CantApplyBadType of
-      (int * constr * constr) * unsafe_judgment * unsafe_judgment array
-  | CantApplyNonFunctional of unsafe_judgment * unsafe_judgment array
-  | IllFormedRecBody of guard_error * Name.t array * int * env * unsafe_judgment array
+      (int * 'constr * 'constr) * ('constr, 'types) punsafe_judgment * ('constr, 'types) punsafe_judgment array
+  | CantApplyNonFunctional of ('constr, 'types) punsafe_judgment * ('constr, 'types) punsafe_judgment array
+  | IllFormedRecBody of 'constr pguard_error * Name.t array * int * env * ('constr, 'types) punsafe_judgment array
   | IllTypedRecBody of
-      int * Name.t array * unsafe_judgment array * types array
+      int * Name.t array * ('constr, 'types) punsafe_judgment array * 'types array
   | UnsatisfiedConstraints of Univ.constraints
 
+type type_error = (constr, types) ptype_error
+
 exception TypeError of env * type_error
 
 val error_unbound_rel : env -> int -> 'a