diff --git a/lang/elaborator/src/normalizer/eval.rs b/lang/elaborator/src/normalizer/eval.rs
index ebb105837..3ceed6a26 100644
--- a/lang/elaborator/src/normalizer/eval.rs
+++ b/lang/elaborator/src/normalizer/eval.rs
@@ -144,7 +144,7 @@ impl Eval for ust::LocalComatch {
     type Val = Rc<Val>;
 
     fn eval(&self, prg: &ust::Prg, env: &mut Env) -> Result<Self::Val, TypeError> {
-        let ust::LocalComatch { span, info: (), ctx: _, name, is_lambda_sugar, body } = self;
+        let ust::LocalComatch { span, name, is_lambda_sugar, body, .. } = self;
         Ok(Rc::new(Val::Comatch {
             span: *span,
             name: name.clone(),
diff --git a/lang/elaborator/src/normalizer/read_back.rs b/lang/elaborator/src/normalizer/read_back.rs
index e2dffafdf..8b3c4d960 100644
--- a/lang/elaborator/src/normalizer/read_back.rs
+++ b/lang/elaborator/src/normalizer/read_back.rs
@@ -38,11 +38,11 @@ impl ReadBack for val::Val {
             val::Val::Comatch { span, name, is_lambda_sugar, body } => {
                 ust::Exp::LocalComatch(ust::LocalComatch {
                     span: *span,
-                    info: (),
                     ctx: None,
                     name: name.clone(),
                     is_lambda_sugar: *is_lambda_sugar,
                     body: body.read_back(prg)?,
+                    inferred_type: None,
                 })
             }
             val::Val::Neu { exp } => exp.read_back(prg)?,
@@ -71,13 +71,13 @@ impl ReadBack for val::Neu {
             }),
             val::Neu::Match { span, name, on_exp, body } => ust::Exp::LocalMatch(ust::LocalMatch {
                 span: *span,
-                info: (),
                 ctx: None,
                 motive: None,
                 ret_typ: None,
                 name: name.clone(),
                 on_exp: on_exp.read_back(prg)?,
                 body: body.read_back(prg)?,
+                inferred_type: None,
             }),
             val::Neu::Hole { span } => {
                 ust::Exp::Hole(Hole { span: *span, inferred_type: None, inferred_ctx: None })
diff --git a/lang/elaborator/src/typechecker/typecheck.rs b/lang/elaborator/src/typechecker/typecheck.rs
index 81b7aaf93..875fa4a47 100644
--- a/lang/elaborator/src/typechecker/typecheck.rs
+++ b/lang/elaborator/src/typechecker/typecheck.rs
@@ -729,8 +729,7 @@ impl Check for ust::LocalMatch {
         ctx: &mut Ctx,
         t: Rc<ust::Exp>,
     ) -> Result<Self::Target, TypeError> {
-        let ust::LocalMatch { span, info: (), ctx: _, name, on_exp, motive, ret_typ: _, body } =
-            self;
+        let ust::LocalMatch { span, name, on_exp, motive, body, .. } = self;
         let on_exp_out = on_exp.infer(prg, ctx)?;
         let typ_app_nf = on_exp_out
             .typ()
@@ -790,13 +789,13 @@ impl Check for ust::LocalMatch {
 
         Ok(tst::LocalMatch {
             span: *span,
-            info: tst::TypeAppInfo { typ: typ_app },
             ctx: Some(ctx.vars.clone()),
             name: name.clone(),
             on_exp: on_exp_out,
             motive: motive_out,
             ret_typ: ret_typ_out.into(),
             body: body_out,
+            inferred_type: Some(typ_app),
         })
     }
 }
@@ -810,7 +809,7 @@ impl Check for ust::LocalComatch {
         ctx: &mut Ctx,
         t: Rc<ust::Exp>,
     ) -> Result<Self::Target, TypeError> {
-        let ust::LocalComatch { span, info: (), ctx: _, name, is_lambda_sugar, body } = self;
+        let ust::LocalComatch { span, name, is_lambda_sugar, body, .. } = self;
         let typ_app_nf = t.expect_typ_app()?;
         let typ_app = typ_app_nf.infer(prg, ctx)?;
 
@@ -833,11 +832,11 @@ impl Check for ust::LocalComatch {
 
         Ok(tst::LocalComatch {
             span: *span,
-            info: tst::TypeAppInfo { typ: typ_app },
             ctx: Some(ctx.vars.clone()),
             name: name.clone(),
             is_lambda_sugar: *is_lambda_sugar,
             body: body_out,
+            inferred_type: Some(typ_app),
         })
     }
 }
diff --git a/lang/lifting/src/fv.rs b/lang/lifting/src/fv.rs
index 69201d543..7621d5332 100644
--- a/lang/lifting/src/fv.rs
+++ b/lang/lifting/src/fv.rs
@@ -35,14 +35,7 @@ impl FV for ust::Exp {
                 typ.visit_fv(v)
             }
             ust::Exp::Variable(e) => e.visit_fv(v),
-            ust::Exp::LocalComatch(ust::LocalComatch {
-                span: _,
-                info: _,
-                ctx: _,
-                name: _,
-                is_lambda_sugar: _,
-                body,
-            }) => body.visit_fv(v),
+            ust::Exp::LocalComatch(ust::LocalComatch { body, .. }) => body.visit_fv(v),
             ust::Exp::Call(ust::Call { args, .. }) => args.visit_fv(v),
             ust::Exp::DotCall(ust::DotCall { exp, args, .. }) => {
                 exp.visit_fv(v);
@@ -51,16 +44,7 @@ impl FV for ust::Exp {
             ust::Exp::TypCtor(e) => e.visit_fv(v),
             ust::Exp::Hole(Hole { .. }) => {}
             ust::Exp::TypeUniv(TypeUniv { span: _ }) => {}
-            ust::Exp::LocalMatch(ust::LocalMatch {
-                span: _,
-                info: _,
-                ctx: _,
-                name: _,
-                on_exp,
-                motive,
-                ret_typ: _,
-                body,
-            }) => {
+            ust::Exp::LocalMatch(ust::LocalMatch { on_exp, motive, body, .. }) => {
                 on_exp.visit_fv(v);
                 motive.visit_fv(v);
                 body.visit_fv(v)
diff --git a/lang/lifting/src/lib.rs b/lang/lifting/src/lib.rs
index 1d93486d0..22f2ee56e 100644
--- a/lang/lifting/src/lib.rs
+++ b/lang/lifting/src/lib.rs
@@ -417,9 +417,26 @@ impl Lift for tst::LocalMatch {
     type Target = ust::Exp;
 
     fn lift(&self, ctx: &mut Ctx) -> Self::Target {
-        let tst::LocalMatch { span, info, ctx: type_ctx, name, on_exp, motive, ret_typ, body } =
-            self;
-        ctx.lift_match(span, info, &type_ctx.clone().unwrap(), name, on_exp, motive, ret_typ, body)
+        let tst::LocalMatch {
+            span,
+            ctx: type_ctx,
+            name,
+            on_exp,
+            motive,
+            ret_typ,
+            body,
+            inferred_type,
+        } = self;
+        ctx.lift_match(
+            span,
+            &inferred_type.clone().unwrap(),
+            &type_ctx.clone().unwrap(),
+            name,
+            on_exp,
+            motive,
+            ret_typ,
+            body,
+        )
     }
 }
 
@@ -427,8 +444,16 @@ impl Lift for tst::LocalComatch {
     type Target = ust::Exp;
 
     fn lift(&self, ctx: &mut Ctx) -> Self::Target {
-        let tst::LocalComatch { span, info, ctx: type_ctx, name, is_lambda_sugar, body } = self;
-        ctx.lift_comatch(span, info, &type_ctx.clone().unwrap(), name, *is_lambda_sugar, body)
+        let tst::LocalComatch { span, ctx: type_ctx, name, is_lambda_sugar, body, inferred_type } =
+            self;
+        ctx.lift_comatch(
+            span,
+            &inferred_type.clone().unwrap(),
+            &type_ctx.clone().unwrap(),
+            name,
+            *is_lambda_sugar,
+            body,
+        )
     }
 }
 impl Lift for tst::Motive {
@@ -538,7 +563,7 @@ impl Ctx {
     fn lift_match(
         &mut self,
         span: &Option<Span>,
-        info: &tst::TypeAppInfo,
+        inferred_type: &tst::TypCtor,
         type_ctx: &TypeCtx,
         name: &tst::Label,
         on_exp: &Rc<tst::Exp>,
@@ -547,10 +572,10 @@ impl Ctx {
         body: &tst::Match,
     ) -> ust::Exp {
         // Only lift local matches for the specified type
-        if info.typ.name != self.name {
+        if inferred_type.name != self.name {
             return ust::Exp::LocalMatch(ust::LocalMatch {
                 span: *span,
-                info: info.forget_tst(),
+                inferred_type: None,
                 ctx: None,
                 name: name.clone(),
                 on_exp: on_exp.lift(self),
@@ -571,7 +596,7 @@ impl Ctx {
             .unwrap_or_else(|| free_vars(&ret_typ.forget_tst(), type_ctx));
 
         let body = body.lift(self);
-        let self_typ = info.typ.lift(self);
+        let self_typ = inferred_type.lift(self);
 
         let FreeVarsResult { telescope, subst, args } = free_vars(&body, type_ctx)
             .union(free_vars(&self_typ, type_ctx))
@@ -592,7 +617,7 @@ impl Ctx {
         };
 
         // Build the new top-level definition
-        let name = self.unique_def_name(name, &info.typ.name);
+        let name = self.unique_def_name(name, &inferred_type.name);
 
         let def = ust::Def {
             span: None,
@@ -624,28 +649,28 @@ impl Ctx {
     fn lift_comatch(
         &mut self,
         span: &Option<Span>,
-        info: &tst::TypeAppInfo,
+        inferred_type: &tst::TypCtor,
         type_ctx: &TypeCtx,
         name: &tst::Label,
         is_lambda_sugar: bool,
         body: &tst::Match,
     ) -> ust::Exp {
         // Only lift local matches for the specified type
-        if info.typ.name != self.name {
+        if inferred_type.name != self.name {
             return ust::Exp::LocalComatch(ust::LocalComatch {
                 span: *span,
-                info: info.forget_tst(),
                 ctx: None,
                 name: name.clone(),
                 is_lambda_sugar,
                 body: body.lift(self),
+                inferred_type: None,
             });
         }
 
         self.mark_modified();
 
         let body = body.lift(self);
-        let typ = info.typ.lift(self);
+        let typ = inferred_type.lift(self);
 
         // Collect the free variables in the comatch and the return type
         // Build a telescope of the types of the lifted variables
@@ -657,7 +682,7 @@ impl Ctx {
         let typ = typ.subst(&mut self.ctx, &subst.in_body());
 
         // Build the new top-level definition
-        let name = self.unique_codef_name(name, &info.typ.name);
+        let name = self.unique_codef_name(name, &inferred_type.name);
 
         let codef = ust::Codef {
             span: None,
diff --git a/lang/lowering/src/lower/exp.rs b/lang/lowering/src/lower/exp.rs
index 697688d86..d2bd3728e 100644
--- a/lang/lowering/src/lower/exp.rs
+++ b/lang/lowering/src/lower/exp.rs
@@ -174,13 +174,13 @@ impl Lower for cst::exp::LocalMatch {
         let cst::exp::LocalMatch { span, name, on_exp, motive, body } = self;
         Ok(ust::Exp::LocalMatch(ust::LocalMatch {
             span: Some(*span),
-            info: (),
             ctx: None,
             name: ctx.unique_label(name.to_owned(), span)?,
             on_exp: on_exp.lower(ctx)?,
             motive: motive.lower(ctx)?,
             ret_typ: None,
             body: body.lower(ctx)?,
+            inferred_type: None,
         }))
     }
 }
@@ -192,11 +192,11 @@ impl Lower for cst::exp::LocalComatch {
         let cst::exp::LocalComatch { span, name, is_lambda_sugar, body } = self;
         Ok(ust::Exp::LocalComatch(ust::LocalComatch {
             span: Some(*span),
-            info: (),
             ctx: None,
             name: ctx.unique_label(name.to_owned(), span)?,
             is_lambda_sugar: *is_lambda_sugar,
             body: body.lower(ctx)?,
+            inferred_type: None,
         }))
     }
 }
diff --git a/lang/printer/src/generic.rs b/lang/printer/src/generic.rs
index 56a6e3342..5a080d057 100644
--- a/lang/printer/src/generic.rs
+++ b/lang/printer/src/generic.rs
@@ -590,7 +590,7 @@ impl<'a, P: Phase> Print<'a> for LocalMatch<P> {
         alloc: &'a Alloc<'a>,
         _prec: Precedence,
     ) -> Builder<'a> {
-        let LocalMatch { span: _, info: _, ctx: _, name, on_exp, motive, ret_typ: _, body } = self;
+        let LocalMatch { name, on_exp, motive, body, .. } = self;
         on_exp
             .print(cfg, alloc)
             .append(DOT)
@@ -612,7 +612,7 @@ impl<'a, P: Phase> Print<'a> for LocalComatch<P> {
         alloc: &'a Alloc<'a>,
         _prec: Precedence,
     ) -> Builder<'a> {
-        let LocalComatch { span: _, info: _, ctx: _, name, is_lambda_sugar, body } = self;
+        let LocalComatch { name, is_lambda_sugar, body, .. } = self;
         if *is_lambda_sugar && cfg.print_lambda_sugar {
             print_lambda_sugar(body, cfg, alloc)
         } else {
diff --git a/lang/renaming/src/ast.rs b/lang/renaming/src/ast.rs
index 812214149..f91ca03b3 100644
--- a/lang/renaming/src/ast.rs
+++ b/lang/renaming/src/ast.rs
@@ -49,7 +49,6 @@ impl<R: Rename + Clone> Rename for Rc<R> {
 impl<P: Phase> Rename for Prg<P>
 where
     P::TypeInfo: Rename,
-    P::TypeAppInfo: Rename,
 {
     fn rename_in_ctx(self, ctx: &mut Ctx) -> Self {
         let Prg { decls } = self;
@@ -61,7 +60,6 @@ where
 impl<P: Phase> Rename for Decls<P>
 where
     P::TypeInfo: Rename,
-    P::TypeAppInfo: Rename,
 {
     fn rename_in_ctx(self, ctx: &mut Ctx) -> Self {
         Decls {
@@ -74,7 +72,6 @@ where
 impl<P: Phase> Rename for Decl<P>
 where
     P::TypeInfo: Rename,
-    P::TypeAppInfo: Rename,
 {
     fn rename_in_ctx(self, ctx: &mut Ctx) -> Self {
         match self {
@@ -92,7 +89,6 @@ where
 impl<P: Phase> Rename for Data<P>
 where
     P::TypeInfo: Rename,
-    P::TypeAppInfo: Rename,
 {
     fn rename_in_ctx(self, ctx: &mut Ctx) -> Self {
         let Data { span, doc, name, attr, typ, ctors } = self;
@@ -103,7 +99,6 @@ where
 impl<P: Phase> Rename for Codata<P>
 where
     P::TypeInfo: Rename,
-    P::TypeAppInfo: Rename,
 {
     fn rename_in_ctx(self, ctx: &mut Ctx) -> Self {
         let Codata { span, doc, name, attr, typ, dtors } = self;
@@ -115,7 +110,6 @@ where
 impl<P: Phase> Rename for Ctor<P>
 where
     P::TypeInfo: Rename,
-    P::TypeAppInfo: Rename,
 {
     fn rename_in_ctx(self, ctx: &mut Ctx) -> Self {
         let Ctor { span, doc, name, params, typ } = self;
@@ -130,7 +124,6 @@ where
 impl<P: Phase> Rename for Dtor<P>
 where
     P::TypeInfo: Rename,
-    P::TypeAppInfo: Rename,
 {
     fn rename_in_ctx(self, ctx: &mut Ctx) -> Self {
         let Dtor { span, doc, name, params, self_param, ret_typ } = self;
@@ -150,7 +143,6 @@ where
 impl<P: Phase> Rename for Def<P>
 where
     P::TypeInfo: Rename,
-    P::TypeAppInfo: Rename,
 {
     fn rename_in_ctx(self, ctx: &mut Ctx) -> Self {
         let Def { span, doc, name, attr, params, self_param, ret_typ, body } = self;
@@ -180,7 +172,6 @@ where
 impl<P: Phase> Rename for Codef<P>
 where
     P::TypeInfo: Rename,
-    P::TypeAppInfo: Rename,
 {
     fn rename_in_ctx(self, ctx: &mut Ctx) -> Self {
         let Codef { span, doc, name, attr, params, typ, body } = self;
@@ -200,7 +191,6 @@ where
 impl<P: Phase> Rename for Let<P>
 where
     P::TypeInfo: Rename,
-    P::TypeAppInfo: Rename,
 {
     fn rename_in_ctx(self, ctx: &mut Ctx) -> Self {
         let Let { span, doc, name, attr, params, typ, body } = self;
@@ -220,7 +210,6 @@ where
 impl<P: Phase> Rename for TypAbs<P>
 where
     P::TypeInfo: Rename,
-    P::TypeAppInfo: Rename,
 {
     fn rename_in_ctx(self, ctx: &mut Ctx) -> Self {
         let TypAbs { params } = self;
@@ -231,7 +220,6 @@ where
 impl<P: Phase> Rename for Telescope<P>
 where
     P::TypeInfo: Rename,
-    P::TypeAppInfo: Rename,
 {
     fn rename_in_ctx(self, ctx: &mut Ctx) -> Self {
         let Telescope { params } = self;
@@ -253,7 +241,6 @@ where
 impl<P: Phase> Rename for Param<P>
 where
     P::TypeInfo: Rename,
-    P::TypeAppInfo: Rename,
 {
     fn rename_in_ctx(self, ctx: &mut Ctx) -> Self {
         let Param { name, typ } = self;
@@ -268,7 +255,6 @@ where
 impl<P: Phase> Rename for TelescopeInst<P>
 where
     P::TypeInfo: Rename,
-    P::TypeAppInfo: Rename,
 {
     fn rename_in_ctx(self, ctx: &mut Ctx) -> Self {
         let TelescopeInst { params } = self;
@@ -290,7 +276,6 @@ where
 impl<P: Phase> Rename for ParamInst<P>
 where
     P::TypeInfo: Rename,
-    P::TypeAppInfo: Rename,
 {
     fn rename_in_ctx(self, ctx: &mut Ctx) -> Self {
         let ParamInst { span, name, typ, info } = self;
@@ -306,7 +291,6 @@ where
 impl<P: Phase> Rename for SelfParam<P>
 where
     P::TypeInfo: Rename,
-    P::TypeAppInfo: Rename,
 {
     fn rename_in_ctx(self, ctx: &mut Ctx) -> Self {
         let SelfParam { info, name, typ } = self;
@@ -320,19 +304,18 @@ where
 impl<P: Phase> Rename for Exp<P>
 where
     P::TypeInfo: Rename,
-    P::TypeAppInfo: Rename,
 {
     fn rename_in_ctx(self, ctx: &mut Ctx) -> Self {
         match self {
             Exp::Variable(e) => Exp::Variable(e.rename_in_ctx(ctx)),
-            Exp::LocalComatch(LocalComatch { span, info, ctx: _, name, is_lambda_sugar, body }) => {
+            Exp::LocalComatch(LocalComatch { span, name, is_lambda_sugar, body, .. }) => {
                 Exp::LocalComatch(LocalComatch {
                     span,
-                    info: info.rename_in_ctx(ctx),
                     ctx: None,
                     name,
                     is_lambda_sugar,
                     body: body.rename_in_ctx(ctx),
+                    inferred_type: None,
                 })
             }
             Exp::Anno(Anno { span, exp, typ, normalized_type }) => Exp::Anno(Anno {
@@ -354,25 +337,18 @@ where
                 args: args.rename_in_ctx(ctx),
                 inferred_type: inferred_type.rename_in_ctx(ctx),
             }),
-            Exp::LocalMatch(LocalMatch {
-                span,
-                info,
-                ctx: _,
-                name,
-                on_exp,
-                motive,
-                ret_typ,
-                body,
-            }) => Exp::LocalMatch(LocalMatch {
-                span,
-                info: info.rename_in_ctx(ctx),
-                ctx: None,
-                name,
-                on_exp: on_exp.rename_in_ctx(ctx),
-                motive: motive.rename_in_ctx(ctx),
-                ret_typ: ret_typ.rename_in_ctx(ctx),
-                body: body.rename_in_ctx(ctx),
-            }),
+            Exp::LocalMatch(LocalMatch { span, name, on_exp, motive, ret_typ, body, .. }) => {
+                Exp::LocalMatch(LocalMatch {
+                    span,
+                    ctx: None,
+                    name,
+                    on_exp: on_exp.rename_in_ctx(ctx),
+                    motive: motive.rename_in_ctx(ctx),
+                    ret_typ: ret_typ.rename_in_ctx(ctx),
+                    body: body.rename_in_ctx(ctx),
+                    inferred_type: None,
+                })
+            }
             Exp::DotCall(DotCall { span, exp, name, args, inferred_type }) => {
                 Exp::DotCall(DotCall {
                     span,
@@ -400,7 +376,6 @@ impl Rename for Variable {
 impl<P: Phase> Rename for TypCtor<P>
 where
     P::TypeInfo: Rename,
-    P::TypeAppInfo: Rename,
 {
     fn rename_in_ctx(self, ctx: &mut Ctx) -> Self {
         let TypCtor { span, name, args } = self;
@@ -411,7 +386,6 @@ where
 impl<P: Phase> Rename for Match<P>
 where
     P::TypeInfo: Rename,
-    P::TypeAppInfo: Rename,
 {
     fn rename_in_ctx(self, ctx: &mut Ctx) -> Self {
         let Match { span, cases, omit_absurd } = self;
@@ -423,7 +397,6 @@ where
 impl<P: Phase> Rename for Args<P>
 where
     P::TypeInfo: Rename,
-    P::TypeAppInfo: Rename,
 {
     fn rename_in_ctx(self, ctx: &mut Ctx) -> Self {
         let Args { args } = self;
@@ -435,7 +408,6 @@ where
 impl<P: Phase> Rename for Case<P>
 where
     P::TypeInfo: Rename,
-    P::TypeAppInfo: Rename,
 {
     fn rename_in_ctx(self, ctx: &mut Ctx) -> Self {
         let Case { span, name, params, body } = self;
@@ -453,7 +425,6 @@ where
 impl<P: Phase> Rename for Motive<P>
 where
     P::TypeInfo: Rename,
-    P::TypeAppInfo: Rename,
 {
     fn rename_in_ctx(self, ctx: &mut Ctx) -> Self {
         let Motive { span, param, ret_typ } = self;
diff --git a/lang/syntax/src/trees/generic/exp.rs b/lang/syntax/src/trees/generic/exp.rs
index d841a9963..987986baa 100644
--- a/lang/syntax/src/trees/generic/exp.rs
+++ b/lang/syntax/src/trees/generic/exp.rs
@@ -7,6 +7,7 @@ use derivative::Derivative;
 
 use crate::common::*;
 use crate::ctx::values::TypeCtx;
+use crate::tst::TST;
 use crate::ust::UST;
 
 pub trait Phase
@@ -15,9 +16,6 @@ where
 {
     /// Type of the `info` field, containing (depending on the phase) type information
     type TypeInfo: Clone + fmt::Debug;
-    /// Type of the `info` field, containing (depending on the phase) type information
-    /// where the type is required to be the full application of a type constructor
-    type TypeAppInfo: Clone + fmt::Debug;
 }
 
 #[derive(Debug, Clone, Derivative)]
@@ -282,8 +280,6 @@ pub struct LocalMatch<P: Phase> {
     #[derivative(PartialEq = "ignore", Hash = "ignore")]
     pub span: Option<Span>,
     #[derivative(PartialEq = "ignore", Hash = "ignore")]
-    pub info: P::TypeAppInfo,
-    #[derivative(PartialEq = "ignore", Hash = "ignore")]
     pub ctx: Option<TypeCtx>,
     pub name: Label,
     pub on_exp: Rc<Exp<P>>,
@@ -291,6 +287,8 @@ pub struct LocalMatch<P: Phase> {
     #[derivative(PartialEq = "ignore", Hash = "ignore")]
     pub ret_typ: Option<Rc<Exp<P>>>,
     pub body: Match<P>,
+    #[derivative(PartialEq = "ignore", Hash = "ignore")]
+    pub inferred_type: Option<TypCtor<TST>>,
 }
 
 impl<P: Phase> HasSpan for LocalMatch<P> {
@@ -309,12 +307,12 @@ pub struct LocalComatch<P: Phase> {
     #[derivative(PartialEq = "ignore", Hash = "ignore")]
     pub span: Option<Span>,
     #[derivative(PartialEq = "ignore", Hash = "ignore")]
-    pub info: P::TypeAppInfo,
-    #[derivative(PartialEq = "ignore", Hash = "ignore")]
     pub ctx: Option<TypeCtx>,
     pub name: Label,
     pub is_lambda_sugar: bool,
     pub body: Match<P>,
+    #[derivative(PartialEq = "ignore", Hash = "ignore")]
+    pub inferred_type: Option<TypCtor<TST>>,
 }
 
 impl<P: Phase> HasSpan for LocalComatch<P> {
diff --git a/lang/syntax/src/trees/tst/def.rs b/lang/syntax/src/trees/tst/def.rs
index 3d5f3655d..06e23e22e 100644
--- a/lang/syntax/src/trees/tst/def.rs
+++ b/lang/syntax/src/trees/tst/def.rs
@@ -15,7 +15,6 @@ pub struct TST;
 
 impl generic::Phase for TST {
     type TypeInfo = TypeInfo;
-    type TypeAppInfo = TypeAppInfo;
 }
 
 pub type Ident = generic::Ident;
@@ -64,11 +63,6 @@ impl From<Rc<ust::Exp>> for TypeInfo {
     }
 }
 
-#[derive(Debug, Clone)]
-pub struct TypeAppInfo {
-    pub typ: TypCtor,
-}
-
 pub trait HasTypeInfo {
     fn typ(&self) -> Option<Rc<ust::Exp>>;
 }
@@ -83,12 +77,10 @@ impl HasTypeInfo for Exp {
             Exp::Anno(e) => e.normalized_type.clone(),
             Exp::TypeUniv(_) => Some(Rc::new(ust::Exp::TypeUniv(TypeUniv { span: None }))),
             Exp::LocalMatch(e) => {
-                let ust::TypCtor { span, name, args } = e.info.clone().typ.forget_tst();
-                Some(Rc::new(ust::Exp::TypCtor(ust::TypCtor { span, name, args })))
+                e.inferred_type.forget_tst().map(|typctor| Rc::new(ust::Exp::TypCtor(typctor)))
             }
             Exp::LocalComatch(e) => {
-                let ust::TypCtor { span, name, args } = e.info.clone().typ.forget_tst();
-                Some(Rc::new(ust::Exp::TypCtor(ust::TypCtor { span, name, args })))
+                e.inferred_type.forget_tst().map(|typctor| Rc::new(ust::Exp::TypCtor(typctor)))
             }
             Exp::Hole(e) => e.inferred_type.clone(),
         }
diff --git a/lang/syntax/src/trees/tst/forget.rs b/lang/syntax/src/trees/tst/forget.rs
index 5974689f1..29ba50909 100644
--- a/lang/syntax/src/trees/tst/forget.rs
+++ b/lang/syntax/src/trees/tst/forget.rs
@@ -331,16 +331,16 @@ impl ForgetTST for LocalMatch {
     type Target = ust::LocalMatch;
 
     fn forget_tst(&self) -> Self::Target {
-        let LocalMatch { span, info, ctx: _, name, on_exp, motive, ret_typ, body } = self;
+        let LocalMatch { span, ctx: _, name, on_exp, motive, ret_typ, body, .. } = self;
         ust::LocalMatch {
             span: *span,
-            info: info.forget_tst(),
             ctx: None,
             name: name.clone(),
             on_exp: on_exp.forget_tst(),
             motive: motive.forget_tst(),
             ret_typ: ret_typ.forget_tst(),
             body: body.forget_tst(),
+            inferred_type: None,
         }
     }
 }
@@ -349,15 +349,15 @@ impl ForgetTST for LocalComatch {
     type Target = ust::LocalComatch;
 
     fn forget_tst(&self) -> Self::Target {
-        let LocalComatch { span, info, ctx: _, name, is_lambda_sugar, body } = self;
+        let LocalComatch { span, ctx: _, name, is_lambda_sugar, body, .. } = self;
 
         ust::LocalComatch {
             span: *span,
-            info: info.forget_tst(),
             ctx: None,
             name: name.clone(),
             is_lambda_sugar: *is_lambda_sugar,
             body: body.forget_tst(),
+            inferred_type: None,
         }
     }
 }
@@ -439,9 +439,3 @@ impl ForgetTST for TypeInfo {
 
     fn forget_tst(&self) -> Self::Target {}
 }
-
-impl ForgetTST for TypeAppInfo {
-    type Target = ();
-
-    fn forget_tst(&self) -> Self::Target {}
-}
diff --git a/lang/syntax/src/trees/ust/def.rs b/lang/syntax/src/trees/ust/def.rs
index f391f1c15..22caf7882 100644
--- a/lang/syntax/src/trees/ust/def.rs
+++ b/lang/syntax/src/trees/ust/def.rs
@@ -5,7 +5,6 @@ pub struct UST;
 
 impl generic::Phase for UST {
     type TypeInfo = ();
-    type TypeAppInfo = ();
 }
 
 pub type Ident = generic::Ident;
diff --git a/lang/syntax/src/trees/ust/shift.rs b/lang/syntax/src/trees/ust/shift.rs
index 0b360c79f..0b236e434 100644
--- a/lang/syntax/src/trees/ust/shift.rs
+++ b/lang/syntax/src/trees/ust/shift.rs
@@ -85,30 +85,30 @@ impl Shift for TypeUniv {
 
 impl Shift for LocalMatch {
     fn shift_in_range<R: ShiftRange>(&self, range: R, by: (isize, isize)) -> Self {
-        let LocalMatch { span, info, ctx: _, name, on_exp, motive, ret_typ: _, body } = self;
+        let LocalMatch { span, name, on_exp, motive, body, .. } = self;
         LocalMatch {
             span: *span,
-            info: *info,
             ctx: None,
             name: name.clone(),
             on_exp: on_exp.shift_in_range(range.clone(), by),
             motive: motive.shift_in_range(range.clone(), by),
             ret_typ: None,
             body: body.shift_in_range(range, by),
+            inferred_type: None,
         }
     }
 }
 
 impl Shift for LocalComatch {
     fn shift_in_range<R: ShiftRange>(&self, range: R, by: (isize, isize)) -> Self {
-        let LocalComatch { span, info, ctx: _, name, is_lambda_sugar, body } = self;
+        let LocalComatch { span, name, is_lambda_sugar, body, .. } = self;
         LocalComatch {
             span: *span,
-            info: *info,
             ctx: None,
             name: name.clone(),
             is_lambda_sugar: *is_lambda_sugar,
             body: body.shift_in_range(range, by),
+            inferred_type: None,
         }
     }
 }
diff --git a/lang/syntax/src/trees/ust/subst.rs b/lang/syntax/src/trees/ust/subst.rs
index 168f5542d..cc06c21c3 100644
--- a/lang/syntax/src/trees/ust/subst.rs
+++ b/lang/syntax/src/trees/ust/subst.rs
@@ -42,33 +42,26 @@ impl Substitutable<Rc<Exp>> for Rc<Exp> {
                 normalized_type: None,
             })),
             Exp::TypeUniv(TypeUniv { span }) => Rc::new(Exp::TypeUniv(TypeUniv { span: *span })),
-            Exp::LocalMatch(LocalMatch {
-                span,
-                info,
-                ctx: _,
-                name,
-                on_exp,
-                motive,
-                ret_typ,
-                body,
-            }) => Rc::new(Exp::LocalMatch(LocalMatch {
-                span: *span,
-                info: *info,
-                ctx: None,
-                name: name.clone(),
-                on_exp: on_exp.subst(ctx, by),
-                motive: motive.subst(ctx, by),
-                ret_typ: ret_typ.subst(ctx, by),
-                body: body.subst(ctx, by),
-            })),
-            Exp::LocalComatch(LocalComatch { span, info, ctx: _, name, is_lambda_sugar, body }) => {
+            Exp::LocalMatch(LocalMatch { span, name, on_exp, motive, ret_typ, body, .. }) => {
+                Rc::new(Exp::LocalMatch(LocalMatch {
+                    span: *span,
+                    ctx: None,
+                    name: name.clone(),
+                    on_exp: on_exp.subst(ctx, by),
+                    motive: motive.subst(ctx, by),
+                    ret_typ: ret_typ.subst(ctx, by),
+                    body: body.subst(ctx, by),
+                    inferred_type: None,
+                }))
+            }
+            Exp::LocalComatch(LocalComatch { span, name, is_lambda_sugar, body, .. }) => {
                 Rc::new(Exp::LocalComatch(LocalComatch {
                     span: *span,
-                    info: *info,
                     ctx: None,
                     name: name.clone(),
                     is_lambda_sugar: *is_lambda_sugar,
                     body: body.subst(ctx, by),
+                    inferred_type: None,
                 }))
             }
             Exp::Hole(Hole { span, .. }) => {