Add a use_coercions flag to pretype_flags

Author: proux01

pretyping/coercion.ml

@@ -519,11 +519,12 @@ let reapply_coercions_body sigma trace body =
     start_app_body sigma body
 
 (* Try to coerce to a funclass; raise NoCoercion if not possible *)
-let inh_app_fun_core ~program_mode env sigma body typ =
+let inh_app_fun_core ~program_mode ?(use_coercions=true) env sigma body typ =
   match unify_product env sigma typ with
   | Inl sigma -> sigma, body, typ, IdCoe
   | Inr t ->
     try
+      if not use_coercions then raise NoCoercion;
       let p = lookup_path_to_fun_from env sigma typ in
       let body = force_app_body body in
       let sigma, body, typ, trace = apply_coercion env sigma p body typ in
@@ -541,13 +542,13 @@ let inh_app_fun_core ~program_mode env sigma body typ =
       else Exninfo.iraise (NoCoercion,info)
 
 (* Try to coerce to a funclass; returns [j] if no coercion is applicable *)
-let inh_app_fun ~program_mode ~resolve_tc env sigma body typ =
-  try inh_app_fun_core ~program_mode env sigma body typ
+let inh_app_fun ~program_mode ~resolve_tc ?use_coercions env sigma body typ =
+  try inh_app_fun_core ~program_mode ?use_coercions env sigma body typ
   with
   | NoCoercion when not resolve_tc
     || not (get_use_typeclasses_for_conversion ()) -> (sigma, body, typ, IdCoe)
   | NoCoercion ->
-    try inh_app_fun_core ~program_mode env (saturate_evd env sigma) body typ
+    try inh_app_fun_core ~program_mode ?use_coercions env (saturate_evd env sigma) body typ
     with NoCoercion -> (sigma, body, typ, IdCoe)
 
 let type_judgment env sigma j =
@@ -564,15 +565,16 @@ let inh_tosort_force ?loc env sigma ({ uj_val; uj_type } as j) =
   with Not_found | NoCoercion ->
     error_not_a_type ?loc env sigma j
 
-let inh_coerce_to_sort ?loc env sigma j =
+let inh_coerce_to_sort ?loc ?(use_coercions=true) env sigma j =
   let typ = whd_all env sigma j.uj_type in
     match EConstr.kind sigma typ with
     | Sort s -> (sigma,{ utj_val = j.uj_val; utj_type = ESorts.kind sigma s })
     | Evar ev ->
         let (sigma,s) = Evardefine.define_evar_as_sort env sigma ev in
           (sigma,{ utj_val = j.uj_val; utj_type = s })
     | _ ->
-        inh_tosort_force ?loc env sigma j
+        if use_coercions then inh_tosort_force ?loc env sigma j
+        else error_not_a_type ?loc env sigma j
 
 let inh_coerce_to_base ?loc ~program_mode env sigma j =
   if program_mode then
@@ -582,8 +584,8 @@ let inh_coerce_to_base ?loc ~program_mode env sigma j =
     sigma, res
   else (sigma, j)
 
-let inh_coerce_to_fail flags env sigma rigidonly v v_ty target_type =
-  if rigidonly && not (Heads.is_rigid env (EConstr.Unsafe.to_constr target_type) && Heads.is_rigid env (EConstr.Unsafe.to_constr v_ty))
+let inh_coerce_to_fail ?(use_coercions=true) flags env sigma rigidonly v v_ty target_type =
+  if not use_coercions || (rigidonly && not (Heads.is_rigid env (EConstr.Unsafe.to_constr target_type) && Heads.is_rigid env (EConstr.Unsafe.to_constr v_ty)))
   then
     raise NoCoercion
   else
@@ -601,10 +603,10 @@ let inh_coerce_to_fail flags env sigma rigidonly v v_ty target_type =
 let default_flags_of env =
   default_flags_of TransparentState.full
 
-let rec inh_conv_coerce_to_fail ?loc env sigma ?(flags=default_flags_of env) rigidonly v t c1 =
+let rec inh_conv_coerce_to_fail ?loc ?use_coercions env sigma ?(flags=default_flags_of env) rigidonly v t c1 =
   try (unify_leq_delay ~flags env sigma t c1, v, IdCoe)
   with UnableToUnify (best_failed_sigma,e) ->
-    try inh_coerce_to_fail flags env sigma rigidonly v t c1
+    try inh_coerce_to_fail ?use_coercions flags env sigma rigidonly v t c1
     with NoCoercion as exn ->
       let _, info = Exninfo.capture exn in
       match
@@ -624,21 +626,21 @@ let rec inh_conv_coerce_to_fail ?loc env sigma ?(flags=default_flags_of env) rig
           let open Context.Rel.Declaration in
           let env1 = push_rel (LocalAssum (name,u1)) env in
           let (sigma, v1, trace1) =
-            inh_conv_coerce_to_fail ?loc env1 sigma rigidonly
+            inh_conv_coerce_to_fail ?loc ?use_coercions env1 sigma rigidonly
               (mkRel 1) (lift 1 u1) (lift 1 t1) in
           let v2 = beta_applist sigma (lift 1 v,[v1]) in
           let t2 = Retyping.get_type_of env1 sigma v2 in
-          let (sigma,v2',trace2) = inh_conv_coerce_to_fail ?loc env1 sigma rigidonly v2 t2 u2 in
+          let (sigma,v2',trace2) = inh_conv_coerce_to_fail ?loc ?use_coercions env1 sigma rigidonly v2 t2 u2 in
           let trace = ProdCoe { na=name; ty=u1; dom=trace1; body=trace2 } in
           (sigma, mkLambda (name, u1, v2'), trace)
       | _ ->
         Exninfo.iraise (NoCoercionNoUnifier (best_failed_sigma,e), info)
 
 (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *)
-let inh_conv_coerce_to_gen ?loc ~program_mode ~resolve_tc rigidonly flags env sigma cj t =
+let inh_conv_coerce_to_gen ?loc ~program_mode ~resolve_tc ?use_coercions rigidonly flags env sigma cj t =
   let (sigma, val', otrace) =
     try
-      let (sigma, val', trace) = inh_conv_coerce_to_fail ?loc env sigma ~flags rigidonly cj.uj_val cj.uj_type t in
+      let (sigma, val', trace) = inh_conv_coerce_to_fail ?loc ?use_coercions env sigma ~flags rigidonly cj.uj_val cj.uj_type t in
       (sigma, val', Some trace)
     with NoCoercionNoUnifier (best_failed_sigma,e) as exn ->
       let _, info = Exninfo.capture exn in
@@ -659,15 +661,15 @@ let inh_conv_coerce_to_gen ?loc ~program_mode ~resolve_tc rigidonly flags env si
               error_actual_type ?loc ~info env best_failed_sigma cj t e
             else
               let sigma = sigma' in
-              let (sigma, val', trace) = inh_conv_coerce_to_fail ?loc env sigma rigidonly cj.uj_val cj.uj_type t in
+              let (sigma, val', trace) = inh_conv_coerce_to_fail ?loc ?use_coercions env sigma rigidonly cj.uj_val cj.uj_type t in
               (sigma, val', Some trace)
           with NoCoercionNoUnifier (_sigma,_error) as exn ->
             let _, info = Exninfo.capture exn in
             error_actual_type ?loc ~info env best_failed_sigma cj t e
   in
   (sigma,{ uj_val = val'; uj_type = t },otrace)
 
-let inh_conv_coerce_to ?loc ~program_mode ~resolve_tc env sigma ?(flags=default_flags_of env) =
-  inh_conv_coerce_to_gen ?loc ~program_mode ~resolve_tc false flags env sigma
-let inh_conv_coerce_rigid_to ?loc ~program_mode ~resolve_tc env sigma ?(flags=default_flags_of env) =
-  inh_conv_coerce_to_gen ?loc ~program_mode ~resolve_tc true flags env sigma
+let inh_conv_coerce_to ?loc ~program_mode ~resolve_tc ?use_coercions env sigma ?(flags=default_flags_of env) =
+  inh_conv_coerce_to_gen ?loc ~program_mode ~resolve_tc ?use_coercions false flags env sigma
+let inh_conv_coerce_rigid_to ?loc ~program_mode ~resolve_tc ?use_coercions env sigma ?(flags=default_flags_of env) =
+  inh_conv_coerce_to_gen ?loc ~program_mode ~resolve_tc ?use_coercions true flags env sigma

pretyping/coercion.mli

@@ -25,7 +25,7 @@ val reapply_coercions : evar_map -> coercion_trace -> EConstr.t -> EConstr.t
 (** [inh_coerce_to_sort env isevars j] coerces [j] to a type; i.e. it
     inserts a coercion into [j], if needed, in such a way it gets as
     type a sort; it fails if no coercion is applicable *)
-val inh_coerce_to_sort : ?loc:Loc.t ->
+val inh_coerce_to_sort : ?loc:Loc.t -> ?use_coercions:bool ->
   env -> evar_map -> unsafe_judgment -> evar_map * unsafe_type_judgment
 
 (** [inh_coerce_to_base env isevars j] coerces [j] to its base type; i.e. it
@@ -45,11 +45,11 @@ val remove_subset : env -> evar_map -> types -> types
     resort before failing) *)
 
 val inh_conv_coerce_to : ?loc:Loc.t -> program_mode:bool -> resolve_tc:bool ->
-  env -> evar_map -> ?flags:Evarconv.unify_flags ->
+  ?use_coercions:bool -> env -> evar_map -> ?flags:Evarconv.unify_flags ->
   unsafe_judgment -> types -> evar_map * unsafe_judgment * coercion_trace option
 
 val inh_conv_coerce_rigid_to : ?loc:Loc.t -> program_mode:bool -> resolve_tc:bool ->
-  env -> evar_map -> ?flags:Evarconv.unify_flags ->
+  ?use_coercions:bool -> env -> evar_map -> ?flags:Evarconv.unify_flags ->
   unsafe_judgment -> types -> evar_map * unsafe_judgment * coercion_trace option
 
 (** [inh_pattern_coerce_to loc env isevars pat ind1 ind2] coerces the Cases
@@ -74,5 +74,5 @@ val reapply_coercions_body : evar_map -> coercion_trace -> delayed_app_body -> d
     type a product; it returns [j] if no coercion is applicable.
     resolve_tc=false disables resolving type classes (as the last
     resort before failing) *)
-val inh_app_fun : program_mode:bool -> resolve_tc:bool ->
+val inh_app_fun : program_mode:bool -> resolve_tc:bool -> ?use_coercions:bool ->
   env -> evar_map -> delayed_app_body -> types -> evar_map * delayed_app_body * types * coercion_trace

pretyping/pretyping.ml

@@ -195,6 +195,7 @@ type pretype_flags = {
   poly : bool;
   resolve_tc : bool;
   program_mode : bool;
+  use_coercions : bool;
 }
 
 (* Compute the set of still-undefined initial evars up to restriction
@@ -355,10 +356,10 @@ let adjust_evar_source sigma na c =
   | _, _ -> sigma, c
 
 (* coerce to tycon if any *)
-let inh_conv_coerce_to_tycon ?loc ~flags:{ program_mode; resolve_tc } env sigma j = function
+let inh_conv_coerce_to_tycon ?loc ~flags:{ program_mode; resolve_tc; use_coercions } env sigma j = function
   | None -> sigma, j, Some Coercion.empty_coercion_trace
   | Some t ->
-    Coercion.inh_conv_coerce_to ?loc ~program_mode ~resolve_tc !!env sigma j t
+    Coercion.inh_conv_coerce_to ?loc ~program_mode ~resolve_tc ~use_coercions !!env sigma j t
 
 let check_instance subst = function
   | [] -> ()
@@ -840,7 +841,7 @@ struct
           sigma, body, na, c1, subs, c2, Coercion.empty_coercion_trace
         | _ ->
           let typ = Vars.esubst Vars.lift_substituend subs typ in
-          let sigma, body, typ, trace = Coercion.inh_app_fun ~program_mode:flags.program_mode ~resolve_tc:flags.resolve_tc !!env sigma body typ in
+          let sigma, body, typ, trace = Coercion.inh_app_fun ~program_mode:flags.program_mode ~resolve_tc:flags.resolve_tc ~use_coercions:flags.use_coercions !!env sigma body typ in
           let resty = whd_all !!env sigma typ in
           let na, c1, c2 = match EConstr.kind sigma resty with
           | Prod (na, c1, c2) -> (na, c1, c2)
@@ -923,7 +924,7 @@ struct
   let pretype_lambda self (name, bk, c1, c2) =
     fun ?loc ~flags tycon env sigma ->
     let open Context.Rel.Declaration in
-    let tycon' = if flags.program_mode
+    let tycon' = if flags.program_mode && flags.use_coercions
       then Option.map (Coercion.remove_subset !!env sigma) tycon
       else tycon
     in
@@ -1256,16 +1257,18 @@ let pretype_type self c ?loc ~flags valcon (env : GlobEnv.t) sigma = match DAst.
   | _ ->
       let sigma, j = eval_pretyper self ~flags empty_tycon env sigma c in
       let loc = loc_of_glob_constr c in
-      let sigma, tj = Coercion.inh_coerce_to_sort ?loc !!env sigma j in
-        match valcon with
-        | None -> sigma, tj
-        | Some v ->
-          begin match Evarconv.unify_leq_delay !!env sigma v tj.utj_val with
-            | sigma -> sigma, tj
-            | exception Evarconv.UnableToUnify (sigma,e) ->
-              error_unexpected_type
-                ?loc:(loc_of_glob_constr c) !!env sigma tj.utj_val v e
-          end
+      let sigma, tj =
+        let use_coercions = flags.use_coercions in
+        Coercion.inh_coerce_to_sort ?loc ~use_coercions !!env sigma j in
+      match valcon with
+      | None -> sigma, tj
+      | Some v ->
+        begin match Evarconv.unify_leq_delay !!env sigma v tj.utj_val with
+        | sigma -> sigma, tj
+        | exception Evarconv.UnableToUnify (sigma,e) ->
+          error_unexpected_type
+            ?loc:(loc_of_glob_constr c) !!env sigma tj.utj_val v e
+        end
 
   let pretype_int self i =
     fun ?loc ~flags tycon env sigma ->
@@ -1358,6 +1361,7 @@ let ise_pretype_gen (flags : inference_flags) env sigma lvar kind c =
   let pretype_flags = {
     program_mode = flags.program_mode;
     poly = flags.polymorphic;
+    use_coercions = true;
     resolve_tc = match flags.use_typeclasses with
       | NoUseTC -> false
       | UseTC | UseTCForConv -> true

pretyping/pretyping.mli

@@ -144,6 +144,7 @@ type pretype_flags = {
   poly : bool;
   resolve_tc : bool;
   program_mode : bool;
+  use_coercions : bool;
 }
 
 type 'a pretype_fun = ?loc:Loc.t -> flags:pretype_flags -> Evardefine.type_constraint -> GlobEnv.t -> evar_map -> evar_map * 'a