Remove typ_nf from TypAppInfo

polarity-lang · Apr 28, 2024 · 392dc3b · 392dc3b
1 parent 97b23ba
commit 392dc3b
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 5 deletions.
diff --git 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
@@ -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<Rc<ust::Exp>> 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(),