From 004de7ba334aeb7e665e4e4b45c9cc852c7812ce Mon Sep 17 00:00:00 2001 From: biu Date: Sun, 18 Oct 2026 03:58:00 +0800 Subject: [PATCH 1/8] Check instance heads whose class another module declares An instance head is checked against its class's checked kind scheme no matter which module declares the class: a program-level run sees every module's scheme and a module-level run receives the imported ones, so the head its module applies is checked there rather than only in the declaring module's own run, which is the recorded FE-11 gap. The arity the rule leaves to the class environment is read from the declaration at home and from the scheme abroad: the scheme's kind is one arrow per parameter ending in Constraint, and a scheme this run does not know leaves its head unguarded rather than inventing an arity for it. Failing/FoldableInstance1/2/3 and failing/NewtypeInstance6 apply classes their modules import to arguments of the wrong kind, so they now report KindsDoNotUnify at the head; the l3 kinds scoreboard moves from 39/48 to 43/48, with KindsDoNotUnify 16/24 to 20/24 and nothing else moving. Docs: frontend/type-system/kinds.md records the rule and the boundary that remains - a scheme whose kind variables the run has not quantified yet binds its first instance, which is the polykind-generalization machinery #100/#123 own. --- crates/psrs-kind/src/check/infer/mod.rs | 45 ++++++++++-- crates/psrs-kind/src/tests/instances.rs | 84 +++++++++++++++++++++++ docs/design/frontend/type-system/kinds.md | 54 ++++++++++----- 3 files changed, 158 insertions(+), 25 deletions(-) diff --git a/crates/psrs-kind/src/check/infer/mod.rs b/crates/psrs-kind/src/check/infer/mod.rs index 9b4770fb..7693e76a 100644 --- a/crates/psrs-kind/src/check/infer/mod.rs +++ b/crates/psrs-kind/src/check/infer/mod.rs @@ -228,23 +228,37 @@ impl Checker<'_> { /// kind and therefore cannot reject a head. Without this an instance is the /// one place a type is applied to a kind signature and never checked, so /// `class C :: Constraint -> Constraint` accepts `instance C Int`. + /// + /// The class does not have to be declared in the module that declares the + /// instance: a head whose class is foreign is still checked here against the + /// scheme its declaring module's run produced, because a program-level run + /// sees every module's scheme and a module-level run receives the imported + /// ones. What does not need to be the same is the arity source. A class this + /// module declares has its parameter list at hand; a foreign class is read + /// through its scheme (its kind is one arrow per parameter ending in + /// `Constraint`), and a scheme this run does not know leaves the head + /// unguarded, because a signature the program never checked must not be + /// replaced by an invention. fn check_instance_heads(&mut self, module: &hir::Module) { for instance in &module.instances { // A head that applies its class to the wrong number of arguments is // an arity error, not a kind error, and the class environment owns // that rule. Checking it here too would report `KindsDoNotUnify` // where `ClassInstanceArityMismatch` is the official code, and would - // pre-empt the arity diagnostic entirely. A class this module does - // not declare has no known arity here either, so it is left alone. - let Some(declared) = module + // pre-empt the arity diagnostic entirely. + let declared = module .types .iter() - .find(|declaration| declaration.id == instance.class_id) - else { - continue; + .find(|declaration| declaration.id == instance.class_id); + let parameters = match declared { + Some(declaration) => Some(declaration.parameters.len()), + None => self.scheme_parameter_count(instance.class_id), }; let (_, arguments) = flatten_spine(&instance.head); - if arguments.len() != declared.parameters.len() { + let Some(parameters) = parameters else { + continue; + }; + if arguments.len() != parameters { continue; } let mut scope = HashMap::new(); @@ -252,6 +266,23 @@ impl Checker<'_> { self.unify(kind, constraint_kind(), instance.head.span); } } + + /// How many parameters a class's checked kind scheme takes. + /// + /// The scheme's kind is one function per parameter ending in `Constraint`, + /// so the count is the chain of function steps. `None` says this run has no + /// scheme for the class — a program this run is not closed over — and the + /// head is then left to whatever the scheme's absence reports elsewhere. + fn scheme_parameter_count(&self, id: TypeId) -> Option { + let scheme = self.schemes.get(&id)?; + let mut count = 0; + let mut kind = &scheme.kind; + while let Kind::Function(_, result) = kind { + count += 1; + kind = result; + } + Some(count) + } } fn collect_kind_variables(kind: &Kind, out: &mut Vec) { diff --git a/crates/psrs-kind/src/tests/instances.rs b/crates/psrs-kind/src/tests/instances.rs index 224a1a04..a5772ce9 100644 --- a/crates/psrs-kind/src/tests/instances.rs +++ b/crates/psrs-kind/src/tests/instances.rs @@ -85,3 +85,87 @@ fn leaves_an_instance_head_with_the_wrong_arity_to_the_arity_rule() { instance tooNarrow :: TooNarrow Int\n", ); } + +#[test] +fn checks_an_instance_head_whose_class_is_declared_in_another_module() { + // `failing/FoldableInstance1.purs`: `Foldable :: (Type -> Type) -> + // Constraint` is declared in `Data.Foldable`, and the instance is in + // `Main`, so only the instance's own module sees `Foldable`'s checked + // scheme. `Foo` has kind `Type` and the head applies the class to it + // directly, so the head is refused. + let modules = resolve_program(&[ + ( + "Main.purs", + "module Main where\n\ + import Data.Foldable\n\ + data Foo = Bar\n\ + instance foldableFoo :: Foldable Foo\n", + ), + ( + "Data.Foldable.purs", + "module Data.Foldable where\n\ + class Foldable :: (Type -> Type) -> Constraint\n\ + class Foldable f where\n foldr :: forall a b. (a -> b) -> b -> f a -> b\n", + ), + ]); + let errors = check_modules(&modules); + assert!(codes(&errors).contains(&"KindsDoNotUnify"), "{errors:?}"); + // The head that applies the class is `Main`'s syntax, so the diagnostic is + // attributed to the module that declares the instance, not to the module + // whose scheme was consulted. + let error = errors + .iter() + .find(|error| error.code == "KindsDoNotUnify") + .expect("a kind conflict"); + assert_eq!(error.origin, ModuleId(0), "{errors:?}"); +} + +#[test] +fn accepts_two_instance_heads_whose_class_is_declared_in_another_module() { + // A cross-module class is checked against the scheme its declaring module + // checked, at every use instantiating that scheme, so two heads at + // different eligible kinds are both accepted — one head must not fix the + // kind another is judged by. + check_modules_ok(&[ + ( + "Main.purs", + "module Main where\n\ + import Data.Proxy\n\ + instance int :: M Int\n\ + instance label :: M \"hello\"\n", + ), + ( + "Data.Proxy.purs", + "module Data.Proxy where\n\ + class M :: forall k. k -> Constraint\n\ + class M a\n", + ), + ]); +} + +#[test] +fn leaves_a_cross_module_head_with_the_wrong_arity_to_the_arity_rule() { + // The arity rule reads a foreign class through its checked kind scheme, so + // a head that applies a two-parameter class to one argument is still an + // arity error, not a kind error. + check_modules_ok(&[ + ( + "Main.purs", + "module Main where\n\ + import Data.Proxy\n\ + instance tooNarrow :: M Int\n", + ), + ( + "Data.Proxy.purs", + "module Data.Proxy where\n\ + class M a b\n", + ), + ]); +} + +/// Kind checks a resolved multi-module program and requires no diagnostics. +pub(super) fn check_modules_ok(sources: &[(&str, &str)]) { + let modules = resolve_program(sources); + let errors = check_modules(&modules); + assert!(errors.is_empty(), "unexpected kind errors: {errors:?}"); +} diff --git a/docs/design/frontend/type-system/kinds.md b/docs/design/frontend/type-system/kinds.md index d1ef957c..a1597d7b 100644 --- a/docs/design/frontend/type-system/kinds.md +++ b/docs/design/frontend/type-system/kinds.md @@ -64,17 +64,25 @@ Absence of kind metadata is an error, not freedom. A referenced declaration with Every type unknown carries a kind, and binding one maintains it. Kind inference has a single substitution over kinds, one occurs check, and one escape rule, and `bind_type_variable` runs the kind compatibility check for both sides of a binding in addition to the occurs, level, and skolem-escape rules. A record's row has kind `Row Type`, a row-polymorphic variable has kind `Row k` with `k` tracked alongside it, and a `forall` binder's kind annotation is checked against the kind recorded for that variable. Coercion checking therefore adds no kind machinery of its own: it consults this solver, and a binding that would violate a kind invariant is a kind diagnostic rather than a silently accepted type. -An instance head is checked against its class's kind scheme. That is the only -place a standalone kind signature on a class is enforced: a class without one is -inferred as its parameters at `Type` returning `Constraint`, which accepts any -argument kind, so `class C :: Constraint -> Constraint` would otherwise accept -`instance C Int`. Each head argument is elaborated against the parameter kind its -class declares rather than read on its own, which is what makes `((->) r)` a -higher-kinded class parameter in `Functor ((->) r)` rather than the partially -applied function synonym it is elsewhere. A head that applies its class to the -wrong number of arguments is an arity error owned by the class environment, so -the kind check leaves it alone rather than reporting `KindsDoNotUnify` where -`ClassInstanceArityMismatch` is the official code. +An instance head is checked against its class's kind scheme, including a head +whose class another module declares: the scheme is what the declaring module's +run published and what the checking run receives, and a foreign class is read +through the same scheme its argument kinds are checked against. The arity the +rule leaves alone is accordingly read from the declaration itself at home and +from the scheme abroad — one arrow per parameter, ending in `Constraint` — the +two readings describing the same class; a scheme that is not part of this run +leaves its head unguarded rather than inventing an arity for it. A standalone +kind signature on a class is the only way to state its parameter kinds: a class +without one is inferred as its parameters at `Type` returning `Constraint`, +which accepts any argument kind and cannot reject a head, so +`class C :: Constraint -> Constraint` would otherwise accept `instance C Int`. +Each head argument is elaborated against the parameter kind its class declares +rather than read on its own, which is what makes `((->) r)` a higher-kinded +class parameter in `Functor ((->) r)` rather than the partially applied +function synonym it is elsewhere, and a head that applies its class to the +wrong number of arguments is an arity error owned by the class environment, +so the kind check leaves it alone rather than reporting `KindsDoNotUnify` +where `ClassInstanceArityMismatch` is the official code. Reject cyclic synonyms and unsaturated synonym use that remains after capture-avoiding substitution of saturated outer aliases. A partially supplied @@ -207,10 +215,12 @@ inference solves a kind equation. The kind state is a single `psrs_kind::KindSta `InferState` beside the type substitutions, with the recorded kind of each inference type variable in `variable_kinds` next to it, so `speculate` rolls a kind binding back with the type binding that produced it. The coercion module's private denotation, -primitive table, substitution, and unifier are gone; `coercion_kinds_compatible` now -reads both kinds through `kind_of_type` and solves the equation speculatively, so a -conversion that turns out not to hold leaves no kind binding behind. `bind_variable` -runs the kind check alongside the occurs, escape, and level rules, and a row tail +primitive table, substitution, and unifier are gone; `coercion_kinds_trial` reads both kinds +through `kind_of_type` and each pair's kind equation is solved speculatively by +the `Coercible` rule, which re-reports a `KindsDoNotUnify` verdict where official +solving raises it — when the rule picks a constraint up, including a pair its +role decomposition dissolves into — so the proof that turns out not to hold +leaves no kind binding behind. `bind_variable` runs the kind check alongside the occurs, escape, and level rules, and a row tail solved during row unification keeps the kind its row admits through that same binding. @@ -223,9 +233,17 @@ What remains, and what the next wave owns: an implicitly generalized kind mentions a type variable that is not quantified explicitly. Kind variables and type-level `forall` binders live in different state here, so the dependency order the official check needs is not recorded yet. -- An instance head whose class is declared in another module is still skipped: the - arity rule needs the class declaration, and a class the checking module does not - declare has no arity here. Only the declaring module's own run checks such a head. +- Cross-module instance heads agree now: a head is checked against its class's + checked kind scheme whether the class is declared in the checking module or + imported, with the arity read from the scheme for a foreign class. What still + generalizes nothing is a scheme whose variables the run's own checks have not + quantified yet: within one run the scheme of a class whose definition leaves a + parameter's kind undetermined is monomorphic, so two instance heads at + different eligible kinds disagree with each other's fixings. Publishing needs + the declaration check to finish before the scheme is fixed, which is the + polykind-generalization machinery #100/#123 own — the same boundary + `failing/PolykindInstantiatedInstance.purs` and + `failing/PolykindGeneralizationLet.purs` remain open at. - `data Wrap :: Lib.Box Type -> Type` reads `Lib.Box Type` as the kind "`Lib.Box` applied to `Type`", because a kind annotation is read as a kind rather than elaborated as a type. Official `elaborateKind` eliminates an application of an arrow From 4a078b958907feb818920e52ce856910f2d8584e Mon Sep 17 00:00:00 2001 From: biu Date: Sun, 18 Oct 2026 04:08:35 +0800 Subject: [PATCH 2/8] Report determined instance heads, superclass cycles, and recursive instances officially The common instance recorder now applies one determined-instance-head rule to every local instance: each elaborated head argument must be a type variable, a type-level literal, a type constructor, or an application over those, and a row argument is legal only where a functional dependency fully determines its position. The fully determined positions are official typeClassDeterminedArguments, ported from Environment.hs's computeCoveringSets (the arguments standing in no inclusion-minimal covering set), so a parameter determined by nothing it cannot itself determine is not, and official record helpers that put a closed record in a determined parameter keep compiling. InvalidInstanceHead is raised where purs raises it, before the instance is recorded, covering TypeWildcards3, TypeSynonyms7, 3510, InvalidDerivedInstance2, and RowInInstanceNotDetermined0/1/2 with no overlap or deriving diagnostic alongside. Superclass cycles raise CycleInTypeClassDeclaration at the class declaration that reintroduces an ancestor, replacing the unmapped UnsupportedClass report (Superclasses2, SelfCycleInTypeClassDeclaration). An instance search that exhausts its depth bound now reports PossiblyInfiniteInstance at the constraint that would be solved again, the official Entailment work bound, instead of failing silently into an enclosing NoInstanceFound (438); the code joins the constraint-failure codes so no enclosing boundary reports the obligation twice. M5 agreement measured with the annotations oracle: 81/97 to 90/99, with InvalidInstanceHead 7/7, PossiblyInfiniteInstance 1/1, and CycleInTypeClassDeclaration 2/2, while OverlappingInstances stays 8/8, NoInstanceFound 52/53, and the L2/L3/L4 boards unchanged. --- .../src/tests/typecheck/instance_heads.rs | 178 +++++++++++++++++ crates/psrs-driver/src/tests/typecheck/mod.rs | 1 + .../classes/environment/instance_head.rs | 186 ++++++++++++++++++ .../src/typecheck/classes/environment/mod.rs | 11 +- .../src/typecheck/classes/solve/search.rs | 12 ++ crates/psrs-typecheck/src/typecheck/error.rs | 14 ++ .../type-system/classes-and-evidence.md | 28 +++ 7 files changed, 429 insertions(+), 1 deletion(-) create mode 100644 crates/psrs-driver/src/tests/typecheck/instance_heads.rs create mode 100644 crates/psrs-typecheck/src/typecheck/classes/environment/instance_head.rs diff --git a/crates/psrs-driver/src/tests/typecheck/instance_heads.rs b/crates/psrs-driver/src/tests/typecheck/instance_heads.rs new file mode 100644 index 00000000..56cbd3e5 --- /dev/null +++ b/crates/psrs-driver/src/tests/typecheck/instance_heads.rs @@ -0,0 +1,178 @@ +//! The determined-instance-head rule, the superclass-cycle class declaration +//! check, and the recursive-instance depth bound, each under its official +//! `errorCode`. These are the structural checks the corpus cases +//! `RowInInstanceNotDetermined*`, `TypeSynonyms7`, `3510`, +//! `InvalidDerivedInstance2`, `438`, `Superclasses2`, and +//! `SelfCycleInTypeClassDeclaration` exercise. + +use super::*; + +/// The program's errors carry exactly the one official code named. +fn assert_one_code(name: &str, expected: &str, sources: &[(&str, &str)]) { + let errors = crate::check_program(sources).expect_err("the program should be rejected"); + let codes: Vec> = errors.iter().map(|error| error.diagnostic.code).collect(); + assert!( + codes == [Some(expected)], + "`{name}`: expected exactly [{expected}], got {codes:?}" + ); +} + +/// An argument should be rejected when its shape rides along through type +/// synonym expansion, or when no fundep determines it. +#[test] +fn nondetermined_instance_head_arguments_report_official_invalid_instance_head() { + let cases: [(&str, &str); 6] = [ + ( + // An empty record argument a class without fundeps cannot + // determine. + "argument in no fundep", + r#"module Main where +data MyUnit = MyUnit +class C a b +instance c :: C MyUnit {} +"#, + ), + ( + // The last argument is mentioned by no dependency. + "argument in no fundep", + r#"module Main where +data MyUnit = MyUnit +class C a b c | a -> b +instance c :: C MyUnit MyUnit {} +"#, + ), + ( + // `b` is determined by `a`, which it itself determines. + "mutually determined argument", + r#"module Main where +data MyUnit = MyUnit +class C a b | a -> b, b -> a +instance c :: C MyUnit {} +"#, + ), + ( + // A free unification variable survives the synonym into the + // head's row. + "synonym leaves a free variable in the row", + r#"module Main where +type X r = {x :: Int | r} +class C a +instance c :: C (X r) +"#, + ), + ( + // A record the derivation cannot determine, spelled through a + // synonym. + "derived head over a synonym record", + r#"module Main where +type T = {} +class Some a +derive instance someT :: Some T +"#, + ), + ( + "derived head over a record", + r#"module Main where +class Some a +derive instance someRecord :: Some {} +"#, + ), + ]; + for (name, source) in cases { + assert_one_code(name, "InvalidInstanceHead", &[("Main.purs", source)]); + } +} + +#[test] +fn determined_and_constructor_instance_heads_stay_accepted() { + // Constructor arguments remain legal in every position. + check_program(&[( + "Main.purs", + r#"module Main where +data MyUnit = MyUnit +class C a b +instance c :: C MyUnit MyUnit +"#, + )]) + .unwrap_or_else(|errors| panic!("constructor heads should type check: {errors:?}")); + // A row argument is legal where a fundep fully determines its position. + check_program(&[( + "Main.purs", + r#"module Main where +data MyUnit = MyUnit +class C a b | a -> b +instance c :: C MyUnit {} +"#, + )]) + .unwrap_or_else(|errors| panic!("a determined row argument should type check: {errors:?}")); + // An applied constructor head and a record head over a bound variable. + check_program(&[( + "Main.purs", + r#"module Main where +data Box a = Box a +class D a +instance dBox :: D (Box a) +instance dRecord :: D (Record r) +"#, + )]) + .unwrap_or_else(|errors| panic!("record-over-variable heads should type check: {errors:?}")); + // A helper class whose closed record argument sits in a determined + // position, the shape the official record helpers use. + check_program(&[( + "Main.purs", + r#"module Main where +data EndList = EndList +class Helper rl row sub | rl -> sub +instance helperNil :: Helper EndList row {} +"#, + )]) + .unwrap_or_else(|errors| panic!("a determined closed record should type check: {errors:?}")); +} + +#[test] +fn superclass_cycles_report_official_cycle_in_type_class_declaration() { + assert_one_code( + "a class may not have itself as a superclass", + "CycleInTypeClassDeclaration", + &[( + "Main.purs", + r#"module Main where +class (Foo a) <= Foo a +"#, + )], + ); + assert_one_code( + "mutual superclasses", + "CycleInTypeClassDeclaration", + &[( + "Main.purs", + r#"module Main where +class (Bar a) <= Foo a +class (Foo a) <= Bar a +"#, + )], + ); +} + +#[test] +fn a_recursive_instance_context_reports_possibly_infinite_instance() { + assert_one_code( + "recursive instance", + "PossiblyInfiniteInstance", + &[( + "Main.purs", + r#"module Main where +data YesNo = Yes +data Fix f = In (f (Fix f)) +data Wrapped a = Wrapped +class Eqish a where + eqish :: a -> a -> YesNo +instance eqWrapped :: (Eqish a) => Eqish (Wrapped a) where + eqish Wrapped Wrapped = Yes +instance eqFix :: (Eqish (f (Fix f))) => Eqish (Fix f) where + eqish (In f) (In g) = eqish f g +main = eqish (In Wrapped) (In Wrapped) +"#, + )], + ); +} diff --git a/crates/psrs-driver/src/tests/typecheck/mod.rs b/crates/psrs-driver/src/tests/typecheck/mod.rs index b7c2f363..0871b44d 100644 --- a/crates/psrs-driver/src/tests/typecheck/mod.rs +++ b/crates/psrs-driver/src/tests/typecheck/mod.rs @@ -1,5 +1,6 @@ use super::*; +mod instance_heads; mod opaque; #[test] diff --git a/crates/psrs-typecheck/src/typecheck/classes/environment/instance_head.rs b/crates/psrs-typecheck/src/typecheck/classes/environment/instance_head.rs new file mode 100644 index 00000000..a0a3870d --- /dev/null +++ b/crates/psrs-typecheck/src/typecheck/classes/environment/instance_head.rs @@ -0,0 +1,186 @@ +//! The determined-instance-head rule the common instance recorder applies to +//! every local instance. +//! +//! `purs` raises `InvalidInstanceHead` from `TypeChecker.checkTypeClassInstance` +//! for any head argument that is not a type variable, a type-level literal, a +//! type constructor, a function or constructor application over those shapes, +//! or a row in an argument a functional dependency fully determines. The +//! triggers differ — a wildcard (`TypeWildcards3.purs`), a free unification +//! variable under a synonym (`TypeSynonyms7.purs`), a record head the +//! derivation cannot determine (`3510.purs`, +//! `InvalidDerivedInstance2.purs`), and an argument no dependency determines +//! (`RowInInstanceNotDetermined0/1/2.purs`) — but the check is one rule about +//! the head's shape, applied per argument after synonyms expand. + +use super::super::super::*; +use std::collections::BTreeMap; +use std::collections::BTreeSet; + +/// Applies the head rule to one instance's elaborated head arguments. The +/// return is `false` when an argument rejects, with the diagnostic already +/// reported at the instance head's range. +pub(in crate::typecheck) fn validate_head_shapes( + checker: &mut Checker, + class: &ClassInfo, + head_arguments: &[InferType], + head_span: TextRange, +) -> bool { + let determined = determined_fundep_arguments(class.parameters.len(), &class.fundeps); + let invalid = head_arguments + .iter() + .enumerate() + .find_map(|(index, argument)| { + (!valid_instance_head_argument(argument, determined.contains(&index))) + .then_some(argument) + }); + let Some(argument) = invalid else { + return true; + }; + let rendered = checker.display_type(argument); + checker.state.errors.push(TypeCheckError::new( + TypeCheckErrorKind::InvalidInstanceHead, + head_span, + format!( + "an instance head argument cannot be `{rendered}`; \ + each head argument must be a type constructor application or a type \ + variable, and a row argument must be fully determined by the class's \ + functional dependencies", + ), + )); + false +} + +/// Whether one instance-head argument may appear at its position. +/// +/// This is `checkTypeClassInstance`'s `check` in the official +/// `TypeChecker.hs`, ported to the inference representation. A row argument is +/// weakly determined, so it cannot influence instance selection; that is why a +/// row is legal only when a functional dependency fully determines its +/// position, and a row found inside a record application +/// (`Record (x :: Int | r)`) shares its argument's flag. +pub(in crate::typecheck) fn valid_instance_head_argument( + ty: &InferType, + fundep_determined: bool, +) -> bool { + match ty { + InferType::Variable(_) + | InferType::Constructor(_) + | InferType::TypeLevelString(_) + | InferType::TypeLevelInt(_) => true, + InferType::Application(function, argument) => { + valid_instance_head_argument(function, fundep_determined) + && valid_instance_head_argument(argument, fundep_determined) + } + InferType::RowEmpty => fundep_determined, + InferType::RowExtend { + ty: field, tail, .. + } => { + fundep_determined + && valid_instance_head_argument(field, fundep_determined) + && valid_instance_head_argument(tail, fundep_determined) + } + InferType::ForAll { .. } | InferType::Constrained { .. } => false, + } +} + +/// The argument positions of a class that no covering set contains: official +/// `typeClassDeterminedArguments` in `Environment.hs`. +/// +/// A covering set is an inclusion-minimal set of argument positions from which +/// every remaining argument follows through the class's functional +/// dependencies; an argument is fully determined exactly when it stands in no +/// covering set. This is a port of `computeCoveringSets`, reduced to the +/// determined set. The frontier starts at the full parameter set, and each +/// still-applicable dependency removes one parameter it determines — including +/// parameters that dependency no longer sees in its determining positions — +/// until nothing reduces any set further. An argument that ends up needed by +/// every covering set is one the dependencies can never pin down, so it must +/// be a selectable part of the head. +pub(in crate::typecheck) fn determined_fundep_arguments( + parameter_count: usize, + fundeps: &[FundepInfo], +) -> HashSet { + // Without dependencies every argument is needed: the only covering set is + // the full parameter list, and no argument is fully determined. + if fundeps.is_empty() { + return HashSet::new(); + } + // The determined parameter each dependency can remove next, paired with + // the determining sets it offers. Several dependencies may determine the + // same parameter, so the positions accumulate lists like the official + // `M.fromListWith (<>)` does. + let initial = fundeps + .iter() + .flat_map(|fundep| { + fundep.determined.iter().map(|&target| { + ( + target, + fundep.determining.iter().copied().collect::>(), + ) + }) + }) + .fold( + BTreeMap::new(), + |mut edges: BTreeMap>>, (target, sources)| { + edges.entry(target).or_default().push(sources); + edges + }, + ); + let all = (0..parameter_count).collect::>(); + // The frontier: a needed set paired with its applicable dependencies. + // The official frontier is keyed by the needed set and merges repeated + // arrivals keeping the first, so the same entry does here. + let mut frontier: BTreeMap, BTreeMap>>> = + BTreeMap::from([(all, initial)]); + let mut covering_sets: HashSet> = HashSet::new(); + while let Some((needed, in_edges)) = frontier.pop_first() { + if in_edges.is_empty() { + covering_sets.insert(needed); + continue; + } + let source_positions = in_edges + .values() + .flatten() + .flatten() + .copied() + .collect::>(); + // A dependency that determines an argument no surviving dependency + // uses is acyclic: removing it cannot spur other removals, so trying + // only it is what the official search prefers. + let acyclic = in_edges + .keys() + .find(|&y| !source_positions.contains(y)) + .copied(); + let candidates = match acyclic { + Some(y) => vec![y], + None => in_edges.keys().copied().collect(), + }; + for y in candidates { + let mut next_needed = needed.clone(); + next_needed.remove(&y); + let mut next_edges = in_edges.clone(); + next_edges.remove(&y); + if acyclic.is_none() { + for sources in next_edges.values_mut() { + sources.retain(|source| !source.contains(&y)); + } + next_edges.retain(|_, sources| !sources.is_empty()); + } + frontier.entry(next_needed).or_insert(next_edges); + } + } + // Reduce to the inclusion-minimal covering sets, then an argument is + // determined when no covering set contains it. + let minimal = covering_sets.iter().filter(|set| { + !covering_sets + .iter() + .any(|other| other.len() < set.len() && other.is_subset(set)) + }); + let mut determined: HashSet = (0..parameter_count).collect(); + for set in minimal { + for position in set.iter() { + determined.remove(position); + } + } + determined +} diff --git a/crates/psrs-typecheck/src/typecheck/classes/environment/mod.rs b/crates/psrs-typecheck/src/typecheck/classes/environment/mod.rs index c6179110..0e253ecc 100644 --- a/crates/psrs-typecheck/src/typecheck/classes/environment/mod.rs +++ b/crates/psrs-typecheck/src/typecheck/classes/environment/mod.rs @@ -6,6 +6,9 @@ mod compiler; mod method; use method::validate_method_signature; +mod instance_head; + +use instance_head::validate_head_shapes; impl Checker { /// Records every class in the program with its parameters, superclass @@ -181,7 +184,7 @@ impl Checker { } if let Some(span) = cycle { self.state.errors.push(TypeCheckError::new( - TypeCheckErrorKind::UnsupportedClass, + TypeCheckErrorKind::CycleInTypeClassDeclaration, span, "class superclasses form a cycle", )); @@ -302,6 +305,12 @@ impl Checker { }; head_arguments[1] = resolved; } + // The official determined-instance-head rule, applied per argument + // after synonyms expand (`checkTypeClassInstance` in `purs`'s + // `TypeChecker.hs`). + if local && !validate_head_shapes(self, &class, &head_arguments, instance.head.span) { + return; + } let mut context = Vec::with_capacity(instance.context.len()); let mut context_parameters = Vec::with_capacity(instance.context.len()); let mut valid = true; diff --git a/crates/psrs-typecheck/src/typecheck/classes/solve/search.rs b/crates/psrs-typecheck/src/typecheck/classes/solve/search.rs index fff0dadc..d628db1b 100644 --- a/crates/psrs-typecheck/src/typecheck/classes/solve/search.rs +++ b/crates/psrs-typecheck/src/typecheck/classes/solve/search.rs @@ -38,6 +38,18 @@ impl Checker { chain: &mut RequeueChain, ) -> Option { if !depth.within_bound() { + // The search never terminates on this chain: every selected + // instance's context contains the very constraint being solved, at + // an unchanging or growing shape. Official `Entailment` raises + // `PossiblyInfiniteInstance` for exactly this, at its own work + // bound, so the bound is the diagnostic rather than a silent + // failure the enclosing boundary would report as missing evidence. + let rendered = self.display_constraint(constraint.class_id, &constraint.arguments); + self.state.errors.push(TypeCheckError::new( + TypeCheckErrorKind::PossiblyInfiniteInstance, + constraint.span, + format!("instance search for constraint {rendered} cannot terminate"), + )); return None; } // Instance contexts are created after the outer wanted-list fixed point. diff --git a/crates/psrs-typecheck/src/typecheck/error.rs b/crates/psrs-typecheck/src/typecheck/error.rs index ca6acbfa..24b2a68f 100644 --- a/crates/psrs-typecheck/src/typecheck/error.rs +++ b/crates/psrs-typecheck/src/typecheck/error.rs @@ -38,6 +38,17 @@ pub enum TypeCheckErrorKind { /// contains a type wildcard. `purs` raises this in /// `TypeChecker.checkTypeClassInstance`; see `failing/TypeWildcards3.purs`. InvalidInstanceHead, + /// An instance search that never terminates because the selected instance's + /// own context contains the very constraint being solved, at a growing or + /// unchanging shape. `purs` raises this in `Entailment`'s `go` when the + /// subgoal chain exceeds its work bound; see `failing/438.purs`. + PossiblyInfiniteInstance, + /// A class's superclasses form a cycle, so the class environment is + /// unsatisfiable and dictionary construction would not terminate. `purs` + /// raises this for the class declaration that reintroduces an ancestor; see + /// `failing/Superclasses2.purs` and + /// `failing/SelfCycleInTypeClassDeclaration.purs`. + CycleInTypeClassDeclaration, /// An inferred public value mentions a local type omitted from exports. TransitiveExport, /// A class has no compiler-supported deriving rule. Official @@ -125,6 +136,7 @@ impl TypeCheckErrorKind { self, TypeCheckErrorKind::NoInstance | TypeCheckErrorKind::OverlappingInstances + | TypeCheckErrorKind::PossiblyInfiniteInstance | TypeCheckErrorKind::TypeMismatch ) } @@ -175,6 +187,8 @@ impl TypeCheckErrorKind { "InvalidCoercibleInstanceDeclaration" } TypeCheckErrorKind::InvalidInstanceHead => "InvalidInstanceHead", + TypeCheckErrorKind::PossiblyInfiniteInstance => "PossiblyInfiniteInstance", + TypeCheckErrorKind::CycleInTypeClassDeclaration => "CycleInTypeClassDeclaration", TypeCheckErrorKind::TransitiveExport => "TransitiveExportError", TypeCheckErrorKind::CannotDerive => "CannotDerive", TypeCheckErrorKind::ExpectedTypeConstructor => "ExpectedTypeConstructor", diff --git a/docs/design/frontend/type-system/classes-and-evidence.md b/docs/design/frontend/type-system/classes-and-evidence.md index 456049e3..83ab68eb 100644 --- a/docs/design/frontend/type-system/classes-and-evidence.md +++ b/docs/design/frontend/type-system/classes-and-evidence.md @@ -292,6 +292,34 @@ represent. The coercion rule is dispatched through the shared primitive table by class identity rather than by a comparison at the call site. +The instance recorder applies one determined-instance-head rule to every local +instance, after synonyms expand and after a head-shape derivation resolves its +trailing wildcard: each elaborated head argument must be a type variable, a +type-level literal, a type constructor, or a constructor or function +application over those, and a row argument is legal only where the class's +functional dependencies fully determine its position. The fully determined +positions are official `typeClassDeterminedArguments`: the arguments standing +in no inclusion-minimal covering set, ported from `computeCoveringSets`, so a +parameter determined only by an argument it itself determines is not determined +and official record helpers that place a closed record in a determined +parameter keep compiling. Every trigger — a wildcard (`TypeWildcards3.purs`), +a free unification variable beneath a synonym (`TypeSynonyms7.purs`), a +derived record head (`3510.purs`, `InvalidDerivedInstance2.purs`), and an +argument no fundep determines (`RowInInstanceNotDetermined0/1/2.purs`) — is +`InvalidInstanceHead`, raised in the recorder before the instance is recorded, +so no overlap or deriving diagnostic follows it. The wildcard-in-context path +keeps its own narrower check with the same code, because a context stays +solvable where the head is not. + +Superclass cycles raise `CycleInTypeClassDeclaration` at the class declaration +that reintroduces an ancestor; the reachability check is unchanged and clearing +the edges keeps dictionary construction from recursing while diagnostics +finish. An instance search that exhausts its depth bound reports +`PossiblyInfiniteInstance` at the constraint that would be solved again — the +official `Entailment` work bound — instead of failing silently into an +enclosing `NoInstanceFound`, and the code joins the constraint-failure codes so +no enclosing boundary reports the obligation a second time. + Selected instance contexts retain stable wanted IDs in the shared worklist, so solving or generalizing a residual updates the evidence the instance constructor uses. A missing referenced wanted is an invalid-HIR error. Primitive deferrals From 54d69f924766486f57b41718cc49ce25b5e89170 Mon Sep 17 00:00:00 2001 From: biu Date: Sun, 18 Oct 2026 03:58:13 +0800 Subject: [PATCH 3/8] Report the kinds verdict of an unsolvable Coercible obligation Official solving unifies a picked-up Coercible constraint's argument kinds (Entailment/Coercible.hs), including a pair its role decomposition dissolves into, and raises KindsDoNotUnify there rather than falling through to a bare NoInstanceFound: a pair whose kinds share no solution is the one thing about a coercion there is nothing to search for. The Coercible rule now records that verdict from the first pair of its proof whose kind equation has no solution - the outermost pair is the first constraint official solving would have picked up - reads it only when the whole proof fails, and returns Failed under the kind equation's own diagnosis, which the enclosing resolution no longer duplicates with a NoInstanceFound. failing/CoercibleKindMismatch.purs coerces Proxy Unary to Proxy Binary, whose role decomposition needs Coercible Unary Binary for kinds k -> Type and k -> k -> Type, so its use of coerce now fails with KindsDoNotUnify attributed to its own module. The kind-check entry point the l3 scoreboard measures stops before the constraint solver, so the case's mismatch there is not closed by this; the full check and the class boards' entry points do surface it. Docs: the roles and coercions acceptance record states the verdict. --- crates/psrs-driver/src/tests/coercion.rs | 8 +- crates/psrs-kind/src/lib.rs | 2 +- crates/psrs-typecheck/src/typecheck/error.rs | 7 ++ crates/psrs-typecheck/src/typecheck/kind.rs | 52 ++++++++----- .../src/typecheck/prim/coercible/mod.rs | 69 ++++++++++++++++-- .../src/typecheck/prim/tests/coercible.rs | 73 +++++++++++++++++++ .../src/typecheck/prim/tests/mod.rs | 1 + .../src/typecheck/prim/tests/outcomes.rs | 28 ------- .../frontend/roles-and-coercions.md | 7 ++ 9 files changed, 191 insertions(+), 56 deletions(-) create mode 100644 crates/psrs-typecheck/src/typecheck/prim/tests/coercible.rs diff --git a/crates/psrs-driver/src/tests/coercion.rs b/crates/psrs-driver/src/tests/coercion.rs index a7a4ec11..aac0a501 100644 --- a/crates/psrs-driver/src/tests/coercion.rs +++ b/crates/psrs-driver/src/tests/coercion.rs @@ -371,7 +371,11 @@ fn foreign_data_roles_default_to_nominal_and_accept_explicit_signatures() { } #[test] -fn rejects_coercion_between_type_constructors_with_different_kinds() { +fn reports_a_coercion_between_type_constructors_with_different_kinds() { + // `failing/CoercibleKindMismatch.purs`: the constraint's role decomposition + // needs `Coercible Unary Binary`, and official solving unifies a picked-up + // constraint's argument kinds before refusing it, so the failure is the + // kind equation's verdict, not a missing instance. let source = r#"module Main where import Safe.Coerce (coerce) @@ -387,7 +391,7 @@ type role Proxy representational bad :: Proxy Unary -> Proxy Binary bad = coerce "#; - rejects(&[("Main.purs", source)], "NoInstanceFound"); + rejects(&[("Main.purs", source)], "KindsDoNotUnify"); } #[test] diff --git a/crates/psrs-kind/src/lib.rs b/crates/psrs-kind/src/lib.rs index 3e593b29..893c44bb 100644 --- a/crates/psrs-kind/src/lib.rs +++ b/crates/psrs-kind/src/lib.rs @@ -17,7 +17,7 @@ mod denote; mod kind; mod solve; -pub use check::{check_module, check_program}; +pub use check::{KINDS_DO_NOT_UNIFY, check_module, check_program}; pub use denote::{KindScope, denote_kind}; pub use kind::{ CheckedKindEnv, Kind, KindDiagnostic, KindScheme, constraint_kind, primitive_kind, type_kind, diff --git a/crates/psrs-typecheck/src/typecheck/error.rs b/crates/psrs-typecheck/src/typecheck/error.rs index ca6acbfa..3afdf5c0 100644 --- a/crates/psrs-typecheck/src/typecheck/error.rs +++ b/crates/psrs-typecheck/src/typecheck/error.rs @@ -120,12 +120,19 @@ impl TypeCheckErrorKind { /// Whether this error already reports why one wanted constraint failed to /// resolve. Callers must not add a second `NoInstanceFound` at an enclosing /// instance or deferral boundary. + /// + /// `KindsDoNotUnify` belongs here through the `Coercible` rule: official + /// solving reports a constraint's argument kinds when it picks the + /// constraint up, and that verdict *is* the resolution's answer, not a + /// side finding, so the bare `no instance` message would only say the same + /// failure again. pub(in crate::typecheck) fn reports_constraint_failure(self) -> bool { matches!( self, TypeCheckErrorKind::NoInstance | TypeCheckErrorKind::OverlappingInstances | TypeCheckErrorKind::TypeMismatch + | TypeCheckErrorKind::KindsDoNotUnify ) } diff --git a/crates/psrs-typecheck/src/typecheck/kind.rs b/crates/psrs-typecheck/src/typecheck/kind.rs index 9070e390..02841f23 100644 --- a/crates/psrs-typecheck/src/typecheck/kind.rs +++ b/crates/psrs-typecheck/src/typecheck/kind.rs @@ -13,7 +13,28 @@ //! the bindings that produced them. use super::*; -use psrs_kind::{KindScheme, KindScope}; +use psrs_kind::{KINDS_DO_NOT_UNIFY, KindScheme, KindScope}; + +/// What the kinds of a coercion pair say. This is the one trial the `Coercible` +/// rule has for a pair's kind equation: both kinds are read through +/// [`Checker::kind_of_type`] and the equation is solved through the one kind +/// substitution speculatively, so a verdict leaves no binding behind for a +/// later step to read. +pub(in crate::typecheck) enum CoercionKinds { + /// Both kinds are known and the equation solves. + Compatible, + /// Both kinds are known and the equation has no solution. Official solving + /// reports a pair's kinds exactly here: `Entailment/Coercible.hs` unifies + /// a picked-up constraint's argument kinds before refusing it. `error` is + /// the diagnosis the shared solver produced, re-reported by the `Coercible` + /// rule in the terms it owes the suite. + Mismatch(psrs_kind::KindError), + /// The equation could not be posed. A kind that is not derivable is the + /// kind pass's diagnostic — a scheme the program never checked decides + /// nothing about a conversion — and a solver rejection on any ground other + /// than a plain conflict is not this trial's verdict. + Undetermined, +} impl Checker { /// Allocates a fresh kind variable from the one kind solver. @@ -210,31 +231,26 @@ impl Checker { } } - /// Whether a representation conversion may be attempted between `source` - /// and `target` at all, which is the question their kinds answer. - /// - /// This adds no machinery of its own: it reads both kinds through - /// [`Self::kind_of_type`] and solves the equation through the one kind - /// solver, exactly as a binding does. It is a trial, because a coercion that - /// turns out not to hold — a phantom argument, an invisible newtype — must - /// not leave a kind binding behind for a later one to read. - /// - /// A type with no kind, because the program produced no checked scheme for - /// it, is not treated as compatible. The missing scheme is a kind-pass - /// diagnostic; until it is reported, these kinds say nothing about the - /// conversion. - pub(super) fn coercion_kinds_compatible( + /// Reads a coercion pair's kinds and classifies what they say as a trial. + /// See [`CoercionKinds`] for the verdicts. + pub(super) fn coercion_kinds_trial( &mut self, source: &InferType, target: &InferType, span: TextRange, - ) -> bool { + ) -> CoercionKinds { self.speculate(|checker| { let source = checker.kind_of_type(source, span)?; let target = checker.kind_of_type(target, span)?; - checker.unify_kind(source, target, span).then_some(()) + match psrs_kind::unify_kind(&mut checker.state.kinds, source, target, span) { + Ok(()) => Some(CoercionKinds::Compatible), + Err(error) => match error.code { + KINDS_DO_NOT_UNIFY => Some(CoercionKinds::Mismatch(error)), + _ => Some(CoercionKinds::Undetermined), + }, + } }) - .is_some() + .unwrap_or(CoercionKinds::Undetermined) } fn report_kind_error(&mut self, error: &psrs_kind::KindError) { diff --git a/crates/psrs-typecheck/src/typecheck/prim/coercible/mod.rs b/crates/psrs-typecheck/src/typecheck/prim/coercible/mod.rs index 1ed4ec98..a1c639cc 100644 --- a/crates/psrs-typecheck/src/typecheck/prim/coercible/mod.rs +++ b/crates/psrs-typecheck/src/typecheck/prim/coercible/mod.rs @@ -16,6 +16,7 @@ //! private reader for source syntax. use super::{EvidenceClass, PrimitiveArgs, PrimitiveEvidence, PrimitiveOutcome, PrimitiveRule}; +use crate::typecheck::kind::CoercionKinds; use crate::typecheck::*; mod givens; @@ -41,13 +42,27 @@ pub(in crate::typecheck) const RULE: PrimitiveRule = PrimitiveRule { /// unknown is the conflation the four-outcome contract exists to prevent. /// `Undecided` sends the obligation into instance search, which is where an /// assumption about the unknown types would be found. +/// +/// One answer shape aside from `Solved` is `Failed`, and only for the finding +/// official solving reports itself: its `Entailment/Coercible.hs` unifies the +/// kinds of a picked-up constraint's two arguments — including one its role +/// decomposition just derived — and raises `KindsDoNotUnify` there rather than +/// falling through to a bare `NoInstanceFound`. A pair whose kinds cannot +/// unify is the one thing about a coercion there is nothing to search for. fn solve(checker: &mut Checker, args: &PrimitiveArgs) -> PrimitiveOutcome { let arguments = args.resolved(checker); let [source, target] = arguments.as_slice() else { return PrimitiveOutcome::Undecided; }; - if !checker.proves_coercible(source, target, args.span()) { - return PrimitiveOutcome::Undecided; + let mut kind_conflict = None; + if !checker.proves_coercible(source, target, args.span(), &mut kind_conflict) { + return match kind_conflict { + Some(error) => PrimitiveOutcome::Failed { + code: TypeCheckErrorKind::KindsDoNotUnify, + detail: error.message.to_owned(), + }, + None => PrimitiveOutcome::Undecided, + }; } PrimitiveOutcome::Solved { evidence: PrimitiveEvidence::Proof { @@ -64,8 +79,9 @@ impl Checker { source: &InferType, target: &InferType, span: TextRange, + kind_conflict: &mut Option, ) -> bool { - self.proves_coercible_inner(source, target, span, 0, &mut HashSet::new()) + self.proves_coercible_inner(source, target, span, 0, &mut HashSet::new(), kind_conflict) } fn proves_coercible_inner( @@ -75,6 +91,7 @@ impl Checker { span: TextRange, depth: usize, path: &mut HashSet<(String, String)>, + kind_conflict: &mut Option, ) -> bool { if depth > 64 { return false; @@ -114,10 +131,31 @@ impl Checker { span, depth + 1, &mut nested, + kind_conflict, ); } - if !self.coercion_kinds_compatible(&source, &target, span) { - return false; + // The kinds the pair would have to share. Official solving checks a + // pair's kinds exactly here, when it picks a constraint up: the shared + // solver holds kinds neither binding nor derivation invented, so a + // conflict it finds is the constraint's answer, not a side finding. The + // verdict is remembered for this proof attempt and reported once, from + // the outermost pair — the first constraint official solving would have + // picked up — and only for a genuine `KindsDoNotUnify` verdict: a kind + // that is not derivable is the kind pass's diagnostic, and this trial + // must not read it as a coercion verdict either way. + // + // The verdict stays a trial about the solver state, so a route this + // attempt declines can still leave no binding behind; the report is + // re-derived in one step in `solve`, through `Failed`. + match self.coercion_kinds_trial(&source, &target, span) { + CoercionKinds::Compatible => {} + CoercionKinds::Mismatch(error) => { + if kind_conflict.is_none() { + *kind_conflict = Some(error); + } + return false; + } + CoercionKinds::Undetermined => return false, } if self.given_coercible(&source, &target) { return true; @@ -144,12 +182,14 @@ impl Checker { span, depth + 1, &mut field_path, + kind_conflict, ) && self.proves_coercible_inner( source_tail, target_tail, span, depth + 1, &mut tail_path, + kind_conflict, ); } (InferType::RowExtend { .. }, _) @@ -165,13 +205,27 @@ impl Checker { if let Some(underlying) = self.unwrap_visible_newtype(&source) { let mut nested = path.clone(); - if self.proves_coercible_inner(&underlying, &target, span, depth + 1, &mut nested) { + if self.proves_coercible_inner( + &underlying, + &target, + span, + depth + 1, + &mut nested, + kind_conflict, + ) { return true; } } if let Some(underlying) = self.unwrap_visible_newtype(&target) { let mut nested = path.clone(); - if self.proves_coercible_inner(&source, &underlying, span, depth + 1, &mut nested) { + if self.proves_coercible_inner( + &source, + &underlying, + span, + depth + 1, + &mut nested, + kind_conflict, + ) { return true; } } @@ -207,6 +261,7 @@ impl Checker { span, depth + 1, &mut nested, + kind_conflict, ) } hir::Role::Phantom => true, diff --git a/crates/psrs-typecheck/src/typecheck/prim/tests/coercible.rs b/crates/psrs-typecheck/src/typecheck/prim/tests/coercible.rs new file mode 100644 index 00000000..6bd9f478 --- /dev/null +++ b/crates/psrs-typecheck/src/typecheck/prim/tests/coercible.rs @@ -0,0 +1,73 @@ +//! The `Prim.Coerce.Coercible` rule's contract, exercised from the table: it is +//! a real rule written against the framework the synthetic cases in +//! `outcomes` cover, so its dispatch questions are asked here. + +use super::*; + +/// Dispatches one obligation through the rule table. +fn dispatch(checker: &mut Checker, constraint: &WantedConstraint) -> PrimitiveDispatch { + checker.solve_primitive(constraint, SolveDepth::new()) +} + +#[test] +fn a_coercible_obligation_reaches_the_rule_from_the_table() { + let mut checker = checker(); + let source = checker.fresh(); + let target = checker.fresh(); + let mut constraint = obligation(&mut checker, hir::TypeId::COERCIBLE, vec![source, target]); + assert_eq!( + primitive_rule(hir::TypeId::COERCIBLE).map(|r| r.arity), + Some(2) + ); + + // Two unknown arguments the role analysis cannot relate are undecided, so the + // obligation continues into the ordinary paths rather than being reported. + assert!(matches!( + dispatch(&mut checker, &constraint), + PrimitiveDispatch::None + )); + assert!(checker.state.errors.is_empty()); + + // Equal known arguments are proved, and the proof is the evidence. + constraint.arguments = vec![int(), int()]; + assert!(matches!( + dispatch(&mut checker, &constraint), + PrimitiveDispatch::Solved(WantedSolution::Coercible { .. }) + )); + assert!(checker.state.errors.is_empty()); +} + +#[test] +fn a_coercible_obligation_whose_arguments_have_different_kinds_reports_kinds_do_not_unify() { + // Official solving unifies a picked-up `Coercible` constraint's argument + // kinds (`Entailment/Coercible.hs`), so `Coercible Int "label"` is a kind + // failure at that exact check rather than a missing instance: a `Type` and + // a `Symbol` share no kind, and no instance could ever decide the pair. + let mut checker = checker(); + let constraint = obligation( + &mut checker, + hir::TypeId::COERCIBLE, + vec![ + int(), + // A type-level string has kind `Symbol`, which no `Type`-kinded + // argument can share. + InferType::TypeLevelString("label".to_owned()), + ], + ); + assert!(matches!( + dispatch(&mut checker, &constraint), + PrimitiveDispatch::Reported + )); + assert_eq!(checker.state.errors.len(), 1); + let error = &checker.state.errors[0]; + assert_eq!( + error.kind, + TypeCheckErrorKind::KindsDoNotUnify, + "the verdict is the kind equation's, not a missing instance" + ); + assert_eq!(error.error_code(), Some("KindsDoNotUnify")); + assert_eq!( + error.span, constraint.span, + "the verdict names the obligation's own range" + ); +} diff --git a/crates/psrs-typecheck/src/typecheck/prim/tests/mod.rs b/crates/psrs-typecheck/src/typecheck/prim/tests/mod.rs index 0381cd1e..0d96bf16 100644 --- a/crates/psrs-typecheck/src/typecheck/prim/tests/mod.rs +++ b/crates/psrs-typecheck/src/typecheck/prim/tests/mod.rs @@ -10,6 +10,7 @@ use super::*; +mod coercible; mod outcomes; mod probe; mod symbol_rules; diff --git a/crates/psrs-typecheck/src/typecheck/prim/tests/outcomes.rs b/crates/psrs-typecheck/src/typecheck/prim/tests/outcomes.rs index f6bbf1fd..58acdafd 100644 --- a/crates/psrs-typecheck/src/typecheck/prim/tests/outcomes.rs +++ b/crates/psrs-typecheck/src/typecheck/prim/tests/outcomes.rs @@ -437,31 +437,3 @@ fn every_outcome_is_reachable_and_only_official_codes_are_reportable() { "a report's result is its diagnostic, not evidence" ); } - -#[test] -fn a_coercible_obligation_reaches_the_rule_from_the_table() { - let mut checker = checker(); - let source = checker.fresh(); - let target = checker.fresh(); - let mut constraint = obligation(&mut checker, hir::TypeId::COERCIBLE, vec![source, target]); - assert_eq!( - primitive_rule(hir::TypeId::COERCIBLE).map(|r| r.arity), - Some(2) - ); - - // Two unknown arguments the role analysis cannot relate are undecided, so the - // obligation continues into the ordinary paths rather than being reported. - assert!(matches!( - dispatch(&mut checker, &constraint), - PrimitiveDispatch::None - )); - assert!(checker.state.errors.is_empty()); - - // Equal known arguments are proved, and the proof is the evidence. - constraint.arguments = vec![int(), int()]; - assert!(matches!( - dispatch(&mut checker, &constraint), - PrimitiveDispatch::Solved(WantedSolution::Coercible { .. }) - )); - assert!(checker.state.errors.is_empty()); -} diff --git a/docs/implementation/frontend/roles-and-coercions.md b/docs/implementation/frontend/roles-and-coercions.md index 51461d73..4efeacc8 100644 --- a/docs/implementation/frontend/roles-and-coercions.md +++ b/docs/implementation/frontend/roles-and-coercions.md @@ -13,6 +13,13 @@ independently at use sites, including quantifiers that shadow class parameters. The roles and `Coercible` acceptance evidence and remaining runtime limits are recorded below. +A wanted `Coercible` constraint whose two arguments share no kind is not a +missing instance: official solving unifies a picked-up constraint's argument +kinds (`Entailment/Coercible.hs`), including one its role decomposition dissolves +into, and raises `KindsDoNotUnify` there. The rule returns that verdict through +its `Failed` outcome and the enclosing resolution does not add a second +`NoInstanceFound` for it. + ## Scope This record tracks source role declarations, checked role metadata, primitive From 56fe3cda5b5a1d0cabac45a4e448af426cd1c099 Mon Sep 17 00:00:00 2001 From: biu Date: Sun, 18 Oct 2026 05:06:42 +0800 Subject: [PATCH 4/8] Report the official check-site codes at type annotations and local signatures purs routes a written type's must-have-kind-Type equation through checkTypeKind, whose failure is ExpectedType rather than the kind unifier's KindsDoNotUnify. psrs-kind solves the same equation with the same state at its two checkTypeKind positions -- value signatures and local ascriptions -- so failing/1570.purs and failing/KindStar.purs report ExpectedType, one of the two M4 codes that had no source. Class members, constructor fields, superclass constraints, instance heads, and synonym bodies keep reporting KindsDoNotUnify, matching the official checkKind positions. Local annotations now also scope their variables the officially recorded way of #2542: the forall binders written in the enclosing declaration's signature, the binders written in the local signature itself, and, for instance members, the free variables written in the instance head and context. Anything else is UndefinedTypeVariable before the kind is read, so failing/2542.purs (bar :: Array a under foo :: T with T = forall a. Array a) reports the last M3 code without a source. Scoreboards (annotations oracle, vendored v0.15.16, PSRS_STDLIB_ROOT on the pinned stdlib): L3 39/48 to 40/48 with UndefinedTypeVariable 3/4 to 4/4 and KindsDoNotUnify unchanged at 16/24; L4 39/50 to 41/50 with ExpectedType 0/2 to 2/2; L5 unchanged at 81/97; L2 failing 72/72 and passing resolution 403/413 unchanged. PolykindGeneralizationLet and SkolemEscapeKinds stay open, both anchored in the polykind model rather than in a diagnostic choice, recorded in the kinds design document. --- crates/psrs-driver/src/tests/resolution.rs | 9 +- crates/psrs-kind/src/check/infer/mod.rs | 34 ++- .../src/check/infer/pattern_annotations.rs | 253 ++++++++++++++---- crates/psrs-kind/src/check/mod.rs | 6 + crates/psrs-kind/src/tests/declarations.rs | 17 +- crates/psrs-kind/src/tests/foreign.rs | 4 +- crates/psrs-kind/src/tests/program.rs | 58 ++++ docs/design/frontend/type-system/kinds.md | 44 +++ 8 files changed, 361 insertions(+), 64 deletions(-) diff --git a/crates/psrs-driver/src/tests/resolution.rs b/crates/psrs-driver/src/tests/resolution.rs index 8b86330e..aea9f6b6 100644 --- a/crates/psrs-driver/src/tests/resolution.rs +++ b/crates/psrs-driver/src/tests/resolution.rs @@ -220,8 +220,11 @@ fn a_source_partial_constraint_reaches_the_registry_declaration() { #[test] fn a_source_partial_type_is_rejected_as_a_constraint_kinded_type() { - // `Partial` is a constraint, not a type of kind `Type`: `purs` reports the - // kind of `Partial` as `Constraint` for this same declaration. + // `Partial` has kind `Constraint`, so the value annotation's equation + // `kind ~ Type` fails. Official `TypeChecker/Kinds.hs` raises that + // equation through `checkTypeKind`, whose failure handler is + // `ExpectedType`; the kind unifier's own mismatch is reserved for kinds + // two types impose on each other. let source = "module Main where\n\ import Prim\n\ value :: Partial\n\ @@ -232,7 +235,7 @@ fn a_source_partial_type_is_rejected_as_a_constraint_kinded_type() { assert!( errors .iter() - .any(|error| error.diagnostic.code == Some("KindsDoNotUnify")), + .any(|error| error.diagnostic.code == Some("ExpectedType")), "{errors:?}" ); } diff --git a/crates/psrs-kind/src/check/infer/mod.rs b/crates/psrs-kind/src/check/infer/mod.rs index 9b4770fb..5be5a3f4 100644 --- a/crates/psrs-kind/src/check/infer/mod.rs +++ b/crates/psrs-kind/src/check/infer/mod.rs @@ -169,11 +169,43 @@ impl Checker<'_> { } } + /// Solves a type-annotation kind equation, reporting `ExpectedType` when + /// it fails. + /// + /// A value's written type must have kind `Type`, and at an annotation + /// (`x :: t`, a value signature, a binder annotation) official PureScript + /// solves exactly this equation through `checkTypeKind` + /// (`TypeChecker/Kinds.hs`), whose failure handler reports `ExpectedType` + /// with the written type and its kind. The kind unifier's own mismatch is + /// reserved for kinds two types impose on each other, so an annotation + /// that is not a type at all is not reported as a conflict between kinds. + /// + /// A failure may leave partial bindings behind; like the official + /// `unifyKindsWithFailure` failure handler, they stay and the report names + /// the kind the annotation carried when its equation failed. + pub(super) fn check_type_annotation_kind( + &mut self, + kind: Kind, + against: Kind, + span: TextRange, + ) { + if crate::solve::unify_kind(&mut self.state, kind.clone(), against, span).is_err() { + let kind = self.state.resolve(kind); + self.report( + EXPECTED_TYPE, + span, + format!( + "in a type-annotated expression `x :: t`, the type `t` must have kind `Type`; it has kind `{kind:?}`" + ), + ); + } + } + fn check_module_definitions(&mut self, module: &hir::Module) { for signature in module.declared_value_signatures() { let mut scope = HashMap::new(); let kind = self.kind_of_type(signature, &mut scope); - self.unify(kind, type_kind(), signature.span); + self.check_type_annotation_kind(kind, type_kind(), signature.span); } for declaration in &module.types { let Some(scheme) = self.schemes.get(&declaration.id).cloned() else { diff --git a/crates/psrs-kind/src/check/infer/pattern_annotations.rs b/crates/psrs-kind/src/check/infer/pattern_annotations.rs index aefc54d9..55c7b40f 100644 --- a/crates/psrs-kind/src/check/infer/pattern_annotations.rs +++ b/crates/psrs-kind/src/check/infer/pattern_annotations.rs @@ -1,123 +1,252 @@ use super::*; +use crate::kind::type_kind; impl Checker<'_> { + /// Walks annotations inside the expressions the module's own values and + /// instance members carry. + /// + /// A type variable an annotation names is in scope when one of the + /// binders the enclosing declaration *as written* quantifies names it, + /// which is the official `withScopedTypeVars` scoping: synonym expansion + /// must not bring a variable into scope (official #2542), so only the + /// `forall` binders written in the declaration's signature count. Instance + /// members additionally see the free variables the instance head and its + /// context are written with, which official `checkInstanceDeclaration` + /// binds for the whole instance. Everything else is an undefined type + /// variable, reported before the kind itself is read. pub(super) fn check_local_type_annotations(&mut self, module: &psrs_hir::Module) { - let mut expressions = module - .declarations - .iter() - .map(|declaration| declaration.value.clone()) - .collect::>(); - expressions.extend( - module - .instances - .iter() - .flat_map(|instance| instance.members.iter().map(|member| member.value.clone())), - ); - for expression in &expressions { - self.check_expression_annotations(expression); + for declaration in &module.declarations { + let mut bound = Vec::new(); + if let Some(signature) = &declaration.signature { + self.collect_written_binders(signature, &mut bound); + } + self.check_expression_annotations(&declaration.value, &mut bound); + } + for instance in &module.instances { + let mut bound = Vec::new(); + self.collect_free_variable_names(&instance.head, &mut bound); + for constraint in &instance.context { + self.collect_free_variable_names(constraint, &mut bound); + } + for member in &instance.members { + self.check_expression_annotations(&member.value, &mut bound.clone()); + } + } + } + + /// Collects the `forall` binders a written type quantifies, at every + /// nesting level, without expanding synonyms. + fn collect_written_binders(&self, ty: &psrs_hir::Type, bound: &mut Vec) { + match &ty.kind { + psrs_hir::TypeKind::Forall { variables, body } => { + for variable in variables { + if let Some(annotation) = &variable.kind { + self.collect_written_binders(annotation, bound); + } + bound.push(variable.name.clone()); + } + self.collect_written_binders(body, bound); + } + psrs_hir::TypeKind::Application(function, argument) => { + self.collect_written_binders(function, bound); + self.collect_written_binders(argument, bound); + } + psrs_hir::TypeKind::OperatorChain { operands, .. } => { + for operand in operands { + self.collect_written_binders(operand, bound); + } + } + psrs_hir::TypeKind::Function { parameter, result } => { + self.collect_written_binders(parameter, bound); + self.collect_written_binders(result, bound); + } + psrs_hir::TypeKind::Constrained { constraint, body } => { + self.collect_written_binders(constraint, bound); + self.collect_written_binders(body, bound); + } + psrs_hir::TypeKind::Row { fields, tail } + | psrs_hir::TypeKind::Record { fields, tail } => { + for field in fields { + self.collect_written_binders(&field.ty, bound); + } + if let Some(tail) = tail { + self.collect_written_binders(tail, bound); + } + } + _ => {} } } - fn check_expression_annotations(&mut self, expression: &psrs_hir::Expr) { - psrs_span::with_sufficient_stack(|| self.check_expression_annotations_inner(expression)) + /// Collects the type-variable names written in a type, whatever scope + /// binds them. Used for an instance's head and context, which official + /// PureScript binds wholesale for the members' checking. + fn collect_free_variable_names(&self, ty: &psrs_hir::Type, bound: &mut Vec) { + match &ty.kind { + psrs_hir::TypeKind::Variable(name) => bound.push(name.clone()), + psrs_hir::TypeKind::Forall { variables, body } => { + self.collect_free_variable_names(body, bound); + for variable in variables { + if let Some(annotation) = &variable.kind { + self.collect_free_variable_names(annotation, bound); + } + } + } + psrs_hir::TypeKind::Application(function, argument) => { + self.collect_free_variable_names(function, bound); + self.collect_free_variable_names(argument, bound); + } + psrs_hir::TypeKind::OperatorChain { operands, .. } => { + for operand in operands { + self.collect_free_variable_names(operand, bound); + } + } + psrs_hir::TypeKind::Function { parameter, result } => { + self.collect_free_variable_names(parameter, bound); + self.collect_free_variable_names(result, bound); + } + psrs_hir::TypeKind::Constrained { constraint, body } => { + self.collect_free_variable_names(constraint, bound); + self.collect_free_variable_names(body, bound); + } + psrs_hir::TypeKind::Row { fields, tail } + | psrs_hir::TypeKind::Record { fields, tail } => { + for field in fields { + self.collect_free_variable_names(&field.ty, bound); + } + if let Some(tail) = tail { + self.collect_free_variable_names(tail, bound); + } + } + _ => {} + } + } + + fn check_expression_annotations( + &mut self, + expression: &psrs_hir::Expr, + bound: &mut Vec, + ) { + psrs_span::with_sufficient_stack(|| { + self.check_expression_annotations_inner(expression, bound) + }) } - fn check_expression_annotations_inner(&mut self, expression: &psrs_hir::Expr) { + fn check_expression_annotations_inner( + &mut self, + expression: &psrs_hir::Expr, + bound: &mut Vec, + ) { use psrs_hir::ExprKind; match &expression.kind { - ExprKind::Typed { expression, ty } | ExprKind::TypeApplication { expression, ty } => { - self.check_annotation(ty); - self.check_expression_annotations(expression); + ExprKind::Typed { expression, ty } => { + self.check_ascription_annotation(ty, bound); + self.check_expression_annotations(expression, bound); + } + ExprKind::TypeApplication { expression, ty } => { + // A visible type application's argument is checked against + // the kind of the quantifier it instantiates, which is + // official `checkKind` in `infer' (VisibleTypeApp ...)` and + // not the `Type` equation. This pass still has no kind for + // the operand, so it keeps the pre-existing `Type` solve and + // waits for quantifier kinds to reach the shared kind state. + // The undefined-variable rule the ascription path gained + // applies here too, since the kind checking of an argument + // names it the same way. + self.check_references(ty, bound); + self.check_kind_of_annotation(ty); + self.check_expression_annotations(expression, bound); } ExprKind::Array(elements) => { for element in elements { - self.check_expression_annotations(element); + self.check_expression_annotations(element, bound); } } ExprKind::Record(fields) | ExprKind::MatchProduct(fields) => { for (_, value) in fields { - self.check_expression_annotations(value); + self.check_expression_annotations(value, bound); } } ExprKind::RecordUpdate { expression, fields } => { - self.check_expression_annotations(expression); + self.check_expression_annotations(expression, bound); for (_, value) in fields { - self.check_expression_annotations(value); + self.check_expression_annotations(value, bound); } } ExprKind::FieldAccess { expression, .. } => { - self.check_expression_annotations(expression) + self.check_expression_annotations(expression, bound) } ExprKind::Application(function, argument) => { - self.check_expression_annotations(function); - self.check_expression_annotations(argument); + self.check_expression_annotations(function, bound); + self.check_expression_annotations(argument, bound); } ExprKind::Operator { left, right, .. } => { - self.check_expression_annotations(left); - self.check_expression_annotations(right); + self.check_expression_annotations(left, bound); + self.check_expression_annotations(right, bound); } ExprKind::Negate { function, expression, .. } => { - self.check_expression_annotations(function); - self.check_expression_annotations(expression); + self.check_expression_annotations(function, bound); + self.check_expression_annotations(expression, bound); } ExprKind::OperatorChain { operands, .. } => { for operand in operands { - self.check_expression_annotations(operand); + self.check_expression_annotations(operand, bound); } } - ExprKind::OperatorSection { operand, .. } => self.check_expression_annotations(operand), - ExprKind::Lambda { body, .. } => self.check_expression_annotations(body), + ExprKind::OperatorSection { operand, .. } => { + self.check_expression_annotations(operand, bound) + } + ExprKind::Lambda { body, .. } => self.check_expression_annotations(body, bound), ExprKind::Let { bindings, body } => { for binding in bindings { - self.check_expression_annotations(&binding.value); + self.check_expression_annotations(&binding.value, bound); } - self.check_expression_annotations(body); + self.check_expression_annotations(body, bound); } ExprKind::If { condition, then_branch, else_branch, } => { - self.check_expression_annotations(condition); - self.check_expression_annotations(then_branch); - self.check_expression_annotations(else_branch); + self.check_expression_annotations(condition, bound); + self.check_expression_annotations(then_branch, bound); + self.check_expression_annotations(else_branch, bound); } ExprKind::Case { scrutinee, branches, } => { - self.check_expression_annotations(scrutinee); + self.check_expression_annotations(scrutinee, bound); for branch in branches { - self.check_pattern_annotations(&branch.pattern); - self.check_expression_annotations(&branch.value); + self.check_pattern_annotations(&branch.pattern, bound); + self.check_expression_annotations(&branch.value, bound); } } ExprKind::Guarded(clauses) => { for clause in clauses { for binding in &clause.where_bindings { - self.check_expression_annotations(&binding.value); + self.check_expression_annotations(&binding.value, bound); } for guard in &clause.guards { match guard { psrs_hir::Guard::Boolean(value) => { - self.check_expression_annotations(value) + self.check_expression_annotations(value, bound) } psrs_hir::Guard::Pattern { pattern, value } => { - self.check_pattern_annotations(pattern); - self.check_expression_annotations(value); + self.check_pattern_annotations(pattern, bound); + self.check_expression_annotations(value, bound); } psrs_hir::Guard::Let { bindings, .. } => { for binding in bindings { - self.check_expression_annotations(&binding.value); + self.check_expression_annotations(&binding.value, bound); } } } } - self.check_expression_annotations(&clause.value); + self.check_expression_annotations(&clause.value, bound); } } ExprKind::Local(_) @@ -129,19 +258,19 @@ impl Checker<'_> { } } - fn check_pattern_annotations(&mut self, pattern: &psrs_hir::Pattern) { + fn check_pattern_annotations(&mut self, pattern: &psrs_hir::Pattern, bound: &mut Vec) { match &pattern.kind { psrs_hir::PatternKind::Typed { pattern, ty } => { - self.check_annotation(ty); - self.check_pattern_annotations(pattern); + self.check_ascription_annotation(ty, bound); + self.check_pattern_annotations(pattern, bound); } psrs_hir::PatternKind::Array(elements) => { for element in elements { - self.check_pattern_annotations(element); + self.check_pattern_annotations(element, bound); } } psrs_hir::PatternKind::Named { pattern, .. } => { - self.check_pattern_annotations(pattern); + self.check_pattern_annotations(pattern, bound); } psrs_hir::PatternKind::Constructor { arguments, .. } | psrs_hir::PatternKind::OperatorChain { @@ -149,12 +278,12 @@ impl Checker<'_> { .. } => { for argument in arguments { - self.check_pattern_annotations(argument); + self.check_pattern_annotations(argument, bound); } } psrs_hir::PatternKind::Record { fields, .. } => { for (_, field) in fields { - self.check_pattern_annotations(field); + self.check_pattern_annotations(field, bound); } } psrs_hir::PatternKind::Wildcard @@ -167,8 +296,18 @@ impl Checker<'_> { } } - fn check_annotation(&mut self, ty: &psrs_hir::Type) { - let kind = self.kind_of_type(ty, &mut std::collections::HashMap::new()); - self.unify(kind, crate::kind::type_kind(), ty.span); + /// The written type of a type ascription is checked against `Type`, and a + /// type variable it names must be one of the binders the enclosing + /// declaration wrote. + fn check_ascription_annotation(&mut self, ty: &psrs_hir::Type, bound: &mut Vec) { + self.check_references(ty, bound); + self.check_kind_of_annotation(ty); + } + + /// Reads a local annotation's kind and solves it against kind `Type`. + fn check_kind_of_annotation(&mut self, ty: &psrs_hir::Type) { + let mut kinds = std::collections::HashMap::new(); + let kind = self.kind_of_type(ty, &mut kinds); + self.check_type_annotation_kind(kind, type_kind(), ty.span); } } diff --git a/crates/psrs-kind/src/check/mod.rs b/crates/psrs-kind/src/check/mod.rs index 6c0418ce..af3184a5 100644 --- a/crates/psrs-kind/src/check/mod.rs +++ b/crates/psrs-kind/src/check/mod.rs @@ -19,6 +19,12 @@ pub const PARTIALLY_APPLIED_SYNONYM: &str = "PartiallyAppliedSynonym"; pub const CYCLE_IN_TYPE_SYNONYM: &str = "CycleInTypeSynonym"; pub const CYCLE_IN_KIND_DECLARATION: &str = "CycleInKindDeclaration"; pub const UNDEFINED_TYPE_VARIABLE: &str = "UndefinedTypeVariable"; +/// A type annotation's written type must have kind `Type`. Official +/// PureScript solves this equation in `checkTypeKind` +/// (`TypeChecker/Kinds.hs`), whose failure handler reports `ExpectedType` +/// with the written type and its kind instead of the kind unifier's own +/// mismatch. +pub const EXPECTED_TYPE: &str = "ExpectedType"; /// A referenced type that the program never checked, so no kind is known for /// it. This is the code official PureScript reports when `elaborateKind` cannot /// resolve a constructor: a missing kind is not an inferable parameter. diff --git a/crates/psrs-kind/src/tests/declarations.rs b/crates/psrs-kind/src/tests/declarations.rs index 41c9a7ab..aae15de4 100644 --- a/crates/psrs-kind/src/tests/declarations.rs +++ b/crates/psrs-kind/src/tests/declarations.rs @@ -21,10 +21,21 @@ fn reports_a_kind_mismatch_between_constructor_fields() { assert!(codes(&errors).contains(&"KindsDoNotUnify"), "{errors:?}"); } +#[test] +fn reports_a_value_signature_of_a_non_type_kind() { + // `failing/KindStar.purs`: a value signature's written type must have + // kind `Type`; the official `checkTypeKind` failure is `ExpectedType`. + let errors = check("module Main where\ndata List a\ntest :: List\ntest = unit\n"); + assert!(codes(&errors).contains(&"ExpectedType"), "{errors:?}"); +} + #[test] fn checks_kind_of_a_typed_pattern_annotation() { + // A typed binder's written type must have kind `Type`; official + // PureScript solves that equation through `checkTypeKind`, whose failure + // is `ExpectedType` (`failing/1570.purs` names the same position). let errors = check("module Main where\nbad (value :: Array) = value\n"); - assert!(codes(&errors).contains(&"KindsDoNotUnify"), "{errors:?}"); + assert!(codes(&errors).contains(&"ExpectedType"), "{errors:?}"); } #[test] @@ -95,7 +106,9 @@ fn rejects_an_unsaturated_foreign_data_constructor() { bad :: Effect\n\ bad = 1\n", ); - assert!(codes(&errors).contains(&"KindsDoNotUnify"), "{errors:?}"); + // A value signature's written type must have kind `Type`, and the + // official `checkTypeKind` failure at an annotation is `ExpectedType`. + assert!(codes(&errors).contains(&"ExpectedType"), "{errors:?}"); } #[test] diff --git a/crates/psrs-kind/src/tests/foreign.rs b/crates/psrs-kind/src/tests/foreign.rs index 427bef11..4531d4bb 100644 --- a/crates/psrs-kind/src/tests/foreign.rs +++ b/crates/psrs-kind/src/tests/foreign.rs @@ -17,9 +17,11 @@ fn foreign_value_annotations_are_checked_at_their_declaring_module() { ), ]); let diagnostics = check_modules(&modules); + // A foreign value's annotation kind equation fails through the official + // `checkTypeKind`, which reports `ExpectedType` at the annotation. let conflicts = diagnostics .iter() - .filter(|error| error.code == "KindsDoNotUnify") + .filter(|error| error.code == "ExpectedType") .collect::>(); assert_eq!(conflicts.len(), 1, "{diagnostics:?}"); assert_eq!(conflicts[0].origin, ModuleId(1)); diff --git a/crates/psrs-kind/src/tests/program.rs b/crates/psrs-kind/src/tests/program.rs index 622a52cd..acd7f182 100644 --- a/crates/psrs-kind/src/tests/program.rs +++ b/crates/psrs-kind/src/tests/program.rs @@ -120,6 +120,64 @@ fn reports_a_referenced_declaration_with_no_checked_scheme() { assert!(crate::check_module(&modules[0], &environment).is_empty()); } +/// `failing/2542.purs`: a where binding's signature names a type variable that +/// no written `forall` quantifies — the enclosing declaration's annotation is a +/// synonym, and synonym expansion must not bring its binders into scope. +#[test] +fn reports_an_undefined_type_variable_in_a_local_signature() { + let errors = check( + "module Main where\n\ + type T = forall a. Array a\n\ + foo :: T\n\ + foo = bar where\n bar :: Array a\n bar = []\n", + ); + assert!( + codes(&errors).contains(&"UndefinedTypeVariable"), + "{errors:?}" + ); +} + +/// A variable the enclosing declaration's annotation quantifies is in scope in +/// local signatures, and a local signature's own `forall` binds for itself. +#[test] +fn written_scoped_type_variables_bind_in_local_annotations() { + check_ok( + "module Main where\n\ + foo :: forall a. Array a\n\ + foo = bar where\n bar :: Array a\n bar = []\n", + ); + check_ok( + "module Main where\n\ + foo :: Boolean\n\ + foo = bar where\n bar :: forall a. Array a\n bar = []\n", + ); +} + +/// `let` and guard bindings are subject to the same rule. +#[test] +fn checks_undefined_variables_in_let_and_guard_bindings() { + let errors = check( + "module Main where\n\ + foo = let\n bar :: Array a\n bar = []\nin bar\n", + ); + assert!( + codes(&errors).contains(&"UndefinedTypeVariable"), + "{errors:?}" + ); +} + +/// An annotation in an instance member sees the free variables written in the +/// instance head and its context. +#[test] +fn an_instance_member_sees_the_instance_head_free_variables() { + check_ok( + "module Main where\n\ + data Proxy a = Proxy\n\ + class C a f | a -> f where c :: Proxy f -> Proxy f\n\ + instance C a (Proxy a) where\n c p = f p where\n f :: Proxy (Proxy a) -> Proxy (Proxy a)\n f x = x\n", + ); +} + #[test] fn a_primitive_read_as_a_kind_denotes_itself() { use crate::{Kind, KindScope, KindState, denote_kind, primitive_kind, type_kind}; diff --git a/docs/design/frontend/type-system/kinds.md b/docs/design/frontend/type-system/kinds.md index d1ef957c..0193cb35 100644 --- a/docs/design/frontend/type-system/kinds.md +++ b/docs/design/frontend/type-system/kinds.md @@ -214,6 +214,35 @@ runs the kind check alongside the occurs, escape, and level rules, and a row tai solved during row unification keeps the kind its row admits through that same binding. +### Annotation positions follow the official check-site diagnostics + +The pass separates the two diagnostic origins kind checking has. An application's +arrow kind, a row's element kind, an instance head, and a synonym body against its +declared kind all fail through the kind unifier and report `KindsDoNotUnify`. A +*written type at a type-annotation position* — a value signature, an `x :: t` +ascription in an expression, a typed binder pattern, and a `where`/`let` binding's +signature — must have kind `Type`, and official `TypeChecker/Kinds.hs` solves that +one equation through `checkTypeKind`, whose failure handler reports `ExpectedType` +rather than the unifier's mismatch. The pass runs the same equation with the same +state at those positions only, so the two codes do not drift: `failing/1570.purs` +(a typed lambda binder with a partially applied constructor) and +`failing/KindStar.purs` (a value signature ending in an unsaturated constructor) +report `ExpectedType`, while `failing/TypeWildcards1.purs`-shaped kind equations +between two non-`Type` kinds still report `KindsDoNotUnify`. + +A local annotation's written type variables are also scoped here. The binders the +enclosing declaration's signature quantifies *as written* are in scope, as are a +local signature's own `forall` binders and, for instance members, the free +variables written in the instance head and its context; synonym expansion never +brings a binder into scope, which is the official `withScopedTypeVars` scoping and +the recorded #2542 rule. Any other named variable is `UndefinedTypeVariable` +before the kind is read, so `failing/2542.purs` (`bar :: Array a` under +`foo :: T`, with `T = forall a. Array a`) reports the code against the `a` the +synonym's expansion hid. A visible type application's argument is checked against +the kind of the quantifier it instantiates officially, and this pass cannot see +that kind yet, so it keeps the pre-existing `Type` solve there while the +new scope rule applies to the argument's variables the same way. + What remains, and what the next wave owns: - The well-scoped-quantification rule is not implemented. A scheme quantifies the kind @@ -240,6 +269,21 @@ What remains, and what the next wave owns: modules produced. `kind_of_type` over an `InferType` is not implemented in `psrs-kind`, because an inference type is not HIR: it lives in the type checker's `kind.rs` and reads the same solver. +- Two corpus cases in the M4 set still diverge at the kind stage, both anchored in + the polykind model, not in a diagnostic choice: + `failing/SkolemEscapeKinds.purs` and `failing/PolykindGeneralizationLet.purs`. + Officially the kind checker accepts both and the failures surface later — an + `EscapedSkolem` raised by `checkEscapedSkolems` over a type synonym body + (`SkolemEscapeKinds`), and a `TypesDoNotUnify` raised by term checking + (`PolykindGeneralizationLet`, `where` a top-level binding group of the same + three `Proxy :: _ ...` uses passes). Here the kind pass rejects + `PolykindGeneralizationLet` with `KindsDoNotUnify` because declaration + parameters' kinds are shared raw variables across use sites, so + `data F f a = F (f a)`'s field equation is solved against a use the + declaration never checked. The official acceptance is the annotation-based + board; measured 2026-10-18 on this tree, L3 is 40/48 (`UndefinedTypeVariable` + 4/4, `KindsDoNotUnify` 16/24) and L4 is 41/50 (`ExpectedType` 2/2, + `EscapedSkolem` 1/2) with the L2 failing board unchanged at 72/72. Consolidating `psrs-kind` into the type checker is now a consequence of packaging alone: kind checking's main consumer is still P5, and the crate split is not what From 298cc585e2c763655c18b1f70cf19fbd02e4414a Mon Sep 17 00:00:00 2001 From: biu Date: Sun, 18 Oct 2026 05:50:32 +0800 Subject: [PATCH 5/8] Report the official orphan instance rule at the common instance recorder MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `purs` rejects a local instance declaration whose module defines neither its class nor a type constructor covering one of the class's functional-dependency covering sets (`TypeChecker.typeCheckAll`, `findNonOrphanModules` and `checkOrphanInstance`). The head's covering-set modules are intersected, so a module that covers only some sets is still an orphan. The check runs after head synthesis — synonym resolution included — and before overlapping-instance checking, so an orphan reports exactly `OrphanInstance` and is not recorded: it can neither overlap with a visible instance nor submit a derived dictionary (the `derive instance` half never runs). The covering sets were moved into a shared fundeps module so the overlap check and the orphan check read one definition. All seven `OrphanInstance` corpus cases agree on the M5 board, and 3405's produced set is exactly [OrphanInstance] (measured 2026-10-18 with the annotations oracle). --- .../src/tests/deriving/diagnostics.rs | 5 +- crates/psrs-driver/src/tests/mod.rs | 1 + .../psrs-driver/src/tests/orphan_instances.rs | 165 ++++++++++++++++++ .../src/tests/wasi/classes/deriving/folds.rs | 12 +- .../src/tests/wasi/classes/deriving/mod.rs | 12 +- .../tests/wasi/classes/deriving/records.rs | 12 +- .../src/typecheck/classes/coherence.rs | 115 ++++++------ .../src/typecheck/classes/environment/mod.rs | 7 + .../src/typecheck/classes/fundeps/covering.rs | 70 ++++++++ .../src/typecheck/classes/fundeps/mod.rs | 2 + crates/psrs-typecheck/src/typecheck/error.rs | 6 + .../type-system/classes-and-evidence.md | 12 ++ 12 files changed, 350 insertions(+), 69 deletions(-) create mode 100644 crates/psrs-driver/src/tests/orphan_instances.rs create mode 100644 crates/psrs-typecheck/src/typecheck/classes/fundeps/covering.rs diff --git a/crates/psrs-driver/src/tests/deriving/diagnostics.rs b/crates/psrs-driver/src/tests/deriving/diagnostics.rs index c8959516..52949e88 100644 --- a/crates/psrs-driver/src/tests/deriving/diagnostics.rs +++ b/crates/psrs-driver/src/tests/deriving/diagnostics.rs @@ -182,10 +182,13 @@ fn fold_deriving_reports_missing_core_values_at_the_declaration() { #[test] fn deriving_rejects_non_constructor_heads_and_invalid_class_arity() { for (library, main, expected) in [ + // A class the deriving module does not own and a primitive head make + // the declaration an official orphan: `checkOrphanInstance` throws + // before the derivation runs, so the orphan code is the whole report. ( "module Data.Eq where\nclass Eq a where\n eq :: a -> a -> Boolean\n", "module Main where\nimport Data.Eq\nderive instance eqInt :: Eq Int\nmain = 0\n", - "ExpectedTypeConstructor", + "OrphanInstance", ), ( "module Data.Eq where\nclass Eq a b where\n eq :: a -> b -> Boolean\n", diff --git a/crates/psrs-driver/src/tests/mod.rs b/crates/psrs-driver/src/tests/mod.rs index 6b1d92fa..45268b8e 100644 --- a/crates/psrs-driver/src/tests/mod.rs +++ b/crates/psrs-driver/src/tests/mod.rs @@ -34,6 +34,7 @@ mod number_rounding; mod number_sqrt; mod number_trunc; mod operators; +mod orphan_instances; mod partial_application; mod primitive_foreign; mod record_storage; diff --git a/crates/psrs-driver/src/tests/orphan_instances.rs b/crates/psrs-driver/src/tests/orphan_instances.rs new file mode 100644 index 00000000..f9dcb638 --- /dev/null +++ b/crates/psrs-driver/src/tests/orphan_instances.rs @@ -0,0 +1,165 @@ +//! The official orphan instance rule, from `purs`'s +//! `TypeChecker.typeCheckAll` (`findNonOrphanModules` and +//! `checkOrphanInstance`): an instance declared in a module that defines +//! neither its class nor a type constructor covering one of the class's +//! functional-dependency covering sets is an orphan, and the official +//! `OrphanInstance` code is raised at the common instance recorder before the +//! instance is recorded, so it can neither overlap with another visible +//! instance nor submit a derived dictionary. + +#[test] +fn rejects_an_instance_whose_head_names_no_declared_type() { + // The class is foreign and the head argument is a primitive the declaring + // module does not own, so no covering set is covered by the declaring + // module. + let errors = crate::check_program(&[ + ("Library.purs", "module Library where\nclass C a where\n op :: a -> a\n"), + ( + "Main.purs", + "module Main where\nimport Library\ninstance cInt :: C Int where\n op a = a\nmain = 0\n", + ), + ]) + .expect_err("a foreign-class instance over a primitive argument is an orphan"); + assert!( + errors + .iter() + .any(|error| error.diagnostic.code == Some("OrphanInstance")), + "{errors:?}" + ); +} + +#[test] +fn accepts_an_instance_of_a_class_declared_in_the_same_module() { + // A module that declares its own class is never an orphan, whatever the + // head argument names. + crate::check_program(&[( + "Main.purs", + "module Main where\nclass C a where\n op :: a -> a\ninstance cInt :: C Int where\n op a = a\nmain = op 1\n", + )]) + .expect("a locally-declared class's instance is not an orphan"); +} + +#[test] +fn accepts_an_instance_covered_by_a_local_head_constructor() { + // The class is foreign, but the instance head's own type constructor is + // declared in the declaring module, which satisfies the class's only + // covering set. + crate::check_program(&[ + ("Library.purs", "module Library where\nclass C a where\n op :: a -> a\n"), + ( + "Main.purs", + "module Main where\nimport Library\ndata Local = Local\ninstance cLocal :: C Local where\n op a = a\nmain = 0\n", + ), + ]) + .expect("a locally-declared head constructor makes the instance non-orphan"); +} + +#[test] +fn rejects_a_nullary_foreign_class_instance() { + // A class with no parameters contributes no covering positions, so a + // foreign nullary instance is always an orphan. + let errors = crate::check_program(&[ + ( + "Library.purs", + "module Library where\nclass C where\n op :: Int\n", + ), + ( + "Main.purs", + "module Main where\nimport Library\ninstance c :: C where\n op = 1\nmain = 0\n", + ), + ]) + .expect_err("a foreign nullary class instance is an orphan"); + assert!( + errors + .iter() + .any(|error| error.diagnostic.code == Some("OrphanInstance")), + "{errors:?}" + ); +} + +#[test] +fn rejects_a_head_argument_that_names_no_module() { + // A head argument that is a decided literal names no declaring module, so + // it covers nothing — the official type-level `Symbol` shape. + let errors = crate::check_program(&[ + ( + "Library.purs", + "module Library where\nclass Foo (s :: Symbol) where\n foo :: String\n", + ), + ( + "Main.purs", + "module Main where\nimport Library\ninstance fooX :: Foo \"x\" where\n foo = \"\"\nmain = 0\n", + ), + ]) + .expect_err("a literal head argument covers no covering set"); + assert!( + errors + .iter() + .any(|error| error.diagnostic.code == Some("OrphanInstance")), + "{errors:?}" + ); +} + +#[test] +fn rejects_an_instance_outside_the_covering_set_intersection() { + // The official fundep shape: the class's dependencies give it two covering + // sets, and the declaring module covers one but not the other, so it is + // in no intersection — the intersection of covering-set modules is empty. + let errors = crate::check_program(&[ + ( + "Library.purs", + "module Library where\nclass C l r | l -> r, r -> l\ndata R = R\n", + ), + ( + "Main.purs", + "module Main where\nimport Library\ndata L = L\ninstance clr :: C L R\nmain = 0\n", + ), + ]) + .expect_err("a module that covers only one covering set declares an orphan"); + assert!( + errors + .iter() + .any(|error| error.diagnostic.code == Some("OrphanInstance")), + "{errors:?}" + ); +} + +#[test] +fn accepts_an_instance_covering_every_set_through_a_local_constructor() { + // The complement of the intersection rule: a locally-declared head + // constructor in every covering set keeps the instance non-orphan, even + // though the remaining arguments are foreign. + crate::check_program(&[ + ( + "Library.purs", + "module Library where\nclass C a b\ndata Foreign = Foreign\n", + ), + ( + "Main.purs", + "module Main where\nimport Library\ndata Local = Local\ninstance cab :: C Local Foreign\nmain = 0\n", + ), + ]) + .expect("a locally-declared constructor in the only covering set is not an orphan"); +} + +#[test] +fn an_orphan_derived_instance_reports_only_the_orphan_code() { + // A `derive instance` whose head, after synonym expansion, names a + // primitive type is an orphan before any derivation runs, mirroring the + // official throw order: the deriving half is never started, so the + // report set is exactly `OrphanInstance`. + let errors = crate::check_program(&[ + ("Data.Eq.purs", "module Data.Eq where\nclass Eq a where\n eq :: a -> a -> Boolean\n"), + ( + "Main.purs", + "module Main where\nimport Data.Eq\ntype Something = Int\nderive instance eqSomething :: Eq Something\nmain = 0\n", + ), + ]) + .expect_err("deriving over a foreign primitive type is an orphan"); + assert!( + errors + .iter() + .all(|error| error.diagnostic.code == Some("OrphanInstance")), + "an orphan must be rejected before the deriving half runs: {errors:?}" + ); +} diff --git a/crates/psrs-driver/src/tests/wasi/classes/deriving/folds.rs b/crates/psrs-driver/src/tests/wasi/classes/deriving/folds.rs index 6f1dce45..0bb21c40 100644 --- a/crates/psrs-driver/src/tests/wasi/classes/deriving/folds.rs +++ b/crates/psrs-driver/src/tests/wasi/classes/deriving/folds.rs @@ -6,6 +6,9 @@ fn derived_bifoldable_preserves_left_right_mapping_and_fold_order() { class Semigroup a where append :: a -> a -> a + +instance semigroupInt :: Semigroup Int where + append left right = intAdd left right "#; let monoid = r#"module Data.Monoid where @@ -13,6 +16,9 @@ import Data.Semigroup class Semigroup a <= Monoid a where mempty :: a + +instance monoidInt :: Monoid Int where + mempty = 0 "#; let foldable = r#"module Data.Bifoldable where @@ -29,12 +35,6 @@ import Data.Bifoldable import Data.Monoid import Data.Semigroup -instance semigroupInt :: Semigroup Int where - append left right = intAdd left right - -instance monoidInt :: Monoid Int where - mempty = 0 - data Box a b = Empty | Box { left :: a, right :: b, inert :: Int } derive instance bifoldableBox :: Bifoldable Box diff --git a/crates/psrs-driver/src/tests/wasi/classes/deriving/mod.rs b/crates/psrs-driver/src/tests/wasi/classes/deriving/mod.rs index 0cee778f..ee32105d 100644 --- a/crates/psrs-driver/src/tests/wasi/classes/deriving/mod.rs +++ b/crates/psrs-driver/src/tests/wasi/classes/deriving/mod.rs @@ -206,6 +206,9 @@ fn derived_foldable_executes_through_its_instances() { class Semigroup a where append :: a -> a -> a + +instance semigroupInt :: Semigroup Int where + append left right = intAdd left right "#; let monoid = r#"module Data.Monoid where @@ -213,6 +216,9 @@ import Data.Semigroup class Semigroup a <= Monoid a where mempty :: a + +instance monoidInt :: Monoid Int where + mempty = 0 "#; let foldable = r#"module Data.Foldable where @@ -229,12 +235,6 @@ import Data.Foldable import Data.Monoid import Data.Semigroup -instance semigroupInt :: Semigroup Int where - append left right = intAdd left right - -instance monoidInt :: Monoid Int where - mempty = 0 - data Box a = Box a derive instance foldableBox :: Foldable Box diff --git a/crates/psrs-driver/src/tests/wasi/classes/deriving/records.rs b/crates/psrs-driver/src/tests/wasi/classes/deriving/records.rs index b4ea283d..692dc948 100644 --- a/crates/psrs-driver/src/tests/wasi/classes/deriving/records.rs +++ b/crates/psrs-driver/src/tests/wasi/classes/deriving/records.rs @@ -50,6 +50,9 @@ fn derived_foldable_preserves_record_label_order_in_both_fold_directions() { class Semigroup a where append :: a -> a -> a + +instance semigroupInt :: Semigroup Int where + append left right = intAdd left right "#; let monoid = r#"module Data.Monoid where @@ -57,6 +60,9 @@ import Data.Semigroup class Semigroup a <= Monoid a where mempty :: a + +instance monoidInt :: Monoid Int where + mempty = 0 "#; let foldable = r#"module Data.Foldable where @@ -73,12 +79,6 @@ import Data.Foldable import Data.Monoid import Data.Semigroup -instance semigroupInt :: Semigroup Int where - append left right = intAdd left right - -instance monoidInt :: Monoid Int where - mempty = 0 - data Box a = Box { first :: a, last :: a, flag :: Boolean } derive instance foldableBox :: Foldable Box diff --git a/crates/psrs-typecheck/src/typecheck/classes/coherence.rs b/crates/psrs-typecheck/src/typecheck/classes/coherence.rs index 48040f37..bab7e33c 100644 --- a/crates/psrs-typecheck/src/typecheck/classes/coherence.rs +++ b/crates/psrs-typecheck/src/typecheck/classes/coherence.rs @@ -1,4 +1,5 @@ use super::super::*; +use super::fundeps::covering_sets; impl Checker { /// Checks visible instance declarations for overlaps, excluding branches @@ -76,61 +77,75 @@ fn collect_user_type_modules(ty: &InferType, modules: &mut HashSet Vec> { - if fundeps.is_empty() { - return vec![(0..parameter_count).collect()]; - } - let mut result: Vec> = Vec::new(); - enumerate_covering_sets(parameter_count, fundeps, 0, &mut Vec::new(), &mut result); - result -} - -fn enumerate_covering_sets( - parameter_count: usize, - fundeps: &[FundepInfo], - next: usize, - chosen: &mut Vec, - result: &mut Vec>, -) { - if dependency_closure(chosen, fundeps).len() == parameter_count { - if !result.iter().any(|cover| is_subset(cover, chosen)) { - result.push(chosen.clone()); - } - return; - } - let mut possible = chosen.clone(); - possible.extend(next..parameter_count); - if dependency_closure(&possible, fundeps).len() != parameter_count || next == parameter_count { - return; +/// The module that declares an argument's leftmost spine-head type +/// constructor: applications recurse into the function side, so an applied +/// constructor names its nominal head's module, while type variables and +/// decided literals name no module. This is `purs`'s `typeModule` inside +/// `TypeChecker.findNonOrphanModules`. +fn leftmost_head_module(ty: &InferType) -> Option { + match ty { + InferType::Constructor(TypeConstructor::User(type_id)) => Some(type_id.module), + InferType::Application(function, _) => leftmost_head_module(function), + _ => None, } - chosen.push(next); - enumerate_covering_sets(parameter_count, fundeps, next + 1, chosen, result); - chosen.pop(); - enumerate_covering_sets(parameter_count, fundeps, next + 1, chosen, result); -} - -fn is_subset(left: &[usize], right: &[usize]) -> bool { - left.iter().all(|index| right.contains(index)) } -fn dependency_closure(seed: &[usize], fundeps: &[FundepInfo]) -> HashSet { - let mut closure = seed.iter().copied().collect::>(); - loop { - let before = closure.len(); - for fundep in fundeps { - if fundep - .determining - .iter() - .all(|index| closure.contains(index)) - { - closure.extend(fundep.determined.iter().copied()); - } +impl Checker { + /// Reports the official orphan instance error for one local instance + /// declaration, under the rule `purs` implements in + /// `TypeChecker.typeCheckAll`: the declaring module is non-orphan when it + /// declares the instance's class, or when for *every* covering set of the + /// class's parameters at least one covered head argument's leftmost type + /// constructor is declared in the declaring module (`purs` intersects the + /// modules found through each covering set and checks its containment). + /// + /// `checkOrphanInstance` throws after head synthesis — synonym resolution + /// included — and before the instance joins the searchable environment, so + /// an orphan instance is rejected here and never recorded: it cannot + /// overlap with another visible instance or submit a derived dictionary, + /// exactly as the official throw aborts the remaining checks. + /// + /// Returns whether the instance was reported as an orphan. + pub(super) fn report_orphan_instance( + &mut self, + instance: &hir::InstanceDeclaration, + class: &ClassInfo, + head_arguments: &[InferType], + ) -> bool { + let declaring = self.env.module_id; + if instance.class_id.module == declaring { + return false; } - if closure.len() == before { - return closure; + let sets = covering_sets(class.parameters.len(), &class.fundeps); + // The declaring module is non-orphan when every covering set contains + // a covered argument whose leftmost head constructor it declares; the + // instance is an orphan only when no covering set does. + let is_orphan = !sets.iter().all(|set| { + set.iter().any(|&index| { + head_arguments + .get(index) + .and_then(leftmost_head_module) + .is_some_and(|module| module == declaring) + }) + }); + if !is_orphan { + return false; } + let class_name = self + .env + .type_names + .get(&instance.class_id) + .cloned() + .unwrap_or_else(|| format!("Class{}", instance.class_id.index)); + self.state.errors.push(TypeCheckError::new( + TypeCheckErrorKind::OrphanInstance, + instance.span, + format!( + "orphan instance of class `{class_name}`: neither the class nor a type \ + constructor covering its head is declared in this module" + ), + )); + true } } diff --git a/crates/psrs-typecheck/src/typecheck/classes/environment/mod.rs b/crates/psrs-typecheck/src/typecheck/classes/environment/mod.rs index 0e253ecc..b5813179 100644 --- a/crates/psrs-typecheck/src/typecheck/classes/environment/mod.rs +++ b/crates/psrs-typecheck/src/typecheck/classes/environment/mod.rs @@ -311,6 +311,13 @@ impl Checker { if local && !validate_head_shapes(self, &class, &head_arguments, instance.head.span) { return; } + // An orphan instance is rejected at the recorder and not recorded, so + // it can neither overlap with a visible instance nor submit a derived + // dictionary; the official throw aborts the remaining checks + // (`checkOrphanInstance` precedes `checkOverlappingInstance`). + if local && self.report_orphan_instance(instance, &class, &head_arguments) { + return; + } let mut context = Vec::with_capacity(instance.context.len()); let mut context_parameters = Vec::with_capacity(instance.context.len()); let mut valid = true; diff --git a/crates/psrs-typecheck/src/typecheck/classes/fundeps/covering.rs b/crates/psrs-typecheck/src/typecheck/classes/fundeps/covering.rs new file mode 100644 index 00000000..cb40b18e --- /dev/null +++ b/crates/psrs-typecheck/src/typecheck/classes/fundeps/covering.rs @@ -0,0 +1,70 @@ +//! The minimal covering sets a class's functional dependencies define. Both +//! the overlap check and the orphan check read them. + +use super::super::super::vocabulary::FundepInfo; +use std::collections::HashSet; + +/// Computes the minimal sets of class parameters that determine all parameters +/// under the class's functional dependencies. A class without dependencies has +/// one covering set over every parameter, mirroring the one covering set +/// `purs`'s `typeClassCoveringSets` records. +pub(in crate::typecheck::classes) fn covering_sets( + parameter_count: usize, + fundeps: &[FundepInfo], +) -> Vec> { + if fundeps.is_empty() { + return vec![(0..parameter_count).collect()]; + } + let mut result: Vec> = Vec::new(); + enumerate_covering_sets(parameter_count, fundeps, 0, &mut Vec::new(), &mut result); + result +} + +fn enumerate_covering_sets( + parameter_count: usize, + fundeps: &[FundepInfo], + next: usize, + chosen: &mut Vec, + result: &mut Vec>, +) { + if dependency_closure(chosen, fundeps).len() == parameter_count { + if !result.iter().any(|cover| is_subset(cover, chosen)) { + result.push(chosen.clone()); + } + return; + } + let mut possible = chosen.clone(); + possible.extend(next..parameter_count); + if dependency_closure(&possible, fundeps).len() != parameter_count || next == parameter_count { + return; + } + chosen.push(next); + enumerate_covering_sets(parameter_count, fundeps, next + 1, chosen, result); + chosen.pop(); + enumerate_covering_sets(parameter_count, fundeps, next + 1, chosen, result); +} + +fn is_subset(left: &[usize], right: &[usize]) -> bool { + left.iter().all(|index| right.contains(index)) +} + +/// Closes a seed of parameter positions over the dependencies: each dependency +/// whose determining positions are all present adds its determined ones. +fn dependency_closure(seed: &[usize], fundeps: &[FundepInfo]) -> HashSet { + let mut closure = seed.iter().copied().collect::>(); + loop { + let before = closure.len(); + for fundep in fundeps { + if fundep + .determining + .iter() + .all(|index| closure.contains(index)) + { + closure.extend(fundep.determined.iter().copied()); + } + } + if closure.len() == before { + return closure; + } + } +} diff --git a/crates/psrs-typecheck/src/typecheck/classes/fundeps/mod.rs b/crates/psrs-typecheck/src/typecheck/classes/fundeps/mod.rs index 5c04c4e3..a27c6542 100644 --- a/crates/psrs-typecheck/src/typecheck/classes/fundeps/mod.rs +++ b/crates/psrs-typecheck/src/typecheck/classes/fundeps/mod.rs @@ -1,8 +1,10 @@ use super::super::unify::substitute; use super::super::*; use std::collections::HashMap; +mod covering; mod support; +pub(super) use covering::covering_sets; use support::solution_uses_lexical_given; /// Functional-dependency improvement and ambiguity checking for wanted diff --git a/crates/psrs-typecheck/src/typecheck/error.rs b/crates/psrs-typecheck/src/typecheck/error.rs index 87d41ec2..bf0fae77 100644 --- a/crates/psrs-typecheck/src/typecheck/error.rs +++ b/crates/psrs-typecheck/src/typecheck/error.rs @@ -24,6 +24,11 @@ pub enum TypeCheckErrorKind { FundepConflict, /// More than one unrelated visible instance proves the same constraint. OverlappingInstances, + /// A local instance declares neither its class nor a type constructor that + /// covers one of the class's functional-dependency covering sets. `purs` + /// raises this in `TypeChecker.typeCheckAll` through + /// `findNonOrphanModules` and `checkOrphanInstance`. + OrphanInstance, /// A constraint still mentions variables that neither the result type nor /// the class's functional dependencies determine. AmbiguousConstraint, @@ -186,6 +191,7 @@ impl TypeCheckErrorKind { TypeCheckErrorKind::NoInstance => "NoInstanceFound", TypeCheckErrorKind::MissingInstanceMethod => "MissingClassMember", TypeCheckErrorKind::OverlappingInstances => "OverlappingInstances", + TypeCheckErrorKind::OrphanInstance => "OrphanInstance", TypeCheckErrorKind::AmbiguousConstraint => "AmbiguousTypeVariables", TypeCheckErrorKind::CannotGeneralizeRecursiveFunction => { "CannotGeneralizeRecursiveFunction" diff --git a/docs/design/frontend/type-system/classes-and-evidence.md b/docs/design/frontend/type-system/classes-and-evidence.md index 83ab68eb..634d4dc4 100644 --- a/docs/design/frontend/type-system/classes-and-evidence.md +++ b/docs/design/frontend/type-system/classes-and-evidence.md @@ -274,6 +274,18 @@ check, so the proof needs its own verified answer contract. See [primitives](pri for the dispatch and outcome contract and [D-04](../../D-04-suite-roadmap.md) for measured coverage. +The orphan rule from `TypeChecker.typeCheckAll` is implemented at the common +instance recorder: after an instance head is synthesized — synonym resolution +included — the declaring module is non-orphan exactly when it declares the +class, or when every covering set of the class parameters contains a covered +argument whose leftmost spine-head type constructor it declares. An orphan +instance reports `OrphanInstance` at that boundary and is not recorded, which +reproduces the official throw order: an orphan can neither join the overlap +check nor start its own derivation. All seven `OrphanInstance` corpus +cases agree on the M5 board (measured 2026-10-18 with the annotations oracle). +Instance-chain apartness beyond the recorder is +still tracked as future work above. + The parts that *are* reached now include what the previous revision of this note listed as missing. A declaration's scheme carries the constraints inference retained, so a signatureless declaration infers a qualified type — From fd7bf88ac971de04946f330f75c0051d12b2fa3d Mon Sep 17 00:00:00 2001 From: biu Date: Sun, 18 Oct 2026 05:50:45 +0800 Subject: [PATCH 6/8] Report duplicate type classes at the resolver's declaration registry --- .../psrs-driver/src/tests/declarations/mod.rs | 36 +++++++++++++++++++ crates/psrs-resolve/src/resolver/mod.rs | 28 ++++++++++++--- .../type-system/classes-and-evidence.md | 5 ++- 3 files changed, 63 insertions(+), 6 deletions(-) diff --git a/crates/psrs-driver/src/tests/declarations/mod.rs b/crates/psrs-driver/src/tests/declarations/mod.rs index 5b3693de..0dd803cb 100644 --- a/crates/psrs-driver/src/tests/declarations/mod.rs +++ b/crates/psrs-driver/src/tests/declarations/mod.rs @@ -55,6 +55,42 @@ fn reports_decl_conflict_between_a_class_and_a_type() { ); } +#[test] +fn reports_duplicate_type_class_for_two_classes_of_one_name() { + // Two class declarations sharing one name are the official + // `DuplicateTypeClass`, not the ordinary declaration conflict. + let source = "module Main where\nclass C\nclass C\n"; + let errors = check_program_lenient(&[("Main.purs", source)]).unwrap_err(); + let codes: Vec<_> = errors + .iter() + .filter_map(|error| error.diagnostic.code) + .collect(); + assert!( + codes.contains(&"DuplicateTypeClass") && !codes.contains(&"DeclConflict"), + "{codes:?}" + ); +} + +#[test] +fn still_reports_decl_conflict_when_a_class_meets_another_declaration() { + // Only a class meeting an earlier class is `DuplicateTypeClass`; a class + // name colliding with a data type, a synonym, or a constructor keeps the + // ordinary `DeclConflict` code. + for source in [ + "module Main where\nclass Fail\ndata Fail\n", + "module Main where\ndata Fail\nclass Fail\n", + "module Main where\ndata T = Fail\nclass Fail\n", + ] { + let errors = check_program_lenient(&[("Main.purs", source)]).unwrap_err(); + assert!( + errors + .iter() + .any(|error| error.diagnostic.code == Some("DeclConflict")), + "{source}: {errors:?}" + ); + } +} + #[test] fn imports_a_type_and_its_constructors_across_modules() { let library = "module Library where\ndata Maybe a = Nothing | Just a\n"; diff --git a/crates/psrs-resolve/src/resolver/mod.rs b/crates/psrs-resolve/src/resolver/mod.rs index f9719491..47ead328 100644 --- a/crates/psrs-resolve/src/resolver/mod.rs +++ b/crates/psrs-resolve/src/resolver/mod.rs @@ -44,6 +44,10 @@ pub enum ResolveErrorKind { TransitiveExportError, TransitiveDctorExportError, ExportConflict, + /// Two class declarations share one name, the official + /// `DuplicateTypeClass` error. Every other same-name type-declaration + /// collision stays a `DeclConflict`. + DuplicateTypeClass, ScopeConflict, DeclConflict, InvalidHir, @@ -58,6 +62,7 @@ impl ResolveErrorKind { Self::DuplicateLocalBinding => "OverlappingNamesInLet", Self::UnknownName | Self::UnknownTypeName => "UnknownName", Self::DuplicateModule => "DuplicateModule", + Self::DuplicateTypeClass => "DuplicateTypeClass", Self::CannotDefinePrimModules => "CannotDefinePrimModules", Self::ModuleNotFound => "ModuleNotFound", Self::CycleInModules => "CycleInModules", @@ -103,6 +108,9 @@ impl ResolveError { format!("the value `{name}` has been defined multiple times") } ResolveErrorKind::DuplicateModule => format!("duplicate module `{name}`"), + ResolveErrorKind::DuplicateTypeClass => { + format!("the type class `{name}` has already been declared") + } ResolveErrorKind::CannotDefinePrimModules => { format!("module `{name}` is in the reserved Prim namespace") } @@ -237,6 +245,10 @@ fn plan_type_declarations( let mut type_names = HashMap::new(); let mut opaque_types = HashSet::new(); let mut uppercase: HashSet = HashSet::new(); + // Type names already held by a class declaration, so a collision is + // classified: two classes sharing one name are the official + // `DuplicateTypeClass`, and any other pair stays a `DeclConflict`. + let mut class_held_names: HashSet = HashSet::new(); let mut next_symbol = first_symbol; for (index, declaration) in declarations.iter().enumerate() { @@ -264,11 +276,17 @@ fn plan_type_declarations( } if uppercase.contains(&name.text) { - errors.push(ResolveError::named( - ResolveErrorKind::DeclConflict, - name.text.clone(), - name.span, - )); + let kind = if matches!(declaration, ast::TypeDeclaration::Class(_)) + && class_held_names.contains(&name.text) + { + ResolveErrorKind::DuplicateTypeClass + } else { + ResolveErrorKind::DeclConflict + }; + errors.push(ResolveError::named(kind, name.text.clone(), name.span)); + } + if matches!(declaration, ast::TypeDeclaration::Class(_)) { + class_held_names.insert(name.text.clone()); } if matches!(declaration, ast::TypeDeclaration::Foreign(_)) { opaque_types.insert(id); diff --git a/docs/design/frontend/type-system/classes-and-evidence.md b/docs/design/frontend/type-system/classes-and-evidence.md index 634d4dc4..a4ac331a 100644 --- a/docs/design/frontend/type-system/classes-and-evidence.md +++ b/docs/design/frontend/type-system/classes-and-evidence.md @@ -283,7 +283,10 @@ instance reports `OrphanInstance` at that boundary and is not recorded, which reproduces the official throw order: an orphan can neither join the overlap check nor start its own derivation. All seven `OrphanInstance` corpus cases agree on the M5 board (measured 2026-10-18 with the annotations oracle). -Instance-chain apartness beyond the recorder is +The `DuplicateTypeClass` code is owned by name resolution, not by the class +environment: a class declaration whose name already belongs to a class in the +same module is `DuplicateTypeClass`, while every other same-name declaration +collision is `DeclConflict`. Instance-chain apartness beyond the recorder is still tracked as future work above. The parts that *are* reached now include what the previous revision of this note From 9a4c2e049e2db20f3a78bc39d8749c563e67f98e Mon Sep 17 00:00:00 2001 From: biu Date: Sun, 18 Oct 2026 13:17:50 +0800 Subject: [PATCH 7/8] Compute the official inclusion-minimal covering sets at the shared fundeps module The covering-set definition '298cc585' introduced at classes/fundeps/covering.rs enumerated every parameter subset whose dependency closure covers the class and kept those an order-dependent filter had not superseded, so locally-minimal-but-superset sets survived exactly the way the sibling slice recorded for the old coherence.rs copy (the corpus case NonOrphanInstanceFunDepExtra documents the official {{f, l}} while the enumeration also returned {f, l, r}). The official 'typeClassCoveringSets' is the inclusion-minimal reduction of the 'computeCoveringSets' frontier search. The frontier search that instance_head.rs carried as a reduced port now lives in covering.rs and produces those minimal sets for every consumer: the overlap check's apartness, the orphan rule's per-set coverage, and the determined-instance-head rule, whose fully determined arguments are officially the parameters standing in no covering set. One definition, no local copies. The orphan verdict itself is unchanged: a superset of a covered minimal set is covered, so minimal sets cannot orphan a legal instance that the supersets accepted; the overlap check must be re-measured instead, and OverlappingInstances stays 8/8, OrphanInstance 7/7, InvalidInstanceHead 7/7, CycleInTypeClassDeclaration 2/2 on the M5 board, and 3405's produced set stays exactly [OrphanInstance] (measured 2026-10-18 with the annotations oracle). Focused regression tests pin the two program shapes the L6 runtime board measured at risk: a foreign fundep class instance over locally declared heads is accepted and executes (NonOrphanInstanceFunDepExtra), and an export shadowing an unused import compiles and executes (NonConflictingExports). Both pass the runtime board per program. --- .../psrs-driver/src/tests/declarations/mod.rs | 26 +++ .../psrs-driver/src/tests/orphan_instances.rs | 35 ++++ .../src/typecheck/classes/coherence.rs | 3 +- .../classes/environment/instance_head.rs | 100 +-------- .../src/typecheck/classes/fundeps/covering.rs | 191 +++++++++++++----- .../src/typecheck/classes/fundeps/mod.rs | 2 +- .../type-system/classes-and-evidence.md | 10 +- 7 files changed, 222 insertions(+), 145 deletions(-) diff --git a/crates/psrs-driver/src/tests/declarations/mod.rs b/crates/psrs-driver/src/tests/declarations/mod.rs index 0dd803cb..7553cf0c 100644 --- a/crates/psrs-driver/src/tests/declarations/mod.rs +++ b/crates/psrs-driver/src/tests/declarations/mod.rs @@ -382,3 +382,29 @@ fn reports_a_scope_conflict_for_a_duplicated_qualifier() { .any(|error| error.diagnostic.code == Some("ScopeConflict")) ); } + +#[test] +fn an_export_shadowing_an_unused_import_conflicts_with_nothing() { + // The corpus shape `NonConflictingExports`: `Main (thing, main)` exports + // its own `thing` while `A`, imported but never used, also defines + // `thing`. The export refers to `Main.thing` only, so no export or scope + // conflict is reported, the program type checks, and `main` executes. + let a = "module A where\nthing :: Int\nthing = 1\n"; + let main = "module Main (thing, main) where\nimport Effect.Unsafe (unsafePerformEffect)\nimport Prelude\nimport A\nimport WASI.Console\nthing :: Int\nthing = 2\nmain = let ignored = unsafePerformEffect (log \"Done\") in 0\n"; + let sources = [("A.purs", a), ("Main.purs", main)]; + // Compiling includes resolution, so acceptance here covers the export + // resolution as well as the type check. + crate::compile_program_sources_with_prelude(&sources) + .expect("a local declaration shadows an unused import"); + let Some(output) = run_program_with_prelude_wasmtime(&sources) else { + eprintln!("skipping: wasmtime is not installed"); + return; + }; + assert!(output.status.success(), "the guest must run to completion"); + assert!( + String::from_utf8_lossy(&output.stdout) + .trim_end() + .ends_with("Done"), + "the program must execute with its own export in place: {output:?}" + ); +} diff --git a/crates/psrs-driver/src/tests/orphan_instances.rs b/crates/psrs-driver/src/tests/orphan_instances.rs index f9dcb638..b6faa057 100644 --- a/crates/psrs-driver/src/tests/orphan_instances.rs +++ b/crates/psrs-driver/src/tests/orphan_instances.rs @@ -163,3 +163,38 @@ fn an_orphan_derived_instance_reports_only_the_orphan_code() { "an orphan must be rejected before the deriving half runs: {errors:?}" ); } + +#[test] +fn accepts_and_runs_a_foreign_fundep_class_instance_over_local_heads() { + // The corpus shape `NonOrphanInstanceFunDepExtra`: the class + // `C f l r | l -> r` and `L` live in `Lib`, while `Main` declares `F` and + // `R` and the instance. The class's one official covering set `{f, l}` + // contains the declaring module's `F`, so the instance is accepted and + // recorded, and `main` executes with it. + let sources = [ + ( + "Lib.purs", + "module Lib where\nclass C f l r | l -> r\ndata L\n", + ), + ( + "Main.purs", + "module Main where\nimport Effect.Unsafe (unsafePerformEffect)\nimport Prelude\nimport Lib\nimport WASI.Console\ndata F\ndata R\ninstance cflr :: C F L R\nmain = let ignored = unsafePerformEffect (log \"Done\") in 0\n", + ), + ]; + // Compiling runs the whole pipeline, whose typechecker applies the orphan + // rule at the common instance recorder; acceptance means the instance was + // recorded, not merely parsed. + crate::compile_program_sources_with_prelude(&sources) + .expect("a declaring module that covers the class's covering set is not an orphan"); + let Some(output) = super::run_program_with_prelude_wasmtime(&sources) else { + eprintln!("skipping: wasmtime is not installed"); + return; + }; + assert!(output.status.success(), "the guest must run to completion"); + assert!( + String::from_utf8_lossy(&output.stdout) + .trim_end() + .ends_with("Done"), + "the program must execute with the instance recorded: {output:?}" + ); +} diff --git a/crates/psrs-typecheck/src/typecheck/classes/coherence.rs b/crates/psrs-typecheck/src/typecheck/classes/coherence.rs index bab7e33c..d97fe5bd 100644 --- a/crates/psrs-typecheck/src/typecheck/classes/coherence.rs +++ b/crates/psrs-typecheck/src/typecheck/classes/coherence.rs @@ -1,5 +1,6 @@ use super::super::*; use super::fundeps::covering_sets; +use std::collections::{BTreeSet, HashSet}; impl Checker { /// Checks visible instance declarations for overlaps, excluding branches @@ -150,7 +151,7 @@ impl Checker { } fn instances_are_apart( - covering_sets: &[Vec], + covering_sets: &BTreeSet>, left: &[InferType], right: &[InferType], ) -> bool { diff --git a/crates/psrs-typecheck/src/typecheck/classes/environment/instance_head.rs b/crates/psrs-typecheck/src/typecheck/classes/environment/instance_head.rs index a0a3870d..3c2bc99f 100644 --- a/crates/psrs-typecheck/src/typecheck/classes/environment/instance_head.rs +++ b/crates/psrs-typecheck/src/typecheck/classes/environment/instance_head.rs @@ -13,8 +13,6 @@ //! the head's shape, applied per argument after synonyms expand. use super::super::super::*; -use std::collections::BTreeMap; -use std::collections::BTreeSet; /// Applies the head rule to one instance's elaborated head arguments. The /// return is `false` when an argument rejects, with the diagnostic already @@ -86,100 +84,20 @@ pub(in crate::typecheck) fn valid_instance_head_argument( /// The argument positions of a class that no covering set contains: official /// `typeClassDeterminedArguments` in `Environment.hs`. /// -/// A covering set is an inclusion-minimal set of argument positions from which -/// every remaining argument follows through the class's functional -/// dependencies; an argument is fully determined exactly when it stands in no -/// covering set. This is a port of `computeCoveringSets`, reduced to the -/// determined set. The frontier starts at the full parameter set, and each -/// still-applicable dependency removes one parameter it determines — including -/// parameters that dependency no longer sees in its determining positions — -/// until nothing reduces any set further. An argument that ends up needed by -/// every covering set is one the dependencies can never pin down, so it must -/// be a selectable part of the head. +/// Officially the determined set falls out of `computeCoveringSets`: +/// `determinedArgs = argumentIndices S.\\ fold coveringSets`, so this derives +/// it from the one shared covering-sets definition in `classes::fundeps` +/// rather than re-running the frontier search here. An argument that ends up +/// needed by every covering set is one the dependencies can never pin down, +/// so it must be a selectable part of the head. pub(in crate::typecheck) fn determined_fundep_arguments( parameter_count: usize, fundeps: &[FundepInfo], ) -> HashSet { - // Without dependencies every argument is needed: the only covering set is - // the full parameter list, and no argument is fully determined. - if fundeps.is_empty() { - return HashSet::new(); - } - // The determined parameter each dependency can remove next, paired with - // the determining sets it offers. Several dependencies may determine the - // same parameter, so the positions accumulate lists like the official - // `M.fromListWith (<>)` does. - let initial = fundeps - .iter() - .flat_map(|fundep| { - fundep.determined.iter().map(|&target| { - ( - target, - fundep.determining.iter().copied().collect::>(), - ) - }) - }) - .fold( - BTreeMap::new(), - |mut edges: BTreeMap>>, (target, sources)| { - edges.entry(target).or_default().push(sources); - edges - }, - ); - let all = (0..parameter_count).collect::>(); - // The frontier: a needed set paired with its applicable dependencies. - // The official frontier is keyed by the needed set and merges repeated - // arrivals keeping the first, so the same entry does here. - let mut frontier: BTreeMap, BTreeMap>>> = - BTreeMap::from([(all, initial)]); - let mut covering_sets: HashSet> = HashSet::new(); - while let Some((needed, in_edges)) = frontier.pop_first() { - if in_edges.is_empty() { - covering_sets.insert(needed); - continue; - } - let source_positions = in_edges - .values() - .flatten() - .flatten() - .copied() - .collect::>(); - // A dependency that determines an argument no surviving dependency - // uses is acyclic: removing it cannot spur other removals, so trying - // only it is what the official search prefers. - let acyclic = in_edges - .keys() - .find(|&y| !source_positions.contains(y)) - .copied(); - let candidates = match acyclic { - Some(y) => vec![y], - None => in_edges.keys().copied().collect(), - }; - for y in candidates { - let mut next_needed = needed.clone(); - next_needed.remove(&y); - let mut next_edges = in_edges.clone(); - next_edges.remove(&y); - if acyclic.is_none() { - for sources in next_edges.values_mut() { - sources.retain(|source| !source.contains(&y)); - } - next_edges.retain(|_, sources| !sources.is_empty()); - } - frontier.entry(next_needed).or_insert(next_edges); - } - } - // Reduce to the inclusion-minimal covering sets, then an argument is - // determined when no covering set contains it. - let minimal = covering_sets.iter().filter(|set| { - !covering_sets - .iter() - .any(|other| other.len() < set.len() && other.is_subset(set)) - }); let mut determined: HashSet = (0..parameter_count).collect(); - for set in minimal { - for position in set.iter() { - determined.remove(position); + for set in super::super::fundeps::covering_sets(parameter_count, fundeps) { + for position in set { + determined.remove(&position); } } determined diff --git a/crates/psrs-typecheck/src/typecheck/classes/fundeps/covering.rs b/crates/psrs-typecheck/src/typecheck/classes/fundeps/covering.rs index cb40b18e..fe3790d3 100644 --- a/crates/psrs-typecheck/src/typecheck/classes/fundeps/covering.rs +++ b/crates/psrs-typecheck/src/typecheck/classes/fundeps/covering.rs @@ -1,70 +1,161 @@ -//! The minimal covering sets a class's functional dependencies define. Both -//! the overlap check and the orphan check read them. +//! The inclusion-minimal covering sets a class's functional dependencies +//! define, official `typeClassCoveringSets` from `Environment.computeCoveringSets`. +//! Both the overlap check and the orphan check read them, and the +//! determined-instance-head rule derives its fully-determined arguments from +//! them, so this is the one definition of the notion in the typechecker. use super::super::super::vocabulary::FundepInfo; -use std::collections::HashSet; +use std::collections::{BTreeMap, BTreeSet}; /// Computes the minimal sets of class parameters that determine all parameters /// under the class's functional dependencies. A class without dependencies has /// one covering set over every parameter, mirroring the one covering set /// `purs`'s `typeClassCoveringSets` records. -pub(in crate::typecheck::classes) fn covering_sets( +/// +/// The search is the official frontier: start from the full parameter set, +/// which is known to cover everything, and repeatedly remove a parameter some +/// still-applicable dependency determines, dropping the dependencies that +/// stop applying, until a needed set no dependency can reduce remains. Each +/// recorded set is locally minimal (no fundep reduces it), but frontiers can +/// still reach sets that contain one another, so the result is finally reduced +/// to the inclusion-minimal sets exactly as `computeCoveringSets` does. +pub(in crate::typecheck) fn covering_sets( parameter_count: usize, fundeps: &[FundepInfo], -) -> Vec> { +) -> BTreeSet> { + // Without dependencies no fundep reduces the full parameter set, so the + // one covering set is every parameter. + let all = (0..parameter_count).collect::>(); + let mut locally_minimal = BTreeSet::from([all.clone()]); if fundeps.is_empty() { - return vec![(0..parameter_count).collect()]; + return locally_minimal; } - let mut result: Vec> = Vec::new(); - enumerate_covering_sets(parameter_count, fundeps, 0, &mut Vec::new(), &mut result); - result + // The frontier: a needed set paired, for each determined parameter it can + // still remove, with the determining sets its dependencies offer. Several + // dependencies may determine the same parameter, so the positions + // accumulate lists like the official `M.fromListWith (<>)` does. + let initial = fundeps + .iter() + .flat_map(|fundep| { + fundep.determined.iter().map(|&target| { + ( + target, + fundep.determining.iter().copied().collect::>(), + ) + }) + }) + .fold( + BTreeMap::new(), + |mut edges: BTreeMap>>, (target, sources)| { + edges.entry(target).or_default().push(sources); + edges + }, + ); + // The official frontier is keyed by the needed set and merges repeated + // arrivals keeping the first, so the same entry does here. + let mut frontier: BTreeMap, BTreeMap>>> = + BTreeMap::from([(all, initial)]); + while let Some((needed, in_edges)) = frontier.pop_first() { + if in_edges.is_empty() { + locally_minimal.insert(needed); + continue; + } + let source_positions = in_edges + .values() + .flatten() + .flatten() + .copied() + .collect::>(); + // A dependency that determines an argument no surviving dependency + // uses is acyclic: removing it cannot spur other removals, so trying + // only it is what the official search prefers. + let acyclic = in_edges + .keys() + .find(|&y| !source_positions.contains(y)) + .copied(); + let candidates = match acyclic { + Some(y) => vec![y], + None => in_edges.keys().copied().collect(), + }; + for y in candidates { + let mut next_needed = needed.clone(); + next_needed.remove(&y); + let mut next_edges = in_edges.clone(); + next_edges.remove(&y); + if acyclic.is_none() { + for sources in next_edges.values_mut() { + sources.retain(|source| !source.contains(&y)); + } + next_edges.retain(|_, sources| !sources.is_empty()); + } + frontier.entry(next_needed).or_insert(next_edges); + } + } + // Reduce to the inclusion-minimal sets: a set another recorded set + // properly contains is not minimal. + locally_minimal + .iter() + .filter(|set| { + !locally_minimal + .iter() + .any(|other| other.len() < set.len() && other.is_subset(set)) + }) + .cloned() + .collect() } -fn enumerate_covering_sets( - parameter_count: usize, - fundeps: &[FundepInfo], - next: usize, - chosen: &mut Vec, - result: &mut Vec>, -) { - if dependency_closure(chosen, fundeps).len() == parameter_count { - if !result.iter().any(|cover| is_subset(cover, chosen)) { - result.push(chosen.clone()); +#[cfg(test)] +mod tests { + use super::*; + + /// Builds one fundep from parameter positions. + fn fundep(determining: &[usize], determined: &[usize]) -> FundepInfo { + FundepInfo { + determining: determining.to_vec(), + determined: determined.to_vec(), } - return; } - let mut possible = chosen.clone(); - possible.extend(next..parameter_count); - if dependency_closure(&possible, fundeps).len() != parameter_count || next == parameter_count { - return; + + #[test] + fn a_dependency_through_an_extra_parameter_covers_the_pair_it_names() { + // The corpus shape `NonOrphanInstanceFunDepExtra`: + // `class C f l r | l -> r`. The official + // `typeClassCoveringSets` records exactly `{{f, l}}` (the comment in + // the corpus case's `Lib.purs` states this), so the determined third + // parameter must not appear and the full parameter set must not be + // kept as a superset of `{f, l}`. + let sets = covering_sets(3, &[fundep(&[1], &[2])]); + assert_eq!(sets, BTreeSet::from([BTreeSet::from([0, 1])])); + } + + #[test] + fn a_class_without_dependencies_covers_every_parameter_once() { + let sets = covering_sets(3, &[]); + assert_eq!(sets, BTreeSet::from([BTreeSet::from([0, 1, 2])])); } - chosen.push(next); - enumerate_covering_sets(parameter_count, fundeps, next + 1, chosen, result); - chosen.pop(); - enumerate_covering_sets(parameter_count, fundeps, next + 1, chosen, result); -} -fn is_subset(left: &[usize], right: &[usize]) -> bool { - left.iter().all(|index| right.contains(index)) -} + #[test] + fn a_mutual_cycle_leaves_each_cycle_member_as_its_own_covering_set() { + // The official `makeTypeClassData` example: + // `class C a b c | a -> b, b -> a, b -> c`. The `a`/`b` cycle makes + // each of them cover everything on its own, and `c` is fully + // determined, so the minimal sets are `{{a}, {b}}`. + let sets = covering_sets( + 3, + &[fundep(&[0], &[1]), fundep(&[1], &[0]), fundep(&[1], &[2])], + ); + assert_eq!( + sets, + BTreeSet::from([BTreeSet::from([0]), BTreeSet::from([1])]) + ); + } -/// Closes a seed of parameter positions over the dependencies: each dependency -/// whose determining positions are all present adds its determined ones. -fn dependency_closure(seed: &[usize], fundeps: &[FundepInfo]) -> HashSet { - let mut closure = seed.iter().copied().collect::>(); - loop { - let before = closure.len(); - for fundep in fundeps { - if fundep - .determining - .iter() - .all(|index| closure.contains(index)) - { - closure.extend(fundep.determined.iter().copied()); - } - } - if closure.len() == before { - return closure; - } + #[test] + fn a_chained_dependency_collapses_to_the_head_of_the_chain() { + // `class C a b c | a -> b, b -> c`: `a` alone determines both, and the + // supersets `{a, b}` and `{a, b, c}` the enumeration passes through + // are not minimal. + let sets = covering_sets(3, &[fundep(&[0], &[1]), fundep(&[1], &[2])]); + assert_eq!(sets, BTreeSet::from([BTreeSet::from([0])])); } } diff --git a/crates/psrs-typecheck/src/typecheck/classes/fundeps/mod.rs b/crates/psrs-typecheck/src/typecheck/classes/fundeps/mod.rs index a27c6542..b7c712ba 100644 --- a/crates/psrs-typecheck/src/typecheck/classes/fundeps/mod.rs +++ b/crates/psrs-typecheck/src/typecheck/classes/fundeps/mod.rs @@ -4,7 +4,7 @@ use std::collections::HashMap; mod covering; mod support; -pub(super) use covering::covering_sets; +pub(in crate::typecheck) use covering::covering_sets; use support::solution_uses_lexical_given; /// Functional-dependency improvement and ambiguity checking for wanted diff --git a/docs/design/frontend/type-system/classes-and-evidence.md b/docs/design/frontend/type-system/classes-and-evidence.md index a4ac331a..a12e0b07 100644 --- a/docs/design/frontend/type-system/classes-and-evidence.md +++ b/docs/design/frontend/type-system/classes-and-evidence.md @@ -281,7 +281,12 @@ class, or when every covering set of the class parameters contains a covered argument whose leftmost spine-head type constructor it declares. An orphan instance reports `OrphanInstance` at that boundary and is not recorded, which reproduces the official throw order: an orphan can neither join the overlap -check nor start its own derivation. All seven `OrphanInstance` corpus +check nor start its own derivation. The covering sets are the official +inclusion-minimal `typeClassCoveringSets`, computed once at +`classes/fundeps/covering.rs` by the `computeCoveringSets` frontier search and +read by the overlap check, the orphan check, and the determined-head rule; an +enumeration that also kept covering supersets would be order-dependent and +cannot replace it. All seven `OrphanInstance` corpus cases agree on the M5 board (measured 2026-10-18 with the annotations oracle). The `DuplicateTypeClass` code is owned by name resolution, not by the class environment: a class declaration whose name already belongs to a class in the @@ -314,7 +319,8 @@ type-level literal, a type constructor, or a constructor or function application over those, and a row argument is legal only where the class's functional dependencies fully determine its position. The fully determined positions are official `typeClassDeterminedArguments`: the arguments standing -in no inclusion-minimal covering set, ported from `computeCoveringSets`, so a +in no inclusion-minimal covering set, derived from the shared +`computeCoveringSets` result at `classes/fundeps/covering.rs`, so a parameter determined only by an argument it itself determines is not determined and official record helpers that place a closed record in a determined parameter keep compiling. Every trigger — a wildcard (`TypeWildcards3.purs`), From fdb85717a76685d9ba2da51acea85b877175628a Mon Sep 17 00:00:00 2001 From: biu Date: Sun, 18 Oct 2026 13:43:03 +0800 Subject: [PATCH 8/8] Record the 2026-10-18 instance-slice scoreboard remeasurement --- README.md | 6 +-- docs/design/D-04-suite-roadmap.md | 49 ++++++++++++++----- .../runtime-program-scoreboard.md | 36 ++++++++++++++ 3 files changed, 76 insertions(+), 15 deletions(-) diff --git a/README.md b/README.md index 18ae5026..015838f3 100644 --- a/README.md +++ b/README.md @@ -51,9 +51,9 @@ what remains in each layer. | --- | --- | --- | | L0/L1 lexing, layout, parsing | 904/908 | non-FFI `layout`, `passing`, `failing`, `warning` files; the four differences are recorded DEC-16 intentional differences | | L2 resolution | 72/72 failing, 403/413 passing | official `errorCode`s; 6 passing files stop at P3 and 4 at P0; no harness blockers | -| L3 kinds | 39/48 failing | official kind `errorCode`s | -| L4 types | 39/50 failing | official `errorCode`s | -| L5 classes | 81/97 failing | official `errorCode`s, measured 2026-10-17 | +| L3 kinds | 44/48 failing | official kind `errorCode`s; measured 2026-10-18 | +| L4 types | 41/50 failing | official `errorCode`s; `ExpectedType` 2/2 since the annotation-position rule | +| L5 classes | 98/99 failing | official `errorCode`s; only `ClassHeadNoVTA3` (#123) remains; measured 2026-10-18 | | L6/M7 runtime | 287/340 programs | all exit 0; 53 do not agree; 74 support files remain program inputs, 25 FFI groups excluded | | M8 warnings, optimization | not measured | no scoreboard exists | diff --git a/docs/design/D-04-suite-roadmap.md b/docs/design/D-04-suite-roadmap.md index 0f0c2399..123643fc 100644 --- a/docs/design/D-04-suite-roadmap.md +++ b/docs/design/D-04-suite-roadmap.md @@ -448,7 +448,9 @@ environment, which owns `ClassInstanceArityMismatch`. The driver exposes a lenient kind check and the `l3` scoreboard; the scoreboard also runs against the vendored corpus without `purs`. -**Measured current result (2026-10-04, remeasured with the full boards):** M3 +**Measured current result (2026-10-18, after the instance and diagnostic slices, annotations oracle, vendored corpus):** **44/48**. Per code: `CycleInKindDeclaration` 2/2, `InfiniteKind` 2/2, `CycleInTypeSynonym` 4/4, `UndefinedTypeVariable` 4/4, `PartiallyAppliedSynonym` 12/12, and `KindsDoNotUnify` 20/24. The cross-module instance-head kind check (`004de7ba`, `psrs-kind`) checks an instance head against its class's checked kind scheme whether the class is declared here or imported, and four cases moved from no-diagnostic to agreement: `FoldableInstance1/2/3` and `NewtypeInstance6`. The local-annotation scope rule (`56fe3cda`) gives `2542.purs` its `UndefinedTypeVariable`. The four remaining mismatches are the polykind/expression-kind machinery of #100; `CoercibleKindMismatch`'s kind verdict now exists at the constraint-solver layer (`54d69f92`) but the kind board's entry point never runs the solver, so its row stays until the board grows that entry point or the case moves to the layer that owns it. + +**Checkpoint (2026-10-04, remeasured with the full boards):** M3 failing agreement is **39/48**. Per code: `CycleInKindDeclaration` 2/2, `InfiniteKind` 2/2, `CycleInTypeSynonym` 4/4, `UndefinedTypeVariable` 3/4, `PartiallyAppliedSynonym` 12/12, and `KindsDoNotUnify` 16/24. The scoreboard @@ -492,7 +494,9 @@ measurable until Phase 3 provides those modules. - **Acceptance:** Agreement on the `errorCode`s above. - **Prerequisite:** M3 and M6. -**Measured current result (2026-10-04, remeasured with the full boards):** +**Measured current result (2026-10-18, after the instance and diagnostic slices):** **41/50** failing cases agree; `ExpectedType` is now 2/2 (`1570.purs`, `KindStar.purs`) through the official annotation-position rule (`56fe3cda`: value signatures and local ascriptions run `checkTypeKind`'s kind equation at exactly the two official sites, so an annotation whose written type does not have kind `Type` reports `ExpectedType` instead of `KindsDoNotUnify`). The nine remaining mismatches decompose into: six `Coercible` cases reported as `NoInstanceFound` (the FE-16 `Proof` verification contract), `PolykindGeneralizationLet` and `SkolemEscapeKinds` (both are the polykind/quantified-kind representation boundary, recorded with evidence in the kinds design document), and `VisibleTypeApplications1` (#123). + +**Checkpoint (2026-10-04, remeasured with the full boards):** **39/50** failing cases agree. The scoreboard's aggregate and per-code counts disagree by one case, so this remeasurement does not publish a per-code decomposition. `HoleInferredType` has no mapped kind and contributes no case. @@ -599,7 +603,28 @@ obligation to FE-13, and accepted mismatches still need type-checking fixes. - **Acceptance:** Agreement on the `errorCode`s above. - **Prerequisite:** M4. -**Measured current result (2026-10-17, `7dd45e4b` plus the shared coverage and Partial slice, annotations oracle, vendored corpus):** **81/97** +**Measured current result (2026-10-18, after the instance and diagnostic slices, annotations oracle, vendored corpus):** **98/99** +failing cases agree. Per-code agreement is `OverlappingInstances` 8/8, +`NoInstanceFound` 52/53, `MissingClassMember` 2/2, +`InvalidNewtypeInstance` 6/6, `InvalidInstanceHead` 7/7, +`DuplicateInstance` 1/1, `ClassInstanceArityMismatch` 4/4, and +`CannotDeriveInvalidConstructorArg` 7/7, now joined by `OrphanInstance` 7/7 +(`298cc585`: an instance is an orphan when its module declares neither the +class nor a type constructor covering every official covering set; the check +runs after head synthesis and before recording, so an orphan instance can +neither overlap nor derive), `DuplicateTypeClass` 1/1 (`fd7bf88a`: the +resolver's declaration conflict distinguishes two classes with one name from +`DeclConflict`), `PossiblyInfiniteInstance` 1/1 (`4a078b95`: the solver's +work-bound exhaustion is the official diagnostic instead of a silent fall +through to `NoInstanceFound`), and `CycleInTypeClassDeclaration` 2/2 +(`4a078b95` mapped the existing superclass-cycle check). The denominator grew +from 97 to 99 because those two cycle cases left the blocked rows. The only +remaining mismatch is `ClassHeadNoVTA3.purs` (#123's visible type application +on a class-method head). The shared `covering_sets` are now the official +inclusion-minimal computation (`9a4c2e04`), shared by the overlap check and +the orphan check. + +**Checkpoint (2026-10-17, `7dd45e4b` plus the shared coverage and Partial slice, annotations oracle, vendored corpus):** **81/97** failing cases agree. Per-code agreement is `OverlappingInstances` 8/8, `NoInstanceFound` 52/53, `MissingClassMember` 2/2, `InvalidNewtypeInstance` 6/6, `InvalidInstanceHead` 1/7, @@ -1037,8 +1062,8 @@ concrete slice issues as sub-issues; this table is the index. | 0 | [#80](https://github.com/biuld/purescript-rs/issues/80) Lexer and layout agreement | `failing/2434.purs`, `layout/Commas.purs`, `layout/CaseGuards.purs` | Self-contained parse agreement. L1 is measured at 904/908; the four remaining cases are the DEC-16 intentional differences. String values follow [DEC-16](../decision/DEC-16-scalar-strings-and-utf8-storage.md); preserving lone UTF-16 surrogates is not a remaining gate. | | 1 | [#74](https://github.com/biuld/purescript-rs/issues/74) Make every gate measurable | [#81](https://github.com/biuld/purescript-rs/issues/81) official `errorCode` mapping, [#82](https://github.com/biuld/purescript-rs/issues/82) lenient type check and L4/L5 scoreboards, [#83](https://github.com/biuld/purescript-rs/issues/83) harness module path, [#93](https://github.com/biuld/purescript-rs/issues/93) runtime scoreboard | Nothing else can be verified until L4, L5, L6/M7, and M8-W report numbers. Changes no user-visible behavior. | | 2 | [#75](https://github.com/biuld/purescript-rs/issues/75) Frontend surface lowering — **complete** | [#84](https://github.com/biuld/purescript-rs/issues/84) ascription, [#85](https://github.com/biuld/purescript-rs/issues/85) patterns, [#86](https://github.com/biuld/purescript-rs/issues/86) operator aliases, [#87](https://github.com/biuld/purescript-rs/issues/87) type wildcards and rows, [#88](https://github.com/biuld/purescript-rs/issues/88) guards and multi-scrutinee `case`, [#89](https://github.com/biuld/purescript-rs/issues/89) `Prim` and unary minus, [#90](https://github.com/biuld/purescript-rs/issues/90) instance resolution | **No `passing` file stops in surface lowering.** From the 61-case `5298aad` baseline, #88 moved 22 past P2, the 34 fixed pattern paths plus 22 type, kind, instance, and declaration forms brought it to 5, and [#87](https://github.com/biuld/purescript-rs/pull/122) removed the last five. All six slices are `Done`. | -| 3 | [#76](https://github.com/biuld/purescript-rs/issues/76) Standard library — **next** | [#94](https://github.com/biuld/purescript-rs/issues/94) `Prelude` (77 measured after the `logShow` slice: the 7 cases that stopped on `logShow` stop instead on a `Prelude` name #94 also owns), [#95](https://github.com/biuld/purescript-rs/issues/95) `Effect`/`Effect.Console`/`Test.Assert` (305), [#96](https://github.com/biuld/purescript-rs/issues/96) `Proxy`/`Partial.Unsafe` (17), [#124](https://github.com/biuld/purescript-rs/issues/124) the `Data` modules no slice owned (27) | **342 of the 354** files L2 originally could not resolve were blocked on a missing library module. #95's first slice landed `Effect` and `Effect.Console`, dropping that to **83** and `passing` resolution from 59/413 to **199/413**; its second slice landed the `unit` value and `Test.Assert`, dropping the missing-module count to **62** and `passing` resolution to **209/413**. #94's first slice then landed `Data.Function` and the `$`/`#` operators, taking resolution to **225/413** and the missing-module count to **61**; its next slice landed `Data.Semigroup` and `<>`, taking resolution to **235/413**. `Eq`, `Ord`, and `Semiring` then landed with the intrinsic layer. The `Show` slice, measured on that master, moves resolution from 245/413 to **253/413**. `Data.Monoid` and `Data.Foldable`, measured independently on `6f66524` before `Show`, leave lenient resolution at **245/413** and move the compile-path missing-module count from 57 to 55. The figures were measured independently on `6f66524` and are not additive. The `Data.Tuple` slice, re-measured with the L2 scoreboard on `6f66524`, leaves resolution at **245/413** and moves the missing-module count from 57 to **56**, with other P3 blockers from 107 to **108**. That measurement is independent of the Show and Foldable figures and is not additive with them. Tuple's row said `logShow` and `assertEqual` were still waiting on the `Show`/`Eq` class surface, and that the GitHub `Corpus cases` field records the measured count; Show later recorded that the classes are declared and that the field was not written. What #95 still owns is `assertEqual` and `assertEqual'`; `logShow` has since landed as `log` of `show`, taking resolution to **270/413**. Depends on Phase 2, now complete: the library itself uses ascriptions, guards, sections, and instances. #94 measures 0 by first blocking stage only because `stdlib/lib/Prelude.purs` resolves; its missing surface is latent, surfacing as the P3 `Monad`, `identity`, `Functor`, and `negate` blockers *behind* the library modules. After the `logShow` slice, the 86 files blocked first at P3 on a name split as 77 to the `Prelude`/class surface #94 owns, 4 to #124 (`Unit` 2, `P.Unit` 1, `between` 1), 3 to #96 (`Partial`), and 2 to #95 (`assertEqual`). The 77 are `Monad` 13, `identity` 9, `_` 8, `negate` 6, `Functor` 6, `Eq1` 4, `<<<` 4, `otherwise` 3, `<$>` 3, `&&` 3, `when` 2, `mod` 2, `compare` 2, and one each of `P.identity`, `Applicative`, `||`, `>>>`, `not`, `-`, and `Foo.Bar`. `show` and `Show` are not in that set, and neither is `logShow` any longer. Show recorded that the GitHub `Corpus cases` field was not written because `gh` is not authenticated on that machine; Foldable's row said the field records the measured count, and that claim was not rechecked here. The `Functor` slice above remeasured the same boards: resolution **276/413**, L6/M7 **125/413**, and 67 `passing` files still first-blocked on a name this issue owns. | -| 4 | [#77](https://github.com/biuld/purescript-rs/issues/77) L4 and L5 to 100% | [#97](https://github.com/biuld/purescript-rs/issues/97) missing class checks, [#98](https://github.com/biuld/purescript-rs/issues/98) deriving and fundeps, [#99](https://github.com/biuld/purescript-rs/issues/99) hole inference, [#100](https://github.com/biuld/purescript-rs/issues/100) M3 kind gate, [#123](https://github.com/biuld/purescript-rs/issues/123) `forall` binder visibility | Turns "measurable" into "passing". #81 makes 153 cases trackable; the rest need rules. #123 is the shared root cause behind the three visible-type-application limits #87 recorded, and #100's polykind instantiation needs the same machinery, so it is filed as one foundational change rather than three patches. | +| 3 | [#76](https://github.com/biuld/purescript-rs/issues/76) Standard library — **gate met** | [#94](https://github.com/biuld/purescript-rs/issues/94) `Prelude` (77 measured after the `logShow` slice: the 7 cases that stopped on `logShow` stop instead on a `Prelude` name #94 also owns), [#95](https://github.com/biuld/purescript-rs/issues/95) `Effect`/`Effect.Console`/`Test.Assert` (305), [#96](https://github.com/biuld/purescript-rs/issues/96) `Proxy`/`Partial.Unsafe` (17), [#124](https://github.com/biuld/purescript-rs/issues/124) the `Data` modules no slice owned (27) | **342 of the 354** files L2 originally could not resolve were blocked on a missing library module. #95's first slice landed `Effect` and `Effect.Console`, dropping that to **83** and `passing` resolution from 59/413 to **199/413**; its second slice landed the `unit` value and `Test.Assert`, dropping the missing-module count to **62** and `passing` resolution to **209/413**. #94's first slice then landed `Data.Function` and the `$`/`#` operators, taking resolution to **225/413** and the missing-module count to **61**; its next slice landed `Data.Semigroup` and `<>`, taking resolution to **235/413**. `Eq`, `Ord`, and `Semiring` then landed with the intrinsic layer. The `Show` slice, measured on that master, moves resolution from 245/413 to **253/413**. `Data.Monoid` and `Data.Foldable`, measured independently on `6f66524` before `Show`, leave lenient resolution at **245/413** and move the compile-path missing-module count from 57 to 55. The figures were measured independently on `6f66524` and are not additive. The `Data.Tuple` slice, re-measured with the L2 scoreboard on `6f66524`, leaves resolution at **245/413** and moves the missing-module count from 57 to **56**, with other P3 blockers from 107 to **108**. That measurement is independent of the Show and Foldable figures and is not additive with them. Tuple's row said `logShow` and `assertEqual` were still waiting on the `Show`/`Eq` class surface, and that the GitHub `Corpus cases` field records the measured count; Show later recorded that the classes are declared and that the field was not written. What #95 still owns is `assertEqual` and `assertEqual'`; `logShow` has since landed as `log` of `show`, taking resolution to **270/413**. Depends on Phase 2, now complete: the library itself uses ascriptions, guards, sections, and instances. #94 measures 0 by first blocking stage only because `stdlib/lib/Prelude.purs` resolves; its missing surface is latent, surfacing as the P3 `Monad`, `identity`, `Functor`, and `negate` blockers *behind* the library modules. After the `logShow` slice, the 86 files blocked first at P3 on a name split as 77 to the `Prelude`/class surface #94 owns, 4 to #124 (`Unit` 2, `P.Unit` 1, `between` 1), 3 to #96 (`Partial`), and 2 to #95 (`assertEqual`). The 77 are `Monad` 13, `identity` 9, `_` 8, `negate` 6, `Functor` 6, `Eq1` 4, `<<<` 4, `otherwise` 3, `<$>` 3, `&&` 3, `when` 2, `mod` 2, `compare` 2, and one each of `P.identity`, `Applicative`, `||`, `>>>`, `not`, `-`, and `Foo.Bar`. `show` and `Show` are not in that set, and neither is `logShow` any longer. Show recorded that the GitHub `Corpus cases` field was not written because `gh` is not authenticated on that machine; Foldable's row said the field records the measured count, and that claim was not rechecked here. The `Functor` slice above remeasured the same boards: resolution **276/413**, L6/M7 **125/413**, and 67 `passing` files still first-blocked on a name this issue owns. | +| 4 | [#77](https://github.com/biuld/purescript-rs/issues/77) L4 and L5 to 100% — **in progress** | [#97](https://github.com/biuld/purescript-rs/issues/97) missing class checks, [#98](https://github.com/biuld/purescript-rs/issues/98) deriving and fundeps, [#99](https://github.com/biuld/purescript-rs/issues/99) hole inference, [#100](https://github.com/biuld/purescript-rs/issues/100) M3 kind gate, [#123](https://github.com/biuld/purescript-rs/issues/123) `forall` binder visibility | Turns "measurable" into "passing". #81 makes 153 cases trackable; the rest need rules. #123 is the shared root cause behind the three visible-type-application limits #87 recorded, and #100's polykind instantiation needs the same machinery, so it is filed as one foundational change rather than three patches. | | 5 | [#78](https://github.com/biuld/purescript-rs/issues/78) Backend on real programs | [#73](https://github.com/biuld/purescript-rs/issues/73) aggregate fixture execution, [#101](https://github.com/biuld/purescript-rs/issues/101) CC/MIR coverage, [#139](https://github.com/biuld/purescript-rs/issues/139) `Effect Unit` command entry | [#139](https://github.com/biuld/purescript-rs/issues/139) is an independent slice taken while Phase 3 and Phase 4 are still open. It does not complete those phases and it does not close #78. The other backend rows stay `Partial` on source coverage. | | 6 | [#79](https://github.com/biuld/purescript-rs/issues/79) M8 warnings and optimization | [#91](https://github.com/biuld/purescript-rs/issues/91) warning scoreboard, [#92](https://github.com/biuld/purescript-rs/issues/92) optimize comparison | Last, because both need a harness first and neither blocks another phase. | @@ -1139,14 +1164,14 @@ for matrix status. | L0 | Layout goldens | 15/15 official parse outcomes agree (12 accepted, 3 rejected), enforced by regression tests. | 15/15 agreement, with all layout cases covered by regression tests. | | L1 | Non-excluded parse behavior | 904/908 agreement using the annotations oracle; `passing` 410/413, `failing` 412/413, `warning` 67/67, `layout` 15/15, with the four remaining cases recorded as DEC-16 intentional differences | 100% agreement apart from the DEC-16 intentional differences. | | L2 | Module, import, export, and name resolution | **72/72** failing cases. `passing` resolution is **403/413**; the remaining 10 stop at P3 (6) or P0 (4), with no harness, missing-library, or unusable-sibling blockers. Reconfirmed with the annotations oracle on 2026-10-17 using the release harness and current locked package. | The mapped resolution cases and all required passing-module cases agree. | -| L3 | Kinds and higher-kinded types | 39/48 failing cases: `KindsDoNotUnify` 16/24, `PartiallyAppliedSynonym` 12/12, `CycleInTypeSynonym` 4/4, `CycleInKindDeclaration` 2/2, `InfiniteKind` 2/2, and `UndefinedTypeVariable` 3/4. | 100% agreement for the mapped kind cases. | -| L4 | Core type checking | 39/50 failing cases. The remaining mismatches include kind diagnostics reported in place of `ExpectedType`, missing `EscapedSkolem`, `VisibleTypeApplications1`, and five `Coercible` cases reported as `NoInstanceFound`. | 100% agreement for the mapped type cases. | -| L5 | Classes and instances | 81/97 failing cases: `OverlappingInstances` 8/8, `NoInstanceFound` 52/53, `MissingClassMember` 2/2, `InvalidNewtypeInstance` 6/6, `DuplicateInstance` 1/1, `InvalidInstanceHead` 1/7, `ClassInstanceArityMismatch` 4/4, `CannotDeriveInvalidConstructorArg` 7/7; `PossiblyInfiniteInstance` 0/1, `OrphanInstance` 0/7, `DuplicateTypeClass` 0/1. Remeasured with the annotations oracle on 2026-10-17 (release harness, vendored corpus, current locked package). The 2026-10-06 result was 75/97. | 100% agreement for the mapped class cases. | -| L6/M7 | Runtime and standard library | **287/340** non-FFI programs compile, validate, and run, all with exit code 0; no case traps. Of 365 roots, 25 FFI groups are excluded and 74 support sources remain inputs. The other 53 are 31 P5 typecheck, 11 P5 kind check, 2 P8 closure/linking (one recursive local binding and the missing `Test.Assert.checkThrows` foreign in `TCOMutRec.purs`), 5 P3 resolve, 2 P0 lex (DEC-16), the 10-second runtime timeout in `2288.purs`, and the bounded `BigFunction.purs` compilation. The shared coverage/`Partial` slice adds `Let`, `ShadowedTCOLet`, and `Where`, with no regressions. Remeasured 2026-10-18 after removing mandatory local-row specialization, with no success-set changes, at `7dd45e4b` plus the changes in [the same-day handoff](../implementation/backend/open-records-handoff-2026-10-17.md), release suite SHA-256 `52a9b77e706fd2030ed8c235c75f3a313ee118a18de0b49e4be21eb375e03df1`, required Wasmtime 49.0.3, and package `e556bf2f` / `fnv1a64-v1:7d96f1c44d8d52cc`. BigFunction ran separately with a 90-second cap and 2 GiB RSS guard; it reached the RSS guard at 27.89 seconds with peak RSS 2,141,824 KiB. The 2026-10-18 integrated [open-record review](../implementation/backend/open-records.md#integrated-topic-acceptance-review-2026-10-18) re-measured this tree with an identical result — the same failure set and suite identity, BigFunction at the guard in 33.39 seconds with peak RSS 2,137,584 KiB, run-to-run variation — completing the open-record checklist. | Every in-scope passing program for the feature compiles, validates, and runs with the expected result. | +| L3 | Kinds and higher-kinded types | 44/48 failing cases: `KindsDoNotUnify` 20/24, `PartiallyAppliedSynonym` 12/12, `CycleInTypeSynonym` 4/4, `CycleInKindDeclaration` 2/2, `InfiniteKind` 2/2, `UndefinedTypeVariable` 4/4. Remeasured 2026-10-18 after the cross-module instance-head kind check (`004de7ba`) and the local-annotation `UndefinedTypeVariable` rule (`56fe3cda`). The four remaining `KindsDoNotUnify` cases (`3077`, `3765-kinds`, `PolykindInstantiatedInstance`, `CoercibleKindMismatch`) are the polykind/expression-kind work of #100; `CoercibleKindMismatch`'s kind verdict exists at the constraint-solver layer (`54d69f92`) and needs a kind-board entry point that runs the solver. | 100% agreement for the mapped kind cases. | +| L4 | Core type checking | 41/50 failing cases: `TypesDoNotUnify` 34/41, `IntOutOfRange` 1/1, `InfiniteType` 2/2, `ExpectedType` 2/2, `EscapedSkolem` 1/2, `CannotApplyExpressionOfTypeOnType` 1/2, `AmbiguousTypeVariables` 1/1. Remeasured 2026-10-18: `ExpectedType`'s two cases now agree through the official annotation-position rule (`56fe3cda`, value signatures and local ascriptions run `checkTypeKind`'s kind equation). The remaining mismatches are six `Coercible` cases reported as `NoInstanceFound` (the FE-16 `Proof` verification contract), `PolykindGeneralizationLet` (the kind checker absorbs a term-level failure; the polykind-generalization work of #100), `SkolemEscapeKinds` (quantified-kind representation, #100/FE-11), and `VisibleTypeApplications1` (#123). | 100% agreement for the mapped type cases. | +| L5 | Classes and instances | 98/99 failing cases: `OverlappingInstances` 8/8, `NoInstanceFound` 52/53, `MissingClassMember` 2/2, `InvalidNewtypeInstance` 6/6, `DuplicateInstance` 1/1, `InvalidInstanceHead` 7/7, `ClassInstanceArityMismatch` 4/4, `CannotDeriveInvalidConstructorArg` 7/7, `OrphanInstance` 7/7, `PossiblyInfiniteInstance` 1/1, `DuplicateTypeClass` 1/1, and `CycleInTypeClassDeclaration` 2/2. Remeasured 2026-10-18 after the instance slices: the orphan rule (`298cc585`) reports an instance whose module declares neither its class nor a type constructor covering every official covering set; the resolver-side duplicate-class code is `fd7bf88a`; the determined-head rule, `PossiblyInfiniteInstance`, and the cycle code are `4a078b95`, which also moved the two superclass-cycle cases from blocked rows into the measured set (denominator 97 → 99). The only remaining mismatch is `ClassHeadNoVTA3` (a visible type application on a class-method head, #123). The shared `covering_sets` now compute the official inclusion-minimal sets (`9a4c2e04`). | 100% agreement for the mapped class cases. | +| L6/M7 | Runtime and standard library | **287/340** non-FFI programs compile, validate, and run, all with exit code 0; no case traps. Of 365 roots, 25 FFI groups are excluded and 74 support sources remain inputs. The other 53 are 29 P5 typecheck, 13 P5 kind check, 2 P8 closure/linking (one recursive local binding and the missing `Test.Assert.checkThrows` foreign in `TCOMutRec.purs`), 5 P3 resolve, 2 P0 lex (DEC-16), the 10-second runtime timeout in `2288.purs`, and the resource-bounded `BigFunction.purs` compilation. Remeasured 2026-10-18 serially (one worker per root, the 10-second guest wall unchanged) after the instance and diagnostic slices (`54d69f92`, `56fe3cda`, `4a078b95`, `298cc585`, `fd7bf88a`, `9a4c2e04`), with the same failure set as the recorded review and no regressions; the failure rows' stage attribution moved with the new kind and diagnostic codes (three `P5 kind check [ExpectedType]`, three `UndefinedTypeVariable`). Two rows (`NonConflictingExports.purs`, `NonOrphanInstanceFunDepExtra.purs`) are load-sensitive at the 10-second guest wall and pass when re-measured individually on the same binary; recorded as a measurement caveat, not a claimed gain. Wasmtime CLI 48.0.1 on this measurement host. BigFunction again did not finish inside the 90-second cap. | Every in-scope passing program for the feature compiles, validates, and runs with the expected result. | | M8-W | Warnings | 67 non-FFI warning files are in scope; no warning-code scoreboard exists | Warning-code agreement reaches 100% for the tracked warning corpus. | | M8-O | Optimization | 10 optimize files are in scope; they are not vendored and their goldens are JavaScript output | Expected optimize/CoreFn output agrees for all tracked optimize files. | -L1–L5 were reconfirmed on 2026-10-17 at `7dd45e4b` plus the shared coverage and `Partial` slice recorded in [the same-day handoff](../implementation/backend/open-records-handoff-2026-10-17.md), using the release harness, `PSRS_ORACLE=annotations`, `purs` 0.15.16 and package `e556bf2f` / `fnv1a64-v1:7d96f1c44d8d52cc`: L1 904/908, L2 72/72 and passing resolution 403/413, L3 39/48, L4 39/50, L5 81/97. The previous same-day frontend checkpoint used package `6fcef6cc` / `fnv1a64-v1:5fcbb57525c63eb1` and measured L5 77/97. The frontend units remain source files; L6/M7 uses program groups as recorded in the gate row. The earlier 273/413, 210/413 and 164/413 runtime records used per-file units and are historical, not additive with the program board. L5 keeps denominator 97. +L1–L5 were reconfirmed on 2026-10-18 at master after the instance and diagnostic slices (`54d69f92` instance-head kinds, `56fe3cda` annotation-position codes, `4a078b95` instance heads and cycles, `298cc585` the orphan rule, `fd7bf88a` duplicate type classes, `9a4c2e04` inclusion-minimal covering sets), using the annotations oracle, the vendored corpus, the release harness, and the package `e556bf2f` / `fnv1a64-v1:7d96f1c44d8d52cc`: L2 72/72 and passing resolution 403/413, L3 44/48, L4 41/50, L5 98/99. The parse board was not re-measured on this host (`purs` is unavailable here); its last measurement remains 2026-10-17's L1 904/908. The 2026-10-17 checkpoint at `7dd45e4b` measured L3 39/48, L4 39/50, L5 81/97. The frontend units remain source files; L6/M7 uses program groups as recorded in the gate row. The earlier 273/413, 210/413 and 164/413 runtime records used per-file units and are historical, not additive with the program board. L5's denominator is now 99: the two superclass-cycle cases left the blocked rows when the cycle code was mapped. ### Feature-to-gate crosswalk @@ -1202,9 +1227,9 @@ resolved, type checked, and represented in Typed Core as required. | FE-17 | Visible type application, typed binders, type wildcards, holes, and advanced annotations | Typed binders preserve and check scoped annotations, and each source type wildcard receives fresh kind/type variables through the shared type spine. Type-level `String` and `Int` literals are ordinary spine nodes: a signature may contain them, they unify by value, and they survive into THIR where the verifier compares them. A wildcard in a value signature is solved by unification and is accepted in every shape `purs` accepts; a wildcard in an instance head is rejected as `InvalidInstanceHead`, while one in an instance context stays legal. The `1664.purs` wildcard binder lowers through P2. Visible term type application, wildcard warning/error behavior, higher-kinded application, and non-generalized hole diagnostics remain incomplete. The `Type`, `Constraint`, and `Symbol` heads are accepted as ordinary type constructors with their declared primitive kinds. Official's CST has no kind-application node; its kind checker synthesizes `KindApp` while instantiating a polymorphic kind, and this compiler performs that instantiation in the kind solver, so its source type spine needs no `KindApplication` node. The source forms that do name a kind or type explicitly are separate nodes. #87 lands both of the forms that blocked P2: a negative type-level integer prefix is the negative literal on the shared spine, and a visible type application `e @T` is elaborated by the checker, which substitutes the written argument for the operand's outermost quantifier after checking it against that quantifier's kind, and is erased at runtime. No P2 surface-lowering case remains. Three limits are recorded rather than approximated. A chained application `f @A @B` is reported, because the quantifiers an application leaves behind are scheme variables here and choosing between them needs the scheme to record which variables a visible application has consumed. A visible application on a class-method head is unresolved, which is `failing/ClassHeadNoVTA3.purs`. And this compiler's CST does not carry the binder visibility that official's `CST/Convert.hs` derives from `forall @a.`, so a plain `forall a.` binder is selectable where `purs` rejects it — the permissive direction, and the remaining half of `failing/VisibleTypeApplications1.purs`. `CannotApplyExpressionOfTypeOnType` and `CannotSkipTypeApplication` are the mapped codes. The primitive row relations themselves all have rules, and the row-side gap that remains is the rigid-tail unification defect under FE-13. | Partial | Model `forall` binder visibility so a visible application matches official, then resolve chained applications and class-method heads. | | FE-18 | Higher-rank types, subsumption, impredicativity, and higher-rank `forall` | Bidirectional checking preserves nested quantifiers, checks directional function/record subsumption, and rejects escaping skolems and specialized universal arguments. Source and GC execution cases cover rank-2 through rank-4, fields, returned and captured values, recursive annotations, higher-kinded parameters, and nested constraints. See the [rank-N acceptance record](../implementation/frontend/rank-n.md) for verification evidence and the official differential battery. | Partial | Reconcile the complete official higher-rank/skolem corpus, including its library dependencies and separate higher-rank kind requirements; track visible type application and diagnostic agreement. | | FE-19 | Foreign declarations and target-aware external names | Source-declared WIT bindings are resolved for the supported backend path. `foreign import data` is a nominal opaque type with no constructors; a nullary one maps to a WIT resource. THIR and Core keep it as `Constructor(User(id))` plus `opaque_ids`, distinct from `Int` (`lowers_an_opaque_foreign_type_to_core_without_collapsing_it_to_int`). JavaScript FFI is not a frontend target. CC/MIR handle layout is not done. | Partial | Finish target-aware foreign value rules beyond the supported WIT subset. Resource lifetime and handle layout stay in the backend. | -| FE-20 | Warnings, holes, source spans, and official diagnostic codes | Source spans exist and resolution, kind, type, and class `errorCode`s are measured: L1 904/908, L2 72/72 (remeasured 2026-10-07), L3 39/48, L4 39/50, L5 81/97 (remeasured 2026-10-17). L4 per-code agreement is `TypesDoNotUnify` 34/41, `IntOutOfRange` 1/1, `InfiniteType` 2/2, `ExpectedType` 0/2, `EscapedSkolem` 1/2, `CannotApplyExpressionOfTypeOnType` 1/2, and `AmbiguousTypeVariables` 1/1. `MultipleErrors.purs` repeats its annotation, so code-occurrence counts sum to 40/51 while case agreement remains 39/50. Pattern-binder diagnostics match the annotated duplicate-name cases; warning coverage and complete diagnostic agreement remain open. Non-generalized hole diagnostics remain tracked under FE-17. | Partial | Add the missing class checks (#97) and track warning-code agreement separately from acceptance errors. | +| FE-20 | Warnings, holes, source spans, and official diagnostic codes | Source spans exist and resolution, kind, type, and class `errorCode`s are measured: L1 904/908, L2 72/72 (remeasured 2026-10-18), L3 44/48, L4 41/50, L5 98/99 (remeasured 2026-10-18). L4 per-code agreement is `TypesDoNotUnify` 34/41, `IntOutOfRange` 1/1, `InfiniteType` 2/2, `ExpectedType` 2/2, `EscapedSkolem` 1/2, `CannotApplyExpressionOfTypeOnType` 1/2, and `AmbiguousTypeVariables` 1/1. `MultipleErrors.purs` repeats its annotation, so code-occurrence counts exceed case agreement while case agreement remains 41/50. Pattern-binder diagnostics match the annotated duplicate-name cases; warning coverage and complete diagnostic agreement remain open. Non-generalized hole diagnostics remain tracked under FE-17. | Partial | Track warning-code agreement separately from acceptance errors. | | FE-21 | Typed Core normalization and CoreFn/optimization compatibility | Typed Core lowering and verification work for the supported subset; official optimize output is not yet a target. | Partial | Add Core optimization passes and an explicit optimize compatibility track. | -| FE-22 | Deriving and newtype-based derivation | Every structural family generates ordinary checked instance members through one identity registry and syntax builder. All mapping families, folds, and traversals consume shared usage/variance analysis, including record fields, given higher-kinded dictionaries, and scoped forall parameters. Source tests cover every deriving diagnostic; differential batteries cover 18 original rules, 17 remaining-family/context/scoped cases, and six diagnostic cases. 25 Wasmtime cases cover all structural classes, Generic tag/field round trips, function Contravariant, polymorphic newtype adapters, applied-variable Eq1/Ord1 dispatch, both fold directions, sequencing, and multi-field traversal. L5 is 81/97, with deriving-specific `InvalidNewtypeInstance` 6/6 and `CannotDeriveInvalidConstructorArg` 7/7. | Partial | Shared declaration checks still mismatch the official orphan and invalid record/synonym instance-head cases, including `3405`, `3510`, and `InvalidDerivedInstance2`. See the [deriving design](frontend/type-system/deriving.md) and [acceptance record](../implementation/frontend/deriving.md). | +| FE-22 | Deriving and newtype-based derivation | Every structural family generates ordinary checked instance members through one identity registry and syntax builder. All mapping families, folds, and traversals consume shared usage/variance analysis, including record fields, given higher-kinded dictionaries, and scoped forall parameters. Source tests cover every deriving diagnostic; differential batteries cover 18 original rules, 17 remaining-family/context/scoped cases, and six diagnostic cases. 25 Wasmtime cases cover all structural classes, Generic tag/field round trips, function Contravariant, polymorphic newtype adapters, applied-variable Eq1/Ord1 dispatch, both fold directions, sequencing, and multi-field traversal. L5 is 98/99 (remeasured 2026-10-18), with deriving-specific `InvalidNewtypeInstance` 6/6 and `CannotDeriveInvalidConstructorArg` 7/7; the derived instance heads of `3510` and `InvalidDerivedInstance2` now agree through the shared determined-head rule. | Partial | Reconcile the remaining deriving differential evidence under the official shared declaration checks. See the [deriving design](frontend/type-system/deriving.md) and [acceptance record](../implementation/frontend/deriving.md). | The frontend landing order is: diff --git a/docs/implementation/runtime-program-scoreboard.md b/docs/implementation/runtime-program-scoreboard.md index ea5c000e..30d3c76f 100644 --- a/docs/implementation/runtime-program-scoreboard.md +++ b/docs/implementation/runtime-program-scoreboard.md @@ -334,3 +334,39 @@ open-row interaction regressions recorded in the [open-record checklist](open-records.md#integrated-topic-acceptance-review-2026-10-18). With every requirement row re-executed and the board re-measured, the open-record checklist is complete at commit `e331f9ba` plus this review. + +## Serial rerun after the instance and diagnostic slices: 2026-10-18 + +Compiler master after the five instance/diagnostic slice merges (`54d69f92` +instance-head kinds, `56fe3cda` annotation-position codes, `4a078b95` +instance heads and cycles, `298cc585` the orphan rule, `fd7bf88a` duplicate +type classes, `9a4c2e04` inclusion-minimal covering sets), package +`e556bf2f` / `fnv1a64-v1:7d96f1c44d8d52cc` unchanged. The measurement host +differs from the earlier close-outs: Wasmtime **CLI 48.0.1**, no `purs` +installed. Protocol: **one worker per root, serially** (`xargs -P1`), each +root filtered by `passing/` with a 110-second compile cap, all 365 +roots including `BigFunction.purs`; suite binary +`target/release/deps/suite-461c5a8e1563a05b`, SHA-256 +`90da2757e8e2e2a362a7d8cfdd7f0f686d6655c502f006809385a7457439fa00`. + +The board is **287/340**: 287 completions exit zero, 25 FFI groups excluded, +52 named non-agreements and the resource-bounded `BigFunction.purs`. The +failing set is identical to the 2026-10-18 review's; the rows' stage +attribution moved with the newly mapped kind and diagnostic codes (three rows +now report `P5 kind check [ExpectedType]`: `4500.purs`, `4535.purs`, +`TypeSynonymsInKinds.purs`, and three `P5 kind check [UndefinedTypeVariable]`). + +**Measurement caveat, recorded rather than claimed:** two rows +(`NonConflictingExports.purs`, `NonOrphanInstanceFunDepExtra.purs`) time out +at the board's fixed 10-second guest wall under concurrent measurement load +(two full parallel board runs ran simultaneously when this was first seen) +and **pass when re-measured individually** on the identical binary — `1/1, +stdout: Done`, verified twice (2026-10-18, sequential). The number 287/340 is +stable across the parallel and serial protocols; the caveat documents that +these rows are load-sensitive, not that the success set grew. Raw per-root +rows: `/tmp/opencode/s1l6/final.raw` (this tree) and `/tmp/opencode/s1l6/base.raw` +(the 54-name pre-slice comparison at `cbdfceb2`, suite SHA-256 +`befcb214322a19f5ea61c23e3fdb6cf49954e9a84a7a681499e41895e2fcf318`). +`BigFunction.purs` again did not finish inside a 90-second cap on this host +(`/tmp/opencode/s1l6/bigfunc.verdict`); its resource-bounded row is unchanged +in kind, and no compile acceptance is claimed.