From 7080bbe44d0eb815b4145d5f97e9c8587ac60038 Mon Sep 17 00:00:00 2001
From: Nicolas Abril <nicolas@higherorderco.com>
Date: Wed, 9 Oct 2024 14:58:52 +0000
Subject: [PATCH] Resolve type constructors in the types of constructor fields
 (#728)

---
 src/fun/check/type_check.rs                      |  6 +++---
 src/fun/net_to_term.rs                           | 16 ++++++++--------
 src/fun/transform/resolve_type_ctrs.rs           |  4 ++++
 .../desugar_file/fail_type_bad_rec_fn_adt.bend   | 12 ++++++++++++
 ...ugar_file__fail_type_bad_rec_fn_adt.bend.snap |  7 +++++++
 5 files changed, 34 insertions(+), 11 deletions(-)
 create mode 100644 tests/golden_tests/desugar_file/fail_type_bad_rec_fn_adt.bend
 create mode 100644 tests/snapshots/desugar_file__fail_type_bad_rec_fn_adt.bend.snap

diff --git a/src/fun/check/type_check.rs b/src/fun/check/type_check.rs
index a06935c11..8bcb8be27 100644
--- a/src/fun/check/type_check.rs
+++ b/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.
diff --git a/src/fun/net_to_term.rs b/src/fun/net_to_term.rs
index 5ac6aebd9..21cea1a9b 100644
--- a/src/fun/net_to_term.rs
+++ b/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;
diff --git a/src/fun/transform/resolve_type_ctrs.rs b/src/fun/transform/resolve_type_ctrs.rs
index a8ac534d9..6d12ceb24 100644
--- a/src/fun/transform/resolve_type_ctrs.rs
+++ b/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());
+        }
       }
     }
 
diff --git a/tests/golden_tests/desugar_file/fail_type_bad_rec_fn_adt.bend b/tests/golden_tests/desugar_file/fail_type_bad_rec_fn_adt.bend
new file mode 100644
index 000000000..9ff448210
--- /dev/null
+++ b/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))
diff --git a/tests/snapshots/desugar_file__fail_type_bad_rec_fn_adt.bend.snap b/tests/snapshots/desugar_file__fail_type_bad_rec_fn_adt.bend.snap
new file mode 100644
index 000000000..843358d27
--- /dev/null
+++ b/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)'.