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,
--------------------------------
-- Creating new coercion variables
- newCoVars,
+ newCoVars, newMetaCoVar,
--------------------------------
-- Instantiation
tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxyTyVar,
tcInstSigTyVars, zonkSigTyVar,
tcInstSkolTyVar, tcInstSkolTyVars, tcInstSkolType,
- tcSkolSigType, tcSkolSigTyVars,
+ tcSkolSigType, tcSkolSigTyVars, occurCheckErr,
--------------------------------
-- Checking type validity
Rank, UserTypeCtxt(..), checkValidType,
SourceTyCtxt(..), checkValidTheta, checkFreeness,
- checkValidInstHead, checkValidInstance, checkAmbiguity,
- checkInstTermination,
- arityErr,
+ checkValidInstHead, checkValidInstance,
+ checkInstTermination, checkValidTypeInst, checkTyFamFreeness,
+ checkUpdateMeta, updateMeta, checkTauTvUpdate, fillBoxWithTau, unifyKindCtxt,
+ unifyKindMisMatch, validDerivPred, arityErr, notMonoType, notMonoArgs,
--------------------------------
-- 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"
import TypeRep
import TcType
import Type
-import Type
import Coercion
import Class
import TyCon
import Maybes
import ListSetOps
import UniqSupply
+import SrcLoc
import Outputable
-import Control.Monad ( when )
+import Control.Monad ( when, unless )
import Data.List ( (\\) )
\end{code}
%************************************************************************
%* *
+ Updating tau types
+%* *
+%************************************************************************
+
+Can't be in TcUnify, as we also need it in TcTyFuns.
+
+\begin{code}
+type SwapFlag = Bool
+ -- False <=> the two args are (actual, expected) respectively
+ -- True <=> the two args are (expected, actual) respectively
+
+checkUpdateMeta :: SwapFlag
+ -> TcTyVar -> IORef MetaDetails -> TcType -> TcM ()
+-- Update tv1, which is flexi; occurs check is alrady done
+-- The 'check' version does a kind check too
+-- We do a sub-kind check here: we might unify (a b) with (c d)
+-- where b::*->* and d::*; this should fail
+
+checkUpdateMeta swapped tv1 ref1 ty2
+ = do { checkKinds swapped tv1 ty2
+ ; updateMeta tv1 ref1 ty2 }
+
+updateMeta :: TcTyVar -> IORef MetaDetails -> TcType -> TcM ()
+updateMeta tv1 ref1 ty2
+ = ASSERT( isMetaTyVar tv1 )
+ ASSERT( isBoxyTyVar tv1 || isTauTy ty2 )
+ do { ASSERTM2( do { details <- readMetaTyVar tv1; return (isFlexi details) }, ppr tv1 )
+ ; traceTc (text "updateMeta" <+> ppr tv1 <+> text ":=" <+> ppr ty2)
+ ; writeMutVar ref1 (Indirect ty2)
+ }
+
+----------------
+checkKinds swapped tv1 ty2
+-- We're about to unify a type variable tv1 with a non-tyvar-type ty2.
+-- ty2 has been zonked at this stage, which ensures that
+-- its kind has as much boxity information visible as possible.
+ | tk2 `isSubKind` tk1 = returnM ()
+
+ | otherwise
+ -- Either the kinds aren't compatible
+ -- (can happen if we unify (a b) with (c d))
+ -- or we are unifying a lifted type variable with an
+ -- unlifted type: e.g. (id 3#) is illegal
+ = addErrCtxtM (unifyKindCtxt swapped tv1 ty2) $
+ unifyKindMisMatch k1 k2
+ where
+ (k1,k2) | swapped = (tk2,tk1)
+ | otherwise = (tk1,tk2)
+ tk1 = tyVarKind tv1
+ tk2 = typeKind ty2
+
+----------------
+checkTauTvUpdate :: TcTyVar -> TcType -> TcM TcType
+-- (checkTauTvUpdate tv ty)
+-- We are about to update the TauTv tv with ty.
+-- Check (a) that tv doesn't occur in ty (occurs check)
+-- (b) that ty is a monotype
+-- Furthermore, in the interest of (b), if you find an
+-- empty box (BoxTv that is Flexi), fill it in with a TauTv
+--
+-- Returns the (non-boxy) type to update the type variable with, or fails
+
+checkTauTvUpdate orig_tv orig_ty
+ = go orig_ty
+ where
+ go (TyConApp tc tys)
+ | isSynTyCon tc = go_syn tc tys
+ | otherwise = do { tys' <- mappM go tys; return (TyConApp tc tys') }
+ go (NoteTy _ ty2) = go ty2 -- Discard free-tyvar annotations
+ 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') }
+ -- NB the mkAppTy; we might have instantiated a
+ -- type variable to a type constructor, so we need
+ -- to pull the TyConApp to the top.
+ go (ForAllTy tv ty) = notMonoType orig_ty -- (b)
+
+ go (TyVarTy tv)
+ | orig_tv == tv = occurCheck tv -- (a)
+ | isTcTyVar tv = go_tyvar tv (tcTyVarDetails tv)
+ | otherwise = return (TyVarTy tv)
+ -- Ordinary (non Tc) tyvars
+ -- occur inside quantified types
+
+ 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 t1 t2) = do { t1' <- go t1; t2' <- go t2; return (EqPred t1' t2') }
+
+ go_tyvar tv (SkolemTv _) = return (TyVarTy tv)
+ go_tyvar tv (MetaTv box ref)
+ = do { cts <- readMutVar ref
+ ; case cts of
+ Indirect ty -> go ty
+ Flexi -> case box of
+ BoxTv -> fillBoxWithTau tv ref
+ other -> return (TyVarTy tv)
+ }
+
+ -- go_syn is called for synonyms only
+ -- See Note [Type synonyms and the occur check]
+ go_syn tc tys
+ | not (isTauTyCon tc)
+ = notMonoType orig_ty -- (b) again
+ | otherwise
+ = do { (msgs, mb_tys') <- tryTc (mapM go tys)
+ ; case mb_tys' of
+ Just tys' -> return (TyConApp tc tys')
+ -- Retain the synonym (the common case)
+ Nothing | isOpenTyCon tc
+ -> notMonoArgs (TyConApp tc tys)
+ -- Synonym families must have monotype args
+ | otherwise
+ -> go (expectJust "checkTauTvUpdate"
+ (tcView (TyConApp tc tys)))
+ -- Try again, expanding the synonym
+ }
+
+ occurCheck tv = occurCheckErr (mkTyVarTy tv) orig_ty
+
+fillBoxWithTau :: BoxyTyVar -> IORef MetaDetails -> TcM TcType
+-- (fillBoxWithTau tv ref) fills ref with a freshly allocated
+-- tau-type meta-variable, whose print-name is the same as tv
+-- Choosing the same name is good: when we instantiate a function
+-- we allocate boxy tyvars with the same print-name as the quantified
+-- tyvar; and then we often fill the box with a tau-tyvar, and again
+-- we want to choose the same name.
+fillBoxWithTau tv ref
+ = do { tv' <- tcInstTyVar tv -- Do not gratuitously forget
+ ; let tau = mkTyVarTy tv' -- name of the type variable
+ ; writeMutVar ref (Indirect tau)
+ ; return tau }
+\end{code}
+
+Error mesages in case of kind mismatch.
+
+\begin{code}
+unifyKindMisMatch ty1 ty2
+ = zonkTcKind ty1 `thenM` \ ty1' ->
+ zonkTcKind ty2 `thenM` \ ty2' ->
+ let
+ msg = hang (ptext SLIT("Couldn't match kind"))
+ 2 (sep [quotes (ppr ty1'),
+ ptext SLIT("against"),
+ quotes (ppr ty2')])
+ in
+ failWithTc msg
+
+unifyKindCtxt swapped tv1 ty2 tidy_env -- not swapped => tv1 expected, ty2 inferred
+ -- tv1 and ty2 are zonked already
+ = returnM msg
+ where
+ msg = (env2, ptext SLIT("When matching the kinds of") <+>
+ sep [quotes pp_expected <+> ptext SLIT("and"), quotes pp_actual])
+
+ (pp_expected, pp_actual) | swapped = (pp2, pp1)
+ | otherwise = (pp1, pp2)
+ (env1, tv1') = tidyOpenTyVar tidy_env tv1
+ (env2, ty2') = tidyOpenType env1 ty2
+ pp1 = ppr tv1' <+> dcolon <+> ppr (tyVarKind tv1)
+ pp2 = ppr ty2' <+> dcolon <+> ppr (typeKind ty2)
+\end{code}
+
+Error message for failure due to an occurs check.
+
+\begin{code}
+occurCheckErr :: TcType -> TcType -> TcM a
+occurCheckErr ty containingTy
+ = do { env0 <- tcInitTidyEnv
+ ; ty' <- zonkTcType ty
+ ; containingTy' <- zonkTcType containingTy
+ ; let (env1, tidy_ty1) = tidyOpenType env0 ty'
+ (env2, tidy_ty2) = tidyOpenType env1 containingTy'
+ extra = sep [ppr tidy_ty1, char '=', ppr tidy_ty2]
+ ; failWithTcM (env2, hang msg 2 extra) }
+ where
+ msg = ptext SLIT("Occurs check: cannot construct the infinite type:")
+\end{code}
+
+%************************************************************************
+%* *
Kind variables
%* *
%************************************************************************
(mkCoKind ty1 ty2)
| ((ty1,ty2), uniq) <- spec `zip` uniqsFromSupply us] }
+newMetaCoVar :: TcType -> TcType -> TcM TcTyVar
+newMetaCoVar ty1 ty2 = newMetaTyVar TauTv (mkCoKind ty1 ty2)
+
newKindVar :: TcM TcKind
newKindVar = do { uniq <- newUnique
; ref <- newMutVar Flexi
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
- = ASSERT( isTcTyVar tyvar )
+ = 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}
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
-- 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
ForSigCtxt _ -> isLiftedTypeKind 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_`
-- 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
\end{code}
-
%************************************************************************
%* *
\subsection{Checking a theta or source type}
(_,dups) = removeDups tcCmpPred theta
-------------------------
+check_pred_ty :: DynFlags -> SourceTyCtxt -> PredType -> TcM ()
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
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"))
+ 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 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
check_pred_ty dflags ctxt sty = failWithTc (badPredTyErr sty)
-------------------------
+check_class_pred_tys :: DynFlags -> SourceTyCtxt -> [Type] -> Bool
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
don't need to check for ambiguity either, because the test can't fail
(see is_ambig).
+
\begin{code}
checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
checkAmbiguity forall_tyvars theta tau_tyvars
complain pred = addErrTc (ambigErr pred)
extended_tau_vars = grow theta tau_tyvars
- -- 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'
+ -- See Note [Implicit parameters and ambiguity] in TcSimplify
is_ambig pred = isClassPred pred &&
any ambig_var (varSetElems (tyVarsOfPred pred))
\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)))
complain pred = addErrTc (freeErr pred)
freeErr pred
- = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
- ptext SLIT("are already in scope"),
- nest 4 (ptext SLIT("(at least one must be universally quantified here)"))
- ]
+ = sep [ ptext SLIT("All of the type variables in the constraint") <+>
+ quotes (pprPred pred)
+ , ptext SLIT("are already in scope") <+>
+ ptext SLIT("(at least one must be universally quantified here)")
+ , nest 4 $
+ ptext SLIT("(Use -XFlexibleContexts to lift this restriction)")
+ ]
\end{code}
\begin{code}
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 -XTypeFamilies 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)
n_arguments | n == 0 = ptext SLIT("no arguments")
| n == 1 = ptext SLIT("1 argument")
| True = hsep [int n, ptext SLIT("arguments")]
+
+-----------------
+notMonoType ty
+ = do { ty' <- zonkTcType ty
+ ; env0 <- tcInitTidyEnv
+ ; let (env1, tidy_ty) = tidyOpenType env0 ty'
+ msg = ptext SLIT("Cannot match a monotype with") <+> quotes (ppr tidy_ty)
+ ; failWithTcM (env1, msg) }
+
+notMonoArgs ty
+ = do { ty' <- zonkTcType ty
+ ; env0 <- tcInitTidyEnv
+ ; let (env1, tidy_ty) = tidyOpenType env0 ty'
+ msg = ptext SLIT("Arguments of type synonym families must be monotypes") <+> quotes (ppr tidy_ty)
+ ; failWithTcM (env1, msg) }
\end{code}
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) $
- mapM_ failWithTc (checkInstTermination inst_tys theta)
+ -- 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)
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.
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}
+
+
+%************************************************************************
+%* *
+ Checking the context of a derived instance declaration
+%* *
+%************************************************************************
+
+Note [Exotic derived instance contexts]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In a 'derived' instance declaration, we *infer* the context. It's a
+bit unclear what rules we should apply for this; the Haskell report is
+silent. Obviously, constraints like (Eq a) are fine, but what about
+ data T f a = MkT (f a) deriving( Eq )
+where we'd get an Eq (f a) constraint. That's probably fine too.
+
+One could go further: consider
+ data T a b c = MkT (Foo a b c) deriving( Eq )
+ instance (C Int a, Eq b, Eq c) => Eq (Foo a b c)
+
+Notice that this instance (just) satisfies the Paterson termination
+conditions. Then we *could* derive an instance decl like this:
+
+ instance (C Int a, Eq b, Eq c) => Eq (T a b c)
+
+even though there is no instance for (C Int a), because there just
+*might* be an instance for, say, (C Int Bool) at a site where we
+need the equality instance for T's.
+
+However, this seems pretty exotic, and it's quite tricky to allow
+this, and yet give sensible error messages in the (much more common)
+case where we really want that instance decl for C.
+
+So for now we simply require that the derived instance context
+should have only type-variable constraints.
+
+Here is another example:
+ data Fix f = In (f (Fix f)) deriving( Eq )
+Here, if we are prepared to allow -fallow-undecidable-instances we
+could derive the instance
+ instance Eq (f (Fix f)) => Eq (Fix f)
+but this is so delicate that I don't think it should happen inside
+'deriving'. If you want this, write it yourself!
+
+NB: if you want to lift this condition, make sure you still meet the
+termination conditions! If not, the deriving mechanism generates
+larger and larger constraints. Example:
+ data Succ a = S a
+ data Seq a = Cons a (Seq (Succ a)) | Nil deriving Show
+
+Note the lack of a Show instance for Succ. First we'll generate
+ instance (Show (Succ a), Show a) => Show (Seq a)
+and then
+ instance (Show (Succ (Succ a)), Show (Succ a), Show a) => Show (Seq a)
+and so on. Instead we want to complain of no instance for (Show (Succ a)).
+
+The bottom line
+~~~~~~~~~~~~~~~
+Allow constraints which consist only of type variables, with no repeats.
+\begin{code}
+validDerivPred :: PredType -> Bool
+validDerivPred (ClassP cls tys) = hasNoDups fvs && sizeTypes tys == length fvs
+ where fvs = fvTypes tys
+validDerivPred otehr = False
+\end{code}
+
+%************************************************************************
+%* *
+ 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
projects / ghc-hetmet.git / blobdiff