Simon Peyton Jones pushed to branch wip/24279 at Glasgow Haskell Compiler / GHC

Commits:

14 changed files:

Changes:

  • compiler/GHC/Builtin/Types/Prim.hs
    ... ... @@ -752,8 +752,9 @@ Specifically (a ~# b) :: CONSTRAINT (TupleRep [])
    752 752
    753 753 
     Wrinkles
    754 754
    755 
    -(W1) Type and Constraint are considered distinct throughout GHC. But they
    756 
    -     are not /apart/: see Note [Type and Constraint are not apart]
    755 
    +(W1) Type and Constraint are considered distinct throughout GHC.
    756 
    +     That wasn't always the case:
    757 
    +          see Historical Note [Type and Constraint are not apart]
    757 758
    758 759 
     (W2) We need two absent-error Ids, aBSENT_ERROR_ID for types of kind Type, and
    759 760 
          aBSENT_CONSTRAINT_ERROR_ID for types of kind Constraint.
    ... ... @@ -768,8 +769,24 @@ Wrinkles
    768 769 
          of type TYPE rr. See (CPR2) in Note [Which types are unboxed?] in
    769 770 
          GHC.Core.Opt.WorkWrap.Utils.
    770 771
    771 
    -Note [Type and Constraint are not apart]
    772 
    -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    772 
    +-------------------------------------------------------------
    773 
    +Historical Note [Type and Constraint are not apart]
    774 
    +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    775 
    +Nov 2025:
    776 
    +  In the past, Type and Constraint were carefully coonsiderd to be
    777 
    +  not /apart/.  But the necessity for that vanished with unary classes
    778 
    +  (see Note [Unary class magic]), done in
    779 
    +
    780 
    +     commit 9bd7fcc518111a1549c98720c222cdbabd32ed46
    781 
    +     Author: Simon Peyton Jones <simon.peytonjones@gmail.com>
    782 
    +     Date:   Tue Apr 15 17:43:46 2025 +0100
    783 
    +     Implement unary classes
    784 
    +
    785 
    +  So now Type and Constraint are simply distinct type constructors, just as
    786 
    +  much as Int and Bool.
    787 
    +
    788 
    +  The rest of this Note is preserved for historical interest.
    789 
    +
    773 790 
     Type and Constraint are not equal (eqType) but they are not /apart/
    774 791 
     either. Reason (c.f. #7451):
    775 792
    ... ... @@ -841,6 +858,9 @@ Wrinkles
    841 858 
          So in GHC.Tc.Instance.Class.matchTypeable, Type and Constraint are
    842 859 
          treated as separate TyCons; i.e. given no special treatment.
    843 860
    861 
    +End of Historical Note
    862 
    +-------------------------------------------------------------
    863 
    +
    844 864 
     Note [RuntimeRep polymorphism]
    845 865 
     ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    846 866 
     Generally speaking, you can't be polymorphic in `RuntimeRep`.  E.g

  • compiler/GHC/Core/Coercion.hs
    ... ... @@ -641,11 +641,6 @@ eqTyConRole tc
    641 641
    642 642 
     -- | Given a coercion `co :: (t1 :: TYPE r1) ~ (t2 :: TYPE r2)`
    643 643 
     -- produce a coercion `rep_co :: r1 ~ r2`
    644 
    --- But actually it is possible that
    645 
    ---     co :: (t1 :: CONSTRAINT r1) ~ (t2 :: CONSTRAINT r2)
    646 
    --- or  co :: (t1 :: TYPE r1)       ~ (t2 :: CONSTRAINT r2)
    647 
    --- or  co :: (t1 :: CONSTRAINT r1) ~ (t2 :: TYPE r2)
    648 
    --- See Note [mkRuntimeRepCo]
    649 644 
     mkRuntimeRepCo :: HasDebugCallStack => Coercion -> Coercion
    650 645 
     mkRuntimeRepCo co
    651 646 
       = assert (isTYPEorCONSTRAINT k1 && isTYPEorCONSTRAINT k2) $
    ... ... @@ -654,26 +649,6 @@ mkRuntimeRepCo co
    654 649 
         kind_co = mkKindCo co  -- kind_co :: TYPE r1 ~ TYPE r2
    655 650 
         Pair k1 k2 = coercionKind kind_co
    656 651
    657 
    -{- Note [mkRuntimeRepCo]
    658 
    -~~~~~~~~~~~~~~~~~~~~~~~~
    659 
    -Given
    660 
    -   class C a where { op :: Maybe a }
    661 
    -we will get an axiom
    662 
    -   axC a :: (C a :: CONSTRAINT r1) ~ (Maybe a :: TYPE r2)
    663 
    -(See Note [Type and Constraint are not apart] in GHC.Builtin.Types.Prim.)
    664 
    -
    665 
    -Then we may call mkRuntimeRepCo on (axC ty), and that will return
    666 
    -   mkSelCo (SelTyCon 0 Nominal) (Kind (axC ty)) :: r1 ~ r2
    667 
    -
    668 
    -So mkSelCo needs to be happy with decomposing a coercion of kind
    669 
    -   CONSTRAINT r1 ~ TYPE r2
    670 
    -
    671 
    -Hence the use of `tyConIsTYPEorCONSTRAINT` in the assertion `good_call`
    672 
    -in `mkSelCo`. See #23018 for a concrete example.  (In this context it's
    673 
    -important that TYPE and CONSTRAINT have the same arity and kind, not
    674 
    -merely that they are not-apart; otherwise SelCo would not make sense.)
    675 
    --}
    676 
    -
    677 652 
     isReflCoVar_maybe :: Var -> Maybe Coercion
    678 653 
     -- If cv :: t~t then isReflCoVar_maybe cv = Just (Refl t)
    679 654 
     -- Works on all kinds of Vars, not just CoVars
    ... ... @@ -1305,8 +1280,7 @@ mkSelCo_maybe cs co
    1305 1280 
            , Just (tc2, tys2) <- splitTyConApp_maybe ty2
    1306 1281 
            , let { len1 = length tys1
    1307 1282 
                  ; len2 = length tys2 }
    1308 
    -       =  (tc1 == tc2 || (tyConIsTYPEorCONSTRAINT tc1 && tyConIsTYPEorCONSTRAINT tc2))
    1309 
    -                      -- tyConIsTYPEorCONSTRAINT: see Note [mkRuntimeRepCo]
    1283 
    +       =  tc1 == tc2
    1310 1284 
            && len1 == len2
    1311 1285 
            && n < len1
    1312 1286 
            && r == tyConRole (coercionRole co) tc1 n

  • compiler/GHC/Core/Lint.hs
    ... ... @@ -2891,13 +2891,9 @@ lint_branch ax_tc (CoAxBranch { cab_tvs = tvs, cab_cvs = cvs
    2891 2891 
              hang (text "Inhomogeneous axiom")
    2892 2892 
                 2 (text "lhs:" <+> ppr lhs <+> dcolon <+> ppr lhs_kind $$
    2893 2893 
                    text "rhs:" <+> ppr rhs <+> dcolon <+> ppr rhs_kind) }
    2894 
    -         -- Type and Constraint are not Apart, so this test allows
    2895 
    -         -- the newtype axiom for a single-method class.  Indeed the
    2896 
    -         -- whole reason Type and Constraint are not Apart is to allow
    2897 
    -         -- such axioms!
    2898 2894
    2899 
    --- these checks do not apply to newtype axioms
    2900 2895 
     lint_family_branch :: TyCon -> CoAxBranch -> LintM ()
    2896 
    +-- These checks do not apply to newtype axioms
    2901 2897 
     lint_family_branch fam_tc br@(CoAxBranch { cab_tvs     = tvs
    2902 2898 
                                              , cab_eta_tvs = eta_tvs
    2903 2899 
                                              , cab_cvs     = cvs

  • compiler/GHC/Core/RoughMap.hs
    ... ... @@ -36,7 +36,6 @@ import GHC.Core.Type
    36 36 
     import GHC.Utils.Outputable
    37 37 
     import GHC.Types.Name
    38 38 
     import GHC.Types.Name.Env
    39 
    -import GHC.Builtin.Types.Prim( cONSTRAINTTyConName, tYPETyConName )
    40 39
    41 40 
     import Control.Monad (join)
    42 41 
     import Data.Data (Data)
    ... ... @@ -347,16 +346,7 @@ typeToRoughMatchTc ty
    347 346
    348 347 
     roughMatchTyConName :: TyCon -> Name
    349 348 
     roughMatchTyConName tc
    350 
    -  | tc_name == cONSTRAINTTyConName
    351 
    -  = tYPETyConName  -- TYPE and CONSTRAINT are not apart, so they must use
    352 
    -                   -- the same rough-map key. We arbitrarily use TYPE.
    353 
    -                   -- See Note [Type and Constraint are not apart]
    354 
    -                   -- wrinkle (W1) in GHC.Builtin.Types.Prim
    355 
    -  | otherwise
    356 
    -  = assertPpr (isGenerativeTyCon tc Nominal) (ppr tc) tc_name
    357 
    -  where
    358 
    -    tc_name = tyConName tc
    359 
    -
    349 
    +  = assertPpr (isGenerativeTyCon tc Nominal) (ppr tc) (tyConName tc)
    360 350
    361 351 
     -- | Trie of @[RoughMatchTc]@
    362 352 
     --

  • compiler/GHC/Core/Type.hs
    ... ... @@ -1421,8 +1421,6 @@ piResultTy ty arg = case piResultTy_maybe ty arg of
    1421 1421 
                           Nothing  -> pprPanic "piResultTy" (ppr ty $$ ppr arg)
    1422 1422
    1423 1423 
     piResultTy_maybe :: Type -> Type -> Maybe Type
    1424 
    --- We don't need a 'tc' version, because
    1425 
    --- this function behaves the same for Type and Constraint
    1426 1424 
     piResultTy_maybe ty arg = case coreFullView ty of
    1427 1425 
       FunTy { ft_res = res } -> Just res
    1428 1426

  • compiler/GHC/Core/Unify.hs
    ... ... @@ -27,7 +27,6 @@ import GHC.Prelude
    27 27 
     import GHC.Types.Var
    28 28 
     import GHC.Types.Var.Env
    29 29 
     import GHC.Types.Var.Set
    30 
    -import GHC.Builtin.Names( tYPETyConKey, cONSTRAINTTyConKey )
    31 30 
     import GHC.Core.Type     hiding ( getTvSubstEnv )
    32 31 
     import GHC.Core.Coercion hiding ( getCvSubstEnv )
    33 32 
     import GHC.Core.Predicate( scopedSort )
    ... ... @@ -98,8 +97,6 @@ of ways. Here we summarise, but see Note [Specification of unification].
    98 97 
              See Note [Apartness and type families]
    99 98 
         * MARInfinite (occurs check):
    100 99 
              See Note [Infinitary substitutions]
    101 
    -    * MARTypeVsConstraint:
    102 
    -         See Note [Type and Constraint are not apart] in GHC.Builtin.Types.Prim
    103 100 
         * MARCast (obscure):
    104 101 
              See (KCU2) in Note [Kind coercions in Unify]
    105 102
    ... ... @@ -997,16 +994,12 @@ data UnifyResultM a = Unifiable a -- the subst that unifies the types
    997 994
    998 995 
     -- | Why are two types 'MaybeApart'? 'MARInfinite' takes precedence:
    999 996 
     -- This is used (only) in Note [Infinitary substitution in lookup] in GHC.Core.InstEnv
    1000 
    --- As of Feb 2022, we never differentiate between MARTypeFamily and MARTypeVsConstraint;
    1001 
    --- it's really only MARInfinite that's interesting here.
    997 
    +-- It's really only MARInfinite that's interesting here.
    1002 998 
     data MaybeApartReason
    1003 999 
       = MARTypeFamily   -- ^ matching e.g. F Int ~? Bool
    1004 1000
    1005 1001 
       | MARInfinite     -- ^ matching e.g. a ~? Maybe a
    1006 1002
    1007 
    -  | MARTypeVsConstraint  -- ^ matching Type ~? Constraint or the arrow types
    1008 
    -    -- See Note [Type and Constraint are not apart] in GHC.Builtin.Types.Prim
    1009 
    -
    1010 1003 
       | MARCast         -- ^ Very obscure.
    1011 1004 
         -- See (KCU2) in Note [Kind coercions in Unify]
    1012 1005
    ... ... @@ -1015,13 +1008,11 @@ combineMAR :: MaybeApartReason -> MaybeApartReason -> MaybeApartReason
    1015 1008 
     -- See (UR1) in Note [Unification result] for why MARInfinite wins
    1016 1009 
     combineMAR MARInfinite         _ = MARInfinite   -- MARInfinite wins
    1017 1010 
     combineMAR MARTypeFamily       r = r             -- Otherwise it doesn't really matter
    1018 
    -combineMAR MARTypeVsConstraint r = r
    1019 1011 
     combineMAR MARCast             r = r
    1020 1012
    1021 1013 
     instance Outputable MaybeApartReason where
    1022 1014 
       ppr MARTypeFamily       = text "MARTypeFamily"
    1023 1015 
       ppr MARInfinite         = text "MARInfinite"
    1024 
    -  ppr MARTypeVsConstraint = text "MARTypeVsConstraint"
    1025 1016 
       ppr MARCast             = text "MARCast"
    1026 1017
    1027 1018 
     instance Semigroup MaybeApartReason where
    ... ... @@ -1729,30 +1720,6 @@ unify_ty env ty1 ty2 kco
    1729 1720 
            ; unify_tc_app env tc1 tys1 tys2
    1730 1721 
            }
    1731 1722
    1732 
    -  -- TYPE and CONSTRAINT are not Apart
    1733 
    -  -- See Note [Type and Constraint are not apart] in GHC.Builtin.Types.Prim
    1734 
    -  -- NB: at this point we know that the two TyCons do not match
    1735 
    -  | Just (tc1,_) <- mb_tc_app1, let u1 = tyConUnique tc1
    1736 
    -  , Just (tc2,_) <- mb_tc_app2, let u2 = tyConUnique tc2
    1737 
    -  , (u1 == tYPETyConKey && u2 == cONSTRAINTTyConKey) ||
    1738 
    -    (u2 == tYPETyConKey && u1 == cONSTRAINTTyConKey)
    1739 
    -  = maybeApart MARTypeVsConstraint
    1740 
    -    -- We don't bother to look inside; wrinkle (W3) in GHC.Builtin.Types.Prim
    1741 
    -    -- Note [Type and Constraint are not apart]
    1742 
    -
    1743 
    -  -- The arrow types are not Apart
    1744 
    -  -- See Note [Type and Constraint are not apart] in GHC.Builtin.Types.Prim
    1745 
    -  --     wrinkle (W2)
    1746 
    -  -- NB1: at this point we know that the two TyCons do not match
    1747 
    -  -- NB2: In the common FunTy/FunTy case you might wonder if we want to go via
    1748 
    -  --      splitTyConApp_maybe.  But yes we do: we need to look at those implied
    1749 
    -  --      kind argument in order to satisfy (Unification Kind Invariant)
    1750 
    -  | FunTy {} <- ty1
    1751 
    -  , FunTy {} <- ty2
    1752 
    -  = maybeApart MARTypeVsConstraint
    1753 
    -    -- We don't bother to look inside; wrinkle (W3) in GHC.Builtin.Types.Prim
    1754 
    -    -- Note [Type and Constraint are not apart]
    1755 
    -
    1756 1723 
       where
    1757 1724 
         mb_tc_app1 = splitTyConApp_maybe ty1
    1758 1725 
         mb_tc_app2 = splitTyConApp_maybe ty2

  • compiler/GHC/Tc/Instance/Class.hs
    ... ... @@ -963,11 +963,6 @@ matchTypeable clas [k,t] -- clas = Typeable
    963 963 
       | k `eqType` naturalTy      = doTyLit knownNatClassName         t
    964 964 
       | k `eqType` typeSymbolKind = doTyLit knownSymbolClassName      t
    965 965 
       | k `eqType` charTy         = doTyLit knownCharClassName        t
    966 
    -
    967 
    -  -- TyCon applied to its kind args
    968 
    -  -- No special treatment of Type and Constraint; they get distinct TypeReps
    969 
    -  -- see wrinkle (W4) of Note [Type and Constraint are not apart]
    970 
    -  --     in GHC.Builtin.Types.Prim.
    971 966 
       | Just (tc, ks) <- splitTyConApp_maybe t -- See Note [Typeable (T a b c)]
    972 967 
       , onlyNamedBndrsApplied tc ks            = doTyConApp clas t tc ks
    973 968

  • docs/users_guide/9.16.1-notes.rst
    ... ... @@ -16,6 +16,17 @@ Language
    16 16 
       result, you may need to enable :extension:`DataKinds` in code that did not
    17 17 
       previously require it.
    18 18
    19 
    +- ``Type`` and ``Constraint`` are now (at last) completely distinct types, just as much
    20 
    +  as ``Int`` and ``Bool``.  For example, you can now
    21 
    +  write::
    22 
    +
    23 
    +    type family F a
    24 
    +
    25 
    +    type instance F Type = Int
    26 
    +    type instance F Constraint = Bool
    27 
    +
    28 
    +  which was previously rejected with "Conflicting family instance declarations".
    29 
    +
    19 30 
     Compiler
    20 31 
     ~~~~~~~~
    21 32

  • testsuite/tests/indexed-types/should_fail/T21092.hs
    ... ... @@ -7,3 +7,5 @@ type family F a
    7 7
    8 8 
     type instance F Type = Int
    9 9 
     type instance F Constraint = Bool
    10 
    +
    11 
    +-- Nov 2025: Type and Constraint are now Apart (#24279)

  • testsuite/tests/indexed-types/should_fail/T21092.stderr deleted
    1 
    -
    2 
    -T21092.hs:8:15: error: [GHC-34447]
    3 
    -    Conflicting family instance declarations:
    4 
    -      F (*) = Int -- Defined at T21092.hs:8:15
    5 
    -      F Constraint = Bool -- Defined at T21092.hs:9:15

  • testsuite/tests/indexed-types/should_fail/all.T
    ... ... @@ -107,7 +107,7 @@ test('T8368', normal, compile_fail, [''])
    107 107 
     test('T8368a', normal, compile_fail, [''])
    108 108 
     test('T8518', normal, compile_fail, [''])
    109 109 
     test('T9036', normal, compile_fail, [''])
    110 
    -test('T21092', normal, compile_fail, [''])
    110 
    +test('T21092', normal, compile, [''])   # Now compiles fine
    111 111 
     test('T9167', normal, compile_fail, [''])
    112 112 
     test('T9171', normal, compile_fail, [''])
    113 113 
     test('T9097', normal, compile_fail, [''])

  • testsuite/tests/typecheck/should_fail/T24279.hs
    ... ... @@ -13,7 +13,7 @@ type G :: Type -> RuntimeRep -> Type
    13 13 
     type family G a where
    14 14 
       G (a b) = a
    15 15
    16 
    --- Should be rejected
    16 
    +-- Now (Nov 2025) accepted
    17 17 
     foo :: (F (G Constraint)) -> Bool
    18 18 
     foo x = x
    19 19
    ... ... @@ -22,10 +22,10 @@ type family H a b where
    22 22 
       H a a = Int
    23 23 
       H a b = Bool
    24 24
    25 
    --- Should be rejected
    26 
    -bar1 :: H TYPE CONSTRAINT -> Int
    25 
    +-- Now (Nov 2025) accepted
    26 
    +bar1 :: H TYPE CONSTRAINT -> Bool
    27 27 
     bar1 x = x
    28 28
    29 
    --- Should be rejected
    30 
    -bar2 :: H Type Constraint -> Int
    29 
    +-- Now (Nov 2025) accepted
    30 
    +bar2 :: H Type Constraint -> Bool
    31 31 
     bar2 x = x

  • testsuite/tests/typecheck/should_fail/T24279.stderr deleted
    1 
    -
    2 
    -T24279.hs:18:9: error: [GHC-83865]
    3 
    -    • Couldn't match type ‘F CONSTRAINT’ with ‘Bool’
    4 
    -      Expected: Bool
    5 
    -        Actual: F (G Constraint)
    6 
    -    • In the expression: x
    7 
    -      In an equation for ‘foo’: foo x = x
    8 
    -
    9 
    -T24279.hs:27:10: error: [GHC-83865]
    10 
    -    • Couldn't match expected type ‘Int’
    11 
    -                  with actual type ‘H TYPE CONSTRAINT’
    12 
    -    • In the expression: x
    13 
    -      In an equation for ‘bar1’: bar1 x = x
    14 
    -
    15 
    -T24279.hs:31:10: error: [GHC-83865]
    16 
    -    • Couldn't match expected type ‘Int’
    17 
    -                  with actual type ‘H (*) Constraint’
    18 
    -    • In the expression: x
    19 
    -      In an equation for ‘bar2’: bar2 x = x

  • testsuite/tests/typecheck/should_fail/all.T
    ... ... @@ -718,7 +718,7 @@ test('T24064', normal, compile_fail, [''])
    718 718 
     test('T24090a', normal, compile_fail, [''])
    719 719 
     test('T24090b', normal, compile, ['']) # scheduled to become an actual error in GHC 9.16
    720 720 
     test('T24298', normal, compile_fail, [''])
    721 
    -test('T24279', normal, compile_fail, [''])
    721 
    +test('T24279', normal, compile, [''])  # Now accepted (Nov 2025)
    722 722 
     test('T24318', normal, compile_fail, [''])
    723 723
    724 724 
     # all the various do expansion fail messages

    • —
    View it on GitLab.
    You're receiving this email because of your account on gitlab.haskell.org. Manage all notifications · Help