diff --git a/src/kind-derive/src/matching.rs b/src/kind-derive/src/matching.rs
index a4f5655c..537e7cb4 100644
--- a/src/kind-derive/src/matching.rs
+++ b/src/kind-derive/src/matching.rs
@@ -92,19 +92,23 @@ pub fn derive_match(range: Range, sum: &SumTypeDecl) -> concrete::Entry {
     });
 
     let params = sum.parameters.map(|x| Binding::Positional(mk_var(x.name.clone())));
+    let indices = sum.indices.map(|x| Binding::Positional(mk_var(x.name.clone())));
 
     // Constructors type
     for cons in &sum.constructors {
         let vars: Vec<Binding> = cons.args.iter().map(|x| Binding::Positional(mk_var(x.name.clone()))).collect();
 
-        let cons_inst = mk_cons(sum.name.add_segment(cons.name.to_str()), [params.as_slice(), vars.as_slice()].concat());
+        let cons_inst = mk_cons(
+            sum.name.add_segment(cons.name.to_str()),
+            [params.as_slice(), if cons.typ.is_none() { indices.as_slice() } else { &[] }, vars.as_slice()].concat(),
+        );
 
         let mut indices_of_cons = match cons.typ.clone().map(|x| x.data) {
             Some(ExprKind::Constr(_, spine)) => spine
                 .iter()
                 .map(|x| match x {
                     Binding::Positional(expr) => AppBinding::explicit(expr.clone()),
-                    Binding::Named(_, _, _) => todo!("Internal Error: Need to reorder"),
+                    Binding::Named(_, _, _) => todo!("Incomplete feature: Need to reorder"),
                 })
                 .collect(),
             _ => [parameter_names.as_slice(), indice_names.as_slice()].concat(),
@@ -114,8 +118,13 @@ pub fn derive_match(range: Range, sum: &SumTypeDecl) -> concrete::Entry {
 
         let cons_tipo = mk_app(mk_var(motive_ident.clone()), indices_of_cons, range);
 
-        let cons_type = cons
-            .args
+        let args = if cons.typ.is_some() {
+            cons.args.clone()
+        } else {
+            sum.indices.extend(&cons.args)
+        };
+
+        let cons_type = args
             .iter()
             .rfold(cons_tipo, |out, arg| mk_pi(arg.name.clone(), arg.typ.clone().unwrap_or_else(mk_typ), out));
 
@@ -138,11 +147,24 @@ pub fn derive_match(range: Range, sum: &SumTypeDecl) -> concrete::Entry {
         let cons_ident = sum.name.add_segment(cons.name.to_str());
         let mut pats: Vec<Box<Pat>> = Vec::new();
 
-        let irrelev = cons.args.map(|x| x.hidden).to_vec();
+        let irrelev: Vec<bool>;
+        let spine_params: Vec<Ident>;
+        let spine: Vec<Ident>;
 
-        let spine_params: Vec<Ident> = sum.parameters.extend(&cons.args).map(|x| x.name.with_name(|f| format!("{}_", f))).to_vec();
-
-        let spine: Vec<Ident> = cons.args.map(|x| x.name.with_name(|f| format!("{}_", f))).to_vec();
+        if cons.typ.is_none() {
+            irrelev = sum.indices.extend(&cons.args).map(|x| x.hidden).to_vec();
+            spine_params = sum
+                .parameters
+                .extend(&sum.indices)
+                .extend(&cons.args)
+                .map(|x| x.name.with_name(|f| format!("{}_", f)))
+                .to_vec();
+            spine = sum.indices.extend(&cons.args).map(|x| x.name.with_name(|f| format!("{}_", f))).to_vec();
+        } else {
+            irrelev = cons.args.map(|x| x.hidden).to_vec();
+            spine_params = sum.parameters.extend(&cons.args).map(|x| x.name.with_name(|f| format!("{}_", f))).to_vec();
+            spine = cons.args.map(|x| x.name.with_name(|f| format!("{}_", f))).to_vec();
+        }
 
         pats.push(Box::new(Pat {
             data: concrete::pat::PatKind::App(
@@ -186,12 +208,14 @@ pub fn derive_match(range: Range, sum: &SumTypeDecl) -> concrete::Entry {
             cons.name.range,
         );
 
-        rules.push(Box::new(Rule {
+        let rule = Box::new(Rule {
             name: name.clone(),
             pats,
             body,
             range: cons.name.range,
-        }))
+        });
+
+        rules.push(rule)
     }
     // Rules
 
diff --git a/src/kind-parser/src/expr.rs b/src/kind-parser/src/expr.rs
index 9a2b3488..a35fb661 100644
--- a/src/kind-parser/src/expr.rs
+++ b/src/kind-parser/src/expr.rs
@@ -554,7 +554,7 @@ impl<'a> Parser<'a> {
         }))
     }
 
-    pub fn parse_pat_destruct_bindings(&mut self) -> Result<(Option<Range>, Vec<CaseBinding>, bool), SyntaxError> {
+    pub fn parse_pat_destruct_bindings(&mut self) -> Result<(Option<Range>, Vec<CaseBinding>, Option<Range>), SyntaxError> {
         let mut ignore_rest_range = None;
         let mut bindings = Vec::new();
         let mut range = None;
@@ -587,7 +587,7 @@ impl<'a> Parser<'a> {
                 return Err(SyntaxError::IgnoreRestShouldBeOnTheEnd(range));
             }
         }
-        Ok((range, bindings, ignore_rest_range.is_some()))
+        Ok((range, bindings, ignore_rest_range))
     }
 
     pub fn parse_match(&mut self) -> Result<Box<Expr>, SyntaxError> {
diff --git a/src/kind-pass/src/desugar/destruct.rs b/src/kind-pass/src/desugar/destruct.rs
index 03a69983..816419f0 100644
--- a/src/kind-pass/src/desugar/destruct.rs
+++ b/src/kind-pass/src/desugar/destruct.rs
@@ -15,7 +15,7 @@ impl<'a> DesugarState<'a> {
         type_info: (&Range, String),
         fields: &[(String, bool)],
         cases: &[CaseBinding],
-        jump_rest: bool,
+        jump_rest: Option<Range>,
     ) -> Vec<Option<(Range, PatIdent)>> {
         let mut ordered_fields = vec![None; fields.len()];
         let mut names = FxHashMap::default();
@@ -51,7 +51,7 @@ impl<'a> DesugarState<'a> {
             .map(|(name, _)| name.clone())
             .collect();
 
-        if !jump_rest && !names.is_empty() {
+        if jump_rest.is_none() && !names.is_empty() {
             self.send_err(PassError::NoFieldCoverage(*type_info.0, names))
         }
 
@@ -95,7 +95,7 @@ impl<'a> DesugarState<'a> {
                     if let Some((_, name)) = arg {
                         arguments.push(name.0)
                     } else {
-                        arguments.push(self.gen_name(typ.range))
+                        arguments.push(self.gen_name(jump_rest.unwrap_or(typ.range)))
                     }
                 }
 
@@ -105,7 +105,7 @@ impl<'a> DesugarState<'a> {
 
                 let spine = vec![
                     val,
-                    desugared::Expr::unfold_lambda(range, &irrelev, &arguments, next(self)),
+                    desugared::Expr::unfold_lambda(&irrelev, &arguments, next(self)),
                 ];
 
                 self.mk_desugared_fun(range, open_id, spine, false)
@@ -195,7 +195,7 @@ impl<'a> DesugarState<'a> {
                     if let Some((_, name)) = arg {
                         arguments.push(name.0)
                     } else {
-                        arguments.push(self.gen_name(match_.typ.range));
+                        arguments.push(self.gen_name(case.ignore_rest.unwrap_or(match_.typ.range)));
                     }
                 }
                 cases_args[index] = Some((case.constructor.range, arguments, &case.value));
@@ -207,10 +207,9 @@ impl<'a> DesugarState<'a> {
 
         for (i, case_arg) in cases_args.iter().enumerate() {
             let case = &sum.constructors[i];
-            if let Some((range, arguments, val)) = &case_arg {
+            if let Some((_, arguments, val)) = &case_arg {
                 let case: Vec<bool> = case.args.iter().map(|x| x.erased).rev().collect();
                 lambdas.push(desugared::Expr::unfold_lambda(
-                    *range,
                     &case,
                     arguments,
                     self.desugar_expr(val),
diff --git a/src/kind-pass/src/desugar/top_level.rs b/src/kind-pass/src/desugar/top_level.rs
index 535cfe1a..2e7301fe 100644
--- a/src/kind-pass/src/desugar/top_level.rs
+++ b/src/kind-pass/src/desugar/top_level.rs
@@ -282,7 +282,7 @@ impl<'a> DesugarState<'a> {
                         }
                     }
                 } else if entry.arguments.len() != spine.len() {
-                    println!("{}: {:?}", head, entry);
+                    println!("Ata {} {:?}", head, spine.iter().map(|x| x.to_string()).collect::<Vec<String>>());
                     self.send_err(PassError::IncorrectArity(
                         head.range,
                         spine.iter().map(|x| x.range).collect(),
diff --git a/src/kind-pass/src/erasure/mod.rs b/src/kind-pass/src/erasure/mod.rs
index 15dde7bb..26893e68 100644
--- a/src/kind-pass/src/erasure/mod.rs
+++ b/src/kind-pass/src/erasure/mod.rs
@@ -308,7 +308,7 @@ impl<'a> ErasureState<'a> {
             Lambda(name, body, erased) => {
                 let ctx = self.ctx.clone();
                 if *erased {
-                    self.ctx.insert(name.to_string(), (name.range, (Some(name.range), Relevance::Irrelevant)));
+                    self.ctx.insert(name.to_string(), (name.range, (None, Relevance::Irrelevant)));
                 } else {
                     self.ctx.insert(name.to_string(), (name.range, *on));
                 }
diff --git a/src/kind-tree/src/concrete/expr.rs b/src/kind-tree/src/concrete/expr.rs
index 5fb9f9d6..b219ee6c 100644
--- a/src/kind-tree/src/concrete/expr.rs
+++ b/src/kind-tree/src/concrete/expr.rs
@@ -57,7 +57,7 @@ pub struct Case {
     pub constructor: Ident,
     pub bindings: Vec<CaseBinding>,
     pub value: Box<Expr>,
-    pub ignore_rest: bool,
+    pub ignore_rest: Option<Range>,
 }
 
 /// A match block that will be desugared
@@ -100,7 +100,7 @@ pub enum Literal {
 /// and just translates into a eliminator for records.
 #[derive(Clone, Debug, Hash, PartialEq, Eq)]
 pub enum Destruct {
-    Destruct(Range, QualifiedIdent, Vec<CaseBinding>, bool),
+    Destruct(Range, QualifiedIdent, Vec<CaseBinding>, Option<Range>),
     Ident(Ident),
 }
 
@@ -284,7 +284,7 @@ impl Display for Destruct {
                 for binding in bindings {
                     write!(f, " {}", binding)?;
                 }
-                if *ignore {
+                if ignore.is_some() {
                     write!(f, " ..")?;
                 }
                 Ok(())
@@ -338,7 +338,7 @@ impl Display for Case {
         for bind in &self.bindings {
             write!(f, " {}", bind)?
         }
-        if self.ignore_rest {
+        if self.ignore_rest.is_some() {
             write!(f, " ..")?;
         }
         write!(f, " => {}; ", self.value)
diff --git a/src/kind-tree/src/desugared/mod.rs b/src/kind-tree/src/desugared/mod.rs
index 2477e917..0e9d7b47 100644
--- a/src/kind-tree/src/desugared/mod.rs
+++ b/src/kind-tree/src/desugared/mod.rs
@@ -112,12 +112,12 @@ impl Expr {
         })
     }
 
-    pub fn unfold_lambda(range: Range, irrelev: &[bool], idents: &[Ident], body: Box<Expr>) -> Box<Expr> {
+    pub fn unfold_lambda(irrelev: &[bool], idents: &[Ident], body: Box<Expr>) -> Box<Expr> {
         idents
             .iter()
             .rev()
             .zip(irrelev)
-            .fold(body, |body, (ident, irrelev)| Expr::lambda(range, ident.clone(), body, *irrelev))
+            .fold(body, |body, (ident, irrelev)| Expr::lambda(ident.range, ident.clone(), body, *irrelev))
     }
 
     pub fn app(range: Range, ident: Box<Expr>, spine: Vec<AppBinding>) -> Box<Expr> {