Fixes incorrect variable names in type mismatch errors (#1313)

* Fixes incorrect variable names in type mismatch errors

In certain cases, it was possible for a row type variable to alias an
existing type variable, causing confusing error messages. This commit
fixes that by tracking type variable kinds together with their IDs.

Fixes #1312

Co-authored-by: Matthew Healy <matthew.healy@tweag.io>

* Pass VarId and VarKind separately for nicer call sites

* Update test expectations

---------

Co-authored-by: Matthew Healy <matthew.healy@tweag.io>

src/typecheck/mod.rs

@@ -102,6 +102,9 @@ pub type Wildcards = Vec<Types>;
 /// Unification variable or type constants unique identifier.
 pub type VarId = usize;
 
+/// A table mapping variable IDs with their kind to names.
+pub type NameTable = HashMap<(VarId, VarKind), Ident>;
+
 /// A unifiable record row.
 pub type GenericUnifRecordRow<E> = RecordRowF<Box<GenericUnifType<E>>>;
 
@@ -722,11 +725,12 @@ pub struct State<'a> {
     table: &'a mut UnifTable,
     /// Row constraints.
     constr: &'a mut RowConstr,
-    /// A mapping from unification variable or constants to the name of the corresponding type
-    /// variable which introduced it, if any.
+    /// A mapping from unification variables or constants together with their
+    /// kind to the name of the corresponding type variable which introduced it,
+    /// if any.
     ///
     /// Used for error reporting.
-    names: &'a mut HashMap<VarId, Ident>,
+    names: &'a mut NameTable,
     /// A mapping from wildcard ID to unification variable.
     wildcard_vars: &'a mut Vec<UnifType>,
 }
@@ -735,7 +739,7 @@ pub struct State<'a> {
 /// It is basically an owned-subset of the typechecking state.
 pub struct Extra {
     pub table: UnifTable,
-    pub names: HashMap<VarId, Ident>,
+    pub names: NameTable,
     pub wildcards: Vec<Types>,
 }
 
@@ -2450,7 +2454,7 @@ fn instantiate_foralls(state: &mut State, mut ty: UnifType, inst: ForallInst) ->
                     ForallInst::Constant => UnifType::Constant(fresh_uid),
                     ForallInst::Ptr => UnifType::UnifVar(fresh_uid),
                 };
-                state.names.insert(fresh_uid, var);
+                state.names.insert((fresh_uid, var_kind), var);
                 ty = body.subst_type(&var, &uvar);
             }
             VarKind::RecordRows => {
@@ -2459,7 +2463,7 @@ fn instantiate_foralls(state: &mut State, mut ty: UnifType, inst: ForallInst) ->
                     ForallInst::Constant => UnifRecordRows::Constant(fresh_uid),
                     ForallInst::Ptr => UnifRecordRows::UnifVar(fresh_uid),
                 };
-                state.names.insert(fresh_uid, var);
+                state.names.insert((fresh_uid, var_kind), var);
                 ty = body.subst_rrows(&var, &uvar);
 
                 if inst == ForallInst::Ptr {
@@ -2472,7 +2476,7 @@ fn instantiate_foralls(state: &mut State, mut ty: UnifType, inst: ForallInst) ->
                     ForallInst::Constant => UnifEnumRows::Constant(fresh_uid),
                     ForallInst::Ptr => UnifEnumRows::UnifVar(fresh_uid),
                 };
-                state.names.insert(fresh_uid, var);
+                state.names.insert((fresh_uid, var_kind), var);
                 ty = body.subst_erows(&var, &uvar);
 
                 if inst == ForallInst::Ptr {

src/typecheck/reporting.rs

@@ -6,7 +6,7 @@ use std::collections::HashSet;
 /// A name registry used to replace unification variables and type constants with human-readable
 /// and distinct names.
 pub struct NameReg {
-    reg: HashMap<usize, Ident>,
+    reg: NameTable,
     taken: HashSet<String>,
     var_count: usize,
     cst_count: usize,
@@ -33,18 +33,23 @@ impl NameReg {
 /// the given counter to generate a new single letter.
 ///
 /// Generated name is clearly not necessarily unique. This is handled by [`select_uniq`].
-fn mk_name(names: &HashMap<usize, Ident>, counter: &mut usize, id: usize) -> String {
-    match names.get(&id) {
+fn mk_name(names: &NameTable, counter: &mut usize, id: VarId, kind: VarKind) -> String {
+    match names.get(&(id, kind)) {
         // First check if that constant or variable was introduced by a forall. If it was, try
         // to use the same name.
         Some(orig) => format!("{orig}"),
         None => {
             //Otherwise, generate a new character
             let next = *counter;
             *counter += 1;
-            std::char::from_u32(('a' as u32) + ((next % 26) as u32))
-                .unwrap()
-                .to_string()
+
+            let prefix = match kind {
+                VarKind::Type => "",
+                VarKind::EnumRows => "erows_",
+                VarKind::RecordRows => "rrows_",
+            };
+            let character = std::char::from_u32(('a' as u32) + ((next % 26) as u32)).unwrap();
+            format!("{prefix}{character}")
         }
     }
 }
@@ -54,7 +59,7 @@ fn mk_name(names: &HashMap<usize, Ident>, counter: &mut usize, id: usize) -> Str
 ///
 /// If the name is already taken, it just iterates by adding a numeric suffix `1`, `2`, .., and so
 /// on until a free name is found. See `var_to_type` and `cst_to_type`.
-fn select_uniq(name_reg: &mut NameReg, mut name: String, id: usize) -> Ident {
+fn select_uniq(name_reg: &mut NameReg, mut name: String, id: VarId, kind: VarKind) -> Ident {
     // To avoid clashing with already picked names, we add a numeric suffix to the picked
     // letter.
     if name_reg.taken.contains(&name) {
@@ -68,30 +73,30 @@ fn select_uniq(name_reg: &mut NameReg, mut name: String, id: usize) -> Ident {
     }
 
     let ident = Ident::from(name);
-    name_reg.reg.insert(id, ident);
+    name_reg.reg.insert((id, kind), ident);
     ident
 }
 
 /// Either retrieve or generate a new fresh name for a unification variable for error reporting,
 /// and wrap it as an identifier. Unification variables are named `_a`, `_b`, .., `_a1`, `_b1`, ..
 /// and so on.
-fn var_name(names: &HashMap<usize, Ident>, name_reg: &mut NameReg, p: usize) -> Ident {
-    name_reg.reg.get(&p).cloned().unwrap_or_else(|| {
+fn var_name(names: &NameTable, name_reg: &mut NameReg, id: VarId, kind: VarKind) -> Ident {
+    name_reg.reg.get(&(id, kind)).cloned().unwrap_or_else(|| {
         // Select a candidate name and add a "_" prefix
-        let name = format!("_{}", mk_name(names, &mut name_reg.var_count, p));
+        let name = format!("_{}", mk_name(names, &mut name_reg.var_count, id, kind));
         // Add a suffix to make it unique if it has already been picked
-        select_uniq(name_reg, name, p)
+        select_uniq(name_reg, name, id, kind)
     })
 }
 
 /// Either retrieve or generate a new fresh name for a constant for error reporting, and wrap it as
 /// type variable. Constant are named `a`, `b`, .., `a1`, `b1`, .. and so on.
-fn cst_name(names: &HashMap<usize, Ident>, name_reg: &mut NameReg, c: usize) -> Ident {
-    name_reg.reg.get(&c).cloned().unwrap_or_else(|| {
+fn cst_name(names: &NameTable, name_reg: &mut NameReg, id: VarId, kind: VarKind) -> Ident {
+    name_reg.reg.get(&(id, kind)).cloned().unwrap_or_else(|| {
         // Select a candidate name
-        let name = mk_name(names, &mut name_reg.cst_count, c);
+        let name = mk_name(names, &mut name_reg.cst_count, id, kind);
         // Add a suffix to make it unique if it has already been picked
-        select_uniq(name_reg, name, c)
+        select_uniq(name_reg, name, id, kind)
     })
 }
 
@@ -105,13 +110,13 @@ fn cst_name(names: &HashMap<usize, Ident>, name_reg: &mut NameReg, c: usize) ->
 /// than having `Dyn` everywhere.
 pub fn to_type(
     table: &UnifTable,
-    reported_names: &HashMap<usize, Ident>,
+    reported_names: &NameTable,
     names: &mut NameReg,
     ty: UnifType,
 ) -> Types {
     fn rrows_to_type(
         table: &UnifTable,
-        reported_names: &HashMap<usize, Ident>,
+        reported_names: &NameTable,
         names: &mut NameReg,
         rrows: UnifRecordRows,
     ) -> RecordRows {
@@ -122,10 +127,14 @@ pub fn to_type(
                 reported_names,
                 names,
                 var_id,
+                VarKind::RecordRows,
+            ))),
+            UnifRecordRows::Constant(c) => RecordRows(RecordRowsF::TailVar(cst_name(
+                reported_names,
+                names,
+                c,
+                VarKind::RecordRows,
             ))),
-            UnifRecordRows::Constant(c) => {
-                RecordRows(RecordRowsF::TailVar(cst_name(reported_names, names, c)))
-            }
             UnifRecordRows::Concrete(t) => {
                 let mapped = t.map_state(
                     |btyp, names| Box::new(to_type(table, reported_names, names, *btyp)),
@@ -139,19 +148,25 @@ pub fn to_type(
 
     fn erows_to_type(
         table: &UnifTable,
-        reported_names: &HashMap<usize, Ident>,
+        reported_names: &NameTable,
         names: &mut NameReg,
         erows: UnifEnumRows,
     ) -> EnumRows {
         let erows = erows.into_root(table);
 
         match erows {
-            UnifEnumRows::UnifVar(var_id) => {
-                EnumRows(EnumRowsF::TailVar(var_name(reported_names, names, var_id)))
-            }
-            UnifEnumRows::Constant(c) => {
-                EnumRows(EnumRowsF::TailVar(cst_name(reported_names, names, c)))
-            }
+            UnifEnumRows::UnifVar(var_id) => EnumRows(EnumRowsF::TailVar(var_name(
+                reported_names,
+                names,
+                var_id,
+                VarKind::EnumRows,
+            ))),
+            UnifEnumRows::Constant(c) => EnumRows(EnumRowsF::TailVar(cst_name(
+                reported_names,
+                names,
+                c,
+                VarKind::EnumRows,
+            ))),
             UnifEnumRows::Concrete(t) => {
                 let mapped =
                     t.map(|erows| Box::new(erows_to_type(table, reported_names, names, *erows)));
@@ -163,8 +178,18 @@ pub fn to_type(
     let ty = ty.into_root(table);
 
     match ty {
-        UnifType::UnifVar(p) => Types::from(TypeF::Var(var_name(reported_names, names, p))),
-        UnifType::Constant(c) => Types::from(TypeF::Var(cst_name(reported_names, names, c))),
+        UnifType::UnifVar(p) => Types::from(TypeF::Var(var_name(
+            reported_names,
+            names,
+            p,
+            VarKind::Type,
+        ))),
+        UnifType::Constant(c) => Types::from(TypeF::Var(cst_name(
+            reported_names,
+            names,
+            c,
+            VarKind::Type,
+        ))),
         UnifType::Concrete(t) => {
             let mapped = t.map_state(
                 |btyp, names| Box::new(to_type(table, reported_names, names, *btyp)),

src/types.rs

@@ -131,7 +131,7 @@ pub enum EnumRowsF<ERows> {
 /// write e.g. `forall a :: Type` or `forall a :: Rows`. But the kind of a variable is required for
 /// the typechecker. It is thus determined during parsing and stored as `VarKind` where type
 /// variables are introduced, that is, on forall quantifiers.
-#[derive(Copy, Clone, PartialEq, Eq, Debug)]
+#[derive(Copy, Clone, PartialEq, Eq, Debug, Hash)]
 pub enum VarKind {
     Type,
     EnumRows,

tests/integration/typecheck/fail/mismatch_enum_poly_nested.ncl

@@ -5,8 +5,8 @@
 # error = 'TypecheckError::TypeMismatch'
 #
 # [test.metadata.expectation]
-# expected = 'p'
-# found = "[| 'blo ; _a |]"
+# expected = 'a'
+# found = "[| 'blo ; _erows_a |]"
 let f : forall r. (forall p. [| 'blo, 'ble ; r |] -> [| 'bla, 'bli; p |]) =
   match { 'blo => 'bla, 'ble => 'bli, _ => 'blo } 
 in f 'bli

tests/integration/typecheck/fail/mismatch_enum_poly_row_var.ncl

@@ -5,7 +5,7 @@
 # error = 'TypecheckError::TypeMismatch'
 #
 # [test.metadata.expectation]
-# expected = 'r'
+# expected = 'a'
 # found = "[| 'bli |]"
 let f : forall r. [| 'blo, 'ble; r |] -> Number =
   match { 'blo => 1, 'ble => 2, 'bli => 3 }

tests/integration/typecheck/fail/mismatch_record_dyn_field.ncl

@@ -5,8 +5,8 @@
 # error = 'TypecheckError::TypeMismatch'
 #
 # [test.metadata.expectation]
-# expected = '{ bla: _a ; _a }'
-# found = '{ _ : _b }'
+# expected = '{ bla: _a ; _rrows_b }'
+# found = '{ _ : _c }'
 ({
   "%{if true then "foo" else "bar"}" = 2,
   "foo" = true,

tests/integration/typecheck/fail/mismatch_record_poly_field_misused.ncl

@@ -5,7 +5,7 @@
 # error = 'TypecheckError::TypeMismatch'
 #
 # [test.metadata.expectation]
-# expected = 'r'
+# expected = 'a'
 # found = 'Number'
 
 # TODO: the expected/found types above seem wrong here

tests/snapshot/inputs/errors/unification_variable_aliasing.ncl

@@ -0,0 +1,7 @@
+# capture = 'stderr'
+# command = []
+
+# Regression test for #1312
+let f : forall a. (forall r. { bla : Bool, blo : a, ble : a; r } -> a) = fun r => if r.bla then (r.blo + 1) else r.ble
+  in (f { bla = true, blo = 1, ble = 2, blip = 'blip } : Number)
+

tests/snapshot/snapshots/snapshot__error_stderr_unification_variable_aliasing.ncl.snap

@@ -0,0 +1,15 @@
+---
+source: tests/snapshot/main.rs
+expression: err
+---
+error: incompatible types
+  ┌─ [INPUTS_PATH]/errors/unification_variable_aliasing.ncl:5:98
+  │
+5 │ let f : forall a. (forall r. { bla : Bool, blo : a, ble : a; r } -> a) = fun r => if r.bla then (r.blo + 1) else r.ble
+  │                                                                                                  ^^^^^ this expression
+  │
+  = Expected an expression of type `a`
+  = Found an expression of type `Number`
+  = These types are not compatible
+
+