{-# LANGUAGE DerivingStrategies #-}
{-# 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,
checkValidTyFamEqn, checkValidAssocTyFamDeflt, checkConsistentFamInst,
arityErr,
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(..), InstanceWhat(..), 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.Utils.Env ( tcInitTidyEnv, tcInitOpenTidyEnv )
import GHC.Tc.Instance.FunDeps
import GHC.Tc.Instance.Family
import GHC.Builtin.Types
import GHC.Builtin.Names
import GHC.Builtin.Uniques ( mkAlphaTyVarUnique )
import GHC.Core.Type
import GHC.Core.Unify ( tcMatchTyX_BM, BindFlag(..) )
import GHC.Core.Coercion
import GHC.Core.Coercion.Axiom
import GHC.Core.Class
import GHC.Core.TyCon
import GHC.Core.Predicate
import GHC.Core.TyCo.FVs
import GHC.Core.TyCo.Rep
import GHC.Core.TyCo.Ppr
import GHC.Core.FamInstEnv ( isDominatedBy, injectiveBranches
, InjectivityCheckResult(..) )
import GHC.Iface.Type ( pprIfaceType, pprIfaceTypeApp )
import GHC.CoreToIface ( toIfaceTyCon, toIfaceTcArgs, toIfaceType )
import GHC.Hs
import GHC.Driver.Session
import qualified GHC.LanguageExtensions as LangExt
import GHC.Types.Error
import GHC.Types.Basic ( UnboxedTupleOrSum(..), unboxedTupleOrSumExtension )
import GHC.Types.Name
import GHC.Types.Var.Env
import GHC.Types.Var.Set
import GHC.Types.Var ( VarBndr(..), isInvisibleFunArg, mkTyVar )
import GHC.Types.SrcLoc
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
checkAmbiguity :: UserTypeCtxt -> Type -> TcM ()
checkAmbiguity :: UserTypeCtxt -> Type -> TcM ()
checkAmbiguity UserTypeCtxt
ctxt Type
ty
| UserTypeCtxt -> Bool
wantAmbiguityCheck UserTypeCtxt
ctxt
= do { String -> SDoc -> TcM ()
traceTc String
"Ambiguity check for" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty)
; Bool
allow_ambiguous <- Extension -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. Extension -> TcRnIf gbl lcl Bool
xoptM Extension
LangExt.AllowAmbiguousTypes
; (HsWrapper
_wrap, WantedConstraints
wanted) <- SDoc
-> TcM (HsWrapper, WantedConstraints)
-> TcM (HsWrapper, WantedConstraints)
forall a. SDoc -> TcM a -> TcM a
addErrCtxt (Bool -> SDoc
mk_msg Bool
allow_ambiguous) (TcM (HsWrapper, WantedConstraints)
-> TcM (HsWrapper, WantedConstraints))
-> TcM (HsWrapper, WantedConstraints)
-> TcM (HsWrapper, WantedConstraints)
forall a b. (a -> b) -> a -> b
$
TcM HsWrapper -> TcM (HsWrapper, WantedConstraints)
forall a. TcM a -> TcM (a, WantedConstraints)
captureConstraints (TcM HsWrapper -> TcM (HsWrapper, WantedConstraints))
-> TcM HsWrapper -> TcM (HsWrapper, WantedConstraints)
forall a b. (a -> b) -> a -> b
$
UserTypeCtxt -> Type -> Type -> TcM HsWrapper
tcSubTypeAmbiguity UserTypeCtxt
ctxt Type
ty Type
ty
; Type -> WantedConstraints -> TcM ()
simplifyAmbiguityCheck Type
ty WantedConstraints
wanted
; String -> SDoc -> TcM ()
traceTc String
"Done ambiguity check for" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty) }
| Bool
otherwise
= () -> TcM ()
forall 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 ()
| Bool
otherwise
= Type -> TcM ()
check Type
ty
where
check :: Type -> TcM ()
check Type
ty
| Just Type
msg <- Type -> Maybe Type
userTypeError_maybe Type
ty = Type -> TcM ()
fail_with Type
msg
| Just (Var
_,Type
t1) <- Type -> Maybe (Var, Type)
splitForAllTyCoVar_maybe Type
ty = Type -> TcM ()
check Type
t1
| let (Type
_,[Type]
tys) = Type -> (Type, [Type])
splitAppTys Type
ty = (Type -> TcM ()) -> [Type] -> TcM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Type -> TcM ()
check [Type]
tys
fail_with :: Type -> TcM ()
fail_with :: Type -> TcM ()
fail_with Type
msg = do { TidyEnv
env0 <- TcM TidyEnv
tcInitTidyEnv
; let (TidyEnv
env1, Type
tidy_msg) = TidyEnv -> Type -> (TidyEnv, Type)
tidyOpenType TidyEnv
env0 Type
msg
; (TidyEnv, TcRnMessage) -> TcM ()
forall a. (TidyEnv, TcRnMessage) -> TcM a
failWithTcM (TidyEnv
env1, Type -> TcRnMessage
TcRnUserTypeError Type
tidy_msg)
}
checkValidType :: UserTypeCtxt -> Type -> TcM ()
checkValidType :: UserTypeCtxt -> Type -> TcM ()
checkValidType UserTypeCtxt
ctxt Type
ty
= do { String -> SDoc -> TcM ()
traceTc String
"checkValidType" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty SDoc -> SDoc -> SDoc
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 ((() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
ty))
; Bool
rankn_flag <- Extension -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. Extension -> TcRnIf gbl lcl Bool
xoptM Extension
LangExt.RankNTypes
; Bool
impred_flag <- Extension -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. Extension -> TcRnIf gbl lcl Bool
xoptM Extension
LangExt.ImpredicativeTypes
; let gen_rank :: Rank -> Rank
gen_rank :: Rank -> Rank
gen_rank Rank
r | Bool
rankn_flag = Rank
ArbitraryRank
| Bool
otherwise = Rank
r
rank1 :: Rank
rank1 = Rank -> Rank
gen_rank Rank
r1
rank0 :: Rank
rank0 = Rank -> Rank
gen_rank Rank
MonoTypeRankZero
r1 :: Rank
r1 = Bool -> Rank -> Rank
LimitedRank Bool
True Rank
MonoTypeRankZero
rank :: Rank
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"
; TidyEnv
env <- [Var] -> TcM TidyEnv
tcInitOpenTidyEnv (Type -> [Var]
tyCoVarsOfTypeList Type
ty)
; ExpandMode
expand <- TcM ExpandMode
initialExpandMode
; let ve :: ValidityEnv
ve = ValidityEnv{ ve_tidy_env :: TidyEnv
ve_tidy_env = TidyEnv
env, ve_ctxt :: UserTypeCtxt
ve_ctxt = UserTypeCtxt
ctxt
, ve_rank :: Rank
ve_rank = Rank
rank, ve_expand :: ExpandMode
ve_expand = ExpandMode
expand }
; TcM () -> TcM ()
forall r. TcM r -> TcM r
checkNoErrs (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$
do { ValidityEnv -> Type -> TcM ()
check_type ValidityEnv
ve Type
ty
; UserTypeCtxt -> Type -> TcM ()
checkUserTypeError UserTypeCtxt
ctxt Type
ty
; String -> SDoc -> TcM ()
traceTc String
"done ct" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty) }
; UserTypeCtxt -> Type -> TcM ()
checkAmbiguity UserTypeCtxt
ctxt Type
ty
; String -> SDoc -> TcM ()
traceTc String
"checkValidType done" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty SDoc -> SDoc -> SDoc
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 ((() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
ty)) }
checkValidMonoType :: Type -> TcM ()
checkValidMonoType :: Type -> TcM ()
checkValidMonoType Type
ty
= do { TidyEnv
env <- [Var] -> TcM TidyEnv
tcInitOpenTidyEnv (Type -> [Var]
tyCoVarsOfTypeList Type
ty)
; ExpandMode
expand <- TcM ExpandMode
initialExpandMode
; let ve :: ValidityEnv
ve = ValidityEnv{ ve_tidy_env :: TidyEnv
ve_tidy_env = TidyEnv
env, ve_ctxt :: UserTypeCtxt
ve_ctxt = UserTypeCtxt
SigmaCtxt
, ve_rank :: Rank
ve_rank = Rank
MustBeMonoType, ve_expand :: ExpandMode
ve_expand = ExpandMode
expand }
; ValidityEnv -> Type -> TcM ()
check_type ValidityEnv
ve Type
ty }
checkTySynRhs :: UserTypeCtxt -> TcType -> TcM ()
checkTySynRhs :: UserTypeCtxt -> Type -> TcM ()
checkTySynRhs UserTypeCtxt
ctxt Type
ty
| Type -> Bool
returnsConstraintKind Type
actual_kind
= do { Bool
ck <- Extension -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. Extension -> TcRnIf gbl lcl Bool
xoptM Extension
LangExt.ConstraintKinds
; if Bool
ck
then Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Type -> Bool
isConstraintLikeKind Type
actual_kind)
(do { DynFlags
dflags <- IOEnv (Env TcGblEnv TcLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
; ExpandMode
expand <- TcM ExpandMode
initialExpandMode
; TidyEnv -> DynFlags -> UserTypeCtxt -> ExpandMode -> Type -> TcM ()
check_pred_ty TidyEnv
emptyTidyEnv DynFlags
dflags UserTypeCtxt
ctxt ExpandMode
expand Type
ty })
else (TidyEnv, TcRnMessage) -> TcM ()
addErrTcM ( TidyEnv
emptyTidyEnv
, Type -> TcRnMessage
TcRnIllegalConstraintSynonymOfKind (TidyEnv -> Type -> Type
tidyType TidyEnv
emptyTidyEnv Type
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 = (() :: Constraint) => 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 = (() :: Constraint) => 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
Bool
liberal_flag <- Extension -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. Extension -> TcRnIf gbl lcl Bool
xoptM Extension
LangExt.LiberalTypeSynonyms
ExpandMode -> TcM ExpandMode
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ExpandMode -> TcM ExpandMode) -> ExpandMode -> TcM ExpandMode
forall a b. (a -> b) -> a -> b
$ if Bool
liberal_flag then ExpandMode
Expand else ExpandMode
Both
data ValidityEnv = ValidityEnv
{ ValidityEnv -> TidyEnv
ve_tidy_env :: TidyEnv
, ValidityEnv -> UserTypeCtxt
ve_ctxt :: UserTypeCtxt
, ValidityEnv -> Rank
ve_rank :: Rank
, ValidityEnv -> ExpandMode
ve_expand :: ExpandMode }
instance Outputable ValidityEnv where
ppr :: ValidityEnv -> SDoc
ppr (ValidityEnv{ ve_tidy_env :: ValidityEnv -> TidyEnv
ve_tidy_env = TidyEnv
env, ve_ctxt :: ValidityEnv -> UserTypeCtxt
ve_ctxt = UserTypeCtxt
ctxt
, ve_rank :: ValidityEnv -> Rank
ve_rank = Rank
rank, ve_expand :: ValidityEnv -> ExpandMode
ve_expand = ExpandMode
expand }) =
SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
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
= (Type -> TcM ()) -> [Type] -> TcM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Bool -> ValidityEnv -> Type -> TcM ()
check_arg_type Bool
False ValidityEnv
ve) [Type]
tys
check_type ValidityEnv
_ (LitTy {}) = () -> TcM ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
check_type ValidityEnv
ve (CastTy Type
ty KindCoercion
_) = ValidityEnv -> Type -> TcM ()
check_type ValidityEnv
ve Type
ty
check_type ve :: ValidityEnv
ve@(ValidityEnv{ ve_tidy_env :: ValidityEnv -> TidyEnv
ve_tidy_env = TidyEnv
env
, ve_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
env, Rank -> Type -> TcRnMessage
TcRnForAllRankErr Rank
rank (TidyEnv -> Type -> Type
tidyType TidyEnv
env Type
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
_ Type
ty = String -> SDoc -> TcM ()
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"check_type" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty)
check_syn_tc_app :: ValidityEnv
-> KindOrType -> TyCon -> [KindOrType] -> TcM ()
check_syn_tc_app :: ValidityEnv -> Type -> TyCon -> [Type] -> TcM ()
check_syn_tc_app (ve :: ValidityEnv
ve@ValidityEnv{ ve_ctxt :: ValidityEnv -> UserTypeCtxt
ve_ctxt = UserTypeCtxt
ctxt, ve_expand :: ValidityEnv -> ExpandMode
ve_expand = ExpandMode
expand })
Type
ty TyCon
tc [Type]
tys
| [Type]
tys [Type] -> Int -> Bool
forall a. [a] -> Int -> Bool
`lengthAtLeast` Int
tc_arity
= case ExpandMode
expand of
ExpandMode
_ | TyCon -> Bool
isTypeFamilyTyCon TyCon
tc
-> ExpandMode -> TcM ()
check_args_only ExpandMode
expand
ExpandMode
Expand -> ExpandMode -> TcM ()
check_expansion_only ExpandMode
expand
ExpandMode
NoExpand -> ExpandMode -> TcM ()
check_args_only ExpandMode
expand
ExpandMode
Both -> ExpandMode -> TcM ()
check_args_only ExpandMode
NoExpand TcM () -> TcM () -> TcM ()
forall 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 { Bool
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
; Bool -> (TidyEnv, TcRnMessage) -> TcM ()
checkTcM Bool
ub_thing_allowed
(TidyEnv
env, UnboxedTupleOrSum -> Type -> TcRnMessage
TcRnUnboxedTupleOrSumTypeFuncArg UnboxedTupleOrSum
tup_or_sum (TidyEnv -> Type -> Type
tidyType TidyEnv
env Type
ty))
; Bool
impred <- Extension -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. Extension -> TcRnIf gbl lcl Bool
xoptM Extension
LangExt.ImpredicativeTypes
; let rank' :: Rank
rank' = if Bool
impred then Rank
ArbitraryRank else Rank
MonoTypeTyConArg
; (Type -> TcM ()) -> [Type] -> TcM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (ValidityEnv -> Type -> TcM ()
check_type (ValidityEnv
ve{ve_rank = rank'})) [Type]
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 { Bool
impred <- Extension -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. Extension -> TcRnIf gbl lcl Bool
xoptM Extension
LangExt.ImpredicativeTypes
; let rank' :: Rank
rank' = case Rank
rank of
Rank
_ | Bool
type_syn -> Rank
MonoTypeSynArg
Rank
MustBeMonoType -> Rank
MustBeMonoType
Rank
_other | Bool
impred -> Rank
ArbitraryRank
| Bool
otherwise -> Rank
MonoTypeTyConArg
ctxt' :: UserTypeCtxt
ctxt' :: UserTypeCtxt
ctxt'
| GhciCtxt Bool
_ <- UserTypeCtxt
ctxt = Bool -> UserTypeCtxt
GhciCtxt Bool
False
| Bool
otherwise = UserTypeCtxt
ctxt
; ValidityEnv -> Type -> TcM ()
check_type (ValidityEnv
ve{ve_ctxt = ctxt', ve_rank = rank'}) Type
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
=
Bool -> (TidyEnv, TcRnMessage) -> TcM ()
checkTcM ((Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Type -> Bool
isEqPred [Type]
theta) (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
Bool -> (TidyEnv, TcRnMessage) -> TcM ()
checkTcM (UserTypeCtxt -> Bool
vdqAllowed UserTypeCtxt
ctxt Bool -> Bool -> Bool
|| Bool
no_vdq)
(TidyEnv
env, Maybe Type -> TcRnMessage
TcRnVDQInTermType (Type -> Maybe Type
forall a. a -> Maybe a
Just (TidyEnv -> Type -> Type
tidyType TidyEnv
env Type
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
checkValidTheta :: UserTypeCtxt -> ThetaType -> TcM ()
checkValidTheta :: UserTypeCtxt -> [Type] -> TcM ()
checkValidTheta UserTypeCtxt
ctxt [Type]
theta
= (TidyEnv -> TcM (TidyEnv, SDoc)) -> TcM () -> TcM ()
forall a. (TidyEnv -> TcM (TidyEnv, SDoc)) -> TcM a -> TcM a
addErrCtxtM (UserTypeCtxt -> [Type] -> TidyEnv -> TcM (TidyEnv, SDoc)
checkThetaCtxt UserTypeCtxt
ctxt [Type]
theta) (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$
do { TidyEnv
env <- [Var] -> TcM TidyEnv
tcInitOpenTidyEnv ([Type] -> [Var]
tyCoVarsOfTypesList [Type]
theta)
; ExpandMode
expand <- TcM ExpandMode
initialExpandMode
; TidyEnv -> UserTypeCtxt -> ExpandMode -> [Type] -> TcM ()
check_valid_theta TidyEnv
env UserTypeCtxt
ctxt ExpandMode
expand [Type]
theta }
check_valid_theta :: TidyEnv -> UserTypeCtxt -> ExpandMode
-> [PredType] -> TcM ()
check_valid_theta :: TidyEnv -> UserTypeCtxt -> ExpandMode -> [Type] -> TcM ()
check_valid_theta TidyEnv
_ UserTypeCtxt
_ ExpandMode
_ []
= () -> TcM ()
forall 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 { DynFlags
dflags <- IOEnv (Env TcGblEnv TcLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
; String -> SDoc -> TcM ()
traceTc String
"check_valid_theta" ([Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
theta)
; (Type -> TcM ()) -> [Type] -> TcM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (TidyEnv -> DynFlags -> UserTypeCtxt -> ExpandMode -> Type -> TcM ()
check_pred_ty TidyEnv
env DynFlags
dflags UserTypeCtxt
ctxt ExpandMode
expand) [Type]
theta }
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
isEqPredClass 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 { ClsInstResult
result <- DynFlags -> Bool -> Class -> [Type] -> TcM ClsInstResult
matchGlobalInst DynFlags
dflags Bool
False Class
cls [Type]
tys
; case ClsInstResult
result of
OneInst { cir_what :: ClsInstResult -> InstanceWhat
cir_what = InstanceWhat
what }
-> let dia :: TcRnMessage
dia = DiagnosticMessage -> TcRnMessage
forall a.
(Diagnostic a, Typeable a, DiagnosticOpts a ~ NoDiagnosticOpts) =>
a -> TcRnMessage
mkTcRnUnknownMessage (DiagnosticMessage -> TcRnMessage)
-> DiagnosticMessage -> TcRnMessage
forall a b. (a -> b) -> a -> b
$
DiagnosticReason -> [GhcHint] -> SDoc -> DiagnosticMessage
mkPlainDiagnostic (WarningFlag -> DiagnosticReason
WarningWithFlag WarningFlag
Opt_WarnSimplifiableClassConstraints)
[GhcHint]
noHints
(InstanceWhat -> SDoc
simplifiable_constraint_warn InstanceWhat
what)
in TcRnMessage -> TcM ()
addDiagnosticTc TcRnMessage
dia
ClsInstResult
_ -> () -> TcM ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return () }
where
pred :: Type
pred = Class -> [Type] -> Type
mkClassPred Class
cls [Type]
tys
simplifiable_constraint_warn :: InstanceWhat -> SDoc
simplifiable_constraint_warn :: InstanceWhat -> SDoc
simplifiable_constraint_warn InstanceWhat
what
= [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"The constraint" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc -> SDoc
quotes (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TidyEnv -> Type -> Type
tidyType TidyEnv
env Type
pred))
SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"matches")
Int
2 (InstanceWhat -> SDoc
forall a. Outputable a => a -> SDoc
ppr InstanceWhat
what)
, SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"This makes type inference for inner bindings fragile;")
Int
2 (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"either use MonoLocalBinds, or simplify it using the instance") ]
okIPCtxt :: UserTypeCtxt -> Bool
okIPCtxt :: UserTypeCtxt -> Bool
okIPCtxt (FunSigCtxt {}) = Bool
True
okIPCtxt (InfSigCtxt {}) = Bool
True
okIPCtxt (ExprSigCtxt {}) = Bool
True
okIPCtxt UserTypeCtxt
TypeAppCtxt = Bool
True
okIPCtxt UserTypeCtxt
PatSigCtxt = Bool
True
okIPCtxt UserTypeCtxt
GenSigCtxt = Bool
True
okIPCtxt (ConArgCtxt {}) = Bool
True
okIPCtxt (ForSigCtxt {}) = Bool
True
okIPCtxt (GhciCtxt {}) = Bool
True
okIPCtxt UserTypeCtxt
SigmaCtxt = Bool
True
okIPCtxt (DataTyCtxt {}) = Bool
True
okIPCtxt (PatSynCtxt {}) = Bool
True
okIPCtxt (TySynCtxt {}) = Bool
True
okIPCtxt (KindSigCtxt {}) = Bool
False
okIPCtxt (StandaloneKindSigCtxt {}) = Bool
False
okIPCtxt (ClassSCCtxt {}) = Bool
False
okIPCtxt (InstDeclCtxt {}) = Bool
False
okIPCtxt (SpecInstCtxt {}) = Bool
False
okIPCtxt (RuleSigCtxt {}) = Bool
False
okIPCtxt UserTypeCtxt
DefaultDeclCtxt = Bool
False
okIPCtxt UserTypeCtxt
DerivClauseCtxt = Bool
False
okIPCtxt (TyVarBndrKindCtxt {}) = Bool
False
okIPCtxt (DataKindCtxt {}) = Bool
False
okIPCtxt (TySynKindCtxt {}) = Bool
False
okIPCtxt (TyFamResKindCtxt {}) = Bool
False
checkThetaCtxt :: UserTypeCtxt -> ThetaType -> TidyEnv -> TcM (TidyEnv, SDoc)
checkThetaCtxt :: UserTypeCtxt -> [Type] -> TidyEnv -> TcM (TidyEnv, SDoc)
checkThetaCtxt UserTypeCtxt
ctxt [Type]
theta TidyEnv
env
= (TidyEnv, SDoc) -> TcM (TidyEnv, SDoc)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) 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
= SDoc -> Name -> Int -> Int -> TcRnMessage
forall a. Outputable a => SDoc -> a -> Int -> Int -> TcRnMessage
arityErr (TyConFlavour -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TyCon -> TyConFlavour
tyConFlavour TyCon
tc)) (TyCon -> Name
tyConName TyCon
tc)
Int
tc_type_arity Int
tc_type_args
where
vis_tks :: [Type]
vis_tks = TyCon -> [Type] -> [Type]
filterOutInvisibleTypes TyCon
tc [Type]
tks
tc_type_arity :: Int
tc_type_arity = (VarBndr 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
arityErr :: Outputable a => SDoc -> a -> Int -> Int -> TcRnMessage
arityErr :: forall a. Outputable a => SDoc -> a -> Int -> Int -> TcRnMessage
arityErr SDoc
what a
name Int
n Int
m
= DiagnosticMessage -> TcRnMessage
forall a.
(Diagnostic a, Typeable a, DiagnosticOpts a ~ NoDiagnosticOpts) =>
a -> TcRnMessage
mkTcRnUnknownMessage (DiagnosticMessage -> TcRnMessage)
-> DiagnosticMessage -> TcRnMessage
forall a b. (a -> b) -> a -> b
$ [GhcHint] -> SDoc -> DiagnosticMessage
mkPlainError [GhcHint]
noHints (SDoc -> DiagnosticMessage) -> SDoc -> DiagnosticMessage
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
forall doc. IsLine doc => [doc] -> doc
hsep [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"The" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
what, SDoc -> SDoc
quotes (a -> SDoc
forall a. Outputable a => a -> SDoc
ppr a
name), String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"should have",
SDoc
n_arguments SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> SDoc
forall doc. IsLine doc => doc
comma, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"but has been given",
if Int
mInt -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==Int
0 then String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"none" else Int -> SDoc
forall doc. IsLine doc => Int -> doc
int Int
m]
where
n_arguments :: SDoc
n_arguments | Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"no arguments"
| Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"1 argument"
| Bool
True = [SDoc] -> SDoc
forall doc. IsLine doc => [doc] -> doc
hsep [Int -> SDoc
forall doc. IsLine doc => Int -> doc
int Int
n, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"arguments"]
checkValidInstHead :: UserTypeCtxt -> Class -> [Type] -> TcM ()
checkValidInstHead :: UserTypeCtxt -> Class -> [Type] -> TcM ()
checkValidInstHead UserTypeCtxt
ctxt Class
clas [Type]
cls_args
= do { DynFlags
dflags <- IOEnv (Env TcGblEnv TcLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
; Bool
is_boot <- TcRnIf TcGblEnv TcLclEnv Bool
tcIsHsBootOrSig
; Bool
is_sig <- TcRnIf TcGblEnv TcLclEnv Bool
tcIsHsig
; DynFlags
-> Bool -> Bool -> UserTypeCtxt -> Class -> [Type] -> TcM ()
check_special_inst_head DynFlags
dflags Bool
is_boot Bool
is_sig UserTypeCtxt
ctxt Class
clas [Type]
cls_args
; TyCon -> [Type] -> TcM ()
checkValidTypePats (Class -> TyCon
classTyCon Class
clas) [Type]
cls_args
}
check_special_inst_head :: DynFlags -> Bool -> Bool
-> UserTypeCtxt -> Class -> [Type] -> TcM ()
check_special_inst_head :: DynFlags
-> Bool -> Bool -> UserTypeCtxt -> Class -> [Type] -> TcM ()
check_special_inst_head DynFlags
dflags Bool
is_boot Bool
is_sig UserTypeCtxt
ctxt Class
clas [Type]
cls_args
| Class -> Bool
isAbstractClass Class
clas
, Bool -> Bool
not Bool
is_boot
= TcRnMessage -> TcM ()
forall a. TcRnMessage -> TcM a
failWithTc (Class -> TcRnMessage
TcRnAbstractClassInst Class
clas)
| Name
clas_nm Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
typeableClassName
, Bool -> Bool
not Bool
is_sig
, Bool
hand_written_bindings
= TcRnMessage -> TcM ()
forall a. TcRnMessage -> TcM a
failWithTc (TcRnMessage -> TcM ()) -> TcRnMessage -> TcM ()
forall a b. (a -> b) -> a -> b
$ Class -> Bool -> TcRnMessage
TcRnSpecialClassInst 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 ]
, (Bool -> Bool
not Bool
is_sig Bool -> Bool -> Bool
&& Bool
hand_written_bindings) Bool -> Bool -> Bool
|| Bool
derived_instance
= TcRnMessage -> TcM ()
forall a. TcRnMessage -> TcM a
failWithTc (TcRnMessage -> TcM ()) -> TcRnMessage -> TcM ()
forall a b. (a -> b) -> a -> b
$ Class -> Bool -> TcRnMessage
TcRnSpecialClassInst 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 ]
, Bool -> Bool
not Bool
quantified_constraint
= TcRnMessage -> TcM ()
forall a. TcRnMessage -> TcM a
failWithTc (TcRnMessage -> TcM ()) -> TcRnMessage -> TcM ()
forall a b. (a -> b) -> a -> b
$ Class -> Bool -> TcRnMessage
TcRnSpecialClassInst 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 -> TcRnMessage -> TcM ()
failIfTc (DynFlags -> Bool
safeLanguageOn DynFlags
dflags) (Class -> Bool -> TcRnMessage
TcRnSpecialClassInst 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
= TcRnMessage -> TcM ()
forall a. TcRnMessage -> TcM a
failWithTc (Class -> TcRnMessage
TcRnTupleConstraintInst Class
clas)
| Bool
check_h98_arg_shape
, Just SDoc
msg <- Maybe SDoc
mb_ty_args_msg
= TcRnMessage -> TcM ()
forall a. TcRnMessage -> TcM a
failWithTc (Class -> [Type] -> SDoc -> TcRnMessage
instTypeErr Class
clas [Type]
cls_args SDoc
msg)
| Bool
otherwise
= () -> TcM ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
where
clas_nm :: Name
clas_nm = Class -> Name
forall a. NamedThing a => a -> Name
getName Class
clas
ty_args :: [Type]
ty_args = TyCon -> [Type] -> [Type]
filterOutInvisibleTypes (Class -> TyCon
classTyCon Class
clas) [Type]
cls_args
hand_written_bindings :: Bool
hand_written_bindings
= case UserTypeCtxt
ctxt of
InstDeclCtxt Bool
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
head_type_synonym_msg :: SDoc
head_type_synonym_msg = SDoc -> SDoc
forall doc. IsLine doc => doc -> doc
parens (
String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"All instance types must be of the form (T t1 ... tn)" SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$
String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"where T is not a synonym." SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$
String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Use TypeSynonymInstances if you want to disable this.")
head_type_args_tyvars_msg :: SDoc
head_type_args_tyvars_msg = SDoc -> SDoc
forall doc. IsLine doc => doc -> doc
parens ([SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [
String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"All instance types must be of the form (T a1 ... an)",
String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"where a1 ... an are *distinct type variables*,",
String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"and each type variable appears at most once in the instance head.",
String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Use FlexibleInstances if you want to disable this."])
head_one_type_msg :: SDoc
head_one_type_msg = SDoc -> SDoc
forall doc. IsLine doc => doc -> doc
parens (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Only one type can be given in an instance head." SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$
String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Use MultiParamTypeClasses if you want to allow more, or zero."
mb_ty_args_msg :: Maybe SDoc
mb_ty_args_msg
| Bool -> Bool
not (Extension -> DynFlags -> Bool
xopt Extension
LangExt.TypeSynonymInstances DynFlags
dflags)
, Bool -> Bool
not ((Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Type -> Bool
tcInstHeadTyNotSynonym [Type]
ty_args)
= SDoc -> Maybe SDoc
forall a. a -> Maybe a
Just SDoc
head_type_synonym_msg
| Bool -> Bool
not (Extension -> DynFlags -> Bool
xopt Extension
LangExt.FlexibleInstances DynFlags
dflags)
, Bool -> Bool
not ((Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Type -> Bool
tcInstHeadTyAppAllTyVars [Type]
ty_args)
= SDoc -> Maybe SDoc
forall a. a -> Maybe a
Just SDoc
head_type_args_tyvars_msg
| [Type] -> Int
forall 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)
= SDoc -> Maybe SDoc
forall a. a -> Maybe a
Just SDoc
head_one_type_msg
| Bool
otherwise
= Maybe SDoc
forall a. Maybe a
Nothing
tcInstHeadTyNotSynonym :: Type -> Bool
tcInstHeadTyNotSynonym :: Type -> Bool
tcInstHeadTyNotSynonym Type
ty
= case Type
ty of
TyConApp TyCon
tc [Type]
_ -> Bool -> Bool
not (TyCon -> Bool
isTypeSynonymTyCon TyCon
tc) Bool -> Bool -> Bool
|| TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
unrestrictedFunTyCon
Type
_ -> Bool
True
tcInstHeadTyAppAllTyVars :: Type -> Bool
tcInstHeadTyAppAllTyVars :: Type -> Bool
tcInstHeadTyAppAllTyVars Type
ty
| Just (TyCon
tc, [Type]
tys) <- HasCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
tcSplitTyConApp_maybe (Type -> Type
dropCasts Type
ty)
= let tys' :: [Type]
tys' = TyCon -> [Type] -> [Type]
filterOutInvisibleTypes TyCon
tc [Type]
tys
tys'' :: [Type]
tys'' | TyCon
tc TyCon -> 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
instTypeErr :: Class -> [Type] -> SDoc -> TcRnMessage
instTypeErr :: Class -> [Type] -> SDoc -> TcRnMessage
instTypeErr Class
cls [Type]
tys SDoc
msg
= DiagnosticMessage -> TcRnMessage
forall a.
(Diagnostic a, Typeable a, DiagnosticOpts a ~ NoDiagnosticOpts) =>
a -> TcRnMessage
mkTcRnUnknownMessage (DiagnosticMessage -> TcRnMessage)
-> DiagnosticMessage -> TcRnMessage
forall a b. (a -> b) -> a -> b
$ [GhcHint] -> SDoc -> DiagnosticMessage
mkPlainError [GhcHint]
noHints (SDoc -> DiagnosticMessage) -> SDoc -> DiagnosticMessage
forall a b. (a -> b) -> a -> b
$
SDoc -> Int -> SDoc -> SDoc
hang (SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Illegal instance declaration for")
Int
2 (SDoc -> SDoc
quotes (Class -> [Type] -> SDoc
pprClassPred Class
cls [Type]
tys)))
Int
2 SDoc
msg
checkHasFieldInst :: Class -> [Type] -> TcM ()
checkHasFieldInst :: Class -> [Type] -> TcM ()
checkHasFieldInst Class
cls tys :: [Type]
tys@[Type
_k_ty, Type
x_ty, Type
r_ty, Type
_a_ty] =
case (() :: Constraint) => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
r_ty of
Maybe (TyCon, [Type])
Nothing -> SDoc -> TcM ()
whoops (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Record data type must be specified")
Just (TyCon
tc, [Type]
_)
| TyCon -> Bool
isFamilyTyCon TyCon
tc
-> SDoc -> TcM ()
whoops (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Record data type may not be a data family")
| Bool
otherwise -> case Type -> Maybe FastString
isStrLitTy Type
x_ty of
Just FastString
lbl
| Maybe FieldLabel -> Bool
forall a. Maybe a -> Bool
isJust (FieldLabelString -> TyCon -> Maybe FieldLabel
lookupTyConFieldLabel (FastString -> FieldLabelString
FieldLabelString FastString
lbl) TyCon
tc)
-> SDoc -> TcM ()
whoops (TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tc SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"already has a field"
SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc -> SDoc
quotes (FastString -> SDoc
forall a. Outputable a => a -> SDoc
ppr FastString
lbl))
| 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) -> () -> TcM ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
| Bool
otherwise -> SDoc -> TcM ()
whoops (TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tc SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"has fields")
where
whoops :: SDoc -> TcM ()
whoops = TcRnMessage -> TcM ()
addErrTc (TcRnMessage -> TcM ()) -> (SDoc -> TcRnMessage) -> SDoc -> TcM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Class -> [Type] -> SDoc -> TcRnMessage
instTypeErr Class
cls [Type]
tys
checkHasFieldInst Class
_ [Type]
tys = String -> SDoc -> TcM ()
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"checkHasFieldInst" ([Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
tys)
validDerivPred :: 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)
where
check_size :: PatersonSize -> Bool
check_size PatersonSize
pred_size = Maybe PatersonSizeFailure -> Bool
forall a. Maybe a -> Bool
isNothing (PatersonSize
pred_size PatersonSize -> PatersonSize -> Maybe PatersonSizeFailure
`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 -> case TyCon -> Maybe Class
tyConClass_maybe TyCon
tc of
Maybe Class
Nothing -> TcRnMessage -> TcM ()
forall a. TcRnMessage -> TcM a
failWithTc (TyConFlavour -> TcRnMessage
TcRnIllegalClassInst (TyCon -> TyConFlavour
tyConFlavour TyCon
tc))
Just Class
clas -> do
{ SrcSpanAnn' (EpAnn AnnListItem) -> TcM () -> TcM ()
forall ann a. SrcSpanAnn' ann -> TcRn a -> TcRn a
setSrcSpanA SrcSpanAnn' (EpAnn AnnListItem)
head_loc (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$
UserTypeCtxt -> Class -> [Type] -> TcM ()
checkValidInstHead UserTypeCtxt
ctxt Class
clas [Type]
inst_tys
; String -> SDoc -> TcM ()
traceTc String
"checkValidInstance {" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty)
; TidyEnv
env0 <- TcM TidyEnv
tcInitTidyEnv
; ExpandMode
expand <- TcM ExpandMode
initialExpandMode
; TidyEnv -> UserTypeCtxt -> ExpandMode -> [Type] -> TcM ()
check_valid_theta TidyEnv
env0 UserTypeCtxt
ctxt ExpandMode
expand [Type]
theta
; Bool
undecidable_ok <- Extension -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. Extension -> TcRnIf gbl lcl Bool
xoptM Extension
LangExt.UndecidableInstances
; if Bool
undecidable_ok
then UserTypeCtxt -> Type -> TcM ()
checkAmbiguity UserTypeCtxt
ctxt Type
ty
else [Type] -> Type -> TcM ()
checkInstTermination [Type]
theta Type
tau
; String -> SDoc -> TcM ()
traceTc String
"cvi 2" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty)
; case (Bool -> Class -> [Type] -> [Type] -> Validity
checkInstCoverage Bool
undecidable_ok Class
clas [Type]
theta [Type]
inst_tys) of
Validity
IsValid -> () -> TcM ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
NotValid SDoc
msg -> TcRnMessage -> TcM ()
addErrTc (Class -> [Type] -> SDoc -> TcRnMessage
instTypeErr Class
clas [Type]
inst_tys SDoc
msg)
; String -> SDoc -> TcM ()
traceTc String
"End checkValidInstance }" SDoc
forall doc. IsOutput doc => doc
empty
; () -> TcM ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return () }
Type
_ -> TcRnMessage -> TcM ()
forall a. TcRnMessage -> TcM a
failWithTc (Type -> TcRnMessage
TcRnNoClassInstHead Type
tau)
where
([Type]
theta, Type
tau) = Type -> ([Type], Type)
splitInstTyForValidity Type
ty
head_loc :: SrcSpanAnn' (EpAnn AnnListItem)
head_loc = GenLocated (SrcSpanAnn' (EpAnn AnnListItem)) (HsType GhcRn)
-> SrcSpanAnn' (EpAnn AnnListItem)
forall l e. GenLocated l e -> l
getLoc (LHsSigType GhcRn -> LHsType GhcRn
forall (p :: Pass). LHsSigType (GhcPass p) -> LHsType (GhcPass p)
getLHsInstDeclHead LHsSigType GhcRn
hs_type)
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 PatersonSizeFailure
`ltPatersonSize` PatersonSize
head_size of
Just PatersonSizeFailure
ps_failure -> TcRnMessage -> TcM ()
forall a. TcRnMessage -> TcM a
failWithTc (TcRnMessage -> TcM ()) -> TcRnMessage -> TcM ()
forall a b. (a -> b) -> a -> b
$ PatersonSizeFailure -> Type -> Type -> TcRnMessage
mkInstSizeError PatersonSizeFailure
ps_failure Type
head_pred Type
pred
Maybe PatersonSizeFailure
Nothing -> () -> TcM ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
mkInstSizeError :: PatersonSizeFailure -> TcPredType -> TcPredType -> TcRnMessage
mkInstSizeError :: PatersonSizeFailure -> Type -> Type -> TcRnMessage
mkInstSizeError PatersonSizeFailure
ps_failure Type
head_pred Type
pred
= DiagnosticMessage -> TcRnMessage
forall a.
(Diagnostic a, Typeable a, DiagnosticOpts a ~ NoDiagnosticOpts) =>
a -> TcRnMessage
mkTcRnUnknownMessage (DiagnosticMessage -> TcRnMessage)
-> DiagnosticMessage -> TcRnMessage
forall a b. (a -> b) -> a -> b
$ [GhcHint] -> SDoc -> DiagnosticMessage
mkPlainError [GhcHint]
noHints (SDoc -> DiagnosticMessage) -> SDoc -> DiagnosticMessage
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ SDoc
main_msg
, SDoc -> SDoc
forall doc. IsLine doc => doc -> doc
parens SDoc
undecidableMsg ]
where
pp_head :: SDoc
pp_head = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"instance head" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc -> SDoc
quotes (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
head_pred)
pp_pred :: SDoc
pp_pred = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"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)
main_msg :: SDoc
main_msg = case PatersonSizeFailure
ps_failure of
PSF_TyFam TyCon
tc ->
SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Illegal use of type family" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc -> SDoc
quotes (TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tc))
Int
2 (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"in the" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
pp_pred)
PSF_TyVar [Var]
tvs -> SDoc -> Int -> SDoc -> SDoc
hang ([Var] -> SDoc
occMsg [Var]
tvs)
Int
2 ([SDoc] -> SDoc
forall doc. IsLine doc => [doc] -> doc
sep [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"in the" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
pp_pred
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"than in the" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
pp_head ])
PatersonSizeFailure
PSF_Size -> SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"The" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
pp_pred)
Int
2 ([SDoc] -> SDoc
forall doc. IsLine doc => [doc] -> doc
sep [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"is no smaller than", String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"the" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
pp_head ])
occMsg :: [TyVar] -> SDoc
occMsg :: [Var] -> SDoc
occMsg [Var]
tvs = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Variable" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> [Var] -> SDoc
forall a. [a] -> SDoc
plural [Var]
tvs SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc -> SDoc
quotes ((Var -> SDoc) -> [Var] -> SDoc
forall a. (a -> SDoc) -> [a] -> SDoc
pprWithCommas Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Var]
tvs)
SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
pp_occurs SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"more often"
where
pp_occurs :: SDoc
pp_occurs | [Var] -> Bool
forall a. [a] -> Bool
isSingleton [Var]
tvs = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"occurs"
| Bool
otherwise = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"occur"
undecidableMsg :: SDoc
undecidableMsg :: SDoc
undecidableMsg = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Use UndecidableInstances to permit this"
checkValidCoAxiom :: CoAxiom Branched -> TcM ()
checkValidCoAxiom :: CoAxiom Branched -> TcM ()
checkValidCoAxiom ax :: CoAxiom Branched
ax@(CoAxiom { co_ax_tc :: forall (br :: BranchFlag). CoAxiom br -> TyCon
co_ax_tc = TyCon
fam_tc, co_ax_branches :: forall (br :: BranchFlag). CoAxiom br -> Branches br
co_ax_branches = Branches Branched
branches })
= do { (CoAxBranch -> TcM ()) -> [CoAxBranch] -> TcM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (TyCon -> CoAxBranch -> TcM ()
checkValidCoAxBranch TyCon
fam_tc) [CoAxBranch]
branch_list
; ([CoAxBranch]
-> CoAxBranch -> IOEnv (Env TcGblEnv TcLclEnv) [CoAxBranch])
-> [CoAxBranch] -> [CoAxBranch] -> TcM ()
forall (m :: * -> *) (t :: * -> *) a b.
(Monad m, Foldable t) =>
(a -> b -> m a) -> a -> t b -> m ()
foldlM_ [CoAxBranch]
-> CoAxBranch -> IOEnv (Env TcGblEnv TcLclEnv) [CoAxBranch]
check_branch_compat [] [CoAxBranch]
branch_list }
where
branch_list :: [CoAxBranch]
branch_list = Branches Branched -> [CoAxBranch]
forall (br :: BranchFlag). Branches br -> [CoAxBranch]
fromBranches Branches Branched
branches
injectivity :: Injectivity
injectivity = TyCon -> Injectivity
tyConInjectivityInfo TyCon
fam_tc
check_branch_compat :: [CoAxBranch]
-> CoAxBranch
-> TcM [CoAxBranch]
check_branch_compat :: [CoAxBranch]
-> CoAxBranch -> IOEnv (Env TcGblEnv TcLclEnv) [CoAxBranch]
check_branch_compat [CoAxBranch]
prev_branches CoAxBranch
cur_branch
| CoAxBranch
cur_branch CoAxBranch -> [CoAxBranch] -> Bool
`isDominatedBy` [CoAxBranch]
prev_branches
= do { let dia :: TcRnMessage
dia = DiagnosticMessage -> TcRnMessage
forall a.
(Diagnostic a, Typeable a, DiagnosticOpts a ~ NoDiagnosticOpts) =>
a -> TcRnMessage
mkTcRnUnknownMessage (DiagnosticMessage -> TcRnMessage)
-> DiagnosticMessage -> TcRnMessage
forall a b. (a -> b) -> a -> b
$
DiagnosticReason -> [GhcHint] -> SDoc -> DiagnosticMessage
mkPlainDiagnostic DiagnosticReason
WarningWithoutFlag [GhcHint]
noHints (TyCon -> CoAxBranch -> SDoc
inaccessibleCoAxBranch 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 { DynFlags
dflags <- IOEnv (Env TcGblEnv TcLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
; let conflicts :: [CoAxBranch]
conflicts =
([CoAxBranch], Int) -> [CoAxBranch]
forall a b. (a, b) -> a
fst (([CoAxBranch], Int) -> [CoAxBranch])
-> ([CoAxBranch], Int) -> [CoAxBranch]
forall a b. (a -> b) -> a -> b
$ (([CoAxBranch], Int) -> CoAxBranch -> ([CoAxBranch], Int))
-> ([CoAxBranch], Int) -> [CoAxBranch] -> ([CoAxBranch], Int)
forall 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
; TyCon -> [CoAxBranch] -> CoAxBranch -> TcM ()
reportConflictingInjectivityErrs TyCon
fam_tc [CoAxBranch]
conflicts CoAxBranch
cur_branch
; DynFlags -> CoAxiom Branched -> CoAxBranch -> [Bool] -> TcM ()
forall (br :: BranchFlag).
DynFlags -> CoAxiom br -> CoAxBranch -> [Bool] -> TcM ()
reportInjectivityErrors DynFlags
dflags CoAxiom Branched
ax CoAxBranch
cur_branch [Bool]
inj }
| Bool
otherwise
= () -> TcM ()
forall 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_tvs :: CoAxBranch -> [Var]
cab_tvs = [Var]
tvs, cab_cvs :: CoAxBranch -> [Var]
cab_cvs = [Var]
cvs
, cab_lhs :: CoAxBranch -> [Type]
cab_lhs = [Type]
typats
, cab_rhs :: CoAxBranch -> Type
cab_rhs = Type
rhs, cab_loc :: CoAxBranch -> SrcSpan
cab_loc = SrcSpan
loc })
= SrcSpan -> TcM () -> TcM ()
forall a. SrcSpan -> TcRn a -> TcRn a
setSrcSpan SrcSpan
loc (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$
TyCon -> [Var] -> [Type] -> Type -> TcM ()
checkValidTyFamEqn TyCon
fam_tc ([Var]
tvs[Var] -> [Var] -> [Var]
forall a. [a] -> [a] -> [a]
++[Var]
cvs) [Type]
typats Type
rhs
checkValidTyFamEqn :: TyCon
-> [Var]
-> [Type]
-> Type
-> TcM ()
checkValidTyFamEqn :: TyCon -> [Var] -> [Type] -> Type -> TcM ()
checkValidTyFamEqn TyCon
fam_tc [Var]
qvs [Type]
typats Type
rhs
= do { TyCon -> [Type] -> TcM ()
checkValidTypePats TyCon
fam_tc [Type]
typats
; TyCon -> [Var] -> [Type] -> Type -> TcM ()
checkFamPatBinders TyCon
fam_tc [Var]
qvs [Type]
typats Type
rhs
; Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (TyCon -> Bool
isTypeFamilyTyCon TyCon
fam_tc) (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$
case Int -> [Type] -> [Type]
forall a. Int -> [a] -> [a]
drop (TyCon -> Int
tyConArity TyCon
fam_tc) [Type]
typats of
[] -> () -> TcM ()
forall 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
; Bool
undecidable_ok <- Extension -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. Extension -> TcRnIf gbl lcl Bool
xoptM Extension
LangExt.UndecidableInstances
; String -> SDoc -> TcM ()
traceTc String
"checkVTFE" (TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
fam_tc SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
rhs SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ [(TyCon, [Type])] -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Type -> [(TyCon, [Type])]
tcTyFamInsts Type
rhs))
; Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
undecidable_ok (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$
(TcRnMessage -> TcM ()) -> [TcRnMessage] -> TcM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ TcRnMessage -> TcM ()
addErrTc (TyCon -> [Type] -> [(TyCon, [Type])] -> [TcRnMessage]
checkFamInstRhs TyCon
fam_tc [Type]
typats (Type -> [(TyCon, [Type])]
tcTyFamInsts Type
rhs)) }
checkValidAssocTyFamDeflt :: TyCon
-> [Type]
-> TcM ()
checkValidAssocTyFamDeflt :: TyCon -> [Type] -> TcM ()
checkValidAssocTyFamDeflt TyCon
fam_tc [Type]
pats =
do { [Var]
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
; [(Var, ForAllTyFlag)] -> TcM ()
check_all_distinct_tvs ([(Var, ForAllTyFlag)] -> TcM ())
-> [(Var, ForAllTyFlag)] -> TcM ()
forall a b. (a -> b) -> a -> b
$ [Var] -> [ForAllTyFlag] -> [(Var, ForAllTyFlag)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
cpt_tvs [ForAllTyFlag]
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
$ DiagnosticMessage -> TcRnMessage
forall a.
(Diagnostic a, Typeable a, DiagnosticOpts a ~ NoDiagnosticOpts) =>
a -> TcRnMessage
mkTcRnUnknownMessage (DiagnosticMessage -> TcRnMessage)
-> DiagnosticMessage -> TcRnMessage
forall a b. (a -> b) -> a -> b
$ [GhcHint] -> SDoc -> DiagnosticMessage
mkPlainError [GhcHint]
noHints (SDoc -> DiagnosticMessage) -> SDoc -> DiagnosticMessage
forall a b. (a -> b) -> a -> b
$
Bool -> SDoc -> SDoc
pprWithExplicitKindsWhen (ForAllTyFlag -> Bool
isInvisibleForAllTyFlag ForAllTyFlag
pat_vis) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Illegal argument" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc -> SDoc
quotes (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
pat) SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"in:")
Int
2 ([SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [SDoc
ppr_eqn, SDoc
suggestion])
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) Any)
-> [NonEmpty (Var, ForAllTyFlag)] -> TcM ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_
(\NonEmpty (Var, ForAllTyFlag)
d -> let (Var
pat_tv, ForAllTyFlag
pat_vis) = NonEmpty (Var, ForAllTyFlag) -> (Var, ForAllTyFlag)
forall a. NonEmpty a -> a
NE.head NonEmpty (Var, ForAllTyFlag)
d in TcRnMessage -> IOEnv (Env TcGblEnv TcLclEnv) Any
forall a. TcRnMessage -> TcM a
failWithTc (TcRnMessage -> IOEnv (Env TcGblEnv TcLclEnv) Any)
-> TcRnMessage -> IOEnv (Env TcGblEnv TcLclEnv) Any
forall a b. (a -> b) -> a -> b
$
DiagnosticMessage -> TcRnMessage
forall a.
(Diagnostic a, Typeable a, DiagnosticOpts a ~ NoDiagnosticOpts) =>
a -> TcRnMessage
mkTcRnUnknownMessage (DiagnosticMessage -> TcRnMessage)
-> DiagnosticMessage -> TcRnMessage
forall a b. (a -> b) -> a -> b
$ [GhcHint] -> SDoc -> DiagnosticMessage
mkPlainError [GhcHint]
noHints (SDoc -> DiagnosticMessage) -> SDoc -> DiagnosticMessage
forall a b. (a -> b) -> a -> b
$
Bool -> SDoc -> SDoc
pprWithExplicitKindsWhen (ForAllTyFlag -> Bool
isInvisibleForAllTyFlag ForAllTyFlag
pat_vis) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Illegal duplicate variable"
SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc -> SDoc
quotes (Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
pat_tv) SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"in:")
Int
2 ([SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [SDoc
ppr_eqn, SDoc
suggestion]))
[NonEmpty (Var, ForAllTyFlag)]
dups
ppr_eqn :: SDoc
ppr_eqn :: SDoc
ppr_eqn =
SDoc -> SDoc
quotes (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"type" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TyCon -> [Type] -> Type
mkTyConApp TyCon
fam_tc [Type]
pats)
SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
forall doc. IsLine doc => doc
equals SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"...")
suggestion :: SDoc
suggestion :: SDoc
suggestion = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"The arguments to" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc -> SDoc
quotes (TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
fam_tc)
SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"must all be distinct type variables"
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 PatersonSizeFailure
ps_failure <- [Type] -> PatersonSize
pSizeTypes [Type]
tys PatersonSize -> PatersonSize -> Maybe PatersonSizeFailure
`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
$ PatersonSizeFailure -> Type -> Type -> TcRnMessage
mkFamSizeError PatersonSizeFailure
ps_failure (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
mkFamSizeError :: PatersonSizeFailure -> Type -> Type -> TcRnMessage
mkFamSizeError :: PatersonSizeFailure -> Type -> Type -> TcRnMessage
mkFamSizeError PatersonSizeFailure
ps_failure Type
lhs Type
fam_call
= DiagnosticMessage -> TcRnMessage
forall a.
(Diagnostic a, Typeable a, DiagnosticOpts a ~ NoDiagnosticOpts) =>
a -> TcRnMessage
mkTcRnUnknownMessage (DiagnosticMessage -> TcRnMessage)
-> DiagnosticMessage -> TcRnMessage
forall a b. (a -> b) -> a -> b
$ [GhcHint] -> SDoc -> DiagnosticMessage
mkPlainError [GhcHint]
noHints (SDoc -> DiagnosticMessage) -> SDoc -> DiagnosticMessage
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ SDoc
main_msg
, SDoc -> SDoc
forall doc. IsLine doc => doc -> doc
parens SDoc
undecidableMsg ]
where
pp_lhs :: SDoc
pp_lhs = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"LHS of the family instance" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc -> SDoc
quotes (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
lhs)
pp_call :: SDoc
pp_call = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"type-family application" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc -> SDoc
quotes (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
fam_call)
main_msg :: SDoc
main_msg = case PatersonSizeFailure
ps_failure of
PSF_TyFam TyCon
tc ->
SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Illegal nested use of type family" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc -> SDoc
quotes (TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tc))
Int
2 (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"in the arguments of the" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
pp_call)
PSF_TyVar [Var]
tvs -> SDoc -> Int -> SDoc -> SDoc
hang ([Var] -> SDoc
occMsg [Var]
tvs)
Int
2 ([SDoc] -> SDoc
forall doc. IsLine doc => [doc] -> doc
sep [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"in the" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
pp_call
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"than in the" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
pp_lhs ])
PatersonSizeFailure
PSF_Size -> SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"The" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
pp_call)
Int
2 ([SDoc] -> SDoc
forall doc. IsLine doc => [doc] -> doc
sep [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"is no smaller than", String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"the" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
pp_lhs ])
checkFamPatBinders :: TyCon
-> [TcTyVar]
-> [TcType]
-> Type
-> TcM ()
checkFamPatBinders :: TyCon -> [Var] -> [Type] -> Type -> TcM ()
checkFamPatBinders TyCon
fam_tc [Var]
qtvs [Type]
pats Type
rhs
= do { String -> SDoc -> TcM ()
traceTc String
"checkFamPatBinders" (SDoc -> TcM ()) -> SDoc -> TcM ()
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
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
"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_tvs:" 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 ]
; [Var] -> SDoc -> SDoc -> TcM ()
check_tvs [Var]
bad_rhs_tvs (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"mentioned in the RHS")
(String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"bound on the LHS of")
; [Var] -> SDoc -> SDoc -> TcM ()
check_tvs [Var]
bad_qtvs (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"bound by a forall")
(String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"used in")
}
where
cpt_tvs :: VarSet
cpt_tvs = [Type] -> VarSet
tyCoVarsOfTypes [Type]
pats
inj_cpt_tvs :: VarSet
inj_cpt_tvs = FV -> VarSet
fvVarSet (FV -> VarSet) -> FV -> VarSet
forall a b. (a -> b) -> a -> b
$ Bool -> [Type] -> FV
injectiveVarsOfTypes Bool
False [Type]
pats
rhs_fvs :: FV
rhs_fvs = Type -> FV
tyCoFVsOfType Type
rhs
used_tvs :: VarSet
used_tvs = VarSet
cpt_tvs VarSet -> VarSet -> VarSet
`unionVarSet` FV -> VarSet
fvVarSet FV
rhs_fvs
bad_qtvs :: [Var]
bad_qtvs = (Var -> Bool) -> [Var] -> [Var]
forall a. (a -> Bool) -> [a] -> [a]
filterOut (Var -> VarSet -> Bool
`elemVarSet` VarSet
used_tvs) [Var]
qtvs
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) (FV -> [Var]
fvVarList FV
rhs_fvs)
dodgy_tvs :: VarSet
dodgy_tvs = VarSet
cpt_tvs VarSet -> VarSet -> VarSet
`minusVarSet` VarSet
inj_cpt_tvs
check_tvs :: [Var] -> SDoc -> SDoc -> TcM ()
check_tvs [Var]
tvs SDoc
what SDoc
what2
= Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Var] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Var]
tvs) (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$ SrcSpan -> TcRnMessage -> TcM ()
addErrAt (Var -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
getSrcSpan ([Var] -> Var
forall a. HasCallStack => [a] -> a
head [Var]
tvs)) (TcRnMessage -> TcM ()) -> TcRnMessage -> TcM ()
forall a b. (a -> b) -> a -> b
$ DiagnosticMessage -> TcRnMessage
forall a.
(Diagnostic a, Typeable a, DiagnosticOpts a ~ NoDiagnosticOpts) =>
a -> TcRnMessage
mkTcRnUnknownMessage (DiagnosticMessage -> TcRnMessage)
-> DiagnosticMessage -> TcRnMessage
forall a b. (a -> b) -> a -> b
$ [GhcHint] -> SDoc -> DiagnosticMessage
mkPlainError [GhcHint]
noHints (SDoc -> DiagnosticMessage) -> SDoc -> DiagnosticMessage
forall a b. (a -> b) -> a -> b
$
SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Type variable" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> [Var] -> SDoc
forall a. [a] -> SDoc
plural [Var]
tvs SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Var] -> SDoc
forall a. Outputable a => [a] -> SDoc
pprQuotedList [Var]
tvs
SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Var] -> SDoc
forall a. [a] -> SDoc
isOrAre [Var]
tvs SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
what SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> SDoc
forall doc. IsLine doc => doc
comma)
Int
2 ([SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"but not" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
what2 SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"the family instance"
, [Var] -> SDoc
mk_extra [Var]
tvs ])
mk_extra :: [Var] -> SDoc
mk_extra [Var]
tvs = Bool -> SDoc -> SDoc
forall doc. IsOutput doc => Bool -> doc -> doc
ppWhen ((Var -> Bool) -> [Var] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Var -> VarSet -> Bool
`elemVarSet` VarSet
dodgy_tvs) [Var]
tvs) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"The real LHS (expanding synonyms) is:")
Int
2 (TyCon -> [Type] -> SDoc
pprTypeApp TyCon
fam_tc ((Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Type
expandTypeSynonyms [Type]
pats))
checkValidTypePats :: TyCon -> [Type] -> TcM ()
checkValidTypePats :: TyCon -> [Type] -> TcM ()
checkValidTypePats TyCon
tc [Type]
pat_ty_args
= do {
(Type -> TcM ()) -> [Type] -> TcM ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ Type -> TcM ()
checkValidMonoType [Type]
pat_ty_args
; case TyCon -> [Type] -> [(Bool, TyCon, [Type])]
tcTyConAppTyFamInstsAndVis TyCon
tc [Type]
pat_ty_args of
[] -> () -> TcM ()
forall 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
$ DiagnosticMessage -> TcRnMessage
forall a.
(Diagnostic a, Typeable a, DiagnosticOpts a ~ NoDiagnosticOpts) =>
a -> TcRnMessage
mkTcRnUnknownMessage (DiagnosticMessage -> TcRnMessage)
-> DiagnosticMessage -> TcRnMessage
forall a b. (a -> b) -> a -> b
$ [GhcHint] -> SDoc -> DiagnosticMessage
mkPlainError [GhcHint]
noHints (SDoc -> DiagnosticMessage) -> SDoc -> DiagnosticMessage
forall a b. (a -> b) -> a -> b
$
Bool -> Type -> SDoc
ty_fam_inst_illegal_err Bool
tf_is_invis_arg
(TyCon -> [Type] -> Type
mkTyConApp TyCon
tf_tc [Type]
tf_args) }
where
inst_ty :: Type
inst_ty = TyCon -> [Type] -> Type
mkTyConApp TyCon
tc [Type]
pat_ty_args
ty_fam_inst_illegal_err :: Bool -> Type -> SDoc
ty_fam_inst_illegal_err :: Bool -> Type -> SDoc
ty_fam_inst_illegal_err Bool
invis_arg Type
ty
= Bool -> SDoc -> SDoc
pprWithExplicitKindsWhen Bool
invis_arg (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Illegal type synonym family application"
SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc -> SDoc
quotes (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
"in instance" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> SDoc
forall doc. IsLine doc => doc
colon)
Int
2 (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
inst_ty)
inaccessibleCoAxBranch :: TyCon -> CoAxBranch -> SDoc
inaccessibleCoAxBranch :: TyCon -> CoAxBranch -> SDoc
inaccessibleCoAxBranch TyCon
fam_tc CoAxBranch
cur_branch
= String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Type family instance equation is overlapped:" SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$
Int -> SDoc -> SDoc
nest Int
2 (TyCon -> CoAxBranch -> SDoc
pprCoAxBranchUser TyCon
fam_tc CoAxBranch
cur_branch)
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)
(Name -> Name -> TcRnMessage
TcRnBadAssociatedType (Class -> Name
className Class
clas) (TyCon -> Name
tyConName 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] ]
pp_wrong_at_arg :: ForAllTyFlag -> SDoc
pp_wrong_at_arg ForAllTyFlag
vis
= Bool -> SDoc -> SDoc
pprWithExplicitKindsWhen (ForAllTyFlag -> Bool
isInvisibleForAllTyFlag ForAllTyFlag
vis) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Type indexes must match class instance head"
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Expected:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
pp_expected_ty
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
" Actual:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
pp_actual_ty ]
(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)
pp_expected_ty :: SDoc
pp_expected_ty = PprPrec -> IfaceTyCon -> IfaceAppArgs -> SDoc
pprIfaceTypeApp PprPrec
topPrec (TyCon -> IfaceTyCon
toIfaceTyCon TyCon
fam_tc) (IfaceAppArgs -> SDoc) -> IfaceAppArgs -> SDoc
forall a b. (a -> b) -> a -> b
$
TyCon -> [Type] -> IfaceAppArgs
toIfaceTcArgs TyCon
fam_tc ([Type] -> IfaceAppArgs) -> [Type] -> IfaceAppArgs
forall a b. (a -> b) -> a -> b
$
[ case VarEnv Type -> 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 ]
pp_actual_ty :: SDoc
pp_actual_ty = PprPrec -> IfaceTyCon -> IfaceAppArgs -> SDoc
pprIfaceTypeApp PprPrec
topPrec (TyCon -> IfaceTyCon
toIfaceTyCon TyCon
fam_tc) (IfaceAppArgs -> SDoc) -> IfaceAppArgs -> SDoc
forall a b. (a -> b) -> a -> b
$
TyCon -> [Type] -> IfaceAppArgs
toIfaceTcArgs TyCon
fam_tc ([Type] -> IfaceAppArgs) -> [Type] -> IfaceAppArgs
forall a b. (a -> b) -> a -> b
$
TidyEnv -> [Type] -> [Type]
tidyTypes TidyEnv
tidy_env2 [Type]
ax_arg_tys
mk_wildcard :: 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 (DiagnosticMessage -> TcRnMessage
forall a.
(Diagnostic a, Typeable a, DiagnosticOpts a ~ NoDiagnosticOpts) =>
a -> TcRnMessage
mkTcRnUnknownMessage (DiagnosticMessage -> TcRnMessage)
-> DiagnosticMessage -> TcRnMessage
forall a b. (a -> b) -> a -> b
$ [GhcHint] -> SDoc -> DiagnosticMessage
mkPlainError [GhcHint]
noHints (SDoc -> DiagnosticMessage) -> SDoc -> DiagnosticMessage
forall a b. (a -> b) -> a -> b
$ ForAllTyFlag -> SDoc
pp_wrong_at_arg ForAllTyFlag
vis)
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
$ DiagnosticMessage -> TcRnMessage
forall a.
(Diagnostic a, Typeable a, DiagnosticOpts a ~ NoDiagnosticOpts) =>
a -> TcRnMessage
mkTcRnUnknownMessage (DiagnosticMessage -> TcRnMessage)
-> DiagnosticMessage -> TcRnMessage
forall a b. (a -> b) -> a -> b
$ [GhcHint] -> SDoc -> DiagnosticMessage
mkPlainError [GhcHint]
noHints (SDoc -> DiagnosticMessage) -> SDoc -> DiagnosticMessage
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"The kind of" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc -> SDoc
quotes (TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tc) SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"is ill-scoped")
Int
2 SDoc
pp_tc_kind
, SDoc
extra
, SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Perhaps try this order instead:")
Int
2 ([Var] -> SDoc
pprTyVars [Var]
sorted_tvs) ]
| 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
tvs :: [Var]
tvs = [VarBndr Var TyConBndrVis] -> [Var]
forall tv argf. [VarBndr tv argf] -> [tv]
binderVars [VarBndr Var TyConBndrVis]
tcbs
sorted_tvs :: [Var]
sorted_tvs = [Var] -> [Var]
scopedSort [Var]
tvs
(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)
inferred_tvs :: [Var]
inferred_tvs = [ VarBndr Var TyConBndrVis -> Var
forall tv argf. VarBndr tv argf -> tv
binderVar VarBndr Var TyConBndrVis
tcb
| VarBndr Var TyConBndrVis
tcb <- [VarBndr Var TyConBndrVis]
tcbs, ForAllTyFlag
Inferred ForAllTyFlag -> ForAllTyFlag -> Bool
forall a. Eq a => a -> a -> Bool
== VarBndr Var TyConBndrVis -> ForAllTyFlag
tyConBinderForAllTyFlag VarBndr Var TyConBndrVis
tcb ]
specified_tvs :: [Var]
specified_tvs = [ VarBndr Var TyConBndrVis -> Var
forall tv argf. VarBndr tv argf -> tv
binderVar VarBndr Var TyConBndrVis
tcb
| VarBndr Var TyConBndrVis
tcb <- [VarBndr Var TyConBndrVis]
tcbs, ForAllTyFlag
Specified ForAllTyFlag -> ForAllTyFlag -> Bool
forall a. Eq a => a -> a -> Bool
== VarBndr Var TyConBndrVis -> ForAllTyFlag
tyConBinderForAllTyFlag VarBndr Var TyConBndrVis
tcb ]
pp_inf :: SDoc
pp_inf = SDoc -> SDoc
forall doc. IsLine doc => doc -> doc
parens (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"namely:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Var] -> SDoc
pprTyVars [Var]
inferred_tvs)
pp_spec :: SDoc
pp_spec = SDoc -> SDoc
forall doc. IsLine doc => doc -> doc
parens (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"namely:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Var] -> SDoc
pprTyVars [Var]
specified_tvs)
pp_tc_kind :: SDoc
pp_tc_kind = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Inferred kind:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tc SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
ppr_untidy (TyCon -> Type
tyConKind TyCon
tc)
ppr_untidy :: Type -> SDoc
ppr_untidy Type
ty = IfaceType -> SDoc
pprIfaceType (Type -> IfaceType
toIfaceType Type
ty)
extra :: SDoc
extra
| [Var] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Var]
inferred_tvs Bool -> Bool -> Bool
&& [Var] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Var]
specified_tvs
= SDoc
forall doc. IsOutput doc => doc
empty
| [Var] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Var]
inferred_tvs
= SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"NB: Specified variables")
Int
2 ([SDoc] -> SDoc
forall doc. IsLine doc => [doc] -> doc
sep [SDoc
pp_spec, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"always come first"])
| [Var] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Var]
specified_tvs
= SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"NB: Inferred variables")
Int
2 ([SDoc] -> SDoc
forall doc. IsLine doc => [doc] -> doc
sep [SDoc
pp_inf, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"always come first"])
| Bool
otherwise
= SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"NB: Inferred variables")
Int
2 ([SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ [SDoc] -> SDoc
forall doc. IsLine doc => [doc] -> doc
sep [ SDoc
pp_inf, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"always come first"]
, [SDoc] -> SDoc
forall doc. IsLine doc => [doc] -> doc
sep [String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"then Specified variables", SDoc
pp_spec]])