diff --git a/lang/elaborator/src/typechecker/typecheck.rs b/lang/elaborator/src/typechecker/typecheck.rs index e76d35e7f..81b7aaf93 100644 --- a/lang/elaborator/src/typechecker/typecheck.rs +++ b/lang/elaborator/src/typechecker/typecheck.rs @@ -790,7 +790,7 @@ impl Check for ust::LocalMatch { Ok(tst::LocalMatch { span: *span, - info: tst::TypeAppInfo { typ: typ_app, typ_nf: typ_app_nf }, + info: tst::TypeAppInfo { typ: typ_app }, ctx: Some(ctx.vars.clone()), name: name.clone(), on_exp: on_exp_out, @@ -833,7 +833,7 @@ impl Check for ust::LocalComatch { Ok(tst::LocalComatch { span: *span, - info: tst::TypeAppInfo { typ: typ_app, typ_nf: typ_app_nf }, + info: tst::TypeAppInfo { typ: typ_app }, ctx: Some(ctx.vars.clone()), name: name.clone(), is_lambda_sugar: *is_lambda_sugar, diff --git a/lang/syntax/src/trees/tst/def.rs b/lang/syntax/src/trees/tst/def.rs index 24e47f44d..3d5f3655d 100644 --- a/lang/syntax/src/trees/tst/def.rs +++ b/lang/syntax/src/trees/tst/def.rs @@ -8,6 +8,8 @@ use crate::ust; use crate::generic; +use super::forget::ForgetTST; + #[derive(Default, Clone, Debug, Eq, PartialEq, Hash)] pub struct TST; @@ -65,7 +67,6 @@ impl From> for TypeInfo { #[derive(Debug, Clone)] pub struct TypeAppInfo { pub typ: TypCtor, - pub typ_nf: ust::TypCtor, } pub trait HasTypeInfo { @@ -82,11 +83,11 @@ 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_nf; + let ust::TypCtor { span, name, args } = e.info.clone().typ.forget_tst(); Some(Rc::new(ust::Exp::TypCtor(ust::TypCtor { span, name, args }))) } Exp::LocalComatch(e) => { - let ust::TypCtor { span, name, args } = e.info.clone().typ_nf; + let ust::TypCtor { span, name, args } = e.info.clone().typ.forget_tst(); Some(Rc::new(ust::Exp::TypCtor(ust::TypCtor { span, name, args }))) } Exp::Hole(e) => e.inferred_type.clone(),