Summary
In compiler-core/checking/src/core/constraint.rs, the elide_missing_patterns check (introduced in #146) uses implication_given.contains(partial) to decide whether to suppress MissingPatterns errors. This only inspects the raw/direct given set and does not account for Partial being made available through superclass entailment.
As a result, if Partial is reachable via a superclass but not listed as a direct given, MissingPatterns errors may still be emitted even though the scope should permit partiality.
Details
- File:
compiler-core/checking/src/core/constraint.rs
- Relevant lines: around the
elide_missing_patterns computation in collect_scoped_constraints
The fix would be to consult the elaborated/entailment-aware given set when computing elide_missing_patterns, so that Partial derived through superclass entailment also suppresses the error.
Context
Raised as a review comment on #146: #146 (comment)
Acknowledged as a known limitation by @purefunctor — Partial is typically provided directly in practice, making this a very small class of bug unlikely to appear in real-world codebases. Tracked here for completeness.
Summary
In
compiler-core/checking/src/core/constraint.rs, theelide_missing_patternscheck (introduced in #146) usesimplication_given.contains(partial)to decide whether to suppressMissingPatternserrors. This only inspects the raw/direct given set and does not account forPartialbeing made available through superclass entailment.As a result, if
Partialis reachable via a superclass but not listed as a direct given,MissingPatternserrors may still be emitted even though the scope should permit partiality.Details
compiler-core/checking/src/core/constraint.rselide_missing_patternscomputation incollect_scoped_constraintsThe fix would be to consult the elaborated/entailment-aware given set when computing
elide_missing_patterns, so thatPartialderived through superclass entailment also suppresses the error.Context
Raised as a review comment on #146: #146 (comment)
Acknowledged as a known limitation by @purefunctor —
Partialis typically provided directly in practice, making this a very small class of bug unlikely to appear in real-world codebases. Tracked here for completeness.