[Git][ghc/ghc][master] 2 commits: Update equality-type documenation in GHC.Builtin.Types.Prim

Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC Commits: d910b353 by Simon Peyton Jones at 2026-07-08T04:48:36-04:00 Update equality-type documenation in GHC.Builtin.Types.Prim Fix #27466 - - - - - b2530542 by Simon Peyton Jones at 2026-07-08T04:48:36-04:00 Honour -dsuppress-coercions in GHC.Core.TyCo.pprCo Fixes #27467 - - - - - 11 changed files: - compiler/GHC/Builtin/Types/Prim.hs - compiler/GHC/Core/Ppr.hs - compiler/GHC/Core/TyCo/Ppr.hs - compiler/GHC/Core/TyCo/Rep.hs - testsuite/tests/codeGen/should_compile/T25177.stderr - testsuite/tests/numeric/should_compile/T15547.stderr - testsuite/tests/simplCore/should_compile/DataToTagFamilyScrut.stderr - testsuite/tests/simplCore/should_compile/T14978.stdout - testsuite/tests/simplCore/should_compile/T18013.stderr - testsuite/tests/simplCore/should_compile/T24229a.stderr - testsuite/tests/simplCore/should_compile/T24229b.stderr Changes: ===================================== compiler/GHC/Builtin/Types/Prim.hs ===================================== @@ -1002,26 +1002,29 @@ doublePrimTyCon = pcPrimTyCon0 doublePrimTyConName doubleRepDataConTy Note [The equality types story] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -GHC sports a veritable menagerie of equality types: - - Type or Lifted? Hetero? Role Built in Defining module - class? L/U TyCon ------------------------------------------------------------------------------------------ -~# T U hetero nominal eqPrimTyCon GHC.Prim -~~ C L hetero nominal heqTyCon GHC.Types -~ C L homo nominal eqTyCon GHC.Types -:~: T L homo nominal (not built-in) Data.Type.Equality -:~~: T L hetero nominal (not built-in) Data.Type.Equality - -~R# T U hetero repr eqReprPrimTy GHC.Prim -Coercible C L homo repr coercibleTyCon GHC.Types -Coercion T L homo repr (not built-in) Data.Type.Coercion -~P# T U hetero phantom eqPhantPrimTyCon GHC.Prim +GHC sports a veritable menagerie of equality types. + + Result kind Hetero? Role Built in Defining module +--------------------------------------------------------------------------------- +~# Constraint# hetero nominal eqPrimTyCon GHC.Prim +~~ Constraint hetero nominal heqTyCon GHC.Types +~ Constraint homo nominal eqTyCon GHC.Types +:~: Type homo nominal (not built-in) Data.Type.Equality +:~~: Type hetero nominal (not built-in) Data.Type.Equality + +~R# Constraint# hetero repr eqReprPrimTy GHC.Prim +Coercible Constraint homo repr coercibleTyCon GHC.Types +Coercion Type homo repr (not built-in) Data.Type.Coercion +~P# Constraint# hetero phantom eqPhantPrimTyCon GHC.Prim + +Here `Constraint#` means `CONSTRAINT (TupleRep [])`, a constraint kind that is +represented by a zero-width tuple. Recall that "hetero" means the equality can related types of different kinds. Knowing that (t1 ~# t2) or (t1 ~R# t2) or even that (t1 ~P# t2) also means that (k1 ~# k2), where (t1 :: k1) and (t2 :: k2). + To produce less confusion for end users, when not dumping and without -fprint-equality-relations, each of these groups is printed as the bottommost listed equality. That is, (~#) and (~~) are both rendered as (~) in @@ -1030,7 +1033,7 @@ error messages, and (~R#) is rendered as Coercible. Let's take these one at a time: -------------------------- - (~#) :: forall k1 k2. k1 -> k2 -> TYPE (TupleRep '[]) + (~#) :: forall k1 k2. k1 -> k2 -> CONSTRAINT (TupleRep '[]) -------------------------- This is The Type Of Equality in GHC. It classifies nominal coercions. This type is used in the solver for recording equality constraints. @@ -1054,8 +1057,6 @@ This is (almost) an ordinary class, defined as if by Here's what's unusual about it: * We can't actually declare it that way because we don't have syntax for ~#. - And ~# isn't a constraint, so even if we could write it, it wouldn't kind - check. * Users cannot write instances of it. @@ -1112,7 +1113,7 @@ They are not defined within GHC at all. -------------------------- - (~R#) :: forall k1 k2. k1 -> k2 -> TYPE (TupleRep '[]) + (~R#) :: forall k1 k2. k1 -> k2 -> CONSTRAINT (TupleRep '[]) -------------------------- The is the representational analogue of ~#. This is the type of representational equalities that the solver works on. All wanted constraints of this type are @@ -1147,7 +1148,7 @@ within GHC at all. -------------------------- - (~P#) :: forall k1 k2. k1 -> k2 -> TYPE (TupleRep '[]) + (~P#) :: forall k1 k2. k1 -> k2 -> CONSTRAINT (TupleRep '[]) -------------------------- This is the phantom analogue of ~# and it is barely used at all. (The solver has no idea about this one.) Here is the motivation: ===================================== compiler/GHC/Core/Ppr.hs ===================================== @@ -292,14 +292,14 @@ noParens :: SDoc -> SDoc noParens pp = pp pprOptCo :: Coercion -> SDoc --- Print a coercion optionally; i.e. honouring -dsuppress-coercions -pprOptCo co = sdocOption sdocSuppressCoercions $ \case - True -> angleBrackets (text "Co:" <> int (coercionSize co)) <+> dcolon <+> co_type - False -> parens $ sep [ppr co, dcolon <+> co_type] - where - co_type = sdocOption sdocSuppressCoercionTypes $ \case - True -> ellipsis - False -> ppr (coercionType co) +-- Print a coercion with its type (unless suppressed by -dsuppress-coercion-types) +-- Honour -dsuppress-coercions +-- Placed here because it needs GHC.Core.Coercion.coercionType +pprOptCo co = sdocOption sdocSuppressCoercionTypes $ \case + True -> pprParendCo co + False -> parens (sep [pprCo co, dcolon <+> pp_co_type]) + where + pp_co_type = ppr (coercionType co) ppr_id_occ :: (SDoc -> SDoc) -> Id -> SDoc ppr_id_occ add_par id ===================================== compiler/GHC/Core/TyCo/Ppr.hs ===================================== @@ -132,8 +132,14 @@ tidyToIfaceTypeX env ty = toIfaceTypeX (mkVarSet free_tcvs) (tidyType env' ty) ------------ pprCo, pprParendCo :: Coercion -> SDoc -pprCo co = getPprStyle $ \ sty -> pprIfaceCoercion (tidyToIfaceCoSty co sty) -pprParendCo co = getPprStyle $ \ sty -> pprParendIfaceCoercion (tidyToIfaceCoSty co sty) +-- Print a coercion without its type +-- Honour -dsuppress-coercions +pprCo co = sdocOption sdocSuppressCoercions $ \case + True -> angleBrackets (text "Co:" <> int (coercionSize co)) + False -> getPprStyle $ \ sty -> pprIfaceCoercion (tidyToIfaceCoSty co sty) +pprParendCo co = sdocOption sdocSuppressCoercions $ \case + True -> angleBrackets (text "Co:" <> int (coercionSize co)) + False -> getPprStyle $ \ sty -> pprParendIfaceCoercion (tidyToIfaceCoSty co sty) tidyToIfaceCoSty :: Coercion -> PprStyle -> IfaceCoercion tidyToIfaceCoSty co sty ===================================== compiler/GHC/Core/TyCo/Rep.hs ===================================== @@ -1640,7 +1640,7 @@ Here, co3 = UnivCo ProofIrrelProv Nominal (CoercionTy co1) (CoercionTy co2) [co5] where co5 :: (a1 ~# Bool) ~# (a2 ~# Bool) - co5 = TyConAppCo Nominal (~#) [, , co4, <Bool>] + co5 = TyConAppCo Nominal (~#) [, , co4, <Bool>] Note [The importance of tracking UnivCo dependencies] ===================================== testsuite/tests/codeGen/should_compile/T25177.stderr ===================================== @@ -11,7 +11,7 @@ lvl = foo d bar1 = \ x eta -> case lvl of { W# ipv -> (# eta, () #) } -bar = bar1 `cast` Co:6 :: ... +bar = bar1 `cast` Co:6 ===================================== testsuite/tests/numeric/should_compile/T15547.stderr ===================================== @@ -5,25 +5,25 @@ Result size of Tidy Core nat2Word# = \ @n $dKnownNat p1 -> - naturalToWord# ((natSing $dKnownNat) `cast` Co:2 :: ...) + naturalToWord# ((natSing $dKnownNat) `cast` Co:2) foo = \ ds -> 18## fd = \ @n $dKnownNat ds -> - naturalToWord# ((natSing $dKnownNat) `cast` Co:6 :: ...) + naturalToWord# ((natSing $dKnownNat) `cast` Co:6) d = \ ds -> 3## fm = \ @n $dKnownNat ds -> - naturalToWord# ((natSing $dKnownNat) `cast` Co:8 :: ...) + naturalToWord# ((natSing $dKnownNat) `cast` Co:8) m = \ ds -> 9## fp = \ @n $dKnownNat ds -> - naturalToWord# ((natSing $dKnownNat) `cast` Co:10 :: ...) + naturalToWord# ((natSing $dKnownNat) `cast` Co:10) p = \ ds -> 512## ===================================== testsuite/tests/simplCore/should_compile/DataToTagFamilyScrut.stderr ===================================== @@ -5,7 +5,7 @@ Result size of Tidy Core testFun = \ @x v -> - case v `cast` Co:2 :: ... of { + case v `cast` Co:2 of { __DEFAULT -> 47#; C0 ipv -> -3#; C2 -> 13#; ===================================== testsuite/tests/simplCore/should_compile/T14978.stdout ===================================== @@ -1,2 +1,2 @@ foo :: Goof Int -foo = T14978.Goof @Int @~Co:1 :: Int GHC.Internal.Prim.~# Int +foo = T14978.Goof @Int @~(Co:1 :: Int GHC.Internal.Prim.~# Int) ===================================== testsuite/tests/simplCore/should_compile/T18013.stderr ===================================== @@ -161,11 +161,11 @@ T18013.$wmapMaybeRule @s @(Maybe b) ww2 (GHC.Internal.Maybe.Nothing @b) #); Just x -> case ((wild s2 x) - `cast` Co:4 :: IO (Result s b) - ~R# (GHC.Internal.Prim.State# GHC.Internal.Prim.RealWorld - -> (# GHC.Internal.Prim.State# - GHC.Internal.Prim.RealWorld, - Result s b #))) + `cast` (Co:4 + :: IO (Result s b) + ~R# (GHC.Internal.Prim.State# GHC.Internal.Prim.RealWorld + -> (# GHC.Internal.Prim.State# GHC.Internal.Prim.RealWorld, + Result s b #)))) s1 of { (# ipv, ipv1 #) -> @@ -175,12 +175,13 @@ T18013.$wmapMaybeRule } } }) - `cast` Co:13 :: (s - -> Maybe a - -> GHC.Internal.Prim.State# GHC.Internal.Prim.RealWorld - -> (# GHC.Internal.Prim.State# GHC.Internal.Prim.RealWorld, - Result s (Maybe b) #)) - ~R# (s -> Maybe a -> IO (Result s (Maybe b)))) + `cast` (Co:13 + :: (s + -> Maybe a + -> GHC.Internal.Prim.State# GHC.Internal.Prim.RealWorld + -> (# GHC.Internal.Prim.State# GHC.Internal.Prim.RealWorld, + Result s (Maybe b) #)) + ~R# (s -> Maybe a -> IO (Result s (Maybe b))))) } } ===================================== testsuite/tests/simplCore/should_compile/T24229a.stderr ===================================== @@ -15,8 +15,8 @@ foo = \ @a ds ds1 -> case ds of { I# ww -> case ww of ds2 { - __DEFAULT -> case ds1 `cast` Co:4 :: ... of { (x, y) -> case foo_$s$wfoo (-# ds2 1#) y x of { (# ww1 #) -> Just ww1 } }; - 0# -> Just (ds1 `cast` Co:4 :: ...) + __DEFAULT -> case ds1 `cast` Co:4 of { (x, y) -> case foo_$s$wfoo (-# ds2 1#) y x of { (# ww1 #) -> Just ww1 } }; + 0# -> Just (ds1 `cast` Co:4) } } ===================================== testsuite/tests/simplCore/should_compile/T24229b.stderr ===================================== @@ -15,8 +15,8 @@ foo = \ @a ds ds1 -> case ds of { I# ww -> case ww of ds2 { - __DEFAULT -> case ds1 `cast` Co:4 :: ... of { (x, y) -> case foo_$s$wfoo (-# ds2 1#) y x of { (# ww1 #) -> Just ww1 } }; - 0# -> Just (ds1 `cast` Co:4 :: ...) + __DEFAULT -> case ds1 `cast` Co:4 of { (x, y) -> case foo_$s$wfoo (-# ds2 1#) y x of { (# ww1 #) -> Just ww1 } }; + 0# -> Just (ds1 `cast` Co:4) } } View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/4ebfc47842229a94a28c459806d9d8b... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/4ebfc47842229a94a28c459806d9d8b... You're receiving this email because of your account on gitlab.haskell.org.