--------------------------------
-- Instantiation
tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxyTyVar,
- tcInstSigTyVars,
- tcInstSkolTyVar, tcInstSkolTyVars, tcInstSkolType,
+ tcInstSigType,
+ tcInstSkolTyVars, tcInstSkolType,
tcSkolSigType, tcSkolSigTyVars, occurCheckErr,
--------------------------------
tcSkolSigTyVars info tyvars = [ mkSkolTyVar (tyVarName tv) (tyVarKind tv) info
| tv <- tyvars ]
-tcInstSkolTyVar :: SkolemInfo -> Maybe SrcSpan -> TyVar -> TcM TcTyVar
+tcInstSkolTyVar :: SkolemInfo -> (Name -> 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
+tcInstSkolTyVar info get_loc tyvar
= do { uniq <- newUnique
; let old_name = tyVarName tyvar
kind = tyVarKind tyvar
- loc = mb_loc `orElse` getSrcSpan old_name
+ loc = get_loc old_name
new_name = mkInternalName uniq (nameOccName old_name) loc
; return (mkSkolTyVar new_name kind info) }
-- Get the location from the monad
tcInstSkolTyVars info tyvars
= do { span <- getSrcSpanM
- ; mapM (tcInstSkolTyVar info (Just span)) tyvars }
+ ; mapM (tcInstSkolTyVar info (const 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
+
+tcInstSigType :: Bool -> SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcRhoType)
+-- Instantiate with skolems or meta SigTvs; depending on use_skols
+-- Always take location info from the supplied tyvars
+tcInstSigType use_skols skol_info ty
+ = tcInstType (mapM inst_tyvar) ty
+ where
+ inst_tyvar | use_skols = tcInstSkolTyVar skol_info getSrcSpan
+ | otherwise = instMetaTyVar (SigTv skol_info)
\end{code}
-- 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 )
+ ; traceTc (text "writeMetaTyVar" <+> ppr tyvar <+> text ":=" <+> ppr ty)
; writeMutVar (metaTvRef tyvar) (Indirect ty) }
where
_k1 = tyVarKind tyvar
%************************************************************************
\begin{code}
-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
zonkSigTyVar sig_tv
| isSkolemTyVar sig_tv
* Now abstract over the 'a', but float out the Num (C d a) constraint
because it does not 'really' mention a. (see exactTyVarsOfType)
The arg to foo becomes
- /\a -> \t -> t+t
+ \/\a -> \t -> t+t
* So we get a dict binding for Num (C d a), which is zonked to give
a = ()
quantification, so the floated dict will still have type (C d a).
Which renders this whole note moot; happily!]
-* Then the /\a abstraction has a zonked 'a' in it.
+* Then the \/\a abstraction has a zonked 'a' in it.
All very silly. I think its harmless to ignore the problem. We'll end up with
-a /\a in the final result but all the occurrences of a will be zonked to ()
+a \/\a in the final result but all the occurrences of a will be zonked to ()
Note [Zonking to Skolem]
~~~~~~~~~~~~~~~~~~~~~~~~
rankn <- doptM Opt_RankNTypes
polycomp <- doptM Opt_PolymorphicComponents
let
- rank | rankn = Arbitrary
- | rank2 = Rank 2
- | otherwise
- = case ctxt of -- Haskell 98
- GenPatCtxt -> Rank 0
- LamPatSigCtxt -> Rank 0
- BindPatSigCtxt -> Rank 0
- DefaultDeclCtxt-> Rank 0
- ResSigCtxt -> Rank 0
- TySynCtxt _ -> Rank 0
- ExprSigCtxt -> Rank 1
- FunSigCtxt _ -> Rank 1
- ConArgCtxt _ -> if polycomp
- then Rank 2
+ gen_rank n | rankn = ArbitraryRank
+ | rank2 = Rank 2
+ | otherwise = Rank n
+ rank
+ = case ctxt of
+ DefaultDeclCtxt-> MustBeMonoType
+ ResSigCtxt -> MustBeMonoType
+ LamPatSigCtxt -> gen_rank 0
+ BindPatSigCtxt -> gen_rank 0
+ TySynCtxt _ -> gen_rank 0
+ GenPatCtxt -> gen_rank 1
+ -- This one is a bit of a hack
+ -- See the forall-wrapping in TcClassDcl.mkGenericInstance
+
+ ExprSigCtxt -> gen_rank 1
+ FunSigCtxt _ -> gen_rank 1
+ ConArgCtxt _ | polycomp -> gen_rank 2
-- We are given the type of the entire
-- constructor, hence rank 1
- else Rank 1
- ForSigCtxt _ -> Rank 1
- SpecInstCtxt -> Rank 1
+ | otherwise -> gen_rank 1
+
+ ForSigCtxt _ -> gen_rank 1
+ SpecInstCtxt -> gen_rank 1
actual_kind = typeKind ty
traceTc (text "checkValidType done" <+> ppr ty)
checkValidMonoType :: Type -> TcM ()
-checkValidMonoType ty = check_mono_type ty
+checkValidMonoType ty = check_mono_type MustBeMonoType ty
\end{code}
\begin{code}
-data Rank = Rank Int | Arbitrary
+data Rank = ArbitraryRank -- Any rank ok
+ | MustBeMonoType -- Monotype regardless of flags
+ | TyConArgMonoType -- Monotype but could be poly if -XImpredicativeTypes
+ | Rank Int -- Rank n, but could be more with -XRankNTypes
-decRank :: Rank -> Rank
-decRank Arbitrary = Arbitrary
-decRank (Rank n) = Rank (n-1)
+decRank :: Rank -> Rank -- Function arguments
+decRank (Rank 0) = Rank 0
+decRank (Rank n) = Rank (n-1)
+decRank other_rank = other_rank
nonZeroRank :: Rank -> Bool
-nonZeroRank (Rank 0) = False
-nonZeroRank _ = True
+nonZeroRank ArbitraryRank = True
+nonZeroRank (Rank n) = n>0
+nonZeroRank _ = False
----------------------------------------
data UbxTupFlag = UT_Ok | UT_NotOk
-- The "Ok" version means "ok if UnboxedTuples is on"
----------------------------------------
-check_mono_type :: Type -> TcM () -- No foralls anywhere
- -- No unlifted types of any kind
-check_mono_type ty
- = do { check_type (Rank 0) UT_NotOk ty
+check_mono_type :: Rank -> Type -> TcM () -- No foralls anywhere
+ -- No unlifted types of any kind
+check_mono_type rank ty
+ = do { check_type rank UT_NotOk ty
; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
check_type :: Rank -> UbxTupFlag -> Type -> TcM ()
--- The args say what the *type* context requires, independent
+-- The args say what the *type context* requires, independent
-- of *flag* settings. You test the flag settings at usage sites.
--
-- Rank is allowed rank for function args
check_type rank ubx_tup ty
| not (null tvs && null theta)
- = do { checkTc (nonZeroRank rank) (forAllTyErr ty)
+ = do { checkTc (nonZeroRank rank) (forAllTyErr rank ty)
-- Reject e.g. (Maybe (?x::Int => Int)),
-- with a decent error message
; check_valid_theta SigmaCtxt theta
; liberal <- doptM Opt_LiberalTypeSynonyms
; if not liberal || isOpenSynTyCon tc then
-- For H98 and synonym families, do check the type args
- mapM_ check_mono_type tys
+ mapM_ (check_mono_type TyConArgMonoType) tys
else -- In the liberal case (only for closed syns), expand then check
case tcView ty of
; checkTc (ubx_tup_ok ub_tuples_allowed) ubx_tup_msg
; impred <- doptM Opt_ImpredicativeTypes
- ; let rank' = if impred then rank else Rank 0
+ ; let rank' = if impred then ArbitraryRank else TyConArgMonoType
-- c.f. check_arg_type
-- However, args are allowed to be unlifted, or
-- more unboxed tuples, so can't use check_arg_ty
check_arg_type rank ty
= do { impred <- doptM Opt_ImpredicativeTypes
- ; let rank' = if impred then rank else Rank 0 -- Monotype unless impredicative
+ ; let rank' = if impred then ArbitraryRank -- Arg of tycon can have arby rank, regardless
+ else case rank of -- Predictive => must be monotype
+ MustBeMonoType -> MustBeMonoType
+ _ -> TyConArgMonoType
+ -- Make sure that MustBeMonoType is propagated,
+ -- so that we don't suggest -XImpredicativeTypes in
+ -- (Ord (forall a.a)) => a -> a
+
; check_type rank' UT_NotOk ty
; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
----------------------------------------
-forAllTyErr, unliftedArgErr, ubxArgTyErr :: Type -> SDoc
-forAllTyErr ty = sep [ptext (sLit "Illegal polymorphic or qualified type:"), ppr ty]
+forAllTyErr :: Rank -> Type -> SDoc
+forAllTyErr rank ty
+ = vcat [ hang (ptext (sLit "Illegal polymorphic or qualified type:")) 2 (ppr ty)
+ , suggestion ]
+ where
+ suggestion = case rank of
+ Rank _ -> ptext (sLit "Perhaps you intended to use -XRankNTypes or -XRank2Types")
+ TyConArgMonoType -> ptext (sLit "Perhaps you intended to use -XImpredicativeTypes")
+ _ -> empty -- Polytype is always illegal
+
+unliftedArgErr, ubxArgTyErr :: Type -> SDoc
unliftedArgErr ty = sep [ptext (sLit "Illegal unlifted type:"), ppr ty]
ubxArgTyErr ty = sep [ptext (sLit "Illegal unboxed tuple type as function argument:"), ppr ty]
; checkTc (arity == n_tys) arity_err
-- Check the form of the argument types
- ; mapM_ check_mono_type tys
+ ; mapM_ checkValidMonoType tys
; checkTc (check_class_pred_tys dflags ctxt tys)
(predTyVarErr pred $$ how_to_allow)
}
; checkTc (dopt Opt_TypeFamilies dflags) (eqPredTyErr pred)
-- Check the form of the argument types
- ; check_mono_type ty1
- ; check_mono_type ty2
+ ; checkValidMonoType ty1
+ ; checkValidMonoType ty2
}
-check_pred_ty _ SigmaCtxt (IParam _ ty) = check_mono_type ty
+check_pred_ty _ SigmaCtxt (IParam _ ty) = checkValidMonoType 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
Just (clas,tys) -> do
dflags <- getDOpts
- mapM_ check_mono_type tys
check_inst_head dflags clas tys
return (clas, tys)
}}
check_inst_head :: DynFlags -> Class -> [Type] -> TcM ()
check_inst_head dflags clas tys
- -- If GlasgowExts then check at least one isn't a type variable
- = 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_mono_type tys
+ = do { -- If GlasgowExts then check at least one isn't a type variable
+ ; 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)
+ -- May not contain type family applications
+ ; mapM_ checkTyFamFreeness tys
+
+ ; mapM_ checkValidMonoType tys
-- For now, I only allow tau-types (not polytypes) in
-- the head of an instance decl.
-- E.g. instance C (forall a. a->a) is rejected
-- One could imagine generalising that, but I'm not sure
-- what all the consequences might be
+ }
where
head_type_synonym_msg = parens (
; mapM_ checkTyFamFreeness typats
-- the right-hand side is a tau type
- ; checkTc (isTauTy rhs) $
- polyTyErr rhs
+ ; checkValidMonoType rhs
-- we have a decidable instance unless otherwise permitted
; undecidable_ok <- doptM Opt_UndecidableInstances
checkTyFamFreeness :: Type -> TcM ()
checkTyFamFreeness ty
= checkTc (isTyFamFree ty) $
- tyFamInstInIndexErr ty
+ tyFamInstIllegalErr ty
-- Check that a type does not contain any type family applications.
--
-- Error messages
-tyFamInstInIndexErr :: Type -> SDoc
-tyFamInstInIndexErr ty
- = hang (ptext (sLit "Illegal type family application in type instance") <>
+tyFamInstIllegalErr :: Type -> SDoc
+tyFamInstIllegalErr ty
+ = hang (ptext (sLit "Illegal type synonym family application in instance") <>
colon) 4 $
ppr ty
-polyTyErr :: Type -> SDoc
-polyTyErr ty
- = hang (ptext (sLit "Illegal polymorphic type in type instance") <> colon) 4 $
- ppr ty
-
famInstUndecErr :: Type -> SDoc -> SDoc
famInstUndecErr ty msg
= sep [msg,