summaryrefslogtreecommitdiff
path: root/compiler/GHC/Core
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/GHC/Core')
-rw-r--r--compiler/GHC/Core/Coercion.hs92
-rw-r--r--compiler/GHC/Core/Coercion.hs-boot6
-rw-r--r--compiler/GHC/Core/Predicate.hs2
-rw-r--r--compiler/GHC/Core/Reduction.hs4
-rw-r--r--compiler/GHC/Core/TyCo/Compare.hs2
-rw-r--r--compiler/GHC/Core/TyCo/Rep.hs15
-rw-r--r--compiler/GHC/Core/TyCo/Subst.hs6
-rw-r--r--compiler/GHC/Core/Type.hs4
8 files changed, 73 insertions, 58 deletions
diff --git a/compiler/GHC/Core/Coercion.hs b/compiler/GHC/Core/Coercion.hs
index 6459136973..a2f4a2cecf 100644
--- a/compiler/GHC/Core/Coercion.hs
+++ b/compiler/GHC/Core/Coercion.hs
@@ -39,8 +39,8 @@ module GHC.Core.Coercion (
mkSymCo, mkTransCo,
mkSelCo, getNthFun, getNthFromType, mkLRCo,
mkInstCo, mkAppCo, mkAppCos, mkTyConAppCo,
- mkFunCo1, mkFunCo2, mkFunCoNoFTF, mkFunResCo,
- mkNakedFunCo1, mkNakedFunCo2,
+ mkFunCo, mkFunCo2, mkFunCoNoFTF, mkFunResCo,
+ mkNakedFunCo,
mkForAllCo, mkForAllCos, mkHomoForAllCos,
mkPhantomCo,
mkHoleCo, mkUnivCo, mkSubCo,
@@ -51,7 +51,7 @@ module GHC.Core.Coercion (
castCoercionKind, castCoercionKind1, castCoercionKind2,
mkPrimEqPred, mkReprPrimEqPred, mkPrimEqPredRole,
- mkHeteroPrimEqPred, mkHeteroReprPrimEqPred,
+ mkNomPrimEqPred,
-- ** Decomposition
instNewTyCon_maybe,
@@ -811,29 +811,20 @@ mkFunCoNoFTF r w arg_co res_co
-- or @(a => x) ~ (b => y)@, depending on the kind of @a@/@b@.
-- This (most common) version takes a single FunTyFlag, which is used
-- for both fco_afl and ftf_afr of the FunCo
-mkFunCo1 :: HasDebugCallStack => Role -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion
-mkFunCo1 r af w arg_co res_co
+mkFunCo :: Role -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion
+mkFunCo r af w arg_co res_co
= mkFunCo2 r af af w arg_co res_co
-mkNakedFunCo1 :: Role -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion
--- This version of mkFunCo1 does not check FunCo invariants (checkFunCo)
--- It is called during typechecking on un-zonked types;
--- in particular there may be un-zonked coercion variables.
-mkNakedFunCo1 r af w arg_co res_co
- = mkNakedFunCo2 r af af w arg_co res_co
+mkNakedFunCo :: Role -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion
+-- This version of mkFunCo does not check FunCo invariants (checkFunCo)
+-- It's a historical vestige; See Note [No assertion check on mkFunCo]
+mkNakedFunCo = mkFunCo
-mkFunCo2 :: HasDebugCallStack => Role -> FunTyFlag -> FunTyFlag
- -> CoercionN -> Coercion -> Coercion -> Coercion
+mkFunCo2 :: Role -> FunTyFlag -> FunTyFlag
+ -> CoercionN -> Coercion -> Coercion -> Coercion
-- This is the smart constructor for FunCo; it checks invariants
mkFunCo2 r afl afr w arg_co res_co
- = assertPprMaybe (checkFunCo r afl afr w arg_co res_co) $
- mkNakedFunCo2 r afl afr w arg_co res_co
-
-mkNakedFunCo2 :: Role -> FunTyFlag -> FunTyFlag
- -> CoercionN -> Coercion -> Coercion -> Coercion
--- This is the smart constructor for FunCo
--- "Naked"; it does not check invariants
-mkNakedFunCo2 r afl afr w arg_co res_co
+ -- See Note [No assertion check on mkFunCo]
| Just (ty1, _) <- isReflCo_maybe arg_co
, Just (ty2, _) <- isReflCo_maybe res_co
, Just (w, _) <- isReflCo_maybe w
@@ -844,6 +835,19 @@ mkNakedFunCo2 r afl afr w arg_co res_co
, fco_mult = w, fco_arg = arg_co, fco_res = res_co }
+{- Note [No assertion check on mkFunCo]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We used to have a checkFunCo assertion on mkFunCo, but during typechecking
+we can (legitimately) have not-full-zonked types or coercion variables, so
+the assertion spuriously fails (test T11480b is a case in point). Lint
+checks all these things anyway.
+
+We used to get around the problem by calling mkNakedFunCo from within the
+typechecker, which dodged the assertion check. But then mkAppCo calls
+mkTyConAppCo, which calls tyConAppFunCo_maybe, which calls mkFunCo.
+Duplicating this stack of calls with "naked" versions of each seems too much.
+
+-- Commented out: see Note [No assertion check on mkFunCo]
checkFunCo :: Role -> FunTyFlag -> FunTyFlag
-> CoercionN -> Coercion -> Coercion
-> Maybe SDoc
@@ -875,6 +879,7 @@ checkFunCo _r afl afr _w arg_co res_co
ok ty = isTYPEorCONSTRAINT (typeKind ty)
pp_ty str ty = text str <> colon <+> hang (ppr ty)
2 (dcolon <+> ppr (typeKind ty))
+-}
-- | Apply a 'Coercion' to another 'Coercion'.
-- The second coercion must be Nominal, unless the first is Phantom.
@@ -2068,7 +2073,7 @@ ty_co_subst !lc role ty
liftCoSubstTyVar lc r tv
go r (AppTy ty1 ty2) = mkAppCo (go r ty1) (go Nominal ty2)
go r (TyConApp tc tys) = mkTyConAppCo r tc (zipWith go (tyConRoleListX r tc) tys)
- go r (FunTy af w t1 t2) = mkFunCo1 r af (go Nominal w) (go r t1) (go r t2)
+ go r (FunTy af w t1 t2) = mkFunCo r af (go Nominal w) (go r t1) (go r t2)
go r t@(ForAllTy (Bndr v _) ty)
= let (lc', v', h) = liftCoSubstVarBndr lc v
body_co = ty_co_subst lc' r ty in
@@ -2597,7 +2602,8 @@ mkCoercionType Phantom = \ty1 ty2 ->
in
TyConApp eqPhantPrimTyCon [ki1, ki2, ty1, ty2]
--- | Creates a primitive type equality predicate.
+-- | Creates a primitive nominal type equality predicate.
+-- t1 ~# t2
-- Invariant: the types are not Coercions
mkPrimEqPred :: Type -> Type -> Type
mkPrimEqPred ty1 ty2
@@ -2606,22 +2612,9 @@ mkPrimEqPred ty1 ty2
k1 = typeKind ty1
k2 = typeKind ty2
--- | Makes a lifted equality predicate at the given role
-mkPrimEqPredRole :: Role -> Type -> Type -> PredType
-mkPrimEqPredRole Nominal = mkPrimEqPred
-mkPrimEqPredRole Representational = mkReprPrimEqPred
-mkPrimEqPredRole Phantom = panic "mkPrimEqPredRole phantom"
-
--- | Creates a primitive type equality predicate with explicit kinds
-mkHeteroPrimEqPred :: Kind -> Kind -> Type -> Type -> Type
-mkHeteroPrimEqPred k1 k2 ty1 ty2 = mkTyConApp eqPrimTyCon [k1, k2, ty1, ty2]
-
--- | Creates a primitive representational type equality predicate
--- with explicit kinds
-mkHeteroReprPrimEqPred :: Kind -> Kind -> Type -> Type -> Type
-mkHeteroReprPrimEqPred k1 k2 ty1 ty2
- = mkTyConApp eqReprPrimTyCon [k1, k2, ty1, ty2]
-
+-- | Creates a primitive representational type equality predicate.
+-- t1 ~R# t2
+-- Invariant: the types are not Coercions
mkReprPrimEqPred :: Type -> Type -> Type
mkReprPrimEqPred ty1 ty2
= mkTyConApp eqReprPrimTyCon [k1, k2, ty1, ty2]
@@ -2629,6 +2622,17 @@ mkReprPrimEqPred ty1 ty2
k1 = typeKind ty1
k2 = typeKind ty2
+-- | Makes a lifted equality predicate at the given role
+mkPrimEqPredRole :: Role -> Type -> Type -> PredType
+mkPrimEqPredRole Nominal = mkPrimEqPred
+mkPrimEqPredRole Representational = mkReprPrimEqPred
+mkPrimEqPredRole Phantom = panic "mkPrimEqPredRole phantom"
+
+-- | Creates a primitive nominal type equality predicate with an explicit
+-- (but homogeneous) kind: (~#) k k ty1 ty2
+mkNomPrimEqPred :: Kind -> Type -> Type -> Type
+mkNomPrimEqPred k ty1 ty2 = mkTyConApp eqPrimTyCon [k, k, ty1, ty2]
+
-- | Assuming that two types are the same, ignoring coercions, find
-- a nominal coercion between the types. This is useful when optimizing
-- transitivity over coercion applications, where splitting two
@@ -2659,7 +2663,7 @@ buildCoercion orig_ty1 orig_ty2 = go orig_ty1 orig_ty2
go (FunTy { ft_af = af1, ft_mult = w1, ft_arg = arg1, ft_res = res1 })
(FunTy { ft_af = af2, ft_mult = w2, ft_arg = arg2, ft_res = res2 })
= assert (af1 == af2) $
- mkFunCo1 Nominal af1 (go w1 w2) (go arg1 arg2) (go res1 res2)
+ mkFunCo Nominal af1 (go w1 w2) (go arg1 arg2) (go res1 res2)
go (TyConApp tc1 args1) (TyConApp tc2 args2)
= assert (tc1 == tc2) $
@@ -2740,15 +2744,17 @@ has_co_hole_co :: Coercion -> Monoid.Any
folder = TyCoFolder { tcf_view = noView
, tcf_tyvar = const2 (Monoid.Any False)
, tcf_covar = const2 (Monoid.Any False)
- , tcf_hole = const2 (Monoid.Any True)
+ , tcf_hole = \_ hole -> Monoid.Any (isHeteroKindCoHole hole)
, tcf_tycobinder = const2
}
--- | Is there a coercion hole in this type?
+-- | Is there a hetero-kind coercion hole in this type?
+-- (That is, a coercion hole with ch_hetero_kind=True.)
+-- See wrinkle (EIK2) of Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Equality
hasCoercionHoleTy :: Type -> Bool
hasCoercionHoleTy = Monoid.getAny . has_co_hole_ty
--- | Is there a coercion hole in this coercion?
+-- | Is there a hetero-kind coercion hole in this coercion?
hasCoercionHoleCo :: Coercion -> Bool
hasCoercionHoleCo = Monoid.getAny . has_co_hole_co
diff --git a/compiler/GHC/Core/Coercion.hs-boot b/compiler/GHC/Core/Coercion.hs-boot
index 0d56cf628c..3143414feb 100644
--- a/compiler/GHC/Core/Coercion.hs-boot
+++ b/compiler/GHC/Core/Coercion.hs-boot
@@ -17,9 +17,9 @@ mkReflCo :: Role -> Type -> Coercion
mkTyConAppCo :: HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
mkAppCo :: Coercion -> Coercion -> Coercion
mkForAllCo :: TyCoVar -> Coercion -> Coercion -> Coercion
-mkFunCo1 :: HasDebugCallStack => Role -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion
-mkNakedFunCo1 :: Role -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion
-mkFunCo2 :: HasDebugCallStack => Role -> FunTyFlag -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion
+mkFunCo :: Role -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion
+mkNakedFunCo :: Role -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion
+mkFunCo2 :: Role -> FunTyFlag -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion
mkCoVarCo :: CoVar -> Coercion
mkAxiomInstCo :: CoAxiom Branched -> BranchIndex -> [Coercion] -> Coercion
mkPhantomCo :: Coercion -> Type -> Type -> Coercion
diff --git a/compiler/GHC/Core/Predicate.hs b/compiler/GHC/Core/Predicate.hs
index c8d280259a..2fc07e1be1 100644
--- a/compiler/GHC/Core/Predicate.hs
+++ b/compiler/GHC/Core/Predicate.hs
@@ -16,7 +16,7 @@ module GHC.Core.Predicate (
getEqPredTys, getEqPredTys_maybe, getEqPredRole,
predTypeEqRel,
mkPrimEqPred, mkReprPrimEqPred, mkPrimEqPredRole,
- mkHeteroPrimEqPred, mkHeteroReprPrimEqPred,
+ mkNomPrimEqPred,
-- Class predicates
mkClassPred, isDictTy, typeDeterminesValue,
diff --git a/compiler/GHC/Core/Reduction.hs b/compiler/GHC/Core/Reduction.hs
index 07d7a93748..a4f1df4f70 100644
--- a/compiler/GHC/Core/Reduction.hs
+++ b/compiler/GHC/Core/Reduction.hs
@@ -361,8 +361,8 @@ mkFunRedn r af
(Reduction arg_co arg_ty)
(Reduction res_co res_ty)
= mkReduction
- (mkFunCo1 r af w_co arg_co res_co)
- (mkFunTy af w_ty arg_ty res_ty)
+ (mkFunCo r af w_co arg_co res_co)
+ (mkFunTy af w_ty arg_ty res_ty)
{-# INLINE mkFunRedn #-}
-- | Create a 'Reduction' associated to a Π type,
diff --git a/compiler/GHC/Core/TyCo/Compare.hs b/compiler/GHC/Core/TyCo/Compare.hs
index 4ef9d04eb8..9c32675d3e 100644
--- a/compiler/GHC/Core/TyCo/Compare.hs
+++ b/compiler/GHC/Core/TyCo/Compare.hs
@@ -379,7 +379,7 @@ We perform this optimisation in a number of places:
* GHC.Core.Types.eqType
* GHC.Core.Types.nonDetCmpType
* GHC.Core.Unify.unify_ty
- * TcCanonical.can_eq_nc'
+ * GHC.Tc.Solver.Equality.can_eq_nc'
* TcUnify.uType
This optimisation is especially helpful for the ubiquitous GHC.Types.Type,
diff --git a/compiler/GHC/Core/TyCo/Rep.hs b/compiler/GHC/Core/TyCo/Rep.hs
index 8417ded123..245a1c507b 100644
--- a/compiler/GHC/Core/TyCo/Rep.hs
+++ b/compiler/GHC/Core/TyCo/Rep.hs
@@ -38,7 +38,7 @@ module GHC.Core.TyCo.Rep (
-- * Coercions
Coercion(..), CoSel(..), FunSel(..),
UnivCoProvenance(..),
- CoercionHole(..), coHoleCoVar, setCoHoleCoVar,
+ CoercionHole(..), coHoleCoVar, setCoHoleCoVar, isHeteroKindCoHole,
CoercionN, CoercionR, CoercionP, KindCoercion,
MCoercion(..), MCoercionR, MCoercionN,
@@ -1454,12 +1454,20 @@ data CoercionHole
= CoercionHole { ch_co_var :: CoVar
-- See Note [CoercionHoles and coercion free variables]
- , ch_ref :: IORef (Maybe Coercion)
+ , ch_ref :: IORef (Maybe Coercion)
+
+ , ch_hetero_kind :: Bool
+ -- True <=> arises from a kind-level equality
+ -- See Note [Equalities with incompatible kinds]
+ -- in GHC.Tc.Solver.Equality, wrinkle (EIK2)
}
coHoleCoVar :: CoercionHole -> CoVar
coHoleCoVar = ch_co_var
+isHeteroKindCoHole :: CoercionHole -> Bool
+isHeteroKindCoHole = ch_hetero_kind
+
setCoHoleCoVar :: CoercionHole -> CoVar -> CoercionHole
setCoHoleCoVar h cv = h { ch_co_var = cv }
@@ -1470,7 +1478,8 @@ instance Data.Data CoercionHole where
dataTypeOf _ = mkNoRepType "CoercionHole"
instance Outputable CoercionHole where
- ppr (CoercionHole { ch_co_var = cv }) = braces (ppr cv)
+ ppr (CoercionHole { ch_co_var = cv, ch_hetero_kind = hk })
+ = braces (ppr cv <> ppWhen hk (text "[hk]"))
instance Uniquable CoercionHole where
getUnique (CoercionHole { ch_co_var = cv }) = getUnique cv
diff --git a/compiler/GHC/Core/TyCo/Subst.hs b/compiler/GHC/Core/TyCo/Subst.hs
index ebf87dae94..4224bd127b 100644
--- a/compiler/GHC/Core/TyCo/Subst.hs
+++ b/compiler/GHC/Core/TyCo/Subst.hs
@@ -387,9 +387,9 @@ extendTvSubstWithClone :: Subst -> TyVar -> TyVar -> Subst
-- those variables should be in scope already
extendTvSubstWithClone (Subst in_scope idenv tenv cenv) tv tv'
= Subst (extendInScopeSet in_scope tv')
- idenv
- (extendVarEnv tenv tv (mkTyVarTy tv'))
- cenv
+ idenv
+ (extendVarEnv tenv tv (mkTyVarTy tv'))
+ cenv
-- | Add a substitution from a 'CoVar' to a 'Coercion' to the 'Subst':
-- you must ensure that the in-scope set satisfies
diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs
index 796fb5aecd..5e4be72a34 100644
--- a/compiler/GHC/Core/Type.hs
+++ b/compiler/GHC/Core/Type.hs
@@ -274,7 +274,7 @@ import {-# SOURCE #-} GHC.Core.Coercion
, mkTyConAppCo, mkAppCo
, mkForAllCo, mkFunCo2, mkAxiomInstCo, mkUnivCo
, mkSymCo, mkTransCo, mkSelCo, mkLRCo, mkInstCo
- , mkKindCo, mkSubCo, mkFunCo1
+ , mkKindCo, mkSubCo, mkFunCo
, decomposePiCos, coercionKind
, coercionRKind, coercionType
, isReflexiveCo, seqCo
@@ -1332,7 +1332,7 @@ tyConAppFunCo_maybe :: HasDebugCallStack => Role -> TyCon -> [Coercion]
-- ^ Return Just if this TyConAppCo should be represented as a FunCo
tyConAppFunCo_maybe r tc cos
| Just (af, mult, arg, res) <- ty_con_app_fun_maybe (mkReflCo r manyDataConTy) tc cos
- = Just (mkFunCo1 r af mult arg res)
+ = Just (mkFunCo r af mult arg res)
| otherwise = Nothing
ty_con_app_fun_maybe :: (HasDebugCallStack, Outputable a) => a -> TyCon -> [a]
View Lorry Controller Status