Simon Peyton Jones pushed to branch wip/24279 at Glasgow Haskell Compiler / GHC
Commits:
bb084298 by Simon Peyton Jones at 2025-11-08T11:41:44+00:00
Make TYPE and CONSTRAINT apart again
- - - - -
9 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
- testsuite/tests/typecheck/should_fail/T24279.hs
- 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,6 +2891,8 @@ 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) }
+ -- ToDo: I don't understand this comment; and in any case, Type
+ -- and Constraint now are apart
-- 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
=====================================
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
=====================================
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/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, [''])
test('T24318', normal, compile_fail, [''])
# all the various do expansion fail messages
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/bb0842989b6a7a78fac7d94725beb562...
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/bb0842989b6a7a78fac7d94725beb562...
You're receiving this email because of your account on gitlab.haskell.org.
