[Git][ghc/ghc][wip/T21623-tycon] 3 commits: Fix decomposition of TyConApps
Andreas Klebinger (@AndreasK)
gitlab at gitlab.haskell.org
Mon Nov 28 16:27:31 UTC 2022
Andreas Klebinger pushed to branch wip/T21623-tycon at Glasgow Haskell Compiler / GHC
Commits:
d10dc6bd by Simon Peyton Jones at 2022-11-25T22:31:27+00:00
Fix decomposition of TyConApps
Ticket #22331 showed that we were being too eager to decompose
a Wanted TyConApp, leading to incompleteness in the solver.
To understand all this I ended up doing a substantial rewrite
of the old Note [Decomposing equalities], now reborn as
Note [Decomposing TyConApp equalities]. Plus rewrites of other
related Notes.
The actual fix is very minor and actually simplifies the code: in
`can_decompose` in `GHC.Tc.Solver.Canonical.canTyConApp`, we now call
`noMatchableIrreds`. A closely related refactor: we stop trying to
use the same "no matchable givens" function here as in
`matchClassInst`. Instead split into two much simpler functions.
- - - - -
2da5c38a by Will Hawkins at 2022-11-26T04:05:04-05:00
Redirect output of musttail attribute test
Compilation output from test for support of musttail attribute leaked to
the console.
- - - - -
95a58b68 by Simon Peyton Jones at 2022-11-28T17:25:18+01:00
Refactor TyCon to have a top-level product
This patch changes the representation of TyCon so that it has
a top-level product type, with a field that gives the details
(newtype, type family etc), #22458.
Not much change in allocation, but execution seems to be a bit
faster.
Includes a change to the haddock submodule to adjust for API changes.
- - - - -
16 changed files:
- compiler/GHC/Builtin/Types.hs
- compiler/GHC/Core/Map/Type.hs
- compiler/GHC/Core/Opt/WorkWrap/Utils.hs
- + compiler/GHC/Core/TyCo/FVs.hs-boot
- compiler/GHC/Core/TyCon.hs
- compiler/GHC/Iface/Make.hs
- compiler/GHC/Tc/Gen/Splice.hs
- compiler/GHC/Tc/Solver/Canonical.hs
- compiler/GHC/Tc/Solver/InertSet.hs
- compiler/GHC/Tc/Solver/Interact.hs
- compiler/GHC/Tc/TyCl.hs
- compiler/GHC/Tc/Utils/TcMType.hs
- m4/fp_musttail.m4
- + testsuite/tests/typecheck/should_compile/T22331.hs
- testsuite/tests/typecheck/should_compile/all.T
- utils/haddock
Changes:
=====================================
compiler/GHC/Builtin/Types.hs
=====================================
@@ -1038,12 +1038,11 @@ unboxedTupleKind = unboxedTupleSumKind tupleRepDataConTyCon
mk_tuple :: Boxity -> Int -> (TyCon,DataCon)
mk_tuple Boxed arity = (tycon, tuple_con)
where
- tycon = mkTupleTyCon tc_name tc_binders tc_res_kind tc_arity tuple_con
+ tycon = mkTupleTyCon tc_name tc_binders tc_res_kind tuple_con
BoxedTuple flavour
tc_binders = mkTemplateAnonTyConBinders (replicate arity liftedTypeKind)
tc_res_kind = liftedTypeKind
- tc_arity = arity
flavour = VanillaAlgTyCon (mkPrelTyConRepName tc_name)
dc_tvs = binderVars tc_binders
@@ -1061,7 +1060,7 @@ mk_tuple Boxed arity = (tycon, tuple_con)
mk_tuple Unboxed arity = (tycon, tuple_con)
where
- tycon = mkTupleTyCon tc_name tc_binders tc_res_kind tc_arity tuple_con
+ tycon = mkTupleTyCon tc_name tc_binders tc_res_kind tuple_con
UnboxedTuple flavour
-- See Note [Unboxed tuple RuntimeRep vars] in GHC.Core.TyCon
@@ -1070,8 +1069,6 @@ mk_tuple Unboxed arity = (tycon, tuple_con)
(\ks -> map mkTYPEapp ks)
tc_res_kind = unboxedTupleKind rr_tys
-
- tc_arity = arity * 2
flavour = VanillaAlgTyCon (mkPrelTyConRepName tc_name)
dc_tvs = binderVars tc_binders
@@ -1224,7 +1221,7 @@ unboxedSumKind = unboxedTupleSumKind sumRepDataConTyCon
mk_sum :: Arity -> (TyCon, Array ConTagZ DataCon)
mk_sum arity = (tycon, sum_cons)
where
- tycon = mkSumTyCon tc_name tc_binders tc_res_kind (arity * 2) tyvars (elems sum_cons)
+ tycon = mkSumTyCon tc_name tc_binders tc_res_kind (elems sum_cons)
UnboxedSumTyCon
tc_binders = mkTemplateTyConBinders (replicate arity runtimeRepTy)
=====================================
compiler/GHC/Core/Map/Type.hs
=====================================
@@ -271,7 +271,10 @@ eqDeBruijnType env_t1@(D env1 t1) env_t2@(D env2 t2) =
-> TEQ
_ -> TNEQ
- gos _ _ [] [] = TEQ
+ -- These bangs make 'gos' strict in the CMEnv, which in turn
+ -- keeps the CMEnv unboxed across the go/gos mutual recursion
+ -- (If you want a test case, T9872c really exercises this code.)
+ gos !_ !_ [] [] = TEQ
gos e1 e2 (ty1:tys1) (ty2:tys2) = go (D e1 ty1) (D e2 ty2) `andEq`
gos e1 e2 tys1 tys2
gos _ _ _ _ = TNEQ
=====================================
compiler/GHC/Core/Opt/WorkWrap/Utils.hs
=====================================
@@ -571,6 +571,11 @@ data UnboxingDecision unboxing_info
-- returned product was constructed, so unbox it.
| DropAbsent -- ^ The argument/field was absent. Drop it.
+instance Outputable i => Outputable (UnboxingDecision i) where
+ ppr DontUnbox = text "DontUnbox"
+ ppr DropAbsent = text "DropAbsent"
+ ppr (DoUnbox i) = text "DoUnbox" <> braces (ppr i)
+
-- | Do we want to create workers just for unlifting?
wwUseForUnlifting :: WwOpts -> WwUse
wwUseForUnlifting !opts
=====================================
compiler/GHC/Core/TyCo/FVs.hs-boot
=====================================
@@ -0,0 +1,6 @@
+module GHC.Core.TyCo.FVs where
+
+import GHC.Prelude ( Bool )
+import {-# SOURCE #-} GHC.Core.TyCo.Rep ( Type )
+
+noFreeVarsOfType :: Type -> Bool
=====================================
compiler/GHC/Core/TyCon.hs
=====================================
@@ -81,7 +81,7 @@ module GHC.Core.TyCon(
tyConKind,
tyConUnique,
tyConTyVars, tyConVisibleTyVars,
- tyConCType, tyConCType_maybe,
+ tyConCType_maybe,
tyConDataCons, tyConDataCons_maybe,
tyConSingleDataCon_maybe, tyConSingleDataCon,
tyConAlgDataCons_maybe,
@@ -96,7 +96,7 @@ module GHC.Core.TyCon(
tyConFamInst_maybe, tyConFamInstSig_maybe, tyConFamilyCoercion_maybe,
tyConFamilyResVar_maybe,
synTyConDefn_maybe, synTyConRhs_maybe,
- famTyConFlav_maybe, famTcResVar,
+ famTyConFlav_maybe,
algTyConRhs,
newTyConRhs, newTyConEtadArity, newTyConEtadRhs,
unwrapNewTyCon_maybe, unwrapNewTyConEtad_maybe,
@@ -104,7 +104,8 @@ module GHC.Core.TyCon(
algTcFields,
tyConPromDataConInfo,
tyConBinders, tyConResKind, tyConInvisTVBinders,
- tcTyConScopedTyVars, tcTyConIsPoly,
+ tcTyConScopedTyVars, isMonoTcTyCon,
+ tyConHasClosedResKind,
mkTyConTagMap,
-- ** Manipulating TyCons
@@ -138,6 +139,8 @@ import GHC.Platform
import {-# SOURCE #-} GHC.Core.TyCo.Rep
( Kind, Type, PredType, mkForAllTy, mkNakedKindFunTy, mkNakedTyConTy )
+import {-# SOURCE #-} GHC.Core.TyCo.FVs
+ ( noFreeVarsOfType )
import {-# SOURCE #-} GHC.Core.TyCo.Ppr
( pprType )
import {-# SOURCE #-} GHC.Builtin.Types
@@ -773,10 +776,34 @@ instance Binary TyConBndrVis where
--
-- This data type also encodes a number of primitive, built in type constructors
-- such as those for function and tuple types.
-
+--
-- If you edit this type, you may need to update the GHC formalism
-- See Note [GHC Formalism] in GHC.Core.Lint
-data TyCon =
+data TyCon = TyCon {
+ tyConUnique :: !Unique, -- ^ A Unique of this TyCon. Invariant:
+ -- identical to Unique of Name stored in
+ -- tyConName field.
+
+ tyConName :: !Name, -- ^ Name of the constructor
+
+ -- See Note [The binders/kind/arity fields of a TyCon]
+ tyConBinders :: [TyConBinder], -- ^ Full binders
+ tyConResKind :: Kind, -- ^ Result kind
+ tyConHasClosedResKind :: Bool,
+
+ -- Cached values
+ tyConTyVars :: [TyVar], -- ^ TyVar binders
+ tyConKind :: Kind, -- ^ Kind of this TyCon
+ tyConArity :: Arity, -- ^ Arity
+ tyConNullaryTy :: Type, -- ^ A pre-allocated @TyConApp tycon []@
+
+ tyConRoles :: [Role], -- ^ The role for each type variable
+ -- This list has length = tyConArity
+ -- See also Note [TyCon Role signatures]
+
+ tyConDetails :: !TyConDetails }
+
+data TyConDetails =
-- | Algebraic data types, from
-- - @data@ declarations
-- - @newtype@ declarations
@@ -790,20 +817,6 @@ data TyCon =
-- Data/newtype/type /families/ are handled by 'FamilyTyCon'.
-- See 'AlgTyConRhs' for more information.
AlgTyCon {
- tyConUnique :: !Unique, -- ^ A Unique of this TyCon. Invariant:
- -- identical to Unique of Name stored in
- -- tyConName field.
-
- tyConName :: Name, -- ^ Name of the constructor
-
- -- See Note [The binders/kind/arity fields of a TyCon]
- tyConBinders :: [TyConBinder], -- ^ Full binders
- tyConTyVars :: [TyVar], -- ^ TyVar binders
- tyConResKind :: Kind, -- ^ Result kind
- tyConKind :: Kind, -- ^ Kind of this TyCon
- tyConArity :: Arity, -- ^ Arity
- tyConNullaryTy :: Type, -- ^ A pre-allocated @TyConApp tycon []@
-
-- The tyConTyVars scope over:
--
-- 1. The 'algTcStupidTheta'
@@ -813,10 +826,6 @@ data TyCon =
-- Note that it does /not/ scope over the data
-- constructors.
- tcRoles :: [Role], -- ^ The role for each type variable
- -- This list has length = tyConArity
- -- See also Note [TyCon Role signatures]
-
tyConCType :: Maybe CType,-- ^ The C type that should be used
-- for this type when using the FFI
-- and CAPI
@@ -851,25 +860,8 @@ data TyCon =
-- | Represents type synonyms
| SynonymTyCon {
- tyConUnique :: !Unique, -- ^ A Unique of this TyCon. Invariant:
- -- identical to Unique of Name stored in
- -- tyConName field.
-
- tyConName :: Name, -- ^ Name of the constructor
-
- -- See Note [The binders/kind/arity fields of a TyCon]
- tyConBinders :: [TyConBinder], -- ^ Full binders
- tyConTyVars :: [TyVar], -- ^ TyVar binders
- tyConResKind :: Kind, -- ^ Result kind
- tyConKind :: Kind, -- ^ Kind of this TyCon
- tyConArity :: Arity, -- ^ Arity
- tyConNullaryTy :: Type, -- ^ A pre-allocated @TyConApp tycon []@
-- tyConTyVars scope over: synTcRhs
- tcRoles :: [Role], -- ^ The role for each type variable
- -- This list has length = tyConArity
- -- See also Note [TyCon Role signatures]
-
synTcRhs :: Type, -- ^ Contains information about the expansion
-- of the synonym
@@ -890,19 +882,6 @@ data TyCon =
-- | Represents families (both type and data)
-- Argument roles are all Nominal
| FamilyTyCon {
- tyConUnique :: !Unique, -- ^ A Unique of this TyCon. Invariant:
- -- identical to Unique of Name stored in
- -- tyConName field.
-
- tyConName :: Name, -- ^ Name of the constructor
-
- -- See Note [The binders/kind/arity fields of a TyCon]
- tyConBinders :: [TyConBinder], -- ^ Full binders
- tyConTyVars :: [TyVar], -- ^ TyVar binders
- tyConResKind :: Kind, -- ^ Result kind
- tyConKind :: Kind, -- ^ Kind of this TyCon
- tyConArity :: Arity, -- ^ Arity
- tyConNullaryTy :: Type, -- ^ A pre-allocated @TyConApp tycon []@
-- tyConTyVars connect an associated family TyCon
-- with its parent class; see GHC.Tc.Validity.checkConsistentFamInst
@@ -928,23 +907,6 @@ data TyCon =
-- the usual suspects (such as @Int#@) as well as foreign-imported
-- types and kinds (@*@, @#@, and @?@)
| PrimTyCon {
- tyConUnique :: !Unique, -- ^ A Unique of this TyCon. Invariant:
- -- identical to Unique of Name stored in
- -- tyConName field.
-
- tyConName :: Name, -- ^ Name of the constructor
-
- -- See Note [The binders/kind/arity fields of a TyCon]
- tyConBinders :: [TyConBinder], -- ^ Full binders
- tyConResKind :: Kind, -- ^ Result kind
- tyConKind :: Kind, -- ^ Kind of this TyCon
- tyConArity :: Arity, -- ^ Arity
- tyConNullaryTy :: Type, -- ^ A pre-allocated @TyConApp tycon []@
-
- tcRoles :: [Role], -- ^ The role for each type variable
- -- This list has length = tyConArity
- -- See also Note [TyCon Role signatures]
-
primRepName :: TyConRepName -- ^ The 'Typeable' representation.
-- A cached version of
-- @'mkPrelTyConRepName' ('tyConName' tc)@.
@@ -952,18 +914,6 @@ data TyCon =
-- | Represents promoted data constructor.
| PromotedDataCon { -- See Note [Promoted data constructors]
- tyConUnique :: !Unique, -- ^ Same Unique as the data constructor
- tyConName :: Name, -- ^ Same Name as the data constructor
-
- -- See Note [The binders/kind/arity fields of a TyCon]
- tyConBinders :: [TyConPiTyBinder], -- ^ Full binders
- -- TyConPiTyBinder: see Note [Promoted GADT data constructors]
- tyConResKind :: Kind, -- ^ Result kind
- tyConKind :: Kind, -- ^ Kind of this TyCon
- tyConArity :: Arity, -- ^ Arity
- tyConNullaryTy :: Type, -- ^ A pre-allocated @TyConApp tycon []@
-
- tcRoles :: [Role], -- ^ Roles: N for kind vars, R for type vars
dataCon :: DataCon, -- ^ Corresponding data constructor
tcRepName :: TyConRepName,
promDcInfo :: PromDataConInfo -- ^ See comments with 'PromDataConInfo'
@@ -972,31 +922,20 @@ data TyCon =
-- | These exist only during type-checking. See Note [How TcTyCons work]
-- in "GHC.Tc.TyCl"
| TcTyCon {
- tyConUnique :: !Unique,
- tyConName :: Name,
-
- -- See Note [The binders/kind/arity fields of a TyCon]
- tyConBinders :: [TyConBinder], -- ^ Full binders
- tyConTyVars :: [TyVar], -- ^ TyVar binders
- tyConResKind :: Kind, -- ^ Result kind
- tyConKind :: Kind, -- ^ Kind of this TyCon
- tyConArity :: Arity, -- ^ Arity
- tyConNullaryTy :: Type, -- ^ A pre-allocated @TyConApp tycon []@
-
-- NB: the tyConArity of a TcTyCon must match
-- the number of Required (positional, user-specified)
-- arguments to the type constructor; see the use
-- of tyConArity in generaliseTcTyCon
- tcTyConScopedTyVars :: [(Name,TcTyVar)],
+ tctc_scoped_tvs :: [(Name,TcTyVar)],
-- ^ Scoped tyvars over the tycon's body
-- The range is always a skolem or TcTyVar, be
-- MonoTcTyCon only: see Note [Scoped tyvars in a TcTyCon]
- tcTyConIsPoly :: Bool, -- ^ Is this TcTyCon already generalized?
- -- Used only to make zonking more efficient
+ tctc_is_poly :: Bool, -- ^ Is this TcTyCon already generalized?
+ -- Used only to make zonking more efficient
- tcTyConFlavour :: TyConFlavour
+ tctc_flavour :: TyConFlavour
-- ^ What sort of 'TyCon' this represents.
}
@@ -1515,21 +1454,24 @@ type TyConRepName = Name
-- $tcMaybe = TyCon { tyConName = "Maybe", ... }
tyConRepName_maybe :: TyCon -> Maybe TyConRepName
-tyConRepName_maybe (PrimTyCon { primRepName = rep_nm })
- = Just rep_nm
-tyConRepName_maybe (AlgTyCon { algTcFlavour = parent }) = case parent of
- VanillaAlgTyCon rep_nm -> Just rep_nm
- UnboxedSumTyCon -> Nothing
- ClassTyCon _ rep_nm -> Just rep_nm
- DataFamInstTyCon {} -> Nothing
-tyConRepName_maybe (FamilyTyCon { famTcFlav = DataFamilyTyCon rep_nm })
- = Just rep_nm
-tyConRepName_maybe (PromotedDataCon { dataCon = dc, tcRepName = rep_nm })
- | isUnboxedSumDataCon dc -- see #13276
- = Nothing
- | otherwise
- = Just rep_nm
-tyConRepName_maybe _ = Nothing
+tyConRepName_maybe (TyCon { tyConDetails = details }) = get_rep_nm details
+ where
+ get_rep_nm (PrimTyCon { primRepName = rep_nm })
+ = Just rep_nm
+ get_rep_nm (AlgTyCon { algTcFlavour = parent })
+ = case parent of
+ VanillaAlgTyCon rep_nm -> Just rep_nm
+ UnboxedSumTyCon -> Nothing
+ ClassTyCon _ rep_nm -> Just rep_nm
+ DataFamInstTyCon {} -> Nothing
+ get_rep_nm (FamilyTyCon { famTcFlav = DataFamilyTyCon rep_nm })
+ = Just rep_nm
+ get_rep_nm (PromotedDataCon { dataCon = dc, tcRepName = rep_nm })
+ | isUnboxedSumDataCon dc -- see #13276
+ = Nothing
+ | otherwise
+ = Just rep_nm
+ get_rep_nm _ = Nothing
-- | Make a 'Name' for the 'Typeable' representation of the given wired-in type
mkPrelTyConRepName :: Name -> TyConRepName
@@ -1801,9 +1743,9 @@ tyConFieldLabels tc = dFsEnvElts $ tyConFieldLabelEnv tc
-- | The labels for the fields of this particular 'TyCon'
tyConFieldLabelEnv :: TyCon -> FieldLabelEnv
-tyConFieldLabelEnv tc
- | isAlgTyCon tc = algTcFields tc
- | otherwise = emptyDFsEnv
+tyConFieldLabelEnv (TyCon { tyConDetails = details })
+ | AlgTyCon { algTcFields = fields } <- details = fields
+ | otherwise = emptyDFsEnv
-- | Look up a field label belonging to this 'TyCon'
lookupTyConFieldLabel :: FieldLabelString -> TyCon -> Maybe FieldLabel
@@ -1833,6 +1775,25 @@ module mutual-recursion. And they aren't called from many places.
So we compromise, and move their Kind calculation to the call site.
-}
+mkTyCon :: Name -> [TyConBinder] -> Kind -> [Role] -> TyConDetails -> TyCon
+mkTyCon name binders res_kind roles details
+ = tc
+ where
+ -- Recurisve binding because of tcNullaryTy
+ tc = TyCon { tyConName = name
+ , tyConUnique = nameUnique name
+ , tyConBinders = binders
+ , tyConResKind = res_kind
+ , tyConRoles = roles
+ , tyConDetails = details
+
+ -- Cached things
+ , tyConKind = mkTyConKind binders res_kind
+ , tyConArity = length binders
+ , tyConNullaryTy = mkNakedTyConTy tc
+ , tyConHasClosedResKind = noFreeVarsOfType res_kind
+ , tyConTyVars = binderVars binders }
+
-- | This is the making of an algebraic 'TyCon'.
mkAlgTyCon :: Name
-> [TyConBinder] -- ^ Binders of the 'TyCon'
@@ -1847,25 +1808,14 @@ mkAlgTyCon :: Name
-> Bool -- ^ Was the 'TyCon' declared with GADT syntax?
-> TyCon
mkAlgTyCon name binders res_kind roles cType stupid rhs parent gadt_syn
- = let tc =
- AlgTyCon {
- tyConName = name,
- tyConUnique = nameUnique name,
- tyConBinders = binders,
- tyConResKind = res_kind,
- tyConKind = mkTyConKind binders res_kind,
- tyConArity = length binders,
- tyConNullaryTy = mkNakedTyConTy tc,
- tyConTyVars = binderVars binders,
- tcRoles = roles,
- tyConCType = cType,
- algTcStupidTheta = stupid,
- algTcRhs = rhs,
- algTcFields = fieldsOfAlgTcRhs rhs,
- algTcFlavour = assertPpr (okParent name parent) (ppr name $$ ppr parent) parent,
- algTcGadtSyntax = gadt_syn
- }
- in tc
+ = mkTyCon name binders res_kind roles $
+ AlgTyCon { tyConCType = cType
+ , algTcStupidTheta = stupid
+ , algTcRhs = rhs
+ , algTcFields = fieldsOfAlgTcRhs rhs
+ , algTcFlavour = assertPpr (okParent name parent)
+ (ppr name $$ ppr parent) parent
+ , algTcGadtSyntax = gadt_syn }
-- | Simpler specialization of 'mkAlgTyCon' for classes
mkClassTyCon :: Name -> [TyConBinder]
@@ -1879,61 +1829,37 @@ mkClassTyCon name binders roles rhs clas tc_rep_name
mkTupleTyCon :: Name
-> [TyConBinder]
-> Kind -- ^ Result kind of the 'TyCon'
- -> Arity -- ^ Arity of the tuple 'TyCon'
-> DataCon
-> TupleSort -- ^ Whether the tuple is boxed or unboxed
-> AlgTyConFlav
-> TyCon
-mkTupleTyCon name binders res_kind arity con sort parent
- = let tc =
- AlgTyCon {
- tyConUnique = nameUnique name,
- tyConName = name,
- tyConBinders = binders,
- tyConTyVars = binderVars binders,
- tyConResKind = res_kind,
- tyConKind = mkTyConKind binders res_kind,
- tyConArity = arity,
- tyConNullaryTy = mkNakedTyConTy tc,
- tcRoles = replicate arity Representational,
- tyConCType = Nothing,
- algTcGadtSyntax = False,
- algTcStupidTheta = [],
- algTcRhs = TupleTyCon { data_con = con,
- tup_sort = sort },
- algTcFields = emptyDFsEnv,
- algTcFlavour = parent
- }
- in tc
+mkTupleTyCon name binders res_kind con sort parent
+ = mkTyCon name binders res_kind (constRoles binders Representational) $
+ AlgTyCon { tyConCType = Nothing
+ , algTcGadtSyntax = False
+ , algTcStupidTheta = []
+ , algTcRhs = TupleTyCon { data_con = con
+ , tup_sort = sort }
+ , algTcFields = emptyDFsEnv
+ , algTcFlavour = parent }
+
+constRoles :: [TyConBinder] -> Role -> [Role]
+constRoles bndrs role = [role | _ <- bndrs]
mkSumTyCon :: Name
- -> [TyConBinder]
- -> Kind -- ^ Kind of the resulting 'TyCon'
- -> Arity -- ^ Arity of the sum
- -> [TyVar] -- ^ 'TyVar's scoped over: see 'tyConTyVars'
- -> [DataCon]
- -> AlgTyConFlav
- -> TyCon
-mkSumTyCon name binders res_kind arity tyvars cons parent
- = let tc =
- AlgTyCon {
- tyConUnique = nameUnique name,
- tyConName = name,
- tyConBinders = binders,
- tyConTyVars = tyvars,
- tyConResKind = res_kind,
- tyConKind = mkTyConKind binders res_kind,
- tyConArity = arity,
- tyConNullaryTy = mkNakedTyConTy tc,
- tcRoles = replicate arity Representational,
- tyConCType = Nothing,
- algTcGadtSyntax = False,
- algTcStupidTheta = [],
- algTcRhs = mkSumTyConRhs cons,
- algTcFields = emptyDFsEnv,
- algTcFlavour = parent
- }
- in tc
+ -> [TyConBinder]
+ -> Kind -- ^ Kind of the resulting 'TyCon'
+ -> [DataCon]
+ -> AlgTyConFlav
+ -> TyCon
+mkSumTyCon name binders res_kind cons parent
+ = mkTyCon name binders res_kind (constRoles binders Representational) $
+ AlgTyCon { tyConCType = Nothing
+ , algTcGadtSyntax = False
+ , algTcStupidTheta = []
+ , algTcRhs = mkSumTyConRhs cons
+ , algTcFields = emptyDFsEnv
+ , algTcFlavour = parent }
-- | Makes a tycon suitable for use during type-checking. It stores
-- a variety of details about the definition of the TyCon, but no
@@ -1951,19 +1877,10 @@ mkTcTyCon :: Name
-> TyConFlavour -- ^ What sort of 'TyCon' this represents
-> TyCon
mkTcTyCon name binders res_kind scoped_tvs poly flav
- = let tc =
- TcTyCon { tyConUnique = getUnique name
- , tyConName = name
- , tyConTyVars = binderVars binders
- , tyConBinders = binders
- , tyConResKind = res_kind
- , tyConKind = mkTyConKind binders res_kind
- , tyConArity = length binders
- , tyConNullaryTy = mkNakedTyConTy tc
- , tcTyConScopedTyVars = scoped_tvs
- , tcTyConIsPoly = poly
- , tcTyConFlavour = flav }
- in tc
+ = mkTyCon name binders res_kind (constRoles binders Nominal) $
+ TcTyCon { tctc_scoped_tvs = scoped_tvs
+ , tctc_is_poly = poly
+ , tctc_flavour = flav }
-- | No scoped type variables (to be used with mkTcTyCon).
noTcTyConScopedTyVars :: [(Name, TcTyVar)]
@@ -1980,64 +1897,29 @@ mkPrimTyCon :: Name -> [TyConBinder]
-> [Role]
-> TyCon
mkPrimTyCon name binders res_kind roles
- = let tc =
- PrimTyCon {
- tyConName = name,
- tyConUnique = nameUnique name,
- tyConBinders = binders,
- tyConResKind = res_kind,
- tyConKind = mkTyConKind binders res_kind,
- tyConArity = length roles,
- tyConNullaryTy = mkNakedTyConTy tc,
- tcRoles = roles,
- primRepName = mkPrelTyConRepName name
- }
- in tc
+ = mkTyCon name binders res_kind roles $
+ PrimTyCon { primRepName = mkPrelTyConRepName name }
-- | Create a type synonym 'TyCon'
mkSynonymTyCon :: Name -> [TyConBinder] -> Kind -- ^ /result/ kind
-> [Role] -> Type -> Bool -> Bool -> Bool -> TyCon
mkSynonymTyCon name binders res_kind roles rhs is_tau is_fam_free is_forgetful
- = let tc =
- SynonymTyCon {
- tyConName = name,
- tyConUnique = nameUnique name,
- tyConBinders = binders,
- tyConResKind = res_kind,
- tyConKind = mkTyConKind binders res_kind,
- tyConArity = length binders,
- tyConNullaryTy = mkNakedTyConTy tc,
- tyConTyVars = binderVars binders,
- tcRoles = roles,
- synTcRhs = rhs,
- synIsTau = is_tau,
- synIsFamFree = is_fam_free,
- synIsForgetful = is_forgetful
- }
- in tc
+ = mkTyCon name binders res_kind roles $
+ SynonymTyCon { synTcRhs = rhs
+ , synIsTau = is_tau
+ , synIsFamFree = is_fam_free
+ , synIsForgetful = is_forgetful }
-- | Create a type family 'TyCon'
mkFamilyTyCon :: Name -> [TyConBinder] -> Kind -- ^ /result/ kind
-> Maybe Name -> FamTyConFlav
-> Maybe Class -> Injectivity -> TyCon
mkFamilyTyCon name binders res_kind resVar flav parent inj
- = let tc =
- FamilyTyCon
- { tyConUnique = nameUnique name
- , tyConName = name
- , tyConBinders = binders
- , tyConResKind = res_kind
- , tyConKind = mkTyConKind binders res_kind
- , tyConArity = length binders
- , tyConNullaryTy = mkNakedTyConTy tc
- , tyConTyVars = binderVars binders
- , famTcResVar = resVar
- , famTcFlav = flav
- , famTcParent = classTyCon <$> parent
- , famTcInj = inj
- }
- in tc
-
+ = mkTyCon name binders res_kind (constRoles binders Nominal) $
+ FamilyTyCon { famTcResVar = resVar
+ , famTcFlav = flav
+ , famTcParent = classTyCon <$> parent
+ , famTcInj = inj }
-- | Create a promoted data constructor 'TyCon'
-- Somewhat dodgily, we give it the same Name
@@ -2047,43 +1929,36 @@ mkPromotedDataCon :: DataCon -> Name -> TyConRepName
-> [TyConPiTyBinder] -> Kind -> [Role]
-> PromDataConInfo -> TyCon
mkPromotedDataCon con name rep_name binders res_kind roles rep_info
- = let tc =
- PromotedDataCon {
- tyConUnique = nameUnique name,
- tyConName = name,
- tyConArity = length roles,
- tyConNullaryTy = mkNakedTyConTy tc,
- tcRoles = roles,
- tyConBinders = binders,
- tyConResKind = res_kind,
- tyConKind = mkTyConKind binders res_kind,
- dataCon = con,
- tcRepName = rep_name,
- promDcInfo = rep_info
- }
- in tc
+ = mkTyCon name binders res_kind roles $
+ PromotedDataCon { dataCon = con
+ , tcRepName = rep_name
+ , promDcInfo = rep_info }
-- | Test if the 'TyCon' is algebraic but abstract (invisible data constructors)
isAbstractTyCon :: TyCon -> Bool
-isAbstractTyCon (AlgTyCon { algTcRhs = AbstractTyCon {} }) = True
-isAbstractTyCon _ = False
+isAbstractTyCon (TyCon { tyConDetails = details })
+ | AlgTyCon { algTcRhs = AbstractTyCon {} } <- details = True
+ | otherwise = False
-- | Does this 'TyCon' represent something that cannot be defined in Haskell?
isPrimTyCon :: TyCon -> Bool
-isPrimTyCon (PrimTyCon {}) = True
-isPrimTyCon _ = False
+isPrimTyCon (TyCon { tyConDetails = details })
+ | PrimTyCon {} <- details = True
+ | otherwise = False
-- | Returns @True@ if the supplied 'TyCon' resulted from either a
-- @data@ or @newtype@ declaration
isAlgTyCon :: TyCon -> Bool
-isAlgTyCon (AlgTyCon {}) = True
-isAlgTyCon _ = False
+isAlgTyCon (TyCon { tyConDetails = details })
+ | AlgTyCon {} <- details = True
+ | otherwise = False
-- | Returns @True@ for vanilla AlgTyCons -- that is, those created
-- with a @data@ or @newtype@ declaration.
isVanillaAlgTyCon :: TyCon -> Bool
-isVanillaAlgTyCon (AlgTyCon { algTcFlavour = VanillaAlgTyCon _ }) = True
-isVanillaAlgTyCon _ = False
+isVanillaAlgTyCon (TyCon { tyConDetails = details })
+ | AlgTyCon { algTcFlavour = VanillaAlgTyCon _ } <- details = True
+ | otherwise = False
isDataTyCon :: TyCon -> Bool
-- ^ Returns @True@ for data types that are /definitely/ represented by
@@ -2097,7 +1972,8 @@ isDataTyCon :: TyCon -> Bool
--
-- NB: for a data type family, only the /instance/ 'TyCon's
-- get an info table. The family declaration 'TyCon' does not
-isDataTyCon (AlgTyCon {algTcRhs = rhs})
+isDataTyCon (TyCon { tyConDetails = details })
+ | AlgTyCon {algTcRhs = rhs} <- details
= case rhs of
TupleTyCon { tup_sort = sort }
-> isBoxed (tupleSortBoxity sort)
@@ -2113,40 +1989,50 @@ isDataTyCon _ = False
-- | Was this 'TyCon' declared as "type data"?
-- See Note [Type data declarations] in GHC.Rename.Module.
isTypeDataTyCon :: TyCon -> Bool
-isTypeDataTyCon (AlgTyCon {algTcRhs = DataTyCon {is_type_data = type_data }})
- = type_data
-isTypeDataTyCon _ = False
+isTypeDataTyCon (TyCon { tyConDetails = details })
+ | AlgTyCon {algTcRhs = DataTyCon {is_type_data = type_data }} <- details
+ = type_data
+ | otherwise = False
-- | 'isInjectiveTyCon' is true of 'TyCon's for which this property holds
--- (where X is the role passed in):
--- If (T a1 b1 c1) ~X (T a2 b2 c2), then (a1 ~X1 a2), (b1 ~X2 b2), and (c1 ~X3 c2)
--- (where X1, X2, and X3, are the roles given by tyConRolesX tc X)
--- See also Note [Decomposing equality] in "GHC.Tc.Solver.Canonical"
+-- (where r is the role passed in):
+-- If (T a1 b1 c1) ~r (T a2 b2 c2), then (a1 ~r1 a2), (b1 ~r2 b2), and (c1 ~r3 c2)
+-- (where r1, r2, and r3, are the roles given by tyConRolesX tc r)
+-- See also Note [Decomposing TyConApp equalities] in "GHC.Tc.Solver.Canonical"
isInjectiveTyCon :: TyCon -> Role -> Bool
-isInjectiveTyCon _ Phantom = False
-isInjectiveTyCon (AlgTyCon {}) Nominal = True
-isInjectiveTyCon (AlgTyCon {algTcRhs = rhs}) Representational
- = isGenInjAlgRhs rhs
-isInjectiveTyCon (SynonymTyCon {}) _ = False
-isInjectiveTyCon (FamilyTyCon { famTcFlav = DataFamilyTyCon _ })
- Nominal = True
-isInjectiveTyCon (FamilyTyCon { famTcInj = Injective inj }) Nominal = and inj
-isInjectiveTyCon (FamilyTyCon {}) _ = False
-isInjectiveTyCon (PrimTyCon {}) _ = True
-isInjectiveTyCon (PromotedDataCon {}) _ = True
-isInjectiveTyCon (TcTyCon {}) _ = True
+isInjectiveTyCon (TyCon { tyConDetails = details }) role
+ = go details role
+ where
+ go _ Phantom = True -- Vacuously; (t1 ~P t2) holes for all t1, t2!
+ go (AlgTyCon {}) Nominal = True
+ go (AlgTyCon {algTcRhs = rhs}) Representational
+ = isGenInjAlgRhs rhs
+ go (SynonymTyCon {}) _ = False
+ go (FamilyTyCon { famTcFlav = DataFamilyTyCon _ })
+ Nominal = True
+ go (FamilyTyCon { famTcInj = Injective inj }) Nominal = and inj
+ go (FamilyTyCon {}) _ = False
+ go (PrimTyCon {}) _ = True
+ go (PromotedDataCon {}) _ = True
+ go (TcTyCon {}) _ = True
+
-- Reply True for TcTyCon to minimise knock on type errors
-- See Note [How TcTyCons work] item (1) in GHC.Tc.TyCl
+
-- | 'isGenerativeTyCon' is true of 'TyCon's for which this property holds
--- (where X is the role passed in):
--- If (T tys ~X t), then (t's head ~X T).
--- See also Note [Decomposing equality] in "GHC.Tc.Solver.Canonical"
+-- (where r is the role passed in):
+-- If (T tys ~r t), then (t's head ~r T).
+-- See also Note [Decomposing TyConApp equalities] in "GHC.Tc.Solver.Canonical"
isGenerativeTyCon :: TyCon -> Role -> Bool
-isGenerativeTyCon (FamilyTyCon { famTcFlav = DataFamilyTyCon _ }) Nominal = True
-isGenerativeTyCon (FamilyTyCon {}) _ = False
- -- in all other cases, injectivity implies generativity
-isGenerativeTyCon tc r = isInjectiveTyCon tc r
+isGenerativeTyCon tc@(TyCon { tyConDetails = details }) role
+ = go role details
+ where
+ go Nominal (FamilyTyCon { famTcFlav = DataFamilyTyCon _ }) = True
+ go _ (FamilyTyCon {}) = False
+
+ -- In all other cases, injectivity implies generativity
+ go r _ = isInjectiveTyCon tc r
-- | Is this an 'AlgTyConRhs' of a 'TyCon' that is generative and injective
-- with respect to representational equality?
@@ -2159,42 +2045,46 @@ isGenInjAlgRhs (NewTyCon {}) = False
-- | Is this 'TyCon' that for a @newtype@
isNewTyCon :: TyCon -> Bool
-isNewTyCon (AlgTyCon {algTcRhs = NewTyCon {}}) = True
-isNewTyCon _ = False
+isNewTyCon (TyCon { tyConDetails = details })
+ | AlgTyCon {algTcRhs = NewTyCon {}} <- details = True
+ | otherwise = False
-- | Take a 'TyCon' apart into the 'TyVar's it scopes over, the 'Type' it
-- expands into, and (possibly) a coercion from the representation type to the
-- @newtype at .
-- Returns @Nothing@ if this is not possible.
unwrapNewTyCon_maybe :: TyCon -> Maybe ([TyVar], Type, CoAxiom Unbranched)
-unwrapNewTyCon_maybe (AlgTyCon { tyConTyVars = tvs,
- algTcRhs = NewTyCon { nt_co = co,
- nt_rhs = rhs }})
- = Just (tvs, rhs, co)
-unwrapNewTyCon_maybe _ = Nothing
+unwrapNewTyCon_maybe (TyCon { tyConTyVars = tvs, tyConDetails = details })
+ | AlgTyCon { algTcRhs = NewTyCon { nt_co = co, nt_rhs = rhs }} <- details
+ = Just (tvs, rhs, co)
+ | otherwise = Nothing
unwrapNewTyConEtad_maybe :: TyCon -> Maybe ([TyVar], Type, CoAxiom Unbranched)
-unwrapNewTyConEtad_maybe (AlgTyCon { algTcRhs = NewTyCon { nt_co = co,
- nt_etad_rhs = (tvs,rhs) }})
- = Just (tvs, rhs, co)
-unwrapNewTyConEtad_maybe _ = Nothing
+unwrapNewTyConEtad_maybe (TyCon { tyConDetails = details })
+ | AlgTyCon { algTcRhs = NewTyCon { nt_co = co
+ , nt_etad_rhs = (tvs,rhs) }} <- details
+ = Just (tvs, rhs, co)
+ | otherwise = Nothing
-- | Is this a 'TyCon' representing a regular H98 type synonym (@type@)?
{-# INLINE isTypeSynonymTyCon #-} -- See Note [Inlining coreView] in GHC.Core.Type
isTypeSynonymTyCon :: TyCon -> Bool
-isTypeSynonymTyCon (SynonymTyCon {}) = True
-isTypeSynonymTyCon _ = False
+isTypeSynonymTyCon (TyCon { tyConDetails = details })
+ | SynonymTyCon {} <- details = True
+ | otherwise = False
isTauTyCon :: TyCon -> Bool
-isTauTyCon (SynonymTyCon { synIsTau = is_tau }) = is_tau
-isTauTyCon _ = True
+isTauTyCon (TyCon { tyConDetails = details })
+ | SynonymTyCon { synIsTau = is_tau } <- details = is_tau
+ | otherwise = True
-- | Is this tycon neither a type family nor a synonym that expands
-- to a type family?
isFamFreeTyCon :: TyCon -> Bool
-isFamFreeTyCon (SynonymTyCon { synIsFamFree = fam_free }) = fam_free
-isFamFreeTyCon (FamilyTyCon { famTcFlav = flav }) = isDataFamFlav flav
-isFamFreeTyCon _ = True
+isFamFreeTyCon (TyCon { tyConDetails = details })
+ | SynonymTyCon { synIsFamFree = fam_free } <- details = fam_free
+ | FamilyTyCon { famTcFlav = flav } <- details = isDataFamFlav flav
+ | otherwise = True
-- | Is this a forgetful type synonym? If this is a type synonym whose
-- RHS does not mention one (or more) of its bound variables, returns
@@ -2202,8 +2092,9 @@ isFamFreeTyCon _ = True
-- True may not mean anything, as the test to set this flag is
-- conservative.
isForgetfulSynTyCon :: TyCon -> Bool
-isForgetfulSynTyCon (SynonymTyCon { synIsForgetful = forget }) = forget
-isForgetfulSynTyCon _ = False
+isForgetfulSynTyCon (TyCon { tyConDetails = details })
+ | SynonymTyCon { synIsForgetful = forget } <- details = forget
+ | otherwise = False
-- As for newtypes, it is in some contexts important to distinguish between
-- closed synonyms and synonym families, as synonym families have no unique
@@ -2224,71 +2115,86 @@ tyConMustBeSaturated = tcFlavourMustBeSaturated . tyConFlavour
-- | Is this an algebraic 'TyCon' declared with the GADT syntax?
isGadtSyntaxTyCon :: TyCon -> Bool
-isGadtSyntaxTyCon (AlgTyCon { algTcGadtSyntax = res }) = res
-isGadtSyntaxTyCon _ = False
+isGadtSyntaxTyCon (TyCon { tyConDetails = details })
+ | AlgTyCon { algTcGadtSyntax = res } <- details = res
+ | otherwise = False
-- | Is this an algebraic 'TyCon' which is just an enumeration of values?
isEnumerationTyCon :: TyCon -> Bool
-- See Note [Enumeration types] in GHC.Core.TyCon
-isEnumerationTyCon (AlgTyCon { tyConArity = arity, algTcRhs = rhs })
+isEnumerationTyCon (TyCon { tyConArity = arity, tyConDetails = details })
+ | AlgTyCon { algTcRhs = rhs } <- details
= case rhs of
DataTyCon { is_enum = res } -> res
TupleTyCon {} -> arity == 0
_ -> False
-isEnumerationTyCon _ = False
+ | otherwise = False
-- | Is this a 'TyCon', synonym or otherwise, that defines a family?
isFamilyTyCon :: TyCon -> Bool
-isFamilyTyCon (FamilyTyCon {}) = True
-isFamilyTyCon _ = False
+isFamilyTyCon (TyCon { tyConDetails = details })
+ | FamilyTyCon {} <- details = True
+ | otherwise = False
-- | Is this a 'TyCon', synonym or otherwise, that defines a family with
-- instances?
isOpenFamilyTyCon :: TyCon -> Bool
-isOpenFamilyTyCon (FamilyTyCon {famTcFlav = flav })
- | OpenSynFamilyTyCon <- flav = True
- | DataFamilyTyCon {} <- flav = True
-isOpenFamilyTyCon _ = False
+isOpenFamilyTyCon (TyCon { tyConDetails = details })
+ | FamilyTyCon {famTcFlav = flav } <- details
+ = case flav of
+ OpenSynFamilyTyCon -> True
+ DataFamilyTyCon {} -> True
+ _ -> False
+ | otherwise = False
-- | Is this a synonym 'TyCon' that can have may have further instances appear?
isTypeFamilyTyCon :: TyCon -> Bool
-isTypeFamilyTyCon (FamilyTyCon { famTcFlav = flav }) = not (isDataFamFlav flav)
-isTypeFamilyTyCon _ = False
+isTypeFamilyTyCon (TyCon { tyConDetails = details })
+ | FamilyTyCon { famTcFlav = flav } <- details = not (isDataFamFlav flav)
+ | otherwise = False
-- | Is this a synonym 'TyCon' that can have may have further instances appear?
isDataFamilyTyCon :: TyCon -> Bool
-isDataFamilyTyCon (FamilyTyCon { famTcFlav = flav }) = isDataFamFlav flav
-isDataFamilyTyCon _ = False
+isDataFamilyTyCon (TyCon { tyConDetails = details })
+ | FamilyTyCon { famTcFlav = flav } <- details = isDataFamFlav flav
+ | otherwise = False
-- | Is this an open type family TyCon?
isOpenTypeFamilyTyCon :: TyCon -> Bool
-isOpenTypeFamilyTyCon (FamilyTyCon {famTcFlav = OpenSynFamilyTyCon }) = True
-isOpenTypeFamilyTyCon _ = False
+isOpenTypeFamilyTyCon (TyCon { tyConDetails = details })
+ | FamilyTyCon {famTcFlav = OpenSynFamilyTyCon } <- details = True
+ | otherwise = False
-- | Is this a non-empty closed type family? Returns 'Nothing' for
-- abstract or empty closed families.
isClosedSynFamilyTyConWithAxiom_maybe :: TyCon -> Maybe (CoAxiom Branched)
-isClosedSynFamilyTyConWithAxiom_maybe
- (FamilyTyCon {famTcFlav = ClosedSynFamilyTyCon mb}) = mb
-isClosedSynFamilyTyConWithAxiom_maybe _ = Nothing
+isClosedSynFamilyTyConWithAxiom_maybe (TyCon { tyConDetails = details })
+ | FamilyTyCon {famTcFlav = ClosedSynFamilyTyCon mb} <- details = mb
+ | otherwise = Nothing
+
+isBuiltInSynFamTyCon_maybe :: TyCon -> Maybe BuiltInSynFamily
+isBuiltInSynFamTyCon_maybe (TyCon { tyConDetails = details })
+ | FamilyTyCon {famTcFlav = BuiltInSynFamTyCon ops } <- details = Just ops
+ | otherwise = Nothing
+
+-- | Extract type variable naming the result of injective type family
+tyConFamilyResVar_maybe :: TyCon -> Maybe Name
+tyConFamilyResVar_maybe (TyCon { tyConDetails = details })
+ | FamilyTyCon {famTcResVar = res} <- details = res
+ | otherwise = Nothing
-- | @'tyConInjectivityInfo' tc@ returns @'Injective' is@ if @tc@ is an
-- injective tycon (where @is@ states for which 'tyConBinders' @tc@ is
-- injective), or 'NotInjective' otherwise.
tyConInjectivityInfo :: TyCon -> Injectivity
-tyConInjectivityInfo tc
- | FamilyTyCon { famTcInj = inj } <- tc
+tyConInjectivityInfo tc@(TyCon { tyConDetails = details })
+ | FamilyTyCon { famTcInj = inj } <- details
= inj
| isInjectiveTyCon tc Nominal
= Injective (replicate (tyConArity tc) True)
| otherwise
= NotInjective
-isBuiltInSynFamTyCon_maybe :: TyCon -> Maybe BuiltInSynFamily
-isBuiltInSynFamTyCon_maybe
- (FamilyTyCon {famTcFlav = BuiltInSynFamTyCon ops }) = Just ops
-isBuiltInSynFamTyCon_maybe _ = Nothing
-
isDataFamFlav :: FamTyConFlav -> Bool
isDataFamFlav (DataFamilyTyCon {}) = True -- Data family
isDataFamFlav _ = False -- Type synonym family
@@ -2317,39 +2223,50 @@ isTupleTyCon :: TyCon -> Bool
-- 'isTupleTyCon', because they are built as 'AlgTyCons'. However they
-- get spat into the interface file as tuple tycons, so I don't think
-- it matters.
-isTupleTyCon (AlgTyCon { algTcRhs = TupleTyCon {} }) = True
-isTupleTyCon _ = False
+isTupleTyCon (TyCon { tyConDetails = details })
+ | AlgTyCon { algTcRhs = TupleTyCon {} } <- details = True
+ | otherwise = False
tyConTuple_maybe :: TyCon -> Maybe TupleSort
-tyConTuple_maybe (AlgTyCon { algTcRhs = rhs })
- | TupleTyCon { tup_sort = sort} <- rhs = Just sort
-tyConTuple_maybe _ = Nothing
+tyConTuple_maybe (TyCon { tyConDetails = details })
+ | AlgTyCon { algTcRhs = rhs } <- details
+ , TupleTyCon { tup_sort = sort} <- rhs = Just sort
+ | otherwise = Nothing
-- | Is this the 'TyCon' for an unboxed tuple?
isUnboxedTupleTyCon :: TyCon -> Bool
-isUnboxedTupleTyCon (AlgTyCon { algTcRhs = rhs })
- | TupleTyCon { tup_sort = sort } <- rhs
- = not (isBoxed (tupleSortBoxity sort))
-isUnboxedTupleTyCon _ = False
+isUnboxedTupleTyCon (TyCon { tyConDetails = details })
+ | AlgTyCon { algTcRhs = rhs } <- details
+ , TupleTyCon { tup_sort = sort } <- rhs
+ = not (isBoxed (tupleSortBoxity sort))
+ | otherwise = False
-- | Is this the 'TyCon' for a boxed tuple?
isBoxedTupleTyCon :: TyCon -> Bool
-isBoxedTupleTyCon (AlgTyCon { algTcRhs = rhs })
- | TupleTyCon { tup_sort = sort } <- rhs
- = isBoxed (tupleSortBoxity sort)
-isBoxedTupleTyCon _ = False
+isBoxedTupleTyCon (TyCon { tyConDetails = details })
+ | AlgTyCon { algTcRhs = rhs } <- details
+ , TupleTyCon { tup_sort = sort } <- rhs
+ = isBoxed (tupleSortBoxity sort)
+ | otherwise = False
-- | Is this the 'TyCon' for an unboxed sum?
isUnboxedSumTyCon :: TyCon -> Bool
-isUnboxedSumTyCon (AlgTyCon { algTcRhs = rhs })
- | SumTyCon {} <- rhs
- = True
-isUnboxedSumTyCon _ = False
+isUnboxedSumTyCon (TyCon { tyConDetails = details })
+ | AlgTyCon { algTcRhs = rhs } <- details
+ , SumTyCon {} <- rhs
+ = True
+ | otherwise = False
isLiftedAlgTyCon :: TyCon -> Bool
-isLiftedAlgTyCon (AlgTyCon { tyConResKind = res_kind })
- = isLiftedTypeKind res_kind
-isLiftedAlgTyCon _ = False
+isLiftedAlgTyCon (TyCon { tyConResKind = res_kind, tyConDetails = details })
+ | AlgTyCon {} <- details = isLiftedTypeKind res_kind
+ | otherwise = False
+
+-- | Retrieves the promoted DataCon if this is a PromotedDataCon;
+isPromotedDataCon_maybe :: TyCon -> Maybe DataCon
+isPromotedDataCon_maybe (TyCon { tyConDetails = details })
+ | PromotedDataCon { dataCon = dc } <- details = Just dc
+ | otherwise = Nothing
-- | Is this the 'TyCon' for a /promoted/ tuple?
isPromotedTupleTyCon :: TyCon -> Bool
@@ -2360,8 +2277,9 @@ isPromotedTupleTyCon tyCon
-- | Is this a PromotedDataCon?
isPromotedDataCon :: TyCon -> Bool
-isPromotedDataCon (PromotedDataCon {}) = True
-isPromotedDataCon _ = False
+isPromotedDataCon (TyCon { tyConDetails = details })
+ | PromotedDataCon {} <- details = True
+ | otherwise = False
-- | This function identifies PromotedDataCon's from data constructors in
-- `data T = K1 | K2`, promoted by -XDataKinds. These type constructors
@@ -2372,14 +2290,10 @@ isPromotedDataCon _ = False
-- represented with their original undecorated names.
-- See Note [Type data declarations] in GHC.Rename.Module
isDataKindsPromotedDataCon :: TyCon -> Bool
-isDataKindsPromotedDataCon (PromotedDataCon { dataCon = dc })
- = not (isTypeDataCon dc)
-isDataKindsPromotedDataCon _ = False
-
--- | Retrieves the promoted DataCon if this is a PromotedDataCon;
-isPromotedDataCon_maybe :: TyCon -> Maybe DataCon
-isPromotedDataCon_maybe (PromotedDataCon { dataCon = dc }) = Just dc
-isPromotedDataCon_maybe _ = Nothing
+isDataKindsPromotedDataCon (TyCon { tyConDetails = details })
+ | PromotedDataCon { dataCon = dc } <- details
+ = not (isTypeDataCon dc)
+ | otherwise = False
-- | Is this tycon really meant for use at the kind level? That is,
-- should it be permitted without -XDataKinds?
@@ -2416,36 +2330,22 @@ isLiftedTypeKindTyConName = (`hasKey` liftedTypeKindTyConKey)
-- (namely: boxed and unboxed tuples are wired-in and implicit,
-- but constraint tuples are not)
isImplicitTyCon :: TyCon -> Bool
-isImplicitTyCon (PrimTyCon {}) = True
-isImplicitTyCon (PromotedDataCon {}) = True
-isImplicitTyCon (AlgTyCon { algTcRhs = rhs, tyConName = name })
- | TupleTyCon {} <- rhs = isWiredInName name
- | SumTyCon {} <- rhs = True
- | otherwise = False
-isImplicitTyCon (FamilyTyCon { famTcParent = parent }) = isJust parent
-isImplicitTyCon (SynonymTyCon {}) = False
-isImplicitTyCon (TcTyCon {}) = False
+isImplicitTyCon (TyCon { tyConName = name, tyConDetails = details }) = go details
+ where
+ go (PrimTyCon {}) = True
+ go (PromotedDataCon {}) = True
+ go (SynonymTyCon {}) = False
+ go (TcTyCon {}) = False
+ go (FamilyTyCon { famTcParent = parent }) = isJust parent
+ go (AlgTyCon { algTcRhs = rhs })
+ | TupleTyCon {} <- rhs = isWiredInName name
+ | SumTyCon {} <- rhs = True
+ | otherwise = False
tyConCType_maybe :: TyCon -> Maybe CType
-tyConCType_maybe tc@(AlgTyCon {}) = tyConCType tc
-tyConCType_maybe _ = Nothing
-
--- | Is this a TcTyCon? (That is, one only used during type-checking?)
-isTcTyCon :: TyCon -> Bool
-isTcTyCon (TcTyCon {}) = True
-isTcTyCon _ = False
-
-setTcTyConKind :: TyCon -> Kind -> TyCon
--- Update the Kind of a TcTyCon
--- The new kind is always a zonked version of its previous
--- kind, so we don't need to update any other fields.
--- See Note [The Purely Kinded Type Invariant (PKTI)] in GHC.Tc.Gen.HsType
-setTcTyConKind tc@(TcTyCon {}) kind = let tc' = tc { tyConKind = kind
- , tyConNullaryTy = mkNakedTyConTy tc'
- -- see Note [Sharing nullary TyConApps]
- }
- in tc'
-setTcTyConKind tc _ = pprPanic "setTcTyConKind" (ppr tc)
+tyConCType_maybe (TyCon { tyConDetails = details })
+ | AlgTyCon { tyConCType = mb_ctype} <- details = mb_ctype
+ | otherwise = Nothing
-- | Does this 'TyCon' have a syntactically fixed RuntimeRep when fully applied,
-- as per Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete?
@@ -2455,31 +2355,33 @@ setTcTyConKind tc _ = pprPanic "setTcTyConKind" (ppr tc)
--
-- See Note [Representation-polymorphic TyCons]
tcHasFixedRuntimeRep :: TyCon -> Bool
-tcHasFixedRuntimeRep (AlgTyCon { algTcRhs = rhs }) = case rhs of
- AbstractTyCon {} -> False
- -- An abstract TyCon might not have a fixed runtime representation.
- -- Note that this is an entirely different matter from the concreteness
- -- of the 'TyCon', in the sense of 'isConcreteTyCon'.
+tcHasFixedRuntimeRep tc@(TyCon { tyConDetails = details })
+ | AlgTyCon { algTcRhs = rhs } <- details
+ = case rhs of
+ AbstractTyCon {} -> False
+ -- An abstract TyCon might not have a fixed runtime representation.
+ -- Note that this is an entirely different matter from the concreteness
+ -- of the 'TyCon', in the sense of 'isConcreteTyCon'.
- DataTyCon { data_fixed_lev = fixed_lev } -> fixed_lev
- -- A datatype might not have a fixed levity with UnliftedDatatypes (#20423).
- -- NB: the current representation-polymorphism checks require that
- -- the representation be fully-known, including levity variables.
- -- This might be relaxed in the future (#15532).
+ DataTyCon { data_fixed_lev = fixed_lev } -> fixed_lev
+ -- A datatype might not have a fixed levity with UnliftedDatatypes (#20423).
+ -- NB: the current representation-polymorphism checks require that
+ -- the representation be fully-known, including levity variables.
+ -- This might be relaxed in the future (#15532).
- TupleTyCon { tup_sort = tuple_sort } -> isBoxed (tupleSortBoxity tuple_sort)
+ TupleTyCon { tup_sort = tuple_sort } -> isBoxed (tupleSortBoxity tuple_sort)
- SumTyCon {} -> False -- only unboxed sums here
+ SumTyCon {} -> False -- only unboxed sums here
- NewTyCon { nt_fixed_rep = fixed_rep } -> fixed_rep
- -- A newtype might not have a fixed runtime representation
- -- with UnliftedNewtypes (#17360)
+ NewTyCon { nt_fixed_rep = fixed_rep } -> fixed_rep
+ -- A newtype might not have a fixed runtime representation
+ -- with UnliftedNewtypes (#17360)
-tcHasFixedRuntimeRep SynonymTyCon{} = False -- conservative choice
-tcHasFixedRuntimeRep FamilyTyCon{} = False
-tcHasFixedRuntimeRep PrimTyCon{} = True
-tcHasFixedRuntimeRep TcTyCon{} = False
-tcHasFixedRuntimeRep tc at PromotedDataCon{} = pprPanic "tcHasFixedRuntimeRep datacon" (ppr tc)
+ | SynonymTyCon {} <- details = False -- conservative choice
+ | FamilyTyCon{} <- details = False
+ | PrimTyCon{} <- details = True
+ | TcTyCon{} <- details = False
+ | PromotedDataCon{} <- details = pprPanic "tcHasFixedRuntimeRep datacon" (ppr tc)
-- | Is this 'TyCon' concrete (i.e. not a synonym/type family)?
--
@@ -2505,6 +2407,40 @@ isConcreteTyConFlavour = \case
BuiltInTypeFlavour -> True
PromotedDataConFlavour -> True
+{-
+-----------------------------------------------
+-- TcTyCon
+-----------------------------------------------
+-}
+
+-- | Is this a TcTyCon? (That is, one only used during type-checking?)
+isTcTyCon :: TyCon -> Bool
+isTcTyCon (TyCon { tyConDetails = details })
+ | TcTyCon {} <- details = True
+ | otherwise = False
+
+setTcTyConKind :: TyCon -> Kind -> TyCon
+-- Update the Kind of a TcTyCon
+-- The new kind is always a zonked version of its previous
+-- kind, so we don't need to update any other fields.
+-- See Note [The Purely Kinded Type Invariant (PKTI)] in GHC.Tc.Gen.HsType
+setTcTyConKind tc kind
+ = assert (isMonoTcTyCon tc) $
+ let tc' = tc { tyConKind = kind
+ , tyConNullaryTy = mkNakedTyConTy tc' }
+ -- See Note [Sharing nullary TyConApps]
+ in tc'
+
+isMonoTcTyCon :: TyCon -> Bool
+isMonoTcTyCon (TyCon { tyConDetails = details })
+ | TcTyCon { tctc_is_poly = is_poly } <- details = not is_poly
+ | otherwise = False
+
+tcTyConScopedTyVars :: TyCon -> [(Name,TcTyVar)]
+tcTyConScopedTyVars tc@(TyCon { tyConDetails = details })
+ | TcTyCon { tctc_scoped_tvs = scoped_tvs } <- details = scoped_tvs
+ | otherwise = pprPanic "tcTyConScopedTyVars" (ppr tc)
+
{-
-----------------------------------------------
-- Expand type-constructor applications
@@ -2525,8 +2461,9 @@ expandSynTyCon_maybe
-- ^ Expand a type synonym application
-- Return Nothing if the TyCon is not a synonym,
-- or if not enough arguments are supplied
-expandSynTyCon_maybe tc tys
- | SynonymTyCon { tyConTyVars = tvs, synTcRhs = rhs, tyConArity = arity } <- tc
+expandSynTyCon_maybe (TyCon { tyConTyVars = tvs, tyConArity = arity
+ , tyConDetails = details }) tys
+ | SynonymTyCon { synTcRhs = rhs } <- details
= if arity == 0
then ExpandsSyn [] rhs tys -- Avoid a bit of work in the case of nullary synonyms
else case tys `listLengthCmp` arity of
@@ -2546,17 +2483,17 @@ expandSynTyCon_maybe tc tys
-- exported tycon can have a pattern synonym bundled with it, e.g.,
-- module Foo (TyCon(.., PatSyn)) where
isTyConWithSrcDataCons :: TyCon -> Bool
-isTyConWithSrcDataCons (AlgTyCon { algTcRhs = rhs, algTcFlavour = parent }) =
- case rhs of
- DataTyCon {} -> isSrcParent
- NewTyCon {} -> isSrcParent
- TupleTyCon {} -> isSrcParent
- _ -> False
- where
- isSrcParent = isNoParent parent
-isTyConWithSrcDataCons (FamilyTyCon { famTcFlav = DataFamilyTyCon {} })
- = True -- #14058
-isTyConWithSrcDataCons _ = False
+isTyConWithSrcDataCons (TyCon { tyConDetails = details })
+ | AlgTyCon { algTcRhs = rhs, algTcFlavour = parent } <- details
+ , let isSrcParent = isNoParent parent
+ = case rhs of
+ DataTyCon {} -> isSrcParent
+ NewTyCon {} -> isSrcParent
+ TupleTyCon {} -> isSrcParent
+ _ -> False
+ | FamilyTyCon { famTcFlav = DataFamilyTyCon {} } <- details
+ = True -- #14058
+ | otherwise = False
-- | As 'tyConDataCons_maybe', but returns the empty list of constructors if no
@@ -2570,7 +2507,8 @@ tyConDataCons tycon = tyConDataCons_maybe tycon `orElse` []
-- is the sort that can have any constructors (note: this does not include
-- abstract algebraic types)
tyConDataCons_maybe :: TyCon -> Maybe [DataCon]
-tyConDataCons_maybe (AlgTyCon {algTcRhs = rhs})
+tyConDataCons_maybe (TyCon { tyConDetails = details })
+ | AlgTyCon {algTcRhs = rhs} <- details
= case rhs of
DataTyCon { data_cons = cons } -> Just cons
NewTyCon { data_con = con } -> Just [con]
@@ -2584,13 +2522,14 @@ tyConDataCons_maybe _ = Nothing
-- is returned. If the 'TyCon' has more than one constructor, or represents a
-- primitive or function type constructor then @Nothing@ is returned.
tyConSingleDataCon_maybe :: TyCon -> Maybe DataCon
-tyConSingleDataCon_maybe (AlgTyCon { algTcRhs = rhs })
+tyConSingleDataCon_maybe (TyCon { tyConDetails = details })
+ | AlgTyCon { algTcRhs = rhs } <- details
= case rhs of
DataTyCon { data_cons = [c] } -> Just c
TupleTyCon { data_con = c } -> Just c
NewTyCon { data_con = c } -> Just c
_ -> Nothing
-tyConSingleDataCon_maybe _ = Nothing
+ | otherwise = Nothing
-- | Like 'tyConSingleDataCon_maybe', but panics if 'Nothing'.
tyConSingleDataCon :: TyCon -> DataCon
@@ -2619,68 +2558,56 @@ tyConAlgDataCons_maybe tycon
-- | Determine the number of value constructors a 'TyCon' has. Panics if the
-- 'TyCon' is not algebraic or a tuple
tyConFamilySize :: TyCon -> Int
-tyConFamilySize tc@(AlgTyCon { algTcRhs = rhs })
+tyConFamilySize tc@(TyCon { tyConDetails = details })
+ | AlgTyCon { algTcRhs = rhs } <- details
= case rhs of
DataTyCon { data_cons_size = size } -> size
NewTyCon {} -> 1
TupleTyCon {} -> 1
SumTyCon { data_cons_size = size } -> size
_ -> pprPanic "tyConFamilySize 1" (ppr tc)
-tyConFamilySize tc = pprPanic "tyConFamilySize 2" (ppr tc)
+ | otherwise = pprPanic "tyConFamilySize 2" (ppr tc)
-- | Extract an 'AlgTyConRhs' with information about data constructors from an
-- algebraic or tuple 'TyCon'. Panics for any other sort of 'TyCon'
algTyConRhs :: TyCon -> AlgTyConRhs
-algTyConRhs (AlgTyCon {algTcRhs = rhs}) = rhs
-algTyConRhs other = pprPanic "algTyConRhs" (ppr other)
-
--- | Extract type variable naming the result of injective type family
-tyConFamilyResVar_maybe :: TyCon -> Maybe Name
-tyConFamilyResVar_maybe (FamilyTyCon {famTcResVar = res}) = res
-tyConFamilyResVar_maybe _ = Nothing
-
--- | Get the list of roles for the type parameters of a TyCon
-tyConRoles :: TyCon -> [Role]
--- See also Note [TyCon Role signatures]
-tyConRoles tc
- = case tc of
- { AlgTyCon { tcRoles = roles } -> roles
- ; SynonymTyCon { tcRoles = roles } -> roles
- ; FamilyTyCon {} -> const_role Nominal
- ; PrimTyCon { tcRoles = roles } -> roles
- ; PromotedDataCon { tcRoles = roles } -> roles
- ; TcTyCon {} -> const_role Nominal
- }
- where
- const_role r = replicate (tyConArity tc) r
+algTyConRhs tc@(TyCon { tyConDetails = details })
+ | AlgTyCon {algTcRhs = rhs} <- details = rhs
+ | otherwise = pprPanic "algTyConRhs" (ppr tc)
-- | Extract the bound type variables and type expansion of a type synonym
-- 'TyCon'. Panics if the 'TyCon' is not a synonym
newTyConRhs :: TyCon -> ([TyVar], Type)
-newTyConRhs (AlgTyCon {tyConTyVars = tvs, algTcRhs = NewTyCon { nt_rhs = rhs }})
- = (tvs, rhs)
-newTyConRhs tycon = pprPanic "newTyConRhs" (ppr tycon)
+newTyConRhs tc@(TyCon { tyConTyVars = tvs, tyConDetails = details })
+ | AlgTyCon { algTcRhs = NewTyCon { nt_rhs = rhs }} <- details
+ = (tvs, rhs)
+ | otherwise
+ = pprPanic "newTyConRhs" (ppr tc)
-- | The number of type parameters that need to be passed to a newtype to
-- resolve it. May be less than in the definition if it can be eta-contracted.
newTyConEtadArity :: TyCon -> Int
-newTyConEtadArity (AlgTyCon {algTcRhs = NewTyCon { nt_etad_rhs = tvs_rhs }})
- = length (fst tvs_rhs)
-newTyConEtadArity tycon = pprPanic "newTyConEtadArity" (ppr tycon)
+newTyConEtadArity tc@(TyCon { tyConDetails = details })
+ | AlgTyCon {algTcRhs = NewTyCon { nt_etad_rhs = tvs_rhs }} <- details
+ = length (fst tvs_rhs)
+ | otherwise
+ = pprPanic "newTyConEtadArity" (ppr tc)
-- | Extract the bound type variables and type expansion of an eta-contracted
-- type synonym 'TyCon'. Panics if the 'TyCon' is not a synonym
newTyConEtadRhs :: TyCon -> ([TyVar], Type)
-newTyConEtadRhs (AlgTyCon {algTcRhs = NewTyCon { nt_etad_rhs = tvs_rhs }}) = tvs_rhs
-newTyConEtadRhs tycon = pprPanic "newTyConEtadRhs" (ppr tycon)
+newTyConEtadRhs tc@(TyCon { tyConDetails = details })
+ | AlgTyCon {algTcRhs = NewTyCon { nt_etad_rhs = tvs_rhs }} <- details = tvs_rhs
+ | otherwise = pprPanic "newTyConEtadRhs" (ppr tc)
-- | Extracts the @newtype@ coercion from such a 'TyCon', which can be used to
-- construct something with the @newtype at s type from its representation type
-- (right hand side). If the supplied 'TyCon' is not a @newtype@, returns
-- @Nothing@
newTyConCo_maybe :: TyCon -> Maybe (CoAxiom Unbranched)
-newTyConCo_maybe (AlgTyCon {algTcRhs = NewTyCon { nt_co = co }}) = Just co
-newTyConCo_maybe _ = Nothing
+newTyConCo_maybe (TyCon { tyConDetails = details })
+ | AlgTyCon {algTcRhs = NewTyCon { nt_co = co }} <- details = Just co
+ | otherwise = Nothing
newTyConCo :: TyCon -> CoAxiom Unbranched
newTyConCo tc = case newTyConCo_maybe tc of
@@ -2688,83 +2615,93 @@ newTyConCo tc = case newTyConCo_maybe tc of
Nothing -> pprPanic "newTyConCo" (ppr tc)
newTyConDataCon_maybe :: TyCon -> Maybe DataCon
-newTyConDataCon_maybe (AlgTyCon {algTcRhs = NewTyCon { data_con = con }}) = Just con
-newTyConDataCon_maybe _ = Nothing
+newTyConDataCon_maybe (TyCon { tyConDetails = details })
+ | AlgTyCon {algTcRhs = NewTyCon { data_con = con }} <- details = Just con
+ | otherwise = Nothing
-- | Find the \"stupid theta\" of the 'TyCon'. A \"stupid theta\" is the context
-- to the left of an algebraic type declaration, e.g. @Eq a@ in the declaration
-- @data Eq a => T a ... at . See @Note [The stupid context]@ in "GHC.Core.DataCon".
tyConStupidTheta :: TyCon -> [PredType]
-tyConStupidTheta (AlgTyCon {algTcStupidTheta = stupid}) = stupid
-tyConStupidTheta (PrimTyCon {}) = []
-tyConStupidTheta tycon = pprPanic "tyConStupidTheta" (ppr tycon)
+tyConStupidTheta tc@(TyCon { tyConDetails = details })
+ | AlgTyCon {algTcStupidTheta = stupid} <- details = stupid
+ | PrimTyCon {} <- details = []
+ | otherwise = pprPanic "tyConStupidTheta" (ppr tc)
-- | Extract the 'TyVar's bound by a vanilla type synonym
-- and the corresponding (unsubstituted) right hand side.
synTyConDefn_maybe :: TyCon -> Maybe ([TyVar], Type)
-synTyConDefn_maybe (SynonymTyCon {tyConTyVars = tyvars, synTcRhs = ty})
+synTyConDefn_maybe (TyCon { tyConTyVars = tyvars, tyConDetails = details })
+ | SynonymTyCon {synTcRhs = ty} <- details
= Just (tyvars, ty)
-synTyConDefn_maybe _ = Nothing
+ | otherwise
+ = Nothing
-- | Extract the information pertaining to the right hand side of a type synonym
-- (@type@) declaration.
synTyConRhs_maybe :: TyCon -> Maybe Type
-synTyConRhs_maybe (SynonymTyCon {synTcRhs = rhs}) = Just rhs
-synTyConRhs_maybe _ = Nothing
+synTyConRhs_maybe (TyCon { tyConDetails = details })
+ | SynonymTyCon {synTcRhs = rhs} <- details = Just rhs
+ | otherwise = Nothing
-- | Extract the flavour of a type family (with all the extra information that
-- it carries)
famTyConFlav_maybe :: TyCon -> Maybe FamTyConFlav
-famTyConFlav_maybe (FamilyTyCon {famTcFlav = flav}) = Just flav
-famTyConFlav_maybe _ = Nothing
+famTyConFlav_maybe (TyCon { tyConDetails = details })
+ | FamilyTyCon {famTcFlav = flav} <- details = Just flav
+ | otherwise = Nothing
-- | Is this 'TyCon' that for a class instance?
isClassTyCon :: TyCon -> Bool
-isClassTyCon (AlgTyCon {algTcFlavour = ClassTyCon {}}) = True
-isClassTyCon _ = False
+isClassTyCon (TyCon { tyConDetails = details })
+ | AlgTyCon {algTcFlavour = ClassTyCon {}} <- details = True
+ | otherwise = False
-- | If this 'TyCon' is that for a class instance, return the class it is for.
-- Otherwise returns @Nothing@
tyConClass_maybe :: TyCon -> Maybe Class
-tyConClass_maybe (AlgTyCon {algTcFlavour = ClassTyCon clas _}) = Just clas
-tyConClass_maybe _ = Nothing
+tyConClass_maybe (TyCon { tyConDetails = details })
+ | AlgTyCon {algTcFlavour = ClassTyCon clas _} <- details = Just clas
+ | otherwise = Nothing
-- | Return the associated types of the 'TyCon', if any
tyConATs :: TyCon -> [TyCon]
-tyConATs (AlgTyCon {algTcFlavour = ClassTyCon clas _}) = classATs clas
-tyConATs _ = []
+tyConATs (TyCon { tyConDetails = details })
+ | AlgTyCon {algTcFlavour = ClassTyCon clas _} <- details = classATs clas
+ | otherwise = []
----------------------------------------------------------------------------
-- | Is this 'TyCon' that for a data family instance?
isFamInstTyCon :: TyCon -> Bool
-isFamInstTyCon (AlgTyCon {algTcFlavour = DataFamInstTyCon {} })
- = True
-isFamInstTyCon _ = False
+isFamInstTyCon (TyCon { tyConDetails = details })
+ | AlgTyCon {algTcFlavour = DataFamInstTyCon {} } <- details = True
+ | otherwise = False
tyConFamInstSig_maybe :: TyCon -> Maybe (TyCon, [Type], CoAxiom Unbranched)
-tyConFamInstSig_maybe (AlgTyCon {algTcFlavour = DataFamInstTyCon ax f ts })
- = Just (f, ts, ax)
-tyConFamInstSig_maybe _ = Nothing
+tyConFamInstSig_maybe (TyCon { tyConDetails = details })
+ | AlgTyCon {algTcFlavour = DataFamInstTyCon ax f ts } <- details = Just (f, ts, ax)
+ | otherwise = Nothing
-- | If this 'TyCon' is that of a data family instance, return the family in question
-- and the instance types. Otherwise, return @Nothing@
tyConFamInst_maybe :: TyCon -> Maybe (TyCon, [Type])
-tyConFamInst_maybe (AlgTyCon {algTcFlavour = DataFamInstTyCon _ f ts })
- = Just (f, ts)
-tyConFamInst_maybe _ = Nothing
+tyConFamInst_maybe (TyCon { tyConDetails = details })
+ | AlgTyCon {algTcFlavour = DataFamInstTyCon _ f ts } <- details = Just (f, ts)
+ | otherwise = Nothing
-- | If this 'TyCon' is that of a data family instance, return a 'TyCon' which
-- represents a coercion identifying the representation type with the type
-- instance family. Otherwise, return @Nothing@
tyConFamilyCoercion_maybe :: TyCon -> Maybe (CoAxiom Unbranched)
-tyConFamilyCoercion_maybe (AlgTyCon {algTcFlavour = DataFamInstTyCon ax _ _ })
- = Just ax
-tyConFamilyCoercion_maybe _ = Nothing
+tyConFamilyCoercion_maybe (TyCon { tyConDetails = details })
+ | AlgTyCon {algTcFlavour = DataFamInstTyCon ax _ _ } <- details = Just ax
+ | otherwise = Nothing
-- | Extract any 'RuntimeRepInfo' from this TyCon
tyConPromDataConInfo :: TyCon -> PromDataConInfo
-tyConPromDataConInfo (PromotedDataCon { promDcInfo = rri }) = rri
-tyConPromDataConInfo _ = NoPromInfo
+tyConPromDataConInfo (TyCon { tyConDetails = details })
+ | PromotedDataCon { promDcInfo = rri } <- details = rri
+ | otherwise = NoPromInfo
-- could panic in that second case. But Douglas Adams told me not to.
{-
@@ -2854,26 +2791,30 @@ instance Outputable TyConFlavour where
go PromotedDataConFlavour = "promoted data constructor"
tyConFlavour :: TyCon -> TyConFlavour
-tyConFlavour (AlgTyCon { algTcFlavour = parent, algTcRhs = rhs })
- | ClassTyCon _ _ <- parent = ClassFlavour
- | otherwise = case rhs of
+tyConFlavour (TyCon { tyConDetails = details })
+ | AlgTyCon { algTcFlavour = parent, algTcRhs = rhs } <- details
+ = case parent of
+ ClassTyCon {} -> ClassFlavour
+ _ -> case rhs of
TupleTyCon { tup_sort = sort }
-> TupleFlavour (tupleSortBoxity sort)
SumTyCon {} -> SumFlavour
DataTyCon {} -> DataTypeFlavour
NewTyCon {} -> NewtypeFlavour
AbstractTyCon {} -> AbstractTypeFlavour
-tyConFlavour (FamilyTyCon { famTcFlav = flav, famTcParent = parent })
+
+ | FamilyTyCon { famTcFlav = flav, famTcParent = parent } <- details
= case flav of
DataFamilyTyCon{} -> DataFamilyFlavour parent
OpenSynFamilyTyCon -> OpenTypeFamilyFlavour parent
ClosedSynFamilyTyCon{} -> ClosedTypeFamilyFlavour
AbstractClosedSynFamilyTyCon -> ClosedTypeFamilyFlavour
BuiltInSynFamTyCon{} -> ClosedTypeFamilyFlavour
-tyConFlavour (SynonymTyCon {}) = TypeSynonymFlavour
-tyConFlavour (PrimTyCon {}) = BuiltInTypeFlavour
-tyConFlavour (PromotedDataCon {}) = PromotedDataConFlavour
-tyConFlavour (TcTyCon { tcTyConFlavour = flav }) = flav
+
+ | SynonymTyCon {} <- details = TypeSynonymFlavour
+ | PrimTyCon {} <- details = BuiltInTypeFlavour
+ | PromotedDataCon {} <- details = PromotedDataConFlavour
+ | TcTyCon { tctc_flavour = flav } <-details = flav
-- | Can this flavour of 'TyCon' appear unsaturated?
tcFlavourMustBeSaturated :: TyConFlavour -> Bool
=====================================
compiler/GHC/Iface/Make.hs
=====================================
@@ -532,7 +532,7 @@ tyConToIfaceDecl env tycon
, IfaceData { ifName = getName tycon,
ifBinders = if_binders,
ifResKind = if_res_kind,
- ifCType = tyConCType tycon,
+ ifCType = tyConCType_maybe tycon,
ifRoles = tyConRoles tycon,
ifCtxt = tidyToIfaceContext tc_env1 (tyConStupidTheta tycon),
ifCons = ifaceConDecls (algTyConRhs tycon),
=====================================
compiler/GHC/Tc/Gen/Splice.hs
=====================================
@@ -2121,7 +2121,7 @@ reifyTyCon tc
| isTypeFamilyTyCon tc
= do { let tvs = tyConTyVars tc
res_kind = tyConResKind tc
- resVar = famTcResVar tc
+ resVar = tyConFamilyResVar_maybe tc
; kind' <- reifyKind res_kind
; let (resultSig, injectivity) =
=====================================
compiler/GHC/Tc/Solver/Canonical.hs
=====================================
@@ -1073,7 +1073,8 @@ can_eq_nc' _rewritten _rdr_env _envs ev eq_rel
-- See Note [Canonicalising type applications] about why we require rewritten types
-- Use tcSplitAppTy, not matching on AppTy, to catch oversaturated type families
--- NB: Only decompose AppTy for nominal equality. See Note [Decomposing equality]
+-- NB: Only decompose AppTy for nominal equality.
+-- See Note [Decomposing AppTy equalities]
can_eq_nc' True _rdr_env _envs ev NomEq ty1 _ ty2 _
| Just (t1, s1) <- tcSplitAppTy_maybe ty1
, Just (t2, s2) <- tcSplitAppTy_maybe ty2
@@ -1350,6 +1351,8 @@ zonk_eq_types = go
{- See Note [Unwrap newtypes first]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+See also Note [Decomposing newtype equalities]
+
Consider
newtype N m a = MkN (m a)
Then N will get a conservative, Nominal role for its second parameter 'a',
@@ -1463,7 +1466,7 @@ can_eq_app :: CtEvidence -- :: s1 t1 ~N s2 t2
-- AppTys only decompose for nominal equality, so this case just leads
-- to an irreducible constraint; see typecheck/should_compile/T10494
--- See Note [Decomposing AppTy at representational role]
+-- See Note [Decomposing AppTy equalities]
can_eq_app ev s1 t1 s2 t2
| CtWanted { ctev_dest = dest, ctev_rewriters = rewriters } <- ev
= do { co_s <- unifyWanted rewriters loc Nominal s1 s2
@@ -1530,8 +1533,9 @@ canTyConApp :: CtEvidence -> EqRel
-> TyCon -> [TcType]
-> TyCon -> [TcType]
-> TcS (StopOrContinue Ct)
--- See Note [Decomposing TyConApps]
--- Neither tc1 nor tc2 is a saturated funTyCon
+-- See Note [Decomposing TyConApp equalities]
+-- Neither tc1 nor tc2 is a saturated funTyCon, nor a type family
+-- But they can be data families.
canTyConApp ev eq_rel tc1 tys1 tc2 tys2
| tc1 == tc2
, tys1 `equalLength` tys2
@@ -1561,13 +1565,17 @@ canTyConApp ev eq_rel tc1 tys1 tc2 tys2
ty1 = mkTyConApp tc1 tys1
ty2 = mkTyConApp tc2 tys2
- loc = ctEvLoc ev
- pred = ctEvPred ev
-
- -- See Note [Decomposing equality]
+ -- See Note [Decomposing TyConApp equalities]
+ -- Note [Decomposing newtypes a bit more aggressively]
can_decompose inerts
= isInjectiveTyCon tc1 (eqRelRole eq_rel)
- || (ctEvFlavour ev /= Given && isEmptyBag (matchableGivens loc pred inerts))
+ || (assert (eq_rel == ReprEq) $
+ -- assert: isInjectiveTyCon is always True for Nominal except
+ -- for type synonyms/families, neither of which happen here
+ -- Moreover isInjectiveTyCon is True for Representational
+ -- for algebraic data types. So we are down to newtypes
+ -- and data families.
+ ctEvFlavour ev == Wanted && noGivenIrreds inerts)
{-
Note [Use canEqFailure in canDecomposableTyConApp]
@@ -1601,219 +1609,329 @@ For example, see typecheck/should_compile/T10493, repeated here:
That should compile, but only because we use canEqFailure and not
canEqHardFailure.
-Note [Decomposing equality]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~
-If we have a constraint (of any flavour and role) that looks like
-T tys1 ~ T tys2, what can we conclude about tys1 and tys2? The answer,
-of course, is "it depends". This Note spells it all out.
-
-In this Note, "decomposition" refers to taking the constraint
- [fl] (T tys1 ~X T tys2)
-(for some flavour fl and some role X) and replacing it with
- [fls'] (tys1 ~Xs' tys2)
-where that notation indicates a list of new constraints, where the
-new constraints may have different flavours and different roles.
-
-The key property to consider is injectivity. When decomposing a Given, the
-decomposition is sound if and only if T is injective in all of its type
-arguments. When decomposing a Wanted, the decomposition is sound (assuming the
-correct roles in the produced equality constraints), but it may be a guess --
-that is, an unforced decision by the constraint solver. Decomposing Wanteds
-over injective TyCons does not entail guessing. But sometimes we want to
-decompose a Wanted even when the TyCon involved is not injective! (See below.)
-
-So, in broad strokes, we want this rule:
-
-(*) Decompose a constraint (T tys1 ~X T tys2) if and only if T is injective
-at role X.
-
-Pursuing the details requires exploring three axes:
-* Flavour: Given vs. Wanted
-* Role: Nominal vs. Representational
-* TyCon species: datatype vs. newtype vs. data family vs. type family vs. type variable
-
-(A type variable isn't a TyCon, of course, but it's convenient to put the AppTy case
-in the same table.)
-
-Here is a table (discussion following) detailing where decomposition of
- (T s1 ... sn) ~r (T t1 .. tn)
-is allowed. The first four lines (Data types ... type family) refer
-to TyConApps with various TyCons T; the last line is for AppTy, covering
-both where there is a type variable at the head and the case for an over-
-saturated type family.
-
-NOMINAL GIVEN WANTED WHERE
-
-Datatype YES YES canTyConApp
-Newtype YES YES canTyConApp
-Data family YES YES canTyConApp
-Type family NO{1} YES, in injective args{1} canEqCanLHS2
-AppTy YES YES can_eq_app
-
-REPRESENTATIONAL GIVEN WANTED
-
-Datatype YES YES canTyConApp
-Newtype NO{2} MAYBE{2} canTyConApp(can_decompose)
-Data family NO{3} MAYBE{3} canTyConApp(can_decompose)
-Type family NO NO canEqCanLHS2
-AppTy NO{4} NO{4} can_eq_nc'
-
-{1}: Type families can be injective in some, but not all, of their arguments,
-so we want to do partial decomposition. This is quite different than the way
-other decomposition is done, where the decomposed equalities replace the original
-one. We thus proceed much like we do with superclasses, emitting new Wanteds
-when "decomposing" a partially-injective type family Wanted. Injective type
-families have no corresponding evidence of their injectivity, so we cannot
-decompose an injective-type-family Given.
-
-{2}: See Note [Decomposing newtypes at representational role]
-
-{3}: Because of the possibility of newtype instances, we must treat
-data families like newtypes. See also
-Note [Decomposing newtypes at representational role]. See #10534 and
-test case typecheck/should_fail/T10534.
-
-{4}: See Note [Decomposing AppTy at representational role]
-
- Because type variables can stand in for newtypes, we conservatively do not
- decompose AppTys over representational equality. Here are two examples that
- demonstrate why we can't:
-
- 4a: newtype Phant a = MkPhant Int
- [W] alpha Int ~R beta Bool
-
- If we eventually solve alpha := Phant and beta := Phant, then we can solve
- this equality by unwrapping. But it would have been disastrous to decompose
- the wanted to produce Int ~ Bool, which is definitely insoluble.
-
- 4b: newtype Age = MkAge Int
- [W] alpha Age ~R Maybe Int
-
- First, a question: if we know that ty1 ~R ty2, can we conclude that
- a ty1 ~R a ty2? Not for all a. This is precisely why we need role annotations
- on type constructors. So, if we were to decompose, we would need to
- decompose to [W] alpha ~R Maybe and [W] Age ~ Int. On the other hand, if we
- later solve alpha := Maybe, then we would decompose to [W] Age ~R Int, and
- that would be soluble.
-
-In the implementation of can_eq_nc and friends, we don't directly pattern
-match using lines like in the tables above, as those tables don't cover
-all cases (what about PrimTyCon? tuples?). Instead we just ask about injectivity,
-boiling the tables above down to rule (*). The exceptions to rule (*) are for
-injective type families, which are handled separately from other decompositions,
-and the MAYBE entries above.
-
-Note [Decomposing newtypes at representational role]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-This note discusses the 'newtype' line in the REPRESENTATIONAL table
-in Note [Decomposing equality]. (At nominal role, newtypes are fully
-decomposable.)
+Note [Fast path when decomposing TyConApps]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+If we see (T s1 t1 ~ T s2 t2), then we can just decompose to
+ (s1 ~ s2, t1 ~ t2)
+and push those back into the work list. But if
+ s1 = K k1 s2 = K k2
+then we will just decompose s1~s2, and it might be better to
+do so on the spot. An important special case is where s1=s2,
+and we get just Refl.
-Here is a representative example of why representational equality over
-newtypes is tricky:
+So canDecomposableTyConAppOK uses unifyWanted etc to short-cut that work.
- newtype Nt a = Mk Bool -- NB: a is not used in the RHS,
- type role Nt representational -- but the user gives it an R role anyway
+Note [Decomposing TyConApp equalities]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we have
+ [G/W] T ty1 ~r T ty2
+Can we decompose it, and replace it by
+ [G/W] ty1 ~r' ty2
+and if so what role is r'? (In this Note, all the "~" are primitive
+equalities "~#", but I have dropped the noisy "#" symbols.) Lots of
+background in the paper "Safe zero-cost coercions for Haskell".
+
+This Note covers the topic for
+ * Datatypes
+ * Newtypes
+ * Data families
+For the rest:
+ * Type synonyms: are always expanded
+ * Type families: see Note [Decomposing type family applications]
+ * AppTy: see Note [Decomposing AppTy equalities].
+
+---- Roles of the decomposed constraints ----
+For a start, the role r' will always be defined like this:
+ * If r=N then r' = N
+ * If r=R then r' = role of T's first argument
+
+For example:
+ data TR a = MkTR a -- Role of T's first arg is Representational
+ data TN a = MkTN (F a) -- Role of T's first arg is Nominal
+
+The function tyConRolesX :: Role -> TyCon -> [Role] gets the argument
+role r' for a TyCon T at role r. E.g.
+ tyConRolesX Nominal TR = [Nominal]
+ tyConRolesX Representational TR = [Representational]
+
+---- Soundness and completeness ----
+For Givens, for /soundness/ of decomposition we need, forall ty1,ty2:
+ T ty1 ~r T ty2 ===> ty1 ~r' ty2
+Here "===>" means "implies". That is, given evidence for (co1 : T ty1 ~r T co2)
+we can produce evidence for (co2 : ty1 ~r' ty2). But in the solver we
+/replace/ co1 with co2 in the inert set, and we don't want to lose any proofs
+thereby. So for /completeness/ of decomposition we also need the reverse:
+ ty1 ~r' ty2 ===> T ty1 ~r T ty2
+
+For Wanteds, for /soundness/ of decomposition we need:
+ ty1 ~r' ty2 ===> T ty1 ~r T ty2
+because if we do decompose we'll get evidence (co2 : ty1 ~r' ty2) and
+from that we want to derive evidence (T co2 : T ty1 ~r T ty2).
+For /completeness/ of decomposition we need the reverse implication too,
+else we may decompose to a new proof obligation that is stronger than
+the one we started with. See Note [Decomposing newtype equalities].
+
+---- Injectivity ----
+When do these bi-implications hold? In one direction it is easy.
+We /always/ have
+ ty1 ~r' ty2 ===> T ty1 ~r T ty2
+This is the CO_TYCONAPP rule of the paper (Fig 5); see also the
+TyConAppCo case of GHC.Core.Lint.lintCoercion.
+
+In the other direction, we have
+ T ty1 ~r T ty2 ==> ty1 ~r' ty2 if T is /injective at role r/
+This is the very /definition/ of injectivity: injectivity means result
+is the same => arguments are the same, modulo the role shift.
+See comments on GHC.Core.TyCon.isInjectiveTyCon. This is also
+the CO_NTH rule in Fig 5 of the paper, except in the paper only
+newtypes are non-injective at representation role, so the rule says "H
+is not a newtype".
+
+Injectivity is a bit subtle:
+ Nominal Representational
+ Datatype YES YES
+ Newtype YES NO{1}
+ Data family YES NO{2}
+
+{1} Consider newtype N a = MkN (F a) -- Arg has Nominal role
+ Is it true that (N t1) ~R (N t2) ==> t1 ~N t2 ?
+ No, absolutely not. E.g.
+ type instance F Int = Int; type instance F Bool = Char
+ Then (N Int) ~R (N Bool), by unwrapping, but we don't want Int~Char!
+
+ See Note [Decomposing newtype equalities]
+
+{2} We must treat data families precisely like newtypes, because of the
+ possibility of newtype instances. See also
+ Note [Decomposing newtype equalities]. See #10534 and
+ test case typecheck/should_fail/T10534.
+
+---- Takeaway summary -----
+For sound and complete decomposition, we simply need injectivity;
+that is for isInjectiveTyCon to be true:
+
+* At Nominal role, isInjectiveTyCon is True for all the TyCons we are
+ considering in this Note: datatypes, newtypes, and data families.
+
+* For Givens, injectivity is necessary for soundness; completeness has no
+ side conditions.
+
+* For Wanteds, soundness has no side conditions; but injectivity is needed
+ for completeness. See Note [Decomposing newtype equalities]
+
+This is implemented in `can_decompose` in `canTyConApp`; it looks at
+injectivity, just as specified above.
+
+
+Note [Decomposing type family applications]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Supose we have
+ [G/W] (F ty1) ~r (F ty2)
+This is handled by the TyFamLHS/TyFamLHS case of canEqCanLHS2.
+
+We never decompose to
+ [G/W] ty1 ~r' ty2
+
+Instead
+
+* For Givens we do nothing. Injective type families have no corresponding
+ evidence of their injectivity, so we cannot decompose an
+ injective-type-family Given.
+
+* For Wanteds, for the Nominal role only, we emit new Wanteds rather like
+ functional dependencies, for each injective argument position.
+
+ E.g type family F a b -- injective in first arg, but not second
+ [W] (F s1 t1) ~N (F s2 t2)
+ Emit new Wanteds
+ [W] s1 ~N s2
+ But retain the existing, unsolved constraint.
+
+Note [Decomposing newtype equalities]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+This Note also applies to data families, which we treat like
+newtype in case of 'newtype instance'.
+
+As Note [Decomposing TyConApp equalities] describes, if N is injective
+at role r, we can do this decomposition?
+ [G/W] (N ty1) ~r (N ty2) to [G/W] ty1 ~r' ty2
+
+For a Given with r=R, the answer is a solid NO: newtypes are not injective at
+representational role, and we must not decompose, or we lose soundness.
+Example is wrinkle {1} in Note [Decomposing TyConApp equalities].
+
+For a Wanted with r=R, since newtypes are not injective at representational
+role, decomposition is sound, but we may lose completeness. Nevertheless,
+if the newtype is abstraction (so can't be unwrapped) we can only solve
+the equality by (a) using a Given or (b) decomposition. If (a) is impossible
+(e.g. no Givens) then (b) is safe.
+
+Conclusion: decompose newtypes (at role R) only if there are no usable Givens.
+
+* Incompleteness example (EX1)
+ newtype Nt a = MkNt (Id a)
+ type family Id a where Id a = a
+
+ [W] Nt Int ~R Nt Age
+
+ Because of its use of a type family, Nt's parameter will get inferred to
+ have a nominal role. Thus, decomposing the wanted will yield [W] Int ~N Age,
+ which is unsatisfiable. Unwrapping, though, leads to a solution.
-If we have [W] Nt alpha ~R Nt beta, we *don't* want to decompose to
-[W] alpha ~R beta, because it's possible that alpha and beta aren't
-representationally equal. Here's another example.
+ Conclusion: always unwrap newtypes before attempting to decompose
+ them. This is done in can_eq_nc'. Of course, we can't unwrap if the data
+ constructor isn't in scope. See See Note [Unwrap newtypes first].
- newtype Nt a = MkNt (Id a)
- type family Id a where Id a = a
+* Incompleteness example (EX2)
+ newtype Nt a = Mk Bool -- NB: a is not used in the RHS,
+ type role Nt representational -- but the user gives it an R role anyway
- [W] Nt Int ~R Nt Age
+ If we have [W] Nt alpha ~R Nt beta, we *don't* want to decompose to
+ [W] alpha ~R beta, because it's possible that alpha and beta aren't
+ representationally equal.
-Because of its use of a type family, Nt's parameter will get inferred to have
-a nominal role. Thus, decomposing the wanted will yield [W] Int ~N Age, which
-is unsatisfiable. Unwrapping, though, leads to a solution.
+ and maybe there is a Given (Nt t1 ~R Nt t2), just waiting to be used, if we
+ figure out (elsewhere) that alpha:=t1 and beta:=t2. This is somewhat
+ similar to the question of overlapping Givens for class constraints: see
+ Note [Instance and Given overlap] in GHC.Tc.Solver.Interact.
-Conclusion:
- * Unwrap newtypes before attempting to decompose them.
- This is done in can_eq_nc'.
+ Conclusion: don't decompose [W] N s ~R N t, if there are any Given
+ equalities that could later solve it.
-It all comes from the fact that newtypes aren't necessarily injective
-w.r.t. representational equality.
+ But what does "any Given equalities that could later solve it" mean, precisely?
+ It must be a Given constraint that could turn into N s ~ N t. But that
+ could include [G] (a b) ~ (c d), or even just [G] c. But it'll definitely
+ be an CIrredCan. So we settle for having no CIrredCans at all, which is
+ conservative but safe. See noGivenIrreds and #22331.
-Furthermore, as explained in Note [SelCo and newtypes] in GHC.Core.TyCo.Rep, we can't use
-SelCo on representational coercions over newtypes. SelCo comes into play
-only when decomposing givens.
+ Well not 100.0% safe. There could be a CDictCan with some un-expanded
+ superclasses; but only in some very obscure recursive-superclass
+ situations.
-Conclusion:
- * Do not decompose [G] N s ~R N t
+If there are no Irred Givens (which is quite common) then we will
+successfuly decompose [W] (IO Age) ~R (IO Int), and solve it. But
+that won't happen and [W] (IO Age) ~R (IO Int) will be stuck.
+We /could/, however, be a bit more aggressive about decomposition;
+see Note [Decomposing newtypes a bit more aggressively].
-Is it sensible to decompose *Wanted* constraints over newtypes? Yes!
-It's the only way we could ever prove (IO Int ~R IO Age), recalling
-that IO is a newtype.
+Remember: decomposing Wanteds is always /sound/. This Note is
+only about /completeness/.
-However we must be careful. Consider
+Note [Decomposing newtypes a bit more aggressively]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+c.f. https://github.com/ghc-proposals/ghc-proposals/pull/549
+and discussion on !9282.
+
+Consider [G] c, [W] (IO Int) ~R (IO Age)
+where IO is abstract, and
+ newtype Age = MkAge Int -- Not abstract
+With the above rules, if there any Given Irreds,
+the Wanted is insoluble because we can't decompose it. But in fact,
+if we look at the defn of IO, roughly,
+ newtype IO a = State# -> (State#, a)
+we can see that decomposing [W] (IO Int) ~R (IO Age) to
+ [W] Int ~R Age
+definitely does not lose completeness. Why not? Because the role of
+IO's argment is representational. Hence:
+
+ DecomposeNewtypeIdea:
+ decompose [W] (N s1 .. sn) ~R (N t1 .. tn)
+ if the roles of all N's arguments are representational
+
+If N's arguments really /are/ representational this will not lose
+completeness. Here "really are representational" means "if you expand
+all newtypes in N's RHS, we'd infer a representational role for each
+of N's type variables in that expansion". See Note [Role inference]
+in GHC.Tc.TyCl.Utils.
+
+But the user might /override/ a phantom role with an explicit role
+annotation, and then we could (obscurely) get incompleteness.
+Consider
- type role Nt representational
+ module A( silly, T ) where
+ newtype T a = MkT Int
+ type role T representational -- Override phantom role
- [G] Nt a ~R Nt b (1)
- [W] NT alpha ~R Nt b (2)
- [W] alpha ~ a (3)
+ silly :: Coercion (T Int) (T Bool)
+ silly = Coercion -- Typechecks by unwrapping the newtype
-If we focus on (3) first, we'll substitute in (2), and now it's
-identical to the given (1), so we succeed. But if we focus on (2)
-first, and decompose it, we'll get (alpha ~R b), which is not soluble.
-This is exactly like the question of overlapping Givens for class
-constraints: see Note [Instance and Given overlap] in GHC.Tc.Solver.Interact.
+ data Coercion a b where -- Actually defined in Data.Type.Coercion
+ Coercion :: Coercible a b => Coercion a b
-Conclusion:
- * Decompose [W] N s ~R N t iff there no given constraint that could
- later solve it.
+ module B where
+ import A
+ f :: T Int -> T Bool
+ f = case silly of Coercion -> coerce
-Note [Decomposing AppTy at representational role]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We never decompose AppTy at a representational role. For Givens, doing
-so is simply unsound: the LRCo coercion former requires a nominal-roled
-arguments. (See (1) for an example of why.) For Wanteds, decomposing
-would be sound, but it would be a guess, and a non-confluent one at that.
+Here the `coerce` gives [W] (T Int) ~R (T Bool) which, if we decompose,
+we'll get stuck with (Int ~R Bool). Instead we want to use the
+[G] (T Int) ~R (T Bool), which will be in the Irreds.
-Here is an example:
+Summary: we could adopt (DecomposeNewtypeIdea), at the cost of a very
+obscure incompleteness (above). But no one is reporting a problem from
+the lack of decompostion, so we'll just leave it for now. This long
+Note is just to record the thinking for our future selves.
+
+Note [Decomposing AppTy equalities]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+For AppTy all the same questions arise as in
+Note [Decomposing TyConApp equalities]. We have
+
+ s1 ~r s2, t1 ~N t2 ==> s1 t1 ~r s2 t2 (rule CO_APP)
+ s1 t1 ~N s2 t2 ==> s1 ~N s2, t1 ~N t2 (CO_LEFT, CO_RIGHT)
+
+In the first of these, why do we need Nominal equality in (t1 ~N t2)?
+See {2} below.
+
+For sound and complete solving, we need both directions to decompose. So:
+* At nominal role, all is well: we have both directions.
+* At representational role, decomposition of Givens is unsound (see {1} below),
+ and decomposition of Wanteds is incomplete.
+
+Here is an example of the incompleteness for Wanteds:
[G] g1 :: a ~R b
[W] w1 :: Maybe b ~R alpha a
- [W] w2 :: alpha ~ Maybe
+ [W] w2 :: alpha ~N Maybe
-Suppose we see w1 before w2. If we were to decompose, we would decompose
-this to become
+Suppose we see w1 before w2. If we decompose, using AppCo to prove w1, we get
+ w1 := AppCo w3 w4
[W] w3 :: Maybe ~R alpha
- [W] w4 :: b ~ a
+ [W] w4 :: b ~N a
Note that w4 is *nominal*. A nominal role here is necessary because AppCo
-requires a nominal role on its second argument. (See (2) for an example of
-why.) If we decomposed w1 to w3,w4, we would then get stuck, because w4
-is insoluble. On the other hand, if we see w2 first, setting alpha := Maybe,
-all is well, as we can decompose Maybe b ~R Maybe a into b ~R a.
+requires a nominal role on its second argument. (See {2} for an example of
+why.) Now we are stuck, because w4 is insoluble. On the other hand, if we
+see w2 first, setting alpha := Maybe, all is well, as we can decompose
+Maybe b ~R Maybe a into b ~R a.
Another example:
-
newtype Phant x = MkPhant Int
-
[W] w1 :: Phant Int ~R alpha Bool
[W] w2 :: alpha ~ Phant
If we see w1 first, decomposing would be disastrous, as we would then try
to solve Int ~ Bool. Instead, spotting w2 allows us to simplify w1 to become
-
[W] w1' :: Phant Int ~R Phant Bool
which can then (assuming MkPhant is in scope) be simplified to Int ~R Int,
and all will be well. See also Note [Unwrap newtypes first].
-Bottom line: never decompose AppTy with representational roles.
+Bottom line:
+* Always decompose AppTy at nominal role: can_eq_app
+* Never decompose AppTy at representational role (neither Given nor Wanted):
+ the lack of an equation in can_eq_nc'
-(1) Decomposing a Given AppTy over a representational role is simply
-unsound. For example, if we have co1 :: Phant Int ~R a Bool (for
-the newtype Phant, above), then we surely don't want any relationship
-between Int and Bool, lest we also have co2 :: Phant ~ a around.
+Extra points
+{1} Decomposing a Given AppTy over a representational role is simply
+ unsound. For example, if we have co1 :: Phant Int ~R a Bool (for
+ the newtype Phant, above), then we surely don't want any relationship
+ between Int and Bool, lest we also have co2 :: Phant ~ a around.
-(2) The role on the AppCo coercion is a conservative choice, because we don't
-know the role signature of the function. For example, let's assume we could
-have a representational role on the second argument of AppCo. Then, consider
+{2} The role on the AppCo coercion is a conservative choice, because we don't
+ know the role signature of the function. For example, let's assume we could
+ have a representational role on the second argument of AppCo. Then, consider
data G a where -- G will have a nominal role, as G is a GADT
MkG :: G Int
@@ -1823,9 +1941,8 @@ have a representational role on the second argument of AppCo. Then, consider
co2 :: Age ~R Int -- by newtype axiom
co3 = AppCo co1 co2 :: G Age ~R a Int -- by our broken AppCo
-and now co3 can be used to cast MkG to have type G Age, in violation of
-the way GADTs are supposed to work (which is to use nominal equality).
-
+ and now co3 can be used to cast MkG to have type G Age, in violation of
+ the way GADTs are supposed to work (which is to use nominal equality).
-}
canDecomposableTyConAppOK :: CtEvidence -> EqRel
@@ -1842,6 +1959,7 @@ canDecomposableTyConAppOK ev eq_rel tc tys1 tys2
-- we are guaranteed that cos has the same length
-- as tys1 and tys2
-> do { cos <- zipWith4M (unifyWanted rewriters) new_locs tc_roles tys1 tys2
+ -- See Note [Fast path when decomposing TyConApps]
; setWantedEq dest (mkTyConAppCo role tc cos) }
CtGiven { ctev_evar = evar }
@@ -1945,19 +2063,6 @@ canEqHardFailure ev ty1 ty2
; continueWith (mkIrredCt ShapeMismatchReason new_ev) }
{-
-Note [Decomposing TyConApps]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-If we see (T s1 t1 ~ T s2 t2), then we can just decompose to
- (s1 ~ s2, t1 ~ t2)
-and push those back into the work list. But if
- s1 = K k1 s2 = K k2
-then we will just decompose s1~s2, and it might be better to
-do so on the spot. An important special case is where s1=s2,
-and we get just Refl.
-
-So canDecomposableTyCon is a fast-path decomposition that uses
-unifyWanted etc to short-cut that work.
-
Note [Canonicalising type applications]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Given (s1 t1) ~ ty2, how should we proceed?
@@ -2192,6 +2297,7 @@ canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 ps_xi2 mco
| TyFamLHS fun_tc1 fun_args1 <- lhs1
, TyFamLHS fun_tc2 fun_args2 <- lhs2
+ -- See Note [Decomposing type family applications]
= do { traceTcS "canEqCanLHS2 two type families" (ppr lhs1 $$ ppr lhs2)
-- emit wanted equalities for injective type families
=====================================
compiler/GHC/Tc/Solver/InertSet.hs
=====================================
@@ -20,7 +20,8 @@ module GHC.Tc.Solver.InertSet (
emptyInert,
addInertItem,
- matchableGivens,
+ noMatchableGivenDicts,
+ noGivenIrreds,
mightEqualLater,
prohibitedSuperClassSolve,
@@ -53,6 +54,7 @@ import GHC.Core.Reduction
import GHC.Core.Predicate
import GHC.Core.TyCo.FVs
import qualified GHC.Core.TyCo.Rep as Rep
+import GHC.Core.Class( Class )
import GHC.Core.TyCon
import GHC.Core.Unify
@@ -1535,25 +1537,20 @@ isOuterTyVar tclvl tv
-- becomes "outer" even though its level numbers says it isn't.
| otherwise = False -- Coercion variables; doesn't much matter
--- | Returns Given constraints that might,
--- potentially, match the given pred. This is used when checking to see if a
+noGivenIrreds :: InertSet -> Bool
+noGivenIrreds (IS { inert_cans = inert_cans })
+ = isEmptyBag (inert_irreds inert_cans)
+
+-- | Returns True iff there are no Given constraints that might,
+-- potentially, match the given class consraint. This is used when checking to see if a
-- Given might overlap with an instance. See Note [Instance and Given overlap]
-- in "GHC.Tc.Solver.Interact"
-matchableGivens :: CtLoc -> PredType -> InertSet -> Cts
-matchableGivens loc_w pred_w inerts@(IS { inert_cans = inert_cans })
- = filterBag matchable_given all_relevant_givens
+noMatchableGivenDicts :: InertSet -> CtLoc -> Class -> [TcType] -> Bool
+noMatchableGivenDicts inerts@(IS { inert_cans = inert_cans }) loc_w clas tys
+ = not $ anyBag matchable_given $
+ findDictsByClass (inert_dicts inert_cans) clas
where
- -- just look in class constraints and irreds. matchableGivens does get called
- -- for ~R constraints, but we don't need to look through equalities, because
- -- canonical equalities are used for rewriting. We'll only get caught by
- -- non-canonical -- that is, irreducible -- equalities.
- all_relevant_givens :: Cts
- all_relevant_givens
- | Just (clas, _) <- getClassPredTys_maybe pred_w
- = findDictsByClass (inert_dicts inert_cans) clas
- `unionBags` inert_irreds inert_cans
- | otherwise
- = inert_irreds inert_cans
+ pred_w = mkClassPred clas tys
matchable_given :: Ct -> Bool
matchable_given ct
=====================================
compiler/GHC/Tc/Solver/Interact.hs
=====================================
@@ -1391,7 +1391,7 @@ We generate these Wanteds in three places, depending on how we notice the
injectivity.
1. When we have a [W] F tys1 ~ F tys2. This is handled in canEqCanLHS2, and
-described in Note [Decomposing equality] in GHC.Tc.Solver.Canonical.
+described in Note [Decomposing type family applications] in GHC.Tc.Solver.Canonical.
2. When we have [W] F tys1 ~ T and [W] F tys2 ~ T. Note that neither of these
constraints rewrites the other, as they have different LHSs. This is done
@@ -2283,11 +2283,9 @@ matchClassInst dflags inerts clas tys loc
-- See Note [Instance and Given overlap]
| not (xopt LangExt.IncoherentInstances dflags)
, not (naturallyCoherentClass clas)
- , let matchable_givens = matchableGivens loc pred inerts
- , not (isEmptyBag matchable_givens)
+ , not (noMatchableGivenDicts inerts loc clas tys)
= do { traceTcS "Delaying instance application" $
- vcat [ text "Work item=" <+> pprClassPred clas tys
- , text "Potential matching givens:" <+> ppr matchable_givens ]
+ vcat [ text "Work item=" <+> pprClassPred clas tys ]
; return NotSure }
| otherwise
=====================================
compiler/GHC/Tc/TyCl.hs
=====================================
@@ -5177,8 +5177,7 @@ addVDQNote :: TcTyCon -> TcM a -> TcM a
-- See Note [Inferring visible dependent quantification]
-- Only types without a signature (CUSK or SAK) here
addVDQNote tycon thing_inside
- | assertPpr (isTcTyCon tycon) (ppr tycon) $
- assertPpr (not (tcTyConIsPoly tycon)) (ppr tycon $$ ppr tc_kind)
+ | assertPpr (isMonoTcTyCon tycon) (ppr tycon $$ ppr tc_kind)
has_vdq
= addLandmarkErrCtxt vdq_warning thing_inside
| otherwise
=====================================
compiler/GHC/Tc/Utils/TcMType.hs
=====================================
@@ -2484,9 +2484,9 @@ zonkTcTyCon :: TcTyCon -> TcM TcTyCon
-- A non-poly TcTyCon may have unification
-- variables that need zonking, but poly ones cannot
zonkTcTyCon tc
- | tcTyConIsPoly tc = return tc
- | otherwise = do { tck' <- zonkTcType (tyConKind tc)
+ | isMonoTcTyCon tc = do { tck' <- zonkTcType (tyConKind tc)
; return (setTcTyConKind tc tck') }
+ | otherwise = return tc
zonkTcTyVar :: TcTyVar -> TcM TcType
-- Simply look through all Flexis
=====================================
m4/fp_musttail.m4
=====================================
@@ -5,7 +5,7 @@ AC_DEFUN([FP_MUSTTAIL],
[
AC_MSG_CHECKING([whether __attribute__((musttail)) is supported])
echo 'extern int foo(void); int bar(void) { __attribute__((musttail)) return foo(); }' > conftest.c
- if $CC -c conftest.c -o conftest.o
+ if $CC -c conftest.c -o conftest.o > /dev/null 2>&1
then
AC_MSG_RESULT([yes])
AC_DEFINE(HAS_MUSTTAIL, 1, [Has musttail])
=====================================
testsuite/tests/typecheck/should_compile/T22331.hs
=====================================
@@ -0,0 +1,15 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module T22331 where
+
+import Data.Coerce
+
+data family Fool a
+
+-- This works
+joe :: Coercible (Fool a) (Fool b) => Fool a -> Fool b
+joe = coerce
+
+-- This does not
+bob :: Coercible (Fool a) (Fool b) => Fool b -> Fool a
+bob = coerce
=====================================
testsuite/tests/typecheck/should_compile/all.T
=====================================
@@ -850,3 +850,4 @@ test('T21951a', normal, compile, ['-Wredundant-strictness-flags'])
test('T21951b', normal, compile, ['-Wredundant-strictness-flags'])
test('T21550', normal, compile, [''])
test('T22310', normal, compile, [''])
+test('T22331', normal, compile, [''])
=====================================
utils/haddock
=====================================
@@ -1 +1 @@
-Subproject commit 2ffde83344bab8ed0aee3e8ef46f43856c7ca6ef
+Subproject commit edc72530978d8a9ec92f51d288484986ec0051e3
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/b802803cdae8198ec7fdc9dcd02e13a3b5ecee8c...95a58b685b8c014f5f776be56cd8aeaf1e8d6688
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/b802803cdae8198ec7fdc9dcd02e13a3b5ecee8c...95a58b685b8c014f5f776be56cd8aeaf1e8d6688
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20221128/6386e89f/attachment-0001.html>
More information about the ghc-commits
mailing list