{-# LANGUAGE CPP #-}
{-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
module GHC.Tc.Validity (
Rank, UserTypeCtxt(..), checkValidType, checkValidMonoType,
checkValidTheta,
checkValidInstance, checkValidInstHead, validDerivPred,
checkTySynRhs,
checkValidCoAxiom, checkValidCoAxBranch,
checkValidTyFamEqn, checkValidAssocTyFamDeflt, checkConsistentFamInst,
badATErr, arityErr,
checkTyConTelescope,
allDistinctTyVars
) where
#include "HsVersions.h"
import GHC.Prelude
import GHC.Data.Maybe
import GHC.Tc.Utils.Unify ( tcSubTypeSigma )
import GHC.Tc.Solver ( simplifyAmbiguityCheck )
import GHC.Tc.Instance.Class ( matchGlobalInst, ClsInstResult(..), InstanceWhat(..), AssocInstInfo(..) )
import GHC.Core.TyCo.FVs
import GHC.Core.TyCo.Rep
import GHC.Core.TyCo.Ppr
import GHC.Tc.Utils.TcType hiding ( sizeType, sizeTypes )
import GHC.Builtin.Types ( heqTyConName, eqTyConName, coercibleTyConName, manyDataConTy )
import GHC.Builtin.Names
import GHC.Core.Type
import GHC.Core.Unify ( tcMatchTyX_BM, BindFlag(..) )
import GHC.Core.Coercion
import GHC.Core.Coercion.Axiom
import GHC.Core.Class
import GHC.Core.TyCon
import GHC.Core.Predicate
import GHC.Tc.Types.Origin
import GHC.Iface.Type ( pprIfaceType, pprIfaceTypeApp )
import GHC.CoreToIface ( toIfaceTyCon, toIfaceTcArgs, toIfaceType )
import GHC.Hs
import GHC.Tc.Utils.Monad
import GHC.Tc.Utils.Env ( tcInitTidyEnv, tcInitOpenTidyEnv )
import GHC.Tc.Instance.FunDeps
import GHC.Core.FamInstEnv
( isDominatedBy, injectiveBranches, InjectivityCheckResult(..) )
import GHC.Tc.Instance.Family
import GHC.Types.Name
import GHC.Types.Var.Env
import GHC.Types.Var.Set
import GHC.Types.Var ( VarBndr(..), mkTyVar )
import GHC.Utils.FV
import GHC.Utils.Error
import GHC.Driver.Session
import GHC.Utils.Misc
import GHC.Data.List.SetOps
import GHC.Types.SrcLoc
import GHC.Utils.Outputable as Outputable
import GHC.Utils.Panic
import GHC.Builtin.Uniques ( mkAlphaTyVarUnique )
import GHC.Data.Bag ( emptyBag )
import qualified GHC.LanguageExtensions as LangExt
import Control.Monad
import Data.Foldable
import Data.Function
import Data.List ( (\\), nub )
import qualified Data.List.NonEmpty as NE
checkAmbiguity :: UserTypeCtxt -> Type -> TcM ()
checkAmbiguity :: UserTypeCtxt -> Type -> TcM ()
checkAmbiguity UserTypeCtxt
ctxt Type
ty
| UserTypeCtxt -> Bool
wantAmbiguityCheck UserTypeCtxt
ctxt
= do { String -> SDoc -> TcM ()
traceTc String
"Ambiguity check for" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty)
; Bool
allow_ambiguous <- Extension -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. Extension -> TcRnIf gbl lcl Bool
xoptM Extension
LangExt.AllowAmbiguousTypes
; (HsWrapper
_wrap, WantedConstraints
wanted) <- SDoc
-> TcM (HsWrapper, WantedConstraints)
-> TcM (HsWrapper, WantedConstraints)
forall a. SDoc -> TcM a -> TcM a
addErrCtxt (Bool -> SDoc
mk_msg Bool
allow_ambiguous) (TcM (HsWrapper, WantedConstraints)
-> TcM (HsWrapper, WantedConstraints))
-> TcM (HsWrapper, WantedConstraints)
-> TcM (HsWrapper, WantedConstraints)
forall a b. (a -> b) -> a -> b
$
TcM HsWrapper -> TcM (HsWrapper, WantedConstraints)
forall a. TcM a -> TcM (a, WantedConstraints)
captureConstraints (TcM HsWrapper -> TcM (HsWrapper, WantedConstraints))
-> TcM HsWrapper -> TcM (HsWrapper, WantedConstraints)
forall a b. (a -> b) -> a -> b
$
UserTypeCtxt -> Type -> Type -> TcM HsWrapper
tcSubTypeSigma UserTypeCtxt
ctxt Type
ty Type
ty
; Type -> WantedConstraints -> TcM ()
simplifyAmbiguityCheck Type
ty WantedConstraints
wanted
; String -> SDoc -> TcM ()
traceTc String
"Done ambiguity check for" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty) }
| Bool
otherwise
= () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
where
mk_msg :: Bool -> SDoc
mk_msg Bool
allow_ambiguous
= [SDoc] -> SDoc
vcat [ String -> SDoc
text String
"In the ambiguity check for" SDoc -> SDoc -> SDoc
<+> SDoc
what
, Bool -> SDoc -> SDoc
ppUnless Bool
allow_ambiguous SDoc
ambig_msg ]
ambig_msg :: SDoc
ambig_msg = String -> SDoc
text String
"To defer the ambiguity check to use sites, enable AllowAmbiguousTypes"
what :: SDoc
what | Just Name
n <- UserTypeCtxt -> Maybe Name
isSigMaybe UserTypeCtxt
ctxt = SDoc -> SDoc
quotes (Name -> SDoc
forall a. Outputable a => a -> SDoc
ppr Name
n)
| Bool
otherwise = UserTypeCtxt -> SDoc
pprUserTypeCtxt UserTypeCtxt
ctxt
wantAmbiguityCheck :: UserTypeCtxt -> Bool
wantAmbiguityCheck :: UserTypeCtxt -> Bool
wantAmbiguityCheck UserTypeCtxt
ctxt
= case UserTypeCtxt
ctxt of
GhciCtxt {} -> Bool
False
TySynCtxt {} -> Bool
False
UserTypeCtxt
TypeAppCtxt -> Bool
False
StandaloneKindSigCtxt{} -> Bool
False
UserTypeCtxt
_ -> Bool
True
checkUserTypeError :: Type -> TcM ()
checkUserTypeError :: Type -> TcM ()
checkUserTypeError = Type -> TcM ()
check
where
check :: Type -> TcM ()
check Type
ty
| Just Type
msg <- Type -> Maybe Type
userTypeError_maybe Type
ty = Type -> TcM ()
forall {b}. Type -> IOEnv (Env TcGblEnv TcLclEnv) b
fail_with Type
msg
| Just (TyCon
_,[Type]
ts) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty = (Type -> TcM ()) -> [Type] -> TcM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Type -> TcM ()
check [Type]
ts
| Just (Type
t1,Type
t2) <- Type -> Maybe (Type, Type)
splitAppTy_maybe Type
ty = Type -> TcM ()
check Type
t1 TcM () -> TcM () -> TcM ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Type -> TcM ()
check Type
t2
| Just (TyCoVar
_,Type
t1) <- Type -> Maybe (TyCoVar, Type)
splitForAllTyCoVar_maybe Type
ty = Type -> TcM ()
check Type
t1
| Bool
otherwise = () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
fail_with :: Type -> IOEnv (Env TcGblEnv TcLclEnv) b
fail_with Type
msg = do { TidyEnv
env0 <- TcM TidyEnv
tcInitTidyEnv
; let (TidyEnv
env1, Type
tidy_msg) = TidyEnv -> Type -> (TidyEnv, Type)
tidyOpenType TidyEnv
env0 Type
msg
; (TidyEnv, SDoc) -> IOEnv (Env TcGblEnv TcLclEnv) b
forall a. (TidyEnv, SDoc) -> TcM a
failWithTcM (TidyEnv
env1, Type -> SDoc
pprUserTypeErrorTy Type
tidy_msg) }
checkValidType :: UserTypeCtxt -> Type -> TcM ()
checkValidType :: UserTypeCtxt -> Type -> TcM ()
checkValidType UserTypeCtxt
ctxt Type
ty
= do { String -> SDoc -> TcM ()
traceTc String
"checkValidType" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"::" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (HasDebugCallStack => Type -> Type
Type -> Type
tcTypeKind Type
ty))
; Bool
rankn_flag <- Extension -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. Extension -> TcRnIf gbl lcl Bool
xoptM Extension
LangExt.RankNTypes
; Bool
impred_flag <- Extension -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. Extension -> TcRnIf gbl lcl Bool
xoptM Extension
LangExt.ImpredicativeTypes
; let gen_rank :: Rank -> Rank
gen_rank :: Rank -> Rank
gen_rank Rank
r | Bool
rankn_flag = Rank
ArbitraryRank
| Bool
otherwise = Rank
r
rank1 :: Rank
rank1 = Rank -> Rank
gen_rank Rank
r1
rank0 :: Rank
rank0 = Rank -> Rank
gen_rank Rank
r0
r0 :: Rank
r0 = Rank
rankZeroMonoType
r1 :: Rank
r1 = Bool -> Rank -> Rank
LimitedRank Bool
True Rank
r0
rank :: Rank
rank
= case UserTypeCtxt
ctxt of
UserTypeCtxt
DefaultDeclCtxt-> Rank
MustBeMonoType
UserTypeCtxt
PatSigCtxt -> Rank
rank0
RuleSigCtxt Name
_ -> Rank
rank1
TySynCtxt Name
_ -> Rank
rank0
UserTypeCtxt
ExprSigCtxt -> Rank
rank1
UserTypeCtxt
KindSigCtxt -> Rank
rank1
StandaloneKindSigCtxt{} -> Rank
rank1
UserTypeCtxt
TypeAppCtxt | Bool
impred_flag -> Rank
ArbitraryRank
| Bool
otherwise -> Rank
tyConArgMonoType
FunSigCtxt {} -> Rank
rank1
InfSigCtxt {} -> Rank
rank1
ConArgCtxt Name
_ -> Rank
rank1
PatSynCtxt Name
_ -> Rank
rank1
ForSigCtxt Name
_ -> Rank
rank1
UserTypeCtxt
SpecInstCtxt -> Rank
rank1
GhciCtxt {} -> Rank
ArbitraryRank
TyVarBndrKindCtxt Name
_ -> Rank
rank0
DataKindCtxt Name
_ -> Rank
rank1
TySynKindCtxt Name
_ -> Rank
rank1
TyFamResKindCtxt Name
_ -> Rank
rank1
UserTypeCtxt
_ -> String -> Rank
forall a. String -> a
panic String
"checkValidType"
; TidyEnv
env <- [TyCoVar] -> TcM TidyEnv
tcInitOpenTidyEnv (Type -> [TyCoVar]
tyCoVarsOfTypeList Type
ty)
; ExpandMode
expand <- TcM ExpandMode
initialExpandMode
; let ve :: ValidityEnv
ve = ValidityEnv{ ve_tidy_env :: TidyEnv
ve_tidy_env = TidyEnv
env, ve_ctxt :: UserTypeCtxt
ve_ctxt = UserTypeCtxt
ctxt
, ve_rank :: Rank
ve_rank = Rank
rank, ve_expand :: ExpandMode
ve_expand = ExpandMode
expand }
; TcM () -> TcM ()
forall r. TcM r -> TcM r
checkNoErrs (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$
do { ValidityEnv -> Type -> TcM ()
check_type ValidityEnv
ve Type
ty
; Type -> TcM ()
checkUserTypeError Type
ty
; String -> SDoc -> TcM ()
traceTc String
"done ct" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty) }
; UserTypeCtxt -> Type -> TcM ()
checkAmbiguity UserTypeCtxt
ctxt Type
ty
; String -> SDoc -> TcM ()
traceTc String
"checkValidType done" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"::" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (HasDebugCallStack => Type -> Type
Type -> Type
tcTypeKind Type
ty)) }
checkValidMonoType :: Type -> TcM ()
checkValidMonoType :: Type -> TcM ()
checkValidMonoType Type
ty
= do { TidyEnv
env <- [TyCoVar] -> TcM TidyEnv
tcInitOpenTidyEnv (Type -> [TyCoVar]
tyCoVarsOfTypeList Type
ty)
; ExpandMode
expand <- TcM ExpandMode
initialExpandMode
; let ve :: ValidityEnv
ve = ValidityEnv{ ve_tidy_env :: TidyEnv
ve_tidy_env = TidyEnv
env, ve_ctxt :: UserTypeCtxt
ve_ctxt = UserTypeCtxt
SigmaCtxt
, ve_rank :: Rank
ve_rank = Rank
MustBeMonoType, ve_expand :: ExpandMode
ve_expand = ExpandMode
expand }
; ValidityEnv -> Type -> TcM ()
check_type ValidityEnv
ve Type
ty }
checkTySynRhs :: UserTypeCtxt -> TcType -> TcM ()
checkTySynRhs :: UserTypeCtxt -> Type -> TcM ()
checkTySynRhs UserTypeCtxt
ctxt Type
ty
| Type -> Bool
tcReturnsConstraintKind Type
actual_kind
= do { Bool
ck <- Extension -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. Extension -> TcRnIf gbl lcl Bool
xoptM Extension
LangExt.ConstraintKinds
; if Bool
ck
then Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Type -> Bool
tcIsConstraintKind Type
actual_kind)
(do { DynFlags
dflags <- IOEnv (Env TcGblEnv TcLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
; ExpandMode
expand <- TcM ExpandMode
initialExpandMode
; TidyEnv -> DynFlags -> UserTypeCtxt -> ExpandMode -> Type -> TcM ()
check_pred_ty TidyEnv
emptyTidyEnv DynFlags
dflags UserTypeCtxt
ctxt ExpandMode
expand Type
ty })
else (TidyEnv, SDoc) -> TcM ()
addErrTcM (TidyEnv -> Type -> (TidyEnv, SDoc)
constraintSynErr TidyEnv
emptyTidyEnv Type
actual_kind) }
| Bool
otherwise
= () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
where
actual_kind :: Type
actual_kind = HasDebugCallStack => Type -> Type
Type -> Type
tcTypeKind Type
ty
data Rank = ArbitraryRank
| LimitedRank
Bool
Rank
| MonoType SDoc
| MustBeMonoType
instance Outputable Rank where
ppr :: Rank -> SDoc
ppr Rank
ArbitraryRank = String -> SDoc
text String
"ArbitraryRank"
ppr (LimitedRank Bool
top_forall_ok Rank
r)
= String -> SDoc
text String
"LimitedRank" SDoc -> SDoc -> SDoc
<+> Bool -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bool
top_forall_ok
SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
parens (Rank -> SDoc
forall a. Outputable a => a -> SDoc
ppr Rank
r)
ppr (MonoType SDoc
msg) = String -> SDoc
text String
"MonoType" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
parens SDoc
msg
ppr Rank
MustBeMonoType = String -> SDoc
text String
"MustBeMonoType"
rankZeroMonoType, tyConArgMonoType, synArgMonoType, constraintMonoType :: Rank
rankZeroMonoType :: Rank
rankZeroMonoType = SDoc -> Rank
MonoType (String -> SDoc
text String
"Perhaps you intended to use RankNTypes")
tyConArgMonoType :: Rank
tyConArgMonoType = SDoc -> Rank
MonoType (String -> SDoc
text String
"Perhaps you intended to use ImpredicativeTypes")
synArgMonoType :: Rank
synArgMonoType = SDoc -> Rank
MonoType (String -> SDoc
text String
"Perhaps you intended to use LiberalTypeSynonyms")
constraintMonoType :: Rank
constraintMonoType = SDoc -> Rank
MonoType ([SDoc] -> SDoc
vcat [ String -> SDoc
text String
"A constraint must be a monotype"
, String -> SDoc
text String
"Perhaps you intended to use QuantifiedConstraints" ])
funArgResRank :: Rank -> (Rank, Rank)
funArgResRank :: Rank -> (Rank, Rank)
funArgResRank (LimitedRank Bool
_ Rank
arg_rank) = (Rank
arg_rank, Bool -> Rank -> Rank
LimitedRank (Rank -> Bool
forAllAllowed Rank
arg_rank) Rank
arg_rank)
funArgResRank Rank
other_rank = (Rank
other_rank, Rank
other_rank)
forAllAllowed :: Rank -> Bool
forAllAllowed :: Rank -> Bool
forAllAllowed Rank
ArbitraryRank = Bool
True
forAllAllowed (LimitedRank Bool
forall_ok Rank
_) = Bool
forall_ok
forAllAllowed Rank
_ = Bool
False
data TypeOrKindCtxt
= OnlyTypeCtxt
| OnlyKindCtxt
| BothTypeAndKindCtxt
deriving TypeOrKindCtxt -> TypeOrKindCtxt -> Bool
(TypeOrKindCtxt -> TypeOrKindCtxt -> Bool)
-> (TypeOrKindCtxt -> TypeOrKindCtxt -> Bool) -> Eq TypeOrKindCtxt
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TypeOrKindCtxt -> TypeOrKindCtxt -> Bool
$c/= :: TypeOrKindCtxt -> TypeOrKindCtxt -> Bool
== :: TypeOrKindCtxt -> TypeOrKindCtxt -> Bool
$c== :: TypeOrKindCtxt -> TypeOrKindCtxt -> Bool
Eq
instance Outputable TypeOrKindCtxt where
ppr :: TypeOrKindCtxt -> SDoc
ppr TypeOrKindCtxt
ctxt = String -> SDoc
text (String -> SDoc) -> String -> SDoc
forall a b. (a -> b) -> a -> b
$ case TypeOrKindCtxt
ctxt of
TypeOrKindCtxt
OnlyTypeCtxt -> String
"OnlyTypeCtxt"
TypeOrKindCtxt
OnlyKindCtxt -> String
"OnlyKindCtxt"
TypeOrKindCtxt
BothTypeAndKindCtxt -> String
"BothTypeAndKindCtxt"
typeOrKindCtxt :: UserTypeCtxt -> TypeOrKindCtxt
typeOrKindCtxt :: UserTypeCtxt -> TypeOrKindCtxt
typeOrKindCtxt (FunSigCtxt {}) = TypeOrKindCtxt
OnlyTypeCtxt
typeOrKindCtxt (InfSigCtxt {}) = TypeOrKindCtxt
OnlyTypeCtxt
typeOrKindCtxt (ExprSigCtxt {}) = TypeOrKindCtxt
OnlyTypeCtxt
typeOrKindCtxt (TypeAppCtxt {}) = TypeOrKindCtxt
OnlyTypeCtxt
typeOrKindCtxt (PatSynCtxt {}) = TypeOrKindCtxt
OnlyTypeCtxt
typeOrKindCtxt (PatSigCtxt {}) = TypeOrKindCtxt
OnlyTypeCtxt
typeOrKindCtxt (RuleSigCtxt {}) = TypeOrKindCtxt
OnlyTypeCtxt
typeOrKindCtxt (ForSigCtxt {}) = TypeOrKindCtxt
OnlyTypeCtxt
typeOrKindCtxt (DefaultDeclCtxt {}) = TypeOrKindCtxt
OnlyTypeCtxt
typeOrKindCtxt (InstDeclCtxt {}) = TypeOrKindCtxt
OnlyTypeCtxt
typeOrKindCtxt (SpecInstCtxt {}) = TypeOrKindCtxt
OnlyTypeCtxt
typeOrKindCtxt (GenSigCtxt {}) = TypeOrKindCtxt
OnlyTypeCtxt
typeOrKindCtxt (ClassSCCtxt {}) = TypeOrKindCtxt
OnlyTypeCtxt
typeOrKindCtxt (SigmaCtxt {}) = TypeOrKindCtxt
OnlyTypeCtxt
typeOrKindCtxt (DataTyCtxt {}) = TypeOrKindCtxt
OnlyTypeCtxt
typeOrKindCtxt (DerivClauseCtxt {}) = TypeOrKindCtxt
OnlyTypeCtxt
typeOrKindCtxt (ConArgCtxt {}) = TypeOrKindCtxt
OnlyTypeCtxt
typeOrKindCtxt (KindSigCtxt {}) = TypeOrKindCtxt
OnlyKindCtxt
typeOrKindCtxt (StandaloneKindSigCtxt {}) = TypeOrKindCtxt
OnlyKindCtxt
typeOrKindCtxt (TyVarBndrKindCtxt {}) = TypeOrKindCtxt
OnlyKindCtxt
typeOrKindCtxt (DataKindCtxt {}) = TypeOrKindCtxt
OnlyKindCtxt
typeOrKindCtxt (TySynKindCtxt {}) = TypeOrKindCtxt
OnlyKindCtxt
typeOrKindCtxt (TyFamResKindCtxt {}) = TypeOrKindCtxt
OnlyKindCtxt
typeOrKindCtxt (TySynCtxt {}) = TypeOrKindCtxt
BothTypeAndKindCtxt
typeOrKindCtxt (GhciCtxt {}) = TypeOrKindCtxt
BothTypeAndKindCtxt
typeLevelUserTypeCtxt :: UserTypeCtxt -> Bool
typeLevelUserTypeCtxt :: UserTypeCtxt -> Bool
typeLevelUserTypeCtxt UserTypeCtxt
ctxt = case UserTypeCtxt -> TypeOrKindCtxt
typeOrKindCtxt UserTypeCtxt
ctxt of
TypeOrKindCtxt
OnlyTypeCtxt -> Bool
True
TypeOrKindCtxt
OnlyKindCtxt -> Bool
False
TypeOrKindCtxt
BothTypeAndKindCtxt -> Bool
True
allConstraintsAllowed :: UserTypeCtxt -> Bool
allConstraintsAllowed :: UserTypeCtxt -> Bool
allConstraintsAllowed = UserTypeCtxt -> Bool
typeLevelUserTypeCtxt
linearityAllowed :: UserTypeCtxt -> Bool
linearityAllowed :: UserTypeCtxt -> Bool
linearityAllowed = UserTypeCtxt -> Bool
typeLevelUserTypeCtxt
vdqAllowed :: UserTypeCtxt -> Bool
vdqAllowed :: UserTypeCtxt -> Bool
vdqAllowed UserTypeCtxt
ctxt = case UserTypeCtxt -> TypeOrKindCtxt
typeOrKindCtxt UserTypeCtxt
ctxt of
TypeOrKindCtxt
OnlyTypeCtxt -> Bool
False
TypeOrKindCtxt
OnlyKindCtxt -> Bool
True
TypeOrKindCtxt
BothTypeAndKindCtxt -> Bool
True
data ExpandMode
= Expand
| NoExpand
| Both
instance Outputable ExpandMode where
ppr :: ExpandMode -> SDoc
ppr ExpandMode
e = String -> SDoc
text (String -> SDoc) -> String -> SDoc
forall a b. (a -> b) -> a -> b
$ case ExpandMode
e of
ExpandMode
Expand -> String
"Expand"
ExpandMode
NoExpand -> String
"NoExpand"
ExpandMode
Both -> String
"Both"
initialExpandMode :: TcM ExpandMode
initialExpandMode :: TcM ExpandMode
initialExpandMode = do
Bool
liberal_flag <- Extension -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. Extension -> TcRnIf gbl lcl Bool
xoptM Extension
LangExt.LiberalTypeSynonyms
ExpandMode -> TcM ExpandMode
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ExpandMode -> TcM ExpandMode) -> ExpandMode -> TcM ExpandMode
forall a b. (a -> b) -> a -> b
$ if Bool
liberal_flag then ExpandMode
Expand else ExpandMode
Both
data ValidityEnv = ValidityEnv
{ ValidityEnv -> TidyEnv
ve_tidy_env :: TidyEnv
, ValidityEnv -> UserTypeCtxt
ve_ctxt :: UserTypeCtxt
, ValidityEnv -> Rank
ve_rank :: Rank
, ValidityEnv -> ExpandMode
ve_expand :: ExpandMode }
instance Outputable ValidityEnv where
ppr :: ValidityEnv -> SDoc
ppr (ValidityEnv{ ve_tidy_env :: ValidityEnv -> TidyEnv
ve_tidy_env = TidyEnv
env, ve_ctxt :: ValidityEnv -> UserTypeCtxt
ve_ctxt = UserTypeCtxt
ctxt
, ve_rank :: ValidityEnv -> Rank
ve_rank = Rank
rank, ve_expand :: ValidityEnv -> ExpandMode
ve_expand = ExpandMode
expand }) =
SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"ValidityEnv")
Int
2 ([SDoc] -> SDoc
vcat [ String -> SDoc
text String
"ve_tidy_env" SDoc -> SDoc -> SDoc
<+> TidyEnv -> SDoc
forall a. Outputable a => a -> SDoc
ppr TidyEnv
env
, String -> SDoc
text String
"ve_ctxt" SDoc -> SDoc -> SDoc
<+> UserTypeCtxt -> SDoc
pprUserTypeCtxt UserTypeCtxt
ctxt
, String -> SDoc
text String
"ve_rank" SDoc -> SDoc -> SDoc
<+> Rank -> SDoc
forall a. Outputable a => a -> SDoc
ppr Rank
rank
, String -> SDoc
text String
"ve_expand" SDoc -> SDoc -> SDoc
<+> ExpandMode -> SDoc
forall a. Outputable a => a -> SDoc
ppr ExpandMode
expand ])
check_type :: ValidityEnv -> Type -> TcM ()
check_type :: ValidityEnv -> Type -> TcM ()
check_type ValidityEnv
_ (TyVarTy TyCoVar
_) = () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
check_type ValidityEnv
ve (AppTy Type
ty1 Type
ty2)
= do { ValidityEnv -> Type -> TcM ()
check_type ValidityEnv
ve Type
ty1
; Bool -> ValidityEnv -> Type -> TcM ()
check_arg_type Bool
False ValidityEnv
ve Type
ty2 }
check_type ValidityEnv
ve ty :: Type
ty@(TyConApp TyCon
tc [Type]
tys)
| TyCon -> Bool
isTypeSynonymTyCon TyCon
tc Bool -> Bool -> Bool
|| TyCon -> Bool
isTypeFamilyTyCon TyCon
tc
= ValidityEnv -> Type -> TyCon -> [Type] -> TcM ()
check_syn_tc_app ValidityEnv
ve Type
ty TyCon
tc [Type]
tys
| TyCon -> Bool
isUnboxedTupleTyCon TyCon
tc = ValidityEnv -> Type -> [Type] -> TcM ()
check_ubx_tuple ValidityEnv
ve Type
ty [Type]
tys
| Bool
otherwise = (Type -> TcM ()) -> [Type] -> TcM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Bool -> ValidityEnv -> Type -> TcM ()
check_arg_type Bool
False ValidityEnv
ve) [Type]
tys
check_type ValidityEnv
_ (LitTy {}) = () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
check_type ValidityEnv
ve (CastTy Type
ty KindCoercion
_) = ValidityEnv -> Type -> TcM ()
check_type ValidityEnv
ve Type
ty
check_type ve :: ValidityEnv
ve@(ValidityEnv{ ve_tidy_env :: ValidityEnv -> TidyEnv
ve_tidy_env = TidyEnv
env, ve_ctxt :: ValidityEnv -> UserTypeCtxt
ve_ctxt = UserTypeCtxt
ctxt
, ve_rank :: ValidityEnv -> Rank
ve_rank = Rank
rank, ve_expand :: ValidityEnv -> ExpandMode
ve_expand = ExpandMode
expand }) Type
ty
| Bool -> Bool
not ([TyVarBinder] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TyVarBinder]
tvbs Bool -> Bool -> Bool
&& [Type] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
theta)
= do { String -> SDoc -> TcM ()
traceTc String
"check_type" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty SDoc -> SDoc -> SDoc
$$ Rank -> SDoc
forall a. Outputable a => a -> SDoc
ppr Rank
rank)
; Bool -> (TidyEnv, SDoc) -> TcM ()
checkTcM (Rank -> Bool
forAllAllowed Rank
rank) (TidyEnv -> Rank -> Type -> (TidyEnv, SDoc)
forAllTyErr TidyEnv
env Rank
rank Type
ty)
; ValidityEnv -> [Type] -> Type -> TcM ()
checkConstraintsOK ValidityEnv
ve [Type]
theta Type
ty
; Bool -> (TidyEnv, SDoc) -> TcM ()
checkTcM ((TyVarBinder -> Bool) -> [TyVarBinder] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (ArgFlag -> Bool
isInvisibleArgFlag (ArgFlag -> Bool)
-> (TyVarBinder -> ArgFlag) -> TyVarBinder -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarBinder -> ArgFlag
forall tv argf. VarBndr tv argf -> argf
binderArgFlag) [TyVarBinder]
tvbs
Bool -> Bool -> Bool
|| UserTypeCtxt -> Bool
vdqAllowed UserTypeCtxt
ctxt)
(TidyEnv -> Type -> (TidyEnv, SDoc)
illegalVDQTyErr TidyEnv
env Type
ty)
; TidyEnv -> UserTypeCtxt -> ExpandMode -> [Type] -> TcM ()
check_valid_theta TidyEnv
env' UserTypeCtxt
SigmaCtxt ExpandMode
expand [Type]
theta
; ValidityEnv -> Type -> TcM ()
check_type (ValidityEnv
ve{ve_tidy_env :: TidyEnv
ve_tidy_env = TidyEnv
env'}) Type
tau
; TidyEnv -> [TyVarBinder] -> [Type] -> Type -> TcM ()
checkEscapingKind TidyEnv
env' [TyVarBinder]
tvbs' [Type]
theta Type
tau }
where
([TyVarBinder]
tvbs, Type
phi) = Type -> ([TyVarBinder], Type)
tcSplitForAllTyVarBinders Type
ty
([Type]
theta, Type
tau) = Type -> ([Type], Type)
tcSplitPhiTy Type
phi
(TidyEnv
env', [TyVarBinder]
tvbs') = TidyEnv -> [TyVarBinder] -> (TidyEnv, [TyVarBinder])
forall vis.
TidyEnv
-> [VarBndr TyCoVar vis] -> (TidyEnv, [VarBndr TyCoVar vis])
tidyTyCoVarBinders TidyEnv
env [TyVarBinder]
tvbs
check_type (ve :: ValidityEnv
ve@ValidityEnv{ ve_tidy_env :: ValidityEnv -> TidyEnv
ve_tidy_env = TidyEnv
env, ve_ctxt :: ValidityEnv -> UserTypeCtxt
ve_ctxt = UserTypeCtxt
ctxt
, ve_rank :: ValidityEnv -> Rank
ve_rank = Rank
rank })
ty :: Type
ty@(FunTy AnonArgFlag
_ Type
mult Type
arg_ty Type
res_ty)
= do { Bool -> (TidyEnv, SDoc) -> TcM ()
failIfTcM (Bool -> Bool
not (UserTypeCtxt -> Bool
linearityAllowed UserTypeCtxt
ctxt) Bool -> Bool -> Bool
&& Bool -> Bool
not (Type -> Bool
isManyDataConTy Type
mult))
(TidyEnv -> Type -> (TidyEnv, SDoc)
linearFunKindErr TidyEnv
env Type
ty)
; ValidityEnv -> Type -> TcM ()
check_type (ValidityEnv
ve{ve_rank :: Rank
ve_rank = Rank
arg_rank}) Type
arg_ty
; ValidityEnv -> Type -> TcM ()
check_type (ValidityEnv
ve{ve_rank :: Rank
ve_rank = Rank
res_rank}) Type
res_ty }
where
(Rank
arg_rank, Rank
res_rank) = Rank -> (Rank, Rank)
funArgResRank Rank
rank
check_type ValidityEnv
_ Type
ty = String -> SDoc -> TcM ()
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"check_type" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty)
check_syn_tc_app :: ValidityEnv
-> KindOrType -> TyCon -> [KindOrType] -> TcM ()
check_syn_tc_app :: ValidityEnv -> Type -> TyCon -> [Type] -> TcM ()
check_syn_tc_app (ve :: ValidityEnv
ve@ValidityEnv{ ve_ctxt :: ValidityEnv -> UserTypeCtxt
ve_ctxt = UserTypeCtxt
ctxt, ve_expand :: ValidityEnv -> ExpandMode
ve_expand = ExpandMode
expand })
Type
ty TyCon
tc [Type]
tys
| [Type]
tys [Type] -> Int -> Bool
forall a. [a] -> Int -> Bool
`lengthAtLeast` Int
tc_arity
= case ExpandMode
expand of
ExpandMode
_ | TyCon -> Bool
isTypeFamilyTyCon TyCon
tc
-> ExpandMode -> TcM ()
check_args_only ExpandMode
expand
ExpandMode
Expand -> ExpandMode -> TcM ()
check_expansion_only ExpandMode
expand
ExpandMode
NoExpand -> ExpandMode -> TcM ()
check_args_only ExpandMode
expand
ExpandMode
Both -> ExpandMode -> TcM ()
check_args_only ExpandMode
NoExpand TcM () -> TcM () -> TcM ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ExpandMode -> TcM ()
check_expansion_only ExpandMode
Both
| GhciCtxt Bool
True <- UserTypeCtxt
ctxt
= ExpandMode -> TcM ()
check_args_only ExpandMode
expand
| Bool
otherwise
= SDoc -> TcM ()
forall a. SDoc -> TcM a
failWithTc (TyCon -> [Type] -> SDoc
tyConArityErr TyCon
tc [Type]
tys)
where
tc_arity :: Int
tc_arity = TyCon -> Int
tyConArity TyCon
tc
check_arg :: ExpandMode -> KindOrType -> TcM ()
check_arg :: ExpandMode -> Type -> TcM ()
check_arg ExpandMode
expand =
Bool -> ValidityEnv -> Type -> TcM ()
check_arg_type (TyCon -> Bool
isTypeSynonymTyCon TyCon
tc) (ValidityEnv
ve{ve_expand :: ExpandMode
ve_expand = ExpandMode
expand})
check_args_only, check_expansion_only :: ExpandMode -> TcM ()
check_args_only :: ExpandMode -> TcM ()
check_args_only ExpandMode
expand = (Type -> TcM ()) -> [Type] -> TcM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (ExpandMode -> Type -> TcM ()
check_arg ExpandMode
expand) [Type]
tys
check_expansion_only :: ExpandMode -> TcM ()
check_expansion_only ExpandMode
expand
= ASSERT2( isTypeSynonymTyCon tc, ppr tc )
case Type -> Maybe Type
tcView Type
ty of
Just Type
ty' -> let err_ctxt :: SDoc
err_ctxt = String -> SDoc
text String
"In the expansion of type synonym"
SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tc)
in SDoc -> TcM () -> TcM ()
forall a. SDoc -> TcM a -> TcM a
addErrCtxt SDoc
err_ctxt (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$
ValidityEnv -> Type -> TcM ()
check_type (ValidityEnv
ve{ve_expand :: ExpandMode
ve_expand = ExpandMode
expand}) Type
ty'
Maybe Type
Nothing -> String -> SDoc -> TcM ()
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"check_syn_tc_app" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty)
check_ubx_tuple :: ValidityEnv -> KindOrType -> [KindOrType] -> TcM ()
check_ubx_tuple :: ValidityEnv -> Type -> [Type] -> TcM ()
check_ubx_tuple (ve :: ValidityEnv
ve@ValidityEnv{ve_tidy_env :: ValidityEnv -> TidyEnv
ve_tidy_env = TidyEnv
env}) Type
ty [Type]
tys
= do { Bool
ub_tuples_allowed <- Extension -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. Extension -> TcRnIf gbl lcl Bool
xoptM Extension
LangExt.UnboxedTuples
; Bool -> (TidyEnv, SDoc) -> TcM ()
checkTcM Bool
ub_tuples_allowed (TidyEnv -> Type -> (TidyEnv, SDoc)
ubxArgTyErr TidyEnv
env Type
ty)
; Bool
impred <- Extension -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. Extension -> TcRnIf gbl lcl Bool
xoptM Extension
LangExt.ImpredicativeTypes
; let rank' :: Rank
rank' = if Bool
impred then Rank
ArbitraryRank else Rank
tyConArgMonoType
; (Type -> TcM ()) -> [Type] -> TcM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (ValidityEnv -> Type -> TcM ()
check_type (ValidityEnv
ve{ve_rank :: Rank
ve_rank = Rank
rank'})) [Type]
tys }
check_arg_type
:: Bool
-> ValidityEnv -> KindOrType -> TcM ()
check_arg_type :: Bool -> ValidityEnv -> Type -> TcM ()
check_arg_type Bool
_ ValidityEnv
_ (CoercionTy {}) = () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
check_arg_type Bool
type_syn (ve :: ValidityEnv
ve@ValidityEnv{ve_ctxt :: ValidityEnv -> UserTypeCtxt
ve_ctxt = UserTypeCtxt
ctxt, ve_rank :: ValidityEnv -> Rank
ve_rank = Rank
rank}) Type
ty
= do { Bool
impred <- Extension -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. Extension -> TcRnIf gbl lcl Bool
xoptM Extension
LangExt.ImpredicativeTypes
; let rank' :: Rank
rank' = case Rank
rank of
Rank
_ | Bool
type_syn -> Rank
synArgMonoType
Rank
MustBeMonoType -> Rank
MustBeMonoType
Rank
_other | Bool
impred -> Rank
ArbitraryRank
| Bool
otherwise -> Rank
tyConArgMonoType
ctxt' :: UserTypeCtxt
ctxt' :: UserTypeCtxt
ctxt'
| GhciCtxt Bool
_ <- UserTypeCtxt
ctxt = Bool -> UserTypeCtxt
GhciCtxt Bool
False
| Bool
otherwise = UserTypeCtxt
ctxt
; ValidityEnv -> Type -> TcM ()
check_type (ValidityEnv
ve{ve_ctxt :: UserTypeCtxt
ve_ctxt = UserTypeCtxt
ctxt', ve_rank :: Rank
ve_rank = Rank
rank'}) Type
ty }
forAllTyErr :: TidyEnv -> Rank -> Type -> (TidyEnv, SDoc)
forAllTyErr :: TidyEnv -> Rank -> Type -> (TidyEnv, SDoc)
forAllTyErr TidyEnv
env Rank
rank Type
ty
= ( TidyEnv
env
, [SDoc] -> SDoc
vcat [ SDoc -> Int -> SDoc -> SDoc
hang SDoc
herald Int
2 (TidyEnv -> Type -> SDoc
ppr_tidy TidyEnv
env Type
ty)
, SDoc
suggestion ] )
where
([TyCoVar]
tvs, Type
_rho) = Type -> ([TyCoVar], Type)
tcSplitForAllTyVars Type
ty
herald :: SDoc
herald | [TyCoVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TyCoVar]
tvs = String -> SDoc
text String
"Illegal qualified type:"
| Bool
otherwise = String -> SDoc
text String
"Illegal polymorphic type:"
suggestion :: SDoc
suggestion = case Rank
rank of
LimitedRank {} -> String -> SDoc
text String
"Perhaps you intended to use RankNTypes"
MonoType SDoc
d -> SDoc
d
Rank
_ -> SDoc
Outputable.empty
checkEscapingKind :: TidyEnv -> [TyVarBinder] -> ThetaType -> Type -> TcM ()
checkEscapingKind :: TidyEnv -> [TyVarBinder] -> [Type] -> Type -> TcM ()
checkEscapingKind TidyEnv
env [TyVarBinder]
tvbs [Type]
theta Type
tau =
case [TyCoVar] -> Type -> Maybe Type
occCheckExpand ([TyVarBinder] -> [TyCoVar]
forall tv argf. [VarBndr tv argf] -> [tv]
binderVars [TyVarBinder]
tvbs) Type
phi_kind of
Maybe Type
Nothing -> (TidyEnv, SDoc) -> TcM ()
forall a. (TidyEnv, SDoc) -> TcM a
failWithTcM ((TidyEnv, SDoc) -> TcM ()) -> (TidyEnv, SDoc) -> TcM ()
forall a b. (a -> b) -> a -> b
$ TidyEnv
-> [TyVarBinder] -> [Type] -> Type -> Type -> (TidyEnv, SDoc)
forAllEscapeErr TidyEnv
env [TyVarBinder]
tvbs [Type]
theta Type
tau Type
tau_kind
Just Type
_ -> () -> TcM ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
where
tau_kind :: Type
tau_kind = HasDebugCallStack => Type -> Type
Type -> Type
tcTypeKind Type
tau
phi_kind :: Type
phi_kind | [Type] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
theta = Type
tau_kind
| Bool
otherwise = Type
liftedTypeKind
forAllEscapeErr :: TidyEnv -> [TyVarBinder] -> ThetaType -> Type -> Kind
-> (TidyEnv, SDoc)
forAllEscapeErr :: TidyEnv
-> [TyVarBinder] -> [Type] -> Type -> Type -> (TidyEnv, SDoc)
forAllEscapeErr TidyEnv
env [TyVarBinder]
tvbs [Type]
theta Type
tau Type
tau_kind
= ( TidyEnv
env
, [SDoc] -> SDoc
vcat [ SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Quantified type's kind mentions quantified type variable")
Int
2 (String -> SDoc
text String
"type:" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr ([TyVarBinder] -> [Type] -> Type -> Type
mkSigmaTy [TyVarBinder]
tvbs [Type]
theta Type
tau)))
, SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"where the body of the forall has this kind:")
Int
2 (SDoc -> SDoc
quotes (TidyEnv -> Type -> SDoc
ppr_tidy TidyEnv
env Type
tau_kind)) ] )
ubxArgTyErr :: TidyEnv -> Type -> (TidyEnv, SDoc)
ubxArgTyErr :: TidyEnv -> Type -> (TidyEnv, SDoc)
ubxArgTyErr TidyEnv
env Type
ty
= ( TidyEnv
env, [SDoc] -> SDoc
vcat [ [SDoc] -> SDoc
sep [ String -> SDoc
text String
"Illegal unboxed tuple type as function argument:"
, TidyEnv -> Type -> SDoc
ppr_tidy TidyEnv
env Type
ty ]
, String -> SDoc
text String
"Perhaps you intended to use UnboxedTuples" ] )
checkConstraintsOK :: ValidityEnv -> ThetaType -> Type -> TcM ()
checkConstraintsOK :: ValidityEnv -> [Type] -> Type -> TcM ()
checkConstraintsOK ValidityEnv
ve [Type]
theta Type
ty
| [Type] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
theta = () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
| UserTypeCtxt -> Bool
allConstraintsAllowed (ValidityEnv -> UserTypeCtxt
ve_ctxt ValidityEnv
ve) = () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
| Bool
otherwise
=
Bool -> (TidyEnv, SDoc) -> TcM ()
checkTcM ((Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Type -> Bool
isEqPred [Type]
theta) ((TidyEnv, SDoc) -> TcM ()) -> (TidyEnv, SDoc) -> TcM ()
forall a b. (a -> b) -> a -> b
$
TidyEnv -> Type -> (TidyEnv, SDoc)
constraintTyErr (ValidityEnv -> TidyEnv
ve_tidy_env ValidityEnv
ve) Type
ty
constraintTyErr :: TidyEnv -> Type -> (TidyEnv, SDoc)
constraintTyErr :: TidyEnv -> Type -> (TidyEnv, SDoc)
constraintTyErr TidyEnv
env Type
ty
= (TidyEnv
env, String -> SDoc
text String
"Illegal constraint in a kind:" SDoc -> SDoc -> SDoc
<+> TidyEnv -> Type -> SDoc
ppr_tidy TidyEnv
env Type
ty)
illegalVDQTyErr :: TidyEnv -> Type -> (TidyEnv, SDoc)
illegalVDQTyErr :: TidyEnv -> Type -> (TidyEnv, SDoc)
illegalVDQTyErr TidyEnv
env Type
ty =
(TidyEnv
env, [SDoc] -> SDoc
vcat
[ SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Illegal visible, dependent quantification" SDoc -> SDoc -> SDoc
<+>
String -> SDoc
text String
"in the type of a term:")
Int
2 (TidyEnv -> Type -> SDoc
ppr_tidy TidyEnv
env Type
ty)
, String -> SDoc
text String
"(GHC does not yet support this)" ] )
linearFunKindErr :: TidyEnv -> Type -> (TidyEnv, SDoc)
linearFunKindErr :: TidyEnv -> Type -> (TidyEnv, SDoc)
linearFunKindErr TidyEnv
env Type
ty =
(TidyEnv
env, String -> SDoc
text String
"Illegal linear function in a kind:" SDoc -> SDoc -> SDoc
<+> TidyEnv -> Type -> SDoc
ppr_tidy TidyEnv
env Type
ty)
checkValidTheta :: UserTypeCtxt -> ThetaType -> TcM ()
checkValidTheta :: UserTypeCtxt -> [Type] -> TcM ()
checkValidTheta UserTypeCtxt
ctxt [Type]
theta
= (TidyEnv -> TcM (TidyEnv, SDoc)) -> TcM () -> TcM ()
forall a. (TidyEnv -> TcM (TidyEnv, SDoc)) -> TcM a -> TcM a
addErrCtxtM (UserTypeCtxt -> [Type] -> TidyEnv -> TcM (TidyEnv, SDoc)
checkThetaCtxt UserTypeCtxt
ctxt [Type]
theta) (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$
do { TidyEnv
env <- [TyCoVar] -> TcM TidyEnv
tcInitOpenTidyEnv ([Type] -> [TyCoVar]
tyCoVarsOfTypesList [Type]
theta)
; ExpandMode
expand <- TcM ExpandMode
initialExpandMode
; TidyEnv -> UserTypeCtxt -> ExpandMode -> [Type] -> TcM ()
check_valid_theta TidyEnv
env UserTypeCtxt
ctxt ExpandMode
expand [Type]
theta }
check_valid_theta :: TidyEnv -> UserTypeCtxt -> ExpandMode
-> [PredType] -> TcM ()
check_valid_theta :: TidyEnv -> UserTypeCtxt -> ExpandMode -> [Type] -> TcM ()
check_valid_theta TidyEnv
_ UserTypeCtxt
_ ExpandMode
_ []
= () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
check_valid_theta TidyEnv
env UserTypeCtxt
ctxt ExpandMode
expand [Type]
theta
= do { DynFlags
dflags <- IOEnv (Env TcGblEnv TcLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
; WarnReason -> Bool -> (TidyEnv, SDoc) -> TcM ()
warnTcM (WarningFlag -> WarnReason
Reason WarningFlag
Opt_WarnDuplicateConstraints)
(WarningFlag -> DynFlags -> Bool
wopt WarningFlag
Opt_WarnDuplicateConstraints DynFlags
dflags Bool -> Bool -> Bool
&& [NonEmpty Type] -> Bool
forall (f :: * -> *) a. Foldable f => f a -> Bool
notNull [NonEmpty Type]
dups)
(TidyEnv -> [NonEmpty Type] -> (TidyEnv, SDoc)
dupPredWarn TidyEnv
env [NonEmpty Type]
dups)
; String -> SDoc -> TcM ()
traceTc String
"check_valid_theta" ([Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
theta)
; (Type -> TcM ()) -> [Type] -> TcM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (TidyEnv -> DynFlags -> UserTypeCtxt -> ExpandMode -> Type -> TcM ()
check_pred_ty TidyEnv
env DynFlags
dflags UserTypeCtxt
ctxt ExpandMode
expand) [Type]
theta }
where
([Type]
_,[NonEmpty Type]
dups) = (Type -> Type -> Ordering) -> [Type] -> ([Type], [NonEmpty Type])
forall a. (a -> a -> Ordering) -> [a] -> ([a], [NonEmpty a])
removeDups Type -> Type -> Ordering
nonDetCmpType [Type]
theta
check_pred_ty :: TidyEnv -> DynFlags -> UserTypeCtxt -> ExpandMode
-> PredType -> TcM ()
check_pred_ty :: TidyEnv -> DynFlags -> UserTypeCtxt -> ExpandMode -> Type -> TcM ()
check_pred_ty TidyEnv
env DynFlags
dflags UserTypeCtxt
ctxt ExpandMode
expand Type
pred
= do { ValidityEnv -> Type -> TcM ()
check_type ValidityEnv
ve Type
pred
; Bool -> TidyEnv -> DynFlags -> UserTypeCtxt -> Type -> TcM ()
check_pred_help Bool
False TidyEnv
env DynFlags
dflags UserTypeCtxt
ctxt Type
pred }
where
rank :: Rank
rank | Extension -> DynFlags -> Bool
xopt Extension
LangExt.QuantifiedConstraints DynFlags
dflags
= Rank
ArbitraryRank
| Bool
otherwise
= Rank
constraintMonoType
ve :: ValidityEnv
ve :: ValidityEnv
ve = ValidityEnv{ ve_tidy_env :: TidyEnv
ve_tidy_env = TidyEnv
env
, ve_ctxt :: UserTypeCtxt
ve_ctxt = UserTypeCtxt
SigmaCtxt
, ve_rank :: Rank
ve_rank = Rank
rank
, ve_expand :: ExpandMode
ve_expand = ExpandMode
expand }
check_pred_help :: Bool
-> TidyEnv
-> DynFlags -> UserTypeCtxt
-> PredType -> TcM ()
check_pred_help :: Bool -> TidyEnv -> DynFlags -> UserTypeCtxt -> Type -> TcM ()
check_pred_help Bool
under_syn TidyEnv
env DynFlags
dflags UserTypeCtxt
ctxt Type
pred
| Just Type
pred' <- Type -> Maybe Type
tcView Type
pred
= Bool -> TidyEnv -> DynFlags -> UserTypeCtxt -> Type -> TcM ()
check_pred_help Bool
True TidyEnv
env DynFlags
dflags UserTypeCtxt
ctxt Type
pred'
| Bool
otherwise
= case Type -> Pred
classifyPredType Type
pred of
ClassPred Class
cls [Type]
tys
| Class -> Bool
isCTupleClass Class
cls -> Bool
-> TidyEnv -> DynFlags -> UserTypeCtxt -> Type -> [Type] -> TcM ()
check_tuple_pred Bool
under_syn TidyEnv
env DynFlags
dflags UserTypeCtxt
ctxt Type
pred [Type]
tys
| Bool
otherwise -> TidyEnv
-> DynFlags -> UserTypeCtxt -> Type -> Class -> [Type] -> TcM ()
check_class_pred TidyEnv
env DynFlags
dflags UserTypeCtxt
ctxt Type
pred Class
cls [Type]
tys
EqPred EqRel
_ Type
_ Type
_ -> String -> SDoc -> TcM ()
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"check_pred_help" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
pred)
ForAllPred [TyCoVar]
_ [Type]
theta Type
head -> TidyEnv
-> DynFlags -> UserTypeCtxt -> Type -> [Type] -> Type -> TcM ()
check_quant_pred TidyEnv
env DynFlags
dflags UserTypeCtxt
ctxt Type
pred [Type]
theta Type
head
IrredPred {} -> Bool -> TidyEnv -> DynFlags -> Type -> TcM ()
check_irred_pred Bool
under_syn TidyEnv
env DynFlags
dflags Type
pred
check_eq_pred :: TidyEnv -> DynFlags -> PredType -> TcM ()
check_eq_pred :: TidyEnv -> DynFlags -> Type -> TcM ()
check_eq_pred TidyEnv
env DynFlags
dflags Type
pred
=
Bool -> (TidyEnv, SDoc) -> TcM ()
checkTcM (Extension -> DynFlags -> Bool
xopt Extension
LangExt.TypeFamilies DynFlags
dflags
Bool -> Bool -> Bool
|| Extension -> DynFlags -> Bool
xopt Extension
LangExt.GADTs DynFlags
dflags)
(TidyEnv -> Type -> (TidyEnv, SDoc)
eqPredTyErr TidyEnv
env Type
pred)
check_quant_pred :: TidyEnv -> DynFlags -> UserTypeCtxt
-> PredType -> ThetaType -> PredType -> TcM ()
check_quant_pred :: TidyEnv
-> DynFlags -> UserTypeCtxt -> Type -> [Type] -> Type -> TcM ()
check_quant_pred TidyEnv
env DynFlags
dflags UserTypeCtxt
ctxt Type
pred [Type]
theta Type
head_pred
= SDoc -> TcM () -> TcM ()
forall a. SDoc -> TcM a -> TcM a
addErrCtxt (String -> SDoc
text String
"In the quantified constraint" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
pred)) (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$
do {
case Type -> Pred
classifyPredType Type
head_pred of
ClassPred Class
cls [Type]
tys -> do { UserTypeCtxt -> Class -> [Type] -> TcM ()
checkValidInstHead UserTypeCtxt
SigmaCtxt Class
cls [Type]
tys
; Bool -> TidyEnv -> DynFlags -> UserTypeCtxt -> Type -> TcM ()
check_pred_help Bool
False TidyEnv
env DynFlags
dflags UserTypeCtxt
ctxt Type
head_pred }
IrredPred {} | Type -> Bool
hasTyVarHead Type
head_pred
-> () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Pred
_ -> (TidyEnv, SDoc) -> TcM ()
forall a. (TidyEnv, SDoc) -> TcM a
failWithTcM (TidyEnv -> Type -> (TidyEnv, SDoc)
badQuantHeadErr TidyEnv
env Type
pred)
; Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Extension -> DynFlags -> Bool
xopt Extension
LangExt.UndecidableInstances DynFlags
dflags) (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$
[Type] -> Type -> TcM ()
checkInstTermination [Type]
theta Type
head_pred
}
check_tuple_pred :: Bool -> TidyEnv -> DynFlags -> UserTypeCtxt -> PredType -> [PredType] -> TcM ()
check_tuple_pred :: Bool
-> TidyEnv -> DynFlags -> UserTypeCtxt -> Type -> [Type] -> TcM ()
check_tuple_pred Bool
under_syn TidyEnv
env DynFlags
dflags UserTypeCtxt
ctxt Type
pred [Type]
ts
= do {
Bool -> (TidyEnv, SDoc) -> TcM ()
checkTcM (Bool
under_syn Bool -> Bool -> Bool
|| Extension -> DynFlags -> Bool
xopt Extension
LangExt.ConstraintKinds DynFlags
dflags)
(TidyEnv -> Type -> (TidyEnv, SDoc)
predTupleErr TidyEnv
env Type
pred)
; (Type -> TcM ()) -> [Type] -> TcM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Bool -> TidyEnv -> DynFlags -> UserTypeCtxt -> Type -> TcM ()
check_pred_help Bool
under_syn TidyEnv
env DynFlags
dflags UserTypeCtxt
ctxt) [Type]
ts }
check_irred_pred :: Bool -> TidyEnv -> DynFlags -> PredType -> TcM ()
check_irred_pred :: Bool -> TidyEnv -> DynFlags -> Type -> TcM ()
check_irred_pred Bool
under_syn TidyEnv
env DynFlags
dflags Type
pred
=
Bool -> (TidyEnv, SDoc) -> TcM ()
failIfTcM (Bool -> Bool
not Bool
under_syn Bool -> Bool -> Bool
&& Bool -> Bool
not (Extension -> DynFlags -> Bool
xopt Extension
LangExt.ConstraintKinds DynFlags
dflags)
Bool -> Bool -> Bool
&& Type -> Bool
hasTyVarHead Type
pred)
(TidyEnv -> Type -> (TidyEnv, SDoc)
predIrredErr TidyEnv
env Type
pred)
check_class_pred :: TidyEnv -> DynFlags -> UserTypeCtxt
-> PredType -> Class -> [TcType] -> TcM ()
check_class_pred :: TidyEnv
-> DynFlags -> UserTypeCtxt -> Type -> Class -> [Type] -> TcM ()
check_class_pred TidyEnv
env DynFlags
dflags UserTypeCtxt
ctxt Type
pred Class
cls [Type]
tys
| Class -> Bool
isEqPredClass Class
cls
= TidyEnv -> DynFlags -> Type -> TcM ()
check_eq_pred TidyEnv
env DynFlags
dflags Type
pred
| Class -> Bool
isIPClass Class
cls
= do { TcM ()
check_arity
; Bool -> (TidyEnv, SDoc) -> TcM ()
checkTcM (UserTypeCtxt -> Bool
okIPCtxt UserTypeCtxt
ctxt) (TidyEnv -> Type -> (TidyEnv, SDoc)
badIPPred TidyEnv
env Type
pred) }
| Bool
otherwise
= do { TcM ()
check_arity
; TidyEnv -> DynFlags -> UserTypeCtxt -> Class -> [Type] -> TcM ()
checkSimplifiableClassConstraint TidyEnv
env DynFlags
dflags UserTypeCtxt
ctxt Class
cls [Type]
tys
; Bool -> (TidyEnv, SDoc) -> TcM ()
checkTcM Bool
arg_tys_ok (TidyEnv -> Type -> (TidyEnv, SDoc)
predTyVarErr TidyEnv
env Type
pred) }
where
check_arity :: TcM ()
check_arity = Bool -> SDoc -> TcM ()
checkTc ([Type]
tys [Type] -> Int -> Bool
forall a. [a] -> Int -> Bool
`lengthIs` Class -> Int
classArity Class
cls)
(TyCon -> [Type] -> SDoc
tyConArityErr (Class -> TyCon
classTyCon Class
cls) [Type]
tys)
flexible_contexts :: Bool
flexible_contexts = Extension -> DynFlags -> Bool
xopt Extension
LangExt.FlexibleContexts DynFlags
dflags
arg_tys_ok :: Bool
arg_tys_ok = case UserTypeCtxt
ctxt of
UserTypeCtxt
SpecInstCtxt -> Bool
True
InstDeclCtxt {} -> Bool -> Class -> [Type] -> Bool
checkValidClsArgs Bool
flexible_contexts Class
cls [Type]
tys
UserTypeCtxt
_ -> Bool -> Class -> [Type] -> Bool
checkValidClsArgs Bool
flexible_contexts Class
cls [Type]
tys
checkSimplifiableClassConstraint :: TidyEnv -> DynFlags -> UserTypeCtxt
-> Class -> [TcType] -> TcM ()
checkSimplifiableClassConstraint :: TidyEnv -> DynFlags -> UserTypeCtxt -> Class -> [Type] -> TcM ()
checkSimplifiableClassConstraint TidyEnv
env DynFlags
dflags UserTypeCtxt
ctxt Class
cls [Type]
tys
| Bool -> Bool
not (WarningFlag -> DynFlags -> Bool
wopt WarningFlag
Opt_WarnSimplifiableClassConstraints DynFlags
dflags)
= () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
| Extension -> DynFlags -> Bool
xopt Extension
LangExt.MonoLocalBinds DynFlags
dflags
= () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
| DataTyCtxt {} <- UserTypeCtxt
ctxt
= () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
| Class
cls Class -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
coercibleTyConKey
= () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
| Bool
otherwise
= do { ClsInstResult
result <- DynFlags -> Bool -> Class -> [Type] -> TcM ClsInstResult
matchGlobalInst DynFlags
dflags Bool
False Class
cls [Type]
tys
; case ClsInstResult
result of
OneInst { cir_what :: ClsInstResult -> InstanceWhat
cir_what = InstanceWhat
what }
-> WarnReason -> SDoc -> TcM ()
addWarnTc (WarningFlag -> WarnReason
Reason WarningFlag
Opt_WarnSimplifiableClassConstraints)
(InstanceWhat -> SDoc
simplifiable_constraint_warn InstanceWhat
what)
ClsInstResult
_ -> () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return () }
where
pred :: Type
pred = Class -> [Type] -> Type
mkClassPred Class
cls [Type]
tys
simplifiable_constraint_warn :: InstanceWhat -> SDoc
simplifiable_constraint_warn :: InstanceWhat -> SDoc
simplifiable_constraint_warn InstanceWhat
what
= [SDoc] -> SDoc
vcat [ SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"The constraint" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TidyEnv -> Type -> Type
tidyType TidyEnv
env Type
pred))
SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"matches")
Int
2 (InstanceWhat -> SDoc
forall a. Outputable a => a -> SDoc
ppr InstanceWhat
what)
, SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"This makes type inference for inner bindings fragile;")
Int
2 (String -> SDoc
text String
"either use MonoLocalBinds, or simplify it using the instance") ]
okIPCtxt :: UserTypeCtxt -> Bool
okIPCtxt :: UserTypeCtxt -> Bool
okIPCtxt (FunSigCtxt {}) = Bool
True
okIPCtxt (InfSigCtxt {}) = Bool
True
okIPCtxt UserTypeCtxt
ExprSigCtxt = Bool
True
okIPCtxt UserTypeCtxt
TypeAppCtxt = Bool
True
okIPCtxt UserTypeCtxt
PatSigCtxt = Bool
True
okIPCtxt UserTypeCtxt
GenSigCtxt = Bool
True
okIPCtxt (ConArgCtxt {}) = Bool
True
okIPCtxt (ForSigCtxt {}) = Bool
True
okIPCtxt (GhciCtxt {}) = Bool
True
okIPCtxt UserTypeCtxt
SigmaCtxt = Bool
True
okIPCtxt (DataTyCtxt {}) = Bool
True
okIPCtxt (PatSynCtxt {}) = Bool
True
okIPCtxt (TySynCtxt {}) = Bool
True
okIPCtxt (KindSigCtxt {}) = Bool
False
okIPCtxt (StandaloneKindSigCtxt {}) = Bool
False
okIPCtxt (ClassSCCtxt {}) = Bool
False
okIPCtxt (InstDeclCtxt {}) = Bool
False
okIPCtxt (SpecInstCtxt {}) = Bool
False
okIPCtxt (RuleSigCtxt {}) = Bool
False
okIPCtxt UserTypeCtxt
DefaultDeclCtxt = Bool
False
okIPCtxt UserTypeCtxt
DerivClauseCtxt = Bool
False
okIPCtxt (TyVarBndrKindCtxt {}) = Bool
False
okIPCtxt (DataKindCtxt {}) = Bool
False
okIPCtxt (TySynKindCtxt {}) = Bool
False
okIPCtxt (TyFamResKindCtxt {}) = Bool
False
checkThetaCtxt :: UserTypeCtxt -> ThetaType -> TidyEnv -> TcM (TidyEnv, SDoc)
checkThetaCtxt :: UserTypeCtxt -> [Type] -> TidyEnv -> TcM (TidyEnv, SDoc)
checkThetaCtxt UserTypeCtxt
ctxt [Type]
theta TidyEnv
env
= (TidyEnv, SDoc) -> TcM (TidyEnv, SDoc)
forall (m :: * -> *) a. Monad m => a -> m a
return ( TidyEnv
env
, [SDoc] -> SDoc
vcat [ String -> SDoc
text String
"In the context:" SDoc -> SDoc -> SDoc
<+> [Type] -> SDoc
pprTheta (TidyEnv -> [Type] -> [Type]
tidyTypes TidyEnv
env [Type]
theta)
, String -> SDoc
text String
"While checking" SDoc -> SDoc -> SDoc
<+> UserTypeCtxt -> SDoc
pprUserTypeCtxt UserTypeCtxt
ctxt ] )
eqPredTyErr, predTupleErr, predIrredErr,
badQuantHeadErr :: TidyEnv -> PredType -> (TidyEnv, SDoc)
TidyEnv
env Type
pred
= ( TidyEnv
env
, SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Quantified predicate must have a class or type variable head:")
Int
2 (TidyEnv -> Type -> SDoc
ppr_tidy TidyEnv
env Type
pred) )
eqPredTyErr :: TidyEnv -> Type -> (TidyEnv, SDoc)
eqPredTyErr TidyEnv
env Type
pred
= ( TidyEnv
env
, String -> SDoc
text String
"Illegal equational constraint" SDoc -> SDoc -> SDoc
<+> TidyEnv -> Type -> SDoc
ppr_tidy TidyEnv
env Type
pred SDoc -> SDoc -> SDoc
$$
SDoc -> SDoc
parens (String -> SDoc
text String
"Use GADTs or TypeFamilies to permit this") )
predTupleErr :: TidyEnv -> Type -> (TidyEnv, SDoc)
predTupleErr TidyEnv
env Type
pred
= ( TidyEnv
env
, SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Illegal tuple constraint:" SDoc -> SDoc -> SDoc
<+> TidyEnv -> Type -> SDoc
ppr_tidy TidyEnv
env Type
pred)
Int
2 (SDoc -> SDoc
parens SDoc
constraintKindsMsg) )
predIrredErr :: TidyEnv -> Type -> (TidyEnv, SDoc)
predIrredErr TidyEnv
env Type
pred
= ( TidyEnv
env
, SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Illegal constraint:" SDoc -> SDoc -> SDoc
<+> TidyEnv -> Type -> SDoc
ppr_tidy TidyEnv
env Type
pred)
Int
2 (SDoc -> SDoc
parens SDoc
constraintKindsMsg) )
predTyVarErr :: TidyEnv -> PredType -> (TidyEnv, SDoc)
predTyVarErr :: TidyEnv -> Type -> (TidyEnv, SDoc)
predTyVarErr TidyEnv
env Type
pred
= (TidyEnv
env
, [SDoc] -> SDoc
vcat [ SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Non type-variable argument")
Int
2 (String -> SDoc
text String
"in the constraint:" SDoc -> SDoc -> SDoc
<+> TidyEnv -> Type -> SDoc
ppr_tidy TidyEnv
env Type
pred)
, SDoc -> SDoc
parens (String -> SDoc
text String
"Use FlexibleContexts to permit this") ])
badIPPred :: TidyEnv -> PredType -> (TidyEnv, SDoc)
badIPPred :: TidyEnv -> Type -> (TidyEnv, SDoc)
badIPPred TidyEnv
env Type
pred
= ( TidyEnv
env
, String -> SDoc
text String
"Illegal implicit parameter" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (TidyEnv -> Type -> SDoc
ppr_tidy TidyEnv
env Type
pred) )
constraintSynErr :: TidyEnv -> Type -> (TidyEnv, SDoc)
constraintSynErr :: TidyEnv -> Type -> (TidyEnv, SDoc)
constraintSynErr TidyEnv
env Type
kind
= ( TidyEnv
env
, SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Illegal constraint synonym of kind:" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (TidyEnv -> Type -> SDoc
ppr_tidy TidyEnv
env Type
kind))
Int
2 (SDoc -> SDoc
parens SDoc
constraintKindsMsg) )
dupPredWarn :: TidyEnv -> [NE.NonEmpty PredType] -> (TidyEnv, SDoc)
dupPredWarn :: TidyEnv -> [NonEmpty Type] -> (TidyEnv, SDoc)
dupPredWarn TidyEnv
env [NonEmpty Type]
dups
= ( TidyEnv
env
, String -> SDoc
text String
"Duplicate constraint" SDoc -> SDoc -> SDoc
<> [Type] -> SDoc
forall a. [a] -> SDoc
plural [Type]
primaryDups SDoc -> SDoc -> SDoc
<> String -> SDoc
text String
":"
SDoc -> SDoc -> SDoc
<+> (Type -> SDoc) -> [Type] -> SDoc
forall a. (a -> SDoc) -> [a] -> SDoc
pprWithCommas (TidyEnv -> Type -> SDoc
ppr_tidy TidyEnv
env) [Type]
primaryDups )
where
primaryDups :: [Type]
primaryDups = (NonEmpty Type -> Type) -> [NonEmpty Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map NonEmpty Type -> Type
forall a. NonEmpty a -> a
NE.head [NonEmpty Type]
dups
tyConArityErr :: TyCon -> [TcType] -> SDoc
tyConArityErr :: TyCon -> [Type] -> SDoc
tyConArityErr TyCon
tc [Type]
tks
= SDoc -> Name -> Int -> Int -> SDoc
forall a. Outputable a => SDoc -> a -> Int -> Int -> SDoc
arityErr (TyConFlavour -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TyCon -> TyConFlavour
tyConFlavour TyCon
tc)) (TyCon -> Name
tyConName TyCon
tc)
Int
tc_type_arity Int
tc_type_args
where
vis_tks :: [Type]
vis_tks = TyCon -> [Type] -> [Type]
filterOutInvisibleTypes TyCon
tc [Type]
tks
tc_type_arity :: Int
tc_type_arity = (VarBndr TyCoVar TyConBndrVis -> Bool)
-> [VarBndr TyCoVar TyConBndrVis] -> Int
forall a. (a -> Bool) -> [a] -> Int
count VarBndr TyCoVar TyConBndrVis -> Bool
forall tv. VarBndr tv TyConBndrVis -> Bool
isVisibleTyConBinder (TyCon -> [VarBndr TyCoVar TyConBndrVis]
tyConBinders TyCon
tc)
tc_type_args :: Int
tc_type_args = [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
vis_tks
arityErr :: Outputable a => SDoc -> a -> Int -> Int -> SDoc
arityErr :: forall a. Outputable a => SDoc -> a -> Int -> Int -> SDoc
arityErr SDoc
what a
name Int
n Int
m
= [SDoc] -> SDoc
hsep [ String -> SDoc
text String
"The" SDoc -> SDoc -> SDoc
<+> SDoc
what, SDoc -> SDoc
quotes (a -> SDoc
forall a. Outputable a => a -> SDoc
ppr a
name), String -> SDoc
text String
"should have",
SDoc
n_arguments SDoc -> SDoc -> SDoc
<> SDoc
comma, String -> SDoc
text String
"but has been given",
if Int
mInt -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==Int
0 then String -> SDoc
text String
"none" else Int -> SDoc
int Int
m]
where
n_arguments :: SDoc
n_arguments | Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = String -> SDoc
text String
"no arguments"
| Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 = String -> SDoc
text String
"1 argument"
| Bool
True = [SDoc] -> SDoc
hsep [Int -> SDoc
int Int
n, String -> SDoc
text String
"arguments"]
checkValidInstHead :: UserTypeCtxt -> Class -> [Type] -> TcM ()
checkValidInstHead :: UserTypeCtxt -> Class -> [Type] -> TcM ()
checkValidInstHead UserTypeCtxt
ctxt Class
clas [Type]
cls_args
= do { DynFlags
dflags <- IOEnv (Env TcGblEnv TcLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
; Bool
is_boot <- TcRnIf TcGblEnv TcLclEnv Bool
tcIsHsBootOrSig
; Bool
is_sig <- TcRnIf TcGblEnv TcLclEnv Bool
tcIsHsig
; DynFlags
-> Bool -> Bool -> UserTypeCtxt -> Class -> [Type] -> TcM ()
check_special_inst_head DynFlags
dflags Bool
is_boot Bool
is_sig UserTypeCtxt
ctxt Class
clas [Type]
cls_args
; TyCon -> [Type] -> TcM ()
checkValidTypePats (Class -> TyCon
classTyCon Class
clas) [Type]
cls_args
}
check_special_inst_head :: DynFlags -> Bool -> Bool
-> UserTypeCtxt -> Class -> [Type] -> TcM ()
check_special_inst_head :: DynFlags
-> Bool -> Bool -> UserTypeCtxt -> Class -> [Type] -> TcM ()
check_special_inst_head DynFlags
dflags Bool
is_boot Bool
is_sig UserTypeCtxt
ctxt Class
clas [Type]
cls_args
| Class -> Bool
isAbstractClass Class
clas
, Bool -> Bool
not Bool
is_boot
= SDoc -> TcM ()
forall a. SDoc -> TcM a
failWithTc SDoc
abstract_class_msg
| Name
clas_nm Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
typeableClassName
, Bool -> Bool
not Bool
is_sig
, Bool
hand_written_bindings
= SDoc -> TcM ()
forall a. SDoc -> TcM a
failWithTc SDoc
rejected_class_msg
| Name
clas_nm Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [ Name
knownNatClassName, Name
knownSymbolClassName ]
, Bool -> Bool
not Bool
is_sig
, Bool
hand_written_bindings
= SDoc -> TcM ()
forall a. SDoc -> TcM a
failWithTc SDoc
rejected_class_msg
| Name
clas_nm Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [ Name
heqTyConName, Name
eqTyConName, Name
coercibleTyConName ]
, Bool -> Bool
not Bool
quantified_constraint
= SDoc -> TcM ()
forall a. SDoc -> TcM a
failWithTc SDoc
rejected_class_msg
| Name
clas_nm Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
genericClassNames
, Bool
hand_written_bindings
= do { Bool -> SDoc -> TcM ()
failIfTc (DynFlags -> Bool
safeLanguageOn DynFlags
dflags) SDoc
gen_inst_err
; Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (DynFlags -> Bool
safeInferOn DynFlags
dflags) (WarningMessages -> TcM ()
recordUnsafeInfer WarningMessages
forall a. Bag a
emptyBag) }
| Name
clas_nm Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
hasFieldClassName
= Class -> [Type] -> TcM ()
checkHasFieldInst Class
clas [Type]
cls_args
| Class -> Bool
isCTupleClass Class
clas
= SDoc -> TcM ()
forall a. SDoc -> TcM a
failWithTc SDoc
tuple_class_msg
| Bool
check_h98_arg_shape
, Just SDoc
msg <- Maybe SDoc
mb_ty_args_msg
= SDoc -> TcM ()
forall a. SDoc -> TcM a
failWithTc (Class -> [Type] -> SDoc -> SDoc
instTypeErr Class
clas [Type]
cls_args SDoc
msg)
| Bool
otherwise
= () -> TcM ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
where
clas_nm :: Name
clas_nm = Class -> Name
forall a. NamedThing a => a -> Name
getName Class
clas
ty_args :: [Type]
ty_args = TyCon -> [Type] -> [Type]
filterOutInvisibleTypes (Class -> TyCon
classTyCon Class
clas) [Type]
cls_args
hand_written_bindings :: Bool
hand_written_bindings
= case UserTypeCtxt
ctxt of
InstDeclCtxt Bool
stand_alone -> Bool -> Bool
not Bool
stand_alone
UserTypeCtxt
SpecInstCtxt -> Bool
False
UserTypeCtxt
DerivClauseCtxt -> Bool
False
UserTypeCtxt
_ -> Bool
True
check_h98_arg_shape :: Bool
check_h98_arg_shape = case UserTypeCtxt
ctxt of
UserTypeCtxt
SpecInstCtxt -> Bool
False
UserTypeCtxt
DerivClauseCtxt -> Bool
False
UserTypeCtxt
SigmaCtxt -> Bool
False
UserTypeCtxt
_ -> Bool
True
quantified_constraint :: Bool
quantified_constraint = case UserTypeCtxt
ctxt of
UserTypeCtxt
SigmaCtxt -> Bool
True
UserTypeCtxt
_ -> Bool
False
head_type_synonym_msg :: SDoc
head_type_synonym_msg = SDoc -> SDoc
parens (
String -> SDoc
text String
"All instance types must be of the form (T t1 ... tn)" SDoc -> SDoc -> SDoc
$$
String -> SDoc
text String
"where T is not a synonym." SDoc -> SDoc -> SDoc
$$
String -> SDoc
text String
"Use TypeSynonymInstances if you want to disable this.")
head_type_args_tyvars_msg :: SDoc
head_type_args_tyvars_msg = SDoc -> SDoc
parens ([SDoc] -> SDoc
vcat [
String -> SDoc
text String
"All instance types must be of the form (T a1 ... an)",
String -> SDoc
text String
"where a1 ... an are *distinct type variables*,",
String -> SDoc
text String
"and each type variable appears at most once in the instance head.",
String -> SDoc
text String
"Use FlexibleInstances if you want to disable this."])
head_one_type_msg :: SDoc
head_one_type_msg = SDoc -> SDoc
parens (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
String -> SDoc
text String
"Only one type can be given in an instance head." SDoc -> SDoc -> SDoc
$$
String -> SDoc
text String
"Use MultiParamTypeClasses if you want to allow more, or zero."
rejected_class_msg :: SDoc
rejected_class_msg = String -> SDoc
text String
"Class" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (Name -> SDoc
forall a. Outputable a => a -> SDoc
ppr Name
clas_nm)
SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"does not support user-specified instances"
tuple_class_msg :: SDoc
tuple_class_msg = String -> SDoc
text String
"You can't specify an instance for a tuple constraint"
gen_inst_err :: SDoc
gen_inst_err = SDoc
rejected_class_msg SDoc -> SDoc -> SDoc
$$ Int -> SDoc -> SDoc
nest Int
2 (String -> SDoc
text String
"(in Safe Haskell)")
abstract_class_msg :: SDoc
abstract_class_msg = String -> SDoc
text String
"Cannot define instance for abstract class"
SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (Name -> SDoc
forall a. Outputable a => a -> SDoc
ppr Name
clas_nm)
mb_ty_args_msg :: Maybe SDoc
mb_ty_args_msg
| Bool -> Bool
not (Extension -> DynFlags -> Bool
xopt Extension
LangExt.TypeSynonymInstances DynFlags
dflags)
, Bool -> Bool
not ((Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Type -> Bool
tcInstHeadTyNotSynonym [Type]
ty_args)
= SDoc -> Maybe SDoc
forall a. a -> Maybe a
Just SDoc
head_type_synonym_msg
| Bool -> Bool
not (Extension -> DynFlags -> Bool
xopt Extension
LangExt.FlexibleInstances DynFlags
dflags)
, Bool -> Bool
not ((Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Type -> Bool
tcInstHeadTyAppAllTyVars [Type]
ty_args)
= SDoc -> Maybe SDoc
forall a. a -> Maybe a
Just SDoc
head_type_args_tyvars_msg
| [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ty_args Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
1
, Bool -> Bool
not (Extension -> DynFlags -> Bool
xopt Extension
LangExt.MultiParamTypeClasses DynFlags
dflags)
, Bool -> Bool
not (Extension -> DynFlags -> Bool
xopt Extension
LangExt.NullaryTypeClasses DynFlags
dflags Bool -> Bool -> Bool
&& [Type] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
ty_args)
= SDoc -> Maybe SDoc
forall a. a -> Maybe a
Just SDoc
head_one_type_msg
| Bool
otherwise
= Maybe SDoc
forall a. Maybe a
Nothing
tcInstHeadTyNotSynonym :: Type -> Bool
tcInstHeadTyNotSynonym :: Type -> Bool
tcInstHeadTyNotSynonym Type
ty
= case Type
ty of
TyConApp TyCon
tc [Type]
_ -> Bool -> Bool
not (TyCon -> Bool
isTypeSynonymTyCon TyCon
tc) Bool -> Bool -> Bool
|| TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
unrestrictedFunTyCon
Type
_ -> Bool
True
tcInstHeadTyAppAllTyVars :: Type -> Bool
tcInstHeadTyAppAllTyVars :: Type -> Bool
tcInstHeadTyAppAllTyVars Type
ty
| Just (TyCon
tc, [Type]
tys) <- HasCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
tcSplitTyConApp_maybe (Type -> Type
dropCasts Type
ty)
= let tys' :: [Type]
tys' = TyCon -> [Type] -> [Type]
filterOutInvisibleTypes TyCon
tc [Type]
tys
tys'' :: [Type]
tys'' | TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
funTyCon, Type
tys_h:[Type]
tys_t <- [Type]
tys', Type
tys_h Type -> Type -> Bool
`eqType` Type
manyDataConTy = [Type]
tys_t
| Bool
otherwise = [Type]
tys'
in [Type] -> Bool
ok [Type]
tys''
| LitTy TyLit
_ <- Type
ty = Bool
True
| Bool
otherwise
= Bool
False
where
ok :: [Type] -> Bool
ok [Type]
tys = [TyCoVar] -> [Type] -> Bool
forall a b. [a] -> [b] -> Bool
equalLength [TyCoVar]
tvs [Type]
tys Bool -> Bool -> Bool
&& [TyCoVar] -> Bool
forall a. Eq a => [a] -> Bool
hasNoDups [TyCoVar]
tvs
where
tvs :: [TyCoVar]
tvs = (Type -> Maybe TyCoVar) -> [Type] -> [TyCoVar]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Type -> Maybe TyCoVar
tcGetTyVar_maybe [Type]
tys
dropCasts :: Type -> Type
dropCasts :: Type -> Type
dropCasts (CastTy Type
ty KindCoercion
_) = Type -> Type
dropCasts Type
ty
dropCasts (AppTy Type
t1 Type
t2) = Type -> Type -> Type
mkAppTy (Type -> Type
dropCasts Type
t1) (Type -> Type
dropCasts Type
t2)
dropCasts ty :: Type
ty@(FunTy AnonArgFlag
_ Type
w Type
t1 Type
t2) = Type
ty { ft_mult :: Type
ft_mult = Type -> Type
dropCasts Type
w, ft_arg :: Type
ft_arg = Type -> Type
dropCasts Type
t1, ft_res :: Type
ft_res = Type -> Type
dropCasts Type
t2 }
dropCasts (TyConApp TyCon
tc [Type]
tys) = TyCon -> [Type] -> Type
mkTyConApp TyCon
tc ((Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Type
dropCasts [Type]
tys)
dropCasts (ForAllTy TyVarBinder
b Type
ty) = TyVarBinder -> Type -> Type
ForAllTy (TyVarBinder -> TyVarBinder
dropCastsB TyVarBinder
b) (Type -> Type
dropCasts Type
ty)
dropCasts Type
ty = Type
ty
dropCastsB :: TyVarBinder -> TyVarBinder
dropCastsB :: TyVarBinder -> TyVarBinder
dropCastsB TyVarBinder
b = TyVarBinder
b
instTypeErr :: Class -> [Type] -> SDoc -> SDoc
instTypeErr :: Class -> [Type] -> SDoc -> SDoc
instTypeErr Class
cls [Type]
tys SDoc
msg
= SDoc -> Int -> SDoc -> SDoc
hang (SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Illegal instance declaration for")
Int
2 (SDoc -> SDoc
quotes (Class -> [Type] -> SDoc
pprClassPred Class
cls [Type]
tys)))
Int
2 SDoc
msg
checkHasFieldInst :: Class -> [Type] -> TcM ()
checkHasFieldInst :: Class -> [Type] -> TcM ()
checkHasFieldInst Class
cls tys :: [Type]
tys@[Type
_k_ty, Type
x_ty, Type
r_ty, Type
_a_ty] =
case HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
r_ty of
Maybe (TyCon, [Type])
Nothing -> SDoc -> TcM ()
whoops (String -> SDoc
text String
"Record data type must be specified")
Just (TyCon
tc, [Type]
_)
| TyCon -> Bool
isFamilyTyCon TyCon
tc
-> SDoc -> TcM ()
whoops (String -> SDoc
text String
"Record data type may not be a data family")
| Bool
otherwise -> case Type -> Maybe FastString
isStrLitTy Type
x_ty of
Just FastString
lbl
| Maybe FieldLabel -> Bool
forall a. Maybe a -> Bool
isJust (FastString -> TyCon -> Maybe FieldLabel
lookupTyConFieldLabel FastString
lbl TyCon
tc)
-> SDoc -> TcM ()
whoops (TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tc SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"already has a field"
SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (FastString -> SDoc
forall a. Outputable a => a -> SDoc
ppr FastString
lbl))
| Bool
otherwise -> () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Maybe FastString
Nothing
| [FieldLabel] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (TyCon -> [FieldLabel]
tyConFieldLabels TyCon
tc) -> () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
| Bool
otherwise -> SDoc -> TcM ()
whoops (TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tc SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"has fields")
where
whoops :: SDoc -> TcM ()
whoops = SDoc -> TcM ()
addErrTc (SDoc -> TcM ()) -> (SDoc -> SDoc) -> SDoc -> TcM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Class -> [Type] -> SDoc -> SDoc
instTypeErr Class
cls [Type]
tys
checkHasFieldInst Class
_ [Type]
tys = String -> SDoc -> TcM ()
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"checkHasFieldInst" ([Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
tys)
validDerivPred :: TyVarSet -> PredType -> Bool
validDerivPred :: VarSet -> Type -> Bool
validDerivPred VarSet
tv_set Type
pred
= case Type -> Pred
classifyPredType Type
pred of
ClassPred Class
cls [Type]
tys -> Class
cls Class -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
typeableClassKey
Bool -> Bool -> Bool
|| Class -> [Type] -> Bool
check_tys Class
cls [Type]
tys
EqPred {} -> Bool
False
Pred
_ -> Bool
True
where
check_tys :: Class -> [Type] -> Bool
check_tys Class
cls [Type]
tys
= [TyCoVar] -> Bool
forall a. Eq a => [a] -> Bool
hasNoDups [TyCoVar]
fvs
Bool -> Bool -> Bool
&& [TyCoVar] -> Int -> Bool
forall a. [a] -> Int -> Bool
lengthIs [TyCoVar]
fvs (Type -> Int
sizePred Type
pred)
Bool -> Bool -> Bool
&& (TyCoVar -> Bool) -> [TyCoVar] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (TyCoVar -> VarSet -> Bool
`elemVarSet` VarSet
tv_set) [TyCoVar]
fvs
where tys' :: [Type]
tys' = TyCon -> [Type] -> [Type]
filterOutInvisibleTypes (Class -> TyCon
classTyCon Class
cls) [Type]
tys
fvs :: [TyCoVar]
fvs = [Type] -> [TyCoVar]
fvTypes [Type]
tys'
checkValidInstance :: UserTypeCtxt -> LHsSigType GhcRn -> Type -> TcM ()
checkValidInstance :: UserTypeCtxt -> LHsSigType GhcRn -> Type -> TcM ()
checkValidInstance UserTypeCtxt
ctxt LHsSigType GhcRn
hs_type Type
ty
| Bool -> Bool
not Bool
is_tc_app
= SDoc -> TcM ()
forall a. SDoc -> TcM a
failWithTc (SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Instance head is not headed by a class:")
Int
2 ( Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
tau))
| Maybe Class -> Bool
forall a. Maybe a -> Bool
isNothing Maybe Class
mb_cls
= SDoc -> TcM ()
forall a. SDoc -> TcM a
failWithTc ([SDoc] -> SDoc
vcat [ String -> SDoc
text String
"Illegal instance for a" SDoc -> SDoc -> SDoc
<+> TyConFlavour -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TyCon -> TyConFlavour
tyConFlavour TyCon
tc)
, String -> SDoc
text String
"A class instance must be for a class" ])
| Bool -> Bool
not Bool
arity_ok
= SDoc -> TcM ()
forall a. SDoc -> TcM a
failWithTc (String -> SDoc
text String
"Arity mis-match in instance head")
| Bool
otherwise
= do { SrcSpanAnn' (EpAnn AnnListItem) -> TcM () -> TcM ()
forall ann a. SrcSpanAnn' ann -> TcRn a -> TcRn a
setSrcSpanA SrcSpanAnn' (EpAnn AnnListItem)
head_loc (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$
UserTypeCtxt -> Class -> [Type] -> TcM ()
checkValidInstHead UserTypeCtxt
ctxt Class
clas [Type]
inst_tys
; String -> SDoc -> TcM ()
traceTc String
"checkValidInstance {" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty)
; TidyEnv
env0 <- TcM TidyEnv
tcInitTidyEnv
; ExpandMode
expand <- TcM ExpandMode
initialExpandMode
; TidyEnv -> UserTypeCtxt -> ExpandMode -> [Type] -> TcM ()
check_valid_theta TidyEnv
env0 UserTypeCtxt
ctxt ExpandMode
expand [Type]
theta
; Bool
undecidable_ok <- Extension -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. Extension -> TcRnIf gbl lcl Bool
xoptM Extension
LangExt.UndecidableInstances
; if Bool
undecidable_ok
then UserTypeCtxt -> Type -> TcM ()
checkAmbiguity UserTypeCtxt
ctxt Type
ty
else [Type] -> Type -> TcM ()
checkInstTermination [Type]
theta Type
tau
; String -> SDoc -> TcM ()
traceTc String
"cvi 2" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty)
; case (Bool -> Class -> [Type] -> [Type] -> Validity
checkInstCoverage Bool
undecidable_ok Class
clas [Type]
theta [Type]
inst_tys) of
Validity
IsValid -> () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
NotValid SDoc
msg -> SDoc -> TcM ()
addErrTc (Class -> [Type] -> SDoc -> SDoc
instTypeErr Class
clas [Type]
inst_tys SDoc
msg)
; String -> SDoc -> TcM ()
traceTc String
"End checkValidInstance }" SDoc
empty
; () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return () }
where
([TyCoVar]
_tvs, [Type]
theta, Type
tau) = Type -> ([TyCoVar], [Type], Type)
tcSplitSigmaTy Type
ty
is_tc_app :: Bool
is_tc_app = case Type
tau of { TyConApp {} -> Bool
True; Type
_ -> Bool
False }
TyConApp TyCon
tc [Type]
inst_tys = Type
tau
mb_cls :: Maybe Class
mb_cls = TyCon -> Maybe Class
tyConClass_maybe TyCon
tc
Just Class
clas = Maybe Class
mb_cls
arity_ok :: Bool
arity_ok = [Type]
inst_tys [Type] -> Int -> Bool
forall a. [a] -> Int -> Bool
`lengthIs` Class -> Int
classArity Class
clas
head_loc :: SrcSpanAnn' (EpAnn AnnListItem)
head_loc = GenLocated (SrcSpanAnn' (EpAnn AnnListItem)) (HsType GhcRn)
-> SrcSpanAnn' (EpAnn AnnListItem)
forall l e. GenLocated l e -> l
getLoc (LHsSigType GhcRn -> LHsType GhcRn
forall (p :: Pass). LHsSigType (GhcPass p) -> LHsType (GhcPass p)
getLHsInstDeclHead LHsSigType GhcRn
hs_type)
checkInstTermination :: ThetaType -> TcPredType -> TcM ()
checkInstTermination :: [Type] -> Type -> TcM ()
checkInstTermination [Type]
theta Type
head_pred
= VarSet -> [Type] -> TcM ()
check_preds VarSet
emptyVarSet [Type]
theta
where
head_fvs :: [TyCoVar]
head_fvs = Type -> [TyCoVar]
fvType Type
head_pred
head_size :: Int
head_size = Type -> Int
sizeType Type
head_pred
check_preds :: VarSet -> [PredType] -> TcM ()
check_preds :: VarSet -> [Type] -> TcM ()
check_preds VarSet
foralld_tvs [Type]
preds = (Type -> TcM ()) -> [Type] -> TcM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (VarSet -> Type -> TcM ()
check VarSet
foralld_tvs) [Type]
preds
check :: VarSet -> PredType -> TcM ()
check :: VarSet -> Type -> TcM ()
check VarSet
foralld_tvs Type
pred
= case Type -> Pred
classifyPredType Type
pred of
EqPred {} -> () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
IrredPred {} -> VarSet -> Type -> Int -> TcM ()
check2 VarSet
foralld_tvs Type
pred (Type -> Int
sizeType Type
pred)
ClassPred Class
cls [Type]
tys
| Class -> Bool
isTerminatingClass Class
cls
-> () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
| Class -> Bool
isCTupleClass Class
cls
-> VarSet -> [Type] -> TcM ()
check_preds VarSet
foralld_tvs [Type]
tys
| Bool
otherwise
-> VarSet -> Type -> Int -> TcM ()
check2 VarSet
foralld_tvs Type
pred Int
bogus_size
where
bogus_size :: Int
bogus_size = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [Type] -> Int
sizeTypes (TyCon -> [Type] -> [Type]
filterOutInvisibleTypes (Class -> TyCon
classTyCon Class
cls) [Type]
tys)
ForAllPred [TyCoVar]
tvs [Type]
_ Type
head_pred'
-> VarSet -> Type -> TcM ()
check (VarSet
foralld_tvs VarSet -> [TyCoVar] -> VarSet
`extendVarSetList` [TyCoVar]
tvs) Type
head_pred'
check2 :: VarSet -> Type -> Int -> TcM ()
check2 VarSet
foralld_tvs Type
pred Int
pred_size
| Bool -> Bool
not ([TyCoVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TyCoVar]
bad_tvs) = SDoc -> TcM ()
forall a. SDoc -> TcM a
failWithTc ([TyCoVar] -> SDoc -> SDoc -> SDoc
noMoreMsg [TyCoVar]
bad_tvs SDoc
what (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
head_pred))
| Bool -> Bool
not (Type -> Bool
isTyFamFree Type
pred) = SDoc -> TcM ()
forall a. SDoc -> TcM a
failWithTc (SDoc -> SDoc
nestedMsg SDoc
what)
| Int
pred_size Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
head_size = SDoc -> TcM ()
forall a. SDoc -> TcM a
failWithTc (SDoc -> SDoc -> SDoc
smallerMsg SDoc
what (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
head_pred))
| Bool
otherwise = () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
where
what :: SDoc
what = String -> SDoc
text String
"constraint" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
pred)
bad_tvs :: [TyCoVar]
bad_tvs = (TyCoVar -> Bool) -> [TyCoVar] -> [TyCoVar]
forall a. (a -> Bool) -> [a] -> [a]
filterOut (TyCoVar -> VarSet -> Bool
`elemVarSet` VarSet
foralld_tvs) (Type -> [TyCoVar]
fvType Type
pred)
[TyCoVar] -> [TyCoVar] -> [TyCoVar]
forall a. Eq a => [a] -> [a] -> [a]
\\ [TyCoVar]
head_fvs
smallerMsg :: SDoc -> SDoc -> SDoc
smallerMsg :: SDoc -> SDoc -> SDoc
smallerMsg SDoc
what SDoc
inst_head
= [SDoc] -> SDoc
vcat [ SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"The" SDoc -> SDoc -> SDoc
<+> SDoc
what)
Int
2 ([SDoc] -> SDoc
sep [ String -> SDoc
text String
"is no smaller than"
, String -> SDoc
text String
"the instance head" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes SDoc
inst_head ])
, SDoc -> SDoc
parens SDoc
undecidableMsg ]
noMoreMsg :: [TcTyVar] -> SDoc -> SDoc -> SDoc
noMoreMsg :: [TyCoVar] -> SDoc -> SDoc -> SDoc
noMoreMsg [TyCoVar]
tvs SDoc
what SDoc
inst_head
= [SDoc] -> SDoc
vcat [ SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Variable" SDoc -> SDoc -> SDoc
<> [TyCoVar] -> SDoc
forall a. [a] -> SDoc
plural [TyCoVar]
tvs1 SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes ((TyCoVar -> SDoc) -> [TyCoVar] -> SDoc
forall a. (a -> SDoc) -> [a] -> SDoc
pprWithCommas TyCoVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TyCoVar]
tvs1)
SDoc -> SDoc -> SDoc
<+> SDoc
occurs SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"more often")
Int
2 ([SDoc] -> SDoc
sep [ String -> SDoc
text String
"in the" SDoc -> SDoc -> SDoc
<+> SDoc
what
, String -> SDoc
text String
"than in the instance head" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes SDoc
inst_head ])
, SDoc -> SDoc
parens SDoc
undecidableMsg ]
where
tvs1 :: [TyCoVar]
tvs1 = [TyCoVar] -> [TyCoVar]
forall a. Eq a => [a] -> [a]
nub [TyCoVar]
tvs
occurs :: SDoc
occurs = if [TyCoVar] -> Bool
forall a. [a] -> Bool
isSingleton [TyCoVar]
tvs1 then String -> SDoc
text String
"occurs"
else String -> SDoc
text String
"occur"
undecidableMsg, constraintKindsMsg :: SDoc
undecidableMsg :: SDoc
undecidableMsg = String -> SDoc
text String
"Use UndecidableInstances to permit this"
constraintKindsMsg :: SDoc
constraintKindsMsg = String -> SDoc
text String
"Use ConstraintKinds to permit this"
checkValidCoAxiom :: CoAxiom Branched -> TcM ()
checkValidCoAxiom :: CoAxiom Branched -> TcM ()
checkValidCoAxiom ax :: CoAxiom Branched
ax@(CoAxiom { co_ax_tc :: forall (br :: BranchFlag). CoAxiom br -> TyCon
co_ax_tc = TyCon
fam_tc, co_ax_branches :: forall (br :: BranchFlag). CoAxiom br -> Branches br
co_ax_branches = Branches Branched
branches })
= do { (CoAxBranch -> TcM ()) -> [CoAxBranch] -> TcM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (TyCon -> CoAxBranch -> TcM ()
checkValidCoAxBranch TyCon
fam_tc) [CoAxBranch]
branch_list
; ([CoAxBranch]
-> CoAxBranch -> IOEnv (Env TcGblEnv TcLclEnv) [CoAxBranch])
-> [CoAxBranch] -> [CoAxBranch] -> TcM ()
forall (m :: * -> *) (t :: * -> *) a b.
(Monad m, Foldable t) =>
(a -> b -> m a) -> a -> t b -> m ()
foldlM_ [CoAxBranch]
-> CoAxBranch -> IOEnv (Env TcGblEnv TcLclEnv) [CoAxBranch]
check_branch_compat [] [CoAxBranch]
branch_list }
where
branch_list :: [CoAxBranch]
branch_list = Branches Branched -> [CoAxBranch]
forall (br :: BranchFlag). Branches br -> [CoAxBranch]
fromBranches Branches Branched
branches
injectivity :: Injectivity
injectivity = TyCon -> Injectivity
tyConInjectivityInfo TyCon
fam_tc
check_branch_compat :: [CoAxBranch]
-> CoAxBranch
-> TcM [CoAxBranch]
check_branch_compat :: [CoAxBranch]
-> CoAxBranch -> IOEnv (Env TcGblEnv TcLclEnv) [CoAxBranch]
check_branch_compat [CoAxBranch]
prev_branches CoAxBranch
cur_branch
| CoAxBranch
cur_branch CoAxBranch -> [CoAxBranch] -> Bool
`isDominatedBy` [CoAxBranch]
prev_branches
= do { WarnReason -> SrcSpan -> SDoc -> TcM ()
addWarnAt WarnReason
NoReason (CoAxBranch -> SrcSpan
coAxBranchSpan CoAxBranch
cur_branch) (SDoc -> TcM ()) -> SDoc -> TcM ()
forall a b. (a -> b) -> a -> b
$
TyCon -> CoAxBranch -> SDoc
inaccessibleCoAxBranch TyCon
fam_tc CoAxBranch
cur_branch
; [CoAxBranch] -> IOEnv (Env TcGblEnv TcLclEnv) [CoAxBranch]
forall (m :: * -> *) a. Monad m => a -> m a
return [CoAxBranch]
prev_branches }
| Bool
otherwise
= do { [CoAxBranch] -> CoAxBranch -> TcM ()
check_injectivity [CoAxBranch]
prev_branches CoAxBranch
cur_branch
; [CoAxBranch] -> IOEnv (Env TcGblEnv TcLclEnv) [CoAxBranch]
forall (m :: * -> *) a. Monad m => a -> m a
return (CoAxBranch
cur_branch CoAxBranch -> [CoAxBranch] -> [CoAxBranch]
forall a. a -> [a] -> [a]
: [CoAxBranch]
prev_branches) }
check_injectivity :: [CoAxBranch] -> CoAxBranch -> TcM ()
check_injectivity [CoAxBranch]
prev_branches CoAxBranch
cur_branch
| Injective [Bool]
inj <- Injectivity
injectivity
= do { DynFlags
dflags <- IOEnv (Env TcGblEnv TcLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
; let conflicts :: [CoAxBranch]
conflicts =
([CoAxBranch], Int) -> [CoAxBranch]
forall a b. (a, b) -> a
fst (([CoAxBranch], Int) -> [CoAxBranch])
-> ([CoAxBranch], Int) -> [CoAxBranch]
forall a b. (a -> b) -> a -> b
$ (([CoAxBranch], Int) -> CoAxBranch -> ([CoAxBranch], Int))
-> ([CoAxBranch], Int) -> [CoAxBranch] -> ([CoAxBranch], Int)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' ([Bool]
-> [CoAxBranch]
-> CoAxBranch
-> ([CoAxBranch], Int)
-> CoAxBranch
-> ([CoAxBranch], Int)
gather_conflicts [Bool]
inj [CoAxBranch]
prev_branches CoAxBranch
cur_branch)
([], Int
0) [CoAxBranch]
prev_branches
; TyCon -> [CoAxBranch] -> CoAxBranch -> TcM ()
reportConflictingInjectivityErrs TyCon
fam_tc [CoAxBranch]
conflicts CoAxBranch
cur_branch
; DynFlags -> CoAxiom Branched -> CoAxBranch -> [Bool] -> TcM ()
forall (br :: BranchFlag).
DynFlags -> CoAxiom br -> CoAxBranch -> [Bool] -> TcM ()
reportInjectivityErrors DynFlags
dflags CoAxiom Branched
ax CoAxBranch
cur_branch [Bool]
inj }
| Bool
otherwise
= () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
gather_conflicts :: [Bool]
-> [CoAxBranch]
-> CoAxBranch
-> ([CoAxBranch], Int)
-> CoAxBranch
-> ([CoAxBranch], Int)
gather_conflicts [Bool]
inj [CoAxBranch]
prev_branches CoAxBranch
cur_branch ([CoAxBranch]
acc, Int
n) CoAxBranch
branch
= case [Bool] -> CoAxBranch -> CoAxBranch -> InjectivityCheckResult
injectiveBranches [Bool]
inj CoAxBranch
cur_branch CoAxBranch
branch of
InjectivityUnified CoAxBranch
ax1 CoAxBranch
ax2
| CoAxBranch
ax1 CoAxBranch -> [CoAxBranch] -> Bool
`isDominatedBy` ([CoAxBranch] -> Int -> CoAxBranch -> [CoAxBranch]
replace_br [CoAxBranch]
prev_branches Int
n CoAxBranch
ax2)
-> ([CoAxBranch]
acc, Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
| Bool
otherwise
-> (CoAxBranch
branch CoAxBranch -> [CoAxBranch] -> [CoAxBranch]
forall a. a -> [a] -> [a]
: [CoAxBranch]
acc, Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
InjectivityCheckResult
InjectivityAccepted -> ([CoAxBranch]
acc, Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
replace_br :: [CoAxBranch] -> Int -> CoAxBranch -> [CoAxBranch]
replace_br :: [CoAxBranch] -> Int -> CoAxBranch -> [CoAxBranch]
replace_br [CoAxBranch]
brs Int
n CoAxBranch
br = Int -> [CoAxBranch] -> [CoAxBranch]
forall a. Int -> [a] -> [a]
take Int
n [CoAxBranch]
brs [CoAxBranch] -> [CoAxBranch] -> [CoAxBranch]
forall a. [a] -> [a] -> [a]
++ [CoAxBranch
br] [CoAxBranch] -> [CoAxBranch] -> [CoAxBranch]
forall a. [a] -> [a] -> [a]
++ Int -> [CoAxBranch] -> [CoAxBranch]
forall a. Int -> [a] -> [a]
drop (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) [CoAxBranch]
brs
checkValidCoAxBranch :: TyCon -> CoAxBranch -> TcM ()
checkValidCoAxBranch :: TyCon -> CoAxBranch -> TcM ()
checkValidCoAxBranch TyCon
fam_tc
(CoAxBranch { cab_tvs :: CoAxBranch -> [TyCoVar]
cab_tvs = [TyCoVar]
tvs, cab_cvs :: CoAxBranch -> [TyCoVar]
cab_cvs = [TyCoVar]
cvs
, cab_lhs :: CoAxBranch -> [Type]
cab_lhs = [Type]
typats
, cab_rhs :: CoAxBranch -> Type
cab_rhs = Type
rhs, cab_loc :: CoAxBranch -> SrcSpan
cab_loc = SrcSpan
loc })
= SrcSpan -> TcM () -> TcM ()
forall a. SrcSpan -> TcRn a -> TcRn a
setSrcSpan SrcSpan
loc (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$
TyCon -> [TyCoVar] -> [Type] -> Type -> TcM ()
checkValidTyFamEqn TyCon
fam_tc ([TyCoVar]
tvs[TyCoVar] -> [TyCoVar] -> [TyCoVar]
forall a. [a] -> [a] -> [a]
++[TyCoVar]
cvs) [Type]
typats Type
rhs
checkValidTyFamEqn :: TyCon
-> [Var]
-> [Type]
-> Type
-> TcM ()
checkValidTyFamEqn :: TyCon -> [TyCoVar] -> [Type] -> Type -> TcM ()
checkValidTyFamEqn TyCon
fam_tc [TyCoVar]
qvs [Type]
typats Type
rhs
= do { TyCon -> [Type] -> TcM ()
checkValidTypePats TyCon
fam_tc [Type]
typats
; TyCon -> [TyCoVar] -> [Type] -> Type -> TcM ()
checkFamPatBinders TyCon
fam_tc [TyCoVar]
qvs [Type]
typats Type
rhs
; Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (TyCon -> Bool
isTypeFamilyTyCon TyCon
fam_tc) (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$
case Int -> [Type] -> [Type]
forall a. Int -> [a] -> [a]
drop (TyCon -> Int
tyConArity TyCon
fam_tc) [Type]
typats of
[] -> () -> TcM ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
Type
spec_arg:[Type]
_ ->
SDoc -> TcM ()
addErr (SDoc -> TcM ()) -> SDoc -> TcM ()
forall a b. (a -> b) -> a -> b
$ String -> SDoc
text String
"Illegal oversaturated visible kind argument:"
SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (Char -> SDoc
char Char
'@' SDoc -> SDoc -> SDoc
<> Type -> SDoc
pprParendType Type
spec_arg)
; Type -> TcM ()
checkValidMonoType Type
rhs
; Bool
undecidable_ok <- Extension -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. Extension -> TcRnIf gbl lcl Bool
xoptM Extension
LangExt.UndecidableInstances
; String -> SDoc -> TcM ()
traceTc String
"checkVTFE" (TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
fam_tc SDoc -> SDoc -> SDoc
$$ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
rhs SDoc -> SDoc -> SDoc
$$ [(TyCon, [Type])] -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Type -> [(TyCon, [Type])]
tcTyFamInsts Type
rhs))
; Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
undecidable_ok (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$
(SDoc -> TcM ()) -> [SDoc] -> TcM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ SDoc -> TcM ()
addErrTc (TyCon -> [Type] -> [(TyCon, [Type])] -> [SDoc]
checkFamInstRhs TyCon
fam_tc [Type]
typats (Type -> [(TyCon, [Type])]
tcTyFamInsts Type
rhs)) }
checkValidAssocTyFamDeflt :: TyCon
-> [Type]
-> TcM ()
checkValidAssocTyFamDeflt :: TyCon -> [Type] -> TcM ()
checkValidAssocTyFamDeflt TyCon
fam_tc [Type]
pats =
do { [TyCoVar]
cpt_tvs <- (Type -> ArgFlag -> IOEnv (Env TcGblEnv TcLclEnv) TyCoVar)
-> [Type] -> [ArgFlag] -> IOEnv (Env TcGblEnv TcLclEnv) [TyCoVar]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Type -> ArgFlag -> IOEnv (Env TcGblEnv TcLclEnv) TyCoVar
extract_tv [Type]
pats [ArgFlag]
pats_vis
; [(TyCoVar, ArgFlag)] -> TcM ()
check_all_distinct_tvs ([(TyCoVar, ArgFlag)] -> TcM ()) -> [(TyCoVar, ArgFlag)] -> TcM ()
forall a b. (a -> b) -> a -> b
$ [TyCoVar] -> [ArgFlag] -> [(TyCoVar, ArgFlag)]
forall a b. [a] -> [b] -> [(a, b)]
zip [TyCoVar]
cpt_tvs [ArgFlag]
pats_vis }
where
pats_vis :: [ArgFlag]
pats_vis :: [ArgFlag]
pats_vis = TyCon -> [Type] -> [ArgFlag]
tyConArgFlags TyCon
fam_tc [Type]
pats
extract_tv :: Type
-> ArgFlag
-> TcM TyVar
extract_tv :: Type -> ArgFlag -> IOEnv (Env TcGblEnv TcLclEnv) TyCoVar
extract_tv Type
pat ArgFlag
pat_vis =
case Type -> Maybe TyCoVar
getTyVar_maybe Type
pat of
Just TyCoVar
tv -> TyCoVar -> IOEnv (Env TcGblEnv TcLclEnv) TyCoVar
forall (f :: * -> *) a. Applicative f => a -> f a
pure TyCoVar
tv
Maybe TyCoVar
Nothing -> SDoc -> IOEnv (Env TcGblEnv TcLclEnv) TyCoVar
forall a. SDoc -> TcM a
failWithTc (SDoc -> IOEnv (Env TcGblEnv TcLclEnv) TyCoVar)
-> SDoc -> IOEnv (Env TcGblEnv TcLclEnv) TyCoVar
forall a b. (a -> b) -> a -> b
$
Bool -> SDoc -> SDoc
pprWithExplicitKindsWhen (ArgFlag -> Bool
isInvisibleArgFlag ArgFlag
pat_vis) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Illegal argument" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
pat) SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"in:")
Int
2 ([SDoc] -> SDoc
vcat [SDoc
ppr_eqn, SDoc
suggestion])
check_all_distinct_tvs ::
[(TyVar, ArgFlag)]
-> TcM ()
check_all_distinct_tvs :: [(TyCoVar, ArgFlag)] -> TcM ()
check_all_distinct_tvs [(TyCoVar, ArgFlag)]
cpt_tvs_vis =
let dups :: [NonEmpty (TyCoVar, ArgFlag)]
dups = ((TyCoVar, ArgFlag) -> (TyCoVar, ArgFlag) -> Bool)
-> [(TyCoVar, ArgFlag)] -> [NonEmpty (TyCoVar, ArgFlag)]
forall a. (a -> a -> Bool) -> [a] -> [NonEmpty a]
findDupsEq (TyCoVar -> TyCoVar -> Bool
forall a. Eq a => a -> a -> Bool
(==) (TyCoVar -> TyCoVar -> Bool)
-> ((TyCoVar, ArgFlag) -> TyCoVar)
-> (TyCoVar, ArgFlag)
-> (TyCoVar, ArgFlag)
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (TyCoVar, ArgFlag) -> TyCoVar
forall a b. (a, b) -> a
fst) [(TyCoVar, ArgFlag)]
cpt_tvs_vis in
(NonEmpty (TyCoVar, ArgFlag) -> IOEnv (Env TcGblEnv TcLclEnv) Any)
-> [NonEmpty (TyCoVar, ArgFlag)] -> TcM ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_
(\NonEmpty (TyCoVar, ArgFlag)
d -> let (TyCoVar
pat_tv, ArgFlag
pat_vis) = NonEmpty (TyCoVar, ArgFlag) -> (TyCoVar, ArgFlag)
forall a. NonEmpty a -> a
NE.head NonEmpty (TyCoVar, ArgFlag)
d in SDoc -> IOEnv (Env TcGblEnv TcLclEnv) Any
forall a. SDoc -> TcM a
failWithTc (SDoc -> IOEnv (Env TcGblEnv TcLclEnv) Any)
-> SDoc -> IOEnv (Env TcGblEnv TcLclEnv) Any
forall a b. (a -> b) -> a -> b
$
Bool -> SDoc -> SDoc
pprWithExplicitKindsWhen (ArgFlag -> Bool
isInvisibleArgFlag ArgFlag
pat_vis) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Illegal duplicate variable"
SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (TyCoVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCoVar
pat_tv) SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"in:")
Int
2 ([SDoc] -> SDoc
vcat [SDoc
ppr_eqn, SDoc
suggestion]))
[NonEmpty (TyCoVar, ArgFlag)]
dups
ppr_eqn :: SDoc
ppr_eqn :: SDoc
ppr_eqn =
SDoc -> SDoc
quotes (String -> SDoc
text String
"type" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TyCon -> [Type] -> Type
mkTyConApp TyCon
fam_tc [Type]
pats)
SDoc -> SDoc -> SDoc
<+> SDoc
equals SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"...")
suggestion :: SDoc
suggestion :: SDoc
suggestion = String -> SDoc
text String
"The arguments to" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
fam_tc)
SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"must all be distinct type variables"
checkFamInstRhs :: TyCon -> [Type]
-> [(TyCon, [Type])]
-> [SDoc]
checkFamInstRhs :: TyCon -> [Type] -> [(TyCon, [Type])] -> [SDoc]
checkFamInstRhs TyCon
lhs_tc [Type]
lhs_tys [(TyCon, [Type])]
famInsts
= ((TyCon, [Type]) -> Maybe SDoc) -> [(TyCon, [Type])] -> [SDoc]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (TyCon, [Type]) -> Maybe SDoc
check [(TyCon, [Type])]
famInsts
where
lhs_size :: Int
lhs_size = TyCon -> [Type] -> Int
sizeTyConAppArgs TyCon
lhs_tc [Type]
lhs_tys
inst_head :: SDoc
inst_head = Type -> SDoc
pprType (TyCon -> [Type] -> Type
TyConApp TyCon
lhs_tc [Type]
lhs_tys)
lhs_fvs :: [TyCoVar]
lhs_fvs = [Type] -> [TyCoVar]
fvTypes [Type]
lhs_tys
check :: (TyCon, [Type]) -> Maybe SDoc
check (TyCon
tc, [Type]
tys)
| Bool -> Bool
not ((Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Type -> Bool
isTyFamFree [Type]
tys) = SDoc -> Maybe SDoc
forall a. a -> Maybe a
Just (SDoc -> SDoc
nestedMsg SDoc
what)
| Bool -> Bool
not ([TyCoVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TyCoVar]
bad_tvs) = SDoc -> Maybe SDoc
forall a. a -> Maybe a
Just ([TyCoVar] -> SDoc -> SDoc -> SDoc
noMoreMsg [TyCoVar]
bad_tvs SDoc
what SDoc
inst_head)
| Int
lhs_size Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
fam_app_size = SDoc -> Maybe SDoc
forall a. a -> Maybe a
Just (SDoc -> SDoc -> SDoc
smallerMsg SDoc
what SDoc
inst_head)
| Bool
otherwise = Maybe SDoc
forall a. Maybe a
Nothing
where
what :: SDoc
what = String -> SDoc
text String
"type family application"
SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (Type -> SDoc
pprType (TyCon -> [Type] -> Type
TyConApp TyCon
tc [Type]
tys))
fam_app_size :: Int
fam_app_size = TyCon -> [Type] -> Int
sizeTyConAppArgs TyCon
tc [Type]
tys
bad_tvs :: [TyCoVar]
bad_tvs = [Type] -> [TyCoVar]
fvTypes [Type]
tys [TyCoVar] -> [TyCoVar] -> [TyCoVar]
forall a. Eq a => [a] -> [a] -> [a]
\\ [TyCoVar]
lhs_fvs
checkFamPatBinders :: TyCon
-> [TcTyVar]
-> [TcType]
-> Type
-> TcM ()
checkFamPatBinders :: TyCon -> [TyCoVar] -> [Type] -> Type -> TcM ()
checkFamPatBinders TyCon
fam_tc [TyCoVar]
qtvs [Type]
pats Type
rhs
= do { String -> SDoc -> TcM ()
traceTc String
"checkFamPatBinders" (SDoc -> TcM ()) -> SDoc -> TcM ()
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
vcat [ Type -> SDoc
debugPprType (TyCon -> [Type] -> Type
mkTyConApp TyCon
fam_tc [Type]
pats)
, Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TyCon -> [Type] -> Type
mkTyConApp TyCon
fam_tc [Type]
pats)
, String -> SDoc
text String
"qtvs:" SDoc -> SDoc -> SDoc
<+> [TyCoVar] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TyCoVar]
qtvs
, String -> SDoc
text String
"rhs_tvs:" SDoc -> SDoc -> SDoc
<+> VarSet -> SDoc
forall a. Outputable a => a -> SDoc
ppr (FV -> VarSet
fvVarSet FV
rhs_fvs)
, String -> SDoc
text String
"cpt_tvs:" SDoc -> SDoc -> SDoc
<+> VarSet -> SDoc
forall a. Outputable a => a -> SDoc
ppr VarSet
cpt_tvs
, String -> SDoc
text String
"inj_cpt_tvs:" SDoc -> SDoc -> SDoc
<+> VarSet -> SDoc
forall a. Outputable a => a -> SDoc
ppr VarSet
inj_cpt_tvs ]
; [TyCoVar] -> SDoc -> SDoc -> TcM ()
check_tvs [TyCoVar]
bad_rhs_tvs (String -> SDoc
text String
"mentioned in the RHS")
(String -> SDoc
text String
"bound on the LHS of")
; [TyCoVar] -> SDoc -> SDoc -> TcM ()
check_tvs [TyCoVar]
bad_qtvs (String -> SDoc
text String
"bound by a forall")
(String -> SDoc
text String
"used in")
}
where
cpt_tvs :: VarSet
cpt_tvs = [Type] -> VarSet
tyCoVarsOfTypes [Type]
pats
inj_cpt_tvs :: VarSet
inj_cpt_tvs = FV -> VarSet
fvVarSet (FV -> VarSet) -> FV -> VarSet
forall a b. (a -> b) -> a -> b
$ Bool -> [Type] -> FV
injectiveVarsOfTypes Bool
False [Type]
pats
rhs_fvs :: FV
rhs_fvs = Type -> FV
tyCoFVsOfType Type
rhs
used_tvs :: VarSet
used_tvs = VarSet
cpt_tvs VarSet -> VarSet -> VarSet
`unionVarSet` FV -> VarSet
fvVarSet FV
rhs_fvs
bad_qtvs :: [TyCoVar]
bad_qtvs = (TyCoVar -> Bool) -> [TyCoVar] -> [TyCoVar]
forall a. (a -> Bool) -> [a] -> [a]
filterOut (TyCoVar -> VarSet -> Bool
`elemVarSet` VarSet
used_tvs) [TyCoVar]
qtvs
bad_rhs_tvs :: [TyCoVar]
bad_rhs_tvs = (TyCoVar -> Bool) -> [TyCoVar] -> [TyCoVar]
forall a. (a -> Bool) -> [a] -> [a]
filterOut (TyCoVar -> VarSet -> Bool
`elemVarSet` VarSet
inj_cpt_tvs) (FV -> [TyCoVar]
fvVarList FV
rhs_fvs)
dodgy_tvs :: VarSet
dodgy_tvs = VarSet
cpt_tvs VarSet -> VarSet -> VarSet
`minusVarSet` VarSet
inj_cpt_tvs
check_tvs :: [TyCoVar] -> SDoc -> SDoc -> TcM ()
check_tvs [TyCoVar]
tvs SDoc
what SDoc
what2
= Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([TyCoVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TyCoVar]
tvs) (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$ SrcSpan -> SDoc -> TcM ()
addErrAt (TyCoVar -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
getSrcSpan ([TyCoVar] -> TyCoVar
forall a. [a] -> a
head [TyCoVar]
tvs)) (SDoc -> TcM ()) -> SDoc -> TcM ()
forall a b. (a -> b) -> a -> b
$
SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Type variable" SDoc -> SDoc -> SDoc
<> [TyCoVar] -> SDoc
forall a. [a] -> SDoc
plural [TyCoVar]
tvs SDoc -> SDoc -> SDoc
<+> [TyCoVar] -> SDoc
forall a. Outputable a => [a] -> SDoc
pprQuotedList [TyCoVar]
tvs
SDoc -> SDoc -> SDoc
<+> [TyCoVar] -> SDoc
forall a. [a] -> SDoc
isOrAre [TyCoVar]
tvs SDoc -> SDoc -> SDoc
<+> SDoc
what SDoc -> SDoc -> SDoc
<> SDoc
comma)
Int
2 ([SDoc] -> SDoc
vcat [ String -> SDoc
text String
"but not" SDoc -> SDoc -> SDoc
<+> SDoc
what2 SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"the family instance"
, [TyCoVar] -> SDoc
mk_extra [TyCoVar]
tvs ])
mk_extra :: [TyCoVar] -> SDoc
mk_extra [TyCoVar]
tvs = Bool -> SDoc -> SDoc
ppWhen ((TyCoVar -> Bool) -> [TyCoVar] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (TyCoVar -> VarSet -> Bool
`elemVarSet` VarSet
dodgy_tvs) [TyCoVar]
tvs) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"The real LHS (expanding synonyms) is:")
Int
2 (TyCon -> [Type] -> SDoc
pprTypeApp TyCon
fam_tc ((Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Type
expandTypeSynonyms [Type]
pats))
checkValidTypePats :: TyCon -> [Type] -> TcM ()
checkValidTypePats :: TyCon -> [Type] -> TcM ()
checkValidTypePats TyCon
tc [Type]
pat_ty_args
= do {
(Type -> TcM ()) -> [Type] -> TcM ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ Type -> TcM ()
checkValidMonoType [Type]
pat_ty_args
; case TyCon -> [Type] -> [(Bool, TyCon, [Type])]
tcTyConAppTyFamInstsAndVis TyCon
tc [Type]
pat_ty_args of
[] -> () -> TcM ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
((Bool
tf_is_invis_arg, TyCon
tf_tc, [Type]
tf_args):[(Bool, TyCon, [Type])]
_) -> SDoc -> TcM ()
forall a. SDoc -> TcM a
failWithTc (SDoc -> TcM ()) -> SDoc -> TcM ()
forall a b. (a -> b) -> a -> b
$
Bool -> Type -> SDoc
ty_fam_inst_illegal_err Bool
tf_is_invis_arg
(TyCon -> [Type] -> Type
mkTyConApp TyCon
tf_tc [Type]
tf_args) }
where
inst_ty :: Type
inst_ty = TyCon -> [Type] -> Type
mkTyConApp TyCon
tc [Type]
pat_ty_args
ty_fam_inst_illegal_err :: Bool -> Type -> SDoc
ty_fam_inst_illegal_err :: Bool -> Type -> SDoc
ty_fam_inst_illegal_err Bool
invis_arg Type
ty
= Bool -> SDoc -> SDoc
pprWithExplicitKindsWhen Bool
invis_arg (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Illegal type synonym family application"
SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty) SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"in instance" SDoc -> SDoc -> SDoc
<> SDoc
colon)
Int
2 (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
inst_ty)
inaccessibleCoAxBranch :: TyCon -> CoAxBranch -> SDoc
inaccessibleCoAxBranch :: TyCon -> CoAxBranch -> SDoc
inaccessibleCoAxBranch TyCon
fam_tc CoAxBranch
cur_branch
= String -> SDoc
text String
"Type family instance equation is overlapped:" SDoc -> SDoc -> SDoc
$$
Int -> SDoc -> SDoc
nest Int
2 (TyCon -> CoAxBranch -> SDoc
pprCoAxBranchUser TyCon
fam_tc CoAxBranch
cur_branch)
nestedMsg :: SDoc -> SDoc
nestedMsg :: SDoc -> SDoc
nestedMsg SDoc
what
= [SDoc] -> SDoc
sep [ String -> SDoc
text String
"Illegal nested" SDoc -> SDoc -> SDoc
<+> SDoc
what
, SDoc -> SDoc
parens SDoc
undecidableMsg ]
badATErr :: Name -> Name -> SDoc
badATErr :: Name -> Name -> SDoc
badATErr Name
clas Name
op
= [SDoc] -> SDoc
hsep [String -> SDoc
text String
"Class", SDoc -> SDoc
quotes (Name -> SDoc
forall a. Outputable a => a -> SDoc
ppr Name
clas),
String -> SDoc
text String
"does not have an associated type", SDoc -> SDoc
quotes (Name -> SDoc
forall a. Outputable a => a -> SDoc
ppr Name
op)]
checkConsistentFamInst :: AssocInstInfo
-> TyCon
-> CoAxBranch
-> TcM ()
checkConsistentFamInst :: AssocInstInfo -> TyCon -> CoAxBranch -> TcM ()
checkConsistentFamInst AssocInstInfo
NotAssociated TyCon
_ CoAxBranch
_
= () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkConsistentFamInst (InClsInst { ai_class :: AssocInstInfo -> Class
ai_class = Class
clas
, ai_tyvars :: AssocInstInfo -> [TyCoVar]
ai_tyvars = [TyCoVar]
inst_tvs
, ai_inst_env :: AssocInstInfo -> VarEnv Type
ai_inst_env = VarEnv Type
mini_env })
TyCon
fam_tc CoAxBranch
branch
= do { String -> SDoc -> TcM ()
traceTc String
"checkConsistentFamInst" ([SDoc] -> SDoc
vcat [ [TyCoVar] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TyCoVar]
inst_tvs
, [(Type, Type, ArgFlag)] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [(Type, Type, ArgFlag)]
arg_triples
, VarEnv Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr VarEnv Type
mini_env
, [TyCoVar] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TyCoVar]
ax_tvs
, [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
ax_arg_tys
, [(Type, Type, ArgFlag)] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [(Type, Type, ArgFlag)]
arg_triples ])
; Bool -> SDoc -> TcM ()
checkTc (TyCon -> Maybe TyCon
forall a. a -> Maybe a
Just (Class -> TyCon
classTyCon Class
clas) Maybe TyCon -> Maybe TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon -> Maybe TyCon
tyConAssoc_maybe TyCon
fam_tc)
(Name -> Name -> SDoc
badATErr (Class -> Name
className Class
clas) (TyCon -> Name
tyConName TyCon
fam_tc))
; [(Type, Type, ArgFlag)] -> TcM ()
check_match [(Type, Type, ArgFlag)]
arg_triples
}
where
([TyCoVar]
ax_tvs, [Type]
ax_arg_tys, Type
_) = CoAxBranch -> ([TyCoVar], [Type], Type)
etaExpandCoAxBranch CoAxBranch
branch
arg_triples :: [(Type,Type, ArgFlag)]
arg_triples :: [(Type, Type, ArgFlag)]
arg_triples = [ (Type
cls_arg_ty, Type
at_arg_ty, ArgFlag
vis)
| (TyCoVar
fam_tc_tv, ArgFlag
vis, Type
at_arg_ty)
<- [TyCoVar] -> [ArgFlag] -> [Type] -> [(TyCoVar, ArgFlag, Type)]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 (TyCon -> [TyCoVar]
tyConTyVars TyCon
fam_tc)
(TyCon -> [Type] -> [ArgFlag]
tyConArgFlags TyCon
fam_tc [Type]
ax_arg_tys)
[Type]
ax_arg_tys
, Just Type
cls_arg_ty <- [VarEnv Type -> TyCoVar -> Maybe Type
forall a. VarEnv a -> TyCoVar -> Maybe a
lookupVarEnv VarEnv Type
mini_env TyCoVar
fam_tc_tv] ]
pp_wrong_at_arg :: ArgFlag -> SDoc
pp_wrong_at_arg ArgFlag
vis
= Bool -> SDoc -> SDoc
pprWithExplicitKindsWhen (ArgFlag -> Bool
isInvisibleArgFlag ArgFlag
vis) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
vcat [ String -> SDoc
text String
"Type indexes must match class instance head"
, String -> SDoc
text String
"Expected:" SDoc -> SDoc -> SDoc
<+> SDoc
pp_expected_ty
, String -> SDoc
text String
" Actual:" SDoc -> SDoc -> SDoc
<+> SDoc
pp_actual_ty ]
(TidyEnv
tidy_env1, [TyCoVar]
_) = TidyEnv -> [TyCoVar] -> (TidyEnv, [TyCoVar])
tidyVarBndrs TidyEnv
emptyTidyEnv [TyCoVar]
inst_tvs
(TidyEnv
tidy_env2, [TyCoVar]
_) = TidyEnv -> [TyCoVar] -> (TidyEnv, [TyCoVar])
tidyCoAxBndrsForUser TidyEnv
tidy_env1 ([TyCoVar]
ax_tvs [TyCoVar] -> [TyCoVar] -> [TyCoVar]
forall a. Eq a => [a] -> [a] -> [a]
\\ [TyCoVar]
inst_tvs)
pp_expected_ty :: SDoc
pp_expected_ty = PprPrec -> IfaceTyCon -> IfaceAppArgs -> SDoc
pprIfaceTypeApp PprPrec
topPrec (TyCon -> IfaceTyCon
toIfaceTyCon TyCon
fam_tc) (IfaceAppArgs -> SDoc) -> IfaceAppArgs -> SDoc
forall a b. (a -> b) -> a -> b
$
TyCon -> [Type] -> IfaceAppArgs
toIfaceTcArgs TyCon
fam_tc ([Type] -> IfaceAppArgs) -> [Type] -> IfaceAppArgs
forall a b. (a -> b) -> a -> b
$
[ case VarEnv Type -> TyCoVar -> Maybe Type
forall a. VarEnv a -> TyCoVar -> Maybe a
lookupVarEnv VarEnv Type
mini_env TyCoVar
at_tv of
Just Type
cls_arg_ty -> TidyEnv -> Type -> Type
tidyType TidyEnv
tidy_env2 Type
cls_arg_ty
Maybe Type
Nothing -> TyCoVar -> Type
mk_wildcard TyCoVar
at_tv
| TyCoVar
at_tv <- TyCon -> [TyCoVar]
tyConTyVars TyCon
fam_tc ]
pp_actual_ty :: SDoc
pp_actual_ty = PprPrec -> IfaceTyCon -> IfaceAppArgs -> SDoc
pprIfaceTypeApp PprPrec
topPrec (TyCon -> IfaceTyCon
toIfaceTyCon TyCon
fam_tc) (IfaceAppArgs -> SDoc) -> IfaceAppArgs -> SDoc
forall a b. (a -> b) -> a -> b
$
TyCon -> [Type] -> IfaceAppArgs
toIfaceTcArgs TyCon
fam_tc ([Type] -> IfaceAppArgs) -> [Type] -> IfaceAppArgs
forall a b. (a -> b) -> a -> b
$
TidyEnv -> [Type] -> [Type]
tidyTypes TidyEnv
tidy_env2 [Type]
ax_arg_tys
mk_wildcard :: TyCoVar -> Type
mk_wildcard TyCoVar
at_tv = TyCoVar -> Type
mkTyVarTy (Name -> Type -> TyCoVar
mkTyVar Name
tv_name (TyCoVar -> Type
tyVarKind TyCoVar
at_tv))
tv_name :: Name
tv_name = Unique -> OccName -> SrcSpan -> Name
mkInternalName (Int -> Unique
mkAlphaTyVarUnique Int
1) (String -> OccName
mkTyVarOcc String
"_") SrcSpan
noSrcSpan
check_match :: [(Type,Type,ArgFlag)] -> TcM ()
check_match :: [(Type, Type, ArgFlag)] -> TcM ()
check_match [(Type, Type, ArgFlag)]
triples = TCvSubst -> TCvSubst -> [(Type, Type, ArgFlag)] -> TcM ()
go TCvSubst
emptyTCvSubst TCvSubst
emptyTCvSubst [(Type, Type, ArgFlag)]
triples
go :: TCvSubst -> TCvSubst -> [(Type, Type, ArgFlag)] -> TcM ()
go TCvSubst
_ TCvSubst
_ [] = () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
go TCvSubst
lr_subst TCvSubst
rl_subst ((Type
ty1,Type
ty2,ArgFlag
vis):[(Type, Type, ArgFlag)]
triples)
| Just TCvSubst
lr_subst1 <- BindFun -> TCvSubst -> Type -> Type -> Maybe TCvSubst
tcMatchTyX_BM BindFun
bind_me TCvSubst
lr_subst Type
ty1 Type
ty2
, Just TCvSubst
rl_subst1 <- BindFun -> TCvSubst -> Type -> Type -> Maybe TCvSubst
tcMatchTyX_BM BindFun
bind_me TCvSubst
rl_subst Type
ty2 Type
ty1
= TCvSubst -> TCvSubst -> [(Type, Type, ArgFlag)] -> TcM ()
go TCvSubst
lr_subst1 TCvSubst
rl_subst1 [(Type, Type, ArgFlag)]
triples
| Bool
otherwise
= SDoc -> TcM ()
addErrTc (ArgFlag -> SDoc
pp_wrong_at_arg ArgFlag
vis)
no_bind_set :: VarSet
no_bind_set = [TyCoVar] -> VarSet
mkVarSet [TyCoVar]
inst_tvs
bind_me :: BindFun
bind_me TyCoVar
tv Type
_ty | TyCoVar
tv TyCoVar -> VarSet -> Bool
`elemVarSet` VarSet
no_bind_set = BindFlag
Apart
| Bool
otherwise = BindFlag
BindMe
type TelescopeAcc
= ( TyVarSet
, Bool
)
checkTyConTelescope :: TyCon -> TcM ()
checkTyConTelescope :: TyCon -> TcM ()
checkTyConTelescope TyCon
tc
| Bool
bad_scope
=
SDoc -> TcM ()
addErr (SDoc -> TcM ()) -> SDoc -> TcM ()
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
vcat [ SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"The kind of" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tc) SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"is ill-scoped")
Int
2 SDoc
pp_tc_kind
, SDoc
extra
, SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Perhaps try this order instead:")
Int
2 ([TyCoVar] -> SDoc
pprTyVars [TyCoVar]
sorted_tvs) ]
| Bool
otherwise
= () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
where
tcbs :: [VarBndr TyCoVar TyConBndrVis]
tcbs = TyCon -> [VarBndr TyCoVar TyConBndrVis]
tyConBinders TyCon
tc
tvs :: [TyCoVar]
tvs = [VarBndr TyCoVar TyConBndrVis] -> [TyCoVar]
forall tv argf. [VarBndr tv argf] -> [tv]
binderVars [VarBndr TyCoVar TyConBndrVis]
tcbs
sorted_tvs :: [TyCoVar]
sorted_tvs = [TyCoVar] -> [TyCoVar]
scopedSort [TyCoVar]
tvs
(VarSet
_, Bool
bad_scope) = ((VarSet, Bool) -> VarBndr TyCoVar TyConBndrVis -> (VarSet, Bool))
-> (VarSet, Bool)
-> [VarBndr TyCoVar TyConBndrVis]
-> (VarSet, Bool)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (VarSet, Bool) -> VarBndr TyCoVar TyConBndrVis -> (VarSet, Bool)
add_one (VarSet
emptyVarSet, Bool
False) [VarBndr TyCoVar TyConBndrVis]
tcbs
add_one :: TelescopeAcc -> TyConBinder -> TelescopeAcc
add_one :: (VarSet, Bool) -> VarBndr TyCoVar TyConBndrVis -> (VarSet, Bool)
add_one (VarSet
bound, Bool
bad_scope) VarBndr TyCoVar TyConBndrVis
tcb
= ( VarSet
bound VarSet -> TyCoVar -> VarSet
`extendVarSet` TyCoVar
tv
, Bool
bad_scope Bool -> Bool -> Bool
|| Bool -> Bool
not (VarSet -> Bool
isEmptyVarSet (VarSet
fkvs VarSet -> VarSet -> VarSet
`minusVarSet` VarSet
bound)) )
where
tv :: TyCoVar
tv = VarBndr TyCoVar TyConBndrVis -> TyCoVar
forall tv argf. VarBndr tv argf -> tv
binderVar VarBndr TyCoVar TyConBndrVis
tcb
fkvs :: VarSet
fkvs = Type -> VarSet
tyCoVarsOfType (TyCoVar -> Type
tyVarKind TyCoVar
tv)
inferred_tvs :: [TyCoVar]
inferred_tvs = [ VarBndr TyCoVar TyConBndrVis -> TyCoVar
forall tv argf. VarBndr tv argf -> tv
binderVar VarBndr TyCoVar TyConBndrVis
tcb
| VarBndr TyCoVar TyConBndrVis
tcb <- [VarBndr TyCoVar TyConBndrVis]
tcbs, ArgFlag
Inferred ArgFlag -> ArgFlag -> Bool
forall a. Eq a => a -> a -> Bool
== VarBndr TyCoVar TyConBndrVis -> ArgFlag
tyConBinderArgFlag VarBndr TyCoVar TyConBndrVis
tcb ]
specified_tvs :: [TyCoVar]
specified_tvs = [ VarBndr TyCoVar TyConBndrVis -> TyCoVar
forall tv argf. VarBndr tv argf -> tv
binderVar VarBndr TyCoVar TyConBndrVis
tcb
| VarBndr TyCoVar TyConBndrVis
tcb <- [VarBndr TyCoVar TyConBndrVis]
tcbs, ArgFlag
Specified ArgFlag -> ArgFlag -> Bool
forall a. Eq a => a -> a -> Bool
== VarBndr TyCoVar TyConBndrVis -> ArgFlag
tyConBinderArgFlag VarBndr TyCoVar TyConBndrVis
tcb ]
pp_inf :: SDoc
pp_inf = SDoc -> SDoc
parens (String -> SDoc
text String
"namely:" SDoc -> SDoc -> SDoc
<+> [TyCoVar] -> SDoc
pprTyVars [TyCoVar]
inferred_tvs)
pp_spec :: SDoc
pp_spec = SDoc -> SDoc
parens (String -> SDoc
text String
"namely:" SDoc -> SDoc -> SDoc
<+> [TyCoVar] -> SDoc
pprTyVars [TyCoVar]
specified_tvs)
pp_tc_kind :: SDoc
pp_tc_kind = String -> SDoc
text String
"Inferred kind:" SDoc -> SDoc -> SDoc
<+> TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tc SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> Type -> SDoc
ppr_untidy (TyCon -> Type
tyConKind TyCon
tc)
ppr_untidy :: Type -> SDoc
ppr_untidy Type
ty = IfaceType -> SDoc
pprIfaceType (Type -> IfaceType
toIfaceType Type
ty)
extra :: SDoc
extra
| [TyCoVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TyCoVar]
inferred_tvs Bool -> Bool -> Bool
&& [TyCoVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TyCoVar]
specified_tvs
= SDoc
empty
| [TyCoVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TyCoVar]
inferred_tvs
= SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"NB: Specified variables")
Int
2 ([SDoc] -> SDoc
sep [SDoc
pp_spec, String -> SDoc
text String
"always come first"])
| [TyCoVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TyCoVar]
specified_tvs
= SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"NB: Inferred variables")
Int
2 ([SDoc] -> SDoc
sep [SDoc
pp_inf, String -> SDoc
text String
"always come first"])
| Bool
otherwise
= SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"NB: Inferred variables")
Int
2 ([SDoc] -> SDoc
vcat [ [SDoc] -> SDoc
sep [ SDoc
pp_inf, String -> SDoc
text String
"always come first"]
, [SDoc] -> SDoc
sep [String -> SDoc
text String
"then Specified variables", SDoc
pp_spec]])
fvType :: Type -> [TyCoVar]
fvType :: Type -> [TyCoVar]
fvType Type
ty | Just Type
exp_ty <- Type -> Maybe Type
tcView Type
ty = Type -> [TyCoVar]
fvType Type
exp_ty
fvType (TyVarTy TyCoVar
tv) = [TyCoVar
tv]
fvType (TyConApp TyCon
_ [Type]
tys) = [Type] -> [TyCoVar]
fvTypes [Type]
tys
fvType (LitTy {}) = []
fvType (AppTy Type
fun Type
arg) = Type -> [TyCoVar]
fvType Type
fun [TyCoVar] -> [TyCoVar] -> [TyCoVar]
forall a. [a] -> [a] -> [a]
++ Type -> [TyCoVar]
fvType Type
arg
fvType (FunTy AnonArgFlag
_ Type
w Type
arg Type
res) = Type -> [TyCoVar]
fvType Type
w [TyCoVar] -> [TyCoVar] -> [TyCoVar]
forall a. [a] -> [a] -> [a]
++ Type -> [TyCoVar]
fvType Type
arg [TyCoVar] -> [TyCoVar] -> [TyCoVar]
forall a. [a] -> [a] -> [a]
++ Type -> [TyCoVar]
fvType Type
res
fvType (ForAllTy (Bndr TyCoVar
tv ArgFlag
_) Type
ty)
= Type -> [TyCoVar]
fvType (TyCoVar -> Type
tyVarKind TyCoVar
tv) [TyCoVar] -> [TyCoVar] -> [TyCoVar]
forall a. [a] -> [a] -> [a]
++
(TyCoVar -> Bool) -> [TyCoVar] -> [TyCoVar]
forall a. (a -> Bool) -> [a] -> [a]
filter (TyCoVar -> TyCoVar -> Bool
forall a. Eq a => a -> a -> Bool
/= TyCoVar
tv) (Type -> [TyCoVar]
fvType Type
ty)
fvType (CastTy Type
ty KindCoercion
_) = Type -> [TyCoVar]
fvType Type
ty
fvType (CoercionTy {}) = []
fvTypes :: [Type] -> [TyVar]
fvTypes :: [Type] -> [TyCoVar]
fvTypes [Type]
tys = (Type -> [TyCoVar]) -> [Type] -> [TyCoVar]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Type -> [TyCoVar]
fvType [Type]
tys
sizeType :: Type -> Int
sizeType :: Type -> Int
sizeType Type
ty | Just Type
exp_ty <- Type -> Maybe Type
tcView Type
ty = Type -> Int
sizeType Type
exp_ty
sizeType (TyVarTy {}) = Int
1
sizeType (TyConApp TyCon
tc [Type]
tys) = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ TyCon -> [Type] -> Int
sizeTyConAppArgs TyCon
tc [Type]
tys
sizeType (LitTy {}) = Int
1
sizeType (AppTy Type
fun Type
arg) = Type -> Int
sizeType Type
fun Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Type -> Int
sizeType Type
arg
sizeType (FunTy AnonArgFlag
_ Type
w Type
arg Type
res) = Type -> Int
sizeType Type
w Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Type -> Int
sizeType Type
arg Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Type -> Int
sizeType Type
res Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
sizeType (ForAllTy TyVarBinder
_ Type
ty) = Type -> Int
sizeType Type
ty
sizeType (CastTy Type
ty KindCoercion
_) = Type -> Int
sizeType Type
ty
sizeType (CoercionTy KindCoercion
_) = Int
0
sizeTypes :: [Type] -> Int
sizeTypes :: [Type] -> Int
sizeTypes = (Type -> Int -> Int) -> Int -> [Type] -> Int
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Int -> Int -> Int
forall a. Num a => a -> a -> a
(+) (Int -> Int -> Int) -> (Type -> Int) -> Type -> Int -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Int
sizeType) Int
0
sizeTyConAppArgs :: TyCon -> [Type] -> Int
sizeTyConAppArgs :: TyCon -> [Type] -> Int
sizeTyConAppArgs TyCon
_tc [Type]
tys = [Type] -> Int
sizeTypes [Type]
tys
sizePred :: PredType -> Int
sizePred :: Type -> Int
sizePred Type
ty = Type -> Int
goClass Type
ty
where
goClass :: Type -> Int
goClass Type
p = Pred -> Int
go (Type -> Pred
classifyPredType Type
p)
go :: Pred -> Int
go (ClassPred Class
cls [Type]
tys')
| Class -> Bool
isTerminatingClass Class
cls = Int
0
| Bool
otherwise = [Type] -> Int
sizeTypes (TyCon -> [Type] -> [Type]
filterOutInvisibleTypes (Class -> TyCon
classTyCon Class
cls) [Type]
tys')
go (EqPred {}) = Int
0
go (IrredPred Type
ty) = Type -> Int
sizeType Type
ty
go (ForAllPred [TyCoVar]
_ [Type]
_ Type
pred) = Type -> Int
goClass Type
pred
isTerminatingClass :: Class -> Bool
isTerminatingClass :: Class -> Bool
isTerminatingClass Class
cls
= Class -> Bool
isIPClass Class
cls
Bool -> Bool -> Bool
|| Class -> Bool
isEqPredClass Class
cls
Bool -> Bool -> Bool
|| Class
cls Class -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
typeableClassKey
Bool -> Bool -> Bool
|| Class
cls Class -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
coercibleTyConKey
ppr_tidy :: TidyEnv -> Type -> SDoc
ppr_tidy :: TidyEnv -> Type -> SDoc
ppr_tidy TidyEnv
env Type
ty = Type -> SDoc
pprType (TidyEnv -> Type -> Type
tidyType TidyEnv
env Type
ty)
allDistinctTyVars :: TyVarSet -> [KindOrType] -> Bool
allDistinctTyVars :: VarSet -> [Type] -> Bool
allDistinctTyVars VarSet
_ [] = Bool
True
allDistinctTyVars VarSet
tkvs (Type
ty : [Type]
tys)
= case Type -> Maybe TyCoVar
getTyVar_maybe Type
ty of
Maybe TyCoVar
Nothing -> Bool
False
Just TyCoVar
tv | TyCoVar
tv TyCoVar -> VarSet -> Bool
`elemVarSet` VarSet
tkvs -> Bool
False
| Bool
otherwise -> VarSet -> [Type] -> Bool
allDistinctTyVars (VarSet
tkvs VarSet -> TyCoVar -> VarSet
`extendVarSet` TyCoVar
tv) [Type]
tys