%
+% (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 (
--------------------------------
-- Zonking
zonkType, zonkTcPredType,
- zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkQuantifiedTyVar,
+ zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV,
+ zonkQuantifiedTyVar, zonkQuantifiedTyVars,
zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
- zonkTcKindToKind, zonkTcKind,
+ zonkTcKindToKind, zonkTcKind, zonkTopTyVar,
readKindVar, writeKindVar
#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, UserTypeCtxt(..), kindVarRef,
- mkKindVar, 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 Type ( Kind, KindVar,
- isLiftedTypeKind, isSubArgTypeKind, isSubOpenTypeKind,
- liftedTypeKind, defaultKind
- )
-import Type ( TvSubst, zipTopTvSubst, substTy )
-import Coercion ( mkCoKind )
-import Class ( Class, classArity, className )
-import TyCon ( TyCon, isSynTyCon, isUnboxedTupleTyCon,
- tyConArity, tyConName )
-import Var ( TyVar, tyVarKind, tyVarName, isTcTyVar,
- mkTyVar, mkTcTyVar, tcTyVarDetails,
- CoVar, mkCoVar )
-
- -- Assertions
-#ifdef DEBUG
-import TcType ( isFlexi, isBoxyTyVar, isImmutableTyVar )
-import Type ( isSubKind )
-#endif
+import TypeRep
+import TcType
+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 UniqSupply ( uniqsFromSupply )
+import ErrUtils
+import DynFlags
+import Util
+import Maybes
+import ListSetOps
+import UniqSupply
+import SrcLoc
import Outputable
import Control.Monad ( when )
import Data.List ( (\\) )
-
\end{code}
tcSkolSigTyVars info tyvars = [ mkSkolTyVar (tyVarName tv) (tyVarKind tv) info
| tv <- tyvars ]
-tcInstSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
--- Instantiate a type with fresh skolem constants
-tcInstSkolType info ty = tcInstType (tcInstSkolTyVars info) ty
-
-tcInstSkolTyVar :: SkolemInfo -> TyVar -> TcM TcTyVar
-tcInstSkolTyVar info tyvar
+tcInstSkolTyVar :: SkolemInfo -> Maybe SrcLoc -> TyVar -> TcM TcTyVar
+-- Instantiate the tyvar, using
+-- * the occ-name and kind of the supplied tyvar,
+-- * the unique from the monad,
+-- * the location either from the tyvar (mb_loc = Nothing)
+-- or from mb_loc (Just loc)
+tcInstSkolTyVar info mb_loc tyvar
= do { uniq <- newUnique
- ; let name = setNameUnique (tyVarName tyvar) uniq
- kind = tyVarKind tyvar
- ; return (mkSkolTyVar name kind info) }
+ ; let old_name = tyVarName tyvar
+ kind = tyVarKind tyvar
+ loc = mb_loc `orElse` getSrcLoc old_name
+ new_name = mkInternalName uniq (nameOccName old_name) loc
+ ; return (mkSkolTyVar new_name kind info) }
tcInstSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
-tcInstSkolTyVars info tyvars = mapM (tcInstSkolTyVar info) tyvars
+-- Get the location from the monad
+tcInstSkolTyVars info tyvars
+ = do { span <- getSrcSpanM
+ ; mapM (tcInstSkolTyVar info (Just (srcSpanStart span))) tyvars }
+
+tcInstSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
+-- Instantiate a type with fresh skolem constants
+-- Binding location comes from the monad
+tcInstSkolType info ty = tcInstType (tcInstSkolTyVars info) ty
\end{code}
%************************************************************************
\begin{code}
-tcInstSigTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
--- Instantiate with meta SigTvs
-tcInstSigTyVars skol_info tyvars
+tcInstSigTyVars :: Bool -> SkolemInfo -> [TyVar] -> TcM [TcTyVar]
+-- Instantiate with skolems or meta SigTvs; depending on use_skols
+-- Always take location info from the supplied tyvars
+tcInstSigTyVars use_skols skol_info tyvars
+ | use_skols
+ = mapM (tcInstSkolTyVar skol_info Nothing) tyvars
+
+ | otherwise
= mapM (instMetaTyVar (SigTv skol_info)) tyvars
zonkSigTyVar :: TcTyVar -> TcM TcTyVar
lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult
lookupTcTyVar tyvar
- = case details of
+ = ASSERT2( isTcTyVar tyvar, ppr tyvar )
+ case details of
SkolemTv _ -> return (DoneTv details)
MetaTv _ ref -> do { meta_details <- readMutVar ref
; case meta_details of
are used at the end of type checking
\begin{code}
+zonkTopTyVar :: TcTyVar -> TcM TcTyVar
+-- zonkTopTyVar is used, at the top level, on any un-instantiated meta type variables
+-- to default the kind of ? and ?? etc to *. This is important to ensure that
+-- instance declarations match. For example consider
+-- instance Show (a->b)
+-- foo x = show (\_ -> True)
+-- Then we'll get a constraint (Show (p ->q)) where p has argTypeKind (printed ??),
+-- and that won't match the typeKind (*) in the instance decl.
+--
+-- Because we are at top level, no further constraints are going to affect these
+-- type variables, so it's time to do it by hand. However we aren't ready
+-- to default them fully to () or whatever, because the type-class defaulting
+-- rules have yet to run.
+
+zonkTopTyVar tv
+ | k `eqKind` default_k = return tv
+ | otherwise
+ = do { tv' <- newFlexiTyVar default_k
+ ; writeMetaTyVar tv (mkTyVarTy tv')
+ ; return tv' }
+ where
+ k = tyVarKind tv
+ default_k = defaultKind k
+
+zonkQuantifiedTyVars :: [TcTyVar] -> TcM [TyVar]
+zonkQuantifiedTyVars = mappM zonkQuantifiedTyVar
+
zonkQuantifiedTyVar :: TcTyVar -> TcM TyVar
-- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it.
--- It might be a meta TyVar, in which case we freeze it into an ordinary TyVar.
--- When we do this, we also default the kind -- see notes with Kind.defaultKind
+--
+-- The quantified type variables often include meta type variables
+-- we want to freeze them into ordinary type variables, and
+-- default their kind (e.g. from OpenTypeKind to TypeKind)
+-- -- see notes with Kind.defaultKind
-- The meta tyvar is updated to point to the new regular TyVar. Now any
-- bound occurences of the original type variable will get zonked to
-- the immutable version.
--
-- We leave skolem TyVars alone; they are immutable.
zonkQuantifiedTyVar tv
- | isSkolemTyVar tv = return tv
+ | ASSERT( isTcTyVar tv )
+ isSkolemTyVar tv = return tv
-- It might be a skolem type variable,
-- for example from a user type signature
ConArgCtxt _ -> Rank 1 -- We are given the type of the entire
-- constructor, hence rank 1
ForSigCtxt _ -> Rank 1
- RuleSigCtxt _ -> Rank 1
SpecInstCtxt -> Rank 1
actual_kind = typeKind ty
-------------------------
check_pred_ty dflags ctxt pred@(ClassP cls tys)
- = -- Class predicates are valid in all contexts
- checkTc (arity == n_tys) arity_err `thenM_`
-
- -- Check the form of the argument types
- mappM_ check_arg_type tys `thenM_`
- checkTc (check_class_pred_tys dflags ctxt tys)
- (predTyVarErr pred $$ how_to_allow)
-
+ = do { -- Class predicates are valid in all contexts
+ ; checkTc (arity == n_tys) arity_err
+
+ -- Check the form of the argument types
+ ; mappM_ check_arg_type tys
+ ; checkTc (check_class_pred_tys dflags ctxt tys)
+ (predTyVarErr pred $$ how_to_allow)
+ }
where
class_name = className cls
arity = classArity cls
arity_err = arityErr "Class" class_name arity n_tys
how_to_allow = parens (ptext SLIT("Use -fglasgow-exts to permit this"))
+check_pred_ty dflags ctxt pred@(EqPred ty1 ty2)
+ = do { -- Equational constraints are valid in all contexts if indexed
+ -- types are permitted
+ ; checkTc (dopt Opt_IndexedTypes dflags) (eqPredTyErr pred)
+
+ -- Check the form of the argument types
+ ; check_eq_arg_type ty1
+ ; check_eq_arg_type ty2
+ }
+ where
+ check_eq_arg_type = check_poly_type (Rank 0) UT_NotOk
+
check_pred_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
- -- Implicit parameters only allows in type
+ -- Implicit parameters only allowed in type
-- signatures; not in instance decls, superclasses etc
- -- The reason for not allowing implicit params in instances is a bit subtle
+ -- The reason for not allowing implicit params in instances is a bit
+ -- subtle.
-- If we allowed instance (?x::Int, Eq a) => Foo [a] where ...
-- then when we saw (e :: (?x::Int) => t) it would be unclear how to
-- discharge all the potential usas of the ?x in e. For example, a
\begin{code}
checkFreeness forall_tyvars theta
- = mappM_ complain (filter is_free theta)
+ = do { gla_exts <- doptM Opt_GlasgowExts
+ ; if gla_exts then return () -- New! Oct06
+ else mappM_ complain (filter is_free theta) }
where
is_free pred = not (isIPPred pred)
&& not (any bound_var (varSetElems (tyVarsOfPred pred)))
ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
badPredTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
+eqPredTyErr sty = ptext SLIT("Illegal equational constraint") <+> pprPred sty
+ $$
+ parens (ptext SLIT("Use -findexed-types to permit this"))
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)
-- Check that instance inference will terminate (if we care)
-- For Haskell 98, checkValidTheta has already done that
; when (gla_exts && not undecidable_ok) $
- checkInstTermination theta inst_tys
+ mapM_ addErrTc (checkInstTermination inst_tys theta)
-- The Coverage Condition
; checkTc (undecidable_ok || checkInstCoverage clas inst_tys)
(instTypeErr (pprClassPred clas inst_tys) msg)
}
where
- msg = parens (ptext SLIT("the Coverage Condition fails for one of the functional dependencies"))
+ msg = parens (vcat [ptext SLIT("the Coverage Condition fails for one of the functional dependencies;"),
+ undecidableMsg])
\end{code}
Termination test: each assertion in the context satisfies
\begin{code}
-checkInstTermination :: ThetaType -> [TcType] -> TcM ()
-checkInstTermination theta tys
- = do { mappM_ (check_nomore (fvTypes tys)) theta
- ; mappM_ (check_smaller (sizeTypes tys)) theta }
-
-check_nomore :: [TyVar] -> PredType -> TcM ()
-check_nomore fvs pred
- = checkTc (null (fvPred pred \\ fvs))
- (predUndecErr pred nomoreMsg $$ parens undecidableMsg)
-
-check_smaller :: Int -> PredType -> TcM ()
-check_smaller n pred
- = checkTc (sizePred pred < n)
- (predUndecErr pred smallerMsg $$ parens undecidableMsg)
+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 pred msg = sep [msg,
nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
projects / ghc-hetmet.git / blobdiff