--------------------------------
-- Creating new mutable type variables
- newTyVar, newHoleTyVarTy,
+ newTyVar,
newTyVarTy, -- Kind -> NF_TcM TcType
newTyVarTys, -- Int -> Kind -> NF_TcM [TcType]
newKindVar, newKindVars, newBoxityVar,
putTcTyVar, getTcTyVar,
+ newHoleTyVarTy, readHoleResult, zapToType,
+
--------------------------------
-- Instantiation
- tcInstTyVar, tcInstTyVars,
- tcInstSigTyVars, tcInstType, tcInstSigType,
- tcSplitRhoTyM,
+ tcInstTyVar, tcInstTyVars, tcInstType,
--------------------------------
-- Checking type validity
Rank, UserTypeCtxt(..), checkValidType, pprUserTypeCtxt,
SourceTyCtxt(..), checkValidTheta,
- checkValidInstHead, instTypeErr,
+ checkValidInstHead, instTypeErr, checkAmbiguity,
--------------------------------
-- Zonking
- zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkTcSigTyVars,
+ zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV,
zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
zonkTcPredType, zonkTcTypeToType, zonkTcTyVarToTyVar, zonkKindEnv,
import TcType ( TcType, TcThetaType, TcTauType, TcPredType,
TcTyVarSet, TcKind, TcTyVar, TyVarDetails(..),
tcEqType, tcCmpPred,
- tcSplitRhoTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe,
+ tcSplitPhiTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe,
tcSplitTyConApp_maybe, tcSplitForAllTys,
- tcGetTyVar, tcIsTyVarTy, tcSplitSigmaTy,
- isUnLiftedType, isIPPred,
+ tcIsTyVarTy, tcSplitSigmaTy,
+ isUnLiftedType, isIPPred, isHoleTyVar,
mkAppTy, mkTyVarTy, mkTyVarTys,
tyVarsOfPred, getClassPredTys_maybe,
liftedTypeKind, openTypeKind, defaultKind, superKind,
superBoxity, liftedBoxity, typeKind,
tyVarsOfType, tyVarsOfTypes,
- eqKind, isTypeKind,
+ eqKind, isTypeKind, isAnyTypeKind,
isFFIArgumentTy, isFFIImportResultTy
)
+import qualified Type ( splitFunTys )
import Subst ( Subst, mkTopTyVarSubst, substTy )
import Class ( Class, classArity, className )
import TyCon ( TyCon, mkPrimTyCon, isSynTyCon, isUnboxedTupleTyCon,
- tyConArity, tyConName )
+ tyConArity, tyConName, tyConKind )
import PrimRep ( PrimRep(VoidRep) )
import Var ( TyVar, tyVarKind, tyVarName, isTyVar, mkTyVar, isMutTyVar )
-- others:
import TcMonad -- TcType, amongst others
-import TysWiredIn ( voidTy )
+import TysWiredIn ( voidTy, listTyCon, tupleTyCon )
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
+import Name ( Name, NamedThing(..), setNameUnique, mkSystemName,
+ mkInternalName, mkDerivedTyConOcc
)
import VarSet
+import BasicTypes ( Boxity(Boxed) )
import CmdLineOpts ( dopt, DynFlag(..) )
import Unique ( Uniquable(..) )
import SrcLoc ( noSrcLoc )
newTyVar :: Kind -> NF_TcM TcTyVar
newTyVar kind
= tcGetUnique `thenNF_Tc` \ uniq ->
- tcNewMutTyVar (mkSysLocalName uniq SLIT("t")) kind VanillaTv
+ tcNewMutTyVar (mkSystemName uniq FSLIT("t")) kind VanillaTv
newTyVarTy :: Kind -> NF_TcM TcType
newTyVarTy kind
= newTyVar kind `thenNF_Tc` \ tc_tyvar ->
returnNF_Tc (TyVarTy tc_tyvar)
-newHoleTyVarTy :: NF_TcM TcType
- = tcGetUnique `thenNF_Tc` \ uniq ->
- tcNewMutTyVar (mkSysLocalName uniq SLIT("h")) openTypeKind HoleTv `thenNF_Tc` \ tv ->
- returnNF_Tc (TyVarTy tv)
-
newTyVarTys :: Int -> Kind -> NF_TcM [TcType]
newTyVarTys n kind = mapNF_Tc newTyVarTy (nOfThem n kind)
newKindVar :: NF_TcM TcKind
newKindVar
= tcGetUnique `thenNF_Tc` \ uniq ->
- tcNewMutTyVar (mkSysLocalName uniq SLIT("k")) superKind VanillaTv `thenNF_Tc` \ kv ->
+ tcNewMutTyVar (mkSystemName uniq FSLIT("k")) superKind VanillaTv `thenNF_Tc` \ kv ->
returnNF_Tc (TyVarTy kv)
newKindVars :: Int -> NF_TcM [TcKind]
newBoxityVar :: NF_TcM TcKind
newBoxityVar
= tcGetUnique `thenNF_Tc` \ uniq ->
- tcNewMutTyVar (mkSysLocalName uniq SLIT("bx")) superBoxity VanillaTv `thenNF_Tc` \ kv ->
+ tcNewMutTyVar (mkSystemName uniq FSLIT("bx")) superBoxity VanillaTv `thenNF_Tc` \ kv ->
returnNF_Tc (TyVarTy kv)
\end{code}
%************************************************************************
%* *
-\subsection{Type instantiation}
+\subsection{'hole' type variables}
%* *
%************************************************************************
-I don't understand why this is needed
-An old comments says "No need for tcSplitForAllTyM because a type
- variable can't be instantiated to a for-all type"
-But the same is true of rho types!
-
\begin{code}
-tcSplitRhoTyM :: TcType -> NF_TcM (TcThetaType, TcType)
-tcSplitRhoTyM t
- = go t t []
- where
- -- A type variable is never instantiated to a dictionary type,
- -- so we don't need to do a tcReadVar on the "arg".
- go syn_t (FunTy arg res) ts = case tcSplitPredTy_maybe arg of
- 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 = getTcTyVar tv `thenNF_Tc` \ maybe_ty ->
- case maybe_ty of
- 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}
+newHoleTyVarTy :: NF_TcM TcType
+ = tcGetUnique `thenNF_Tc` \ uniq ->
+ tcNewMutTyVar (mkSystemName uniq FSLIT("h")) openTypeKind HoleTv `thenNF_Tc` \ tv ->
+ returnNF_Tc (TyVarTy tv)
+readHoleResult :: TcType -> NF_TcM TcType
+-- Read the answer out of a hole, constructed by newHoleTyVarTy
+readHoleResult (TyVarTy tv)
+ = ASSERT( isHoleTyVar tv )
+ getTcTyVar tv `thenNF_Tc` \ maybe_res ->
+ case maybe_res of
+ Just ty -> returnNF_Tc ty
+ Nothing -> pprPanic "readHoleResult: empty" (ppr tv)
+readHoleResult ty = pprPanic "readHoleResult: not hole" (ppr ty)
+
+zapToType :: TcType -> NF_TcM TcType
+zapToType (TyVarTy tv)
+ | isHoleTyVar tv
+ = getTcTyVar tv `thenNF_Tc` \ maybe_res ->
+ case maybe_res of
+ Nothing -> newTyVarTy openTypeKind `thenNF_Tc` \ ty ->
+ putTcTyVar tv ty `thenNF_Tc_`
+ returnNF_Tc ty
+ Just ty -> returnNF_Tc ty -- No need to loop; we never
+ -- have chains of holes
+
+zapToType other_ty = returnNF_Tc other_ty
+\end{code}
%************************************************************************
%* *
Instantiating a bunch of type variables
\begin{code}
-tcInstTyVars :: [TyVar]
+tcInstTyVars :: TyVarDetails -> [TyVar]
-> NF_TcM ([TcTyVar], [TcType], Subst)
-tcInstTyVars tyvars
- = mapNF_Tc tcInstTyVar tyvars `thenNF_Tc` \ tc_tyvars ->
+tcInstTyVars tv_details tyvars
+ = mapNF_Tc (tcInstTyVar tv_details) tyvars `thenNF_Tc` \ tc_tyvars ->
let
tys = mkTyVarTys tc_tyvars
in
-- they cannot possibly be captured by
-- any existing for-alls. Hence mkTopTyVarSubst
-tcInstTyVar tyvar
+tcInstTyVar tv_details tyvar
= tcGetUnique `thenNF_Tc` \ uniq ->
let
name = setNameUnique (tyVarName tyvar) uniq
-- that two different tyvars will print the same way
-- in an error message. -dppr-debug will show up the difference
-- Better watch out for this. If worst comes to worst, just
- -- use mkSysLocalName.
+ -- use mkSystemName.
in
- tcNewMutTyVar name (tyVarKind tyvar) VanillaTv
-
-tcInstSigTyVars :: TyVarDetails -> [TyVar] -> NF_TcM [TcTyVar]
-tcInstSigTyVars details tyvars -- Very similar to tcInstTyVar
- = tcGetUniques `thenNF_Tc` \ uniqs ->
- listTc [ ASSERT( not (kind `eqKind` openTypeKind) ) -- Shouldn't happen
- tcNewMutTyVar name kind details
- | (tyvar, uniq) <- tyvars `zip` uniqs,
- let name = setNameUnique (tyVarName tyvar) uniq,
- let kind = tyVarKind tyvar
- ]
-\end{code}
-
-@tcInstType@ instantiates the outer-level for-alls of a TcType with
-fresh type variables, splits off the dictionary part, and returns the results.
+ tcNewMutTyVar name (tyVarKind tyvar) tv_details
-\begin{code}
-tcInstType :: TcType -> NF_TcM ([TcTyVar], TcThetaType, TcType)
-tcInstType ty
+tcInstType :: TyVarDetails -> TcType -> NF_TcM ([TcTyVar], TcThetaType, TcType)
+-- tcInstType instantiates the outer-level for-alls of a TcType with
+-- fresh (mutable) type variables, splits off the dictionary part,
+-- and returns the pieces.
+tcInstType tv_details ty
= case tcSplitForAllTys ty of
- ([], rho) -> -- There may be overloading but no type variables;
+ ([], rho) -> -- There may be overloading despite no type variables;
-- (?x :: Int) => Int -> Int
let
- (theta, tau) = tcSplitRhoTy rho -- Used to be tcSplitRhoTyM
+ (theta, tau) = tcSplitPhiTy rho
in
returnNF_Tc ([], theta, tau)
- (tyvars, rho) -> tcInstTyVars tyvars `thenNF_Tc` \ (tyvars', _, tenv) ->
+ (tyvars, rho) -> tcInstTyVars tv_details tyvars `thenNF_Tc` \ (tyvars', _, tenv) ->
let
- (theta, tau) = tcSplitRhoTy (substTy tenv rho) -- Used to be tcSplitRhoTyM
+ (theta, tau) = tcSplitPhiTy (substTy tenv rho)
in
returnNF_Tc (tyvars', theta, tau)
-
-
-tcInstSigType :: TyVarDetails -> Type -> NF_TcM ([TcTyVar], TcThetaType, TcType)
--- Very similar to tcInstSigType, but uses signature type variables
--- Also, somewhat arbitrarily, don't deal with the monomorphic case so efficiently
-tcInstSigType tv_details poly_ty
- = let
- (tyvars, rho) = tcSplitForAllTys poly_ty
- in
- tcInstSigTyVars tv_details tyvars `thenNF_Tc` \ tyvars' ->
- -- Make *signature* type variables
-
- let
- tyvar_tys' = mkTyVarTys tyvars'
- rho' = substTy (mkTopTyVarSubst tyvars tyvar_tys') rho
- -- mkTopTyVarSubst because the tyvars' are fresh
-
- (theta', tau') = tcSplitRhoTy rho'
- -- This splitRhoTy tries hard to make sure that tau' is a type synonym
- -- wherever possible, which can improve interface files.
- in
- returnNF_Tc (tyvars', theta', tau')
\end{code}
-
%************************************************************************
%* *
\subsection{Putting and getting mutable type variables}
| otherwise
= ASSERT( isMutTyVar tyvar )
- UASSERT2( not (isUTy ty), ppr tyvar <+> ppr ty )
tcWriteMutTyVar tyvar (Just ty) `thenNF_Tc_`
returnNF_Tc ty
\end{code}
zonkTcTyVar :: TcTyVar -> NF_TcM TcType
zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnNF_Tc (TyVarTy tv)) tyvar
-
-zonkTcSigTyVars :: [TcTyVar] -> NF_TcM [TcTyVar]
--- This guy is to zonk the tyvars we're about to feed into tcSimplify
--- Usually this job is done by checkSigTyVars, but in a couple of places
--- that is overkill, so we use this simpler chap
-zonkTcSigTyVars tyvars
- = zonkTcTyVars tyvars `thenNF_Tc` \ tys ->
- returnNF_Tc (map (tcGetTyVar "zonkTcSigTyVars") tys)
\end{code}
----------------- Types
zonkTcTypeToType :: TcType -> NF_TcM Type
zonkTcTypeToType ty = zonkType zonk_unbound_tyvar ty
where
- -- Zonk a mutable but unbound type variable to
- -- Void if it has kind Lifted
- -- :Void otherwise
+ -- Zonk a mutable but unbound type variable to an arbitrary type
-- 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
- = putTcTyVar tv voidTy -- Just to avoid creating a new tycon in
- -- this vastly common case
- | otherwise
- = putTcTyVar tv (TyConApp (mk_void_tycon tv kind) [])
- where
- kind = tyVarKind tv
-
- mk_void_tycon tv kind -- Make a new TyCon with the same kind as the
- -- type variable tv. Same name too, apart from
- -- making it start with a colon (sigh)
+ zonk_unbound_tyvar tv = putTcTyVar tv (mkArbitraryType tv)
+
+
+-- When the type checker finds a type variable with no binding,
+-- which means it can be instantiated with an arbitrary type, it
+-- usually instantiates it to Void. Eg.
+--
+-- length []
+-- ===>
+-- length Void (Nil Void)
+--
+-- But in really obscure programs, the type variable might have
+-- a kind other than *, so we need to invent a suitably-kinded type.
+--
+-- This commit uses
+-- Void for kind *
+-- List for kind *->*
+-- Tuple for kind *->...*->*
+--
+-- which deals with most cases. (Previously, it only dealt with
+-- kind *.)
+--
+-- In the other cases, it just makes up a TyCon with a suitable
+-- kind. If this gets into an interface file, anyone reading that
+-- file won't understand it. This is fixable (by making the client
+-- of the interface file make up a TyCon too) but it is tiresome and
+-- never happens, so I am leaving it
+
+mkArbitraryType :: TcTyVar -> Type
+-- Make up an arbitrary type whose kind is the same as the tyvar.
+-- We'll use this to instantiate the (unbound) tyvar.
+mkArbitraryType tv
+ | isAnyTypeKind kind = voidTy -- The vastly common case
+ | otherwise = TyConApp tycon []
+ where
+ kind = tyVarKind tv
+ (args,res) = Type.splitFunTys kind -- Kinds are simple; use Type.splitFunTys
+
+ tycon | kind `eqKind` tyConKind listTyCon -- *->*
+ = listTyCon -- No tuples this size
+
+ | all isTypeKind args && isTypeKind res
+ = tupleTyCon Boxed (length args) -- *-> ... ->*->*
+
+ | otherwise
+ = pprTrace "Urk! Inventing strangely-kinded void TyCon" (ppr tc_name) $
+ mkPrimTyCon tc_name kind 0 [] VoidRep
+ -- Same name as the tyvar, apart from making it start with a colon (sigh)
-- I dread to think what will happen if this gets out into an
-- interface file. Catastrophe likely. Major sigh.
- = pprTrace "Urk! Inventing strangely-kinded void TyCon" (ppr tc_name) $
- mkPrimTyCon tc_name kind 0 [] VoidRep
- where
- tc_name = mkLocalName (getUnique tv) (mkDerivedTyConOcc (getOccName tv)) noSrcLoc
+
+ tc_name = mkInternalName (getUnique tv) (mkDerivedTyConOcc (getOccName tv)) noSrcLoc
-- zonkTcTyVarToTyVar is applied to the *binding* occurrence
-- of a type variable, at the *end* of type checking. It changes
go (AppTy fun arg) = go fun `thenNF_Tc` \ fun' ->
go arg `thenNF_Tc` \ arg' ->
returnNF_Tc (mkAppTy fun' arg')
-
- go (UsageTy u ty) = go u `thenNF_Tc` \ u' ->
- go ty `thenNF_Tc` \ ty' ->
- returnNF_Tc (UsageTy u' ty')
+ -- NB the mkAppTy; we might have instantiated a
+ -- type variable to a type constructor, so we need
+ -- to pull the TyConApp to the top.
-- The two interesting cases!
go (TyVarTy tyvar) = zonkTyVar unbound_var_fn tyvar
GenPatCtxt -> actual_kind_is_lifted
ForSigCtxt _ -> actual_kind_is_lifted
other -> isTypeKind actual_kind
+
+ ubx_tup | not gla_exts = UT_NotOk
+ | otherwise = case ctxt of
+ TySynCtxt _ -> UT_Ok
+ other -> UT_NotOk
+ -- Unboxed tuples ok in function results,
+ -- but for type synonyms we allow them even at
+ -- top level
in
tcAddErrCtxt (checkTypeCtxt ctxt ty) $
checkTc kind_ok (kindErr actual_kind) `thenTc_`
-- Check the internal validity of the type itself
- check_poly_type rank ty
+ check_poly_type rank ubx_tup ty
checkTypeCtxt ctxt ty
decRank Arbitrary = Arbitrary
decRank (Rank n) = Rank (n-1)
-check_poly_type :: Rank -> Type -> TcM ()
-check_poly_type (Rank 0) ty
- = check_tau_type (Rank 0) False ty
+----------------------------------------
+data UbxTupFlag = UT_Ok | UT_NotOk
+ -- The "Ok" version means "ok if -fglasgow-exts is on"
-check_poly_type rank ty
+----------------------------------------
+check_poly_type :: Rank -> UbxTupFlag -> Type -> TcM ()
+check_poly_type (Rank 0) ubx_tup ty
+ = check_tau_type (Rank 0) ubx_tup ty
+
+check_poly_type rank ubx_tup ty
= let
(tvs, theta, tau) = tcSplitSigmaTy ty
in
check_valid_theta SigmaCtxt theta `thenTc_`
- check_tau_type (decRank rank) False tau `thenTc_`
- checkAmbiguity tvs theta tau
+ check_tau_type (decRank rank) ubx_tup tau `thenTc_`
+ checkFreeness tvs theta `thenTc_`
+ checkAmbiguity tvs theta (tyVarsOfType tau)
----------------------------------------
check_arg_type :: Type -> TcM ()
-- 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.
+-- But not in user code.
+-- Anyway, they are dealt with by a special case in check_tau_type
+
check_arg_type ty
- = check_tau_type (Rank 0) False ty `thenTc_`
+ = check_tau_type (Rank 0) UT_NotOk ty `thenTc_`
checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
----------------------------------------
-check_tau_type :: Rank -> Bool -> Type -> TcM ()
+check_tau_type :: Rank -> UbxTupFlag -> 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 ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
+check_tau_type rank ubx_tup (SourceTy sty) = getDOptsTc `thenNF_Tc` \ dflags ->
+ check_source_ty dflags TypeCtxt sty
+check_tau_type rank ubx_tup (TyVarTy _) = returnTc ()
+check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
+ = check_poly_type rank UT_NotOk arg_ty `thenTc_`
+ check_tau_type rank UT_Ok res_ty
-check_tau_type rank ubx_tup_ok ty@(TyConApp tc tys)
- | isSynTyCon tc
- = checkTc syn_arity_ok arity_msg `thenTc_`
+check_tau_type rank ubx_tup (AppTy ty1 ty2)
+ = check_arg_type ty1 `thenTc_` check_arg_type ty2
+
+check_tau_type rank ubx_tup (NoteTy note ty)
+ = check_tau_type rank ubx_tup ty
+ -- Synonym notes are built only when the synonym is
+ -- saturated (see Type.mkSynTy)
+ -- Not checking the 'note' part allows us to instantiate a synonym
+ -- defn with a for-all type, or with a partially-applied type synonym,
+ -- but that seems OK too
+
+check_tau_type rank ubx_tup ty@(TyConApp tc tys)
+ | isSynTyCon tc
+ = -- NB: Type.mkSynTy builds a TyConApp (not a NoteTy) for an unsaturated
+ -- synonym application, leaving it to checkValidType (i.e. right here
+ -- to find the error
+ 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 (Rank 0) True) tys -- Args are allowed to be unlifted, or
- -- more unboxed tuples, so can't use check_arg_ty
+ = doptsTc Opt_GlasgowExts `thenNF_Tc` \ gla_exts ->
+ checkTc (ubx_tup_ok gla_exts) ubx_tup_msg `thenTc_`
+ mapTc_ (check_tau_type (Rank 0) UT_Ok) 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
+ ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
+
syn_arity_ok = tc_arity <= n_args
-- It's OK to have an *over-applied* type synonym
-- data Tree a b = ...
ubx_tup_msg = ubxArgTyErr ty
----------------------------------------
-check_note (FTVNote _) = returnTc ()
-check_note (SynNote ty) = check_tau_type (Rank 0) False ty
+forAllTyErr ty = ptext SLIT("Illegal polymorphic 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}
Check for ambiguity
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
(see is_ambig).
\begin{code}
-checkAmbiguity :: [TyVar] -> ThetaType -> Type -> TcM ()
-checkAmbiguity forall_tyvars theta tau
- = mapTc_ check_pred theta `thenTc_`
- returnTc ()
+checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
+checkAmbiguity forall_tyvars theta tau_tyvars
+ = mapTc_ complain (filter is_ambig theta)
where
- tau_vars = tyVarsOfType tau
- extended_tau_vars = grow theta tau_vars
+ complain pred = addErrTc (ambigErr pred)
+ extended_tau_vars = grow theta tau_tyvars
+ is_ambig pred = any ambig_var (varSetElems (tyVarsOfPred pred))
- is_ambig ct_var = (ct_var `elem` forall_tyvars) &&
+ ambig_var 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 '=>'"))]
+\end{code}
+
+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.
+\begin{code}
+checkFreeness forall_tyvars theta
+ = mapTc_ complain (filter is_free theta)
+ where
+ is_free pred = not (isIPPred pred)
+ && not (any bound_var (varSetElems (tyVarsOfPred pred)))
+ bound_var ct_var = ct_var `elem` forall_tyvars
+ complain pred = addErrTc (freeErr pred)
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}
-------------------------
check_source_ty dflags ctxt pred@(ClassP cls tys)
= -- Class predicates are valid in all contexts
- mapTc_ check_arg_type tys `thenTc_`
+ mapTc_ check_arg_type tys `thenTc_`
checkTc (arity == n_tys) arity_err `thenTc_`
checkTc (all tyvar_head tys || arby_preds_ok)
(predTyVarErr pred $$ how_to_allow)
= hang (ptext SLIT("Unacceptable instance type for ccall-ish class"))
4 (pprClassPred clas [inst_ty])
\end{code}
-
-