Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC Commits: a00840ea by Simon Peyton Jones at 2025-11-14T15:23:56+00:00 Make TYPE and CONSTRAINT apart again This patch finally fixes #24279. * The story started with #11715 * Then #21623 articulated a plan, which made Type and Constraint not-apart; a horrible hack but it worked. The main patch was commit 778c6adca2c995cd8a1b84394d4d5ca26b915dac Author: Simon Peyton Jones Date: Wed Nov 9 10:33:22 2022 +0000 Type vs Constraint: finally nailed * #24279 reported a bug in the above big commit; this small patch fixes it commit af6932d6c068361c6ae300d52e72fbe13f8e1f18 Author: Simon Peyton Jones Date: Mon Jan 8 10:49:49 2024 +0000 Make TYPE and CONSTRAINT not-apart Issue #24279 showed up a bug in the logic in GHC.Core.Unify.unify_ty which is supposed to make TYPE and CONSTRAINT be not-apart. * Then !10479 implemented "unary classes". * That change in turn allows us to make Type and Constraint apart again, cleaning up the compiler and allowing a little bit more expressiveness. It fixes the original hope in #24279, namely that `Type` and `Constraint` should be distinct throughout. - - - - - 14 changed files: - compiler/GHC/Builtin/Types/Prim.hs - compiler/GHC/Core/Coercion.hs - compiler/GHC/Core/Lint.hs - compiler/GHC/Core/RoughMap.hs - compiler/GHC/Core/Type.hs - compiler/GHC/Core/Unify.hs - compiler/GHC/Tc/Instance/Class.hs - docs/users_guide/9.16.1-notes.rst - testsuite/tests/indexed-types/should_fail/T21092.hs - − testsuite/tests/indexed-types/should_fail/T21092.stderr - testsuite/tests/indexed-types/should_fail/all.T - testsuite/tests/typecheck/should_fail/T24279.hs - − testsuite/tests/typecheck/should_fail/T24279.stderr - testsuite/tests/typecheck/should_fail/all.T Changes: ===================================== compiler/GHC/Builtin/Types/Prim.hs ===================================== @@ -752,8 +752,9 @@ Specifically (a ~# b) :: CONSTRAINT (TupleRep []) Wrinkles -(W1) Type and Constraint are considered distinct throughout GHC. But they - are not /apart/: see Note [Type and Constraint are not apart] +(W1) Type and Constraint are considered distinct throughout GHC. + That wasn't always the case: + see Historical Note [Type and Constraint are not apart] (W2) We need two absent-error Ids, aBSENT_ERROR_ID for types of kind Type, and aBSENT_CONSTRAINT_ERROR_ID for types of kind Constraint. @@ -768,8 +769,24 @@ Wrinkles of type TYPE rr. See (CPR2) in Note [Which types are unboxed?] in GHC.Core.Opt.WorkWrap.Utils. -Note [Type and Constraint are not apart] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +------------------------------------------------------------- +Historical Note [Type and Constraint are not apart] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Nov 2025: + In the past, Type and Constraint were carefully coonsiderd to be + not /apart/. But the necessity for that vanished with unary classes + (see Note [Unary class magic]), done in + + commit 9bd7fcc518111a1549c98720c222cdbabd32ed46 + Author: Simon Peyton Jones + Date: Tue Apr 15 17:43:46 2025 +0100 + Implement unary classes + + So now Type and Constraint are simply distinct type constructors, just as + much as Int and Bool. + + The rest of this Note is preserved for historical interest. + Type and Constraint are not equal (eqType) but they are not /apart/ either. Reason (c.f. #7451): @@ -841,6 +858,9 @@ Wrinkles So in GHC.Tc.Instance.Class.matchTypeable, Type and Constraint are treated as separate TyCons; i.e. given no special treatment. +End of Historical Note +------------------------------------------------------------- + Note [RuntimeRep polymorphism] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Generally speaking, you can't be polymorphic in `RuntimeRep`. E.g ===================================== compiler/GHC/Core/Coercion.hs ===================================== @@ -641,11 +641,6 @@ eqTyConRole tc -- | Given a coercion `co :: (t1 :: TYPE r1) ~ (t2 :: TYPE r2)` -- produce a coercion `rep_co :: r1 ~ r2` --- But actually it is possible that --- co :: (t1 :: CONSTRAINT r1) ~ (t2 :: CONSTRAINT r2) --- or co :: (t1 :: TYPE r1) ~ (t2 :: CONSTRAINT r2) --- or co :: (t1 :: CONSTRAINT r1) ~ (t2 :: TYPE r2) --- See Note [mkRuntimeRepCo] mkRuntimeRepCo :: HasDebugCallStack => Coercion -> Coercion mkRuntimeRepCo co = assert (isTYPEorCONSTRAINT k1 && isTYPEorCONSTRAINT k2) $ @@ -654,26 +649,6 @@ mkRuntimeRepCo co kind_co = mkKindCo co -- kind_co :: TYPE r1 ~ TYPE r2 Pair k1 k2 = coercionKind kind_co -{- Note [mkRuntimeRepCo] -~~~~~~~~~~~~~~~~~~~~~~~~ -Given - class C a where { op :: Maybe a } -we will get an axiom - axC a :: (C a :: CONSTRAINT r1) ~ (Maybe a :: TYPE r2) -(See Note [Type and Constraint are not apart] in GHC.Builtin.Types.Prim.) - -Then we may call mkRuntimeRepCo on (axC ty), and that will return - mkSelCo (SelTyCon 0 Nominal) (Kind (axC ty)) :: r1 ~ r2 - -So mkSelCo needs to be happy with decomposing a coercion of kind - CONSTRAINT r1 ~ TYPE r2 - -Hence the use of `tyConIsTYPEorCONSTRAINT` in the assertion `good_call` -in `mkSelCo`. See #23018 for a concrete example. (In this context it's -important that TYPE and CONSTRAINT have the same arity and kind, not -merely that they are not-apart; otherwise SelCo would not make sense.) --} - isReflCoVar_maybe :: Var -> Maybe Coercion -- If cv :: t~t then isReflCoVar_maybe cv = Just (Refl t) -- Works on all kinds of Vars, not just CoVars @@ -1305,8 +1280,7 @@ mkSelCo_maybe cs co , Just (tc2, tys2) <- splitTyConApp_maybe ty2 , let { len1 = length tys1 ; len2 = length tys2 } - = (tc1 == tc2 || (tyConIsTYPEorCONSTRAINT tc1 && tyConIsTYPEorCONSTRAINT tc2)) - -- tyConIsTYPEorCONSTRAINT: see Note [mkRuntimeRepCo] + = tc1 == tc2 && len1 == len2 && n < len1 && 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 hang (text "Inhomogeneous axiom") 2 (text "lhs:" <+> ppr lhs <+> dcolon <+> ppr lhs_kind $$ text "rhs:" <+> ppr rhs <+> dcolon <+> ppr rhs_kind) } - -- Type and Constraint are not Apart, so this test allows - -- the newtype axiom for a single-method class. Indeed the - -- whole reason Type and Constraint are not Apart is to allow - -- such axioms! --- these checks do not apply to newtype axioms lint_family_branch :: TyCon -> CoAxBranch -> LintM () +-- These checks do not apply to newtype axioms lint_family_branch fam_tc br@(CoAxBranch { cab_tvs = tvs , cab_eta_tvs = eta_tvs , cab_cvs = cvs ===================================== compiler/GHC/Core/RoughMap.hs ===================================== @@ -36,7 +36,6 @@ import GHC.Core.Type import GHC.Utils.Outputable import GHC.Types.Name import GHC.Types.Name.Env -import GHC.Builtin.Types.Prim( cONSTRAINTTyConName, tYPETyConName ) import Control.Monad (join) import Data.Data (Data) @@ -347,16 +346,7 @@ typeToRoughMatchTc ty roughMatchTyConName :: TyCon -> Name roughMatchTyConName tc - | tc_name == cONSTRAINTTyConName - = tYPETyConName -- TYPE and CONSTRAINT are not apart, so they must use - -- the same rough-map key. We arbitrarily use TYPE. - -- See Note [Type and Constraint are not apart] - -- wrinkle (W1) in GHC.Builtin.Types.Prim - | otherwise - = assertPpr (isGenerativeTyCon tc Nominal) (ppr tc) tc_name - where - tc_name = tyConName tc - + = assertPpr (isGenerativeTyCon tc Nominal) (ppr tc) (tyConName tc) -- | Trie of @[RoughMatchTc]@ -- ===================================== compiler/GHC/Core/Type.hs ===================================== @@ -1421,8 +1421,6 @@ piResultTy ty arg = case piResultTy_maybe ty arg of Nothing -> pprPanic "piResultTy" (ppr ty $$ ppr arg) piResultTy_maybe :: Type -> Type -> Maybe Type --- We don't need a 'tc' version, because --- this function behaves the same for Type and Constraint piResultTy_maybe ty arg = case coreFullView ty of FunTy { ft_res = res } -> Just res ===================================== compiler/GHC/Core/Unify.hs ===================================== @@ -27,7 +27,6 @@ import GHC.Prelude import GHC.Types.Var import GHC.Types.Var.Env import GHC.Types.Var.Set -import GHC.Builtin.Names( tYPETyConKey, cONSTRAINTTyConKey ) import GHC.Core.Type hiding ( getTvSubstEnv ) import GHC.Core.Coercion hiding ( getCvSubstEnv ) import GHC.Core.Predicate( scopedSort ) @@ -98,8 +97,6 @@ of ways. Here we summarise, but see Note [Specification of unification]. See Note [Apartness and type families] * MARInfinite (occurs check): See Note [Infinitary substitutions] - * MARTypeVsConstraint: - See Note [Type and Constraint are not apart] in GHC.Builtin.Types.Prim * MARCast (obscure): See (KCU2) in Note [Kind coercions in Unify] @@ -997,16 +994,12 @@ data UnifyResultM a = Unifiable a -- the subst that unifies the types -- | Why are two types 'MaybeApart'? 'MARInfinite' takes precedence: -- This is used (only) in Note [Infinitary substitution in lookup] in GHC.Core.InstEnv --- As of Feb 2022, we never differentiate between MARTypeFamily and MARTypeVsConstraint; --- it's really only MARInfinite that's interesting here. +-- It's really only MARInfinite that's interesting here. data MaybeApartReason = MARTypeFamily -- ^ matching e.g. F Int ~? Bool | MARInfinite -- ^ matching e.g. a ~? Maybe a - | MARTypeVsConstraint -- ^ matching Type ~? Constraint or the arrow types - -- See Note [Type and Constraint are not apart] in GHC.Builtin.Types.Prim - | MARCast -- ^ Very obscure. -- See (KCU2) in Note [Kind coercions in Unify] @@ -1015,13 +1008,11 @@ combineMAR :: MaybeApartReason -> MaybeApartReason -> MaybeApartReason -- See (UR1) in Note [Unification result] for why MARInfinite wins combineMAR MARInfinite _ = MARInfinite -- MARInfinite wins combineMAR MARTypeFamily r = r -- Otherwise it doesn't really matter -combineMAR MARTypeVsConstraint r = r combineMAR MARCast r = r instance Outputable MaybeApartReason where ppr MARTypeFamily = text "MARTypeFamily" ppr MARInfinite = text "MARInfinite" - ppr MARTypeVsConstraint = text "MARTypeVsConstraint" ppr MARCast = text "MARCast" instance Semigroup MaybeApartReason where @@ -1729,30 +1720,6 @@ unify_ty env ty1 ty2 kco ; unify_tc_app env tc1 tys1 tys2 } - -- TYPE and CONSTRAINT are not Apart - -- See Note [Type and Constraint are not apart] in GHC.Builtin.Types.Prim - -- NB: at this point we know that the two TyCons do not match - | Just (tc1,_) <- mb_tc_app1, let u1 = tyConUnique tc1 - , Just (tc2,_) <- mb_tc_app2, let u2 = tyConUnique tc2 - , (u1 == tYPETyConKey && u2 == cONSTRAINTTyConKey) || - (u2 == tYPETyConKey && u1 == cONSTRAINTTyConKey) - = maybeApart MARTypeVsConstraint - -- We don't bother to look inside; wrinkle (W3) in GHC.Builtin.Types.Prim - -- Note [Type and Constraint are not apart] - - -- The arrow types are not Apart - -- See Note [Type and Constraint are not apart] in GHC.Builtin.Types.Prim - -- wrinkle (W2) - -- NB1: at this point we know that the two TyCons do not match - -- NB2: In the common FunTy/FunTy case you might wonder if we want to go via - -- splitTyConApp_maybe. But yes we do: we need to look at those implied - -- kind argument in order to satisfy (Unification Kind Invariant) - | FunTy {} <- ty1 - , FunTy {} <- ty2 - = maybeApart MARTypeVsConstraint - -- We don't bother to look inside; wrinkle (W3) in GHC.Builtin.Types.Prim - -- Note [Type and Constraint are not apart] - where mb_tc_app1 = splitTyConApp_maybe ty1 mb_tc_app2 = splitTyConApp_maybe ty2 ===================================== compiler/GHC/Tc/Instance/Class.hs ===================================== @@ -963,11 +963,6 @@ matchTypeable clas [k,t] -- clas = Typeable | k `eqType` naturalTy = doTyLit knownNatClassName t | k `eqType` typeSymbolKind = doTyLit knownSymbolClassName t | k `eqType` charTy = doTyLit knownCharClassName t - - -- TyCon applied to its kind args - -- No special treatment of Type and Constraint; they get distinct TypeReps - -- see wrinkle (W4) of Note [Type and Constraint are not apart] - -- in GHC.Builtin.Types.Prim. | Just (tc, ks) <- splitTyConApp_maybe t -- See Note [Typeable (T a b c)] , onlyNamedBndrsApplied tc ks = doTyConApp clas t tc ks ===================================== docs/users_guide/9.16.1-notes.rst ===================================== @@ -16,6 +16,17 @@ Language result, you may need to enable :extension:`DataKinds` in code that did not previously require it. +- ``Type`` and ``Constraint`` are now (at last) completely distinct types, just as much + as ``Int`` and ``Bool``. For example, you can now + write:: + + type family F a + + type instance F Type = Int + type instance F Constraint = Bool + + which was previously rejected with "Conflicting family instance declarations". + Compiler ~~~~~~~~ ===================================== testsuite/tests/indexed-types/should_fail/T21092.hs ===================================== @@ -7,3 +7,5 @@ type family F a type instance F Type = Int type instance F Constraint = Bool + +-- Nov 2025: Type and Constraint are now Apart (#24279) ===================================== testsuite/tests/indexed-types/should_fail/T21092.stderr deleted ===================================== @@ -1,5 +0,0 @@ - -T21092.hs:8:15: error: [GHC-34447] - Conflicting family instance declarations: - F (*) = Int -- Defined at T21092.hs:8:15 - 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, ['']) test('T8368a', normal, compile_fail, ['']) test('T8518', normal, compile_fail, ['']) test('T9036', normal, compile_fail, ['']) -test('T21092', normal, compile_fail, ['']) +test('T21092', normal, compile, ['']) # Now compiles fine test('T9167', normal, compile_fail, ['']) test('T9171', normal, compile_fail, ['']) test('T9097', normal, compile_fail, ['']) ===================================== testsuite/tests/typecheck/should_fail/T24279.hs ===================================== @@ -13,7 +13,7 @@ type G :: Type -> RuntimeRep -> Type type family G a where G (a b) = a --- Should be rejected +-- Now (Nov 2025) accepted foo :: (F (G Constraint)) -> Bool foo x = x @@ -22,10 +22,10 @@ type family H a b where H a a = Int H a b = Bool --- Should be rejected -bar1 :: H TYPE CONSTRAINT -> Int +-- Now (Nov 2025) accepted +bar1 :: H TYPE CONSTRAINT -> Bool bar1 x = x --- Should be rejected -bar2 :: H Type Constraint -> Int +-- Now (Nov 2025) accepted +bar2 :: H Type Constraint -> Bool bar2 x = x ===================================== testsuite/tests/typecheck/should_fail/T24279.stderr deleted ===================================== @@ -1,19 +0,0 @@ - -T24279.hs:18:9: error: [GHC-83865] - • Couldn't match type ‘F CONSTRAINT’ with ‘Bool’ - Expected: Bool - Actual: F (G Constraint) - • In the expression: x - In an equation for ‘foo’: foo x = x - -T24279.hs:27:10: error: [GHC-83865] - • Couldn't match expected type ‘Int’ - with actual type ‘H TYPE CONSTRAINT’ - • In the expression: x - In an equation for ‘bar1’: bar1 x = x - -T24279.hs:31:10: error: [GHC-83865] - • Couldn't match expected type ‘Int’ - with actual type ‘H (*) Constraint’ - • In the expression: x - In an equation for ‘bar2’: bar2 x = x ===================================== testsuite/tests/typecheck/should_fail/all.T ===================================== @@ -718,7 +718,7 @@ test('T24064', normal, compile_fail, ['']) test('T24090a', normal, compile_fail, ['']) test('T24090b', normal, compile, ['']) # scheduled to become an actual error in GHC 9.16 test('T24298', normal, compile_fail, ['']) -test('T24279', normal, compile_fail, ['']) +test('T24279', normal, compile, ['']) # Now accepted (Nov 2025) test('T24318', normal, compile_fail, ['']) # all the various do expansion fail messages View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/a00840eacb6e98f0cdc9867db4ebdc66... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/a00840eacb6e98f0cdc9867db4ebdc66... You're receiving this email because of your account on gitlab.haskell.org.