{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE LambdaCase #-}
{-# 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, checkEscapingKind,
checkValidCoAxiom, checkValidCoAxBranch,
checkFamPatBinders, checkTyFamEqnValidityInfo,
checkValidTyFamEqn, checkValidAssocTyFamDeflt, checkConsistentFamInst,
checkTyConTelescope,
) where
import GHC.Prelude
import GHC.Data.FastString
import GHC.Data.Maybe
import GHC.Tc.Utils.Unify ( tcSubTypeAmbiguity )
import GHC.Tc.Solver ( simplifyAmbiguityCheck )
import GHC.Tc.Instance.Class ( matchGlobalInst, ClsInstResult(..), AssocInstInfo(..) )
import GHC.Tc.Utils.TcType
import GHC.Tc.Types.Origin
import GHC.Tc.Types.Rank
import GHC.Tc.Errors.Types
import GHC.Tc.Utils.Monad
import GHC.Tc.Instance.FunDeps
import GHC.Tc.Instance.Family
import GHC.Tc.Zonk.TcType
import GHC.Builtin.Types
import GHC.Builtin.Names
import GHC.Builtin.Uniques ( mkAlphaTyVarUnique )
import GHC.Core.Type
import GHC.Core.Unify ( typesAreApart, 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.Core.TyCo.FVs
import GHC.Core.TyCo.Rep
import GHC.Core.TyCo.Ppr
import GHC.Core.FamInstEnv ( isDominatedBy, injectiveBranches
, InjectivityCheckResult(..) )
import GHC.Hs
import GHC.Driver.Session
import qualified GHC.LanguageExtensions as LangExt
import GHC.Types.Error
import GHC.Types.Basic ( TypeOrKind(..), UnboxedTupleOrSum(..)
, unboxedTupleOrSumExtension )
import GHC.Types.Name
import GHC.Types.Var.Env
import GHC.Types.Var.Set
import GHC.Types.Var ( VarBndr(..), isInvisibleFunArg, mkTyVar, tyVarName )
import GHC.Types.SourceFile
import GHC.Types.SrcLoc
import GHC.Types.TyThing ( TyThing(..) )
import GHC.Types.Unique.Set( isEmptyUniqSet )
import GHC.Utils.FV
import GHC.Utils.Error
import GHC.Utils.Misc
import GHC.Utils.Outputable as Outputable
import GHC.Utils.Panic
import GHC.Data.List.SetOps
import Language.Haskell.Syntax.Basic (FieldLabelString(..))
import Control.Monad
import Data.Foldable
import Data.Function
import Data.List ( (\\) )
import qualified Data.List.NonEmpty as NE
import Data.List.NonEmpty ( NonEmpty(..) )
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)
; allow_ambiguous <- Extension -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. Extension -> TcRnIf gbl lcl Bool
xoptM Extension
LangExt.AllowAmbiguousTypes
; unless allow_ambiguous $
do { (_wrap, wanted) <- addErrCtxt (mk_msg allow_ambiguous) $
captureConstraints $
tcSubTypeAmbiguity ctxt ty ty
; simplifyAmbiguityCheck ty wanted }
; traceTc "} Done ambiguity check for" (ppr ty) }
| Bool
otherwise
= () -> TcM ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
where
mk_msg :: Bool -> SDoc
mk_msg Bool
allow_ambiguous
= [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"In the ambiguity check for" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
what
, Bool -> SDoc -> SDoc
forall doc. IsOutput doc => Bool -> doc -> doc
ppUnless Bool
allow_ambiguous SDoc
ambig_msg ]
ambig_msg :: SDoc
ambig_msg = String -> SDoc
forall doc. IsLine doc => String -> doc
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 :: UserTypeCtxt -> Type -> TcM ()
checkUserTypeError :: UserTypeCtxt -> Type -> TcM ()
checkUserTypeError UserTypeCtxt
ctxt Type
ty
| TySynCtxt {} <- UserTypeCtxt
ctxt
= () -> TcM ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
| Just Type
msg <- Type -> Maybe Type
deepUserTypeError_maybe Type
ty
= do { env0 <- ZonkM TidyEnv -> TcM TidyEnv
forall a. ZonkM a -> TcM a
liftZonkM ZonkM TidyEnv
tcInitTidyEnv
; let (env1, tidy_msg) = tidyOpenTypeX env0 msg
; failWithTcM (env1, TcRnUserTypeError tidy_msg) }
| Bool
otherwise
= () -> TcM ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
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
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"::" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
ty))
; rankn_flag <- Extension -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. Extension -> TcRnIf gbl lcl Bool
xoptM Extension
LangExt.RankNTypes
; impred_flag <- xoptM LangExt.ImpredicativeTypes
; let gen_rank :: Rank -> Rank
gen_rank Rank
r | Bool
rankn_flag = Rank
ArbitraryRank
| Bool
otherwise = Rank
r
rank1 = Rank -> Rank
gen_rank Rank
r1
rank0 = Rank -> Rank
gen_rank Rank
MonoTypeRankZero
r1 = Bool -> Rank -> Rank
LimitedRank Bool
True Rank
MonoTypeRankZero
rank
= case UserTypeCtxt
ctxt of
UserTypeCtxt
DefaultDeclCtxt-> Rank
MustBeMonoType
UserTypeCtxt
PatSigCtxt -> Rank
rank0
RuleSigCtxt {} -> Rank
rank1
TySynCtxt Name
_ -> Rank
rank0
ExprSigCtxt {} -> Rank
rank1
UserTypeCtxt
KindSigCtxt -> Rank
rank1
StandaloneKindSigCtxt{} -> Rank
rank1
UserTypeCtxt
TypeAppCtxt | Bool
impred_flag -> Rank
ArbitraryRank
| Bool
otherwise -> Rank
MonoTypeTyConArg
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. HasCallStack => String -> a
panic String
"checkValidType"
; env <- liftZonkM $ tcInitOpenTidyEnv (tyCoVarsOfTypeList ty)
; expand <- initialExpandMode
; let 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 }
; checkNoErrs $
do { check_type ve ty
; checkUserTypeError ctxt ty
; traceTc "done ct" (ppr ty) }
; checkAmbiguity ctxt ty
; traceTc "checkValidType done" (ppr ty <+> text "::" <+> ppr (typeKind ty)) }
checkValidMonoType :: Type -> TcM ()
checkValidMonoType :: Type -> TcM ()
checkValidMonoType Type
ty
= do { env <- ZonkM TidyEnv -> TcM TidyEnv
forall a. ZonkM a -> TcM a
liftZonkM (ZonkM TidyEnv -> TcM TidyEnv) -> ZonkM TidyEnv -> TcM TidyEnv
forall a b. (a -> b) -> a -> b
$ [Var] -> ZonkM TidyEnv
tcInitOpenTidyEnv (Type -> [Var]
tyCoVarsOfTypeList Type
ty)
; expand <- initialExpandMode
; let 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 }
; check_type ve ty }
checkTySynRhs :: UserTypeCtxt -> TcType -> TcM ()
checkTySynRhs :: UserTypeCtxt -> Type -> TcM ()
checkTySynRhs UserTypeCtxt
ctxt Type
ty
| Type -> Bool
returnsConstraintKind Type
actual_kind
= do { ck <- Extension -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. Extension -> TcRnIf gbl lcl Bool
xoptM Extension
LangExt.ConstraintKinds
; if ck
then when (isConstraintLikeKind actual_kind)
(do { dflags <- getDynFlags
; expand <- initialExpandMode
; check_pred_ty emptyTidyEnv dflags ctxt expand ty })
else addErrTcM ( emptyTidyEnv
, TcRnIllegalConstraintSynonymOfKind (tidyType emptyTidyEnv actual_kind)
) }
| Bool
otherwise
= () -> TcM ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
where
actual_kind :: Type
actual_kind = HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
ty
checkEscapingKind :: Type -> TcM ()
checkEscapingKind :: Type -> TcM ()
checkEscapingKind Type
poly_ty
| ([Var]
tvs, Type
tau) <- Type -> ([Var], Type)
splitForAllTyVars Type
poly_ty
, let tau_kind :: Type
tau_kind = HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
tau
, Maybe Type
Nothing <- [Var] -> Type -> Maybe Type
occCheckExpand [Var]
tvs Type
tau_kind
= TcRnMessage -> TcM ()
forall a. TcRnMessage -> TcM a
failWithTc (TcRnMessage -> TcM ()) -> TcRnMessage -> TcM ()
forall a b. (a -> b) -> a -> b
$ Type -> Type -> TcRnMessage
TcRnForAllEscapeError Type
poly_ty Type
tau_kind
| Bool
otherwise
= () -> TcM ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
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
$c== :: TypeOrKindCtxt -> TypeOrKindCtxt -> Bool
== :: TypeOrKindCtxt -> TypeOrKindCtxt -> Bool
$c/= :: TypeOrKindCtxt -> TypeOrKindCtxt -> Bool
/= :: TypeOrKindCtxt -> TypeOrKindCtxt -> Bool
Eq
instance Outputable TypeOrKindCtxt where
ppr :: TypeOrKindCtxt -> SDoc
ppr TypeOrKindCtxt
ctxt = String -> SDoc
forall doc. IsLine doc => String -> doc
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
forall doc. IsLine doc => String -> doc
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
liberal_flag <- Extension -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. Extension -> TcRnIf gbl lcl Bool
xoptM Extension
LangExt.LiberalTypeSynonyms
pure $ if liberal_flag then Expand else 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
forall doc. IsLine doc => String -> doc
text String
"ValidityEnv")
Int
2 ([SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"ve_tidy_env" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TidyEnv -> SDoc
forall a. Outputable a => a -> SDoc
ppr TidyEnv
env
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"ve_ctxt" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> UserTypeCtxt -> SDoc
pprUserTypeCtxt UserTypeCtxt
ctxt
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"ve_rank" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Rank -> SDoc
forall a. Outputable a => a -> SDoc
ppr Rank
rank
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"ve_expand" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> 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 Var
_)
= () -> TcM ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
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
= UnboxedTupleOrSum -> ValidityEnv -> Type -> [Type] -> TcM ()
check_ubx_tuple_or_sum UnboxedTupleOrSum
UnboxedTupleType ValidityEnv
ve Type
ty [Type]
tys
| TyCon -> Bool
isUnboxedSumTyCon TyCon
tc
= UnboxedTupleOrSum -> ValidityEnv -> Type -> [Type] -> TcM ()
check_ubx_tuple_or_sum UnboxedTupleOrSum
UnboxedSumType ValidityEnv
ve Type
ty [Type]
tys
| Bool
otherwise
= do {
Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (TyCon -> Bool
isKindTyCon TyCon
tc Bool -> Bool -> Bool
|| TyCon -> Bool
isTypeDataTyCon TyCon
tc) (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$
ValidityEnv -> Type -> TcM ()
checkDataKinds ValidityEnv
ve Type
ty
; (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
ve ty :: Type
ty@(LitTy {}) =
ValidityEnv -> Type -> TcM ()
checkDataKinds ValidityEnv
ve Type
ty
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_rank :: ValidityEnv -> Rank
ve_rank = Rank
rank, ve_expand :: ValidityEnv -> ExpandMode
ve_expand = ExpandMode
expand }) Type
ty
| Bool -> Bool
not ([TyVarBinder] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TyVarBinder]
tvbs Bool -> Bool -> Bool
&& [Type] -> Bool
forall a. [a] -> 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
forall doc. IsDoc doc => doc -> doc -> doc
$$ Rank -> SDoc
forall a. Outputable a => a -> SDoc
ppr Rank
rank)
; Bool -> (TidyEnv, TcRnMessage) -> TcM ()
checkTcM (Rank -> Bool
forAllAllowed Rank
rank) ((TidyEnv, TcRnMessage) -> TcM ())
-> (TidyEnv, TcRnMessage) -> TcM ()
forall a b. (a -> b) -> a -> b
$
let (TidyEnv
env1, Type
tidy_ty) = TidyEnv -> Type -> (TidyEnv, Type)
tidyOpenTypeX TidyEnv
env Type
ty
in (TidyEnv
env1, Rank -> Type -> TcRnMessage
TcRnForAllRankErr Rank
rank Type
tidy_ty)
; ValidityEnv -> [Type] -> Type -> TcM ()
checkConstraintsOK ValidityEnv
ve [Type]
theta Type
ty
; ValidityEnv -> [TyVarBinder] -> Type -> TcM ()
checkVdqOK ValidityEnv
ve [TyVarBinder]
tvbs 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 = env'}) 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]
_) = TidyEnv -> [TyVarBinder] -> (TidyEnv, [TyVarBinder])
forall vis.
TidyEnv -> [VarBndr Var vis] -> (TidyEnv, [VarBndr Var vis])
tidyForAllTyBinders 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 FunTyFlag
_ Type
mult Type
arg_ty Type
res_ty)
= do { Bool -> (TidyEnv, TcRnMessage) -> TcM ()
failIfTcM (Bool -> Bool
not (UserTypeCtxt -> Bool
linearityAllowed UserTypeCtxt
ctxt) Bool -> Bool -> Bool
&& Bool -> Bool
not (Type -> Bool
isManyTy Type
mult))
(TidyEnv
env, Type -> TcRnMessage
TcRnLinearFuncInKind (TidyEnv -> Type -> Type
tidyType TidyEnv
env Type
ty))
; ValidityEnv -> Type -> TcM ()
check_type (ValidityEnv
ve{ve_rank = arg_rank}) Type
arg_ty
; ValidityEnv -> Type -> TcM ()
check_type (ValidityEnv
ve{ve_rank = res_rank}) Type
res_ty }
where
(Rank
arg_rank, Rank
res_rank) = Rank -> (Rank, Rank)
funArgResRank Rank
rank
check_type ValidityEnv
_ ty :: Type
ty@(ForAllTy {}) = 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_type ValidityEnv
_ ty :: Type
ty@(CoercionTy {}) = 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 a b.
IOEnv (Env TcGblEnv TcLclEnv) a
-> IOEnv (Env TcGblEnv TcLclEnv) b
-> IOEnv (Env TcGblEnv TcLclEnv) b
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
= TcRnMessage -> TcM ()
forall a. TcRnMessage -> TcM a
failWithTc (TyCon -> [Type] -> TcRnMessage
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 = 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
= Bool -> SDoc -> TcM () -> TcM ()
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (TyCon -> Bool
isTypeSynonymTyCon TyCon
tc) (TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tc) (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$
case Type -> Maybe Type
coreView Type
ty of
Just Type
ty' -> let err_ctxt :: SDoc
err_ctxt = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"In the expansion of type synonym"
SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> 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 = 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_or_sum :: UnboxedTupleOrSum -> ValidityEnv -> KindOrType -> [KindOrType] -> TcM ()
check_ubx_tuple_or_sum :: UnboxedTupleOrSum -> ValidityEnv -> Type -> [Type] -> TcM ()
check_ubx_tuple_or_sum UnboxedTupleOrSum
tup_or_sum (ve :: ValidityEnv
ve@ValidityEnv{ve_tidy_env :: ValidityEnv -> TidyEnv
ve_tidy_env = TidyEnv
env}) Type
ty [Type]
tys
= do { ub_thing_allowed <- Extension -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. Extension -> TcRnIf gbl lcl Bool
xoptM (Extension -> TcRnIf TcGblEnv TcLclEnv Bool)
-> Extension -> TcRnIf TcGblEnv TcLclEnv Bool
forall a b. (a -> b) -> a -> b
$ UnboxedTupleOrSum -> Extension
unboxedTupleOrSumExtension UnboxedTupleOrSum
tup_or_sum
; checkTcM ub_thing_allowed
(env, TcRnUnboxedTupleOrSumTypeFuncArg tup_or_sum (tidyType env ty))
; checkDataKinds ve ty
; impred <- xoptM LangExt.ImpredicativeTypes
; let rank' = if Bool
impred then Rank
ArbitraryRank else Rank
MonoTypeTyConArg
; mapM_ (check_type (ve{ve_rank = rank'})) tys }
check_arg_type
:: Bool
-> ValidityEnv -> KindOrType -> TcM ()
check_arg_type :: Bool -> ValidityEnv -> Type -> TcM ()
check_arg_type Bool
_ ValidityEnv
_ (CoercionTy {}) = () -> TcM ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
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 { impred <- Extension -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. Extension -> TcRnIf gbl lcl Bool
xoptM Extension
LangExt.ImpredicativeTypes
; let rank' = case Rank
rank of
Rank
_ | Bool
type_syn -> Rank
MonoTypeSynArg
Rank
MustBeMonoType -> Rank
MustBeMonoType
Rank
_other | Bool
impred -> Rank
ArbitraryRank
| Bool
otherwise -> Rank
MonoTypeTyConArg
ctxt' :: UserTypeCtxt
ctxt'
| GhciCtxt Bool
_ <- UserTypeCtxt
ctxt = Bool -> UserTypeCtxt
GhciCtxt Bool
False
| Bool
otherwise = UserTypeCtxt
ctxt
; check_type (ve{ve_ctxt = ctxt', ve_rank = rank'}) ty }
checkConstraintsOK :: ValidityEnv -> ThetaType -> Type -> TcM ()
checkConstraintsOK :: ValidityEnv -> [Type] -> Type -> TcM ()
checkConstraintsOK ValidityEnv
ve [Type]
theta Type
ty
| [Type] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
theta = () -> TcM ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
| UserTypeCtxt -> Bool
allConstraintsAllowed (ValidityEnv -> UserTypeCtxt
ve_ctxt ValidityEnv
ve) = () -> TcM ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
| Bool
otherwise
= (TidyEnv, TcRnMessage) -> TcM ()
forall a. (TidyEnv, TcRnMessage) -> TcM a
failWithTcM (TidyEnv
env, Type -> TcRnMessage
TcRnConstraintInKind (TidyEnv -> Type -> Type
tidyType TidyEnv
env Type
ty))
where env :: TidyEnv
env = ValidityEnv -> TidyEnv
ve_tidy_env ValidityEnv
ve
checkVdqOK :: ValidityEnv -> [TyVarBinder] -> Type -> TcM ()
checkVdqOK :: ValidityEnv -> [TyVarBinder] -> Type -> TcM ()
checkVdqOK ValidityEnv
ve [TyVarBinder]
tvbs Type
ty = do
required_type_arguments <- Extension -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. Extension -> TcRnIf gbl lcl Bool
xoptM Extension
LangExt.RequiredTypeArguments
checkTcM (required_type_arguments || vdqAllowed ctxt || no_vdq)
(env, TcRnVDQInTermType (Just (tidyType env ty)))
where
no_vdq :: Bool
no_vdq = (TyVarBinder -> Bool) -> [TyVarBinder] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (ForAllTyFlag -> Bool
isInvisibleForAllTyFlag (ForAllTyFlag -> Bool)
-> (TyVarBinder -> ForAllTyFlag) -> TyVarBinder -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarBinder -> ForAllTyFlag
forall tv argf. VarBndr tv argf -> argf
binderFlag) [TyVarBinder]
tvbs
ValidityEnv{ve_tidy_env :: ValidityEnv -> TidyEnv
ve_tidy_env = TidyEnv
env, ve_ctxt :: ValidityEnv -> UserTypeCtxt
ve_ctxt = UserTypeCtxt
ctxt} = ValidityEnv
ve
checkDataKinds :: ValidityEnv -> Type -> TcM ()
checkDataKinds :: ValidityEnv -> Type -> TcM ()
checkDataKinds (ValidityEnv{ ve_ctxt :: ValidityEnv -> UserTypeCtxt
ve_ctxt = UserTypeCtxt
ctxt, ve_tidy_env :: ValidityEnv -> TidyEnv
ve_tidy_env = TidyEnv
env }) Type
ty = do
data_kinds <- Extension -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. Extension -> TcRnIf gbl lcl Bool
xoptM Extension
LangExt.DataKinds
diagnosticTcM
(not (data_kinds || typeLevelUserTypeCtxt ctxt)) $
(env, TcRnDataKindsError KindLevel (Right (tidyType env ty)))
checkValidTheta :: UserTypeCtxt -> ThetaType -> TcM ()
checkValidTheta :: UserTypeCtxt -> [Type] -> TcM ()
checkValidTheta UserTypeCtxt
ctxt [Type]
theta
= (TidyEnv -> ZonkM (TidyEnv, SDoc)) -> TcM () -> TcM ()
forall a. (TidyEnv -> ZonkM (TidyEnv, SDoc)) -> TcM a -> TcM a
addErrCtxtM (UserTypeCtxt -> [Type] -> TidyEnv -> ZonkM (TidyEnv, SDoc)
checkThetaCtxt UserTypeCtxt
ctxt [Type]
theta) (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$
do { env <- ZonkM TidyEnv -> TcM TidyEnv
forall a. ZonkM a -> TcM a
liftZonkM (ZonkM TidyEnv -> TcM TidyEnv) -> ZonkM TidyEnv -> TcM TidyEnv
forall a b. (a -> b) -> a -> b
$ [Var] -> ZonkM TidyEnv
tcInitOpenTidyEnv ([Type] -> [Var]
tyCoVarsOfTypesList [Type]
theta)
; expand <- initialExpandMode
; check_valid_theta env ctxt expand 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 a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
check_valid_theta TidyEnv
env UserTypeCtxt
ctxt ExpandMode
expand [Type]
theta
= do { dflags <- IOEnv (Env TcGblEnv TcLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
; traceTc "check_valid_theta" (ppr theta)
; mapM_ (check_pred_ty env dflags ctxt expand) 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
MonoTypeConstraint
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
coreView 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 [Var]
_ [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
Pred
_ -> () -> TcM ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
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
forall doc. IsLine doc => String -> doc
text String
"In the quantified constraint" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> 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 a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Pred
_ -> (TidyEnv, TcRnMessage) -> TcM ()
forall a. (TidyEnv, TcRnMessage) -> TcM a
failWithTcM (TidyEnv
env, Type -> TcRnMessage
TcRnBadQuantPredHead (TidyEnv -> Type -> Type
tidyType 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, TcRnMessage) -> TcM ()
checkTcM (Bool
under_syn Bool -> Bool -> Bool
|| Extension -> DynFlags -> Bool
xopt Extension
LangExt.ConstraintKinds DynFlags
dflags)
(TidyEnv
env, Type -> TcRnMessage
TcRnIllegalTupleConstraint (TidyEnv -> Type -> Type
tidyType 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_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
isEqualityClass Class
cls
=
() -> TcM ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
| Class -> Bool
isIPClass Class
cls
= do { TcM ()
check_arity
; Bool -> (TidyEnv, TcRnMessage) -> TcM ()
checkTcM (UserTypeCtxt -> Bool
okIPCtxt UserTypeCtxt
ctxt) (TidyEnv
env, Type -> TcRnMessage
TcRnIllegalImplicitParam (TidyEnv -> Type -> Type
tidyType 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, TcRnMessage) -> TcM ()
checkTcM Bool
arg_tys_ok (TidyEnv
env, Type -> TcRnMessage
TcRnNonTypeVarArgInConstraint (TidyEnv -> Type -> Type
tidyType TidyEnv
env Type
pred)) }
where
check_arity :: TcM ()
check_arity = Bool -> TcRnMessage -> TcM ()
checkTc ([Type]
tys [Type] -> Int -> Bool
forall a. [a] -> Int -> Bool
`lengthIs` Class -> Int
classArity Class
cls)
(TyCon -> [Type] -> TcRnMessage
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 a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
| Extension -> DynFlags -> Bool
xopt Extension
LangExt.MonoLocalBinds DynFlags
dflags
= () -> TcM ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
| DataTyCtxt {} <- UserTypeCtxt
ctxt
= () -> TcM ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
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 a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
| Bool
otherwise
= do { result <- DynFlags
-> Bool -> Class -> [Type] -> Maybe CtLoc -> TcM ClsInstResult
matchGlobalInst DynFlags
dflags Bool
False Class
cls [Type]
tys Maybe CtLoc
forall a. Maybe a
Nothing
; case result of
OneInst { cir_what :: ClsInstResult -> InstanceWhat
cir_what = InstanceWhat
what }
-> TcRnMessage -> TcM ()
addDiagnosticTc (Type -> InstanceWhat -> TcRnMessage
TcRnSimplifiableConstraint Type
pred InstanceWhat
what)
ClsInstResult
_ -> () -> TcM ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return () }
where
pred :: Type
pred = TidyEnv -> Type -> Type
tidyType TidyEnv
env (Class -> [Type] -> Type
mkClassPred Class
cls [Type]
tys)
okIPCtxt :: UserTypeCtxt -> Bool
okIPCtxt :: UserTypeCtxt -> Bool
okIPCtxt (FunSigCtxt {}) = Bool
True
okIPCtxt (InfSigCtxt {}) = Bool
True
okIPCtxt (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 -> ZonkM (TidyEnv, SDoc)
checkThetaCtxt :: UserTypeCtxt -> [Type] -> TidyEnv -> ZonkM (TidyEnv, SDoc)
checkThetaCtxt UserTypeCtxt
ctxt [Type]
theta TidyEnv
env
= (TidyEnv, SDoc) -> ZonkM (TidyEnv, SDoc)
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return ( TidyEnv
env
, [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"In the context:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Type] -> SDoc
pprTheta (TidyEnv -> [Type] -> [Type]
tidyTypes TidyEnv
env [Type]
theta)
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"While checking" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> UserTypeCtxt -> SDoc
pprUserTypeCtxt UserTypeCtxt
ctxt ] )
tyConArityErr :: TyCon -> [TcType] -> TcRnMessage
tyConArityErr :: TyCon -> [Type] -> TcRnMessage
tyConArityErr TyCon
tc [Type]
tks
= TyThing -> Int -> Int -> TcRnMessage
TcRnArityMismatch (TyCon -> TyThing
ATyCon 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 Var TyConBndrVis -> Bool)
-> [VarBndr Var TyConBndrVis] -> Int
forall a. (a -> Bool) -> [a] -> Int
count VarBndr Var TyConBndrVis -> Bool
forall tv. VarBndr tv TyConBndrVis -> Bool
isVisibleTyConBinder (TyCon -> [VarBndr Var TyConBndrVis]
tyConBinders TyCon
tc)
tc_type_args :: Int
tc_type_args = [Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
vis_tks
checkValidInstHead :: UserTypeCtxt -> Class -> [Type] -> TcM ()
checkValidInstHead :: UserTypeCtxt -> Class -> [Type] -> TcM ()
checkValidInstHead UserTypeCtxt
ctxt Class
clas [Type]
cls_args
= do { dflags <- IOEnv (Env TcGblEnv TcLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
; hsc_src <- tcHscSource
; check_special_inst_head dflags hsc_src ctxt clas cls_args
; checkValidTypePats (classTyCon clas) cls_args
}
check_special_inst_head :: DynFlags -> HscSource -> UserTypeCtxt
-> Class -> [Type] -> TcM ()
check_special_inst_head :: DynFlags -> HscSource -> UserTypeCtxt -> Class -> [Type] -> TcM ()
check_special_inst_head DynFlags
dflags HscSource
hs_src UserTypeCtxt
ctxt Class
clas [Type]
cls_args
| Class -> Bool
isAbstractClass Class
clas
, HscSource
hs_src HscSource -> HscSource -> Bool
forall a. Eq a => a -> a -> Bool
== HscSource
HsSrcFile
= IllegalClassInstanceReason -> TcM ()
fail_with_inst_err (IllegalClassInstanceReason -> TcM ())
-> IllegalClassInstanceReason -> TcM ()
forall a b. (a -> b) -> a -> b
$ IllegalInstanceHeadReason -> IllegalClassInstanceReason
IllegalInstanceHead
(IllegalInstanceHeadReason -> IllegalClassInstanceReason)
-> IllegalInstanceHeadReason -> IllegalClassInstanceReason
forall a b. (a -> b) -> a -> b
$ Class -> IllegalInstanceHeadReason
InstHeadAbstractClass Class
clas
| Name
clas_nm Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
typeableClassName
, Bool -> Bool
not (HscSource
hs_src HscSource -> HscSource -> Bool
forall a. Eq a => a -> a -> Bool
== HscSource
HsigFile)
, Bool
hand_written_bindings
= IllegalClassInstanceReason -> TcM ()
fail_with_inst_err (IllegalClassInstanceReason -> TcM ())
-> IllegalClassInstanceReason -> TcM ()
forall a b. (a -> b) -> a -> b
$ Class -> Bool -> IllegalClassInstanceReason
IllegalSpecialClassInstance Class
clas Bool
False
| Name
clas_nm Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [ Name
knownNatClassName, Name
knownSymbolClassName
, Name
knownCharClassName, Name
dataToTagClassName ]
, (Bool -> Bool
not (HscSource
hs_src HscSource -> HscSource -> Bool
forall a. Eq a => a -> a -> Bool
== HscSource
HsigFile) Bool -> Bool -> Bool
&& Bool
hand_written_bindings) Bool -> Bool -> Bool
|| Bool
derived_instance
= IllegalClassInstanceReason -> TcM ()
fail_with_inst_err (IllegalClassInstanceReason -> TcM ())
-> IllegalClassInstanceReason -> TcM ()
forall a b. (a -> b) -> a -> b
$ Class -> Bool -> IllegalClassInstanceReason
IllegalSpecialClassInstance Class
clas Bool
False
| Name
clas_nm Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem`
[ Name
heqTyConName, Name
eqTyConName, Name
coercibleTyConName
, Name
withDictClassName, Name
unsatisfiableClassName ]
, Bool -> Bool
not Bool
quantified_constraint
= IllegalClassInstanceReason -> TcM ()
fail_with_inst_err (IllegalClassInstanceReason -> TcM ())
-> IllegalClassInstanceReason -> TcM ()
forall a b. (a -> b) -> a -> b
$ Class -> Bool -> IllegalClassInstanceReason
IllegalSpecialClassInstance Class
clas Bool
False
| Name
clas_nm Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
genericClassNames
, Bool
hand_written_bindings
= do { Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (DynFlags -> Bool
safeLanguageOn DynFlags
dflags) (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$
IllegalClassInstanceReason -> TcM ()
fail_with_inst_err (IllegalClassInstanceReason -> TcM ())
-> IllegalClassInstanceReason -> TcM ()
forall a b. (a -> b) -> a -> b
$ Class -> Bool -> IllegalClassInstanceReason
IllegalSpecialClassInstance Class
clas Bool
True
; Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (DynFlags -> Bool
safeInferOn DynFlags
dflags) (Messages TcRnMessage -> TcM ()
recordUnsafeInfer Messages TcRnMessage
forall e. Messages e
emptyMessages) }
| Name
clas_nm Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
hasFieldClassName
, Bool -> Bool
not Bool
quantified_constraint
= Class -> [Type] -> TcM ()
checkHasFieldInst Class
clas [Type]
cls_args
| Class -> Bool
isCTupleClass Class
clas
= do
this_mod <- (TcGblEnv -> Module)
-> IOEnv (Env TcGblEnv TcLclEnv) TcGblEnv
-> IOEnv (Env TcGblEnv TcLclEnv) Module
forall a b.
(a -> b)
-> IOEnv (Env TcGblEnv TcLclEnv) a
-> IOEnv (Env TcGblEnv TcLclEnv) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TcGblEnv -> Module
tcg_mod IOEnv (Env TcGblEnv TcLclEnv) TcGblEnv
forall gbl lcl. TcRnIf gbl lcl gbl
getGblEnv
when (this_mod /= gHC_CLASSES) (failWithTc (TcRnTupleConstraintInst clas))
| Bool
check_h98_arg_shape
, Just IllegalInstanceHeadReason
illegal_head <- Maybe IllegalInstanceHeadReason
mb_ty_args_type
= IllegalClassInstanceReason -> TcM ()
fail_with_inst_err (IllegalClassInstanceReason -> TcM ())
-> IllegalClassInstanceReason -> TcM ()
forall a b. (a -> b) -> a -> b
$ IllegalInstanceHeadReason -> IllegalClassInstanceReason
IllegalInstanceHead IllegalInstanceHeadReason
illegal_head
| Bool
otherwise
= () -> TcM ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
where
fail_with_inst_err :: IllegalClassInstanceReason -> TcM ()
fail_with_inst_err IllegalClassInstanceReason
err =
TcRnMessage -> TcM ()
forall a. TcRnMessage -> TcM a
failWithTc (TcRnMessage -> TcM ()) -> TcRnMessage -> TcM ()
forall a b. (a -> b) -> a -> b
$ IllegalInstanceReason -> TcRnMessage
TcRnIllegalInstance
(IllegalInstanceReason -> TcRnMessage)
-> IllegalInstanceReason -> TcRnMessage
forall a b. (a -> b) -> a -> b
$ TypedThing -> IllegalClassInstanceReason -> IllegalInstanceReason
IllegalClassInstance
(Type -> TypedThing
TypeThing (Type -> TypedThing) -> Type -> TypedThing
forall a b. (a -> b) -> a -> b
$ Class -> [Type] -> Type
mkClassPred Class
clas [Type]
cls_args)
(IllegalClassInstanceReason -> IllegalInstanceReason)
-> IllegalClassInstanceReason -> IllegalInstanceReason
forall a b. (a -> b) -> a -> b
$ IllegalClassInstanceReason
err
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
standalone -> Bool -> Bool
not Bool
standalone
UserTypeCtxt
SpecInstCtxt -> Bool
False
UserTypeCtxt
DerivClauseCtxt -> Bool
False
UserTypeCtxt
SigmaCtxt -> Bool
False
UserTypeCtxt
_ -> Bool
True
derived_instance :: Bool
derived_instance
= case UserTypeCtxt
ctxt of
InstDeclCtxt Bool
standalone -> Bool
standalone
UserTypeCtxt
DerivClauseCtxt -> Bool
True
UserTypeCtxt
_ -> Bool
False
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
mb_ty_args_type :: Maybe IllegalInstanceHeadReason
mb_ty_args_type
| 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)
= IllegalInstanceHeadReason -> Maybe IllegalInstanceHeadReason
forall a. a -> Maybe a
Just IllegalInstanceHeadReason
InstHeadTySynArgs
| 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)
= IllegalInstanceHeadReason -> Maybe IllegalInstanceHeadReason
forall a. a -> Maybe a
Just IllegalInstanceHeadReason
InstHeadNonTyVarArgs
| [Type] -> Int
forall a. [a] -> 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 a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
ty_args)
= IllegalInstanceHeadReason -> Maybe IllegalInstanceHeadReason
forall a. a -> Maybe a
Just IllegalInstanceHeadReason
InstHeadMultiParam
| Bool
otherwise
= Maybe IllegalInstanceHeadReason
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) <- HasDebugCallStack => 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 -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
fUNTyConKey
, Type
ManyTy : [Type]
tys_t <- [Type]
tys'
= [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 = [Var] -> [Type] -> Bool
forall a b. [a] -> [b] -> Bool
equalLength [Var]
tvs [Type]
tys Bool -> Bool -> Bool
&& [Var] -> Bool
forall a. Eq a => [a] -> Bool
hasNoDups [Var]
tvs
where
tvs :: [Var]
tvs = (Type -> Maybe Var) -> [Type] -> [Var]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Type -> Maybe Var
getTyVar_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 FunTyFlag
_ Type
w Type
t1 Type
t2) = Type
ty { ft_mult = dropCasts w, ft_arg = dropCasts t1, ft_res = dropCasts 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
checkHasFieldInst :: Class -> [Type] -> TcM ()
checkHasFieldInst :: Class -> [Type] -> TcM ()
checkHasFieldInst Class
cls tys :: [Type]
tys@[Type
_k_ty, Type
_r_rep, Type
_a_rep, Type
lbl_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 -> IllegalHasFieldInstance -> TcM ()
add_err IllegalHasFieldInstance
IllegalHasFieldInstanceNotATyCon
Just (TyCon
tc, [Type]
_)
| TyCon -> Bool
isFamilyTyCon TyCon
tc
-> IllegalHasFieldInstance -> TcM ()
add_err IllegalHasFieldInstance
IllegalHasFieldInstanceFamilyTyCon
| Bool
otherwise -> case Type -> Maybe FastString
isStrLitTy Type
lbl_ty of
Just FastString
lbl
| let lbl_str :: FieldLabelString
lbl_str = FastString -> FieldLabelString
FieldLabelString FastString
lbl
, Maybe FieldLabel -> Bool
forall a. Maybe a -> Bool
isJust (FieldLabelString -> TyCon -> Maybe FieldLabel
lookupTyConFieldLabel FieldLabelString
lbl_str TyCon
tc)
-> IllegalHasFieldInstance -> TcM ()
add_err (IllegalHasFieldInstance -> TcM ())
-> IllegalHasFieldInstance -> TcM ()
forall a b. (a -> b) -> a -> b
$ TyCon -> FieldLabelString -> IllegalHasFieldInstance
IllegalHasFieldInstanceTyConHasField TyCon
tc FieldLabelString
lbl_str
| Bool
otherwise
-> () -> TcM ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Maybe FastString
Nothing
| [FieldLabel] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (TyCon -> [FieldLabel]
tyConFieldLabels TyCon
tc)
Bool -> Bool -> Bool
|| Type -> Type -> Bool
typesAreApart (HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
lbl_ty) Type
typeSymbolKind
-> () -> TcM ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
| Bool
otherwise
-> IllegalHasFieldInstance -> TcM ()
add_err (IllegalHasFieldInstance -> TcM ())
-> IllegalHasFieldInstance -> TcM ()
forall a b. (a -> b) -> a -> b
$ TyCon -> Type -> IllegalHasFieldInstance
IllegalHasFieldInstanceTyConHasFields TyCon
tc Type
lbl_ty
where
add_err :: IllegalHasFieldInstance -> TcM ()
add_err IllegalHasFieldInstance
err = TcRnMessage -> TcM ()
addErrTc (TcRnMessage -> TcM ()) -> TcRnMessage -> TcM ()
forall a b. (a -> b) -> a -> b
$ IllegalInstanceReason -> TcRnMessage
TcRnIllegalInstance
(IllegalInstanceReason -> TcRnMessage)
-> IllegalInstanceReason -> TcRnMessage
forall a b. (a -> b) -> a -> b
$ TypedThing -> IllegalClassInstanceReason -> IllegalInstanceReason
IllegalClassInstance
(Type -> TypedThing
TypeThing (Type -> TypedThing) -> Type -> TypedThing
forall a b. (a -> b) -> a -> b
$ Class -> [Type] -> Type
mkClassPred Class
cls [Type]
tys)
(IllegalClassInstanceReason -> IllegalInstanceReason)
-> IllegalClassInstanceReason -> IllegalInstanceReason
forall a b. (a -> b) -> a -> b
$ IllegalHasFieldInstance -> IllegalClassInstanceReason
IllegalHasFieldInstance IllegalHasFieldInstance
err
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 :: PatersonSize -> PredType -> Bool
validDerivPred :: PatersonSize -> Type -> Bool
validDerivPred PatersonSize
head_size Type
pred
= case Type -> Pred
classifyPredType Type
pred of
EqPred {} -> Bool
False
ForAllPred {} -> Bool
False
ClassPred Class
cls [Type]
tys -> PatersonSize -> Bool
check_size (Class -> [Type] -> PatersonSize
pSizeClassPred Class
cls [Type]
tys)
Bool -> Bool -> Bool
&& UniqSet TyCon -> Bool
forall a. UniqSet a -> Bool
isEmptyUniqSet ([Type] -> UniqSet TyCon
tyConsOfTypes [Type]
visible_tys)
where
visible_tys :: [Type]
visible_tys = TyCon -> [Type] -> [Type]
filterOutInvisibleTypes (Class -> TyCon
classTyCon Class
cls) [Type]
tys
IrredPred {} -> PatersonSize -> Bool
check_size (Type -> PatersonSize
pSizeType Type
pred)
Bool -> Bool -> Bool
&& UniqSet TyCon -> Bool
forall a. UniqSet a -> Bool
isEmptyUniqSet (Type -> UniqSet TyCon
tyConsOfType Type
pred)
where
check_size :: PatersonSize -> Bool
check_size PatersonSize
pred_size = Maybe PatersonCondFailure -> Bool
forall a. Maybe a -> Bool
isNothing (PatersonSize
pred_size PatersonSize -> PatersonSize -> Maybe PatersonCondFailure
`ltPatersonSize` PatersonSize
head_size)
checkValidInstance :: UserTypeCtxt -> LHsSigType GhcRn -> Type -> TcM ()
checkValidInstance :: UserTypeCtxt -> LHsSigType GhcRn -> Type -> TcM ()
checkValidInstance UserTypeCtxt
ctxt LHsSigType GhcRn
hs_type Type
ty = case Type
tau of
TyConApp TyCon
tc [Type]
inst_tys
| Just Class
clas <- TyCon -> Maybe Class
tyConClass_maybe TyCon
tc
-> do
{ EpAnn AnnListItem -> TcM () -> TcM ()
forall ann a. EpAnn ann -> TcRn a -> TcRn a
setSrcSpanA 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)
; env0 <- ZonkM TidyEnv -> TcM TidyEnv
forall a. ZonkM a -> TcM a
liftZonkM (ZonkM TidyEnv -> TcM TidyEnv) -> ZonkM TidyEnv -> TcM TidyEnv
forall a b. (a -> b) -> a -> b
$ ZonkM TidyEnv
tcInitTidyEnv
; expand <- initialExpandMode
; check_valid_theta env0 ctxt expand theta
; undecidable_ok <- xoptM LangExt.UndecidableInstances
; if undecidable_ok
then checkAmbiguity ctxt ty
else checkInstTermination theta tau
; traceTc "cvi 2" (ppr ty)
; case checkInstCoverage undecidable_ok clas theta inst_tys of
Validity' CoverageProblem
IsValid
-> () -> TcM ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
NotValid CoverageProblem
coverageInstErr
-> TcRnMessage -> TcM ()
addErrTc (TcRnMessage -> TcM ()) -> TcRnMessage -> TcM ()
forall a b. (a -> b) -> a -> b
$ IllegalClassInstanceReason -> TcRnMessage
mk_err
(IllegalClassInstanceReason -> TcRnMessage)
-> IllegalClassInstanceReason -> TcRnMessage
forall a b. (a -> b) -> a -> b
$ Class -> CoverageProblem -> IllegalClassInstanceReason
IllegalInstanceFailsCoverageCondition Class
clas CoverageProblem
coverageInstErr
; traceTc "End checkValidInstance }" empty }
| Bool
otherwise
-> TcRnMessage -> TcM ()
forall a. TcRnMessage -> TcM a
failWithTc (TcRnMessage -> TcM ()) -> TcRnMessage -> TcM ()
forall a b. (a -> b) -> a -> b
$ IllegalClassInstanceReason -> TcRnMessage
mk_err (IllegalClassInstanceReason -> TcRnMessage)
-> IllegalClassInstanceReason -> TcRnMessage
forall a b. (a -> b) -> a -> b
$ IllegalInstanceHeadReason -> IllegalClassInstanceReason
IllegalInstanceHead
(IllegalInstanceHeadReason -> IllegalClassInstanceReason)
-> IllegalInstanceHeadReason -> IllegalClassInstanceReason
forall a b. (a -> b) -> a -> b
$ Maybe TyCon -> IllegalInstanceHeadReason
InstHeadNonClass (TyCon -> Maybe TyCon
forall a. a -> Maybe a
Just TyCon
tc)
Type
_ -> TcRnMessage -> TcM ()
forall a. TcRnMessage -> TcM a
failWithTc (TcRnMessage -> TcM ()) -> TcRnMessage -> TcM ()
forall a b. (a -> b) -> a -> b
$ IllegalClassInstanceReason -> TcRnMessage
mk_err (IllegalClassInstanceReason -> TcRnMessage)
-> IllegalClassInstanceReason -> TcRnMessage
forall a b. (a -> b) -> a -> b
$ IllegalInstanceHeadReason -> IllegalClassInstanceReason
IllegalInstanceHead
(IllegalInstanceHeadReason -> IllegalClassInstanceReason)
-> IllegalInstanceHeadReason -> IllegalClassInstanceReason
forall a b. (a -> b) -> a -> b
$ Maybe TyCon -> IllegalInstanceHeadReason
InstHeadNonClass Maybe TyCon
forall a. Maybe a
Nothing
where
([Type]
theta, Type
tau) = Type -> ([Type], Type)
splitInstTyForValidity Type
ty
mk_err :: IllegalClassInstanceReason -> TcRnMessage
mk_err IllegalClassInstanceReason
err = IllegalInstanceReason -> TcRnMessage
TcRnIllegalInstance
(IllegalInstanceReason -> TcRnMessage)
-> IllegalInstanceReason -> TcRnMessage
forall a b. (a -> b) -> a -> b
$ TypedThing -> IllegalClassInstanceReason -> IllegalInstanceReason
IllegalClassInstance (Type -> TypedThing
TypeThing Type
tau) IllegalClassInstanceReason
err
head_loc :: EpAnn AnnListItem
head_loc = GenLocated (EpAnn AnnListItem) (HsType GhcRn) -> 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)
splitInstTyForValidity :: Type -> (ThetaType, Type)
splitInstTyForValidity :: Type -> ([Type], Type)
splitInstTyForValidity = [Type] -> Type -> ([Type], Type)
split_context [] (Type -> ([Type], Type))
-> (Type -> Type) -> Type -> ([Type], Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Type
drop_foralls
where
drop_foralls :: Type -> Type
drop_foralls :: Type -> Type
drop_foralls (ForAllTy (Bndr Var
_tv ForAllTyFlag
argf) Type
ty)
| ForAllTyFlag -> Bool
isInvisibleForAllTyFlag ForAllTyFlag
argf = Type -> Type
drop_foralls Type
ty
drop_foralls Type
ty = Type
ty
split_context :: ThetaType -> Type -> (ThetaType, Type)
split_context :: [Type] -> Type -> ([Type], Type)
split_context [Type]
preds (FunTy { ft_af :: Type -> FunTyFlag
ft_af = FunTyFlag
af, ft_arg :: Type -> Type
ft_arg = Type
pred, ft_res :: Type -> Type
ft_res = Type
tau })
| FunTyFlag -> Bool
isInvisibleFunArg FunTyFlag
af = [Type] -> Type -> ([Type], Type)
split_context (Type
predType -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[Type]
preds) Type
tau
split_context [Type]
preds Type
ty = ([Type] -> [Type]
forall a. [a] -> [a]
reverse [Type]
preds, Type
ty)
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_size :: PatersonSize
head_size = Type -> PatersonSize
pSizeType 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 a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
IrredPred {} -> PatersonSize -> TcM ()
check2 (VarSet -> Type -> PatersonSize
pSizeTypeX VarSet
foralld_tvs Type
pred)
ClassPred Class
cls [Type]
tys
| Class -> Bool
isCTupleClass Class
cls
-> VarSet -> [Type] -> TcM ()
check_preds VarSet
foralld_tvs [Type]
tys
| Bool
otherwise
-> PatersonSize -> TcM ()
check2 (VarSet -> Class -> [Type] -> PatersonSize
pSizeClassPredX VarSet
foralld_tvs Class
cls [Type]
tys)
ForAllPred [Var]
tvs [Type]
_ Type
head_pred'
-> VarSet -> Type -> TcM ()
check (VarSet
foralld_tvs VarSet -> [Var] -> VarSet
`extendVarSetList` [Var]
tvs) Type
head_pred'
where
check2 :: PatersonSize -> TcM ()
check2 PatersonSize
pred_size
= case PatersonSize
pred_size PatersonSize -> PatersonSize -> Maybe PatersonCondFailure
`ltPatersonSize` PatersonSize
head_size of
Just PatersonCondFailure
pc_failure -> TcRnMessage -> TcM ()
forall a. TcRnMessage -> TcM a
failWithTc (TcRnMessage -> TcM ()) -> TcRnMessage -> TcM ()
forall a b. (a -> b) -> a -> b
$ PatersonCondFailure
-> PatersonCondFailureContext -> Type -> Type -> TcRnMessage
TcRnPatersonCondFailure PatersonCondFailure
pc_failure PatersonCondFailureContext
InInstanceDecl Type
pred Type
head_pred
Maybe PatersonCondFailure
Nothing -> () -> TcM ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
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 { let dia :: TcRnMessage
dia = TyCon -> CoAxBranch -> TcRnMessage
TcRnInaccessibleCoAxBranch TyCon
fam_tc CoAxBranch
cur_branch
; SrcSpan -> TcRnMessage -> TcM ()
addDiagnosticAt (CoAxBranch -> SrcSpan
coAxBranchSpan CoAxBranch
cur_branch) TcRnMessage
dia
; [CoAxBranch] -> IOEnv (Env TcGblEnv TcLclEnv) [CoAxBranch]
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
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 a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
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 { dflags <- IOEnv (Env TcGblEnv TcLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
; let 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 b a. (b -> a -> b) -> b -> [a] -> b
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
; reportConflictingInjectivityErrs fam_tc conflicts cur_branch
; reportInjectivityErrors dflags ax cur_branch inj }
| Bool
otherwise
= () -> TcM ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
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_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 -> [Type] -> Type -> TcM ()
checkValidTyFamEqn TyCon
fam_tc [Type]
typats Type
rhs
checkValidTyFamEqn :: TyCon
-> [Type]
-> Type
-> TcM ()
checkValidTyFamEqn :: TyCon -> [Type] -> Type -> TcM ()
checkValidTyFamEqn TyCon
fam_tc [Type]
typats Type
rhs
= do { TyCon -> [Type] -> TcM ()
checkValidTypePats TyCon
fam_tc [Type]
typats
; 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 a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
Type
spec_arg:[Type]
_ ->
TcRnMessage -> TcM ()
addErr (Type -> TcRnMessage
TcRnOversaturatedVisibleKindArg Type
spec_arg)
; Type -> TcM ()
checkValidMonoType Type
rhs
; undecidable_ok <- Extension -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. Extension -> TcRnIf gbl lcl Bool
xoptM Extension
LangExt.UndecidableInstances
; traceTc "checkVTFE" (ppr fam_tc $$ ppr rhs $$ ppr (tcTyFamInsts rhs))
; unless undecidable_ok $
mapM_ addErrTc (checkFamInstRhs fam_tc typats (tcTyFamInsts rhs)) }
checkValidAssocTyFamDeflt :: TyCon
-> [Type]
-> TcM ()
checkValidAssocTyFamDeflt :: TyCon -> [Type] -> TcM ()
checkValidAssocTyFamDeflt TyCon
fam_tc [Type]
pats =
do { cpt_tvs <- (Type -> ForAllTyFlag -> IOEnv (Env TcGblEnv TcLclEnv) Var)
-> [Type] -> [ForAllTyFlag] -> IOEnv (Env TcGblEnv TcLclEnv) [Var]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Type -> ForAllTyFlag -> IOEnv (Env TcGblEnv TcLclEnv) Var
extract_tv [Type]
pats [ForAllTyFlag]
pats_vis
; check_all_distinct_tvs $ zip cpt_tvs pats_vis }
where
pats_vis :: [ForAllTyFlag]
pats_vis :: [ForAllTyFlag]
pats_vis = TyCon -> [Type] -> [ForAllTyFlag]
tyConForAllTyFlags TyCon
fam_tc [Type]
pats
extract_tv :: Type
-> ForAllTyFlag
-> TcM TyVar
extract_tv :: Type -> ForAllTyFlag -> IOEnv (Env TcGblEnv TcLclEnv) Var
extract_tv Type
pat ForAllTyFlag
pat_vis =
case Type -> Maybe Var
getTyVar_maybe Type
pat of
Just Var
tv -> Var -> IOEnv (Env TcGblEnv TcLclEnv) Var
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Var
tv
Maybe Var
Nothing -> TcRnMessage -> IOEnv (Env TcGblEnv TcLclEnv) Var
forall a. TcRnMessage -> TcM a
failWithTc (TcRnMessage -> IOEnv (Env TcGblEnv TcLclEnv) Var)
-> TcRnMessage -> IOEnv (Env TcGblEnv TcLclEnv) Var
forall a b. (a -> b) -> a -> b
$ IllegalInstanceReason -> TcRnMessage
TcRnIllegalInstance
(IllegalInstanceReason -> TcRnMessage)
-> IllegalInstanceReason -> TcRnMessage
forall a b. (a -> b) -> a -> b
$ IllegalFamilyInstanceReason -> IllegalInstanceReason
IllegalFamilyInstance
(IllegalFamilyInstanceReason -> IllegalInstanceReason)
-> IllegalFamilyInstanceReason -> IllegalInstanceReason
forall a b. (a -> b) -> a -> b
$ InvalidAssoc -> IllegalFamilyInstanceReason
InvalidAssoc (InvalidAssoc -> IllegalFamilyInstanceReason)
-> InvalidAssoc -> IllegalFamilyInstanceReason
forall a b. (a -> b) -> a -> b
$ InvalidAssocDefault -> InvalidAssoc
InvalidAssocDefault
(InvalidAssocDefault -> InvalidAssoc)
-> InvalidAssocDefault -> InvalidAssoc
forall a b. (a -> b) -> a -> b
$ TyCon -> [Type] -> AssocDefaultBadArgs -> InvalidAssocDefault
AssocDefaultBadArgs TyCon
fam_tc [Type]
pats
(AssocDefaultBadArgs -> InvalidAssocDefault)
-> AssocDefaultBadArgs -> InvalidAssocDefault
forall a b. (a -> b) -> a -> b
$ (Type, ForAllTyFlag) -> AssocDefaultBadArgs
AssocDefaultNonTyVarArg (Type
pat, ForAllTyFlag
pat_vis)
check_all_distinct_tvs ::
[(TyVar, ForAllTyFlag)]
-> TcM ()
check_all_distinct_tvs :: [(Var, ForAllTyFlag)] -> TcM ()
check_all_distinct_tvs [(Var, ForAllTyFlag)]
cpt_tvs_vis =
let dups :: [NonEmpty (Var, ForAllTyFlag)]
dups = ((Var, ForAllTyFlag) -> (Var, ForAllTyFlag) -> Bool)
-> [(Var, ForAllTyFlag)] -> [NonEmpty (Var, ForAllTyFlag)]
forall a. (a -> a -> Bool) -> [a] -> [NonEmpty a]
findDupsEq (Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Var -> Var -> Bool)
-> ((Var, ForAllTyFlag) -> Var)
-> (Var, ForAllTyFlag)
-> (Var, ForAllTyFlag)
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Var, ForAllTyFlag) -> Var
forall a b. (a, b) -> a
fst) [(Var, ForAllTyFlag)]
cpt_tvs_vis in
(NonEmpty (Var, ForAllTyFlag)
-> IOEnv (Env TcGblEnv TcLclEnv) (ZonkAny 0))
-> [NonEmpty (Var, ForAllTyFlag)] -> TcM ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_
(\NonEmpty (Var, ForAllTyFlag)
d -> TcRnMessage -> IOEnv (Env TcGblEnv TcLclEnv) (ZonkAny 0)
forall a. TcRnMessage -> TcM a
failWithTc (TcRnMessage -> IOEnv (Env TcGblEnv TcLclEnv) (ZonkAny 0))
-> TcRnMessage -> IOEnv (Env TcGblEnv TcLclEnv) (ZonkAny 0)
forall a b. (a -> b) -> a -> b
$ IllegalInstanceReason -> TcRnMessage
TcRnIllegalInstance
(IllegalInstanceReason -> TcRnMessage)
-> IllegalInstanceReason -> TcRnMessage
forall a b. (a -> b) -> a -> b
$ IllegalFamilyInstanceReason -> IllegalInstanceReason
IllegalFamilyInstance
(IllegalFamilyInstanceReason -> IllegalInstanceReason)
-> IllegalFamilyInstanceReason -> IllegalInstanceReason
forall a b. (a -> b) -> a -> b
$ InvalidAssoc -> IllegalFamilyInstanceReason
InvalidAssoc (InvalidAssoc -> IllegalFamilyInstanceReason)
-> InvalidAssoc -> IllegalFamilyInstanceReason
forall a b. (a -> b) -> a -> b
$ InvalidAssocDefault -> InvalidAssoc
InvalidAssocDefault
(InvalidAssocDefault -> InvalidAssoc)
-> InvalidAssocDefault -> InvalidAssoc
forall a b. (a -> b) -> a -> b
$ TyCon -> [Type] -> AssocDefaultBadArgs -> InvalidAssocDefault
AssocDefaultBadArgs TyCon
fam_tc [Type]
pats
(AssocDefaultBadArgs -> InvalidAssocDefault)
-> AssocDefaultBadArgs -> InvalidAssocDefault
forall a b. (a -> b) -> a -> b
$ NonEmpty (Var, ForAllTyFlag) -> AssocDefaultBadArgs
AssocDefaultDuplicateTyVars NonEmpty (Var, ForAllTyFlag)
d)
[NonEmpty (Var, ForAllTyFlag)]
dups
checkFamInstRhs :: TyCon -> [Type]
-> [(TyCon, [Type])]
-> [TcRnMessage]
checkFamInstRhs :: TyCon -> [Type] -> [(TyCon, [Type])] -> [TcRnMessage]
checkFamInstRhs TyCon
lhs_tc [Type]
lhs_tys [(TyCon, [Type])]
famInsts
= ((TyCon, [Type]) -> Maybe TcRnMessage)
-> [(TyCon, [Type])] -> [TcRnMessage]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (TyCon, [Type]) -> Maybe TcRnMessage
check [(TyCon, [Type])]
famInsts
where
lhs_size :: PatersonSize
lhs_size = [Type] -> PatersonSize
pSizeTypes [Type]
lhs_tys
check :: (TyCon, [Type]) -> Maybe TcRnMessage
check (TyCon
tc, [Type]
tys)
| Bool -> Bool
not (TyCon -> Bool
isStuckTypeFamily TyCon
tc)
, Just PatersonCondFailure
pc_failure <- [Type] -> PatersonSize
pSizeTypes [Type]
tys PatersonSize -> PatersonSize -> Maybe PatersonCondFailure
`ltPatersonSize` PatersonSize
lhs_size
= TcRnMessage -> Maybe TcRnMessage
forall a. a -> Maybe a
Just (TcRnMessage -> Maybe TcRnMessage)
-> TcRnMessage -> Maybe TcRnMessage
forall a b. (a -> b) -> a -> b
$ PatersonCondFailure
-> PatersonCondFailureContext -> Type -> Type -> TcRnMessage
TcRnPatersonCondFailure PatersonCondFailure
pc_failure PatersonCondFailureContext
InTyFamEquation (TyCon -> [Type] -> Type
TyConApp TyCon
lhs_tc [Type]
lhs_tys) (TyCon -> [Type] -> Type
TyConApp TyCon
tc [Type]
tys)
| Bool
otherwise
= Maybe TcRnMessage
forall a. Maybe a
Nothing
checkTyFamEqnValidityInfo :: TyCon -> TyFamEqnValidityInfo -> TcM ()
checkTyFamEqnValidityInfo :: TyCon -> TyFamEqnValidityInfo -> TcM ()
checkTyFamEqnValidityInfo TyCon
fam_tc = \ case
TyFamEqnValidityInfo
NoVI -> () -> TcM ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
VI { vi_loc :: TyFamEqnValidityInfo -> SrcSpan
vi_loc = SrcSpan
loc
, vi_qtvs :: TyFamEqnValidityInfo -> [Var]
vi_qtvs = [Var]
qtvs
, vi_non_user_tvs :: TyFamEqnValidityInfo -> VarSet
vi_non_user_tvs = VarSet
non_user_tvs
, vi_pats :: TyFamEqnValidityInfo -> [Type]
vi_pats = [Type]
pats
, vi_rhs :: TyFamEqnValidityInfo -> Type
vi_rhs = Type
rhs } ->
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 -> [Var] -> VarSet -> [Type] -> Type -> TcM ()
checkFamPatBinders TyCon
fam_tc [Var]
qtvs VarSet
non_user_tvs [Type]
pats Type
rhs
checkFamPatBinders :: TyCon
-> [TcTyVar]
-> TyVarSet
-> [TcType]
-> TcType
-> TcM ()
checkFamPatBinders :: TyCon -> [Var] -> VarSet -> [Type] -> Type -> TcM ()
checkFamPatBinders TyCon
fam_tc [Var]
qtvs VarSet
non_user_tvs [Type]
pats Type
rhs
= do { String -> SDoc -> TcM ()
traceTc String
"checkFamPatBinders" (SDoc -> TcM ()) -> SDoc -> TcM ()
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
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
forall doc. IsLine doc => String -> doc
text String
"rhs:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
rhs
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"qtvs:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Var] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Var]
qtvs
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"rhs_fvs:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> VarSet -> SDoc
forall a. Outputable a => a -> SDoc
ppr (FV -> VarSet
fvVarSet FV
rhs_fvs)
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"cpt_tvs:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> VarSet -> SDoc
forall a. Outputable a => a -> SDoc
ppr VarSet
cpt_tvs
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"inj_cpt_tvs:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> VarSet -> SDoc
forall a. Outputable a => a -> SDoc
ppr VarSet
inj_cpt_tvs
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"bad_rhs_tvs:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Var] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Var]
bad_rhs_tvs
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"bad_qtvs:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Var] -> SDoc
forall a. Outputable a => a -> SDoc
ppr ((InvalidFamInstQTv -> Var) -> [InvalidFamInstQTv] -> [Var]
forall a b. (a -> b) -> [a] -> [b]
map InvalidFamInstQTv -> Var
ifiqtv [InvalidFamInstQTv]
bad_qtvs) ]
; (NonEmpty Name -> IllegalFamilyInstanceReason) -> [Name] -> TcM ()
forall {a}.
NamedThing a =>
(NonEmpty a -> IllegalFamilyInstanceReason) -> [a] -> TcM ()
check_tvs (Maybe (TyCon, [Type], VarSet)
-> NonEmpty Name -> IllegalFamilyInstanceReason
FamInstRHSOutOfScopeTyVars ((TyCon, [Type], VarSet) -> Maybe (TyCon, [Type], VarSet)
forall a. a -> Maybe a
Just (TyCon
fam_tc, [Type]
pats, VarSet
dodgy_tvs)))
((Var -> Name) -> [Var] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map Var -> Name
tyVarName [Var]
bad_rhs_tvs)
; (NonEmpty InvalidFamInstQTv -> IllegalFamilyInstanceReason)
-> [InvalidFamInstQTv] -> TcM ()
forall {a}.
NamedThing a =>
(NonEmpty a -> IllegalFamilyInstanceReason) -> [a] -> TcM ()
check_tvs NonEmpty InvalidFamInstQTv -> IllegalFamilyInstanceReason
FamInstLHSUnusedBoundTyVars [InvalidFamInstQTv]
bad_qtvs
}
where
rhs_fvs :: FV
rhs_fvs = Type -> FV
tyCoFVsOfType Type
rhs
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
bad_qtvs :: [InvalidFamInstQTv]
bad_qtvs = (Var -> Maybe InvalidFamInstQTv) -> [Var] -> [InvalidFamInstQTv]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Var -> Maybe InvalidFamInstQTv
bad_qtv_maybe [Var]
qtvs
bad_qtv_maybe :: Var -> Maybe InvalidFamInstQTv
bad_qtv_maybe Var
qtv
| Bool
not_bound_in_pats
= let reason :: InvalidFamInstQTvReason
reason
| Bool
dodgy
= InvalidFamInstQTvReason
InvalidFamInstQTvDodgy
| Bool
used_in_rhs
= InvalidFamInstQTvReason
InvalidFamInstQTvNotBoundInPats
| Bool
otherwise
= InvalidFamInstQTvReason
InvalidFamInstQTvNotUsedInRHS
in InvalidFamInstQTv -> Maybe InvalidFamInstQTv
forall a. a -> Maybe a
Just (InvalidFamInstQTv -> Maybe InvalidFamInstQTv)
-> InvalidFamInstQTv -> Maybe InvalidFamInstQTv
forall a b. (a -> b) -> a -> b
$ InvalidFamInstQTv
{ ifiqtv :: Var
ifiqtv = Var
qtv
, ifiqtv_user_written :: Bool
ifiqtv_user_written = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Var
qtv Var -> VarSet -> Bool
`elemVarSet` VarSet
non_user_tvs
, ifiqtv_reason :: InvalidFamInstQTvReason
ifiqtv_reason = InvalidFamInstQTvReason
reason
}
| Bool
otherwise
= Maybe InvalidFamInstQTv
forall a. Maybe a
Nothing
where
not_bound_in_pats :: Bool
not_bound_in_pats = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Var
qtv Var -> VarSet -> Bool
`elemVarSet` VarSet
inj_cpt_tvs
dodgy :: Bool
dodgy = Bool
not_bound_in_pats Bool -> Bool -> Bool
&& Var
qtv Var -> VarSet -> Bool
`elemVarSet` VarSet
cpt_tvs
used_in_rhs :: Bool
used_in_rhs = Var
qtv Var -> VarSet -> Bool
`elemVarSet` FV -> VarSet
fvVarSet FV
rhs_fvs
bad_rhs_tvs :: [Var]
bad_rhs_tvs = (Var -> Bool) -> [Var] -> [Var]
forall a. (a -> Bool) -> [a] -> [a]
filterOut ((Var -> VarSet -> Bool
`elemVarSet` VarSet
inj_cpt_tvs) (Var -> Bool) -> (Var -> Bool) -> Var -> Bool
forall (f :: * -> *). Applicative f => f Bool -> f Bool -> f Bool
<||> (Var -> [Var] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Var]
qtvs)) (FV -> [Var]
fvVarList FV
rhs_fvs)
dodgy_tvs :: VarSet
dodgy_tvs = VarSet
cpt_tvs VarSet -> VarSet -> VarSet
`minusVarSet` VarSet
inj_cpt_tvs
check_tvs :: (NonEmpty a -> IllegalFamilyInstanceReason) -> [a] -> TcM ()
check_tvs NonEmpty a -> IllegalFamilyInstanceReason
mk_err [a]
tvs
= Maybe (NonEmpty a) -> (NonEmpty a -> TcM ()) -> TcM ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ ([a] -> Maybe (NonEmpty a)
forall a. [a] -> Maybe (NonEmpty a)
NE.nonEmpty [a]
tvs) ((NonEmpty a -> TcM ()) -> TcM ())
-> (NonEmpty a -> TcM ()) -> TcM ()
forall a b. (a -> b) -> a -> b
$ \ ne_tvs :: NonEmpty a
ne_tvs@(a
tv0 :| [a]
_) ->
SrcSpan -> TcRnMessage -> TcM ()
addErrAt (a -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
getSrcSpan a
tv0) (TcRnMessage -> TcM ()) -> TcRnMessage -> TcM ()
forall a b. (a -> b) -> a -> b
$
IllegalInstanceReason -> TcRnMessage
TcRnIllegalInstance (IllegalInstanceReason -> TcRnMessage)
-> IllegalInstanceReason -> TcRnMessage
forall a b. (a -> b) -> a -> b
$ IllegalFamilyInstanceReason -> IllegalInstanceReason
IllegalFamilyInstance (IllegalFamilyInstanceReason -> IllegalInstanceReason)
-> IllegalFamilyInstanceReason -> IllegalInstanceReason
forall a b. (a -> b) -> a -> b
$
NonEmpty a -> IllegalFamilyInstanceReason
mk_err NonEmpty a
ne_tvs
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 a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
((Bool
tf_is_invis_arg, TyCon
tf_tc, [Type]
tf_args):[(Bool, TyCon, [Type])]
_) ->
TcRnMessage -> TcM ()
forall a. TcRnMessage -> TcM a
failWithTc (TcRnMessage -> TcM ()) -> TcRnMessage -> TcM ()
forall a b. (a -> b) -> a -> b
$ IllegalInstanceReason -> TcRnMessage
TcRnIllegalInstance (IllegalInstanceReason -> TcRnMessage)
-> IllegalInstanceReason -> TcRnMessage
forall a b. (a -> b) -> a -> b
$
Type -> Bool -> TyCon -> [Type] -> IllegalInstanceReason
IllegalFamilyApplicationInInstance Type
inst_ty
Bool
tf_is_invis_arg TyCon
tf_tc [Type]
tf_args }
where
inst_ty :: Type
inst_ty = TyCon -> [Type] -> Type
mkTyConApp TyCon
tc [Type]
pat_ty_args
checkConsistentFamInst :: AssocInstInfo
-> TyCon
-> CoAxBranch
-> TcM ()
checkConsistentFamInst :: AssocInstInfo -> TyCon -> CoAxBranch -> TcM ()
checkConsistentFamInst AssocInstInfo
NotAssociated TyCon
_ CoAxBranch
_
= () -> TcM ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkConsistentFamInst (InClsInst { ai_class :: AssocInstInfo -> Class
ai_class = Class
clas
, ai_tyvars :: AssocInstInfo -> [Var]
ai_tyvars = [Var]
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
forall doc. IsDoc doc => [doc] -> doc
vcat [ [Var] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Var]
inst_tvs
, [(Type, Type, ForAllTyFlag)] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [(Type, Type, ForAllTyFlag)]
arg_triples
, VarEnv Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr VarEnv Type
mini_env
, [Var] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Var]
ax_tvs
, [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
ax_arg_tys
, [(Type, Type, ForAllTyFlag)] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [(Type, Type, ForAllTyFlag)]
arg_triples ])
; Bool -> TcRnMessage -> 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) (TcRnMessage -> TcM ()) -> TcRnMessage -> TcM ()
forall a b. (a -> b) -> a -> b
$
IllegalInstanceReason -> TcRnMessage
TcRnIllegalInstance (IllegalInstanceReason -> TcRnMessage)
-> IllegalInstanceReason -> TcRnMessage
forall a b. (a -> b) -> a -> b
$ IllegalFamilyInstanceReason -> IllegalInstanceReason
IllegalFamilyInstance (IllegalFamilyInstanceReason -> IllegalInstanceReason)
-> IllegalFamilyInstanceReason -> IllegalInstanceReason
forall a b. (a -> b) -> a -> b
$
InvalidAssoc -> IllegalFamilyInstanceReason
InvalidAssoc (InvalidAssoc -> IllegalFamilyInstanceReason)
-> InvalidAssoc -> IllegalFamilyInstanceReason
forall a b. (a -> b) -> a -> b
$ InvalidAssocInstance -> InvalidAssoc
InvalidAssocInstance (InvalidAssocInstance -> InvalidAssoc)
-> InvalidAssocInstance -> InvalidAssoc
forall a b. (a -> b) -> a -> b
$
Class -> TyCon -> InvalidAssocInstance
AssocNotInThisClass Class
clas TyCon
fam_tc
; [(Type, Type, ForAllTyFlag)] -> TcM ()
check_match [(Type, Type, ForAllTyFlag)]
arg_triples
}
where
([Var]
ax_tvs, [Type]
ax_arg_tys, Type
_) = CoAxBranch -> ([Var], [Type], Type)
etaExpandCoAxBranch CoAxBranch
branch
arg_triples :: [(Type,Type, ForAllTyFlag)]
arg_triples :: [(Type, Type, ForAllTyFlag)]
arg_triples = [ (Type
cls_arg_ty, Type
at_arg_ty, ForAllTyFlag
vis)
| (Var
fam_tc_tv, ForAllTyFlag
vis, Type
at_arg_ty)
<- [Var] -> [ForAllTyFlag] -> [Type] -> [(Var, ForAllTyFlag, Type)]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 (TyCon -> [Var]
tyConTyVars TyCon
fam_tc)
(TyCon -> [Type] -> [ForAllTyFlag]
tyConForAllTyFlags TyCon
fam_tc [Type]
ax_arg_tys)
[Type]
ax_arg_tys
, Just Type
cls_arg_ty <- [VarEnv Type -> Var -> Maybe Type
forall a. VarEnv a -> Var -> Maybe a
lookupVarEnv VarEnv Type
mini_env Var
fam_tc_tv] ]
(TidyEnv
tidy_env1, [Var]
_) = TidyEnv -> [Var] -> (TidyEnv, [Var])
tidyVarBndrs TidyEnv
emptyTidyEnv [Var]
inst_tvs
(TidyEnv
tidy_env2, [Var]
_) = TidyEnv -> [Var] -> (TidyEnv, [Var])
tidyCoAxBndrsForUser TidyEnv
tidy_env1 ([Var]
ax_tvs [Var] -> [Var] -> [Var]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Var]
inst_tvs)
mk_wildcard :: Var -> Type
mk_wildcard Var
at_tv = Var -> Type
mkTyVarTy (Name -> Type -> Var
mkTyVar Name
tv_name (Var -> Type
tyVarKind Var
at_tv))
tv_name :: Name
tv_name = Unique -> OccName -> SrcSpan -> Name
mkInternalName (Int -> Unique
mkAlphaTyVarUnique Int
1) (FastString -> OccName
mkTyVarOccFS (String -> FastString
fsLit String
"_")) SrcSpan
noSrcSpan
check_match :: [(Type,Type,ForAllTyFlag)] -> TcM ()
check_match :: [(Type, Type, ForAllTyFlag)] -> TcM ()
check_match [(Type, Type, ForAllTyFlag)]
triples = Subst -> Subst -> [(Type, Type, ForAllTyFlag)] -> TcM ()
go Subst
emptySubst Subst
emptySubst [(Type, Type, ForAllTyFlag)]
triples
go :: Subst -> Subst -> [(Type, Type, ForAllTyFlag)] -> TcM ()
go Subst
_ Subst
_ [] = () -> TcM ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
go Subst
lr_subst Subst
rl_subst ((Type
ty1,Type
ty2,ForAllTyFlag
vis):[(Type, Type, ForAllTyFlag)]
triples)
| Just Subst
lr_subst1 <- BindFun -> Subst -> Type -> Type -> Maybe Subst
tcMatchTyX_BM BindFun
bind_me Subst
lr_subst Type
ty1 Type
ty2
, Just Subst
rl_subst1 <- BindFun -> Subst -> Type -> Type -> Maybe Subst
tcMatchTyX_BM BindFun
bind_me Subst
rl_subst Type
ty2 Type
ty1
= Subst -> Subst -> [(Type, Type, ForAllTyFlag)] -> TcM ()
go Subst
lr_subst1 Subst
rl_subst1 [(Type, Type, ForAllTyFlag)]
triples
| Bool
otherwise
= TcRnMessage -> TcM ()
addErrTc (TcRnMessage -> TcM ()) -> TcRnMessage -> TcM ()
forall a b. (a -> b) -> a -> b
$ IllegalInstanceReason -> TcRnMessage
TcRnIllegalInstance (IllegalInstanceReason -> TcRnMessage)
-> IllegalInstanceReason -> TcRnMessage
forall a b. (a -> b) -> a -> b
$ IllegalFamilyInstanceReason -> IllegalInstanceReason
IllegalFamilyInstance
(IllegalFamilyInstanceReason -> IllegalInstanceReason)
-> IllegalFamilyInstanceReason -> IllegalInstanceReason
forall a b. (a -> b) -> a -> b
$ InvalidAssoc -> IllegalFamilyInstanceReason
InvalidAssoc (InvalidAssoc -> IllegalFamilyInstanceReason)
-> InvalidAssoc -> IllegalFamilyInstanceReason
forall a b. (a -> b) -> a -> b
$ InvalidAssocInstance -> InvalidAssoc
InvalidAssocInstance
(InvalidAssocInstance -> InvalidAssoc)
-> InvalidAssocInstance -> InvalidAssoc
forall a b. (a -> b) -> a -> b
$ ForAllTyFlag -> TyCon -> [Type] -> [Type] -> InvalidAssocInstance
AssocTyVarsDontMatch ForAllTyFlag
vis TyCon
fam_tc [Type]
exp_tys [Type]
act_tys
exp_tys :: [Type]
exp_tys =
[ case VarEnv Type -> Var -> Maybe Type
forall a. VarEnv a -> Var -> Maybe a
lookupVarEnv VarEnv Type
mini_env Var
at_tv of
Just Type
cls_arg_ty -> TidyEnv -> Type -> Type
tidyType TidyEnv
tidy_env2 Type
cls_arg_ty
Maybe Type
Nothing -> Var -> Type
mk_wildcard Var
at_tv
| Var
at_tv <- TyCon -> [Var]
tyConTyVars TyCon
fam_tc ]
act_tys :: [Type]
act_tys = TidyEnv -> [Type] -> [Type]
tidyTypes TidyEnv
tidy_env2 [Type]
ax_arg_tys
no_bind_set :: VarSet
no_bind_set = [Var] -> VarSet
mkVarSet [Var]
inst_tvs
bind_me :: BindFun
bind_me Var
tv Type
_ty | Var
tv Var -> 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
=
TcRnMessage -> TcM ()
addErr (TcRnMessage -> TcM ()) -> TcRnMessage -> TcM ()
forall a b. (a -> b) -> a -> b
$ TyCon -> TcRnMessage
TcRnBadTyConTelescope TyCon
tc
| Bool
otherwise
= () -> TcM ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
where
tcbs :: [VarBndr Var TyConBndrVis]
tcbs = TyCon -> [VarBndr Var TyConBndrVis]
tyConBinders TyCon
tc
(VarSet
_, Bool
bad_scope) = ((VarSet, Bool) -> VarBndr Var TyConBndrVis -> (VarSet, Bool))
-> (VarSet, Bool) -> [VarBndr Var TyConBndrVis] -> (VarSet, Bool)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (VarSet, Bool) -> VarBndr Var TyConBndrVis -> (VarSet, Bool)
add_one (VarSet
emptyVarSet, Bool
False) [VarBndr Var TyConBndrVis]
tcbs
add_one :: TelescopeAcc -> TyConBinder -> TelescopeAcc
add_one :: (VarSet, Bool) -> VarBndr Var TyConBndrVis -> (VarSet, Bool)
add_one (VarSet
bound, Bool
bad_scope) VarBndr Var TyConBndrVis
tcb
= ( VarSet
bound VarSet -> Var -> VarSet
`extendVarSet` Var
tv
, Bool
bad_scope Bool -> Bool -> Bool
|| Bool -> Bool
not (VarSet -> Bool
isEmptyVarSet (VarSet
fkvs VarSet -> VarSet -> VarSet
`minusVarSet` VarSet
bound)) )
where
tv :: Var
tv = VarBndr Var TyConBndrVis -> Var
forall tv argf. VarBndr tv argf -> tv
binderVar VarBndr Var TyConBndrVis
tcb
fkvs :: VarSet
fkvs = Type -> VarSet
tyCoVarsOfType (Var -> Type
tyVarKind Var
tv)