Apply freshening when checking instance members

This fixes the 228 test case by introducing a proper instantiation step
for rigid type variables from the instance head canonical. This creates
fresh rigid type variables with update depths, fixing issues with the
escape check in promote_type and subsequently, unification.

This also changes the representation of Bindings::implicit to be based
on Vec instead of HashMap. This enables trivial shadowing, ensuring that
implicit type variables are kept up to date after instantiation.

Author: purefunctor

compiler-core/checking2/src/source.rs

@@ -16,11 +16,10 @@ pub use type_items::check_type_items;
 
 use building_types::QueryResult;
 
-use crate::ExternalQueries;
 use crate::context::CheckContext;
 use crate::core::{Type, TypeId, normalise};
 use crate::state::CheckState;
-use crate::safe_loop;
+use crate::{ExternalQueries, safe_loop};
 
 fn is_binary_operator_type<Q>(
     state: &mut CheckState,

compiler-core/checking2/src/source/term_items.rs

@@ -217,8 +217,7 @@ where
                     item_id,
                     member,
                     (class_file, class_id),
-                    &instance.constraints,
-                    &instance.arguments,
+                    &instance,
                 )?;
             }
         }
@@ -233,8 +232,7 @@ fn check_instance_member_group<Q>(
     instance_item_id: TermItemId,
     member: &lowering::InstanceMemberGroup,
     (class_file, class_id): (FileId, TypeItemId),
-    instance_constraints: &[TypeId],
-    instance_arguments: &[TypeId],
+    instance: &toolkit::DecomposedInstance,
 ) -> QueryResult<()>
 where
     Q: ExternalQueries,
@@ -246,8 +244,7 @@ where
                 context,
                 member,
                 (class_file, class_id),
-                instance_constraints,
-                instance_arguments,
+                instance,
             )
         })
     })
@@ -258,93 +255,137 @@ fn check_instance_member_group_core<Q>(
     context: &CheckContext<Q>,
     member: &lowering::InstanceMemberGroup,
     (class_file, class_id): (FileId, TypeItemId),
-    instance_constraints: &[TypeId],
-    instance_arguments: &[TypeId],
+    instance: &toolkit::DecomposedInstance,
 ) -> QueryResult<()>
 where
     Q: ExternalQueries,
 {
-    for &constraint in instance_constraints {
-        state.push_given(constraint);
-    }
+    let FreshenedInstanceRigids {
+        constraints: instance_constraints,
+        arguments: instance_arguments,
+        substitution,
+    } = freshen_instance_rigids(state, context, instance)?;
+
+    state.with_implicit(context, &substitution, |state| {
+        for &constraint in &instance_constraints {
+            state.push_given(constraint);
+        }
 
-    let class_member_type = if let Some((member_file, member_id)) = member.resolution {
-        Some(toolkit::lookup_file_term(state, context, member_file, member_id)?)
-    } else {
-        None
-    };
+        let class_member_type = if let Some((member_file, member_id)) = member.resolution {
+            Some(toolkit::lookup_file_term(state, context, member_file, member_id)?)
+        } else {
+            None
+        };
 
-    let class_member_type = if let Some(class_member_type) = class_member_type {
-        specialise_class_member_type(
-            state,
-            context,
-            class_member_type,
-            (class_file, class_id),
-            instance_arguments,
-        )?
-    } else {
-        None
-    };
+        let class_member_type = if let Some(class_member_type) = class_member_type {
+            specialise_class_member_type(
+                state,
+                context,
+                class_member_type,
+                (class_file, class_id),
+                &instance_arguments,
+            )?
+        } else {
+            None
+        };
 
-    let residuals = if let Some(signature_id) = member.signature {
-        let (signature_member_type, _) =
-            types::check_kind(state, context, signature_id, context.prim.t)?;
-
-        if let Some(class_member_type) = class_member_type {
-            let unified =
-                unification::unify(state, context, signature_member_type, class_member_type)?;
-            if !unified {
-                let expected = state.pretty_id(context, class_member_type)?;
-                let actual = state.pretty_id(context, signature_member_type)?;
-                state.insert_error(ErrorKind::InstanceMemberTypeMismatch { expected, actual });
+        let residuals = if let Some(signature_id) = member.signature {
+            let (signature_member_type, _) =
+                types::check_kind(state, context, signature_id, context.prim.t)?;
+
+            if let Some(class_member_type) = class_member_type {
+                let unified =
+                    unification::unify(state, context, signature_member_type, class_member_type)?;
+                if !unified {
+                    let expected = state.pretty_id(context, class_member_type)?;
+                    let actual = state.pretty_id(context, signature_member_type)?;
+                    state.insert_error(ErrorKind::InstanceMemberTypeMismatch { expected, actual });
+                }
             }
+
+            let equation_set = equations::analyse_equation_set(
+                state,
+                context,
+                equations::EquationMode::Check {
+                    origin: equations::EquationTypeOrigin::Explicit(signature_id),
+                    expected_type: signature_member_type,
+                },
+                &member.equations,
+            )?;
+            let exhaustiveness = equations::compute_equation_exhaustiveness(
+                state,
+                context,
+                &equation_set,
+                &member.equations,
+            )?;
+            state.report_exhaustiveness(context, exhaustiveness);
+            state.solve_constraints(context)?
+        } else if let Some(specialised_type) = class_member_type {
+            let equation_set = equations::analyse_equation_set(
+                state,
+                context,
+                equations::EquationMode::Check {
+                    origin: equations::EquationTypeOrigin::Implicit,
+                    expected_type: specialised_type,
+                },
+                &member.equations,
+            )?;
+            let exhaustiveness = equations::compute_equation_exhaustiveness(
+                state,
+                context,
+                &equation_set,
+                &member.equations,
+            )?;
+            state.report_exhaustiveness(context, exhaustiveness);
+            state.solve_constraints(context)?
+        } else {
+            vec![]
+        };
+
+        for residual in residuals {
+            let constraint = state.pretty_id(context, residual)?;
+            state.insert_error(ErrorKind::NoInstanceFound { constraint });
         }
 
-        let equation_set = equations::analyse_equation_set(
-            state,
-            context,
-            equations::EquationMode::Check {
-                origin: equations::EquationTypeOrigin::Explicit(signature_id),
-                expected_type: signature_member_type,
-            },
-            &member.equations,
-        )?;
-        let exhaustiveness = equations::compute_equation_exhaustiveness(
-            state,
-            context,
-            &equation_set,
-            &member.equations,
-        )?;
-        state.report_exhaustiveness(context, exhaustiveness);
-        state.solve_constraints(context)?
-    } else if let Some(specialised_type) = class_member_type {
-        let equation_set = equations::analyse_equation_set(
-            state,
-            context,
-            equations::EquationMode::Check {
-                origin: equations::EquationTypeOrigin::Implicit,
-                expected_type: specialised_type,
-            },
-            &member.equations,
-        )?;
-        let exhaustiveness = equations::compute_equation_exhaustiveness(
-            state,
-            context,
-            &equation_set,
-            &member.equations,
-        )?;
-        state.report_exhaustiveness(context, exhaustiveness);
-        state.solve_constraints(context)?
-    } else {
-        vec![]
-    };
+        Ok(())
+    })
+}
+
+struct FreshenedInstanceRigids {
+    constraints: Vec<TypeId>,
+    arguments: Vec<TypeId>,
+    substitution: NameToType,
+}
+
+fn freshen_instance_rigids<Q>(
+    state: &mut CheckState,
+    context: &CheckContext<Q>,
+    instance: &toolkit::DecomposedInstance,
+) -> QueryResult<FreshenedInstanceRigids>
+where
+    Q: ExternalQueries,
+{
+    let mut substitution = NameToType::default();
 
-    for residual in residuals {
-        let constraint = state.pretty_id(context, residual)?;
-        state.insert_error(ErrorKind::NoInstanceFound { constraint });
+    for binder in &instance.binders {
+        let kind = SubstituteName::many(state, context, &substitution, binder.kind)?;
+        let rigid = state.fresh_rigid(context.queries, kind);
+        substitution.insert(binder.name, rigid);
     }
 
-    Ok(())
+    let constraints = instance
+        .constraints
+        .iter()
+        .map(|&constraint| SubstituteName::many(state, context, &substitution, constraint))
+        .collect::<QueryResult<Vec<_>>>()?;
+
+    let arguments = instance
+        .arguments
+        .iter()
+        .map(|&argument| SubstituteName::many(state, context, &substitution, argument))
+        .collect::<QueryResult<Vec<_>>>()?;
+
+    Ok(FreshenedInstanceRigids { constraints, arguments, substitution })
 }
 
 fn specialise_class_member_type<Q>(

compiler-core/checking2/src/state.rs

@@ -11,6 +11,7 @@ use crate::context::CheckContext;
 use crate::core::exhaustive::{
     ExhaustivenessReport, Pattern, PatternConstructor, PatternId, PatternInterner, PatternKind,
 };
+use crate::core::substitute::{NameToType, SubstituteName};
 use crate::core::{Depth, Name, SmolStrId, Type, TypeId, constraint, pretty, zonk};
 use crate::error::{CheckError, ErrorCrumb, ErrorKind};
 use crate::implication::Implications;
@@ -84,18 +85,25 @@ impl Unifications {
 /// Tracks type variable bindings during kind inference.
 #[derive(Default)]
 pub struct Bindings {
-    forall_bindings: FxHashMap<lowering::TypeVariableBindingId, (Name, TypeId)>,
-    implicit_bindings:
-        FxHashMap<(lowering::GraphNodeId, lowering::ImplicitBindingId), (Name, TypeId)>,
+    forall: FxHashMap<lowering::TypeVariableBindingId, (Name, TypeId)>,
+    implicit: Vec<ImplicitBinding>,
+}
+
+#[derive(Debug, Clone, Copy, PartialEq, Eq)]
+struct ImplicitBinding {
+    node: lowering::GraphNodeId,
+    id: lowering::ImplicitBindingId,
+    name: Name,
+    kind: TypeId,
 }
 
 impl Bindings {
     pub fn bind_forall(&mut self, id: lowering::TypeVariableBindingId, name: Name, kind: TypeId) {
-        self.forall_bindings.insert(id, (name, kind));
+        self.forall.insert(id, (name, kind));
     }
 
     pub fn lookup_forall(&self, id: lowering::TypeVariableBindingId) -> Option<(Name, TypeId)> {
-        self.forall_bindings.get(&id).copied()
+        self.forall.get(&id).copied()
     }
 
     pub fn bind_implicit(
@@ -105,15 +113,44 @@ impl Bindings {
         name: Name,
         kind: TypeId,
     ) {
-        self.implicit_bindings.insert((node, id), (name, kind));
+        self.implicit.push(ImplicitBinding { node, id, name, kind });
+    }
+
+    fn bind_implicit_substitution<Q>(
+        state: &mut CheckState,
+        context: &CheckContext<Q>,
+        substitution: &NameToType,
+    ) -> QueryResult<()>
+    where
+        Q: ExternalQueries,
+    {
+        let scope = state.bindings.implicit.len();
+
+        for binding in 0..scope {
+            let ImplicitBinding { node, id, name, kind } = state.bindings.implicit[binding];
+            let Some(&replacement) = substitution.get(&name) else { continue };
+
+            let Type::Rigid(name, _, _) = context.lookup_type(replacement) else {
+                unreachable!("invariant violated: expected a rigid variable");
+            };
+
+            let kind = SubstituteName::many(state, context, substitution, kind)?;
+            state.bindings.implicit.push(ImplicitBinding { node, id, name, kind });
+        }
+
+        Ok(())
     }
 
     pub fn lookup_implicit(
         &self,
         node: lowering::GraphNodeId,
         id: lowering::ImplicitBindingId,
     ) -> Option<(Name, TypeId)> {
-        self.implicit_bindings.get(&(node, id)).copied()
+        self.implicit
+            .iter()
+            .rev()
+            .find(|binding| binding.node == node && binding.id == id)
+            .map(|binding| (binding.name, binding.kind))
     }
 }
 
@@ -199,6 +236,23 @@ impl CheckState {
         result
     }
 
+    pub fn with_implicit<Q, T>(
+        &mut self,
+        context: &CheckContext<Q>,
+        substitution: &NameToType,
+        f: impl FnOnce(&mut CheckState) -> QueryResult<T>,
+    ) -> QueryResult<T>
+    where
+        Q: ExternalQueries,
+    {
+        let scope = self.bindings.implicit.len();
+        Bindings::bind_implicit_substitution(self, context, substitution)?;
+        let result = f(self);
+        self.bindings.implicit.truncate(scope);
+
+        result
+    }
+
     pub fn solve_constraints<Q>(&mut self, context: &CheckContext<Q>) -> QueryResult<Vec<TypeId>>
     where
         Q: ExternalQueries,