%
+% (c) The University of Glasgow 2006
% (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
%
-\section{Monadic type operations}
-This module contains monadic operations over types that contain mutable type variables
+Monadic type operations
+
+This module contains monadic operations over types that contain
+mutable type variables
\begin{code}
module TcMType (
newBoxyTyVar, newBoxyTyVars, newBoxyTyVarTys, readFilledBox,
--------------------------------
+ -- Creating new coercion variables
+ newCoVars,
+
+ --------------------------------
-- Instantiation
- tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxy, tcInstBoxyTyVar,
+ tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxyTyVar,
tcInstSigTyVars, zonkSigTyVar,
tcInstSkolTyVar, tcInstSkolTyVars, tcInstSkolType,
tcSkolSigType, tcSkolSigTyVars,
#include "HsVersions.h"
-
-- friends:
-import TypeRep ( Type(..), PredType(..), -- Friend; can see representation
- ThetaType
- )
-import TcType ( TcType, TcThetaType, TcTauType, TcPredType,
- TcTyVarSet, TcKind, TcTyVar, TcTyVarDetails(..),
- MetaDetails(..), SkolemInfo(..), BoxInfo(..),
- BoxyTyVar, BoxyType, BoxyThetaType, BoxySigmaType,
- UserTypeCtxt(..),
- isMetaTyVar, isSigTyVar, metaTvRef,
- tcCmpPred, isClassPred, tcGetTyVar,
- tcSplitPhiTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe,
- tcValidInstHeadTy, tcSplitForAllTys,
- tcIsTyVarTy, tcSplitSigmaTy,
- isUnLiftedType, isIPPred,
- typeKind, isSkolemTyVar,
- mkAppTy, mkTyVarTy, mkTyVarTys,
- tyVarsOfPred, getClassPredTys_maybe,
- tyVarsOfType, tyVarsOfTypes, tcView,
- pprPred, pprTheta, pprClassPred )
-import Kind ( Kind(..), KindVar, kindVarRef, mkKindVar,
- isLiftedTypeKind, isArgTypeKind, isOpenTypeKind,
- liftedTypeKind, defaultKind
- )
-import Type ( TvSubst, zipTopTvSubst, substTy )
-import Class ( Class, classArity, className )
-import TyCon ( TyCon, isSynTyCon, isUnboxedTupleTyCon,
- tyConArity, tyConName )
-import Var ( TyVar, tyVarKind, tyVarName, isTcTyVar,
- mkTyVar, mkTcTyVar, tcTyVarDetails )
-
- -- Assertions
-#ifdef DEBUG
-import TcType ( isFlexi, isBoxyTyVar, isImmutableTyVar )
-import Kind ( isSubKind )
-#endif
+import TypeRep
+import TcType
+import Type
+import Type
+import Coercion
+import Class
+import TyCon
+import Var
-- others:
import TcRnMonad -- TcType, amongst others
-import FunDeps ( grow, checkInstCoverage )
-import Name ( Name, setNameUnique, mkSysTvName )
+import FunDeps
+import Name
import VarSet
-import DynFlags ( dopt, DynFlag(..) )
-import Util ( nOfThem, isSingleton, notNull )
-import ListSetOps ( removeDups )
+import DynFlags
+import Util
+import ListSetOps
+import UniqSupply
import Outputable
import Control.Monad ( when )
%************************************************************************
\begin{code}
+newCoVars :: [(TcType,TcType)] -> TcM [CoVar]
+newCoVars spec
+ = do { us <- newUniqueSupply
+ ; return [ mkCoVar (mkSysTvName uniq FSLIT("co"))
+ (mkCoKind ty1 ty2)
+ | ((ty1,ty2), uniq) <- spec `zip` uniqsFromSupply us] }
+
newKindVar :: TcM TcKind
newKindVar = do { uniq <- newUnique
- ; ref <- newMutVar Nothing
- ; return (KindVar (mkKindVar uniq ref)) }
+ ; ref <- newMutVar Flexi
+ ; return (mkTyVarTy (mkKindVar uniq ref)) }
newKindVars :: Int -> TcM [TcKind]
newKindVars n = mappM (\ _ -> newKindVar) (nOfThem n ())
; ref <- newMutVar Flexi ;
; let name = mkSysTvName uniq fs
fs = case box_info of
- BoxTv -> FSLIT("bx")
+ BoxTv -> FSLIT("t")
TauTv -> FSLIT("t")
SigTv _ -> FSLIT("a")
+ -- We give BoxTv and TauTv the same string, because
+ -- otherwise we get user-visible differences in error
+ -- messages, which are confusing. If you want to see
+ -- the box_info of each tyvar, use -dppr-debug
; return (mkTcTyVar name kind (MetaTv box_info ref)) }
instMetaTyVar :: BoxInfo -> TyVar -> TcM TcTyVar
tcInstBoxyTyVar :: TyVar -> TcM BoxyTyVar
-- Instantiate with a BOXY type variable
tcInstBoxyTyVar tyvar = instMetaTyVar BoxTv tyvar
-
-tcInstBoxy :: TcType -> TcM ([BoxyTyVar], BoxyThetaType, BoxySigmaType)
--- tcInstType instantiates the outer-level for-alls of a TcType with
--- fresh BOXY type variables, splits off the dictionary part,
--- and returns the pieces.
-tcInstBoxy ty = tcInstType (mapM tcInstBoxyTyVar) ty
\end{code}
lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult
lookupTcTyVar tyvar
- = case details of
+ = ASSERT( isTcTyVar tyvar )
+ case details of
SkolemTv _ -> return (DoneTv details)
MetaTv _ ref -> do { meta_details <- readMutVar ref
; case meta_details of
zonkTcPredType (IParam n t)
= zonkTcType t `thenM` \ new_t ->
returnM (IParam n new_t)
+zonkTcPredType (EqPred t1 t2)
+ = zonkTcType t1 `thenM` \ new_t1 ->
+ zonkTcType t2 `thenM` \ new_t2 ->
+ returnM (EqPred new_t1 new_t2)
\end{code}
------------------- These ...ToType, ...ToKind versions
go ty `thenM` \ ty' ->
returnM (ForAllTy tyvar ty')
- go_pred (ClassP c tys) = mappM go tys `thenM` \ tys' ->
- returnM (ClassP c tys')
- go_pred (IParam n ty) = go ty `thenM` \ ty' ->
- returnM (IParam n ty')
+ go_pred (ClassP c tys) = mappM go tys `thenM` \ tys' ->
+ returnM (ClassP c tys')
+ go_pred (IParam n ty) = go ty `thenM` \ ty' ->
+ returnM (IParam n ty')
+ go_pred (EqPred ty1 ty2) = go ty1 `thenM` \ ty1' ->
+ go ty2 `thenM` \ ty2' ->
+ returnM (EqPred ty1' ty2')
zonk_tc_tyvar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable variable
-> TcTyVar -> TcM TcType
%************************************************************************
\begin{code}
-readKindVar :: KindVar -> TcM (Maybe TcKind)
+readKindVar :: KindVar -> TcM (MetaDetails)
writeKindVar :: KindVar -> TcKind -> TcM ()
readKindVar kv = readMutVar (kindVarRef kv)
-writeKindVar kv val = writeMutVar (kindVarRef kv) (Just val)
+writeKindVar kv val = writeMutVar (kindVarRef kv) (Indirect val)
-------------
zonkTcKind :: TcKind -> TcM TcKind
-zonkTcKind (FunKind k1 k2) = do { k1' <- zonkTcKind k1
- ; k2' <- zonkTcKind k2
- ; returnM (FunKind k1' k2') }
-zonkTcKind k@(KindVar kv) = do { mb_kind <- readKindVar kv
- ; case mb_kind of
- Nothing -> returnM k
- Just k -> zonkTcKind k }
-zonkTcKind other_kind = returnM other_kind
+zonkTcKind k = zonkTcType k
-------------
zonkTcKindToKind :: TcKind -> TcM Kind
-zonkTcKindToKind (FunKind k1 k2) = do { k1' <- zonkTcKindToKind k1
- ; k2' <- zonkTcKindToKind k2
- ; returnM (FunKind k1' k2') }
-
-zonkTcKindToKind (KindVar kv) = do { mb_kind <- readKindVar kv
- ; case mb_kind of
- Nothing -> return liftedTypeKind
- Just k -> zonkTcKindToKind k }
-
-zonkTcKindToKind OpenTypeKind = returnM liftedTypeKind -- An "Open" kind defaults to *
-zonkTcKindToKind other_kind = returnM other_kind
+-- When zonking a TcKind to a kind, we need to instantiate kind variables,
+-- Haskell specifies that * is to be used, so we follow that.
+zonkTcKindToKind k = zonkType (\ _ -> return liftedTypeKind) k
\end{code}
%************************************************************************
kind_ok = case ctxt of
TySynCtxt _ -> True -- Any kind will do
- ResSigCtxt -> isOpenTypeKind actual_kind
- ExprSigCtxt -> isOpenTypeKind actual_kind
+ ResSigCtxt -> isSubOpenTypeKind actual_kind
+ ExprSigCtxt -> isSubOpenTypeKind actual_kind
GenPatCtxt -> isLiftedTypeKind actual_kind
ForSigCtxt _ -> isLiftedTypeKind actual_kind
- other -> isArgTypeKind actual_kind
+ other -> isSubArgTypeKind actual_kind
ubx_tup | not gla_exts = UT_NotOk
| otherwise = case ctxt of
= 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 `thenM_`
- check_tau_type (decRank rank) ubx_tup tau `thenM_`
- checkFreeness tvs theta `thenM_`
- checkAmbiguity tvs theta (tyVarsOfType tau)
-
+ | null tvs && null theta
+ = check_tau_type rank ubx_tup ty
+ | otherwise
+ = do { check_valid_theta SigmaCtxt theta
+ ; check_poly_type rank ubx_tup tau -- Allow foralls to right of arrow
+ ; checkFreeness tvs theta
+ ; checkAmbiguity tvs theta (tyVarsOfType tau) }
+ where
+ (tvs, theta, tau) = tcSplitSigmaTy ty
+
----------------------------------------
check_arg_type :: Type -> TcM ()
-- The sort of type that can instantiate a type variable,
-- The Right Thing would be to fix the way that SPECIALISE instance pragmas
-- are handled, but the quick thing is just to permit PredTys here.
check_tau_type rank ubx_tup (PredTy sty) = getDOpts `thenM` \ dflags ->
- check_source_ty dflags TypeCtxt sty
+ check_pred_ty dflags TypeCtxt sty
check_tau_type rank ubx_tup (TyVarTy _) = returnM ()
check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
- = check_poly_type rank UT_NotOk arg_ty `thenM_`
- check_poly_type rank UT_Ok res_ty
+ = check_poly_type (decRank rank) UT_NotOk arg_ty `thenM_`
+ check_poly_type rank UT_Ok res_ty
check_tau_type rank ubx_tup (AppTy ty1 ty2)
= check_arg_type ty1 `thenM_` check_arg_type ty2
check_valid_theta ctxt theta
= getDOpts `thenM` \ dflags ->
warnTc (notNull dups) (dupPredWarn dups) `thenM_`
- mappM_ (check_source_ty dflags ctxt) theta
+ mappM_ (check_pred_ty dflags ctxt) theta
where
(_,dups) = removeDups tcCmpPred theta
-------------------------
-check_source_ty dflags ctxt pred@(ClassP cls tys)
+check_pred_ty dflags ctxt pred@(ClassP cls tys)
= -- Class predicates are valid in all contexts
checkTc (arity == n_tys) arity_err `thenM_`
arity_err = arityErr "Class" class_name arity n_tys
how_to_allow = parens (ptext SLIT("Use -fglasgow-exts to permit this"))
-check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
+check_pred_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
-- Implicit parameters only allows in type
-- signatures; not in instance decls, superclasses etc
-- The reason for not allowing implicit params in instances is a bit subtle
-- instance decl would show up two uses of ?x.
-- Catch-all
-check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
+check_pred_ty dflags ctxt sty = failWithTc (badPredTyErr sty)
-------------------------
check_class_pred_tys dflags ctxt tys
= vcat [ptext SLIT("In the context:") <+> pprTheta theta,
ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
-badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
+badPredTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
predTyVarErr pred = sep [ptext SLIT("Non type-variable argument"),
nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
dupPredWarn dups = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
fvPred :: PredType -> [TyVar]
fvPred (ClassP _ tys') = fvTypes tys'
fvPred (IParam _ ty) = fvType ty
+fvPred (EqPred ty1 ty2) = fvType ty1 ++ fvType ty2
-- Size of a type: the number of variables and constructors
sizeType :: Type -> Int
sizePred :: PredType -> Int
sizePred (ClassP _ tys') = sizeTypes tys'
sizePred (IParam _ ty) = sizeType ty
+sizePred (EqPred ty1 ty2) = sizeType ty1 + sizeType ty2
\end{code}