Fix spurious T0029 when a field reaches an ATF through a type synonym#5
Open
nanavati wants to merge 12 commits into
Open
Fix spurious T0029 when a field reaches an ATF through a type synonym#5nanavati wants to merge 12 commits into
nanavati wants to merge 12 commits into
Conversation
Also adds tests including the ones added by @quark17 in B-Lang-org#909
This reverts commit de377a9.
…re being filtered anyway
Testsuite-only changes responding to review feedback:
- Keep the original id-based ATFUnify{,HK}Error tests and add
struct-field-access variants (ATFFieldUnify{,HK}Error); refresh
the expected output for the id-based tests.
- Add struct-field tests for the SizeOf-through-synonym context
requirement: field use (ExpSizeOf_FieldSyn_Use_{NoCtx,WithCtx}) and
a field whose type variable is not a struct parameter
(ExpSizeOf_FieldSyn_Unbound_{NoCtx,WithCtx}).
- Add a type-annotated-expression test
(ExpSizeOf_TypedExpr_{NoCtx,WithCtx}) and regroup the explicit-type
tests (valueOf/stringOf/typed-expr/let) under a corrected header.
- Add CExtendATF{,Explicit}: an ATF variant of CExtendSynonym that still
fails without explicit method types, demonstrating GitHub Issue B-Lang-org#311.
- Add ExpSizeOf_VectorIfc for GitHub Issue B-Lang-org#313 (typechecks, but fails
to synthesize; not fixed by PR B-Lang-org#916).
- Record bug numbers (Bluespec Inc Bug 1729, GitHub B-Lang-org#310/B-Lang-org#311/B-Lang-org#313,
bsc-contrib PR 46) and update stale comments.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
When a data/struct field type refers to an associated type function through a type synonym (e.g. `type ElemSyn f = Elem f`), the auto-derived Generic instance failed to typecheck with a spurious "signature too general" (T0029) error, while the same field written with the ATF applied directly (`Elem f`) compiled fine. The instance head (the "given" scheme) is processed by ctxRedCQType', which expands synonyms and generalizes the exposed ATF application into a fresh class-constrained variable: instance (Container f e) => Generic (WrapSyn f) (... Conc e ...) But when the derived method bodies are typechecked, the constructor and field types are instantiated with the synonym unexpanded, and unifying the head's variable `e` against `ElemSyn c` did not recognize the synonym-hidden ATF: mgu structurally bound `e := ElemSyn c`, pinning the fundep-determined variable. The deduced scheme then quantified one fewer variable than the given scheme, and the syntactic scheme comparison in tiExpl''' reported T0029. The direct case works because mgu recognizes ATF applications (isATFAp) and routes them to atfUnify, which refuses to bind bound type variables and instead defers a type equality that eqToPred turns into the class predicate `Container c e` -- satisfiable from the instance context, leaving `e` generic. Fix: in mgu, expand a saturated type-synonym application when (and only when) its expansion is a fully applied ATF application, so that a synonym-hidden ATF unifies exactly like the direct one. Synonyms whose expansion is not ATF-headed -- notably the parameter-dropping TLM-style synonyms that caused earlier synonym-expansion attempts to be reverted (see the XXX comments in CtxRed/TCheck and the CExtendSynonym test) -- keep the existing structural behavior. This also makes the missing-context error for a synonym-hidden ATF (e.g. assigning a field of type `ElemSyn f` to Bool) identical to the direct-ATF case (T0030 naming the needed Container context), and genuinely-too-general signatures still fail with T0029. Adds ATFSynonymField.bs (the reproducer: data and struct fields whose types reach the ATF through a synonym must compile) and ATFSynonymFieldUse.bs (exercises the same shapes through Bits derivation, Generic from/to, and Verilog elaboration). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01M8cZoDh1jk24UJbB51y5tU
checkNoTypeFunInHead scanned instance-head arguments syntactically, so a type function reaching a non-determined head position through a type synonym escaped the T0156 check that rejects the directly-written form. Depending on the shape, the synonym form then either failed with a confusing ambiguity error (T0079) or was silently accepted with instance-head expansion rewriting the head into something other than what was written -- while the identical head written without the synonym was rejected. Since the check runs on raw definitions (before context reduction), the type constructors may not yet carry their symbol-table sorts, so the check now resolves them (updTypes) and expands each saturated synonym application, rejecting any type function application in the expansion that mentions a type variable or is not fully applied: such an application can neither be reduced away nor used for instance matching. The error is reported at the position of the synonym use, naming the type function. Ground applications hidden behind synonyms remain allowed: context reduction expands and reduces them to a concrete type, which is the Bug 1729 / GitHub B-Lang-org#311 behavior that ExpSizeOf_InstancesBaseSyn pins (e.g. `typedef SizeOf#(T) ST' used as an instance argument). Note this remains more permissive than the directly-written ground form, which T0156 still rejects (as pinned by ATFInInstHead); relaxing that for reducible applications could be considered separately. Determined positions remain exempt, synonym or not, since they are never used for instance matching. Adds ATFInInstHeadSynonym.bs and ATFInInstHeadSynonymElsewhere.bs (variable applications, rejected with T0156 like the direct forms), ATFInInstHeadSynonymGround.bs (ground application, still accepted), and ATFInInstHeadDeterminedSynonym.bs (determined position, still accepted). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01M8cZoDh1jk24UJbB51y5tU
nanavati
force-pushed
the
claude/t0029-atf-synonym-regression-mhlsbj
branch
from
July 8, 2026 10:39
dcad864 to
4560905
Compare
Unify.hs: merge the ATF check into a single asATFAp function that returns the type as a fully applied type-function application (either directly, or behind a saturated type synonym), and document why synonyms are not expanded unconditionally: unification is a hot path and expandSyn is a deep expansion; expandSyn fails on unsaturated synonym applications; and a synonym whose expansion is not an ATF application must keep the existing structural unification of the unexpanded synonym (e.g. parameter-dropping synonyms, GitHub issue 311). MakeSymTab.hs: checkNoTypeFunInHead now reports both the directly written type functions and the synonym-hidden ones (deduplicated), instead of omitting the synonym-hidden errors whenever a directly written one is present. Adds ATFInInstHeadSynonymBoth.bs: a direct and a synonym-hidden type function in the same instance head, both reported with T0156. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01M8cZoDh1jk24UJbB51y5tU
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Fixes two holes where a type function (ATF) hidden behind a type synonym behaved differently from the directly-written form. The branch is based on upstream PR B-Lang-org#916 ("Fix B-Lang-org#890 by expanding type functions in tiExpl") — the first 9 commits are that PR unchanged; the last two commits are the fixes.
1.
Unify.hs— spurious T0029 on auto-derived Generic (7a4c248)With PR 916's instance-head expansion, a data/struct field whose type reaches an ATF through a synonym (
type ElemSyn f = Elem f) made the auto-derived Generic instance fail with a spurious "signature too general" (T0029), while the directElem fspelling compiled. Code with this shape is common enough that the regression breaks substantial existing designs.The instance head (given scheme) expands synonyms and generalizes the exposed ATF into a fresh class-constrained variable, but during typecheck of the derived method bodies,
mgudid not recognize the synonym-hidden ATF:isATFApsees only a literalTIatfhead, so unification structurally bound the head's fundep-determined variable to the unexpandedElemSyn c— pinning it. The deduced scheme then quantified one fewer variable than the given scheme andtiExpl'''reported T0029. The direct spelling works becauseatfUnifydefersboundVar ~ Elem cinto an equality that becomes the satisfiable class predicateContainer c e.Fix: in
mgu, expand a saturated type-synonym application when (and only when) its expansion is a fully-applied ATF application, routing it into the existingatfUnifydeferral. Synonyms whose expansion is not ATF-headed — notably the parameter-dropping TLM-style synonyms that forced earlier expansion attempts to be reverted (CExtendSynonym) — keep the existing structural behavior. This also makes the missing-context error for a synonym-hidden ATF identical to the direct case (T0030 naming the needed context), while genuinely-too-general signatures still fail with T0029.2.
MakeSymTab.hs— instance-head check bypass (dcad864)checkNoTypeFunInHeadscanned instance-head arguments syntactically, so an ATF reaching a non-determined head position through a synonym escaped the T0156 check: depending on the shape it either failed with a confusing T0079 or was silently accepted with the head rewritten by instance-head expansion — while the identical head written directly was rejected.Fix: resolve constructor sorts and expand each saturated synonym application in non-determined positions, rejecting ATF applications that mention a type variable or are under-applied (they can neither reduce away nor participate in instance matching), reported at the synonym-use position. Ground applications remain accepted — that is the Bug 1729 / B-Lang-org#311 behavior pinned by
ExpSizeOf_InstancesBaseSyn(typedef SizeOf#(T) STin a head). Determined positions remain exempt, synonym or not. Note the directly-written ground form is still rejected (as pinned byATFInInstHead); relaxing that for reducible applications could be considered separately.Tests
ATFSynonymField.bs— reproducer: data and struct fields reaching an ATF through a synonym compile (was 2× T0029)ATFSynonymFieldUse.bs— same shapes through Bits derivation, explicit Generic from/to, and Verilog elaborationATFInInstHeadSynonym.bs,ATFInInstHeadSynonymElsewhere.bs— variable ATF applications behind synonyms in heads, rejected with T0156 like the direct formsATFInInstHeadSynonymGround.bs— ground application behind a synonym, still acceptedATFInInstHeadDeterminedSynonym.bs— determined position behind a synonym, still acceptedValidation
bsc.typechecker/typeclasses: 107/107,bsc.typechecker/primtcons: 31/31 (includes all PR 916 tests:ExpSizeOf_*,CExtendSynonym,CExtendATF)bsc.typecheckerrecursively: 1184 passes, 0 unexpected failures;bsc.bugs: 940 passes, 1 environment-only failure (permission-denied test running as root);bsc.bluetcl: 189/189🤖 Generated with Claude Code
https://claude.ai/code/session_01M8cZoDh1jk24UJbB51y5tU