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.

7 files changed, 75 insertions, 56 deletions

diff --git a/plugins/ssr/ssrbwd.ml b/plugins/ssr/ssrbwd.ml
index cc0e86684..c29a1fe7c 100644
--- a/plugins/ssr/ssrbwd.ml
+++ b/plugins/ssr/ssrbwd.ml
@@ -42,10 +42,10 @@ let interp_agen ist gl ((goclr, _), (k, gc as c)) (clr, rcs) =
   | Some ghyps ->
     let clr' = snd (interp_hyps ist gl ghyps) @ clr in
     if k <> xNoFlag then clr', rcs' else
-    let open CAst in
-    match rc with
-    | { loc; v = GVar id } when not_section_id id -> SsrHyp (Loc.tag ?loc id) :: clr', rcs'
-    | { loc; v = GRef (VarRef id, _) } when not_section_id id ->
+    let loc = rc.CAst.loc in
+    match DAst.get rc with
+    | GVar id when not_section_id id -> SsrHyp (Loc.tag ?loc id) :: clr', rcs'
+    | GRef (VarRef id, _) when not_section_id id ->
         SsrHyp (Loc.tag ?loc id) :: clr', rcs'
     | _ -> clr', rcs'
 
@@ -68,9 +68,8 @@ let pf_match = pf_apply (fun e s c t -> understand_tcc e s ~expected_type:t c)
 
 let apply_rconstr ?ist t gl =
 (* ppdebug(lazy(str"sigma@apply_rconstr=" ++ pr_evar_map None (project gl))); *)
-  let open CAst in
-  let n = match ist, t with
-    | None, { v = GVar id | GRef (VarRef id,_) } -> pf_nbargs gl (EConstr.mkVar id)
+  let n = match ist, DAst.get t with
+    | None, (GVar id | GRef (VarRef id,_)) -> pf_nbargs gl (EConstr.mkVar id)
     | Some ist, _ -> interp_nbargs ist gl t
     | _ -> anomaly "apply_rconstr without ist and not RVar" in
   let mkRlemma i = mkRApp t (mkRHoles i) in
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 799e969ae..cf5fdf318 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -176,24 +176,26 @@ open Globnames
 open Misctypes
 open Decl_kinds
 
-let mkRHole = CAst.make @@ GHole (Evar_kinds.InternalHole, IntroAnonymous, None)
+let mkRHole = DAst.make @@ GHole (Evar_kinds.InternalHole, IntroAnonymous, None)
 
 let rec mkRHoles n = if n > 0 then mkRHole :: mkRHoles (n - 1) else []
-let rec isRHoles = function { CAst.v = GHole _ } :: cl -> isRHoles cl | cl -> cl = []
-let mkRApp f args = if args = [] then f else CAst.make @@ GApp (f, args)
-let mkRVar id = CAst.make @@ GRef (VarRef id,None)
-let mkRltacVar id = CAst.make @@ GVar (id)
-let mkRCast rc rt =  CAst.make @@ GCast (rc, CastConv rt)
-let mkRType =  CAst.make @@ GSort (GType [])
-let mkRProp =  CAst.make @@ GSort (GProp)
-let mkRArrow rt1 rt2 = CAst.make @@ GProd (Anonymous, Explicit, rt1, rt2)
-let mkRConstruct c = CAst.make @@ GRef (ConstructRef c,None)
-let mkRInd mind = CAst.make @@ GRef (IndRef mind,None)
-let mkRLambda n s t = CAst.make @@ GLambda (n, Explicit, s, t)
+let rec isRHoles cl = match cl with
+| [] -> true
+| c :: l -> match DAst.get c with GHole _ -> isRHoles l | _ -> false
+let mkRApp f args = if args = [] then f else DAst.make @@ GApp (f, args)
+let mkRVar id = DAst.make @@ GRef (VarRef id,None)
+let mkRltacVar id = DAst.make @@ GVar (id)
+let mkRCast rc rt =  DAst.make @@ GCast (rc, CastConv rt)
+let mkRType =  DAst.make @@ GSort (GType [])
+let mkRProp =  DAst.make @@ GSort (GProp)
+let mkRArrow rt1 rt2 = DAst.make @@ GProd (Anonymous, Explicit, rt1, rt2)
+let mkRConstruct c = DAst.make @@ GRef (ConstructRef c,None)
+let mkRInd mind = DAst.make @@ GRef (IndRef mind,None)
+let mkRLambda n s t = DAst.make @@ GLambda (n, Explicit, s, t)
 
 let rec mkRnat n =
-  if n <= 0 then CAst.make @@ GRef (Coqlib.glob_O, None) else
-  mkRApp (CAst.make @@ GRef (Coqlib.glob_S, None)) [mkRnat (n - 1)]
+  if n <= 0 then DAst.make @@ GRef (Coqlib.glob_O, None) else
+  mkRApp (DAst.make @@ GRef (Coqlib.glob_S, None)) [mkRnat (n - 1)]
 
 let glob_constr ist genv = function
   | _, Some ce ->
@@ -710,7 +712,7 @@ let mkSsrRef name =
   try locate_reference (ssrqid name) with Not_found ->
   try locate_reference (ssrtopqid name) with Not_found ->
   CErrors.user_err (Pp.str "Small scale reflection library not loaded")
-let mkSsrRRef name = (CAst.make @@ GRef (mkSsrRef name,None)), None
+let mkSsrRRef name = (DAst.make @@ GRef (mkSsrRef name,None)), None
 let mkSsrConst name env sigma =
   EConstr.fresh_global env sigma (mkSsrRef name)
 let pf_mkSsrConst name gl =
@@ -845,10 +847,10 @@ let pf_interp_ty ?(resolve_typeclasses=false) ist gl ty =
    let n_binders = ref 0 in
    let ty = match ty with
    | a, (t, None) ->
-    let rec force_type ty = CAst.(map (function
+    let rec force_type ty = DAst.(map (function
      | GProd (x, k, s, t) -> incr n_binders; GProd (x, k, s, force_type t)
      | GLetIn (x, v, oty, t) -> incr n_binders; GLetIn (x, v, oty, force_type t)
-     | _ -> (mkRCast ty mkRType).v)) ty in
+     | _ -> DAst.get (mkRCast ty mkRType))) ty in
      a, (force_type t, None)
    | _, (_, Some ty) ->
     let rec force_type ty = CAst.(map (function
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index ab6a60f4e..8b69c3435 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -129,7 +129,7 @@ let newssrcongrtac arg ist gl =
     let eq, gl = pf_fresh_global (Coqlib.build_coq_eq ()) gl in
     pf_saturate gl (EConstr.of_constr eq) 3 in
   tclMATCH_GOAL (equality, gl') (fun gl' -> fs gl' (List.assoc 0 eq_args))
-  (fun ty -> congrtac (arg, Detyping.detype false [] (pf_env gl) (project gl) ty) ist)
+  (fun ty -> congrtac (arg, Detyping.detype Detyping.Now false [] (pf_env gl) (project gl) ty) ist)
   (fun () ->
     let lhs, gl' = mk_evar gl EConstr.mkProp in let rhs, gl' = mk_evar gl' EConstr.mkProp in
     let arrow = EConstr.mkArrow lhs (EConstr.Vars.lift 1 rhs) in
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index 8e6329a15..d01bdc1b9 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -184,9 +184,13 @@ let havetac ist
       mkt ct, mkt cty, mkt (mkCHole None), loc
     | _, (_, Some ct) ->
       mkt ct, mkt (mkCHole None), mkt (mkCHole None), None
-    | _, ({ loc; v = GCast (ct, CastConv cty) }, None) ->
-      mkl ct, mkl cty, mkl mkRHole, loc
-    | _, (t, None) -> mkl t, mkl mkRHole, mkl mkRHole, None in
+    | _, (t, None) ->
+      begin match DAst.get t with
+      | GCast (ct, CastConv cty) ->
+        mkl ct, mkl cty, mkl mkRHole, t.CAst.loc
+      | _ -> mkl t, mkl mkRHole, mkl mkRHole, None
+      end
+  in
   let gl, cut, sol, itac1, itac2 =
    match fk, namefst, suff with
    | FwdHave, true, true ->
@@ -323,11 +327,18 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl =
   let mkpats = function
   | _, Some ((x, _), _) -> fun pats -> IPatId (hoi_id x) :: pats
   | _ -> fun x -> x in
-  let open CAst in
   let ct = match ct with
-  | (a, (b, Some { v = CCast (_, CastConv cty)})) -> a, (b, Some cty)
-  | (a, ({ v = GCast (_, CastConv cty) }, None)) -> a, (cty, None)
-  | _ -> anomaly "wlog: ssr cast hole deleted by typecheck" in
+  | (a, (b, Some ct)) ->
+    begin match ct.CAst.v with
+    | CCast (_, CastConv cty) -> a, (b, Some cty)
+    | _ -> anomaly "wlog: ssr cast hole deleted by typecheck"
+    end
+  | (a, (t, None)) ->
+    begin match DAst.get t with
+    | GCast (_, CastConv cty) -> a, (cty, None)
+    | _ -> anomaly "wlog: ssr cast hole deleted by typecheck"
+    end
+  in
   let cut_implies_goal = not (suff || ghave <> `NoGen) in
   let c, args, ct, gl =
     let gens = List.filter (function _, Some _ -> true | _ -> false) gens in
@@ -398,11 +409,18 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl =
 
 let sufftac ist ((((clr, pats),binders),simpl), ((_, c), hint)) =
   let htac = Tacticals.tclTHEN (introstac ~ist pats) (hinttac ist true hint) in
-  let open CAst in
   let c = match c with
-  | (a, (b, Some { v = CCast (_, CastConv cty)})) -> a, (b, Some cty)
-  | (a, ({ v = GCast (_, CastConv cty) }, None)) -> a, (cty, None)
-  | _ -> anomaly "suff: ssr cast hole deleted by typecheck" in
+  | (a, (b, Some ct)) ->
+    begin match ct.CAst.v with
+    | CCast (_, CastConv cty) -> a, (b, Some cty)
+    | _ -> anomaly "suff: ssr cast hole deleted by typecheck"
+    end
+  | (a, (t, None)) ->
+    begin match DAst.get t with
+    | GCast (_, CastConv cty) -> a, (cty, None)
+    | _ -> anomaly "suff: ssr cast hole deleted by typecheck"
+    end
+  in
   let ctac gl =
     let _,ty,_,uc = pf_interp_ty ist gl c in let gl = pf_merge_uc uc gl in
     basecuttac "ssr_suff" ty gl in
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index db1981228..060225dab 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -342,7 +342,7 @@ let interp_index ist gl idx =
         | None ->
         begin match Tacinterp.Value.to_constr v with
         | Some c ->
-          let rc = Detyping.detype false [] (pf_env gl) (project gl) c in
+          let rc = Detyping.detype Detyping.Now false [] (pf_env gl) (project gl) c in
           begin match Notation.uninterp_prim_token rc with
           | _, Constrexpr.Numeral (s,b) ->
              let n = int_of_string s in if b then n else -n
@@ -1062,32 +1062,32 @@ let rec format_glob_decl h0 d0 = match h0, d0 with
      Bdef (x, None, v) :: format_glob_decl [] d
   | _, [] -> []
 
-let rec format_glob_constr h0 c0 = let open CAst in match h0, c0 with
-  | BFvar :: h, { v = GLambda (x, _, _, c) } ->
+let rec format_glob_constr h0 c0 = match h0, DAst.get c0 with
+  | BFvar :: h, GLambda (x, _, _, c) ->
     let bs, c' = format_glob_constr h c in
     Bvar x :: bs, c'
-  | BFdecl 1 :: h, { v = GLambda (x, _, t, c) } ->
+  | BFdecl 1 :: h, GLambda (x, _, t, c) ->
     let bs, c' = format_glob_constr h c in
     Bdecl ([x], t) :: bs, c'
-  | BFdecl n :: h, { v = GLambda (x, _, t, c) } when n > 1 ->
+  | BFdecl n :: h, GLambda (x, _, t, c) when n > 1 ->
     begin match format_glob_constr (BFdecl (n - 1) :: h) c with
     | Bdecl (xs, _) :: bs, c' -> Bdecl (x :: xs, t) :: bs, c'
     | _ -> [Bdecl ([x], t)], c
     end
-  | BFdef :: h, { v = GLetIn(x, v, oty, c) } ->
+  | BFdef :: h, GLetIn(x, v, oty, c) ->
     let bs, c' = format_glob_constr h c in
     Bdef (x, oty, v) :: bs, c'
-  | [BFcast], { v = GCast (c, CastConv t) } ->
+  | [BFcast], GCast (c, CastConv t) ->
     [Bcast t], c
-  | BFrec (has_str, has_cast) :: h, { v = GRec (f, _, bl, t, c) }
+  | BFrec (has_str, has_cast) :: h, GRec (f, _, bl, t, c)
       when Array.length c = 1 ->
     let bs = format_glob_decl h bl.(0) in
     let bstr = match has_str, f with
     | true, GFix ([|Some i, GStructRec|], _) -> mkBstruct i bs
     | _ -> [] in
     bs @ bstr @ (if has_cast then [Bcast t.(0)] else []), c.(0)
-  | _, c ->
-    [], c
+  | _, _ ->
+    [], c0
 
 (** Forward chaining argument *)
 
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4
index 9c59d83d4..507b4631b 100644
--- a/plugins/ssr/ssrvernac.ml4
+++ b/plugins/ssr/ssrvernac.ml4
@@ -292,7 +292,7 @@ let interp_search_notation ?loc tag okey =
     err (pr_ntn ntn ++ str " is an n-ary notation");
   let nvars = List.filter (fun (_,(_,typ)) -> typ = NtnTypeConstr) nvars in
   let rec sub () = function
-  | NVar x when List.mem_assoc x nvars -> CAst.make ?loc @@ GPatVar (FirstOrderPatVar x)
+  | NVar x when List.mem_assoc x nvars -> DAst.make ?loc @@ GPatVar (FirstOrderPatVar x)
   | c ->
     glob_constr_of_notation_constr_with_binders ?loc (fun _ x -> (), x) sub () c in
   let _, npat = Patternops.pattern_of_glob_constr (sub () body) in
@@ -467,10 +467,10 @@ let pr_raw_ssrhintref prc _ _ = let open CAst in function
     prc c ++ str "|" ++ int (List.length args)
   | c -> prc c
 
-let pr_rawhintref = let open CAst in function
-  | { v = GApp (f, args) } when isRHoles args ->
+let pr_rawhintref c = match DAst.get c with
+  | GApp (f, args) when isRHoles args ->
     pr_glob_constr f ++ str "|" ++ int (List.length args)
-  | c -> pr_glob_constr c
+  | _ -> pr_glob_constr c
 
 let pr_glob_ssrhintref _ _ _ (c, _) = pr_rawhintref c
 
diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml
index 338ecccc2..61b65e347 100644
--- a/plugins/ssr/ssrview.ml
+++ b/plugins/ssr/ssrview.ml
@@ -59,13 +59,13 @@ let glob_view_hints lvh =
 
 let add_view_hints lvh i = Lib.add_anonymous_leaf (in_viewhint (i, lvh))
 
-let interp_view ist si env sigma gv v rid =
-  let open CAst in
-  match v with
-  | { v = GApp ( { v = GHole _ } , rargs); loc } ->
-    let rv = make ?loc @@ GApp (rid, rargs) in
+let interp_view ist si env sigma gv rv rid =
+  match DAst.get rv with
+  | GApp (h, rargs) when (match DAst.get h with GHole _ -> true | _ -> false) ->
+    let loc = rv.CAst.loc in
+    let rv = DAst.make ?loc @@ GApp (rid, rargs) in
     snd (interp_open_constr ist (re_sig si sigma) (rv, None))
-  | rv ->
+  | _ ->
   let interp rc rargs =
     interp_open_constr ist (re_sig si sigma) (mkRApp rc rargs, None) in
   let rec simple_view rargs n =