remove pattern.ident.type_vars

It was not serving any good purpose, and was interfering with proofs.
Any type variable that appears in an identifier's arguments will
either (a) show up in the type of the identifier, (b) show up in
another type somewhere else in the pattern, or (c) not be needed to
well-type anything that is not an argument to that identifier.  (There
is actually a case (d), where the type variable shows up in the
arguments to another identifier but no-where else, but I'll get to
that in a moment.)  In case (a), the type-unification will pick it up
automatically.  In case (b), pattern-type unification elsewhere will
pick up that type variable.  And in case (c), it is the responsibility
of the function that describes the arguments to the identifier to
handle any dependencies.  Case (d), where there is non-linear matching
on identifier type-arguments, is now forbidden; we will allow the
author of the rewrite-rule to deal with such equalities manually.
This allows some proofs about type unification to actually go through
now.

8 files changed, 82 insertions, 165 deletions

diff --git a/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v b/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v
index 37db3be83..43c8eb813 100644
--- a/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v
+++ b/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v
@@ -1120,13 +1120,13 @@ def to_type_var(name, ty):
            'type': name,
            'type.type base.type': name})[ty]
 
-retcode += addnewline((r"""%sDefinition type_vars {t} (idc : ident t) : list type
-  := match idc with
-     | %s
-     end%%type.
-""" % (indent1,
-       '\n     | '.join('@' + pctor + ' => [' + '; '.join(to_type_var(n, t) for n, t in named_ttype) + ']'
-                        for pctor, named_ttype in zip(pctors_with_args, named_ttypes)))).replace('\n', '\n' + indent1))
+#retcode += addnewline((r"""%sDefinition type_vars {t} (idc : ident t) : list type
+#  := match idc with
+#     | %s
+#     end%%type.
+#""" % (indent1,
+#       '\n     | '.join('@' + pctor + ' => [' + '; '.join(to_type_var(n, t) for n, t in named_ttype) + ']'
+#                        for pctor, named_ttype in zip(pctors_with_args, named_ttypes)))).replace('\n', '\n' + indent1))
 
 retcode += addnewline((r"""%sDefinition to_typed {t} (idc : ident t) (evm : EvarMap) : type_of_list (arg_types idc) -> %sident.ident (pattern.type.subst_default t evm)
   := match idc in ident t return type_of_list (arg_types idc) -> %sident.ident (pattern.type.subst_default t evm) with
@@ -2164,87 +2164,6 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
            | @fancy_addm => []
            end%type.
 
-      Definition type_vars {t} (idc : ident t) : list type
-        := match idc with
-           | @Literal t => [type.base (base.type.type_base t)]
-           | @Nat_succ => []
-           | @Nat_pred => []
-           | @Nat_max => []
-           | @Nat_mul => []
-           | @Nat_add => []
-           | @Nat_sub => []
-           | @nil t => [type.base t]
-           | @cons t => [type.base t]
-           | @pair A B => [type.base A; type.base B]
-           | @fst A B => [type.base A; type.base B]
-           | @snd A B => [type.base A; type.base B]
-           | @prod_rect A B T => [type.base A; type.base B; type.base T]
-           | @bool_rect T => [type.base T]
-           | @nat_rect P => [type.base P]
-           | @nat_rect_arrow P Q => [type.base P; type.base Q]
-           | @list_rect A P => [type.base A; type.base P]
-           | @list_case A P => [type.base A; type.base P]
-           | @List_length T => [type.base T]
-           | @List_seq => []
-           | @List_firstn A => [type.base A]
-           | @List_skipn A => [type.base A]
-           | @List_repeat A => [type.base A]
-           | @List_combine A B => [type.base A; type.base B]
-           | @List_map A B => [type.base A; type.base B]
-           | @List_app A => [type.base A]
-           | @List_rev A => [type.base A]
-           | @List_flat_map A B => [type.base A; type.base B]
-           | @List_partition A => [type.base A]
-           | @List_fold_right A B => [type.base A; type.base B]
-           | @List_update_nth T => [type.base T]
-           | @List_nth_default T => [type.base T]
-           | @Z_add => []
-           | @Z_mul => []
-           | @Z_pow => []
-           | @Z_sub => []
-           | @Z_opp => []
-           | @Z_div => []
-           | @Z_modulo => []
-           | @Z_log2 => []
-           | @Z_log2_up => []
-           | @Z_eqb => []
-           | @Z_leb => []
-           | @Z_geb => []
-           | @Z_of_nat => []
-           | @Z_to_nat => []
-           | @Z_shiftr => []
-           | @Z_shiftl => []
-           | @Z_land => []
-           | @Z_lor => []
-           | @Z_bneg => []
-           | @Z_lnot_modulo => []
-           | @Z_mul_split => []
-           | @Z_add_get_carry => []
-           | @Z_add_with_carry => []
-           | @Z_add_with_get_carry => []
-           | @Z_sub_get_borrow => []
-           | @Z_sub_with_get_borrow => []
-           | @Z_zselect => []
-           | @Z_add_modulo => []
-           | @Z_rshi => []
-           | @Z_cc_m => []
-           | @Z_cast => []
-           | @Z_cast2 => []
-           | @fancy_add => []
-           | @fancy_addc => []
-           | @fancy_sub => []
-           | @fancy_subb => []
-           | @fancy_mulll => []
-           | @fancy_mullh => []
-           | @fancy_mulhl => []
-           | @fancy_mulhh => []
-           | @fancy_rshi => []
-           | @fancy_selc => []
-           | @fancy_selm => []
-           | @fancy_sell => []
-           | @fancy_addm => []
-           end%type.
-
       Definition to_typed {t} (idc : ident t) (evm : EvarMap) : type_of_list (arg_types idc) -> Compilers.ident.ident (pattern.type.subst_default t evm)
         := match idc in ident t return type_of_list (arg_types idc) -> Compilers.ident.ident (pattern.type.subst_default t evm) with
            | @Literal t => fun arg => let '(v, _) := eta2r arg in @Compilers.ident.Literal _ v
diff --git a/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypesProofs.v b/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypesProofs.v
index c877c3898..48ac11ce6 100644
--- a/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypesProofs.v
+++ b/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypesProofs.v
@@ -149,10 +149,12 @@ Module Compilers.
         : @eta_ident_cps T t idc f = f t idc.
       Proof. cbv [eta_ident_cps]; break_innermost_match; reflexivity. Qed.
 
+(*
       Lemma is_simple_strip_types_iff_type_vars_nil {t} idc
         : Raw.ident.is_simple (@strip_types t idc) = true
           <-> type_vars idc = List.nil.
       Proof. destruct idc; cbn; intuition congruence. Qed.
+*)
 
       Lemma unify_to_typed {t t' pidc idc}
         : forall v,
@@ -200,6 +202,7 @@ Module Compilers.
                           | progress Compilers.type.inversion_type ].
       Qed.
 
+      (*
       Local Ltac solve_ex_or_eq :=
         lazymatch goal with
         | [ |- ex _ ] => eexists; solve_ex_or_eq
@@ -226,6 +229,7 @@ Module Compilers.
                           | progress destruct_head'_or
                           | solve_ex_or_eq ].
       Qed.
+       *)
     End ident.
   End pattern.
 End Compilers.
diff --git a/src/Experiments/NewPipeline/Rewriter.v b/src/Experiments/NewPipeline/Rewriter.v
index 767404e01..6937a8076 100644
--- a/src/Experiments/NewPipeline/Rewriter.v
+++ b/src/Experiments/NewPipeline/Rewriter.v
@@ -338,12 +338,12 @@ Module Compilers.
          | App s d f x => Raw.App (@to_raw _ _ to_raw_ident _ f) (@to_raw _ _ to_raw_ident _ x)
          end.
 
-    Fixpoint collect_vars {ident} {ident_collect_vars : forall t, ident t -> PositiveSet.t}
+    Fixpoint collect_vars {ident}
              {t} (p : @pattern ident t) : PositiveSet.t
       := match p with
          | Wildcard t => type.collect_vars t
-         | Ident t idc => ident_collect_vars t idc
-         | App s d f x => PositiveSet.union (@collect_vars _ ident_collect_vars _ x) (@collect_vars _ ident_collect_vars _ f)
+         | Ident t idc => type.collect_vars t
+         | App s d f x => PositiveSet.union (@collect_vars _ _ x) (@collect_vars _ _ f)
          end.
 
     Notation ident := ident.ident.
@@ -471,7 +471,6 @@ Module Compilers.
                 {raw_pident : Type}
                 (strip_types : forall t, pident t -> raw_pident)
                 (raw_pident_beq : raw_pident -> raw_pident -> bool)
-                (type_vars_of_pident : forall t, pident t -> list (type.type pattern.base.type))
 
                 (full_types : raw_pident -> Type)
                 (invert_bind_args invert_bind_args_unknown : forall t (idc : ident t) (pidc : raw_pident), option (full_types pidc))
@@ -704,13 +703,9 @@ Module Compilers.
                     (@under_with_unification_resultT' _ _ x evm _ _ F)
              end.
 
-        Definition ident_collect_vars := (fun t idc => fold_right PositiveSet.union PositiveSet.empty (List.map pattern.type.collect_vars (type_vars_of_pident t idc))).
-
         Definition with_unification_resultT {var t} (p : pattern t) (K : type -> Type) : Type
           := pattern.type.forall_vars
-               (@pattern.collect_vars
-                  _ ident_collect_vars
-                  t p)
+               (@pattern.collect_vars _ t p)
                (fun evm => @with_unification_resultT' var t p evm (K (pattern.type.subst_default t evm))).
 
         Definition unification_resultT {var t} (p : pattern t) : Type
@@ -1182,6 +1177,10 @@ Module Compilers.
             := eta_ident_cps _ _ idc (fun t' idc' => assemble_identifier_rewriters' t' (rIdent true idc' #idc') (fun _ => id)).
         End with_do_again.
       End with_var.
+      Global Arguments rew_should_do_again {_ _ _ _ _ _} _.
+      Global Arguments rew_with_opt        {_ _ _ _ _ _} _.
+      Global Arguments rew_under_lets      {_ _ _ _ _ _} _.
+      Global Arguments rew_replacement     {_ _ _ _ _ _} _.
 
       Section full.
         Context {var : type.type base.type -> Type}.
@@ -1249,15 +1248,14 @@ Module Compilers.
         Coercion ptype_base' : base.type.base >-> ptype.
         Coercion type_base : base.type >-> type.
         Coercion ptype_base : pattern.base.type >-> ptype.
-        Local Notation ident_collect_vars := (@ident_collect_vars pattern.ident (@pattern.ident.type_vars)).
-        Local Notation collect_vars := (@pattern.collect_vars pattern.ident (@ident_collect_vars)).
+        Local Notation collect_vars := (@pattern.collect_vars pattern.ident).
         Local Notation with_unification_resultT' := (@with_unification_resultT' pattern.ident (@pattern.ident.arg_types) value).
-        Local Notation with_unification_resultT := (@with_unification_resultT pattern.ident (@pattern.ident.arg_types) (@pattern.ident.type_vars) value).
+        Local Notation with_unification_resultT := (@with_unification_resultT pattern.ident (@pattern.ident.arg_types) value).
         Local Notation under_with_unification_resultT' := (@under_with_unification_resultT' pattern.ident (@pattern.ident.arg_types) value).
-        Local Notation under_with_unification_resultT := (@under_with_unification_resultT pattern.ident (@pattern.ident.arg_types) (@pattern.ident.type_vars) value).
-        Local Notation rewrite_ruleTP := (@rewrite_ruleTP ident var pattern.ident (@pattern.ident.arg_types) (@pattern.ident.type_vars)).
-        Local Notation rewrite_ruleT := (@rewrite_ruleT ident var pattern.ident (@pattern.ident.arg_types) (@pattern.ident.type_vars)).
-        Local Notation rewrite_rule_data := (@rewrite_rule_data ident var pattern.ident (@pattern.ident.arg_types) (@pattern.ident.type_vars)).
+        Local Notation under_with_unification_resultT := (@under_with_unification_resultT pattern.ident (@pattern.ident.arg_types) value).
+        Local Notation rewrite_ruleTP := (@rewrite_ruleTP ident var pattern.ident (@pattern.ident.arg_types)).
+        Local Notation rewrite_ruleT := (@rewrite_ruleT ident var pattern.ident (@pattern.ident.arg_types)).
+        Local Notation rewrite_rule_data := (@rewrite_rule_data ident var pattern.ident (@pattern.ident.arg_types)).
 
         Definition make_base_Literal_pattern (t : base.type.base) : pattern t
           := Eval cbv [pattern.ident.of_typed_ident] in
@@ -1493,14 +1491,14 @@ Module Compilers.
       Coercion ptype_base' : base.type.base >-> ptype.
       Coercion type_base : base.type >-> type.
       Coercion ptype_base : pattern.base.type >-> ptype.
-      Local Notation Build_rewrite_rule_data := (@Build_rewrite_rule_data ident var pattern.ident (@pattern.ident.arg_types) (@pattern.ident.type_vars)).
+      Local Notation Build_rewrite_rule_data := (@Build_rewrite_rule_data ident var pattern.ident (@pattern.ident.arg_types)).
       Local Notation Build_anypattern := (@pattern.Build_anypattern pattern.ident).
-      Local Notation rewrite_ruleTP := (@rewrite_ruleTP ident var pattern.ident (@pattern.ident.arg_types) (@pattern.ident.type_vars)).
-      Local Notation rewrite_ruleT := (@rewrite_ruleT ident var pattern.ident (@pattern.ident.arg_types) (@pattern.ident.type_vars)).
-      Local Notation rewrite_rulesT := (@rewrite_rulesT ident var pattern.ident (@pattern.ident.arg_types) (@pattern.ident.type_vars)).
+      Local Notation rewrite_ruleTP := (@rewrite_ruleTP ident var pattern.ident (@pattern.ident.arg_types)).
+      Local Notation rewrite_ruleT := (@rewrite_ruleT ident var pattern.ident (@pattern.ident.arg_types)).
+      Local Notation rewrite_rulesT := (@rewrite_rulesT ident var pattern.ident (@pattern.ident.arg_types)).
       Definition pident_unify_unknown := @pattern.ident.unify.
       Definition invert_bind_args_unknown := @pattern.Raw.ident.invert_bind_args.
-      Local Notation assemble_identifier_rewriters := (@assemble_identifier_rewriters ident var (@pattern.ident.eta_ident_cps) (@pattern.ident) (@pattern.ident.arg_types) (@pattern.ident.unify) pident_unify_unknown pattern.Raw.ident (@pattern.ident.type_vars) (@pattern.Raw.ident.full_types) (@pattern.Raw.ident.invert_bind_args) invert_bind_args_unknown (@pattern.Raw.ident.type_of) (@pattern.Raw.ident.to_typed) pattern.Raw.ident.is_simple).
+      Local Notation assemble_identifier_rewriters := (@assemble_identifier_rewriters ident var (@pattern.ident.eta_ident_cps) (@pattern.ident) (@pattern.ident.arg_types) (@pattern.ident.unify) pident_unify_unknown pattern.Raw.ident (@pattern.Raw.ident.full_types) (@pattern.Raw.ident.invert_bind_args) invert_bind_args_unknown (@pattern.Raw.ident.type_of) (@pattern.Raw.ident.to_typed) pattern.Raw.ident.is_simple).
 
       Delimit Scope rewrite_scope with rewrite.
       Delimit Scope rewrite_opt_scope with rewrite_opt.
@@ -1959,11 +1957,11 @@ Module Compilers.
            ].
 
       Definition nbe_dtree'
-        := Eval compute in @compile_rewrites ident var pattern.ident (@pattern.ident.arg_types) pattern.Raw.ident (@pattern.ident.strip_types) pattern.Raw.ident.ident_beq (@pattern.ident.type_vars) 100 nbe_rewrite_rules.
+        := Eval compute in @compile_rewrites ident var pattern.ident (@pattern.ident.arg_types) pattern.Raw.ident (@pattern.ident.strip_types) pattern.Raw.ident.ident_beq 100 nbe_rewrite_rules.
       Definition arith_dtree'
-        := Eval compute in @compile_rewrites ident var pattern.ident (@pattern.ident.arg_types) pattern.Raw.ident (@pattern.ident.strip_types) pattern.Raw.ident.ident_beq (@pattern.ident.type_vars) 100 (arith_rewrite_rules 0%Z (* dummy val *)).
+        := Eval compute in @compile_rewrites ident var pattern.ident (@pattern.ident.arg_types) pattern.Raw.ident (@pattern.ident.strip_types) pattern.Raw.ident.ident_beq 100 (arith_rewrite_rules 0%Z (* dummy val *)).
       Definition arith_with_casts_dtree'
-        := Eval compute in @compile_rewrites ident var pattern.ident (@pattern.ident.arg_types) pattern.Raw.ident (@pattern.ident.strip_types) pattern.Raw.ident.ident_beq (@pattern.ident.type_vars) 100 arith_with_casts_rewrite_rules.
+        := Eval compute in @compile_rewrites ident var pattern.ident (@pattern.ident.arg_types) pattern.Raw.ident (@pattern.ident.strip_types) pattern.Raw.ident.ident_beq 100 arith_with_casts_rewrite_rules.
       Definition nbe_dtree : decision_tree
         := Eval compute in invert_Some nbe_dtree'.
       Definition arith_dtree : decision_tree
@@ -2186,11 +2184,11 @@ Z.mul @@ (?x >> 128, ?y >> 128)             --> mulhh @@ (x, y)
           := [].
 
         Definition fancy_dtree'
-          := Eval compute in @compile_rewrites ident var pattern.ident (@pattern.ident.arg_types) pattern.Raw.ident (@pattern.ident.strip_types) pattern.Raw.ident.ident_beq (@pattern.ident.type_vars) 100 fancy_rewrite_rules.
+          := Eval compute in @compile_rewrites ident var pattern.ident (@pattern.ident.arg_types) pattern.Raw.ident (@pattern.ident.strip_types) pattern.Raw.ident.ident_beq 100 fancy_rewrite_rules.
         Definition fancy_dtree : decision_tree
           := Eval compute in invert_Some fancy_dtree'.
         Definition fancy_with_casts_dtree'
-          := Eval compute in @compile_rewrites ident var pattern.ident (@pattern.ident.arg_types) pattern.Raw.ident (@pattern.ident.strip_types) pattern.Raw.ident.ident_beq (@pattern.ident.type_vars) 100 fancy_with_casts_rewrite_rules.
+          := Eval compute in @compile_rewrites ident var pattern.ident (@pattern.ident.arg_types) pattern.Raw.ident (@pattern.ident.strip_types) pattern.Raw.ident.ident_beq 100 fancy_with_casts_rewrite_rules.
         Definition fancy_with_casts_dtree : decision_tree
           := Eval compute in invert_Some fancy_with_casts_dtree'.
         Definition fancy_default_fuel := Eval compute in List.length fancy_rewrite_rules.
diff --git a/src/Experiments/NewPipeline/RewriterRulesGood.v b/src/Experiments/NewPipeline/RewriterRulesGood.v
index 359459764..fd7facb3d 100644
--- a/src/Experiments/NewPipeline/RewriterRulesGood.v
+++ b/src/Experiments/NewPipeline/RewriterRulesGood.v
@@ -80,7 +80,7 @@ Module Compilers.
     Section good.
       Context {var1 var2 : type -> Type}.
 
-      Local Notation rewrite_rules_goodT := (@Compile.rewrite_rules_goodT ident pattern.ident (@pattern.ident.arg_types) (@pattern.ident.type_vars) var1 var2).
+      Local Notation rewrite_rules_goodT := (@Compile.rewrite_rules_goodT ident pattern.ident (@pattern.ident.arg_types) var1 var2).
 
       Lemma wf_rlist_rect_gen
             {ivar1 ivar2 A P}
@@ -214,7 +214,7 @@ Module Compilers.
         end;
         (exists eq_refl);
         cbn [eq_rect];
-        cbv [Compile.wf_deep_rewrite_ruleTP_gen Compile.wf_rewrite_rule_data_curried Compile.rew_replacement Compile.rew_should_do_again Compile.rew_with_opt Compile.rew_under_lets Compile.wf_with_unif_rewrite_ruleTP_gen_curried Compile.wf_with_unification_resultT pattern.pattern_of_anypattern pattern.type_of_anypattern Compile.wf_maybe_under_lets_expr Compile.wf_maybe_do_again_expr Compile.wf_with_unification_resultT pattern.type.under_forall_vars_relation Compile.with_unification_resultT' pattern.collect_vars Compile.ident_collect_vars pattern.ident.type_vars pattern.type.collect_vars pattern.base.collect_vars PositiveSet.empty PositiveSet.elements Compile.under_type_of_list_relation_cps pattern.ident.arg_types pattern.type.subst_default pattern.base.subst_default PositiveSet.rev PositiveMap.empty Compile.under_with_unification_resultT_relation_hetero Compile.under_with_unification_resultT'_relation_hetero Compile.maybe_option_eq];
+        cbv [Compile.wf_deep_rewrite_ruleTP_gen Compile.wf_rewrite_rule_data_curried Compile.rew_replacement Compile.rew_should_do_again Compile.rew_with_opt Compile.rew_under_lets Compile.wf_with_unif_rewrite_ruleTP_gen_curried Compile.wf_with_unification_resultT pattern.pattern_of_anypattern pattern.type_of_anypattern Compile.wf_maybe_under_lets_expr Compile.wf_maybe_do_again_expr Compile.wf_with_unification_resultT pattern.type.under_forall_vars_relation Compile.with_unification_resultT' pattern.collect_vars pattern.type.collect_vars pattern.base.collect_vars PositiveSet.empty PositiveSet.elements Compile.under_type_of_list_relation_cps pattern.ident.arg_types pattern.type.subst_default pattern.base.subst_default PositiveSet.rev PositiveMap.empty Compile.under_with_unification_resultT_relation_hetero Compile.under_with_unification_resultT'_relation_hetero Compile.maybe_option_eq];
         cbn [List.map List.fold_right PositiveSet.union PositiveSet.xelements List.rev List.app projT1 projT2 list_rect PositiveSet.add PositiveSet.rev PositiveSet.rev_append PositiveMap.add PositiveMap.find orb];
         repeat first [ progress intros
                      | match goal with
diff --git a/src/Experiments/NewPipeline/RewriterRulesInterpGood.v b/src/Experiments/NewPipeline/RewriterRulesInterpGood.v
index 88a4f6670..b002bfcb2 100644
--- a/src/Experiments/NewPipeline/RewriterRulesInterpGood.v
+++ b/src/Experiments/NewPipeline/RewriterRulesInterpGood.v
@@ -99,12 +99,12 @@ Module Compilers.
         rewrite UnderLets.interp_splice, IHxs; reflexivity.
       Qed.
 
-      Local Notation rewrite_rules_interp_goodT := (@Compile.rewrite_rules_interp_goodT ident pattern.ident (@pattern.ident.arg_types) (@pattern.ident.type_vars) (@pattern.ident.to_typed) (@ident_interp)).
+      Local Notation rewrite_rules_interp_goodT := (@Compile.rewrite_rules_interp_goodT ident pattern.ident (@pattern.ident.arg_types) (@pattern.ident.to_typed) (@ident_interp)).
 
       Local Ltac do_cbv0 :=
         cbv [id
                Compile.rewrite_rules_interp_goodT_curried
-               Compile.rewrite_rule_data_interp_goodT_curried Compile.under_with_unification_resultT_relation_hetero Compile.under_with_unification_resultT'_relation_hetero Compile.wf_with_unification_resultT Compile.under_type_of_list_relation_cps Compile.under_type_of_list_relation1_cps pattern.pattern_of_anypattern pattern.type_of_anypattern Compile.rew_replacement Compile.rew_should_do_again Compile.rew_with_opt Compile.rew_under_lets Compile.wf_with_unification_resultT Compile.pattern_default_interp pattern.type.under_forall_vars_relation pattern.type.under_forall_vars_relation1 Compile.deep_rewrite_ruleTP_gen Compile.with_unification_resultT' pattern.ident.arg_types pattern.type.lam_forall_vars Compilers.pattern.type.lam_forall_vars_gen Compile.pattern_default_interp' pattern.collect_vars PositiveMap.empty Compile.ident_collect_vars pattern.ident.type_vars pattern.type.collect_vars PositiveSet.elements PositiveSet.union pattern.base.collect_vars PositiveSet.empty PositiveSet.xelements Compile.lam_type_of_list id pattern.ident.to_typed Compile.under_type_of_list_relation_cps Compile.deep_rewrite_ruleTP_gen_good_relation Compile.normalize_deep_rewrite_rule pattern.type.subst_default PositiveSet.add PositiveSet.rev PositiveSet.rev_append PositiveMap.add Compile.option_bind' Compile.wf_value Compile.value pattern.base.subst_default PositiveMap.find Compile.rewrite_ruleTP ident.smart_Literal Compile.value_interp_related].
+               Compile.rewrite_rule_data_interp_goodT_curried Compile.under_with_unification_resultT_relation_hetero Compile.under_with_unification_resultT'_relation_hetero Compile.wf_with_unification_resultT Compile.under_type_of_list_relation_cps Compile.under_type_of_list_relation1_cps pattern.pattern_of_anypattern pattern.type_of_anypattern Compile.rew_replacement Compile.rew_should_do_again Compile.rew_with_opt Compile.rew_under_lets Compile.wf_with_unification_resultT Compile.pattern_default_interp pattern.type.under_forall_vars_relation pattern.type.under_forall_vars_relation1 Compile.deep_rewrite_ruleTP_gen Compile.with_unification_resultT' pattern.ident.arg_types pattern.type.lam_forall_vars Compilers.pattern.type.lam_forall_vars_gen Compile.pattern_default_interp' pattern.collect_vars PositiveMap.empty pattern.type.collect_vars PositiveSet.elements PositiveSet.union pattern.base.collect_vars PositiveSet.empty PositiveSet.xelements Compile.lam_type_of_list id pattern.ident.to_typed Compile.under_type_of_list_relation_cps Compile.deep_rewrite_ruleTP_gen_good_relation Compile.normalize_deep_rewrite_rule pattern.type.subst_default PositiveSet.add PositiveSet.rev PositiveSet.rev_append PositiveMap.add Compile.option_bind' Compile.wf_value Compile.value pattern.base.subst_default PositiveMap.find Compile.rewrite_ruleTP ident.smart_Literal Compile.value_interp_related].
       Local Ltac do_cbv :=
         do_cbv0;
         cbv [List.map List.fold_right List.rev list_rect orb List.app].
diff --git a/src/Experiments/NewPipeline/RewriterWf1.v b/src/Experiments/NewPipeline/RewriterWf1.v
index 967921da5..8d42eb8e5 100644
--- a/src/Experiments/NewPipeline/RewriterWf1.v
+++ b/src/Experiments/NewPipeline/RewriterWf1.v
@@ -801,7 +801,6 @@ Module Compilers.
                 {raw_pident : Type}
                 (strip_types : forall t, pident t -> raw_pident)
                 (raw_pident_beq : raw_pident -> raw_pident -> bool)
-                (type_vars_of_pident : forall t, pident t -> list (type.type pattern.base.type))
 
                 (full_types : raw_pident -> Type)
                 (invert_bind_args invert_bind_args_unknown : forall t (idc : ident t) (pidc : raw_pident), option (full_types pidc))
@@ -848,9 +847,9 @@ Module Compilers.
         Local Notation unify_pattern' var := (@unify_pattern' ident var pident pident_arg_types pident_unify pident_unify_unknown).
         Local Notation unify_pattern var := (@unify_pattern ident var pident pident_arg_types pident_unify pident_unify_unknown).
         Local Notation app_transport_with_unification_resultT'_cps := (@app_transport_with_unification_resultT'_cps pident pident_arg_types).
-        Local Notation app_with_unification_resultT_cps := (@app_with_unification_resultT_cps pident pident_arg_types type_vars_of_pident).
+        Local Notation app_with_unification_resultT_cps := (@app_with_unification_resultT_cps pident pident_arg_types).
         Local Notation with_unification_resultT' := (@with_unification_resultT' pident pident_arg_types).
-        Local Notation with_unification_resultT := (@with_unification_resultT pident pident_arg_types type_vars_of_pident).
+        Local Notation with_unification_resultT := (@with_unification_resultT pident pident_arg_types).
         Local Notation unification_resultT' := (@unification_resultT' pident pident_arg_types).
         Local Notation unification_resultT := (@unification_resultT pident pident_arg_types).
 
@@ -1453,14 +1452,14 @@ Module Compilers.
           Local Notation wf_value_with_lets := (@wf_value_with_lets base.type ident var1 var2).
           Local Notation reify_and_let_binds_cps1 := (@reify_and_let_binds_cps ident var1 reify_and_let_binds_base_cps1).
           Local Notation reify_and_let_binds_cps2 := (@reify_and_let_binds_cps ident var2 reify_and_let_binds_base_cps2).
-          Local Notation rewrite_rulesT1 := (@rewrite_rulesT ident var1 pident pident_arg_types type_vars_of_pident).
-          Local Notation rewrite_rulesT2 := (@rewrite_rulesT ident var2 pident pident_arg_types type_vars_of_pident).
-          Local Notation eval_rewrite_rules1 := (@eval_rewrite_rules ident var1 pident pident_arg_types pident_unify pident_unify_unknown raw_pident type_vars_of_pident full_types invert_bind_args invert_bind_args_unknown type_of_raw_pident raw_pident_to_typed raw_pident_is_simple).
-          Local Notation eval_rewrite_rules2 := (@eval_rewrite_rules ident var2 pident pident_arg_types pident_unify pident_unify_unknown raw_pident type_vars_of_pident full_types invert_bind_args invert_bind_args_unknown type_of_raw_pident raw_pident_to_typed raw_pident_is_simple).
-          Local Notation rewrite_rule_data1 := (@rewrite_rule_data ident var1 pident pident_arg_types type_vars_of_pident).
-          Local Notation rewrite_rule_data2 := (@rewrite_rule_data ident var2 pident pident_arg_types type_vars_of_pident).
-          Local Notation with_unif_rewrite_ruleTP_gen1 := (@with_unif_rewrite_ruleTP_gen ident var1 pident pident_arg_types type_vars_of_pident).
-          Local Notation with_unif_rewrite_ruleTP_gen2 := (@with_unif_rewrite_ruleTP_gen ident var2 pident pident_arg_types type_vars_of_pident).
+          Local Notation rewrite_rulesT1 := (@rewrite_rulesT ident var1 pident pident_arg_types).
+          Local Notation rewrite_rulesT2 := (@rewrite_rulesT ident var2 pident pident_arg_types).
+          Local Notation eval_rewrite_rules1 := (@eval_rewrite_rules ident var1 pident pident_arg_types pident_unify pident_unify_unknown raw_pident full_types invert_bind_args invert_bind_args_unknown type_of_raw_pident raw_pident_to_typed raw_pident_is_simple).
+          Local Notation eval_rewrite_rules2 := (@eval_rewrite_rules ident var2 pident pident_arg_types pident_unify pident_unify_unknown raw_pident full_types invert_bind_args invert_bind_args_unknown type_of_raw_pident raw_pident_to_typed raw_pident_is_simple).
+          Local Notation rewrite_rule_data1 := (@rewrite_rule_data ident var1 pident pident_arg_types).
+          Local Notation rewrite_rule_data2 := (@rewrite_rule_data ident var2 pident pident_arg_types).
+          Local Notation with_unif_rewrite_ruleTP_gen1 := (@with_unif_rewrite_ruleTP_gen ident var1 pident pident_arg_types).
+          Local Notation with_unif_rewrite_ruleTP_gen2 := (@with_unif_rewrite_ruleTP_gen ident var2 pident pident_arg_types).
           Local Notation deep_rewrite_ruleTP_gen1 := (@deep_rewrite_ruleTP_gen ident var1).
           Local Notation deep_rewrite_ruleTP_gen2 := (@deep_rewrite_ruleTP_gen ident var2).
           Local Notation preunify_types1 := (@preunify_types ident var1 pident).
@@ -1923,7 +1922,7 @@ Module Compilers.
                      (r1 : @rewrite_rule_data1 t p)
                      (r2 : @rewrite_rule_data2 t p)
             : Prop
-            := wf_with_unif_rewrite_ruleTP_gen G (rew_replacement _ _ r1) (rew_replacement _ _ r2).
+            := wf_with_unif_rewrite_ruleTP_gen G (rew_replacement r1) (rew_replacement r2).
 
           Definition rewrite_rules_goodT
                      (rew1 : rewrite_rulesT1) (rew2 : rewrite_rulesT2)
@@ -1956,7 +1955,7 @@ Module Compilers.
                      (r1 : @rewrite_rule_data1 t p)
                      (r2 : @rewrite_rule_data2 t p)
             : Prop
-            := wf_with_unif_rewrite_ruleTP_gen_curried G (rew_replacement _ _ r1) (rew_replacement _ _ r2).
+            := wf_with_unif_rewrite_ruleTP_gen_curried G (rew_replacement r1) (rew_replacement r2).
 
           Definition rewrite_rules_goodT_curried
                      (rew1 : rewrite_rulesT1) (rew2 : rewrite_rulesT2)
@@ -2002,9 +2001,9 @@ Module Compilers.
                   {ident_interp_Proper : forall t, Proper (eq ==> type.eqv) (ident_interp t)}.
           Local Notation var := (type.interp base.interp) (only parsing).
           Local Notation expr := (@expr.expr base.type ident var).
-          Local Notation rewrite_rulesT := (@rewrite_rulesT ident var pident pident_arg_types type_vars_of_pident).
-          Local Notation rewrite_rule_data := (@rewrite_rule_data ident var pident pident_arg_types type_vars_of_pident).
-          Local Notation with_unif_rewrite_ruleTP_gen := (@with_unif_rewrite_ruleTP_gen ident var pident pident_arg_types type_vars_of_pident).
+          Local Notation rewrite_rulesT := (@rewrite_rulesT ident var pident pident_arg_types).
+          Local Notation rewrite_rule_data := (@rewrite_rule_data ident var pident pident_arg_types).
+          Local Notation with_unif_rewrite_ruleTP_gen := (@with_unif_rewrite_ruleTP_gen ident var pident pident_arg_types).
           Local Notation normalize_deep_rewrite_rule := (@normalize_deep_rewrite_rule ident var).
 
           Local Notation deep_rewrite_ruleTP_gen := (@deep_rewrite_ruleTP_gen ident var).
@@ -2251,9 +2250,9 @@ Module Compilers.
                     => related_sigT_by_eq
                          (fun evm
                           => @deep_rewrite_ruleTP_gen_good_relation
-                               (rew_should_do_again _ _ r) (rew_with_opt _ _ r) (rew_under_lets _ _ r) (pattern.type.subst_default t evm))
+                               (rew_should_do_again r) (rew_with_opt r) (rew_under_lets r) (pattern.type.subst_default t evm))
                          fx gy)
-                   (app_with_unification_resultT_cps (rew_replacement _ _ r) x _ (@Some _))
+                   (app_with_unification_resultT_cps (rew_replacement r) x _ (@Some _))
                    (app_with_unification_resultT_cps (pattern_default_interp p) y _ (@Some _)).
 
           Definition rewrite_rules_interp_goodT
@@ -2269,7 +2268,7 @@ Module Compilers.
             := under_with_unification_resultT_relation_hetero
                  (fun _ => value_interp_related)
                  (fun evm => deep_rewrite_ruleTP_gen_good_relation)
-                 (rew_replacement _ _ r)
+                 (rew_replacement r)
                  (pattern_default_interp p).
 
           Definition rewrite_rules_interp_goodT_curried
diff --git a/src/Experiments/NewPipeline/RewriterWf2.v b/src/Experiments/NewPipeline/RewriterWf2.v
index 42720bd38..ec6142103 100644
--- a/src/Experiments/NewPipeline/RewriterWf2.v
+++ b/src/Experiments/NewPipeline/RewriterWf2.v
@@ -63,7 +63,6 @@ Module Compilers.
                 {raw_pident : Type}
                 (strip_types : forall t, pident t -> raw_pident)
                 (raw_pident_beq : raw_pident -> raw_pident -> bool)
-                (type_vars_of_pident : forall t, pident t -> list (type.type pattern.base.type))
 
                 (full_types : raw_pident -> Type)
                 (invert_bind_args invert_bind_args_unknown : forall t (idc : ident t) (pidc : raw_pident), option (full_types pidc))
@@ -116,18 +115,18 @@ Module Compilers.
           Local Notation wf_value_with_lets := (@wf_value_with_lets base.type ident var1 var2).
           Local Notation reify_and_let_binds_cps1 := (@reify_and_let_binds_cps ident var1 reify_and_let_binds_base_cps1).
           Local Notation reify_and_let_binds_cps2 := (@reify_and_let_binds_cps ident var2 reify_and_let_binds_base_cps2).
-          Local Notation rewrite_rulesT1 := (@rewrite_rulesT ident var1 pident pident_arg_types type_vars_of_pident).
-          Local Notation rewrite_rulesT2 := (@rewrite_rulesT ident var2 pident pident_arg_types type_vars_of_pident).
-          Local Notation eval_rewrite_rules1 := (@eval_rewrite_rules ident var1 pident pident_arg_types pident_unify pident_unify_unknown raw_pident type_vars_of_pident full_types invert_bind_args invert_bind_args_unknown type_of_raw_pident raw_pident_to_typed raw_pident_is_simple).
-          Local Notation eval_rewrite_rules2 := (@eval_rewrite_rules ident var2 pident pident_arg_types pident_unify pident_unify_unknown raw_pident type_vars_of_pident full_types invert_bind_args invert_bind_args_unknown type_of_raw_pident raw_pident_to_typed raw_pident_is_simple).
+          Local Notation rewrite_rulesT1 := (@rewrite_rulesT ident var1 pident pident_arg_types).
+          Local Notation rewrite_rulesT2 := (@rewrite_rulesT ident var2 pident pident_arg_types).
+          Local Notation eval_rewrite_rules1 := (@eval_rewrite_rules ident var1 pident pident_arg_types pident_unify pident_unify_unknown raw_pident full_types invert_bind_args invert_bind_args_unknown type_of_raw_pident raw_pident_to_typed raw_pident_is_simple).
+          Local Notation eval_rewrite_rules2 := (@eval_rewrite_rules ident var2 pident pident_arg_types pident_unify pident_unify_unknown raw_pident full_types invert_bind_args invert_bind_args_unknown type_of_raw_pident raw_pident_to_typed raw_pident_is_simple).
           Local Notation with_unification_resultT'1 := (@with_unification_resultT' ident var1 pident pident_arg_types).
           Local Notation with_unification_resultT'2 := (@with_unification_resultT' ident var2 pident pident_arg_types).
-          Local Notation with_unification_resultT1 := (@with_unification_resultT ident var1 pident pident_arg_types type_vars_of_pident).
-          Local Notation with_unification_resultT2 := (@with_unification_resultT ident var2 pident pident_arg_types type_vars_of_pident).
-          Local Notation rewrite_rule_data1 := (@rewrite_rule_data ident var1 pident pident_arg_types type_vars_of_pident).
-          Local Notation rewrite_rule_data2 := (@rewrite_rule_data ident var2 pident pident_arg_types type_vars_of_pident).
-          Local Notation with_unif_rewrite_ruleTP_gen1 := (@with_unif_rewrite_ruleTP_gen ident var1 pident pident_arg_types type_vars_of_pident).
-          Local Notation with_unif_rewrite_ruleTP_gen2 := (@with_unif_rewrite_ruleTP_gen ident var2 pident pident_arg_types type_vars_of_pident).
+          Local Notation with_unification_resultT1 := (@with_unification_resultT ident var1 pident pident_arg_types).
+          Local Notation with_unification_resultT2 := (@with_unification_resultT ident var2 pident pident_arg_types).
+          Local Notation rewrite_rule_data1 := (@rewrite_rule_data ident var1 pident pident_arg_types).
+          Local Notation rewrite_rule_data2 := (@rewrite_rule_data ident var2 pident pident_arg_types).
+          Local Notation with_unif_rewrite_ruleTP_gen1 := (@with_unif_rewrite_ruleTP_gen ident var1 pident pident_arg_types).
+          Local Notation with_unif_rewrite_ruleTP_gen2 := (@with_unif_rewrite_ruleTP_gen ident var2 pident pident_arg_types).
           Local Notation wf_rawexpr := (@wf_rawexpr ident var1 var2).
           (** TODO: Move Me up *)
           Local Notation unify_pattern'1 := (@unify_pattern' ident var1 pident pident_arg_types pident_unify pident_unify_unknown).
@@ -136,12 +135,12 @@ Module Compilers.
           Local Notation unify_pattern2 := (@unify_pattern ident var2 pident pident_arg_types pident_unify pident_unify_unknown).
           Local Notation wf_unification_resultT' := (@wf_unification_resultT' ident pident pident_arg_types var1 var2).
           Local Notation wf_unification_resultT := (@wf_unification_resultT ident pident pident_arg_types var1 var2).
-          Local Notation wf_with_unification_resultT := (@wf_with_unification_resultT ident pident pident_arg_types type_vars_of_pident var1 var2).
-          Local Notation wf_with_unif_rewrite_ruleTP_gen := (@wf_with_unif_rewrite_ruleTP_gen ident pident pident_arg_types type_vars_of_pident var1 var2).
+          Local Notation wf_with_unification_resultT := (@wf_with_unification_resultT ident pident pident_arg_types var1 var2).
+          Local Notation wf_with_unif_rewrite_ruleTP_gen := (@wf_with_unif_rewrite_ruleTP_gen ident pident pident_arg_types var1 var2).
           Local Notation wf_deep_rewrite_ruleTP_gen := (@wf_deep_rewrite_ruleTP_gen ident var1 var2).
-          Local Notation app_with_unification_resultT_cps1 := (@app_with_unification_resultT_cps pident pident_arg_types type_vars_of_pident (@value var1)).
-          Local Notation app_with_unification_resultT_cps2 := (@app_with_unification_resultT_cps pident pident_arg_types type_vars_of_pident (@value var2)).
-          Local Notation wf_app_with_unification_resultT := (@wf_app_with_unification_resultT ident pident pident_arg_types type_vars_of_pident var1 var2).
+          Local Notation app_with_unification_resultT_cps1 := (@app_with_unification_resultT_cps pident pident_arg_types (@value var1)).
+          Local Notation app_with_unification_resultT_cps2 := (@app_with_unification_resultT_cps pident pident_arg_types (@value var2)).
+          Local Notation wf_app_with_unification_resultT := (@wf_app_with_unification_resultT ident pident pident_arg_types var1 var2).
 
           (* Because [proj1] and [proj2] in the stdlib are opaque *)
           Local Notation proj1 x := (let (a, b) := x in a).
@@ -541,8 +540,8 @@ Module Compilers.
               = UnderLets.Base (rew [A] p in v).
           Proof. case p; reflexivity. Defined.
 
-          Local Notation rewrite_rules_goodT := (@rewrite_rules_goodT ident pident pident_arg_types type_vars_of_pident var1 var2).
-          Local Notation wf_rewrite_rule_data := (@wf_rewrite_rule_data ident pident pident_arg_types type_vars_of_pident var1 var2).
+          Local Notation rewrite_rules_goodT := (@rewrite_rules_goodT ident pident pident_arg_types var1 var2).
+          Local Notation wf_rewrite_rule_data := (@wf_rewrite_rule_data ident pident pident_arg_types var1 var2).
           Local Notation wf_reflect := (@wf_reflect ident var1 var2).
           Local Notation wf_reify := (@wf_reify ident var1 var2).
 
@@ -750,8 +749,8 @@ Module Compilers.
                         -> expr.wf G' e1 e2
                         -> UnderLets.wf (fun G' => expr.wf G') G (@do_again1 t e1) (@do_again2 t e2)).
 
-            Local Notation assemble_identifier_rewriters' var := (@assemble_identifier_rewriters' ident var pident pident_arg_types pident_unify pident_unify_unknown raw_pident type_vars_of_pident full_types invert_bind_args invert_bind_args_unknown type_of_raw_pident raw_pident_to_typed raw_pident_is_simple dtree).
-            Local Notation assemble_identifier_rewriters var := (@assemble_identifier_rewriters ident var eta_ident_cps pident pident_arg_types pident_unify pident_unify_unknown raw_pident type_vars_of_pident full_types invert_bind_args invert_bind_args_unknown type_of_raw_pident raw_pident_to_typed raw_pident_is_simple dtree).
+            Local Notation assemble_identifier_rewriters' var := (@assemble_identifier_rewriters' ident var pident pident_arg_types pident_unify pident_unify_unknown raw_pident full_types invert_bind_args invert_bind_args_unknown type_of_raw_pident raw_pident_to_typed raw_pident_is_simple dtree).
+            Local Notation assemble_identifier_rewriters var := (@assemble_identifier_rewriters ident var eta_ident_cps pident pident_arg_types pident_unify pident_unify_unknown raw_pident full_types invert_bind_args invert_bind_args_unknown type_of_raw_pident raw_pident_to_typed raw_pident_is_simple dtree).
 
             Lemma wf_assemble_identifier_rewriters' G t re1 e1 re2 e2
                   K1 K2
diff --git a/src/Experiments/NewPipeline/nbe_rewrite_head.out b/src/Experiments/NewPipeline/nbe_rewrite_head.out
index cbd282f50..a60bdfeb4 100644
--- a/src/Experiments/NewPipeline/nbe_rewrite_head.out
+++ b/src/Experiments/NewPipeline/nbe_rewrite_head.out
@@ -408,8 +408,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
             pattern.type.unify_extracted_cps
               (((((unit -> '1%pbtype) ->
                   (ℕ -> '1%pbtype -> '1%pbtype) -> ℕ -> '1%pbtype) ->
-                 unit -> '1%pbtype) -> ℕ -> '1%pbtype -> '1%pbtype) -> 
-               ℕ)%ptype
+                 unit -> '1%pbtype) -> ℕ -> '1%pbtype -> '1%pbtype) -> ℕ)%ptype
               (((((unit -> P) -> (ℕ -> P -> P) -> ℕ -> P) -> unit -> P) ->
                 ℕ -> P -> P) -> (projT1 args))%ptype option
               (fun x2 : option => x2)
@@ -466,11 +465,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
              (((((('1%pbtype -> '2%pbtype) ->
                   (ℕ -> ('1%pbtype -> '2%pbtype) -> '1%pbtype -> '2%pbtype) ->
                   ℕ -> '1%pbtype -> '2%pbtype) -> '1%pbtype -> '2%pbtype) ->
-                ℕ -> ('1%pbtype -> '2%pbtype) -> '1%pbtype -> '2%pbtype) -> 
-               ℕ) -> '1%pbtype)%ptype
+                ℕ -> ('1%pbtype -> '2%pbtype) -> '1%pbtype -> '2%pbtype) -> ℕ) ->
+              '1%pbtype)%ptype
              ((((((P -> Q) -> (ℕ -> (P -> Q) -> P -> Q) -> ℕ -> P -> Q) ->
-                 P -> Q) -> ℕ -> (P -> Q) -> P -> Q) -> (projT1 args)) -> 
-              P)%ptype option (fun x3 : option => x3)
+                 P -> Q) -> ℕ -> (P -> Q) -> P -> Q) -> (projT1 args)) -> P)%ptype
+             option (fun x3 : option => x3)
          with
          | Some
            (_, _, (_, (_, _, (_, _)), (_, (_, _))), (_, _),
@@ -479,8 +478,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
               type.type_beq base.type base.type.type_beq
                 ((((((b -> b16) ->
                      (ℕ -> (b -> b16) -> b -> b16) -> ℕ -> b -> b16) ->
-                    b -> b16) -> ℕ -> (b -> b16) -> b -> b16) -> ℕ) -> 
-                 b)%ptype
+                    b -> b16) -> ℕ -> (b -> b16) -> b -> b16) -> ℕ) -> b)%ptype
                 ((((((P -> Q) -> (ℕ -> (P -> Q) -> P -> Q) -> ℕ -> P -> Q) ->
                     P -> Q) -> ℕ -> (P -> Q) -> P -> Q) -> (projT1 args)) ->
                  P)%ptype