TcTyVar, TcKind, TcType, TcTauType, TcThetaType, TcRhoType, TcTyVarSet,
--------------------------------
- -- Find the type to which a type variable is bound
- tcPutTyVar, -- :: TcTyVar -> TcType -> NF_TcM TcType
- tcGetTyVar, -- :: TcTyVar -> NF_TcM (Maybe TcType) does shorting out
-
- --------------------------------
-- Creating new mutable type variables
newTyVar,
newTyVarTy, -- Kind -> NF_TcM TcType
tcSplitRhoTyM,
--------------------------------
+ -- Checking type validity
+ Rank, UserTypeCtxt(..), checkValidType, pprUserTypeCtxt,
+ SourceTyCtxt(..), checkValidTheta,
+ checkValidInstHead, instTypeErr,
+
+ --------------------------------
-- Unification
unifyTauTy, unifyTauTyList, unifyTauTyLists,
unifyFunTy, unifyListTy, unifyTupleTy,
-- friends:
-import TypeRep ( Type(..), Kind, TyNote(..) ) -- friend
-import Type -- Lots and lots
-import TcType ( SigmaType, RhoType, tcEqType,
+import TypeRep ( Type(..), SourceType(..), TyNote(..), -- Friend; can see representation
+ Kind, TauType, ThetaType,
+ openKindCon, typeCon
+ )
+import TcType ( tcEqType, tcCmpPred,
tcSplitRhoTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe,
- tcSplitTyConApp_maybe, tcSplitFunTy_maybe
+ tcSplitTyConApp_maybe, tcSplitFunTy_maybe, tcSplitForAllTys,
+ tcGetTyVar, tcIsTyVarTy, tcSplitSigmaTy, isUnLiftedType, isIPPred,
+
+ mkAppTy, mkTyVarTy, mkTyVarTys, mkFunTy, mkTyConApp,
+ tyVarsOfPred, getClassPredTys_maybe,
+
+ liftedTypeKind, unliftedTypeKind, openTypeKind, defaultKind, superKind,
+ superBoxity, liftedBoxity, hasMoreBoxityInfo, typeKind,
+ tyVarsOfType, tyVarsOfTypes, tidyOpenType, tidyOpenTypes, tidyTyVar,
+ eqKind, isTypeKind,
+
+ isFFIArgumentTy, isFFIImportResultTy
)
-import PprType ( pprType )
import Subst ( Subst, mkTopTyVarSubst, substTy )
-import TyCon ( TyCon, mkPrimTyCon, isNewTyCon, isSynTyCon, isTupleTyCon,
- tyConArity, tupleTyConBoxity
- )
+import Class ( classArity, className )
+import TyCon ( TyCon, mkPrimTyCon, isSynTyCon, isUnboxedTupleTyCon,
+ isTupleTyCon, tyConArity, tupleTyConBoxity, tyConName )
import PrimRep ( PrimRep(VoidRep) )
import Var ( TyVar, varName, tyVarKind, tyVarName, isTyVar, mkTyVar,
isMutTyVar, isSigTyVar )
-- others:
import TcMonad -- TcType, amongst others
import TysWiredIn ( voidTy, listTyCon, mkListTy, mkTupleTy )
-
+import PrelNames ( cCallableClassKey, cReturnableClassKey, hasKey )
+import ForeignCall ( Safety(..) )
+import FunDeps ( grow )
+import PprType ( pprPred, pprSourceType, pprTheta, pprClassPred )
import Name ( Name, NamedThing(..), setNameUnique, mkSysLocalName,
mkLocalName, mkDerivedTyConOcc, isSystemName
)
-import PrelNames ( floatTyConKey, doubleTyConKey, foreignPtrTyConKey,
- integerTyConKey, intTyConKey, addrTyConKey )
import VarSet
import BasicTypes ( Boxity, Arity, isBoxed )
-import Unique ( Unique, Uniquable(..) )
+import CmdLineOpts ( dopt, DynFlag(..) )
+import Unique ( Uniquable(..) )
import SrcLoc ( noSrcLoc )
import Util ( nOfThem )
+import ListSetOps ( removeDups )
import Outputable
\end{code}
Just pair -> go res res (pair:ts)
Nothing -> returnNF_Tc (reverse ts, syn_t)
go syn_t (NoteTy n t) ts = go syn_t t ts
- go syn_t (TyVarTy tv) ts = tcGetTyVar tv `thenNF_Tc` \ maybe_ty ->
+ go syn_t (TyVarTy tv) ts = getTcTyVar tv `thenNF_Tc` \ maybe_ty ->
case maybe_ty of
- Just ty | not (isTyVarTy ty) -> go syn_t ty ts
- other -> returnNF_Tc (reverse ts, syn_t)
+ Just ty | not (tcIsTyVarTy ty) -> go syn_t ty ts
+ other -> returnNF_Tc (reverse ts, syn_t)
go syn_t (UsageTy _ t) ts = go syn_t t ts
go syn_t t ts = returnNF_Tc (reverse ts, syn_t)
\end{code}
\begin{code}
tcInstType :: TcType -> NF_TcM ([TcTyVar], TcThetaType, TcType)
tcInstType ty
- = case splitForAllTys ty of
+ = case tcSplitForAllTys ty of
([], rho) -> -- There may be overloading but no type variables;
-- (?x :: Int) => Int -> Int
let
%************************************************************************
\begin{code}
-tcPutTyVar :: TcTyVar -> TcType -> NF_TcM TcType
-tcGetTyVar :: TcTyVar -> NF_TcM (Maybe TcType)
+putTcTyVar :: TcTyVar -> TcType -> NF_TcM TcType
+getTcTyVar :: TcTyVar -> NF_TcM (Maybe TcType)
\end{code}
Putting is easy:
\begin{code}
-tcPutTyVar tyvar ty
+putTcTyVar tyvar ty
| not (isMutTyVar tyvar)
- = pprTrace "tcPutTyVar" (ppr tyvar) $
+ = pprTrace "putTcTyVar" (ppr tyvar) $
returnNF_Tc ty
| otherwise
Getting is more interesting. The easy thing to do is just to read, thus:
\begin{verbatim}
-tcGetTyVar tyvar = tcReadMutTyVar tyvar
+getTcTyVar tyvar = tcReadMutTyVar tyvar
\end{verbatim}
But it's more fun to short out indirections on the way: If this
We return Nothing iff the original box was unbound.
\begin{code}
-tcGetTyVar tyvar
+getTcTyVar tyvar
| not (isMutTyVar tyvar)
- = pprTrace "tcGetTyVar" (ppr tyvar) $
+ = pprTrace "getTcTyVar" (ppr tyvar) $
returnNF_Tc (Just (mkTyVarTy tyvar))
| otherwise
-- that is overkill, so we use this simpler chap
zonkTcSigTyVars tyvars
= zonkTcTyVars tyvars `thenNF_Tc` \ tys ->
- returnNF_Tc (map (getTyVar "zonkTcSigTyVars") tys)
+ returnNF_Tc (map (tcGetTyVar "zonkTcSigTyVars") tys)
\end{code}
----------------- Types
-- When zonking a kind, we want to
-- zonk a *kind* variable to (Type *)
-- zonk a *boxity* variable to *
- zonk_unbound_kind_var kv | tyVarKind kv `eqKind` superKind = tcPutTyVar kv liftedTypeKind
- | tyVarKind kv `eqKind` superBoxity = tcPutTyVar kv liftedBoxity
+ zonk_unbound_kind_var kv | tyVarKind kv `eqKind` superKind = putTcTyVar kv liftedTypeKind
+ | tyVarKind kv `eqKind` superBoxity = putTcTyVar kv liftedBoxity
| otherwise = pprPanic "zonkKindEnv" (ppr kv)
zonkTcTypeToType :: TcType -> NF_TcM Type
-- Zonk a mutable but unbound type variable to
-- Void if it has kind Lifted
-- :Void otherwise
+ -- We know it's unbound even though we don't carry an environment,
+ -- because at the binding site for a type variable we bind the
+ -- mutable tyvar to a fresh immutable one. So the mutable store
+ -- plays the role of an environment. If we come across a mutable
+ -- type variable that isn't so bound, it must be completely free.
zonk_unbound_tyvar tv
| kind `eqKind` liftedTypeKind || kind `eqKind` openTypeKind
- = tcPutTyVar tv voidTy -- Just to avoid creating a new tycon in
+ = putTcTyVar tv voidTy -- Just to avoid creating a new tycon in
-- this vastly common case
| otherwise
- = tcPutTyVar tv (TyConApp (mk_void_tycon tv kind) [])
+ = putTcTyVar tv (TyConApp (mk_void_tycon tv kind) [])
where
kind = tyVarKind tv
immut_tv = mkTyVar (tyVarName tv) (defaultKind (tyVarKind tv))
immut_tv_ty = mkTyVarTy immut_tv
- zap tv = tcPutTyVar tv immut_tv_ty
+ zap tv = putTcTyVar tv immut_tv_ty
-- Bind the mutable version to the immutable one
in
-- If the type variable is mutable, then bind it to immut_tv_ty
go (UsageTy u ty) = go u `thenNF_Tc` \ u' ->
go ty `thenNF_Tc` \ ty' ->
- returnNF_Tc (mkUTy u' ty')
+ returnNF_Tc (UsageTy u' ty')
-- The two interesting cases!
go (TyVarTy tyvar) = zonkTyVar unbound_var_fn tyvar
returnNF_Tc (TyVarTy tyvar)
| otherwise
- = tcGetTyVar tyvar `thenNF_Tc` \ maybe_ty ->
+ = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
case maybe_ty of
Nothing -> unbound_var_fn tyvar -- Mutable and unbound
Just other_ty -> zonkType unbound_var_fn other_ty -- Bound
%************************************************************************
%* *
-\subsection{The Kind variants}
+\subsection{Checking a user type}
+%* *
+%************************************************************************
+
+When dealing with a user-written type, we first translate it from an HsType
+to a Type, performing kind checking, and then check various things that should
+be true about it. We don't want to perform these checks at the same time
+as the initial translation because (a) they are unnecessary for interface-file
+types and (b) when checking a mutually recursive group of type and class decls,
+we can't "look" at the tycons/classes yet.
+
+One thing we check for is 'rank'.
+
+ Rank 0: monotypes (no foralls)
+ Rank 1: foralls at the front only, Rank 0 inside
+ Rank 2: foralls at the front, Rank 1 on left of fn arrow,
+
+ basic ::= tyvar | T basic ... basic
+
+ r2 ::= forall tvs. cxt => r2a
+ r2a ::= r1 -> r2a | basic
+ r1 ::= forall tvs. cxt => r0
+ r0 ::= r0 -> r0 | basic
+
+
+\begin{code}
+data UserTypeCtxt
+ = FunSigCtxt Name -- Function type signature
+ | ExprSigCtxt -- Expression type signature
+ | ConArgCtxt Name -- Data constructor argument
+ | TySynCtxt Name -- RHS of a type synonym decl
+ | GenPatCtxt -- Pattern in generic decl
+ -- f{| a+b |} (Inl x) = ...
+ | PatSigCtxt -- Type sig in pattern
+ -- f (x::t) = ...
+ | ResSigCtxt -- Result type sig
+ -- f x :: t = ....
+ | ForSigCtxt Name -- Foreign inport or export signature
+ | RuleSigCtxt Name -- Signature on a forall'd variable in a RULE
+
+-- Notes re TySynCtxt
+-- We allow type synonyms that aren't types; e.g. type List = []
+--
+-- If the RHS mentions tyvars that aren't in scope, we'll
+-- quantify over them:
+-- e.g. type T = a->a
+-- will become type T = forall a. a->a
+--
+-- With gla-exts that's right, but for H98 we should complain.
+
+
+pprUserTypeCtxt (FunSigCtxt n) = ptext SLIT("the type signature for") <+> quotes (ppr n)
+pprUserTypeCtxt ExprSigCtxt = ptext SLIT("an expression type signature")
+pprUserTypeCtxt (ConArgCtxt c) = ptext SLIT("the type of constructor") <+> quotes (ppr c)
+pprUserTypeCtxt (TySynCtxt c) = ptext SLIT("the RHS of a type synonym declaration") <+> quotes (ppr c)
+pprUserTypeCtxt GenPatCtxt = ptext SLIT("the type pattern of a generic definition")
+pprUserTypeCtxt PatSigCtxt = ptext SLIT("a pattern type signature")
+pprUserTypeCtxt ResSigCtxt = ptext SLIT("a result type signature")
+pprUserTypeCtxt (ForSigCtxt n) = ptext SLIT("the foreign signature for") <+> quotes (ppr n)
+pprUserTypeCtxt (RuleSigCtxt n) = ptext SLIT("the type signature on") <+> quotes (ppr n)
+\end{code}
+
+\begin{code}
+checkValidType :: UserTypeCtxt -> Type -> TcM ()
+-- Checks that the type is valid for the given context
+checkValidType ctxt ty
+ = doptsTc Opt_GlasgowExts `thenNF_Tc` \ gla_exts ->
+ let
+ rank = case ctxt of
+ GenPatCtxt -> 0
+ PatSigCtxt -> 0
+ ResSigCtxt -> 0
+ ExprSigCtxt -> 1
+ FunSigCtxt _ | gla_exts -> 2
+ | otherwise -> 1
+ ConArgCtxt _ | gla_exts -> 2 -- We are given the type of the entire
+ | otherwise -> 1 -- constructor; hence rank 1 is ok
+ TySynCtxt _ | gla_exts -> 1
+ | otherwise -> 0
+ ForSigCtxt _ -> 1
+ RuleSigCtxt _ -> 1
+
+ actual_kind = typeKind ty
+
+ actual_kind_is_lifted = actual_kind `eqKind` liftedTypeKind
+
+ kind_ok = case ctxt of
+ TySynCtxt _ -> True -- Any kind will do
+ GenPatCtxt -> actual_kind_is_lifted
+ ForSigCtxt _ -> actual_kind_is_lifted
+ other -> isTypeKind actual_kind
+ in
+ tcAddErrCtxt (checkTypeCtxt ctxt ty) $
+
+ -- Check that the thing has kind Type, and is lifted if necessary
+ checkTc kind_ok (kindErr actual_kind) `thenTc_`
+
+ -- Check the internal validity of the type itself
+ check_poly_type rank ty
+
+
+checkTypeCtxt ctxt ty
+ = vcat [ptext SLIT("In the type:") <+> ppr_ty ty,
+ ptext SLIT("While checking") <+> pprUserTypeCtxt ctxt ]
+
+ -- Hack alert. If there are no tyvars, (ppr sigma_ty) will print
+ -- something strange like {Eq k} -> k -> k, because there is no
+ -- ForAll at the top of the type. Since this is going to the user
+ -- we want it to look like a proper Haskell type even then; hence the hack
+ --
+ -- This shows up in the complaint about
+ -- case C a where
+ -- op :: Eq a => a -> a
+ppr_ty ty | null forall_tvs && not (null theta) = pprTheta theta <+> ptext SLIT("=>") <+> ppr tau
+ | otherwise = ppr ty
+ where
+ (forall_tvs, theta, tau) = tcSplitSigmaTy ty
+\end{code}
+
+
+\begin{code}
+type Rank = Int
+check_poly_type :: Rank -> Type -> TcM ()
+check_poly_type rank ty
+ | rank == 0
+ = check_tau_type 0 False ty
+ | otherwise -- rank > 0
+ = let
+ (tvs, theta, tau) = tcSplitSigmaTy ty
+ in
+ check_valid_theta SigmaCtxt theta `thenTc_`
+ check_tau_type (rank-1) False tau `thenTc_`
+ checkAmbiguity tvs theta tau
+
+----------------------------------------
+check_arg_type :: Type -> TcM ()
+-- The sort of type that can instantiate a type variable,
+-- or be the argument of a type constructor.
+-- Not an unboxed tuple, not a forall.
+-- Other unboxed types are very occasionally allowed as type
+-- arguments depending on the kind of the type constructor
+--
+-- For example, we want to reject things like:
+--
+-- instance Ord a => Ord (forall s. T s a)
+-- and
+-- g :: T s (forall b.b)
+--
+-- NB: unboxed tuples can have polymorphic or unboxed args.
+-- This happens in the workers for functions returning
+-- product types with polymorphic components.
+-- But not in user code
+--
+-- Question: what about nested unboxed tuples?
+-- Currently rejected.
+check_arg_type ty
+ = check_tau_type 0 False ty `thenTc_`
+ checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
+
+----------------------------------------
+check_tau_type :: Rank -> Bool -> Type -> TcM ()
+-- Rank is allowed rank for function args
+-- No foralls otherwise
+-- Bool is True iff unboxed tuple are allowed here
+
+check_tau_type rank ubx_tup_ok ty@(UsageTy _ _) = failWithTc (usageTyErr ty)
+check_tau_type rank ubx_tup_ok ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
+check_tau_type rank ubx_tup_ok (SourceTy sty) = getDOptsTc `thenNF_Tc` \ dflags ->
+ check_source_ty dflags TypeCtxt sty
+check_tau_type rank ubx_tup_ok (TyVarTy _) = returnTc ()
+check_tau_type rank ubx_tup_ok ty@(FunTy arg_ty res_ty)
+ = check_poly_type rank arg_ty `thenTc_`
+ check_tau_type rank True res_ty
+
+check_tau_type rank ubx_tup_ok (AppTy ty1 ty2)
+ = check_arg_type ty1 `thenTc_` check_arg_type ty2
+
+check_tau_type rank ubx_tup_ok (NoteTy note ty)
+ = check_note note `thenTc_` check_tau_type rank ubx_tup_ok ty
+
+check_tau_type rank ubx_tup_ok ty@(TyConApp tc tys)
+ | isSynTyCon tc
+ = checkTc syn_arity_ok arity_msg `thenTc_`
+ mapTc_ check_arg_type tys
+
+ | isUnboxedTupleTyCon tc
+ = checkTc ubx_tup_ok ubx_tup_msg `thenTc_`
+ mapTc_ (check_tau_type 0 True) tys -- Args are allowed to be unlifted, or
+ -- more unboxed tuples, so can't use check_arg_ty
+
+ | otherwise
+ = mapTc_ check_arg_type tys
+
+ where
+ syn_arity_ok = tc_arity <= n_args
+ -- It's OK to have an *over-applied* type synonym
+ -- data Tree a b = ...
+ -- type Foo a = Tree [a]
+ -- f :: Foo a b -> ...
+ n_args = length tys
+ tc_arity = tyConArity tc
+
+ arity_msg = arityErr "Type synonym" (tyConName tc) tc_arity n_args
+ ubx_tup_msg = ubxArgTyErr ty
+
+----------------------------------------
+check_note (FTVNote _) = returnTc ()
+check_note (SynNote ty) = check_tau_type 0 False ty
+\end{code}
+
+Check for ambiguity
+~~~~~~~~~~~~~~~~~~~
+ forall V. P => tau
+is ambiguous if P contains generic variables
+(i.e. one of the Vs) that are not mentioned in tau
+
+However, we need to take account of functional dependencies
+when we speak of 'mentioned in tau'. Example:
+ class C a b | a -> b where ...
+Then the type
+ forall x y. (C x y) => x
+is not ambiguous because x is mentioned and x determines y
+
+NOTE: In addition, GHC insists that at least one type variable
+in each constraint is in V. So we disallow a type like
+ forall a. Eq b => b -> b
+even in a scope where b is in scope.
+This is the is_free test below.
+
+NB; the ambiguity check is only used for *user* types, not for types
+coming from inteface files. The latter can legitimately have
+ambiguous types. Example
+
+ class S a where s :: a -> (Int,Int)
+ instance S Char where s _ = (1,1)
+ f:: S a => [a] -> Int -> (Int,Int)
+ f (_::[a]) x = (a*x,b)
+ where (a,b) = s (undefined::a)
+
+Here the worker for f gets the type
+ fw :: forall a. S a => Int -> (# Int, Int #)
+
+If the list of tv_names is empty, we have a monotype, and then we
+don't need to check for ambiguity either, because the test can't fail
+(see is_ambig).
+
+\begin{code}
+checkAmbiguity :: [TyVar] -> ThetaType -> TauType -> TcM ()
+checkAmbiguity forall_tyvars theta tau
+ = mapTc_ check_pred theta `thenTc_`
+ returnTc ()
+ where
+ tau_vars = tyVarsOfType tau
+ extended_tau_vars = grow theta tau_vars
+
+ is_ambig ct_var = (ct_var `elem` forall_tyvars) &&
+ not (ct_var `elemVarSet` extended_tau_vars)
+ is_free ct_var = not (ct_var `elem` forall_tyvars)
+
+ check_pred pred = checkTc (not any_ambig) (ambigErr pred) `thenTc_`
+ checkTc (isIPPred pred || not all_free) (freeErr pred)
+ where
+ ct_vars = varSetElems (tyVarsOfPred pred)
+ all_free = all is_free ct_vars
+ any_ambig = any is_ambig ct_vars
+\end{code}
+
+\begin{code}
+ambigErr pred
+ = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
+ nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
+ ptext SLIT("must be reachable from the type after the =>"))]
+
+
+freeErr pred
+ = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
+ ptext SLIT("are already in scope"),
+ nest 4 (ptext SLIT("At least one must be universally quantified here"))
+ ]
+
+forAllTyErr ty = ptext SLIT("Illegal polymorphic type:") <+> ppr_ty ty
+usageTyErr ty = ptext SLIT("Illegal usage type:") <+> ppr_ty ty
+unliftedArgErr ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr_ty ty
+ubxArgTyErr ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr_ty ty
+kindErr kind = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
+\end{code}
+
+%************************************************************************
+%* *
+\subsection{Checking a theta or source type}
+%* *
+%************************************************************************
+
+\begin{code}
+data SourceTyCtxt
+ = ClassSCCtxt Name -- Superclasses of clas
+ | SigmaCtxt -- Context of a normal for-all type
+ | DataTyCtxt Name -- Context of a data decl
+ | TypeCtxt -- Source type in an ordinary type
+ | InstThetaCtxt -- Context of an instance decl
+ | InstHeadCtxt -- Head of an instance decl
+
+pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
+pprSourceTyCtxt SigmaCtxt = ptext SLIT("the context of a polymorphic type")
+pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
+pprSourceTyCtxt InstThetaCtxt = ptext SLIT("the context of an instance declaration")
+pprSourceTyCtxt InstHeadCtxt = ptext SLIT("the head of an instance declaration")
+pprSourceTyCtxt TypeCtxt = ptext SLIT("the context of a type")
+\end{code}
+
+\begin{code}
+checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
+checkValidTheta ctxt theta
+ = tcAddErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
+
+-------------------------
+check_valid_theta ctxt []
+ = returnTc ()
+check_valid_theta ctxt theta
+ = getDOptsTc `thenNF_Tc` \ dflags ->
+ warnTc (not (null dups)) (dupPredWarn dups) `thenNF_Tc_`
+ mapTc_ (check_source_ty dflags ctxt) theta
+ where
+ (_,dups) = removeDups tcCmpPred theta
+
+-------------------------
+check_source_ty dflags ctxt pred@(ClassP cls tys)
+ = -- Class predicates are valid in all contexts
+ mapTc_ check_arg_type tys `thenTc_`
+ checkTc (arity == n_tys) arity_err `thenTc_`
+ checkTc (all tyvar_head tys || arby_preds_ok) (predTyVarErr pred)
+
+ where
+ class_name = className cls
+ arity = classArity cls
+ n_tys = length tys
+ arity_err = arityErr "Class" class_name arity n_tys
+
+ arby_preds_ok = case ctxt of
+ InstHeadCtxt -> True -- We check for instance-head formation
+ -- in checkValidInstHead
+ InstThetaCtxt -> dopt Opt_AllowUndecidableInstances dflags
+ other -> dopt Opt_GlasgowExts dflags
+
+check_source_ty dflags SigmaCtxt (IParam name ty) = check_arg_type ty
+check_source_ty dflags TypeCtxt (NType tc tys) = mapTc_ check_arg_type tys
+
+-- Catch-all
+check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
+
+-------------------------
+tyvar_head ty -- Haskell 98 allows predicates of form
+ | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
+ | otherwise -- where a is a type variable
+ = case tcSplitAppTy_maybe ty of
+ Just (ty, _) -> tyvar_head ty
+ Nothing -> False
+\end{code}
+
+\begin{code}
+badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprSourceType sty
+predTyVarErr pred = ptext SLIT("Non-type variables in constraint:") <+> pprPred pred
+dupPredWarn dups = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
+
+checkThetaCtxt ctxt theta
+ = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
+ ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
+\end{code}
+
+
+%************************************************************************
+%* *
+\subsection{Checking for a decent instance head type}
+%* *
+%************************************************************************
+
+@checkValidInstHead@ checks the type {\em and} its syntactic constraints:
+it must normally look like: @instance Foo (Tycon a b c ...) ...@
+
+The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
+flag is on, or (2)~the instance is imported (they must have been
+compiled elsewhere). In these cases, we let them go through anyway.
+
+We can also have instances for functions: @instance Foo (a -> b) ...@.
+
+\begin{code}
+checkValidInstHead :: Type -> TcM ()
+
+checkValidInstHead ty -- Should be a source type
+ = case tcSplitPredTy_maybe ty of {
+ Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
+ Just pred ->
+
+ case getClassPredTys_maybe pred of {
+ Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
+ Just (clas,tys) ->
+
+ getDOptsTc `thenNF_Tc` \ dflags ->
+ mapTc_ check_arg_type tys `thenTc_`
+ check_inst_head dflags clas tys
+ }}
+
+check_inst_head dflags clas tys
+ | -- CCALL CHECK
+ -- A user declaration of a CCallable/CReturnable instance
+ -- must be for a "boxed primitive" type.
+ (clas `hasKey` cCallableClassKey
+ && not (ccallable_type first_ty))
+ || (clas `hasKey` cReturnableClassKey
+ && not (creturnable_type first_ty))
+ = failWithTc (nonBoxedPrimCCallErr clas first_ty)
+
+ -- If GlasgowExts then check at least one isn't a type variable
+ | dopt Opt_GlasgowExts dflags
+ = check_tyvars dflags clas tys
+
+ -- WITH HASKELL 1.4, MUST HAVE C (T a b c)
+ | length tys == 1,
+ Just (tycon, arg_tys) <- tcSplitTyConApp_maybe first_ty,
+ not (isSynTyCon tycon), -- ...but not a synonym
+ all tcIsTyVarTy arg_tys, -- Applied to type variables
+ length (varSetElems (tyVarsOfTypes arg_tys)) == length arg_tys
+ -- This last condition checks that all the type variables are distinct
+ = returnTc ()
+
+ | otherwise
+ = failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg)
+
+ where
+ (first_ty : _) = tys
+
+ ccallable_type ty = isFFIArgumentTy dflags PlayRisky ty
+ creturnable_type ty = isFFIImportResultTy dflags ty
+
+ head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
+ text "where T is not a synonym, and a,b,c are distinct type variables")
+
+check_tyvars dflags clas tys
+ -- Check that at least one isn't a type variable
+ -- unless -fallow-undecideable-instances
+ | dopt Opt_AllowUndecidableInstances dflags = returnTc ()
+ | not (all tcIsTyVarTy tys) = returnTc ()
+ | otherwise = failWithTc (instTypeErr (pprClassPred clas tys) msg)
+ where
+ msg = parens (ptext SLIT("There must be at least one non-type-variable in the instance head")
+ $$ ptext SLIT("Use -fallow-undecidable-instances to lift this restriction"))
+\end{code}
+
+\begin{code}
+instTypeErr pp_ty msg
+ = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,
+ nest 4 msg]
+
+nonBoxedPrimCCallErr clas inst_ty
+ = hang (ptext SLIT("Unacceptable instance type for ccall-ish class"))
+ 4 (pprClassPred clas [inst_ty])
+\end{code}
+
+
+%************************************************************************
+%* *
+\subsection{Kind unification}
%* *
%************************************************************************
-- for some boxity bx
unifyOpenTypeKind ty@(TyVarTy tyvar)
- = tcGetTyVar tyvar `thenNF_Tc` \ maybe_ty ->
+ = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
case maybe_ty of
Just ty' -> unifyOpenTypeKind ty'
other -> unify_open_kind_help ty
unifyOpenTypeKind ty
- = case tcSplitTyConApp_maybe ty of
- Just (tycon, [_]) | tycon == typeCon -> returnTc ()
- other -> unify_open_kind_help ty
+ | isTypeKind ty = returnTc ()
+ | otherwise = unify_open_kind_help ty
unify_open_kind_help ty -- Revert to ordinary unification
= newBoxityVar `thenNF_Tc` \ boxity ->
-> TcM ()
uVar swapped tv1 ps_ty2 ty2
- = tcGetTyVar tv1 `thenNF_Tc` \ maybe_ty1 ->
+ = getTcTyVar tv1 `thenNF_Tc` \ maybe_ty1 ->
case maybe_ty1 of
Just ty1 | swapped -> uTys ps_ty2 ty2 ty1 ty1 -- Swap back
| otherwise -> uTys ty1 ty1 ps_ty2 ty2 -- Same order
-- Distinct type variables
-- ASSERT maybe_ty1 /= Just
| otherwise
- = tcGetTyVar tv2 `thenNF_Tc` \ maybe_ty2 ->
+ = getTcTyVar tv2 `thenNF_Tc` \ maybe_ty2 ->
case maybe_ty2 of
Just ty2' -> uUnboundVar swapped tv1 maybe_ty1 ty2' ty2'
Nothing | update_tv2
-> WARN( not (k1 `hasMoreBoxityInfo` k2), (ppr tv1 <+> ppr k1) $$ (ppr tv2 <+> ppr k2) )
- tcPutTyVar tv2 (TyVarTy tv1) `thenNF_Tc_`
+ putTcTyVar tv2 (TyVarTy tv1) `thenNF_Tc_`
returnTc ()
| otherwise
-> WARN( not (k2 `hasMoreBoxityInfo` k1), (ppr tv2 <+> ppr k2) $$ (ppr tv1 <+> ppr k1) )
- (tcPutTyVar tv1 ps_ty2 `thenNF_Tc_`
+ (putTcTyVar tv1 ps_ty2 `thenNF_Tc_`
returnTc ())
where
k1 = tyVarKind tv1
-- That's why we have this two-state occurs-check
zonkTcType ps_ty2 `thenNF_Tc` \ ps_ty2' ->
if not (tv1 `elemVarSet` tyVarsOfType ps_ty2') then
- tcPutTyVar tv1 ps_ty2' `thenNF_Tc_`
+ putTcTyVar tv1 ps_ty2' `thenNF_Tc_`
returnTc ()
else
zonkTcType non_var_ty2 `thenNF_Tc` \ non_var_ty2' ->
if not (tv1 `elemVarSet` tyVarsOfType non_var_ty2') then
-- This branch rarely succeeds, except in strange cases
-- like that in the example above
- tcPutTyVar tv1 non_var_ty2' `thenNF_Tc_`
+ putTcTyVar tv1 non_var_ty2' `thenNF_Tc_`
returnTc ()
else
failWithTcM (unifyOccurCheck tv1 ps_ty2')
-> TcM (TcType, TcType) -- otherwise return arg and result types
unifyFunTy ty@(TyVarTy tyvar)
- = tcGetTyVar tyvar `thenNF_Tc` \ maybe_ty ->
+ = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
case maybe_ty of
Just ty' -> unifyFunTy ty'
other -> unify_fun_ty_help ty
-> TcM TcType -- list element type
unifyListTy ty@(TyVarTy tyvar)
- = tcGetTyVar tyvar `thenNF_Tc` \ maybe_ty ->
+ = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
case maybe_ty of
Just ty' -> unifyListTy ty'
other -> unify_list_ty_help ty
\begin{code}
unifyTupleTy :: Boxity -> Arity -> TcType -> TcM [TcType]
unifyTupleTy boxity arity ty@(TyVarTy tyvar)
- = tcGetTyVar tyvar `thenNF_Tc` \ maybe_ty ->
+ = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
case maybe_ty of
Just ty' -> unifyTupleTy boxity arity ty'
other -> unify_tuple_ty_help boxity arity ty
projects / ghc-hetmet.git / blobdiff