%
% (c) The University of Glasgow 2006
% (c) The GRASP/AQUA Project, Glasgow University, 19921998
%
Monadic type operations
This module contains monadic operations over types that contain
mutable type variables
\begin{code}
module TcMType (
TcTyVar, TcKind, TcType, TcTauType, TcThetaType, TcTyVarSet,
newFlexiTyVar,
newFlexiTyVarTy,
newFlexiTyVarTys,
newKindVar, newKindVars,
newMetaTyVar, readMetaTyVar, writeMetaTyVar, writeMetaTyVarRef,
isFilledMetaTyVar, isFlexiMetaTyVar,
newEvVar, newCoVar, newEvVars,
newWantedCoVar, writeWantedCoVar, readWantedCoVar,
newIP, newDict, newSelfDict, isSelfDict,
newWantedEvVar, newWantedEvVars,
newTcEvBinds, addTcEvBind,
tcInstTyVar, tcInstTyVars, tcInstSigTyVars,
tcInstType, tcInstSigType, instMetaTyVar,
tcInstSkolTyVars, tcInstSkolTyVar, tcInstSkolType,
tcSkolSigType, tcSkolSigTyVars,
Rank, UserTypeCtxt(..), checkValidType, checkValidMonoType,
SourceTyCtxt(..), checkValidTheta,
checkValidInstHead, checkValidInstance,
checkInstTermination, checkValidTypeInst, checkTyFamFreeness,
arityErr,
growPredTyVars, growThetaTyVars, validDerivPred,
zonkType, mkZonkTcTyVar, zonkTcPredType,
zonkTcTypeCarefully, skolemiseUnboundMetaTyVar,
zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkSigTyVar,
zonkQuantifiedTyVar, zonkQuantifiedTyVars,
zonkTcType, zonkTcTypes, zonkTcThetaType,
zonkTcKindToKind, zonkTcKind,
zonkImplication, zonkWanted, zonkEvVar, zonkWantedEvVar,
zonkTcTypeAndSubst,
tcGetGlobalTyVars,
readKindVar, writeKindVar
) where
#include "HsVersions.h"
import TypeRep
import TcType
import Type
import Coercion
import Class
import TyCon
import Var
import HsSyn
import TcRnMonad
import Id
import FunDeps
import Name
import VarSet
import ErrUtils
import DynFlags
import Util
import Maybes
import ListSetOps
import BasicTypes
import SrcLoc
import Outputable
import FastString
import Bag
import Control.Monad
import Data.List ( (\\) )
\end{code}
%************************************************************************
%* *
Kind variables
%* *
%************************************************************************
\begin{code}
newKindVar :: TcM TcKind
newKindVar = do { uniq <- newUnique
; ref <- newMutVar Flexi
; return (mkTyVarTy (mkKindVar uniq ref)) }
newKindVars :: Int -> TcM [TcKind]
newKindVars n = mapM (\ _ -> newKindVar) (nOfThem n ())
\end{code}
%************************************************************************
%* *
Evidence variables; range over constraints we can abstract over
%* *
%************************************************************************
\begin{code}
newEvVars :: TcThetaType -> TcM [EvVar]
newEvVars theta = mapM newEvVar theta
newWantedEvVar :: TcPredType -> TcM EvVar
newWantedEvVar (EqPred ty1 ty2) = newWantedCoVar ty1 ty2
newWantedEvVar (ClassP cls tys) = newDict cls tys
newWantedEvVar (IParam ip ty) = newIP ip ty
newWantedEvVars :: TcThetaType -> TcM [EvVar]
newWantedEvVars theta = mapM newWantedEvVar theta
newWantedCoVar :: TcType -> TcType -> TcM CoVar
newWantedCoVar ty1 ty2 = newCoVar ty1 ty2
newEvVar :: TcPredType -> TcM EvVar
newEvVar (EqPred ty1 ty2) = newCoVar ty1 ty2
newEvVar (ClassP cls tys) = newDict cls tys
newEvVar (IParam ip ty) = newIP ip ty
newCoVar :: TcType -> TcType -> TcM CoVar
newCoVar ty1 ty2
= do { name <- newName (mkTyVarOccFS (fsLit "co"))
; return (mkCoVar name (mkPredTy (EqPred ty1 ty2))) }
newIP :: IPName Name -> TcType -> TcM IpId
newIP ip ty
= do { name <- newName (getOccName (ipNameName ip))
; return (mkLocalId name (mkPredTy (IParam ip ty))) }
newDict :: Class -> [TcType] -> TcM DictId
newDict cls tys
= do { name <- newName (mkDictOcc (getOccName cls))
; return (mkLocalId name (mkPredTy (ClassP cls tys))) }
newName :: OccName -> TcM Name
newName occ
= do { uniq <- newUnique
; loc <- getSrcSpanM
; return (mkInternalName uniq occ loc) }
newSelfDict :: Class -> [TcType] -> TcM DictId
newSelfDict cls tys
= do { uniq <- newUnique
; let name = mkSystemName uniq selfDictOcc
; return (mkLocalId name (mkPredTy (ClassP cls tys))) }
selfDictOcc :: OccName
selfDictOcc = mkVarOcc "self"
isSelfDict :: EvVar -> Bool
isSelfDict v = isSystemName (Var.varName v)
\end{code}
%************************************************************************
%* *
SkolemTvs (immutable)
%* *
%************************************************************************
\begin{code}
tcInstType :: ([TyVar] -> TcM [TcTyVar])
-> TcType
-> TcM ([TcTyVar], TcThetaType, TcType)
tcInstType inst_tyvars ty
= case tcSplitForAllTys ty of
([], rho) -> let
(theta, tau) = tcSplitPhiTy rho
in
return ([], theta, tau)
(tyvars, rho) -> do { tyvars' <- inst_tyvars tyvars
; let tenv = zipTopTvSubst tyvars (mkTyVarTys tyvars')
; let (theta, tau) = tcSplitPhiTy (substTy tenv rho)
; return (tyvars', theta, tau) }
mkSkolTyVar :: Name -> Kind -> SkolemInfo -> TcTyVar
mkSkolTyVar name kind info = mkTcTyVar name kind (SkolemTv info)
tcSkolSigType :: SkolemInfo -> Type -> TcM ([TcTyVar], TcThetaType, TcType)
tcSkolSigType info ty = tcInstType (\tvs -> return (tcSkolSigTyVars info tvs)) ty
tcSkolSigTyVars :: SkolemInfo -> [TyVar] -> [TcTyVar]
tcSkolSigTyVars info tyvars = [ mkSkolTyVar (tyVarName tv) (tyVarKind tv) info
| tv <- tyvars ]
tcInstSkolTyVar :: SkolemInfo -> TyVar -> TcM TcTyVar
tcInstSkolTyVar skol_info tyvar
= do { uniq <- newUnique
; loc <- case skol_info of
SigSkol {} -> return (getSrcSpan old_name)
_ -> getSrcSpanM
; let new_name = mkInternalName uniq occ loc
; return (mkSkolTyVar new_name kind skol_info) }
where
old_name = tyVarName tyvar
occ = nameOccName old_name
kind = tyVarKind tyvar
tcInstSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
tcInstSkolTyVars info tyvars
= mapM (tcInstSkolTyVar info) tyvars
tcInstSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
tcInstSkolType info ty = tcInstType (tcInstSkolTyVars info) ty
tcInstSigType :: Bool -> Name -> TcType -> TcM ([TcTyVar], TcThetaType, TcRhoType)
tcInstSigType use_skols name ty
| use_skols
= tcInstType (tcInstSkolTyVars (SigSkol (FunSigCtxt name))) ty
| otherwise
= tcInstType tcInstSigTyVars ty
tcInstSigTyVars :: [TyVar] -> TcM [TcTyVar]
tcInstSigTyVars = mapM (\tv -> instMetaTyVar (SigTv (tyVarName tv)) tv)
\end{code}
%************************************************************************
%* *
MetaTvs (meta type variables; mutable)
%* *
%************************************************************************
\begin{code}
newMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar
newMetaTyVar meta_info kind
= do { uniq <- newMetaUnique
; ref <- newMutVar Flexi
; let name = mkSysTvName uniq fs
fs = case meta_info of
TauTv -> fsLit "t"
TcsTv -> fsLit "u"
SigTv _ -> fsLit "a"
; return (mkTcTyVar name kind (MetaTv meta_info ref)) }
instMetaTyVar :: MetaInfo -> TyVar -> TcM TcTyVar
instMetaTyVar meta_info tyvar
= do { uniq <- newMetaUnique
; ref <- newMutVar Flexi
; let name = setNameUnique (tyVarName tyvar) uniq
kind = tyVarKind tyvar
; return (mkTcTyVar name kind (MetaTv meta_info ref)) }
readMetaTyVar :: TyVar -> TcM MetaDetails
readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
readMutVar (metaTvRef tyvar)
readWantedCoVar :: CoVar -> TcM MetaDetails
readWantedCoVar covar = ASSERT2( isMetaTyVar covar, ppr covar )
readMutVar (metaTvRef covar)
isFilledMetaTyVar :: TyVar -> TcM Bool
isFilledMetaTyVar tv
| not (isTcTyVar tv) = return False
| MetaTv _ ref <- tcTyVarDetails tv
= do { details <- readMutVar ref
; return (isIndirect details) }
| otherwise = return False
isFlexiMetaTyVar :: TyVar -> TcM Bool
isFlexiMetaTyVar tv
| not (isTcTyVar tv) = return False
| MetaTv _ ref <- tcTyVarDetails tv
= do { details <- readMutVar ref
; return (isFlexi details) }
| otherwise = return False
writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
writeMetaTyVar tyvar ty
| not debugIsOn
= writeMetaTyVarRef tyvar (metaTvRef tyvar) ty
| not (isTcTyVar tyvar)
= WARN( True, text "Writing to non-tc tyvar" <+> ppr tyvar )
return ()
| MetaTv _ ref <- tcTyVarDetails tyvar
= writeMetaTyVarRef tyvar ref ty
| otherwise
= WARN( True, text "Writing to non-meta tyvar" <+> ppr tyvar )
return ()
writeWantedCoVar :: CoVar -> Coercion -> TcM ()
writeWantedCoVar cv co = writeMetaTyVar cv co
writeMetaTyVarRef :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM ()
writeMetaTyVarRef tyvar ref ty
| not debugIsOn
= do { traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
; writeMutVar ref (Indirect ty) }
| not (isPredTy tv_kind)
, not (ty_kind `isSubKind` tv_kind)
= WARN( True, hang (text "Ill-kinded update to meta tyvar")
2 (ppr tyvar $$ ppr tv_kind $$ ppr ty $$ ppr ty_kind) )
return ()
| otherwise
= do { meta_details <- readMutVar ref;
; WARN( not (isFlexi meta_details),
hang (text "Double update of meta tyvar")
2 (ppr tyvar $$ ppr meta_details) )
traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
; writeMutVar ref (Indirect ty) }
where
tv_kind = tyVarKind tyvar
ty_kind = typeKind ty
\end{code}
%************************************************************************
%* *
MetaTvs: TauTvs
%* *
%************************************************************************
\begin{code}
newFlexiTyVar :: Kind -> TcM TcTyVar
newFlexiTyVar kind = newMetaTyVar TauTv kind
newFlexiTyVarTy :: Kind -> TcM TcType
newFlexiTyVarTy kind = do
tc_tyvar <- newFlexiTyVar kind
return (TyVarTy tc_tyvar)
newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind)
tcInstTyVar :: TyVar -> TcM TcTyVar
tcInstTyVar tyvar = instMetaTyVar TauTv tyvar
tcInstTyVars :: [TyVar] -> TcM ([TcTyVar], [TcType], TvSubst)
tcInstTyVars tyvars
= do { tc_tvs <- mapM tcInstTyVar tyvars
; let tys = mkTyVarTys tc_tvs
; return (tc_tvs, tys, zipTopTvSubst tyvars tys) }
\end{code}
%************************************************************************
%* *
MetaTvs: SigTvs
%* *
%************************************************************************
\begin{code}
zonkSigTyVar :: TcTyVar -> TcM TcTyVar
zonkSigTyVar sig_tv
| isSkolemTyVar sig_tv
= return sig_tv
| otherwise
= ASSERT( isSigTyVar sig_tv )
do { ty <- zonkTcTyVar sig_tv
; return (tcGetTyVar "zonkSigTyVar" ty) }
\end{code}
%************************************************************************
%* *
\subsection{Zonking
%* *
%************************************************************************
@tcGetGlobalTyVars@ returns a fullyzonked set of tyvars free in the environment.
To improve subsequent calls to the same function it writes the zonked set back into
the environment.
\begin{code}
tcGetGlobalTyVars :: TcM TcTyVarSet
tcGetGlobalTyVars
= do { (TcLclEnv {tcl_tyvars = gtv_var}) <- getLclEnv
; gbl_tvs <- readMutVar gtv_var
; gbl_tvs' <- zonkTcTyVarsAndFV gbl_tvs
; writeMutVar gtv_var gbl_tvs'
; return gbl_tvs' }
\end{code}
\begin{code}
zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
zonkTcTyVars tyvars = mapM zonkTcTyVar tyvars
zonkTcTyVarsAndFV :: TcTyVarSet -> TcM TcTyVarSet
zonkTcTyVarsAndFV tyvars = tyVarsOfTypes <$> mapM zonkTcTyVar (varSetElems tyvars)
zonkTcTypeCarefully :: TcType -> TcM TcType
zonkTcTypeCarefully ty
= do { env_tvs <- tcGetGlobalTyVars
; zonkType (zonk_tv env_tvs) ty }
where
zonk_tv env_tvs tv
| tv `elemVarSet` env_tvs
= return (TyVarTy tv)
| otherwise
= ASSERT( isTcTyVar tv )
case tcTyVarDetails tv of
SkolemTv {} -> return (TyVarTy tv)
FlatSkol ty -> zonkType (zonk_tv env_tvs) ty
MetaTv _ ref -> do { cts <- readMutVar ref
; case cts of
Flexi -> return (TyVarTy tv)
Indirect ty -> zonkType (zonk_tv env_tvs) ty }
zonkTcType :: TcType -> TcM TcType
zonkTcType ty = zonkType zonkTcTyVar ty
zonkTcTyVar :: TcTyVar -> TcM TcType
zonkTcTyVar tv
= ASSERT2( isTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
SkolemTv {} -> return (TyVarTy tv)
FlatSkol ty -> zonkTcType ty
MetaTv _ ref -> do { cts <- readMutVar ref
; case cts of
Flexi -> return (TyVarTy tv)
Indirect ty -> zonkTcType ty }
zonkTcTypeAndSubst :: TvSubst -> TcType -> TcM TcType
zonkTcTypeAndSubst subst ty = zonkType zonk_tv ty
where
zonk_tv tv
= case tcTyVarDetails tv of
SkolemTv {} -> return (TyVarTy tv)
FlatSkol ty -> zonkType zonk_tv ty
MetaTv _ ref -> do { cts <- readMutVar ref
; case cts of
Flexi -> zonk_flexi tv
Indirect ty -> zonkType zonk_tv ty }
zonk_flexi tv
= case lookupTyVar subst tv of
Just ty -> zonkType zonk_tv ty
Nothing -> return (TyVarTy tv)
zonkTcTypes :: [TcType] -> TcM [TcType]
zonkTcTypes tys = mapM zonkTcType tys
zonkTcThetaType :: TcThetaType -> TcM TcThetaType
zonkTcThetaType theta = mapM zonkTcPredType theta
zonkTcPredType :: TcPredType -> TcM TcPredType
zonkTcPredType (ClassP c ts) = ClassP c <$> zonkTcTypes ts
zonkTcPredType (IParam n t) = IParam n <$> zonkTcType t
zonkTcPredType (EqPred t1 t2) = EqPred <$> zonkTcType t1 <*> zonkTcType t2
\end{code}
are used at the end of type checking
\begin{code}
zonkQuantifiedTyVars :: [TcTyVar] -> TcM [TcTyVar]
zonkQuantifiedTyVars = mapM zonkQuantifiedTyVar
zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar
zonkQuantifiedTyVar tv
= ASSERT2( isTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
FlatSkol {} -> pprPanic "zonkQuantifiedTyVar" (ppr tv)
SkolemTv {} -> do { kind <- zonkTcType (tyVarKind tv)
; return $ setTyVarKind tv kind }
MetaTv _ _ref ->
#ifdef DEBUG
(readMutVar _ref >>= \cts ->
case cts of
Flexi -> return ()
Indirect ty -> WARN( True, ppr tv $$ ppr ty )
return ()) >>
#endif
skolemiseUnboundMetaTyVar UnkSkol tv
skolemiseUnboundMetaTyVar :: SkolemInfo -> TcTyVar -> TcM TyVar
skolemiseUnboundMetaTyVar skol_info tv
= ASSERT2( isMetaTyVar tv, ppr tv )
do { uniq <- newUnique
; let final_kind = defaultKind (tyVarKind tv)
final_name = setNameUnique (tyVarName tv) uniq
final_tv = mkSkolTyVar final_name final_kind skol_info
; writeMetaTyVar tv (mkTyVarTy final_tv)
; return final_tv }
\end{code}
\begin{code}
zonkImplication :: Implication -> TcM Implication
zonkImplication implic@(Implic { ic_given = given
, ic_wanted = wanted })
= do { given' <- mapM zonkEvVar given
; wanted' <- mapBagM zonkWanted wanted
; return (implic { ic_given = given', ic_wanted = wanted' }) }
zonkEvVar :: EvVar -> TcM EvVar
zonkEvVar var = do { ty' <- zonkTcType (varType var)
; return (setVarType var ty') }
zonkWanted :: WantedConstraint -> TcM WantedConstraint
zonkWanted (WcImplic imp) = do { imp' <- zonkImplication imp; return (WcImplic imp') }
zonkWanted (WcEvVar ev) = do { ev' <- zonkWantedEvVar ev; return (WcEvVar ev') }
zonkWantedEvVar :: WantedEvVar -> TcM WantedEvVar
zonkWantedEvVar (WantedEvVar v l) = do { v' <- zonkEvVar v; return (WantedEvVar v' l) }
\end{code}
Note [Silly Type Synonyms]
~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider this:
type C u a = u
foo :: (forall a. C u a -> C u a) -> u
foo x = ...
bar :: Num u => u
bar = foo (\t -> t + t)
* From the (\t -> t+t) we get type {Num d} => d -> d
where d is fresh.
* Now unify with type of foo's arg, and we get:
{Num (C d a)} => C d a -> C d a
where a is fresh.
* Now abstract over the 'a', but float out the Num (C d a) constraint
because it does not 'really' mention a. (see exactTyVarsOfType)
The arg to foo becomes
\/\a -> \t -> t+t
* So we get a dict binding for Num (C d a), which is zonked to give
a = ()
[Note Sept 04: now that we are zonking quantified type variables
on construction, the 'a' will be frozen as a regular tyvar on
quantification, so the floated dict will still have type (C d a).
Which renders this whole note moot; happily!]
* Then the \/\a abstraction has a zonked 'a' in it.
All very silly. I think its harmless to ignore the problem. We'll end up with
a \/\a in the final result but all the occurrences of a will be zonked to ()
Note [Zonking to Skolem]
~~~~~~~~~~~~~~~~~~~~~~~~
We used to zonk quantified type variables to regular TyVars. However, this
leads to problems. Consider this program from the regression test suite:
eval :: Int -> String -> String -> String
eval 0 root actual = evalRHS 0 root actual
evalRHS :: Int -> a
evalRHS 0 root actual = eval 0 root actual
It leads to the deferral of an equality (wrapped in an implication constraint)
forall a. (String -> String -> String) ~ a
which is propagated up to the toplevel (see TcSimplify.tcSimplifyInferCheck).
In the meantime `a' is zonked and quantified to form `evalRHS's signature.
This has the *side effect* of also zonking the `a' in the deferred equality
(which at this point is being handed around wrapped in an implication
constraint).
Finally, the equality (with the zonked `a') will be handed back to the
simplifier by TcRnDriver.tcRnSrcDecls calling TcSimplify.tcSimplifyTop.
If we zonk `a' with a regular type variable, we will have this regular type
variable now floating around in the simplifier, which in many places assumes to
only see proper TcTyVars.
We can avoid this problem by zonking with a skolem. The skolem is rigid
(which we require for a quantified variable), but is still a TcTyVar that the
simplifier knows how to deal with.
%************************************************************************
%* *
\subsection{Zonking
%* *
%* For internal use only! *
%* *
%************************************************************************
\begin{code}
zonkType :: (TcTyVar -> TcM Type)
-> TcType -> TcM Type
zonkType zonk_tc_tyvar ty
= go ty
where
go (TyConApp tc tys) = do tys' <- mapM go tys
return (TyConApp tc tys')
go (PredTy p) = do p' <- go_pred p
return (PredTy p')
go (FunTy arg res) = do arg' <- go arg
res' <- go res
return (FunTy arg' res')
go (AppTy fun arg) = do fun' <- go fun
arg' <- go arg
return (mkAppTy fun' arg')
go (TyVarTy tyvar) | isTcTyVar tyvar = zonk_tc_tyvar tyvar
| otherwise = liftM TyVarTy $
zonkTyVar zonk_tc_tyvar tyvar
go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar ) do
ty' <- go ty
tyvar' <- zonkTyVar zonk_tc_tyvar tyvar
return (ForAllTy tyvar' ty')
go_pred (ClassP c tys) = do tys' <- mapM go tys
return (ClassP c tys')
go_pred (IParam n ty) = do ty' <- go ty
return (IParam n ty')
go_pred (EqPred ty1 ty2) = do ty1' <- go ty1
ty2' <- go ty2
return (EqPred ty1' ty2')
mkZonkTcTyVar :: (TcTyVar -> TcM Type)
-> TcTyVar -> TcM TcType
mkZonkTcTyVar unbound_var_fn tyvar
= ASSERT( isTcTyVar tyvar )
case tcTyVarDetails tyvar of
SkolemTv {} -> return (TyVarTy tyvar)
FlatSkol ty -> zonkType (mkZonkTcTyVar unbound_var_fn) ty
MetaTv _ ref -> do { cts <- readMutVar ref
; case cts of
Flexi -> unbound_var_fn tyvar
Indirect ty -> zonkType (mkZonkTcTyVar unbound_var_fn) ty }
zonkTyVar :: (TcTyVar -> TcM Type)
-> TyVar -> TcM TyVar
zonkTyVar zonk_tc_tyvar tv
| isCoVar tv
= do { kind <- zonkType zonk_tc_tyvar (tyVarKind tv)
; return $ setTyVarKind tv kind }
| otherwise = return tv
\end{code}
%************************************************************************
%* *
Zonking kinds
%* *
%************************************************************************
\begin{code}
readKindVar :: KindVar -> TcM (MetaDetails)
writeKindVar :: KindVar -> TcKind -> TcM ()
readKindVar kv = readMutVar (kindVarRef kv)
writeKindVar kv val = writeMutVar (kindVarRef kv) (Indirect val)
zonkTcKind :: TcKind -> TcM TcKind
zonkTcKind k = zonkTcType k
zonkTcKindToKind :: TcKind -> TcM Kind
zonkTcKindToKind k
= zonkType (mkZonkTcTyVar (\ _ -> return liftedTypeKind)) k
\end{code}
%************************************************************************
%* *
\subsection{Checking a user type}
%* *
%************************************************************************
When dealing with a userwritten 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 interfacefile
types and (b) when checking a mutually recursive group of type and class decls,
we can't "look" at the tycons/classes yet. Also, the checks are are rather
diverse, and used to really mess up the other code.
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
Another thing is to check that type synonyms are saturated.
This might not necessarily show up in kind checking.
type A i = i
data T k = MkT (k Int)
f :: T A
\begin{code}
checkValidType :: UserTypeCtxt -> Type -> TcM ()
checkValidType ctxt ty = do
traceTc "checkValidType" (ppr ty)
unboxed <- xoptM Opt_UnboxedTuples
rank2 <- xoptM Opt_Rank2Types
rankn <- xoptM Opt_RankNTypes
polycomp <- xoptM Opt_PolymorphicComponents
let
gen_rank n | rankn = ArbitraryRank
| rank2 = Rank 2
| otherwise = Rank n
rank
= case ctxt of
DefaultDeclCtxt-> MustBeMonoType
ResSigCtxt -> MustBeMonoType
LamPatSigCtxt -> gen_rank 0
BindPatSigCtxt -> gen_rank 0
TySynCtxt _ -> gen_rank 0
GenPatCtxt -> gen_rank 1
ExprSigCtxt -> gen_rank 1
FunSigCtxt _ -> gen_rank 1
ConArgCtxt _ | polycomp -> gen_rank 2
| otherwise -> gen_rank 1
ForSigCtxt _ -> gen_rank 1
SpecInstCtxt -> gen_rank 1
ThBrackCtxt -> gen_rank 1
actual_kind = typeKind ty
kind_ok = case ctxt of
TySynCtxt _ -> True
ThBrackCtxt -> True
ResSigCtxt -> isSubOpenTypeKind actual_kind
ExprSigCtxt -> isSubOpenTypeKind actual_kind
GenPatCtxt -> isLiftedTypeKind actual_kind
ForSigCtxt _ -> isLiftedTypeKind actual_kind
_ -> isSubArgTypeKind actual_kind
ubx_tup = case ctxt of
TySynCtxt _ | unboxed -> UT_Ok
ExprSigCtxt | unboxed -> UT_Ok
ThBrackCtxt | unboxed -> UT_Ok
_ -> UT_NotOk
check_type rank ubx_tup ty
checkTc kind_ok (kindErr actual_kind)
traceTc "checkValidType done" (ppr ty)
checkValidMonoType :: Type -> TcM ()
checkValidMonoType ty = check_mono_type MustBeMonoType ty
\end{code}
\begin{code}
data Rank = ArbitraryRank
| MustBeMonoType
| TyConArgMonoType
| SynArgMonoType
| Rank Int
decRank :: Rank -> Rank
decRank (Rank 0) = Rank 0
decRank (Rank n) = Rank (n1)
decRank other_rank = other_rank
nonZeroRank :: Rank -> Bool
nonZeroRank ArbitraryRank = True
nonZeroRank (Rank n) = n>0
nonZeroRank _ = False
data UbxTupFlag = UT_Ok | UT_NotOk
check_mono_type :: Rank -> Type -> TcM ()
check_mono_type rank ty
= do { check_type rank UT_NotOk ty
; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
check_type :: Rank -> UbxTupFlag -> Type -> TcM ()
check_type rank ubx_tup ty
| not (null tvs && null theta)
= do { checkTc (nonZeroRank rank) (forAllTyErr rank ty)
; check_valid_theta SigmaCtxt theta
; check_type rank ubx_tup tau
; checkAmbiguity tvs theta (tyVarsOfType tau) }
where
(tvs, theta, tau) = tcSplitSigmaTy ty
check_type _ _ ty@(PredTy {})
= failWithTc (text "Predicate" <+> ppr ty <+> text "used as a type")
check_type _ _ (TyVarTy _) = return ()
check_type rank _ (FunTy arg_ty res_ty)
= do { check_type (decRank rank) UT_NotOk arg_ty
; check_type rank UT_Ok res_ty }
check_type rank _ (AppTy ty1 ty2)
= do { check_arg_type rank ty1
; check_arg_type rank ty2 }
check_type rank ubx_tup ty@(TyConApp tc tys)
| isSynTyCon tc
= do {
checkTc (tyConArity tc <= length tys) arity_msg
; liberal <- xoptM Opt_LiberalTypeSynonyms
; if not liberal || isSynFamilyTyCon tc then
mapM_ (check_mono_type SynArgMonoType) tys
else
case tcView ty of
Just ty' -> check_type rank ubx_tup ty'
Nothing -> pprPanic "check_tau_type" (ppr ty)
}
| isUnboxedTupleTyCon tc
= do { ub_tuples_allowed <- xoptM Opt_UnboxedTuples
; checkTc (ubx_tup_ok ub_tuples_allowed) ubx_tup_msg
; impred <- xoptM Opt_ImpredicativeTypes
; let rank' = if impred then ArbitraryRank else TyConArgMonoType
; mapM_ (check_type rank' UT_Ok) tys }
| otherwise
= mapM_ (check_arg_type rank) tys
where
ubx_tup_ok ub_tuples_allowed = case ubx_tup of
UT_Ok -> ub_tuples_allowed
_ -> False
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_type _ _ ty = pprPanic "check_type" (ppr ty)
check_arg_type :: Rank -> Type -> TcM ()
check_arg_type rank ty
= do { impred <- xoptM Opt_ImpredicativeTypes
; let rank' = case rank of
MustBeMonoType -> MustBeMonoType
_other | impred -> ArbitraryRank
| otherwise -> TyConArgMonoType
; check_type rank' UT_NotOk ty
; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
forAllTyErr :: Rank -> Type -> SDoc
forAllTyErr rank ty
= vcat [ hang (ptext (sLit "Illegal polymorphic or qualified type:")) 2 (ppr ty)
, suggestion ]
where
suggestion = case rank of
Rank _ -> ptext (sLit "Perhaps you intended to use -XRankNTypes or -XRank2Types")
TyConArgMonoType -> ptext (sLit "Perhaps you intended to use -XImpredicativeTypes")
SynArgMonoType -> ptext (sLit "Perhaps you intended to use -XLiberalTypeSynonyms")
_ -> empty
unliftedArgErr, ubxArgTyErr :: Type -> SDoc
unliftedArgErr ty = sep [ptext (sLit "Illegal unlifted type:"), ppr ty]
ubxArgTyErr ty = sep [ptext (sLit "Illegal unboxed tuple type as function argument:"), ppr ty]
kindErr :: Kind -> SDoc
kindErr kind = sep [ptext (sLit "Expecting an ordinary type, but found a type of kind"), ppr kind]
\end{code}
Note [Liberal type synonyms]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
If XLiberalTypeSynonyms is on, expand closed type synonyms *before*
doing validity checking. This allows us to instantiate a synonym defn
with a forall type, or with a partiallyapplied type synonym.
e.g. type T a b = a
type S m = m ()
f :: S (T Int)
Here, T is partially applied, so it's illegal in H98. But if you
expand S first, then T we get just
f :: Int
which is fine.
IMPORTANT: suppose T is a type synonym. Then we must do validity
checking on an appliation (T ty1 ty2)
*either* before expansion (i.e. check ty1, ty2)
*or* after expansion (i.e. expand T ty1 ty2, and then check)
BUT NOT BOTH
If we do both, we get exponential behaviour!!
data TIACons1 i r c = c i ::: r c
type TIACons2 t x = TIACons1 t (TIACons1 t x)
type TIACons3 t x = TIACons2 t (TIACons1 t x)
type TIACons4 t x = TIACons2 t (TIACons2 t x)
type TIACons7 t x = TIACons4 t (TIACons3 t x)
%************************************************************************
%* *
\subsection{Checking a theta or source type}
%* *
%************************************************************************
\begin{code}
data SourceTyCtxt
= ClassSCCtxt Name
| SigmaCtxt
| DataTyCtxt Name
| TypeCtxt
| InstThetaCtxt
pprSourceTyCtxt :: SourceTyCtxt -> SDoc
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 TypeCtxt = ptext (sLit "the context of a type")
\end{code}
\begin{code}
checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
checkValidTheta ctxt theta
= addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
check_valid_theta :: SourceTyCtxt -> [PredType] -> TcM ()
check_valid_theta _ []
= return ()
check_valid_theta ctxt theta = do
dflags <- getDOpts
warnTc (notNull dups) (dupPredWarn dups)
mapM_ (check_pred_ty dflags ctxt) theta
where
(_,dups) = removeDups tcCmpPred theta
check_pred_ty :: DynFlags -> SourceTyCtxt -> PredType -> TcM ()
check_pred_ty dflags ctxt pred@(ClassP cls tys)
= do {
; checkTc (arity == n_tys) arity_err
; mapM_ checkValidMonoType tys
; checkTc (check_class_pred_tys dflags ctxt tys)
(predTyVarErr pred $$ how_to_allow)
}
where
class_name = className cls
arity = classArity cls
n_tys = length tys
arity_err = arityErr "Class" class_name arity n_tys
how_to_allow = parens (ptext (sLit "Use -XFlexibleContexts to permit this"))
check_pred_ty dflags ctxt pred@(EqPred ty1 ty2)
= do {
; checkTc (xopt Opt_TypeFamilies dflags) (eqPredTyErr pred)
; checkTc (case ctxt of ClassSCCtxt {} -> False; _ -> True)
(eqSuperClassErr pred)
; checkValidMonoType ty1
; checkValidMonoType ty2
}
check_pred_ty _ SigmaCtxt (IParam _ ty) = checkValidMonoType ty
check_pred_ty _ _ sty = failWithTc (badPredTyErr sty)
check_class_pred_tys :: DynFlags -> SourceTyCtxt -> [Type] -> Bool
check_class_pred_tys dflags ctxt tys
= case ctxt of
TypeCtxt -> True
InstThetaCtxt -> flexible_contexts || undecidable_ok || all tcIsTyVarTy tys
_ -> flexible_contexts || all tyvar_head tys
where
flexible_contexts = xopt Opt_FlexibleContexts dflags
undecidable_ok = xopt Opt_UndecidableInstances dflags
tyvar_head :: Type -> Bool
tyvar_head ty
| tcIsTyVarTy ty = True
| otherwise
= case tcSplitAppTy_maybe ty of
Just (ty, _) -> tyvar_head ty
Nothing -> False
\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
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).
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}
checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
checkAmbiguity forall_tyvars theta tau_tyvars
= mapM_ complain (filter is_ambig theta)
where
complain pred = addErrTc (ambigErr pred)
extended_tau_vars = growThetaTyVars theta tau_tyvars
is_ambig pred = isClassPred pred &&
any ambig_var (varSetElems (tyVarsOfPred pred))
ambig_var ct_var = (ct_var `elem` forall_tyvars) &&
not (ct_var `elemVarSet` extended_tau_vars)
ambigErr :: PredType -> SDoc
ambigErr pred
= sep [ptext (sLit "Ambiguous constraint") <+> quotes (pprPred pred),
nest 2 (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}
Note [Growing the tautvs using constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
(growInstsTyVars insts tvs) is the result of extending the set
of tyvars tvs using all conceivable links from pred
E.g. tvs = {a}, preds = {H [a] b, K (b,Int) c, Eq e}
Then grow precs tvs = {a,b,c}
\begin{code}
growThetaTyVars :: TcThetaType -> TyVarSet -> TyVarSet
growThetaTyVars theta tvs
| null theta = tvs
| otherwise = fixVarSet mk_next tvs
where
mk_next tvs = foldr grow_one tvs theta
grow_one pred tvs = growPredTyVars pred tvs `unionVarSet` tvs
growPredTyVars :: TcPredType
-> TyVarSet
-> TyVarSet
growPredTyVars pred tvs
| IParam {} <- pred = pred_tvs
| pred_tvs `intersectsVarSet` tvs = pred_tvs
| otherwise = emptyVarSet
where
pred_tvs = tyVarsOfPred pred
\end{code}
Note [Implicit parameters and ambiguity]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Only a *class* predicate can give rise to ambiguity
An *implicit parameter* cannot. For example:
foo :: (?x :: [a]) => Int
foo = length ?x
is fine. The call site will suppply a particular 'x'
Furthermore, the type variables fixed by an implicit parameter
propagate to the others. E.g.
foo :: (Show a, ?x::[a]) => Int
foo = show (?x++?x)
The type of foo looks ambiguous. But it isn't, because at a call site
we might have
let ?x = 5::Int in foo
and all is well. In effect, implicit parameters are, well, parameters,
so we can take their type variables into account as part of the
"tau-tvs" stuff. This is done in the function 'FunDeps.grow'.
\begin{code}
checkThetaCtxt :: SourceTyCtxt -> ThetaType -> SDoc
checkThetaCtxt ctxt theta
= vcat [ptext (sLit "In the context:") <+> pprTheta theta,
ptext (sLit "While checking") <+> pprSourceTyCtxt ctxt ]
eqSuperClassErr :: PredType -> SDoc
eqSuperClassErr pred
= hang (ptext (sLit "Alas, GHC 7.0 still cannot handle equality superclasses:"))
2 (ppr pred)
badPredTyErr, eqPredTyErr, predTyVarErr :: PredType -> SDoc
badPredTyErr pred = ptext (sLit "Illegal constraint") <+> pprPred pred
eqPredTyErr pred = ptext (sLit "Illegal equational constraint") <+> pprPred pred
$$
parens (ptext (sLit "Use -XTypeFamilies to permit this"))
predTyVarErr pred = sep [ptext (sLit "Non type-variable argument"),
nest 2 (ptext (sLit "in the constraint:") <+> pprPred pred)]
dupPredWarn :: [[PredType]] -> SDoc
dupPredWarn dups = ptext (sLit "Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
arityErr :: Outputable a => String -> a -> Int -> Int -> SDoc
arityErr kind name n m
= hsep [ text kind, quotes (ppr name), ptext (sLit "should have"),
n_arguments <> comma, text "but has been given",
if m==0 then text "none" else int m]
where
n_arguments | n == 0 = ptext (sLit "no arguments")
| n == 1 = ptext (sLit "1 argument")
| True = hsep [int n, ptext (sLit "arguments")]
\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 (Class, [TcType])
checkValidInstHead ty
= 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) -> do
dflags <- getDOpts
check_inst_head dflags clas tys
return (clas, tys)
}}
check_inst_head :: DynFlags -> Class -> [Type] -> TcM ()
check_inst_head dflags clas tys
= do {
; checkTc (xopt Opt_TypeSynonymInstances dflags ||
all tcInstHeadTyNotSynonym tys)
(instTypeErr (pprClassPred clas tys) head_type_synonym_msg)
; checkTc (xopt Opt_FlexibleInstances dflags ||
all tcInstHeadTyAppAllTyVars tys)
(instTypeErr (pprClassPred clas tys) head_type_args_tyvars_msg)
; checkTc (xopt Opt_MultiParamTypeClasses dflags ||
isSingleton tys)
(instTypeErr (pprClassPred clas tys) head_one_type_msg)
; mapM_ checkTyFamFreeness tys
; mapM_ checkValidMonoType tys
}
where
head_type_synonym_msg = parens (
text "All instance types must be of the form (T t1 ... tn)" $$
text "where T is not a synonym." $$
text "Use -XTypeSynonymInstances if you want to disable this.")
head_type_args_tyvars_msg = parens (vcat [
text "All instance types must be of the form (T a1 ... an)",
text "where a1 ... an are type *variables*,",
text "and each type variable appears at most once in the instance head.",
text "Use -XFlexibleInstances if you want to disable this."])
head_one_type_msg = parens (
text "Only one type can be given in an instance head." $$
text "Use -XMultiParamTypeClasses if you want to allow more.")
instTypeErr :: SDoc -> SDoc -> SDoc
instTypeErr pp_ty msg
= sep [ptext (sLit "Illegal instance declaration for") <+> quotes pp_ty,
nest 2 msg]
\end{code}
%************************************************************************
%* *
\subsection{Checking instance for termination}
%* *
%************************************************************************
\begin{code}
checkValidInstance :: LHsType Name -> [TyVar] -> ThetaType -> Type
-> TcM (Class, [TcType])
checkValidInstance hs_type tyvars theta tau
= setSrcSpan (getLoc hs_type) $
do { (clas, inst_tys) <- setSrcSpan head_loc $
checkValidInstHead tau
; undecidable_ok <- xoptM Opt_UndecidableInstances
; checkValidTheta InstThetaCtxt theta
; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys)
; unless undecidable_ok $
mapM_ addErrTc (checkInstTermination inst_tys theta)
; checkTc (undecidable_ok || checkInstCoverage clas inst_tys)
(instTypeErr (pprClassPred clas inst_tys) msg)
; return (clas, inst_tys)
}
where
msg = parens (vcat [ptext (sLit "the Coverage Condition fails for one of the functional dependencies;"),
undecidableMsg])
head_loc = case hs_type of
L _ (HsForAllTy _ _ _ (L loc _)) -> loc
L loc _ -> loc
\end{code}
Termination test: the socalled "Paterson conditions" (see Section 5 of
"Understanding functionsl dependencies via Constraint Handling Rules,
JFP Jan 2007).
We check that each assertion in the context satisfies:
(1) no variable has more occurrences in the assertion than in the head, and
(2) the assertion has fewer constructors and variables (taken together
and counting repetitions) than the head.
This is only needed with -fglasgow-exts, as Haskell 98 restrictions
(which have already been checked) guarantee termination.
The underlying idea is that
for any ground substitution, each assertion in the
context has fewer type constructors than the head.
\begin{code}
checkInstTermination :: [TcType] -> ThetaType -> [Message]
checkInstTermination tys theta
= mapCatMaybes check theta
where
fvs = fvTypes tys
size = sizeTypes tys
check pred
| not (null (fvPred pred \\ fvs))
= Just (predUndecErr pred nomoreMsg $$ parens undecidableMsg)
| sizePred pred >= size
= Just (predUndecErr pred smallerMsg $$ parens undecidableMsg)
| otherwise
= Nothing
predUndecErr :: PredType -> SDoc -> SDoc
predUndecErr pred msg = sep [msg,
nest 2 (ptext (sLit "in the constraint:") <+> pprPred pred)]
nomoreMsg, smallerMsg, undecidableMsg :: SDoc
nomoreMsg = ptext (sLit "Variable occurs more often in a constraint than in the instance head")
smallerMsg = ptext (sLit "Constraint is no smaller than the instance head")
undecidableMsg = ptext (sLit "Use XUndecidableInstances to permit this")
\end{code}
validDeivPred checks for OK 'deriving' context. See Note [Exotic
derived instance contexts] in TcSimplify. However the predicate is
here because it uses sizeTypes, fvTypes.
\begin{code}
validDerivPred :: PredType -> Bool
validDerivPred (ClassP _ tys) = hasNoDups fvs && sizeTypes tys == length fvs
where fvs = fvTypes tys
validDerivPred _ = False
\end{code}
%************************************************************************
%* *
Checking type instance wellformedness and termination
%* *
%************************************************************************
\begin{code}
checkValidTypeInst :: [Type] -> Type -> TcM ()
checkValidTypeInst typats rhs
= do {
; mapM_ checkTyFamFreeness typats
; checkValidMonoType rhs
; undecidable_ok <- xoptM Opt_UndecidableInstances
; unless undecidable_ok $
mapM_ addErrTc (checkFamInst typats (tyFamInsts rhs))
}
checkFamInst :: [Type]
-> [(TyCon, [Type])]
-> [Message]
checkFamInst lhsTys famInsts
= mapCatMaybes check famInsts
where
size = sizeTypes lhsTys
fvs = fvTypes lhsTys
check (tc, tys)
| not (all isTyFamFree tys)
= Just (famInstUndecErr famInst nestedMsg $$ parens undecidableMsg)
| not (null (fvTypes tys \\ fvs))
= Just (famInstUndecErr famInst nomoreVarMsg $$ parens undecidableMsg)
| size <= sizeTypes tys
= Just (famInstUndecErr famInst smallerAppMsg $$ parens undecidableMsg)
| otherwise
= Nothing
where
famInst = TyConApp tc tys
checkTyFamFreeness :: Type -> TcM ()
checkTyFamFreeness ty
= checkTc (isTyFamFree ty) $
tyFamInstIllegalErr ty
isTyFamFree :: Type -> Bool
isTyFamFree = null . tyFamInsts
tyFamInstIllegalErr :: Type -> SDoc
tyFamInstIllegalErr ty
= hang (ptext (sLit "Illegal type synonym family application in instance") <>
colon) 2 $
ppr ty
famInstUndecErr :: Type -> SDoc -> SDoc
famInstUndecErr ty msg
= sep [msg,
nest 2 (ptext (sLit "in the type family application:") <+>
pprType ty)]
nestedMsg, nomoreVarMsg, smallerAppMsg :: SDoc
nestedMsg = ptext (sLit "Nested type family application")
nomoreVarMsg = ptext (sLit "Variable occurs more often than in instance head")
smallerAppMsg = ptext (sLit "Application is no smaller than the instance head")
\end{code}
%************************************************************************
%* *
\subsection{Auxiliary functions}
%* *
%************************************************************************
\begin{code}
fvType :: Type -> [TyVar]
fvType ty | Just exp_ty <- tcView ty = fvType exp_ty
fvType (TyVarTy tv) = [tv]
fvType (TyConApp _ tys) = fvTypes tys
fvType (PredTy pred) = fvPred pred
fvType (FunTy arg res) = fvType arg ++ fvType res
fvType (AppTy fun arg) = fvType fun ++ fvType arg
fvType (ForAllTy tyvar ty) = filter (/= tyvar) (fvType ty)
fvTypes :: [Type] -> [TyVar]
fvTypes tys = concat (map fvType tys)
fvPred :: PredType -> [TyVar]
fvPred (ClassP _ tys') = fvTypes tys'
fvPred (IParam _ ty) = fvType ty
fvPred (EqPred ty1 ty2) = fvType ty1 ++ fvType ty2
sizeType :: Type -> Int
sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty
sizeType (TyVarTy _) = 1
sizeType (TyConApp _ tys) = sizeTypes tys + 1
sizeType (PredTy pred) = sizePred pred
sizeType (FunTy arg res) = sizeType arg + sizeType res + 1
sizeType (AppTy fun arg) = sizeType fun + sizeType arg
sizeType (ForAllTy _ ty) = sizeType ty
sizeTypes :: [Type] -> Int
sizeTypes xs = sum (map sizeType xs)
sizePred :: PredType -> Int
sizePred (ClassP _ tys') = sizeTypes tys'
sizePred (IParam {}) = 0
sizePred (EqPred {}) = 0
\end{code}