Revert "Factor lift_existT into expr_to_pattern_and_replacement_unfol…

…ded{,_split} in reify_to_pattern_and_replacement_in_context"

This reverts commit 499ea11.

It seems to break fiat-crypto

src/Rewriter/Rewriter/Reify.v

@@ -202,10 +202,9 @@ Module Compilers.
                          else None))).
 
         (** N.B. We must annotate the type of [invalid] to relax universe constraints *)
-        Definition expr_to_pattern_and_replacement_unfolded_split gets_inlined should_do_again evm {t} lhs rhs side_conditions
+        Definition expr_to_pattern_and_replacement_unfolded gets_inlined should_do_again evm {t} lhs rhs side_conditions (invalid : forall A B : Type, A -> B)
           := Eval cbv beta iota delta [expr_to_pattern_and_replacement lookup_expr_gets_inlined pattern_of_expr lam_unification_resultT' Pos.succ pair'_unification_resultT' PositiveMap.empty PositiveMap.fold Pos.max expr_pos_to_expr_value (* expr_value_to_rewrite_rule_replacement*) fold_left List.rev List.app value PositiveMap.add PositiveMap.xfoldi Pos.compare Pos.compare_cont FMapPositive.append projT1 projT2 PositiveMap.find Base_value (*UnderLets.map reify_expr_beta_iota reflect_expr_beta_iota*) lam_type_of_list fold_right list_rect pattern.type.relax pattern.type.subst_default pattern.type.subst_default_relax pattern.type.unsubst_default_relax option_map unification_resultT' with_unification_resultT' with_unif_rewrite_ruleTP_gen']
-            in let f := fun (invalid : forall A B : Type, A -> B) => @expr_to_pattern_and_replacement gets_inlined should_do_again evm invalid t lhs rhs side_conditions in
-               existT _ (fun invalid => projT1 (f invalid)) (fun invalid => projT2 (f invalid)).
+            in @expr_to_pattern_and_replacement gets_inlined should_do_again evm invalid t lhs rhs side_conditions.
 
         Definition partial_lam_unif_rewrite_ruleTP_gen_unfolded should_do_again {t} p
           := Eval cbv beta iota delta [partial_lam_unif_rewrite_ruleTP_gen pattern.collect_vars pattern.type.lam_forall_vars partial_lam_unification_resultT pattern.type.collect_vars pattern.base.collect_vars PositiveSet.union PositiveSet.add PositiveSet.empty pattern.type.lam_forall_vars_gen List.rev PositiveSet.elements PositiveSet.xelements PositiveSet.rev PositiveSet.rev_append List.app orb fold_right PositiveMap.add PositiveMap.empty]
@@ -828,6 +827,8 @@ Module Compilers.
           (fun () => Control.refine
                        (fun () => adjust_side_conditions_for_gets_inlined' value_ctx side_conditions (mkVar lookup_gets_inlined))).
 
+      Definition lift_existT {X A B} (v : forall x : X, @sigT (A x) (B x))
+        := Eval cbv [projT1 projT2] in existT _ (fun x => projT1 (v x)) (fun x => projT2 (v x)).
       Ltac2 rec reify_to_pattern_and_replacement_in_context (base : constr) (reify_base : constr -> constr) (base_interp : constr) (base_interp_beq : constr) (try_make_transport_base_cps : constr) (ident : constr) (reify_ident_opt : binder list -> constr -> constr option) (pident : constr) (pident_arg_types : constr) (pident_type_of_list_arg_types_beq : constr) (pident_of_typed_ident : constr) (pident_arg_types_of_typed_ident : constr) (reflect_ident_iota : constr) (avoid : Fresh.Free.t) (type_ctx : constr) (var : constr) (gets_inlined : constr) (should_do_again : constr) (cur_i : constr) (term : constr) (value_ctx : (ident * constr (* ty *) * constr (* var *)) list) : constr :=
         Reify.debug_wrap
           "reify_to_pattern_and_replacement_in_context" Message.of_constr term
@@ -858,7 +859,7 @@ Module Compilers.
                    | (@eq ?t ?a ?b, ?side_conditions)
                      => let base_interp_head := head_reference base_interp in
                         let var_pos := '(fun _ : type $base_type => positive) in
-                        let cexpr_to_pattern_and_replacement_unfolded_split := debug_Constr_check (fun () => mkApp '@expr_to_pattern_and_replacement_unfolded_split [base; try_make_transport_base_cps; ident; var; pident; pident_arg_types; pident_type_of_list_arg_types_beq; pident_of_typed_ident; pident_arg_types_of_typed_ident; mkApp reflect_ident_iota [var]; gets_inlined; should_do_again; type_ctx]) in
+                        let cexpr_to_pattern_and_replacement_unfolded := debug_Constr_check (fun () => mkApp '@expr_to_pattern_and_replacement_unfolded [base; try_make_transport_base_cps; ident; var; pident; pident_arg_types; pident_type_of_list_arg_types_beq; pident_of_typed_ident; pident_arg_types_of_typed_ident; mkApp reflect_ident_iota [var]; gets_inlined; should_do_again; type_ctx]) in
                         let cpartial_lam_unif_rewrite_ruleTP_gen := debug_Constr_check (fun () => mkApp '@partial_lam_unif_rewrite_ruleTP_gen_unfolded [base; ident; var; pident; pident_arg_types; should_do_again]) in
                         let value := debug_Constr_check (fun () => mkApp '@value [base_type; ident; var]) in
                         let cinvalidT := '(forall A B : Type, A -> B) in
@@ -879,17 +880,17 @@ Module Compilers.
                         let rA := expr.reify_in_context base_type ident reify_base_type reify_ident_opt var_pos a [] [] value_ctx [] None in
                         let rB := expr.reify_in_context base_type ident reify_base_type reify_ident_opt var_pos b [] [] value_ctx [] None in
                         let side_conditions := adjust_side_conditions_for_gets_inlined avoid value_ctx side_conditions in
-                        (* N.B. We need check here to ... relax universe constraints? *)
+                        (* N.B. We need both check and η-expansion here to ... relax universe constraints? *)
                         let res := check "res"
-                                         (fun () => mkApp cexpr_to_pattern_and_replacement_unfolded_split [rT; rA; rB; side_conditions]) in
+                                         (fun () => mkApp cexpr_to_pattern_and_replacement_unfolded [rT; rA; rB; side_conditions]) in
                         let res := let pident_arg_types := head_reference pident_arg_types in
                                    let pident_of_typed_ident := head_reference pident_of_typed_ident in
                                    let pident_type_of_list_arg_types_beq := head_reference pident_type_of_list_arg_types_beq in
                                    let pident_arg_types_of_typed_ident := head_reference pident_arg_types_of_typed_ident in
-                                   (eval cbv [expr_to_pattern_and_replacement_unfolded_split $pident_arg_types $pident_of_typed_ident $pident_type_of_list_arg_types_beq $pident_arg_types_of_typed_ident (*reflect_ident_iota*)] in res) in
+                                   (eval cbv [expr_to_pattern_and_replacement_unfolded $pident_arg_types $pident_of_typed_ident $pident_type_of_list_arg_types_beq $pident_arg_types_of_typed_ident (*reflect_ident_iota*)] in res) in
                         let res := (eval cbn [fst snd andb pattern.base.relax pattern.base.subst_default pattern.base.subst_default_relax] in res) in
                         let res := change_pattern_base_subst_default_relax res in
-                        let (p, res) := lazy_match! res with
+                        let (p, res) := lazy_match! (eval cbv [lift_existT] in constr:(@lift_existT _ _ _ $res)) with
                                         | existT _ ?p ?res => (p, res)
                                         end in
                         let p := strip_invalid_or_fail p in