Resolve type constructors in the types of constructor fields (#728)

src/fun/check/type_check.rs

@@ -24,15 +24,15 @@ impl Ctx<'_> {
 type ProgramTypes = HashMap<Name, Scheme>;
 
 /// A type scheme, aka a polymorphic type.
-#[derive(Clone)]
+#[derive(Clone, Debug)]
 struct Scheme(Vec<Name>, Type);
 
 /// A finite mapping from type variables to types.
-#[derive(Clone, Default)]
+#[derive(Clone, Default, Debug)]
 struct Subst(BTreeMap<Name, Type>);
 
 /// A mapping from term variables to type schemes.
-#[derive(Clone, Default)]
+#[derive(Clone, Default, Debug)]
 struct TypeEnv(BTreeMap<Name, Scheme>);
 
 /// Variable generator for type variables.

src/fun/net_to_term.rs

@@ -440,29 +440,29 @@ impl Reader<'_> {
           return Term::Err;
         }
 
-        let zero_term = self.read_term(self.net.enter_port(Port(sel_node, 1)));
-        let mut succ_term = self.read_term(self.net.enter_port(Port(sel_node, 2)));
+        let zero = self.read_term(self.net.enter_port(Port(sel_node, 1)));
+        let mut succ = self.read_term(self.net.enter_port(Port(sel_node, 2)));
         // Call expand_generated in case of succ_term be a lifted term
-        succ_term.expand_generated(self.book, self.recursive_defs);
+        succ.expand_generated(self.book, self.recursive_defs);
 
         // Succ term should be a lambda
-        let (zero, succ) = match &mut succ_term {
+        let succ = match &mut succ {
           Term::Lam { pat, bod, .. } => {
             if let Pattern::Var(nam) = pat.as_ref() {
               let mut bod = std::mem::take(bod.as_mut());
               if let Some(nam) = nam {
                 bod.subst(nam, &Term::Var { nam: Name::new(format!("{bnd}-1")) });
               }
-              (zero_term, bod)
+              bod
             } else {
               // Readback should never generate non-var patterns for lambdas.
               self.error(ReadbackError::InvalidNumericMatch);
-              (zero_term, succ_term)
+              succ
             }
           }
           _ => {
             self.error(ReadbackError::InvalidNumericMatch);
-            (zero_term, succ_term)
+            succ
           }
         };
         Term::Swt {
@@ -562,7 +562,7 @@ impl Reader<'_> {
   /// Returns whether the given port represents a tuple or some other
   /// term (usually a lambda).
   ///
-  /// Used heuristic: a con node is a tuple if port 1 is a closed net and not an ERA.
+  /// Used heuristic: a con node is a tuple if port 1 is a closed tree and not an ERA.
   fn is_tup(&self, node: NodeId) -> bool {
     if !matches!(self.net.node(node).kind, NodeKind::Ctr(CtrKind::Con(_))) {
       return false;

src/fun/transform/resolve_type_ctrs.rs

@@ -17,6 +17,10 @@ impl Ctx<'_> {
       for ctr in adt.ctrs.values_mut() {
         let res = ctr.typ.resolve_type_ctrs(&adts);
         self.info.take_rule_err(res, ctr.name.clone());
+        for field in ctr.fields.iter_mut() {
+          let res = field.typ.resolve_type_ctrs(&adts);
+          self.info.take_rule_err(res, ctr.name.clone());
+        }
       }
     }
 

tests/golden_tests/desugar_file/fail_type_bad_rec_fn_adt.bend

@@ -0,0 +1,12 @@
+# Should give a type error in Erase when unifying the field of type Unit with the match type of Box 
+type Box:
+  Box {x: Unit}
+
+type Unit:
+  Unit
+
+Erase: Box -> None
+(Erase (Box/Box x)) = (Erase x)
+
+main: None
+main = (Erase (Box/Box Unit/Unit))

tests/snapshots/desugar_file__fail_type_bad_rec_fn_adt.bend.snap

@@ -0,0 +1,7 @@
+---
+source: tests/golden_tests.rs
+input_file: tests/golden_tests/desugar_file/fail_type_bad_rec_fn_adt.bend
+---
+Errors:
+In λa match a { Box/Box b: (Erase b); }:
+  Can't unify '(Unit -> d)' and '(Box -> d)'.