%
+% (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}
+{-# OPTIONS -w #-}
+-- The above warning supression flag is a temporary kludge.
+-- While working on this module you are encouraged to remove it and fix
+-- any warnings in the module. See
+-- http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
+-- for details
+
module TcMType (
TcTyVar, TcKind, TcType, TcTauType, TcThetaType, TcTyVarSet,
newBoxyTyVar, newBoxyTyVars, newBoxyTyVarTys, readFilledBox,
--------------------------------
+ -- Creating new coercion variables
+ newCoVars,
+
+ --------------------------------
-- Instantiation
tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxyTyVar,
tcInstSigTyVars, zonkSigTyVar,
Rank, UserTypeCtxt(..), checkValidType,
SourceTyCtxt(..), checkValidTheta, checkFreeness,
checkValidInstHead, checkValidInstance, checkAmbiguity,
- checkInstTermination,
+ checkInstTermination, checkValidTypeInst, checkTyFamFreeness,
arityErr,
--------------------------------
-- Zonking
zonkType, zonkTcPredType,
- zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkQuantifiedTyVar,
+ zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV,
+ zonkQuantifiedTyVar, zonkQuantifiedTyVars,
zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
- zonkTcKindToKind, zonkTcKind,
+ zonkTcKindToKind, zonkTcKind, zonkTopTyVar,
readKindVar, writeKindVar
-
) where
#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(..),
- 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 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 ErrUtils
+import DynFlags
+import Util
+import Maybes
+import ListSetOps
+import UniqSupply
+import SrcLoc
import Outputable
-import Control.Monad ( when )
+import Control.Monad ( when, unless )
import Data.List ( (\\) )
\end{code}
%************************************************************************
\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 ())
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 SrcSpan -> 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` getSrcSpan 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 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}
-- Make a new meta tyvar out of thin air
newMetaTyVar box_info kind
= do { uniq <- newUnique
- ; ref <- newMutVar Flexi ;
+ ; ref <- newMutVar Flexi
; let name = mkSysTvName uniq fs
fs = case box_info of
BoxTv -> FSLIT("t")
-- come from an existing TyVar
instMetaTyVar box_info tyvar
= do { uniq <- newUnique
- ; ref <- newMutVar Flexi ;
+ ; ref <- newMutVar Flexi
; let name = setNameUnique (tyVarName tyvar) uniq
kind = tyVarKind tyvar
; return (mkTcTyVar name kind (MetaTv box_info ref)) }
| otherwise
= ASSERT( isMetaTyVar tyvar )
- ASSERT2( k2 `isSubKind` k1, (ppr tyvar <+> ppr k1) $$ (ppr ty <+> ppr k2) )
+ -- TOM: It should also work for coercions
+ -- ASSERT2( k2 `isSubKind` k1, (ppr tyvar <+> ppr k1) $$ (ppr ty <+> ppr k2) )
do { ASSERTM2( do { details <- readMetaTyVar tyvar; return (isFlexi details) }, ppr tyvar )
; writeMutVar (metaTvRef tyvar) (Indirect ty) }
where
%************************************************************************
\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
readFilledBox box_tv = ASSERT( isBoxyTyVar box_tv )
do { cts <- readMetaTyVar box_tv
; case cts of
- Flexi -> pprPanic "readFilledBox" (ppr box_tv)
+ Flexi -> pprPanic "readFilledBox" (ppr box_tv)
Indirect ty -> return ty }
tcInstBoxyTyVar :: TyVar -> TcM BoxyTyVar
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
Indirect ty -> return (IndirectTv ty)
- Flexi -> return (DoneTv details) }
+ Flexi -> return (DoneTv details) }
where
details = tcTyVarDetails tyvar
returnM (tyVarsOfTypes tys)
zonkTcTyVar :: TcTyVar -> TcM TcType
-zonkTcTyVar tyvar = ASSERT( isTcTyVar tyvar )
+zonkTcTyVar tyvar = ASSERT2( isTcTyVar tyvar, ppr tyvar)
zonk_tc_tyvar (\ tv -> returnM (TyVarTy tv)) tyvar
\end{code}
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
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
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}
%************************************************************************
-- Checks that the type is valid for the given context
checkValidType ctxt ty
= traceTc (text "checkValidType" <+> ppr ty) `thenM_`
- doptM Opt_GlasgowExts `thenM` \ gla_exts ->
+ doptM Opt_UnboxedTuples `thenM` \ unboxed ->
+ doptM Opt_Rank2Types `thenM` \ rank2 ->
+ doptM Opt_RankNTypes `thenM` \ rankn ->
+ doptM Opt_PolymorphicComponents `thenM` \ polycomp ->
let
- rank | gla_exts = Arbitrary
+ rank | rankn = Arbitrary
+ | rank2 = Rank 2
| otherwise
= case ctxt of -- Haskell 98
GenPatCtxt -> Rank 0
TySynCtxt _ -> Rank 0
ExprSigCtxt -> Rank 1
FunSigCtxt _ -> Rank 1
- ConArgCtxt _ -> Rank 1 -- We are given the type of the entire
- -- constructor, hence rank 1
+ ConArgCtxt _ -> if polycomp
+ then Rank 2
+ -- We are given the type of the entire
+ -- constructor, hence rank 1
+ else Rank 1
ForSigCtxt _ -> Rank 1
- RuleSigCtxt _ -> Rank 1
SpecInstCtxt -> Rank 1
actual_kind = typeKind ty
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
- TySynCtxt _ -> UT_Ok
- ExprSigCtxt -> UT_Ok
- other -> UT_NotOk
- -- Unboxed tuples ok in function results,
- -- but for type synonyms we allow them even at
- -- top level
+ ubx_tup = case ctxt of
+ TySynCtxt _ | unboxed -> UT_Ok
+ ExprSigCtxt | unboxed -> UT_Ok
+ _ -> UT_NotOk
in
-- Check that the thing has kind Type, and is lifted if necessary
checkTc kind_ok (kindErr actual_kind) `thenM_`
-- 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)
-- type Foo a = Tree [a]
-- f :: Foo a b -> ...
; case tcView ty of
- Just ty' -> check_tau_type rank ubx_tup ty' -- Check expansion
- Nothing -> failWithTc arity_msg
-
- ; gla_exts <- doptM Opt_GlasgowExts
- ; if gla_exts then
- -- If -fglasgow-exts then don't check the type arguments
+ Just ty' -> check_tau_type rank ubx_tup ty' -- Check expansion
+ Nothing -> unless (isOpenTyCon tc -- No expansion if open
+ && tyConArity tc <= length tys) $
+ failWithTc arity_msg
+
+ ; ok <- doptM Opt_PartiallyAppliedClosedTypeSynonyms
+ ; if ok && not (isOpenTyCon tc) then
+ -- Don't check the type arguments of *closed* synonyms.
-- This allows us to instantiate a synonym defn with a
-- for-all type, or with a partially-applied type synonym.
-- e.g. type T a b = a
}
| isUnboxedTupleTyCon tc
- = doptM Opt_GlasgowExts `thenM` \ gla_exts ->
- checkTc (ubx_tup_ok gla_exts) ubx_tup_msg `thenM_`
+ = doptM Opt_UnboxedTuples `thenM` \ ub_tuples_allowed ->
+ checkTc (ubx_tup_ok ub_tuples_allowed) ubx_tup_msg `thenM_`
mappM_ (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
= mappM_ check_arg_type tys
where
- ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
+ ubx_tup_ok ub_tuples_allowed = case ubx_tup of { UT_Ok -> ub_tuples_allowed; other -> False }
n_args = length tys
tc_arity = tyConArity tc
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)
- = -- 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)
-
+check_pred_ty dflags ctxt pred@(ClassP cls tys)
+ = 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
n_tys = length tys
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
- -- Implicit parameters only allows in type
+ how_to_allow = parens (ptext SLIT("Use -XFlexibleContexts to permit this"))
+
+check_pred_ty dflags ctxt pred@(EqPred ty1 ty2)
+ = do { -- Equational constraints are valid in all contexts if type
+ -- families are permitted
+ ; checkTc (dopt Opt_TypeFamilies 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 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
-- 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
= case ctxt of
TypeCtxt -> True -- {-# SPECIALISE instance Eq (T Int) #-} is fine
- InstThetaCtxt -> gla_exts || undecidable_ok || all tcIsTyVarTy tys
+ InstThetaCtxt -> flexible_contexts || undecidable_ok || all tcIsTyVarTy tys
-- Further checks on head and theta in
-- checkInstTermination
- other -> gla_exts || all tyvar_head tys
+ other -> flexible_contexts || all tyvar_head tys
where
- gla_exts = dopt Opt_GlasgowExts dflags
- undecidable_ok = dopt Opt_AllowUndecidableInstances dflags
+ flexible_contexts = dopt Opt_FlexibleContexts dflags
+ undecidable_ok = dopt Opt_UndecidableInstances dflags
-------------------------
tyvar_head ty -- Haskell 98 allows predicates of form
\begin{code}
checkFreeness forall_tyvars theta
- = mappM_ complain (filter is_free theta)
+ = do { flexible_contexts <- doptM Opt_FlexibleContexts
+ ; unless flexible_contexts $ mappM_ complain (filter is_free theta) }
where
is_free pred = not (isIPPred pred)
&& not (any bound_var (varSetElems (tyVarsOfPred pred)))
= 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
+eqPredTyErr sty = ptext SLIT("Illegal equational constraint") <+> pprPred sty
+ $$
+ parens (ptext SLIT("Use -ftype-families 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_inst_head dflags clas tys
-- If GlasgowExts then check at least one isn't a type variable
- | dopt Opt_GlasgowExts dflags
- = mapM_ check_one tys
-
- -- WITH HASKELL 98, MUST HAVE C (T a b c)
- | otherwise
- = checkTc (isSingleton tys && tcValidInstHeadTy first_ty)
- (instTypeErr (pprClassPred clas tys) head_shape_msg)
-
+ = do checkTc (dopt Opt_TypeSynonymInstances dflags ||
+ all tcInstHeadTyNotSynonym tys)
+ (instTypeErr (pprClassPred clas tys) head_type_synonym_msg)
+ checkTc (dopt Opt_FlexibleInstances dflags ||
+ all tcInstHeadTyAppAllTyVars tys)
+ (instTypeErr (pprClassPred clas tys) head_type_args_tyvars_msg)
+ checkTc (dopt Opt_MultiParamTypeClasses dflags ||
+ isSingleton tys)
+ (instTypeErr (pprClassPred clas tys) head_one_type_msg)
+ mapM_ check_one tys
where
- (first_ty : _) = tys
+ 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 (
+ text "All instance types must be of the form (T a1 ... an)" $$
+ text "where a1 ... an are distinct type *variables*" $$
+ text "Use -XFlexibleInstances if you want to disable this.")
- 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")
+ 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.")
-- For now, I only allow tau-types (not polytypes) in
-- the head of an instance decl.
\begin{code}
checkValidInstance :: [TyVar] -> ThetaType -> Class -> [TcType] -> TcM ()
checkValidInstance tyvars theta clas inst_tys
- = do { gla_exts <- doptM Opt_GlasgowExts
- ; undecidable_ok <- doptM Opt_AllowUndecidableInstances
+ = do { undecidable_ok <- doptM Opt_UndecidableInstances
; checkValidTheta InstThetaCtxt theta
; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys)
-- 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
+ -- For Haskell 98 this will already have been done by checkValidTheta,
+ -- but as we may be using other extensions we need to check.
+ ; unless undecidable_ok $
+ 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
+Termination test: the so-called "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.
\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)]
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 -fallow-undecidable-instances to permit this")
+\end{code}
+
+%************************************************************************
+%* *
+\subsection{Checking type instance well-formedness and termination}
+%* *
+%************************************************************************
+
+\begin{code}
+-- Check that a "type instance" is well-formed (which includes decidability
+-- unless -fallow-undecidable-instances is given).
+--
+checkValidTypeInst :: [Type] -> Type -> TcM ()
+checkValidTypeInst typats rhs
+ = do { -- left-hand side contains no type family applications
+ -- (vanilla synonyms are fine, though)
+ ; mappM_ checkTyFamFreeness typats
+
+ -- the right-hand side is a tau type
+ ; checkTc (isTauTy rhs) $
+ polyTyErr rhs
+
+ -- we have a decidable instance unless otherwise permitted
+ ; undecidable_ok <- doptM Opt_UndecidableInstances
+ ; unless undecidable_ok $
+ mapM_ addErrTc (checkFamInst typats (tyFamInsts rhs))
+ }
+
+-- Make sure that each type family instance is
+-- (1) strictly smaller than the lhs,
+-- (2) mentions no type variable more often than the lhs, and
+-- (3) does not contain any further type family instances.
+--
+checkFamInst :: [Type] -- lhs
+ -> [(TyCon, [Type])] -- type family instances
+ -> [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
+
+-- Ensure that no type family instances occur in a type.
+--
+checkTyFamFreeness :: Type -> TcM ()
+checkTyFamFreeness ty
+ = checkTc (isTyFamFree ty) $
+ tyFamInstInIndexErr ty
+
+-- Check that a type does not contain any type family applications.
+--
+isTyFamFree :: Type -> Bool
+isTyFamFree = null . tyFamInsts
+
+-- Error messages
+
+tyFamInstInIndexErr ty
+ = hang (ptext SLIT("Illegal type family application in type instance") <>
+ colon) 4 $
+ ppr ty
+
+polyTyErr ty
+ = hang (ptext SLIT("Illegal polymorphic type in type instance") <> colon) 4 $
+ ppr ty
+
+famInstUndecErr ty msg
+ = sep [msg,
+ nest 2 (ptext SLIT("in the type family application:") <+>
+ pprType ty)]
+
+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}
-- Free variables of a type, retaining repetitions, and expanding synonyms
fvType :: Type -> [TyVar]
fvType ty | Just exp_ty <- tcView ty = fvType exp_ty
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
+
+-- Type family instances occuring in a type after expanding synonyms
+tyFamInsts :: Type -> [(TyCon, [Type])]
+tyFamInsts ty
+ | Just exp_ty <- tcView ty = tyFamInsts exp_ty
+tyFamInsts (TyVarTy _) = []
+tyFamInsts (TyConApp tc tys)
+ | isOpenSynTyCon tc = [(tc, tys)]
+ | otherwise = concat (map tyFamInsts tys)
+tyFamInsts (FunTy ty1 ty2) = tyFamInsts ty1 ++ tyFamInsts ty2
+tyFamInsts (AppTy ty1 ty2) = tyFamInsts ty1 ++ tyFamInsts ty2
+tyFamInsts (ForAllTy _ ty) = tyFamInsts ty
\end{code}
projects / ghc-hetmet.git / blobdiff