From 4c8a9f915eaed4b64f64b001668db228b83c9fdb Mon Sep 17 00:00:00 2001
From: Nicolas Abril <nicolas.abril@protonmail.ch>
Date: Tue, 27 Feb 2024 19:14:25 +0100
Subject: [PATCH] [sc-301] Fix after merge

---
 src/term/transform/float_combinators.rs |  2 +-
 src/term/transform/linearize_matches.rs | 21 +++++++--------------
 src/term/transform/simplify_matches.rs  |  2 +-
 3 files changed, 9 insertions(+), 16 deletions(-)

diff --git a/src/term/transform/float_combinators.rs b/src/term/transform/float_combinators.rs
index 8bcac0718..b0e3e427c 100644
--- a/src/term/transform/float_combinators.rs
+++ b/src/term/transform/float_combinators.rs
@@ -271,7 +271,7 @@ impl Term {
 
     for rule in rules.iter_mut() {
       for pat in &rule.pats {
-        debug_assert!(pat.is_detached_num_match());
+        debug_assert!(pat.is_native_num_match());
       }
 
       let arm_detach = match rule.body.go_float(depth + 1, term_info) {
diff --git a/src/term/transform/linearize_matches.rs b/src/term/transform/linearize_matches.rs
index 70c3e988a..2f3650334 100644
--- a/src/term/transform/linearize_matches.rs
+++ b/src/term/transform/linearize_matches.rs
@@ -13,7 +13,7 @@ impl Ctx<'_> {
 
     for (def_name, def) in self.book.defs.iter_mut() {
       for rule in def.rules.iter_mut() {
-        let res = rule.body.linearize_simple_matches(&self.book.ctrs, lift_all_vars);
+        let res = rule.body.linearize_simple_matches(lift_all_vars);
         self.info.take_err(res, Some(def_name));
       }
     }
@@ -23,24 +23,17 @@ impl Ctx<'_> {
 }
 
 impl Term {
-  fn linearize_simple_matches(&mut self, ctrs: &Constructors, lift_all_vars: bool) -> Result<(), MatchErr> {
+  fn linearize_simple_matches(&mut self, lift_all_vars: bool) -> Result<(), MatchErr> {
     match self {
       Term::Mat { args: _, rules } => {
         for rule in rules.iter_mut() {
-          rule.body.linearize_simple_matches(ctrs, lift_all_vars).unwrap();
+          rule.body.linearize_simple_matches(lift_all_vars).unwrap();
         }
-        let matched_type = infer_type(rules.iter().map(|r| &r.pats[0]), ctrs)?;
-        match matched_type {
-          Type::Num | Type::Tup | Type::Any => _ = lift_match_vars(self, lift_all_vars),
-          Type::Adt(_) => {
-            lift_match_vars(self, lift_all_vars);
-          }
-        }
-        linearize_match_free_vars(self);
+        lift_match_vars(self, lift_all_vars);
       }
 
       Term::Lam { bod, .. } | Term::Chn { bod, .. } => {
-        bod.linearize_simple_matches(ctrs, lift_all_vars)?;
+        bod.linearize_simple_matches(lift_all_vars)?;
       }
 
       Term::Let { pat: Pattern::Var(..), val: fst, nxt: snd }
@@ -49,8 +42,8 @@ impl Term {
       | Term::Sup { fst, snd, .. }
       | Term::Opx { fst, snd, .. }
       | Term::App { fun: fst, arg: snd, .. } => {
-        fst.linearize_simple_matches(ctrs, lift_all_vars)?;
-        snd.linearize_simple_matches(ctrs, lift_all_vars)?;
+        fst.linearize_simple_matches(lift_all_vars)?;
+        snd.linearize_simple_matches(lift_all_vars)?;
       }
 
       Term::Lst { .. } => unreachable!(),
diff --git a/src/term/transform/simplify_matches.rs b/src/term/transform/simplify_matches.rs
index d8b53451c..c15f880f9 100644
--- a/src/term/transform/simplify_matches.rs
+++ b/src/term/transform/simplify_matches.rs
@@ -327,7 +327,7 @@ fn switch_rule_submatch_arm(rule: &Rule, ctr: &Pattern, nested_fields: &[Option<
       Pattern::Num(NumCtr::Succ(_, Some(var))) => vec![Pattern::Var(var.clone())],
       // Similarly for the default case in a num match
       Pattern::Var(var) => vec![Pattern::Var(var.clone())],
-      _ => rule.pats[0].children().cloned().collect::<Vec<_>>()
+      _ => rule.pats[0].children().cloned().collect::<Vec<_>>(),
     };
     if pats.is_empty() {
       // We say that a unit variant always has an unused wildcard nested