Making detyping potentially lazy.

The internal detype function takes an additional arguments dictating
whether it should be eager or lazy.

We introduce a new type of delayed `DAst.t` AST nodes and use it for
`glob_constr`.

Such type, instead of only containing a value, it can contain a lazy
computation too. We use a GADT to discriminate between both uses
statically, so that no delayed terms ever happen to be
marshalled (which would raise anomalies).

We also fix a regression in the test-suite:

  Mixing laziness and effects is a well-known hell. Here, an exception
  that was raised for mere control purpose was delayed and raised at a
  later time as an anomaly. We make the offending function eager.

1 files changed, 5 insertions, 4 deletions

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 40b8bcad9..79d2c3333 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -572,7 +572,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
   let pretype = pretype k0 resolve_tc in
   let open Context.Rel.Declaration in
   let loc = t.CAst.loc in
-  match t.CAst.v with
+  match DAst.get t with
   | GRef (ref,u) ->
       inh_conv_coerce_to_tycon ?loc env evdref
 	(pretype_ref ?loc evdref env ref u)
@@ -1100,8 +1100,9 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update =
   Array.map_of_list snd subst
 
 (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *)
-and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function
-  | { loc; CAst.v = GHole (knd, naming, None) } ->
+and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar c = match DAst.get c with
+  | GHole (knd, naming, None) ->
+      let loc = loc_of_glob_constr c in
       let rec is_Type c = match EConstr.kind !evdref c with
       | Sort s ->
         begin match ESorts.kind !evdref s with
@@ -1134,7 +1135,7 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function
 	   let s = evd_comb0 (new_sort_variable univ_flexible_alg) evdref in
 	     { utj_val = e_new_evar env evdref ~src:(loc, knd) ~naming (mkSort s);
 	       utj_type = s})
-  | c ->
+  | _ ->
       let j = pretype k0 resolve_tc empty_tycon env evdref lvar c in
       let loc = loc_of_glob_constr c in
       let tj = evd_comb1 (Coercion.inh_coerce_to_sort ?loc env.ExtraEnv.env) evdref j in