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,
Rank, UserTypeCtxt(..), checkValidType,
SourceTyCtxt(..), checkValidTheta, checkFreeness,
checkValidInstHead, checkValidInstance, checkAmbiguity,
- checkInstTermination,
+ checkInstTermination, checkValidTypeInst, checkTyFamFreeness,
arityErr,
--------------------------------
zonkTcKindToKind, zonkTcKind, zonkTopTyVar,
readKindVar, writeKindVar
-
) where
#include "HsVersions.h"
-- 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
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
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
-- 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 | rankn = Arbitrary
| rank2 = Rank 2
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
SpecInstCtxt -> Rank 1
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_`
&& tyConArity tc <= length tys) $
failWithTc arity_msg
- ; gla_exts <- doptM Opt_GlasgowExts
- ; if gla_exts && not (isOpenTyCon tc) then
- -- If -fglasgow-exts then don't check the type arguments of
- -- *closed* synonyms.
+ ; 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
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
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
- = do { gla_exts <- doptM Opt_GlasgowExts
- ; if gla_exts then return () -- New! Oct06
- else 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)))
\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) $
+ -- 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
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
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