Fix bug in forget_tst function

polarity-lang · Apr 30, 2024 · fcf3738 · fcf3738
1 parent 1c7870f
commit fcf3738
Show file tree

Hide file tree

Showing 4 changed files with 13 additions and 28 deletions.
diff --git a/lang/lifting/src/lib.rs b/lang/lifting/src/lib.rs
@@ -528,9 +528,9 @@ impl Lift for tst::ParamInst {
     type Target = ust::ParamInst;
 
     fn lift(&self, _ctx: &mut Ctx) -> Self::Target {
-        let tst::ParamInst { span, info, name, typ: _ } = self;
+        let tst::ParamInst { span, name, typ: _, .. } = self;
 
-        ust::ParamInst { span: *span, info: info.forget_tst(), name: name.clone(), typ: None }
+        ust::ParamInst { span: *span, info: None, name: name.clone(), typ: None }
     }
 }
 
@@ -593,7 +593,7 @@ impl Ctx {
         let ret_fvs = motive
             .as_ref()
             .map(|m| free_vars(&m.forget_tst(), type_ctx))
-            .unwrap_or_else(|| free_vars(&ret_typ.forget_tst(), type_ctx));
+            .unwrap_or_else(|| free_vars(&ret_typ.as_ref().map(|x| x.forget_tst()), type_ctx));
 
         let body = body.lift(self);
         let self_typ = inferred_type.lift(self);

diff --git a/lang/renaming/src/ast.rs b/lang/renaming/src/ast.rs
@@ -233,13 +233,12 @@ impl Rename for TelescopeInst {
 
 impl Rename for ParamInst {
     fn rename_in_ctx(self, ctx: &mut Ctx) -> Self {
-        let ParamInst { span, name, typ, info } = self;
+        let ParamInst { span, name, typ, .. } = self;
 
         let new_typ = typ.rename_in_ctx(ctx);
         let new_name = ctx.disambiguate_name(name);
-        let new_info = info.rename_in_ctx(ctx);
 
-        ParamInst { span, name: new_name, typ: new_typ, info: new_info }
+        ParamInst { span, name: new_name, typ: new_typ, info: None }
     }
 }
 

diff --git a/lang/syntax/src/trees/tst/def.rs b/lang/syntax/src/trees/tst/def.rs
@@ -7,8 +7,6 @@ use crate::ust;
 
 use crate::generic;
 
-use super::forget::ForgetTST;
-
 pub type Ident = generic::Ident;
 pub type Label = generic::Label;
 pub type DocComment = generic::DocComment;
@@ -56,12 +54,8 @@ impl HasTypeInfo for Exp {
             Exp::DotCall(e) => e.inferred_type.clone(),
             Exp::Anno(e) => e.normalized_type.clone(),
             Exp::TypeUniv(_) => Some(Rc::new(ust::Exp::TypeUniv(TypeUniv { span: None }))),
-            Exp::LocalMatch(e) => {
-                e.inferred_type.forget_tst().map(|typctor| Rc::new(ust::Exp::TypCtor(typctor)))
-            }
-            Exp::LocalComatch(e) => {
-                e.inferred_type.forget_tst().map(|typctor| Rc::new(ust::Exp::TypCtor(typctor)))
-            }
+            Exp::LocalMatch(e) => e.inferred_type.clone().map(|x| Rc::new(x.into())),
+            Exp::LocalComatch(e) => e.inferred_type.clone().map(|x| Rc::new(x.into())),
             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
@@ -22,14 +22,6 @@ impl<T: ForgetTST> ForgetTST for Rc<T> {
     }
 }
 
-impl<T: ForgetTST> ForgetTST for Option<T> {
-    type Target = Option<T::Target>;
-
-    fn forget_tst(&self) -> Self::Target {
-        self.as_ref().map(ForgetTST::forget_tst)
-    }
-}
-
 impl<T: ForgetTST> ForgetTST for Vec<T> {
     type Target = Vec<T::Target>;
 
@@ -229,7 +221,7 @@ impl ForgetTST for Case {
             span: *span,
             name: name.clone(),
             params: params.forget_tst(),
-            body: body.forget_tst(),
+            body: body.as_ref().map(|x| x.forget_tst()),
         }
     }
 }
@@ -337,8 +329,8 @@ impl ForgetTST for LocalMatch {
             ctx: None,
             name: name.clone(),
             on_exp: on_exp.forget_tst(),
-            motive: motive.forget_tst(),
-            ret_typ: ret_typ.forget_tst(),
+            motive: motive.as_ref().map(|x| x.forget_tst()),
+            ret_typ: ret_typ.as_ref().map(|x| x.forget_tst()),
             body: body.forget_tst(),
             inferred_type: None,
         }
@@ -415,13 +407,13 @@ impl ForgetTST for ParamInst {
     type Target = ust::ParamInst;
 
     fn forget_tst(&self) -> Self::Target {
-        let ParamInst { span, info, name, typ } = self;
+        let ParamInst { span, name, typ, .. } = self;
 
         ust::ParamInst {
             span: *span,
-            info: info.forget_tst(),
+            info: None,
             name: name.clone(),
-            typ: typ.forget_tst(),
+            typ: typ.as_ref().map(|x| x.forget_tst()),
         }
     }
 }