Initial instance member checking

This also implements several subsystems required to get instance member
checking working, including but not limited to:

- Specialising class members based on instance arguments
- Capturing and rebinding implicit instance variables
- Constraints added to class members, not the instance head
- Errors for mismatched instance heads and member types
- Tracking both explicit and quantified variables for class kinds

Author: purefunctor

compiler-core/checking/src/algorithm.rs

@@ -52,6 +52,7 @@ use std::slice;
 
 use building_types::QueryResult;
 use files::FileId;
+use indexing::TermItemKind;
 use itertools::Itertools;
 use lowering::{DataIr, NewtypeIr, Scc, TermItemIr, TypeItemIr};
 
@@ -66,8 +67,9 @@ pub fn check_source(queries: &impl ExternalQueries, file_id: FileId) -> QueryRes
     check_type_items(&mut state, &context)?;
 
     check_term_signatures(&mut state, &context)?;
-    check_instances(&mut state, &context)?;
+    check_instance_heads(&mut state, &context)?;
     check_value_groups(&mut state, &context)?;
+    check_instance_members(&mut state, &context)?;
 
     Ok(state.checked)
 }
@@ -267,7 +269,7 @@ where
     Ok(())
 }
 
-fn check_instances<Q>(
+fn check_instance_heads<Q>(
     state: &mut state::CheckState,
     context: &state::CheckContext<Q>,
 ) -> QueryResult<()>
@@ -295,6 +297,55 @@ where
     Ok(())
 }
 
+fn check_instance_members<Q>(
+    state: &mut state::CheckState,
+    context: &state::CheckContext<Q>,
+) -> QueryResult<()>
+where
+    Q: ExternalQueries,
+{
+    let items = context.lowered.term_scc.iter().flat_map(|scc| match scc {
+        Scc::Base(item) | Scc::Recursive(item) => slice::from_ref(item),
+        Scc::Mutual(items) => items.as_slice(),
+    });
+
+    for &item_id in items {
+        let Some(TermItemIr::Instance { members, resolution, .. }) =
+            context.lowered.info.get_term_item(item_id)
+        else {
+            continue;
+        };
+
+        let Some((class_file, class_id)) = *resolution else {
+            continue;
+        };
+
+        let TermItemKind::Instance { id: instance_id } = context.indexed.items[item_id].kind else {
+            continue;
+        };
+
+        let Some(instance) = state.checked.instances.get(&instance_id) else {
+            continue;
+        };
+
+        let instance_arguments = instance.arguments.clone();
+        let instance_constraints = instance.constraints.clone();
+
+        let check_members = term_item::CheckInstanceMembers {
+            instance_id: item_id,
+            members,
+            class_file,
+            class_id,
+            instance_arguments: &instance_arguments,
+            instance_constraints: &instance_constraints,
+        };
+
+        term_item::check_instance_members(state, context, check_members)?;
+    }
+
+    Ok(())
+}
+
 fn check_value_groups<Q>(
     state: &mut state::CheckState,
     context: &state::CheckContext<Q>,

compiler-core/checking/src/algorithm/constraint.rs

@@ -21,7 +21,7 @@ use crate::algorithm::fold::{FoldAction, TypeFold, fold_type};
 use crate::algorithm::state::{CheckContext, CheckState};
 use crate::algorithm::{transfer, unification};
 use crate::core::{Class, Instance, Variable, debruijn};
-use crate::{ExternalQueries, Type, TypeId};
+use crate::{CheckedModule, ExternalQueries, Type, TypeId};
 
 pub fn solve_constraints<Q>(
     state: &mut CheckState,
@@ -197,22 +197,23 @@ where
             return Ok(());
         }
 
-        let Some(class_info) = get_class_info(state, context, file_id, item_id)? else {
+        let Some(class_info) = lookup_file_class(state, context, file_id, item_id)? else {
             return Ok(());
         };
 
         if class_info.superclasses.is_empty() {
             return Ok(());
         }
 
+        let initial_level = class_info.quantified_variables.0 + class_info.kind_variables.0;
         let mut bindings = FxHashMap::default();
-        for (&level, &argument) in class_info.variable_levels.iter().zip(&arguments) {
+        for (index, &argument) in arguments.iter().enumerate() {
+            let level = debruijn::Level(initial_level + index as u32);
             bindings.insert(level, argument);
         }
 
-        for &(superclass, _) in &class_info.superclasses {
-            let localized = transfer::localize(state, context, superclass);
-            let substituted = ApplyBindings::on(state, &bindings, localized);
+        for &(superclass, _) in class_info.superclasses.iter() {
+            let substituted = ApplyBindings::on(state, &bindings, superclass);
             constraints.push(substituted);
             aux(state, context, substituted, constraints, seen)?;
         }
@@ -237,15 +238,15 @@ where
         state
             .checked
             .instances
-            .iter()
+            .values()
             .filter(|instance| instance.resolution.1 == item_id)
             .cloned()
             .collect_vec()
     } else {
         let checked = context.queries.checked(file_id)?;
         checked
             .instances
-            .iter()
+            .values()
             .filter(|instance| instance.resolution.1 == item_id)
             .cloned()
             .collect_vec()
@@ -264,8 +265,53 @@ where
     Ok(result)
 }
 
-pub(crate) fn get_class_info<Q>(
-    state: &CheckState,
+fn localize_class<Q>(state: &mut CheckState, context: &CheckContext<Q>, class: &Class) -> Class
+where
+    Q: ExternalQueries,
+{
+    let superclasses = class.superclasses.iter().map(|&(t, k)| {
+        let t = transfer::localize(state, context, t);
+        let k = transfer::localize(state, context, k);
+        (t, k)
+    });
+    Class {
+        superclasses: superclasses.collect(),
+        quantified_variables: class.quantified_variables,
+        kind_variables: class.kind_variables,
+    }
+}
+
+fn lookup_local_class<Q>(
+    state: &mut CheckState,
+    context: &CheckContext<Q>,
+    item_id: TypeItemId,
+) -> Option<Class>
+where
+    Q: ExternalQueries,
+{
+    if let Some(class) = state.binding_group.lookup_class(item_id) {
+        Some(class)
+    } else {
+        let class = state.checked.lookup_class(item_id)?;
+        Some(localize_class(state, context, &class))
+    }
+}
+
+fn lookup_global_class<Q>(
+    state: &mut CheckState,
+    context: &CheckContext<Q>,
+    checked: &CheckedModule,
+    item_id: TypeItemId,
+) -> Option<Class>
+where
+    Q: ExternalQueries,
+{
+    let class = checked.classes.get(&item_id)?;
+    Some(localize_class(state, context, class))
+}
+
+pub(crate) fn lookup_file_class<Q>(
+    state: &mut CheckState,
     context: &CheckContext<Q>,
     file_id: FileId,
     item_id: TypeItemId,
@@ -274,10 +320,10 @@ where
     Q: ExternalQueries,
 {
     if file_id == context.id {
-        Ok(state.checked.classes.get(&item_id).cloned())
+        Ok(lookup_local_class(state, context, item_id))
     } else {
         let checked = context.queries.checked(file_id)?;
-        Ok(checked.classes.get(&item_id).cloned())
+        Ok(lookup_global_class(state, context, &checked, item_id))
     }
 }
 

compiler-core/checking/src/algorithm/state.rs

@@ -17,7 +17,7 @@ use rustc_hash::FxHashMap;
 use sugar::{Bracketed, Sectioned};
 
 use crate::algorithm::{constraint, quantify, transfer};
-use crate::core::{ForallBinder, Synonym, Type, TypeId, TypeInterner, debruijn};
+use crate::core::{Class, ForallBinder, Synonym, Type, TypeId, TypeInterner, debruijn};
 use crate::error::{CheckError, ErrorKind, ErrorStep};
 use crate::{CheckedModule, ExternalQueries};
 
@@ -79,6 +79,26 @@ impl TypeScope {
         self.kinds.unbind(level);
     }
 
+    /// Unbinds variables starting from a level and returns captured implicit bindings.
+    ///
+    /// This is used when checking instances to capture the implicit type variables
+    /// from the instance head before unbinding, so they can be rebound when checking
+    /// instance members.
+    pub fn unbind_implicits(&mut self, level: debruijn::Level) -> Vec<InstanceHeadBinding> {
+        let mut implicits = vec![];
+
+        for (level, variable) in self.bound.iter_from(level) {
+            if let debruijn::Variable::Implicit { node, id } = variable
+                && let Some(&kind) = self.kinds.get(level)
+            {
+                implicits.push(InstanceHeadBinding { node, id, kind });
+            }
+        }
+
+        self.unbind(level);
+        implicits
+    }
+
     pub fn size(&self) -> debruijn::Size {
         self.bound.size()
     }
@@ -127,6 +147,17 @@ impl TermScope {
     }
 }
 
+/// A single implicit variable captured from an instance head.
+///
+/// Instance heads like `instance Show a => Show (Array a)` introduce
+/// implicit type variables that need to be visible when checking instance
+/// member implementations.
+pub struct InstanceHeadBinding {
+    pub node: GraphNodeId,
+    pub id: ImplicitBindingId,
+    pub kind: TypeId,
+}
+
 /// Tracks type variables declared in surface syntax.
 ///
 /// The type checker checks kind/type declarations first before equation
@@ -158,6 +189,7 @@ pub struct SurfaceBindings {
     pub term_item: FxHashMap<TermItemId, Arc<[TypeVariableBindingId]>>,
     pub type_item: FxHashMap<TypeItemId, Arc<[TypeVariableBindingId]>>,
     pub let_binding: FxHashMap<LetBindingNameGroupId, Arc<[TypeVariableBindingId]>>,
+    pub instance_head: FxHashMap<TermItemId, Arc<[InstanceHeadBinding]>>,
 }
 
 impl SurfaceBindings {
@@ -184,6 +216,14 @@ impl SurfaceBindings {
     pub fn get_let(&self, id: LetBindingNameGroupId) -> Option<Arc<[TypeVariableBindingId]>> {
         self.let_binding.get(&id).cloned()
     }
+
+    pub fn insert_instance_head(&mut self, id: TermItemId, v: Arc<[InstanceHeadBinding]>) {
+        self.instance_head.insert(id, v);
+    }
+
+    pub fn get_instance_head(&self, id: TermItemId) -> Option<Arc<[InstanceHeadBinding]>> {
+        self.instance_head.get(&id).cloned()
+    }
 }
 
 /// Collects wanted and given constraints.
@@ -262,6 +302,7 @@ pub struct BindingGroupContext {
     pub terms: FxHashMap<TermItemId, TypeId>,
     pub types: FxHashMap<TypeItemId, TypeId>,
     pub synonyms: FxHashMap<TypeItemId, Synonym>,
+    pub classes: FxHashMap<TypeItemId, Class>,
     pub residual: FxHashMap<TermItemId, Vec<TypeId>>,
     pub data: FxHashMap<TypeItemId, CheckedDataLike>,
 }
@@ -278,6 +319,10 @@ impl BindingGroupContext {
     pub fn lookup_synonym(&self, id: TypeItemId) -> Option<Synonym> {
         self.synonyms.get(&id).copied()
     }
+
+    pub fn lookup_class(&self, id: TypeItemId) -> Option<Class> {
+        self.classes.get(&id).cloned()
+    }
 }
 
 /// The core environment structure threaded through the [`algorithm`].
@@ -622,9 +667,14 @@ impl CheckState {
             }
         }
 
+        let mut classes = mem::take(&mut self.binding_group.classes);
         for (item_id, type_id) in mem::take(&mut self.binding_group.types) {
-            if let Some((type_id, _)) = quantify::quantify(self, type_id) {
-                let type_id = transfer::globalize(self, context, type_id);
+            if let Some((quantified_type, quantified_count)) = quantify::quantify(self, type_id) {
+                if let Some(mut class) = classes.remove(&item_id) {
+                    class.quantified_variables = quantified_count;
+                    self.checked.classes.insert(item_id, class);
+                }
+                let type_id = transfer::globalize(self, context, quantified_type);
                 self.checked.types.insert(item_id, type_id);
             }
         }

compiler-core/checking/src/algorithm/term.rs

@@ -31,7 +31,7 @@ where
     Ok(())
 }
 
-fn infer_equations_core<Q>(
+pub fn infer_equations_core<Q>(
     state: &mut CheckState,
     context: &CheckContext<Q>,
     group_type: TypeId,