CType/IType: qualification-scoped tycon comparison, documented invariant

BSC's front end enforces one type constructor per qualified name, so a
qualified Id determines its (kind, sort) payload.  This invariant was
already load-bearing in comparison code -- TyCon Eq ignored the sort,
and ITCon comparison in IType.cmpT is by Id alone -- but unstated, and
the TyCon instances mixed regimes: Eq compared kinds even for pairs
where the invariant makes that a dead tail, while remaining
kind-sensitive for the unqualified names where the invariant is
undefined.

Scope the TyCon comparisons by qualification:

  * Eq: both-qualified pairs compare by Id (qualEq); the kind hedge is
    kept only when either side is unqualified (resolution-era fuzz).
  * Ord: lexicographic on (base, qual); within a (base, qual) bucket,
    both-qualified ties are EQ without consulting the kinds, and the
    unqualified bucket keeps the kind comparison.  This remains a
    lawful total order.

Document at the instances: the invariant and its qualified-only domain,
the deliberate non-transitivity of Eq via qualEq (pre-existing), the
Eq/Ord disagreement (pre-existing; containers key on Ord), and the
pointer to the tconcheck build step that verifies the handwritten
payload copies the by-Id comparisons rely on.  Also upgrade the cmpT
comment in IType.hs: ITCon by-Id comparison is justified by the same
invariant (all ITCon Ids are qualified, since IType is born
post-resolution at IConv); the ITForAll binder-kind skip is a separate,
alpha-structural assumption, unchanged.

The only behavior delta is a both-qualified pair with the same name and
differing Maybe Kind fields.  An audit of the pipeline found no
comparison site where a qualified Nothing-kinded TyCon (parse-era
trees, cTCon-built compiler-generated code) can meet its Just-kinded
twin (symtab/convCQType-era types): type-level Eq/Ord is only exercised
within a single kind regime, cross-regime checks use kind-agnostic
helpers (leftCon, mkInstId, Id comparisons), and no container is keyed
on Type/CType where mixed twins could coexist.  The full testsuite and
a rebuild of all libraries with the changed compiler back this
empirically.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01LVL9ornS6uf9hVxAuL7GhK

Author: nanavati

src/comp/CType.hs

@@ -201,12 +201,39 @@ instance Eq Type where
 instance Eq TyVar where
     TyVar i n _ == TyVar i' n' _  =  (n, i) == (n', i')
 
+-- TyCon comparison and the one-tycon-per-qualified-name invariant
+--
+-- BSC's front end enforces one type constructor per qualified name, so a
+-- qualified Id determines its (kind, sort) payload.  The invariant holds
+-- ONLY for qualified names: unqualified TyCons exist during scope
+-- resolution, where the same base name may denote different constructors.
+-- The tconcheck build step (src/comp/tconcheck.hs) verifies the compiler's
+-- handwritten copies of Prelude tycon payloads against the compiled
+-- Prelude, keeping the invariant checkable.
+--
+-- Eq is therefore scoped by qualification:
+--  * both ids qualified: the invariant's regime.  Comparison is by Id;
+--    the payloads are determined by the name (checker-verified), so a
+--    payload comparison would be a dead tail.
+--  * either id unqualified: resolution-era fuzz, where the invariant is
+--    undefined; the kind comparison is kept as a hedge.
+--
+-- Two pre-existing quirks, both deliberate and unchanged:
+--  * Eq is non-transitive: qualEq compares by base name alone when either
+--    side is unqualified, so P.T == T and T == Q.T but P.T /= Q.T.
+--  * Eq and Ord disagree: Ord compares the full qualifier on both sides
+--    (a lawful total order), while Eq admits the qualEq fuzz.  Containers
+--    key on Ord.
 instance Eq TyCon where
-    TyCon i k _ == TyCon i' k' _  =  qualEq i i' && k == k'
+    TyCon i k _ == TyCon i' k' _  =  qualEq i i' && (bothQualified i i' || k == k')
     TyNum i _   == TyNum i' _     =  i == i'
     TyStr s _   == TyStr s' _     =  s == s'
     _           == _              =  False
 
+-- both ids carry a package qualifier (see the invariant note above)
+bothQualified :: Id -> Id -> Bool
+bothQualified i i' = not (isUnqualId i) && not (isUnqualId i')
+
 -- Ord instances
 
 instance Ord Type where
@@ -220,7 +247,15 @@ instance Ord TyVar where
     TyVar i n _ `compare` TyVar i' n' _  =  (n, i) `compare` (n', i')
 
 instance Ord TyCon where
-    TyCon i k _ `compare` TyCon i' k' _   =  (getIdBase i, getIdQual i, k) `compare` (getIdBase i', getIdQual i', k')
+    -- lexicographic on (base, qual); within a (base, qual) bucket either
+    -- both ids are qualified -- unique by the invariant documented at Eq,
+    -- so EQ without consulting the kinds -- or both are unqualified, where
+    -- the kind comparison is kept, as in Eq.  This remains a lawful total
+    -- order.
+    TyCon i k _ `compare` TyCon i' k' _   =
+        case (getIdBase i, getIdQual i) `compare` (getIdBase i', getIdQual i') of
+          EQ -> if bothQualified i i' then EQ else compare k k'
+          o  -> o
     TyCon _ _ _ `compare` TyNum _  _      =  LT
     TyCon _ _ _ `compare` TyStr _  _      =  LT
     TyNum _ _   `compare` TyCon _  _  _   =  GT

src/comp/IType.hs

@@ -72,8 +72,19 @@ instance Eq IType where
 instance Ord IType where
     compare x y = cmpT x y
 
+-- ITCon is compared by Id alone.  This is justified by the
+-- one-tycon-per-qualified-name invariant: BSC's front end enforces one
+-- type constructor per qualified name, so a qualified Id determines its
+-- (kind, sort) payload -- and all ITCon Ids are qualified, because IType
+-- is born post-resolution at IConv.  The handwritten payload copies this
+-- relies on are verified against the compiled Prelude by the tconcheck
+-- build step (src/comp/tconcheck.hs).
+--
+-- The ITForAll case skips the binder kinds; that is a separate,
+-- alpha-structural assumption (same binder Id in the same position implies
+-- the same kind), unchanged and unrelated to the tycon invariant.
 cmpT :: IType -> IType -> Ordering
-cmpT (ITForAll i1 _ t1) (ITForAll i2 _ t2) =  -- kind comparison skipped for speed
+cmpT (ITForAll i1 _ t1) (ITForAll i2 _ t2) =  -- binder kind comparison skipped (see above)
         case compare i1 i2 of
         EQ -> cmpT t1 t2
         o  -> o