summaryrefslogtreecommitdiff
path: root/compiler/GHC/Tc
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/GHC/Tc')
-rw-r--r--compiler/GHC/Tc/Errors/Ppr.hs7
-rw-r--r--compiler/GHC/Tc/Errors/Types.hs36
-rw-r--r--compiler/GHC/Tc/Gen/HsType.hs34
-rw-r--r--compiler/GHC/Tc/Solver/Rewrite.hs4
-rw-r--r--compiler/GHC/Tc/TyCl.hs3
-rw-r--r--compiler/GHC/Tc/Utils/Instantiate.hs66
-rw-r--r--compiler/GHC/Tc/Utils/TcType.hs4
-rw-r--r--compiler/GHC/Tc/Utils/Unify.hs-boot1
-rw-r--r--compiler/GHC/Tc/Validity.hs30
9 files changed, 71 insertions, 114 deletions
diff --git a/compiler/GHC/Tc/Errors/Ppr.hs b/compiler/GHC/Tc/Errors/Ppr.hs
index d13aa6b21d..00b37709bd 100644
--- a/compiler/GHC/Tc/Errors/Ppr.hs
+++ b/compiler/GHC/Tc/Errors/Ppr.hs
@@ -913,9 +913,10 @@ instance Diagnostic TcRnMessage where
2 (parens reason))
where
reason = case err of
- ConstrainedDataConPE pred
+ ConstrainedDataConPE theta
-> text "it has an unpromotable context"
- <+> quotes (ppr pred)
+ <+> quotes (pprTheta theta)
+
FamDataConPE -> text "it comes from a data family instance"
NoDataKindsDC -> text "perhaps you intended to use DataKinds"
PatSynPE -> text "pattern synonyms cannot be promoted"
@@ -3385,7 +3386,7 @@ pprHoleError ctxt (Hole { hole_ty, hole_occ}) (HoleError sort other_tvs hole_sko
2 (text "standing for" <+> quotes pp_hole_type_with_kind)
ConstraintHole ->
hang (text "Found extra-constraints wildcard standing for")
- 2 (quotes $ pprType hole_ty) -- always kind constraint
+ 2 (quotes $ pprType hole_ty) -- always kind Constraint
hole_kind = typeKind hole_ty
diff --git a/compiler/GHC/Tc/Errors/Types.hs b/compiler/GHC/Tc/Errors/Types.hs
index 335e7c4965..f4d7d85ed1 100644
--- a/compiler/GHC/Tc/Errors/Types.hs
+++ b/compiler/GHC/Tc/Errors/Types.hs
@@ -3854,9 +3854,8 @@ data PromotionErr
| FamDataConPE -- Data constructor for a data family
-- See Note [AFamDataCon: not promoting data family constructors]
-- in GHC.Tc.Utils.Env.
- | ConstrainedDataConPE PredType
- -- Data constructor with a non-equality context
- -- See Note [Constraints in kinds] in GHC.Core.TyCo.Rep
+ | ConstrainedDataConPE ThetaType -- Data constructor with a context
+ -- See Note [No constraints in kinds] in GHC.Tc.Validity
| PatSynPE -- Pattern synonyms
-- See Note [Don't promote pattern synonyms] in GHC.Tc.Utils.Env
@@ -3866,28 +3865,27 @@ data PromotionErr
| NoDataKindsDC -- -XDataKinds not enabled (for a datacon)
instance Outputable PromotionErr where
- ppr ClassPE = text "ClassPE"
- ppr TyConPE = text "TyConPE"
- ppr PatSynPE = text "PatSynPE"
- ppr FamDataConPE = text "FamDataConPE"
- ppr (ConstrainedDataConPE pred) = text "ConstrainedDataConPE"
- <+> parens (ppr pred)
- ppr RecDataConPE = text "RecDataConPE"
- ppr NoDataKindsDC = text "NoDataKindsDC"
- ppr TermVariablePE = text "TermVariablePE"
+ ppr ClassPE = text "ClassPE"
+ ppr TyConPE = text "TyConPE"
+ ppr PatSynPE = text "PatSynPE"
+ ppr FamDataConPE = text "FamDataConPE"
+ ppr (ConstrainedDataConPE theta) = text "ConstrainedDataConPE" <+> parens (ppr theta)
+ ppr RecDataConPE = text "RecDataConPE"
+ ppr NoDataKindsDC = text "NoDataKindsDC"
+ ppr TermVariablePE = text "TermVariablePE"
pprPECategory :: PromotionErr -> SDoc
pprPECategory = text . capitalise . peCategory
peCategory :: PromotionErr -> String
-peCategory ClassPE = "class"
-peCategory TyConPE = "type constructor"
-peCategory PatSynPE = "pattern synonym"
-peCategory FamDataConPE = "data constructor"
+peCategory ClassPE = "class"
+peCategory TyConPE = "type constructor"
+peCategory PatSynPE = "pattern synonym"
+peCategory FamDataConPE = "data constructor"
peCategory ConstrainedDataConPE{} = "data constructor"
-peCategory RecDataConPE = "data constructor"
-peCategory NoDataKindsDC = "data constructor"
-peCategory TermVariablePE = "term variable"
+peCategory RecDataConPE = "data constructor"
+peCategory NoDataKindsDC = "data constructor"
+peCategory TermVariablePE = "term variable"
-- | Stores the information to be reported in a representation-polymorphism
-- error message.
diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs
index 9d9f597db2..a0a2a51cee 100644
--- a/compiler/GHC/Tc/Gen/HsType.hs
+++ b/compiler/GHC/Tc/Gen/HsType.hs
@@ -137,7 +137,7 @@ import GHC.Data.Bag( unitBag )
import Data.Function ( on )
import Data.List.NonEmpty ( NonEmpty(..), nonEmpty )
import qualified Data.List.NonEmpty as NE
-import Data.List ( find, mapAccumL )
+import Data.List ( mapAccumL )
import Control.Monad
import Data.Tuple( swap )
@@ -1613,8 +1613,7 @@ tcInferTyApps_nosat mode orig_hs_ty fun orig_hs_args
case ki_binder of
-- FunTy with PredTy on LHS, or ForAllTy with Inferred
- Named (Bndr _ Inferred) -> instantiate ki_binder inner_ki
- Anon _ af | isInvisibleFunArg af -> instantiate ki_binder inner_ki
+ Named (Bndr kv Inferred) -> instantiate kv inner_ki
Named (Bndr _ Specified) -> -- Visible kind application
do { traceTc "tcInferTyApps (vis kind app)"
@@ -1644,9 +1643,9 @@ tcInferTyApps_nosat mode orig_hs_ty fun orig_hs_args
---------------- HsValArg: a normal argument (fun ty)
(HsValArg arg : args, Just (ki_binder, inner_ki))
-- next binder is invisible; need to instantiate it
- | isInvisiblePiTyBinder ki_binder -- FunTy with constraint on LHS;
- -- or ForAllTy with Inferred or Specified
- -> instantiate ki_binder inner_ki
+ | Named (Bndr kv flag) <- ki_binder
+ , isInvisibleForAllTyFlag flag -- ForAllTy with Inferred or Specified
+ -> instantiate kv inner_ki
-- "normal" case
| otherwise
@@ -1984,23 +1983,16 @@ tcTyVar name -- Could be a tyvar, a tycon, or a datacon
-- see #15245
promotionErr name FamDataConPE
; let (_, _, _, theta, _, _) = dataConFullSig dc
- ; traceTc "tcTyVar" (ppr dc <+> ppr theta $$ ppr (dc_theta_illegal_constraint theta))
- ; case dc_theta_illegal_constraint theta of
- Just pred -> promotionErr name $
- ConstrainedDataConPE pred
- Nothing -> pure ()
+ ; traceTc "tcTyVar" (ppr dc <+> ppr theta)
+ -- promotionErr: Note [No constraints in kinds] in GHC.Tc.Validity
+ ; unless (null theta) $
+ promotionErr name (ConstrainedDataConPE theta)
; let tc = promoteDataCon dc
; return (mkTyConApp tc [], tyConKind tc) }
APromotionErr err -> promotionErr name err
_ -> wrongThingErr "type" thing name }
- where
- -- We cannot promote a data constructor with a context that contains
- -- constraints other than equalities, so error if we find one.
- -- See Note [Constraints in kinds] in GHC.Core.TyCo.Rep
- dc_theta_illegal_constraint :: ThetaType -> Maybe PredType
- dc_theta_illegal_constraint = find (not . isEqPred)
{-
Note [Recursion through the kinds]
@@ -3715,9 +3707,10 @@ splitTyConKind skol_info in_scope avoid_occs kind
Nothing -> (reverse acc, substTy subst kind)
Just (Anon arg af, kind')
- -> go occs' uniqs' subst' (tcb : acc) kind'
+ -> assert (af == FTF_T_T) $
+ go occs' uniqs' subst' (tcb : acc) kind'
where
- tcb = Bndr tv (AnonTCB af)
+ tcb = Bndr tv AnonTCB
arg' = substTy subst (scaledThing arg)
name = mkInternalName uniq occ loc
tv = mkTcTyVar name arg' details
@@ -3858,7 +3851,8 @@ tcbVisibilities tc orig_args
go fun_kind subst all_args@(arg : args)
| Just (tcb, inner_kind) <- splitPiTy_maybe fun_kind
= case tcb of
- Anon _ af -> AnonTCB af : go inner_kind subst args
+ Anon _ af -> assert (af == FTF_T_T) $
+ AnonTCB : go inner_kind subst args
Named (Bndr tv vis) -> NamedTCB vis : go inner_kind subst' args
where
subst' = extendTCvSubst subst tv arg
diff --git a/compiler/GHC/Tc/Solver/Rewrite.hs b/compiler/GHC/Tc/Solver/Rewrite.hs
index 252e2aba52..6892e9853f 100644
--- a/compiler/GHC/Tc/Solver/Rewrite.hs
+++ b/compiler/GHC/Tc/Solver/Rewrite.hs
@@ -1077,7 +1077,7 @@ ty_con_binders_ty_binders' = foldr go ([], False)
where
go (Bndr tv (NamedTCB vis)) (bndrs, _)
= (Named (Bndr tv vis) : bndrs, True)
- go (Bndr tv (AnonTCB af)) (bndrs, n)
- = (Anon (tymult (tyVarKind tv)) af : bndrs, n)
+ go (Bndr tv AnonTCB) (bndrs, n)
+ = (Anon (tymult (tyVarKind tv)) FTF_T_T : bndrs, n)
{-# INLINE go #-}
{-# INLINE ty_con_binders_ty_binders' #-}
diff --git a/compiler/GHC/Tc/TyCl.hs b/compiler/GHC/Tc/TyCl.hs
index c5f924cea8..32c64b6c7f 100644
--- a/compiler/GHC/Tc/TyCl.hs
+++ b/compiler/GHC/Tc/TyCl.hs
@@ -4069,8 +4069,7 @@ mkGADTVars tmpl_tvs dc_tvs subst
tv_kind = tyVarKind t_tv
tv_kind' = substTy t_sub tv_kind
t_tv' = setTyVarKind t_tv tv_kind'
- eqs' | isConstraintLikeKind (typeKind tv_kind') = eqs
- | otherwise = (t_tv', r_ty) : eqs
+ eqs' = (t_tv', r_ty) : eqs
| otherwise
= pprPanic "mkGADTVars" (ppr tmpl_tvs $$ ppr subst)
diff --git a/compiler/GHC/Tc/Utils/Instantiate.hs b/compiler/GHC/Tc/Utils/Instantiate.hs
index abbee42526..0b6b519028 100644
--- a/compiler/GHC/Tc/Utils/Instantiate.hs
+++ b/compiler/GHC/Tc/Utils/Instantiate.hs
@@ -43,7 +43,7 @@ import GHC.Prelude
import GHC.Driver.Session
import GHC.Driver.Env
-import GHC.Builtin.Types ( heqDataCon, eqDataCon, integerTyConName )
+import GHC.Builtin.Types ( heqDataCon, integerTyConName )
import GHC.Builtin.Names
import GHC.Hs
@@ -53,14 +53,12 @@ import GHC.Core.InstEnv
import GHC.Core.Predicate
import GHC.Core ( Expr(..), isOrphan ) -- For the Coercion constructor
import GHC.Core.Type
-import GHC.Core.Multiplicity
-import GHC.Core.TyCo.Rep
import GHC.Core.TyCo.Ppr ( debugPprType )
import GHC.Core.Class( Class )
import GHC.Core.DataCon
import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcCheckPolyExpr, tcSyntaxOp )
-import {-# SOURCE #-} GHC.Tc.Utils.Unify( unifyType, unifyKind )
+import {-# SOURCE #-} GHC.Tc.Utils.Unify( unifyType )
import GHC.Tc.Utils.Zonk
import GHC.Tc.Utils.Monad
import GHC.Tc.Types.Constraint
@@ -386,71 +384,21 @@ tcInstInvisibleTyBindersN n ty
go n subst kind
| n > 0
- , Just (bndr, body) <- tcSplitPiTy_maybe kind
- , isInvisiblePiTyBinder bndr
- = do { (subst', arg) <- tcInstInvisibleTyBinder subst bndr
+ , Just (bndr, body) <- tcSplitForAllTyVarBinder_maybe kind
+ , isInvisibleForAllTyFlag (binderFlag bndr)
+ = do { (subst', arg) <- tcInstInvisibleTyBinder subst (binderVar bndr)
; (args, inner_ty) <- go (n-1) subst' body
; return (arg:args, inner_ty) }
| otherwise
= return ([], substTy subst kind)
-tcInstInvisibleTyBinder :: Subst -> PiTyVarBinder -> TcM (Subst, TcType)
+tcInstInvisibleTyBinder :: Subst -> TyVar -> TcM (Subst, TcType)
-- Called only to instantiate kinds, in user-written type signatures
-tcInstInvisibleTyBinder subst (Named (Bndr tv _))
+tcInstInvisibleTyBinder subst tv
= do { (subst', tv') <- newMetaTyVarX subst tv
; return (subst', mkTyVarTy tv') }
-tcInstInvisibleTyBinder subst (Anon ty af)
- | Just (mk, k1, k2) <- get_eq_tys_maybe (substTy subst (scaledThing ty))
- -- For kinds like (k1 ~ k2) => blah, we want to emit a unification
- -- constraint for (k1 ~# k2) and return the argument (Eq# k1 k2)
- -- See Note [Constraints in kinds] in GHC.Core.TyCo.Rep
- -- Equality is the *only* constraint currently handled in types.
- = assert (isInvisibleFunArg af) $
- do { co <- unifyKind Nothing k1 k2
- ; return (subst, mk co) }
-
- | otherwise -- This should never happen
- -- See GHC.Core.TyCo.Rep Note [Constraints in kinds]
- = pprPanic "tcInvisibleTyBinder" (ppr ty)
-
--------------------------------
-get_eq_tys_maybe :: Type
- -> Maybe ( Coercion -> Type
- -- Given a coercion proving t1 ~# t2, produce the
- -- right instantiation for the PiTyVarBinder at hand
- , Type -- t1
- , Type -- t2
- )
--- See Note [Constraints in kinds] in GHC.Core.TyCo.Rep
-get_eq_tys_maybe ty
- -- Lifted heterogeneous equality (~~)
- | Just (tc, [_, _, k1, k2]) <- splitTyConApp_maybe ty
- , tc `hasKey` heqTyConKey
- = Just (mkHEqBoxTy k1 k2, k1, k2)
-
- -- Lifted homogeneous equality (~)
- | Just (tc, [_, k1, k2]) <- splitTyConApp_maybe ty
- , tc `hasKey` eqTyConKey
- = Just (mkEqBoxTy k1 k2, k1, k2)
-
- | otherwise
- = Nothing
-
--- | This takes @a ~# b@ and returns @a ~~ b@.
-mkHEqBoxTy :: Type -> Type -> TcCoercion -> Type
-mkHEqBoxTy ty1 ty2 co
- = mkTyConApp (promoteDataCon heqDataCon) [k1, k2, ty1, ty2, mkCoercionTy co]
- where k1 = typeKind ty1
- k2 = typeKind ty2
-
--- | This takes @a ~# b@ and returns @a ~ b@.
-mkEqBoxTy :: Type -> Type -> TcCoercion -> Type
-mkEqBoxTy ty1 ty2 co
- = mkTyConApp (promoteDataCon eqDataCon) [k, ty1, ty2, mkCoercionTy co]
- where k = typeKind ty1
-
{- *********************************************************************
* *
SkolemTvs (immutable)
diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs
index 98b8e2ae76..28894d68ed 100644
--- a/compiler/GHC/Tc/Utils/TcType.hs
+++ b/compiler/GHC/Tc/Utils/TcType.hs
@@ -1342,7 +1342,7 @@ getDFunTyLitKey (CharTyLit n) = mkOccName Name.varName (show n)
-- Always succeeds, even if it returns an empty list.
tcSplitPiTys :: Type -> ([PiTyVarBinder], Type)
tcSplitPiTys ty
- = assert (all isTyBinder (fst sty) ) -- No CoVar binders here
+ = assert (all isTyBinder (fst sty)) -- No CoVar binders here
sty
where sty = splitPiTys ty
@@ -1365,7 +1365,7 @@ tcSplitForAllTyVarBinder_maybe _ = Nothing
-- returning just the tyvars.
tcSplitForAllTyVars :: Type -> ([TyVar], Type)
tcSplitForAllTyVars ty
- = assert (all isTyVar (fst sty) ) sty
+ = assert (all isTyVar (fst sty)) sty
where sty = splitForAllTyCoVars ty
-- | Like 'tcSplitForAllTyVars', but only splits 'ForAllTy's with 'Invisible'
diff --git a/compiler/GHC/Tc/Utils/Unify.hs-boot b/compiler/GHC/Tc/Utils/Unify.hs-boot
index 8afdbcd5ed..0d82ea613e 100644
--- a/compiler/GHC/Tc/Utils/Unify.hs-boot
+++ b/compiler/GHC/Tc/Utils/Unify.hs-boot
@@ -12,6 +12,5 @@ import GHC.Tc.Types.Origin ( CtOrigin, TypedThing )
-- GHC.Tc.Utils.Unify and GHC.Tc.Utils.Instantiate
unifyType :: Maybe TypedThing -> TcTauType -> TcTauType -> TcM TcCoercion
-unifyKind :: Maybe TypedThing -> TcTauType -> TcTauType -> TcM TcCoercion
tcSubMult :: CtOrigin -> Mult -> Mult -> TcM HsWrapper
diff --git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs
index 5ac3377a33..949eb90d53 100644
--- a/compiler/GHC/Tc/Validity.hs
+++ b/compiler/GHC/Tc/Validity.hs
@@ -520,6 +520,8 @@ typeOrKindCtxt (DataKindCtxt {}) = OnlyKindCtxt
typeOrKindCtxt (TySynKindCtxt {}) = OnlyKindCtxt
typeOrKindCtxt (TyFamResKindCtxt {}) = OnlyKindCtxt
+-- These cases are also described in Note [No constraints in kinds], so any
+-- change here should be reflected in that note.
typeOrKindCtxt (TySynCtxt {}) = BothTypeAndKindCtxt
-- Type synonyms can have types and kinds on their RHSs
typeOrKindCtxt (GhciCtxt {}) = BothTypeAndKindCtxt
@@ -543,7 +545,6 @@ typeLevelUserTypeCtxt ctxt = case typeOrKindCtxt ctxt of
-- | Returns 'True' if the supplied 'UserTypeCtxt' is unambiguously not the
-- context for a kind of a type, where the arbitrary use of constraints is
-- currently disallowed.
--- (See @Note [Constraints in kinds]@ in "GHC.Core.TyCo.Rep".)
allConstraintsAllowed :: UserTypeCtxt -> Bool
allConstraintsAllowed = typeLevelUserTypeCtxt
@@ -931,10 +932,9 @@ checkConstraintsOK :: ValidityEnv -> ThetaType -> Type -> TcM ()
checkConstraintsOK ve theta ty
| null theta = return ()
| allConstraintsAllowed (ve_ctxt ve) = return ()
- | otherwise
- = -- We are in a kind, where we allow only equality predicates
- -- See Note [Constraints in kinds] in GHC.Core.TyCo.Rep, and #16263
- checkTcM (all isEqPred theta) (env, TcRnConstraintInKind (tidyType env ty))
+ | otherwise -- We are unambiguously in a kind; see
+ -- Note [No constraints in kinds]
+ = failWithTcM (env, TcRnConstraintInKind (tidyType env ty))
where env = ve_tidy_env ve
checkVdqOK :: ValidityEnv -> [TyVarBinder] -> Type -> TcM ()
@@ -945,7 +945,25 @@ checkVdqOK ve tvbs ty = do
no_vdq = all (isInvisibleForAllTyFlag . binderFlag) tvbs
ValidityEnv{ve_tidy_env = env, ve_ctxt = ctxt} = ve
-{-
+{- Note [No constraints in kinds]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+GHC does not allow constraints in kinds. Equality constraints
+in kinds were allowed from GHC 8.0, but this "feature" was removed
+as part of Proposal #547 (https://github.com/ghc-proposals/ghc-proposals/pull/547),
+which contains further context and motivation for the removal.
+
+The lack of constraints in kinds is enforced by checkConstraintsOK, which
+uses the UserTypeCtxt to determine if we are unambiguously checking a kind.
+There are two ambiguous contexts (constructor BothTypeAndKindCtxt of TypeOrKindCtxt)
+as written in typeOfKindCtxt:
+ - TySynCtxt: this is the RHS of a type synonym. We check the expansion of type
+ synonyms for constraints, so this is handled at the usage site of the synonym.
+ - GhciCtxt: This is the type in a :kind command. A constraint here does not cause
+ any trouble, because the type cannot be used to classify a type.
+
+Beyond these two cases, we also promote data constructors. We check for constraints
+in data constructor types in GHC.Tc.Gen.HsType.tcTyVar.
+
Note [Liberal type synonyms]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
If -XLiberalTypeSynonyms is on, expand closed type synonyms *before*
View Lorry Controller Status