From 18e0103e33b276a88000dde8fccc772af2ca67ea Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 9 Feb 2020 06:48:07 +0100
Subject: Reinforcing the role of type "typing_constraint".

WithoutTypeConstraint says it can be a term. In particular, if it has
manual implicit arguments, these will be allowed only in leading
lambdas. I.e. it can start with "fun {x}" but not with "forall {x}".

New constructor UnknownIfTermOrType allows to be both a term or a
type. In particular, if it allowed start both with "fun {x}" and
"forall {x}".
---
 pretyping/pretyping.ml  | 4 ++--
 pretyping/pretyping.mli | 6 +++++-
 2 files changed, 7 insertions(+), 3 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index cb0c4868b5..2d98d48aa0 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -47,7 +47,7 @@ open Evarconv
 
 module NamedDecl = Context.Named.Declaration
 
-type typing_constraint = OfType of types | IsType | WithoutTypeConstraint
+type typing_constraint = UnknownIfTermOrType | IsType | OfType of types | WithoutTypeConstraint
 
 let (!!) env = GlobEnv.env env
 
@@ -1290,7 +1290,7 @@ let ise_pretype_gen flags env sigma lvar kind c =
   in
   let env = GlobEnv.make ~hypnaming env sigma lvar in
   let sigma', c', c'_ty = match kind with
-    | WithoutTypeConstraint ->
+    | WithoutTypeConstraint | UnknownIfTermOrType ->
       let sigma, j = pretype ~program_mode ~poly flags.use_typeclasses empty_tycon env sigma c in
       sigma, j.uj_val, j.uj_type
     | OfType exptyp ->
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 18e416596e..ee57f690a1 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -38,7 +38,11 @@ val interp_known_glob_level : ?loc:Loc.t -> Evd.evar_map ->
 val search_guard :
   ?loc:Loc.t -> env -> int list list -> Constr.rec_declaration -> int array
 
-type typing_constraint = OfType of types | IsType | WithoutTypeConstraint
+type typing_constraint =
+  | UnknownIfTermOrType (** E.g., unknown if manual implicit arguments allowed *)
+  | IsType (** Necessarily a type *)
+  | OfType of types (** A term of the expected type *)
+  | WithoutTypeConstraint (** A term of unknown expected type *)
 
 type inference_hook = env -> evar_map -> Evar.t -> evar_map * constr
 
-- 
cgit v1.2.3