Nicer error for bad primitive types (through type_errors etc)

4 files changed, 17 insertions, 14 deletions

diff --git a/kernel/cPrimitives.ml b/kernel/cPrimitives.ml
index da5c4fb07b..fdc93cfa89 100644
--- a/kernel/cPrimitives.ml
+++ b/kernel/cPrimitives.ml
@@ -148,7 +148,7 @@ let prim_ind_to_string = function
   | PIT_cmp -> "cmp"
 
 let prim_type_to_string = function
-  | PT_int63 -> "int63"
+  | PT_int63 -> "int63_type"
 
 let op_or_type_to_string = function
   | OT_op op -> to_string op
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index 964d32c6b3..481ffc290c 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -55,6 +55,7 @@ type ('constr, 'types) ptype_error =
   | IllFormedBranch of 'constr * pconstructor * 'constr * 'constr
   | Generalization of (Name.t * 'types) * ('constr, 'types) punsafe_judgment
   | ActualType of ('constr, 'types) punsafe_judgment * 'types
+  | IncorrectPrimitive of (CPrimitives.op_or_type,'types) punsafe_judgment * 'types
   | CantApplyBadType of
       (int * 'constr * 'constr) * ('constr, 'types) punsafe_judgment * ('constr, 'types) punsafe_judgment array
   | CantApplyNonFunctional of ('constr, 'types) punsafe_judgment * ('constr, 'types) punsafe_judgment array
@@ -120,6 +121,9 @@ let error_generalization env nvar c =
 let error_actual_type env j expty =
   raise (TypeError (env, ActualType (j,expty)))
 
+let error_incorrect_primitive env p t =
+  raise (TypeError (env, IncorrectPrimitive (p, t)))
+
 let error_cant_apply_not_functional env rator randl =
   raise (TypeError (env, CantApplyNonFunctional (rator,randl)))
 
@@ -175,6 +179,7 @@ let map_ptype_error f = function
 | IllFormedBranch (c, pc, t1, t2) -> IllFormedBranch (f c, pc, f t1, f t2)
 | Generalization ((na, t), j) -> Generalization ((na, f t), on_judgment f j)
 | ActualType (j, t) -> ActualType (on_judgment f j, f t)
+| IncorrectPrimitive (p, t) -> IncorrectPrimitive ({p with uj_type=f p.uj_type}, f t)
 | CantApplyBadType ((n, c1, c2), j, vj) ->
   CantApplyBadType ((n, f c1, f c2), on_judgment f j, Array.map (on_judgment f) vj)
 | CantApplyNonFunctional (j, jv) -> CantApplyNonFunctional (on_judgment f j, Array.map (on_judgment f) jv)
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index 4b832930e1..c5ab9a4e73 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -56,6 +56,7 @@ type ('constr, 'types) ptype_error =
   | IllFormedBranch of 'constr * pconstructor * 'constr * 'constr
   | Generalization of (Name.t * 'types) * ('constr, 'types) punsafe_judgment
   | ActualType of ('constr, 'types) punsafe_judgment * 'types
+  | IncorrectPrimitive of (CPrimitives.op_or_type,'types) punsafe_judgment * 'types
   | CantApplyBadType of
       (int * 'constr * 'constr) * ('constr, 'types) punsafe_judgment * ('constr, 'types) punsafe_judgment array
   | CantApplyNonFunctional of ('constr, 'types) punsafe_judgment * ('constr, 'types) punsafe_judgment array
@@ -112,6 +113,8 @@ val error_generalization : env -> Name.t * types -> unsafe_judgment -> 'a
 
 val error_actual_type : env -> unsafe_judgment -> types -> 'a
 
+val error_incorrect_primitive : env -> (CPrimitives.op_or_type,types) punsafe_judgment -> types -> 'a
+
 val error_cant_apply_not_functional :
   env -> unsafe_judgment -> unsafe_judgment array -> 'a
 
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 7eb8e803b3..227a164549 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -252,6 +252,11 @@ let type_of_prim env t =
   in
   nary_int63_op (CPrimitives.arity t) return_ty
 
+let type_of_prim_or_type env = let open CPrimitives in
+  function
+  | OT_type t -> type_of_prim_type env t
+  | OT_op op -> type_of_prim env op
+
 let judge_of_int env i =
   make_judge (Constr.mkInt i) (type_of_int env)
 
@@ -664,17 +669,7 @@ let judge_of_case env ci pj cj lfj =
 
 (* Building type of primitive operators and type *)
 
-open CPrimitives
-
 let check_primitive_type env op_t t =
-  match op_t with
-  | OT_type PT_int63 ->
-    (try
-      default_conv ~l2r:false CUMUL env mkSet t
-    with NotConvertible ->
-      CErrors.user_err Pp.(str"Was expecting the sort of this primitive type to be Set"))
-  | OT_op p ->
-    (try
-      default_conv ~l2r:false CUMUL env (type_of_prim env p) t
-    with NotConvertible ->
-      CErrors.user_err Pp.(str"Not the expected type for this primitive"))
+  let inft = type_of_prim_or_type env op_t in
+  try default_conv ~l2r:false CUMUL env inft t
+  with NotConvertible -> error_incorrect_primitive env (make_judge op_t inft) t