2 % (c) The University of Glasgow 2006
3 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
6 Monadic type operations
8 This module contains monadic operations over types that contain
13 -- The above warning supression flag is a temporary kludge.
14 -- While working on this module you are encouraged to remove it and fix
15 -- any warnings in the module. See
16 -- http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
20 TcTyVar, TcKind, TcType, TcTauType, TcThetaType, TcTyVarSet,
22 --------------------------------
23 -- Creating new mutable type variables
25 newFlexiTyVarTy, -- Kind -> TcM TcType
26 newFlexiTyVarTys, -- Int -> Kind -> TcM [TcType]
27 newKindVar, newKindVars,
28 lookupTcTyVar, LookupTyVarResult(..),
29 newMetaTyVar, readMetaTyVar, writeMetaTyVar,
31 --------------------------------
32 -- Boxy type variables
33 newBoxyTyVar, newBoxyTyVars, newBoxyTyVarTys, readFilledBox,
35 --------------------------------
36 -- Creating new coercion variables
37 newCoVars, newMetaCoVar,
39 --------------------------------
41 tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxyTyVar,
42 tcInstSigTyVars, zonkSigTyVar,
43 tcInstSkolTyVar, tcInstSkolTyVars, tcInstSkolType,
44 tcSkolSigType, tcSkolSigTyVars, occurCheckErr,
46 --------------------------------
47 -- Checking type validity
48 Rank, UserTypeCtxt(..), checkValidType,
49 SourceTyCtxt(..), checkValidTheta, checkFreeness,
50 checkValidInstHead, checkValidInstance,
51 checkInstTermination, checkValidTypeInst, checkTyFamFreeness,
52 checkUpdateMeta, updateMeta, checkTauTvUpdate, fillBoxWithTau, unifyKindCtxt,
53 unifyKindMisMatch, validDerivPred, arityErr, notMonoType, notMonoArgs,
55 --------------------------------
57 zonkType, zonkTcPredType,
58 zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV,
59 zonkQuantifiedTyVar, zonkQuantifiedTyVars,
60 zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
61 zonkTcKindToKind, zonkTcKind, zonkTopTyVar,
63 readKindVar, writeKindVar
66 #include "HsVersions.h"
78 import TcRnMonad -- TcType, amongst others
91 import Control.Monad ( when, unless )
92 import Data.List ( (\\) )
96 %************************************************************************
98 Instantiation in general
100 %************************************************************************
103 tcInstType :: ([TyVar] -> TcM [TcTyVar]) -- How to instantiate the type variables
104 -> TcType -- Type to instantiate
105 -> TcM ([TcTyVar], TcThetaType, TcType) -- Result
106 tcInstType inst_tyvars ty
107 = case tcSplitForAllTys ty of
108 ([], rho) -> let -- There may be overloading despite no type variables;
109 -- (?x :: Int) => Int -> Int
110 (theta, tau) = tcSplitPhiTy rho
112 return ([], theta, tau)
114 (tyvars, rho) -> do { tyvars' <- inst_tyvars tyvars
116 ; let tenv = zipTopTvSubst tyvars (mkTyVarTys tyvars')
117 -- Either the tyvars are freshly made, by inst_tyvars,
118 -- or (in the call from tcSkolSigType) any nested foralls
119 -- have different binders. Either way, zipTopTvSubst is ok
121 ; let (theta, tau) = tcSplitPhiTy (substTy tenv rho)
122 ; return (tyvars', theta, tau) }
126 %************************************************************************
130 %************************************************************************
132 Can't be in TcUnify, as we also need it in TcTyFuns.
136 -- False <=> the two args are (actual, expected) respectively
137 -- True <=> the two args are (expected, actual) respectively
139 checkUpdateMeta :: SwapFlag
140 -> TcTyVar -> IORef MetaDetails -> TcType -> TcM ()
141 -- Update tv1, which is flexi; occurs check is alrady done
142 -- The 'check' version does a kind check too
143 -- We do a sub-kind check here: we might unify (a b) with (c d)
144 -- where b::*->* and d::*; this should fail
146 checkUpdateMeta swapped tv1 ref1 ty2
147 = do { checkKinds swapped tv1 ty2
148 ; updateMeta tv1 ref1 ty2 }
150 updateMeta :: TcTyVar -> IORef MetaDetails -> TcType -> TcM ()
151 updateMeta tv1 ref1 ty2
152 = ASSERT( isMetaTyVar tv1 )
153 ASSERT( isBoxyTyVar tv1 || isTauTy ty2 )
154 do { ASSERTM2( do { details <- readMetaTyVar tv1; return (isFlexi details) }, ppr tv1 )
155 ; traceTc (text "updateMeta" <+> ppr tv1 <+> text ":=" <+> ppr ty2)
156 ; writeMutVar ref1 (Indirect ty2)
160 checkKinds swapped tv1 ty2
161 -- We're about to unify a type variable tv1 with a non-tyvar-type ty2.
162 -- ty2 has been zonked at this stage, which ensures that
163 -- its kind has as much boxity information visible as possible.
164 | tk2 `isSubKind` tk1 = returnM ()
167 -- Either the kinds aren't compatible
168 -- (can happen if we unify (a b) with (c d))
169 -- or we are unifying a lifted type variable with an
170 -- unlifted type: e.g. (id 3#) is illegal
171 = addErrCtxtM (unifyKindCtxt swapped tv1 ty2) $
172 unifyKindMisMatch k1 k2
174 (k1,k2) | swapped = (tk2,tk1)
175 | otherwise = (tk1,tk2)
180 checkTauTvUpdate :: TcTyVar -> TcType -> TcM TcType
181 -- (checkTauTvUpdate tv ty)
182 -- We are about to update the TauTv tv with ty.
183 -- Check (a) that tv doesn't occur in ty (occurs check)
184 -- (b) that ty is a monotype
185 -- Furthermore, in the interest of (b), if you find an
186 -- empty box (BoxTv that is Flexi), fill it in with a TauTv
188 -- Returns the (non-boxy) type to update the type variable with, or fails
190 checkTauTvUpdate orig_tv orig_ty
194 | isSynTyCon tc = go_syn tc tys
195 | otherwise = do { tys' <- mappM go tys; return (TyConApp tc tys') }
196 go (NoteTy _ ty2) = go ty2 -- Discard free-tyvar annotations
197 go (PredTy p) = do { p' <- go_pred p; return (PredTy p') }
198 go (FunTy arg res) = do { arg' <- go arg; res' <- go res; return (FunTy arg' res') }
199 go (AppTy fun arg) = do { fun' <- go fun; arg' <- go arg; return (mkAppTy fun' arg') }
200 -- NB the mkAppTy; we might have instantiated a
201 -- type variable to a type constructor, so we need
202 -- to pull the TyConApp to the top.
203 go (ForAllTy tv ty) = notMonoType orig_ty -- (b)
206 | orig_tv == tv = occurCheck tv -- (a)
207 | isTcTyVar tv = go_tyvar tv (tcTyVarDetails tv)
208 | otherwise = return (TyVarTy tv)
209 -- Ordinary (non Tc) tyvars
210 -- occur inside quantified types
212 go_pred (ClassP c tys) = do { tys' <- mapM go tys; return (ClassP c tys') }
213 go_pred (IParam n ty) = do { ty' <- go ty; return (IParam n ty') }
214 go_pred (EqPred t1 t2) = do { t1' <- go t1; t2' <- go t2; return (EqPred t1' t2') }
216 go_tyvar tv (SkolemTv _) = return (TyVarTy tv)
217 go_tyvar tv (MetaTv box ref)
218 = do { cts <- readMutVar ref
222 BoxTv -> fillBoxWithTau tv ref
223 other -> return (TyVarTy tv)
226 -- go_syn is called for synonyms only
227 -- See Note [Type synonyms and the occur check]
229 | not (isTauTyCon tc)
230 = notMonoType orig_ty -- (b) again
232 = do { (msgs, mb_tys') <- tryTc (mapM go tys)
234 Just tys' -> return (TyConApp tc tys')
235 -- Retain the synonym (the common case)
236 Nothing | isOpenTyCon tc
237 -> notMonoArgs (TyConApp tc tys)
238 -- Synonym families must have monotype args
240 -> go (expectJust "checkTauTvUpdate"
241 (tcView (TyConApp tc tys)))
242 -- Try again, expanding the synonym
245 occurCheck tv = occurCheckErr (mkTyVarTy tv) orig_ty
247 fillBoxWithTau :: BoxyTyVar -> IORef MetaDetails -> TcM TcType
248 -- (fillBoxWithTau tv ref) fills ref with a freshly allocated
249 -- tau-type meta-variable, whose print-name is the same as tv
250 -- Choosing the same name is good: when we instantiate a function
251 -- we allocate boxy tyvars with the same print-name as the quantified
252 -- tyvar; and then we often fill the box with a tau-tyvar, and again
253 -- we want to choose the same name.
254 fillBoxWithTau tv ref
255 = do { tv' <- tcInstTyVar tv -- Do not gratuitously forget
256 ; let tau = mkTyVarTy tv' -- name of the type variable
257 ; writeMutVar ref (Indirect tau)
261 Error mesages in case of kind mismatch.
264 unifyKindMisMatch ty1 ty2
265 = zonkTcKind ty1 `thenM` \ ty1' ->
266 zonkTcKind ty2 `thenM` \ ty2' ->
268 msg = hang (ptext SLIT("Couldn't match kind"))
269 2 (sep [quotes (ppr ty1'),
270 ptext SLIT("against"),
275 unifyKindCtxt swapped tv1 ty2 tidy_env -- not swapped => tv1 expected, ty2 inferred
276 -- tv1 and ty2 are zonked already
279 msg = (env2, ptext SLIT("When matching the kinds of") <+>
280 sep [quotes pp_expected <+> ptext SLIT("and"), quotes pp_actual])
282 (pp_expected, pp_actual) | swapped = (pp2, pp1)
283 | otherwise = (pp1, pp2)
284 (env1, tv1') = tidyOpenTyVar tidy_env tv1
285 (env2, ty2') = tidyOpenType env1 ty2
286 pp1 = ppr tv1' <+> dcolon <+> ppr (tyVarKind tv1)
287 pp2 = ppr ty2' <+> dcolon <+> ppr (typeKind ty2)
290 Error message for failure due to an occurs check.
293 occurCheckErr :: TcType -> TcType -> TcM a
294 occurCheckErr ty containingTy
295 = do { env0 <- tcInitTidyEnv
296 ; ty' <- zonkTcType ty
297 ; containingTy' <- zonkTcType containingTy
298 ; let (env1, tidy_ty1) = tidyOpenType env0 ty'
299 (env2, tidy_ty2) = tidyOpenType env1 containingTy'
300 extra = sep [ppr tidy_ty1, char '=', ppr tidy_ty2]
301 ; failWithTcM (env2, hang msg 2 extra) }
303 msg = ptext SLIT("Occurs check: cannot construct the infinite type:")
306 %************************************************************************
310 %************************************************************************
313 newCoVars :: [(TcType,TcType)] -> TcM [CoVar]
315 = do { us <- newUniqueSupply
316 ; return [ mkCoVar (mkSysTvName uniq FSLIT("co"))
318 | ((ty1,ty2), uniq) <- spec `zip` uniqsFromSupply us] }
320 newMetaCoVar :: TcType -> TcType -> TcM TcTyVar
321 newMetaCoVar ty1 ty2 = newMetaTyVar TauTv (mkCoKind ty1 ty2)
323 newKindVar :: TcM TcKind
324 newKindVar = do { uniq <- newUnique
325 ; ref <- newMutVar Flexi
326 ; return (mkTyVarTy (mkKindVar uniq ref)) }
328 newKindVars :: Int -> TcM [TcKind]
329 newKindVars n = mappM (\ _ -> newKindVar) (nOfThem n ())
333 %************************************************************************
335 SkolemTvs (immutable)
337 %************************************************************************
340 mkSkolTyVar :: Name -> Kind -> SkolemInfo -> TcTyVar
341 mkSkolTyVar name kind info = mkTcTyVar name kind (SkolemTv info)
343 tcSkolSigType :: SkolemInfo -> Type -> TcM ([TcTyVar], TcThetaType, TcType)
344 -- Instantiate a type signature with skolem constants, but
345 -- do *not* give them fresh names, because we want the name to
346 -- be in the type environment -- it is lexically scoped.
347 tcSkolSigType info ty = tcInstType (\tvs -> return (tcSkolSigTyVars info tvs)) ty
349 tcSkolSigTyVars :: SkolemInfo -> [TyVar] -> [TcTyVar]
350 -- Make skolem constants, but do *not* give them new names, as above
351 tcSkolSigTyVars info tyvars = [ mkSkolTyVar (tyVarName tv) (tyVarKind tv) info
354 tcInstSkolTyVar :: SkolemInfo -> Maybe SrcSpan -> TyVar -> TcM TcTyVar
355 -- Instantiate the tyvar, using
356 -- * the occ-name and kind of the supplied tyvar,
357 -- * the unique from the monad,
358 -- * the location either from the tyvar (mb_loc = Nothing)
359 -- or from mb_loc (Just loc)
360 tcInstSkolTyVar info mb_loc tyvar
361 = do { uniq <- newUnique
362 ; let old_name = tyVarName tyvar
363 kind = tyVarKind tyvar
364 loc = mb_loc `orElse` getSrcSpan old_name
365 new_name = mkInternalName uniq (nameOccName old_name) loc
366 ; return (mkSkolTyVar new_name kind info) }
368 tcInstSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
369 -- Get the location from the monad
370 tcInstSkolTyVars info tyvars
371 = do { span <- getSrcSpanM
372 ; mapM (tcInstSkolTyVar info (Just span)) tyvars }
374 tcInstSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
375 -- Instantiate a type with fresh skolem constants
376 -- Binding location comes from the monad
377 tcInstSkolType info ty = tcInstType (tcInstSkolTyVars info) ty
381 %************************************************************************
383 MetaTvs (meta type variables; mutable)
385 %************************************************************************
388 newMetaTyVar :: BoxInfo -> Kind -> TcM TcTyVar
389 -- Make a new meta tyvar out of thin air
390 newMetaTyVar box_info kind
391 = do { uniq <- newUnique
392 ; ref <- newMutVar Flexi
393 ; let name = mkSysTvName uniq fs
394 fs = case box_info of
397 SigTv _ -> FSLIT("a")
398 -- We give BoxTv and TauTv the same string, because
399 -- otherwise we get user-visible differences in error
400 -- messages, which are confusing. If you want to see
401 -- the box_info of each tyvar, use -dppr-debug
402 ; return (mkTcTyVar name kind (MetaTv box_info ref)) }
404 instMetaTyVar :: BoxInfo -> TyVar -> TcM TcTyVar
405 -- Make a new meta tyvar whose Name and Kind
406 -- come from an existing TyVar
407 instMetaTyVar box_info tyvar
408 = do { uniq <- newUnique
409 ; ref <- newMutVar Flexi
410 ; let name = setNameUnique (tyVarName tyvar) uniq
411 kind = tyVarKind tyvar
412 ; return (mkTcTyVar name kind (MetaTv box_info ref)) }
414 readMetaTyVar :: TyVar -> TcM MetaDetails
415 readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
416 readMutVar (metaTvRef tyvar)
418 writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
420 writeMetaTyVar tyvar ty = writeMutVar (metaTvRef tyvar) (Indirect ty)
422 writeMetaTyVar tyvar ty
423 | not (isMetaTyVar tyvar)
424 = pprTrace "writeMetaTyVar" (ppr tyvar) $
428 = ASSERT( isMetaTyVar tyvar )
429 -- TOM: It should also work for coercions
430 -- ASSERT2( k2 `isSubKind` k1, (ppr tyvar <+> ppr k1) $$ (ppr ty <+> ppr k2) )
431 do { ASSERTM2( do { details <- readMetaTyVar tyvar; return (isFlexi details) }, ppr tyvar )
432 ; writeMutVar (metaTvRef tyvar) (Indirect ty) }
440 %************************************************************************
444 %************************************************************************
447 newFlexiTyVar :: Kind -> TcM TcTyVar
448 newFlexiTyVar kind = newMetaTyVar TauTv kind
450 newFlexiTyVarTy :: Kind -> TcM TcType
452 = newFlexiTyVar kind `thenM` \ tc_tyvar ->
453 returnM (TyVarTy tc_tyvar)
455 newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
456 newFlexiTyVarTys n kind = mappM newFlexiTyVarTy (nOfThem n kind)
458 tcInstTyVar :: TyVar -> TcM TcTyVar
459 -- Instantiate with a META type variable
460 tcInstTyVar tyvar = instMetaTyVar TauTv tyvar
462 tcInstTyVars :: [TyVar] -> TcM ([TcTyVar], [TcType], TvSubst)
463 -- Instantiate with META type variables
465 = do { tc_tvs <- mapM tcInstTyVar tyvars
466 ; let tys = mkTyVarTys tc_tvs
467 ; returnM (tc_tvs, tys, zipTopTvSubst tyvars tys) }
468 -- Since the tyvars are freshly made,
469 -- they cannot possibly be captured by
470 -- any existing for-alls. Hence zipTopTvSubst
474 %************************************************************************
478 %************************************************************************
481 tcInstSigTyVars :: Bool -> SkolemInfo -> [TyVar] -> TcM [TcTyVar]
482 -- Instantiate with skolems or meta SigTvs; depending on use_skols
483 -- Always take location info from the supplied tyvars
484 tcInstSigTyVars use_skols skol_info tyvars
486 = mapM (tcInstSkolTyVar skol_info Nothing) tyvars
489 = mapM (instMetaTyVar (SigTv skol_info)) tyvars
491 zonkSigTyVar :: TcTyVar -> TcM TcTyVar
493 | isSkolemTyVar sig_tv
494 = return sig_tv -- Happens in the call in TcBinds.checkDistinctTyVars
496 = ASSERT( isSigTyVar sig_tv )
497 do { ty <- zonkTcTyVar sig_tv
498 ; return (tcGetTyVar "zonkSigTyVar" ty) }
499 -- 'ty' is bound to be a type variable, because SigTvs
500 -- can only be unified with type variables
504 %************************************************************************
508 %************************************************************************
511 newBoxyTyVar :: Kind -> TcM BoxyTyVar
512 newBoxyTyVar kind = newMetaTyVar BoxTv kind
514 newBoxyTyVars :: [Kind] -> TcM [BoxyTyVar]
515 newBoxyTyVars kinds = mapM newBoxyTyVar kinds
517 newBoxyTyVarTys :: [Kind] -> TcM [BoxyType]
518 newBoxyTyVarTys kinds = do { tvs <- mapM newBoxyTyVar kinds; return (mkTyVarTys tvs) }
520 readFilledBox :: BoxyTyVar -> TcM TcType
521 -- Read the contents of the box, which should be filled in by now
522 readFilledBox box_tv = ASSERT( isBoxyTyVar box_tv )
523 do { cts <- readMetaTyVar box_tv
525 Flexi -> pprPanic "readFilledBox" (ppr box_tv)
526 Indirect ty -> return ty }
528 tcInstBoxyTyVar :: TyVar -> TcM BoxyTyVar
529 -- Instantiate with a BOXY type variable
530 tcInstBoxyTyVar tyvar = instMetaTyVar BoxTv tyvar
534 %************************************************************************
536 \subsection{Putting and getting mutable type variables}
538 %************************************************************************
540 But it's more fun to short out indirections on the way: If this
541 version returns a TyVar, then that TyVar is unbound. If it returns
542 any other type, then there might be bound TyVars embedded inside it.
544 We return Nothing iff the original box was unbound.
547 data LookupTyVarResult -- The result of a lookupTcTyVar call
548 = DoneTv TcTyVarDetails -- SkolemTv or virgin MetaTv
551 lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult
553 = ASSERT2( isTcTyVar tyvar, ppr tyvar )
555 SkolemTv _ -> return (DoneTv details)
556 MetaTv _ ref -> do { meta_details <- readMutVar ref
557 ; case meta_details of
558 Indirect ty -> return (IndirectTv ty)
559 Flexi -> return (DoneTv details) }
561 details = tcTyVarDetails tyvar
564 -- gaw 2004 We aren't shorting anything out anymore, at least for now
566 | not (isTcTyVar tyvar)
567 = pprTrace "getTcTyVar" (ppr tyvar) $
568 returnM (Just (mkTyVarTy tyvar))
571 = ASSERT2( isTcTyVar tyvar, ppr tyvar )
572 readMetaTyVar tyvar `thenM` \ maybe_ty ->
574 Just ty -> short_out ty `thenM` \ ty' ->
575 writeMetaTyVar tyvar (Just ty') `thenM_`
578 Nothing -> returnM Nothing
580 short_out :: TcType -> TcM TcType
581 short_out ty@(TyVarTy tyvar)
582 | not (isTcTyVar tyvar)
586 = readMetaTyVar tyvar `thenM` \ maybe_ty ->
588 Just ty' -> short_out ty' `thenM` \ ty' ->
589 writeMetaTyVar tyvar (Just ty') `thenM_`
594 short_out other_ty = returnM other_ty
599 %************************************************************************
601 \subsection{Zonking -- the exernal interfaces}
603 %************************************************************************
605 ----------------- Type variables
608 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
609 zonkTcTyVars tyvars = mappM zonkTcTyVar tyvars
611 zonkTcTyVarsAndFV :: [TcTyVar] -> TcM TcTyVarSet
612 zonkTcTyVarsAndFV tyvars = mappM zonkTcTyVar tyvars `thenM` \ tys ->
613 returnM (tyVarsOfTypes tys)
615 zonkTcTyVar :: TcTyVar -> TcM TcType
616 zonkTcTyVar tyvar = ASSERT2( isTcTyVar tyvar, ppr tyvar)
617 zonk_tc_tyvar (\ tv -> returnM (TyVarTy tv)) tyvar
620 ----------------- Types
623 zonkTcType :: TcType -> TcM TcType
624 zonkTcType ty = zonkType (\ tv -> returnM (TyVarTy tv)) ty
626 zonkTcTypes :: [TcType] -> TcM [TcType]
627 zonkTcTypes tys = mappM zonkTcType tys
629 zonkTcClassConstraints cts = mappM zonk cts
630 where zonk (clas, tys)
631 = zonkTcTypes tys `thenM` \ new_tys ->
632 returnM (clas, new_tys)
634 zonkTcThetaType :: TcThetaType -> TcM TcThetaType
635 zonkTcThetaType theta = mappM zonkTcPredType theta
637 zonkTcPredType :: TcPredType -> TcM TcPredType
638 zonkTcPredType (ClassP c ts)
639 = zonkTcTypes ts `thenM` \ new_ts ->
640 returnM (ClassP c new_ts)
641 zonkTcPredType (IParam n t)
642 = zonkTcType t `thenM` \ new_t ->
643 returnM (IParam n new_t)
644 zonkTcPredType (EqPred t1 t2)
645 = zonkTcType t1 `thenM` \ new_t1 ->
646 zonkTcType t2 `thenM` \ new_t2 ->
647 returnM (EqPred new_t1 new_t2)
650 ------------------- These ...ToType, ...ToKind versions
651 are used at the end of type checking
654 zonkTopTyVar :: TcTyVar -> TcM TcTyVar
655 -- zonkTopTyVar is used, at the top level, on any un-instantiated meta type variables
656 -- to default the kind of ? and ?? etc to *. This is important to ensure that
657 -- instance declarations match. For example consider
658 -- instance Show (a->b)
659 -- foo x = show (\_ -> True)
660 -- Then we'll get a constraint (Show (p ->q)) where p has argTypeKind (printed ??),
661 -- and that won't match the typeKind (*) in the instance decl.
663 -- Because we are at top level, no further constraints are going to affect these
664 -- type variables, so it's time to do it by hand. However we aren't ready
665 -- to default them fully to () or whatever, because the type-class defaulting
666 -- rules have yet to run.
669 | k `eqKind` default_k = return tv
671 = do { tv' <- newFlexiTyVar default_k
672 ; writeMetaTyVar tv (mkTyVarTy tv')
676 default_k = defaultKind k
678 zonkQuantifiedTyVars :: [TcTyVar] -> TcM [TyVar]
679 zonkQuantifiedTyVars = mappM zonkQuantifiedTyVar
681 zonkQuantifiedTyVar :: TcTyVar -> TcM TyVar
682 -- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it.
684 -- The quantified type variables often include meta type variables
685 -- we want to freeze them into ordinary type variables, and
686 -- default their kind (e.g. from OpenTypeKind to TypeKind)
687 -- -- see notes with Kind.defaultKind
688 -- The meta tyvar is updated to point to the new regular TyVar. Now any
689 -- bound occurences of the original type variable will get zonked to
690 -- the immutable version.
692 -- We leave skolem TyVars alone; they are immutable.
693 zonkQuantifiedTyVar tv
694 | ASSERT( isTcTyVar tv )
695 isSkolemTyVar tv = return tv
696 -- It might be a skolem type variable,
697 -- for example from a user type signature
699 | otherwise -- It's a meta-type-variable
700 = do { details <- readMetaTyVar tv
702 -- Create the new, frozen, regular type variable
703 ; let final_kind = defaultKind (tyVarKind tv)
704 final_tv = mkTyVar (tyVarName tv) final_kind
706 -- Bind the meta tyvar to the new tyvar
708 Indirect ty -> WARN( True, ppr tv $$ ppr ty )
710 -- [Sept 04] I don't think this should happen
711 -- See note [Silly Type Synonym]
713 Flexi -> writeMetaTyVar tv (mkTyVarTy final_tv)
715 -- Return the new tyvar
719 [Silly Type Synonyms]
722 type C u a = u -- Note 'a' unused
724 foo :: (forall a. C u a -> C u a) -> u
728 bar = foo (\t -> t + t)
730 * From the (\t -> t+t) we get type {Num d} => d -> d
733 * Now unify with type of foo's arg, and we get:
734 {Num (C d a)} => C d a -> C d a
737 * Now abstract over the 'a', but float out the Num (C d a) constraint
738 because it does not 'really' mention a. (see exactTyVarsOfType)
739 The arg to foo becomes
742 * So we get a dict binding for Num (C d a), which is zonked to give
744 [Note Sept 04: now that we are zonking quantified type variables
745 on construction, the 'a' will be frozen as a regular tyvar on
746 quantification, so the floated dict will still have type (C d a).
747 Which renders this whole note moot; happily!]
749 * Then the /\a abstraction has a zonked 'a' in it.
751 All very silly. I think its harmless to ignore the problem. We'll end up with
752 a /\a in the final result but all the occurrences of a will be zonked to ()
755 %************************************************************************
757 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
759 %* For internal use only! *
761 %************************************************************************
764 -- For unbound, mutable tyvars, zonkType uses the function given to it
765 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
766 -- type variable and zonks the kind too
768 zonkType :: (TcTyVar -> TcM Type) -- What to do with unbound mutable type variables
769 -- see zonkTcType, and zonkTcTypeToType
772 zonkType unbound_var_fn ty
775 go (NoteTy _ ty2) = go ty2 -- Discard free-tyvar annotations
777 go (TyConApp tc tys) = mappM go tys `thenM` \ tys' ->
778 returnM (TyConApp tc tys')
780 go (PredTy p) = go_pred p `thenM` \ p' ->
783 go (FunTy arg res) = go arg `thenM` \ arg' ->
784 go res `thenM` \ res' ->
785 returnM (FunTy arg' res')
787 go (AppTy fun arg) = go fun `thenM` \ fun' ->
788 go arg `thenM` \ arg' ->
789 returnM (mkAppTy fun' arg')
790 -- NB the mkAppTy; we might have instantiated a
791 -- type variable to a type constructor, so we need
792 -- to pull the TyConApp to the top.
794 -- The two interesting cases!
795 go (TyVarTy tyvar) | isTcTyVar tyvar = zonk_tc_tyvar unbound_var_fn tyvar
796 | otherwise = return (TyVarTy tyvar)
797 -- Ordinary (non Tc) tyvars occur inside quantified types
799 go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar )
800 go ty `thenM` \ ty' ->
801 returnM (ForAllTy tyvar ty')
803 go_pred (ClassP c tys) = mappM go tys `thenM` \ tys' ->
804 returnM (ClassP c tys')
805 go_pred (IParam n ty) = go ty `thenM` \ ty' ->
806 returnM (IParam n ty')
807 go_pred (EqPred ty1 ty2) = go ty1 `thenM` \ ty1' ->
808 go ty2 `thenM` \ ty2' ->
809 returnM (EqPred ty1' ty2')
811 zonk_tc_tyvar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable variable
812 -> TcTyVar -> TcM TcType
813 zonk_tc_tyvar unbound_var_fn tyvar
814 | not (isMetaTyVar tyvar) -- Skolems
815 = returnM (TyVarTy tyvar)
817 | otherwise -- Mutables
818 = do { cts <- readMetaTyVar tyvar
820 Flexi -> unbound_var_fn tyvar -- Unbound meta type variable
821 Indirect ty -> zonkType unbound_var_fn ty }
826 %************************************************************************
830 %************************************************************************
833 readKindVar :: KindVar -> TcM (MetaDetails)
834 writeKindVar :: KindVar -> TcKind -> TcM ()
835 readKindVar kv = readMutVar (kindVarRef kv)
836 writeKindVar kv val = writeMutVar (kindVarRef kv) (Indirect val)
839 zonkTcKind :: TcKind -> TcM TcKind
840 zonkTcKind k = zonkTcType k
843 zonkTcKindToKind :: TcKind -> TcM Kind
844 -- When zonking a TcKind to a kind, we need to instantiate kind variables,
845 -- Haskell specifies that * is to be used, so we follow that.
846 zonkTcKindToKind k = zonkType (\ _ -> return liftedTypeKind) k
849 %************************************************************************
851 \subsection{Checking a user type}
853 %************************************************************************
855 When dealing with a user-written type, we first translate it from an HsType
856 to a Type, performing kind checking, and then check various things that should
857 be true about it. We don't want to perform these checks at the same time
858 as the initial translation because (a) they are unnecessary for interface-file
859 types and (b) when checking a mutually recursive group of type and class decls,
860 we can't "look" at the tycons/classes yet. Also, the checks are are rather
861 diverse, and used to really mess up the other code.
863 One thing we check for is 'rank'.
865 Rank 0: monotypes (no foralls)
866 Rank 1: foralls at the front only, Rank 0 inside
867 Rank 2: foralls at the front, Rank 1 on left of fn arrow,
869 basic ::= tyvar | T basic ... basic
871 r2 ::= forall tvs. cxt => r2a
872 r2a ::= r1 -> r2a | basic
873 r1 ::= forall tvs. cxt => r0
874 r0 ::= r0 -> r0 | basic
876 Another thing is to check that type synonyms are saturated.
877 This might not necessarily show up in kind checking.
879 data T k = MkT (k Int)
884 checkValidType :: UserTypeCtxt -> Type -> TcM ()
885 -- Checks that the type is valid for the given context
886 checkValidType ctxt ty
887 = traceTc (text "checkValidType" <+> ppr ty) `thenM_`
888 doptM Opt_UnboxedTuples `thenM` \ unboxed ->
889 doptM Opt_Rank2Types `thenM` \ rank2 ->
890 doptM Opt_RankNTypes `thenM` \ rankn ->
891 doptM Opt_PolymorphicComponents `thenM` \ polycomp ->
893 rank | rankn = Arbitrary
896 = case ctxt of -- Haskell 98
898 LamPatSigCtxt -> Rank 0
899 BindPatSigCtxt -> Rank 0
900 DefaultDeclCtxt-> Rank 0
902 TySynCtxt _ -> Rank 0
903 ExprSigCtxt -> Rank 1
904 FunSigCtxt _ -> Rank 1
905 ConArgCtxt _ -> if polycomp
907 -- We are given the type of the entire
908 -- constructor, hence rank 1
910 ForSigCtxt _ -> Rank 1
911 SpecInstCtxt -> Rank 1
913 actual_kind = typeKind ty
915 kind_ok = case ctxt of
916 TySynCtxt _ -> True -- Any kind will do
917 ResSigCtxt -> isSubOpenTypeKind actual_kind
918 ExprSigCtxt -> isSubOpenTypeKind actual_kind
919 GenPatCtxt -> isLiftedTypeKind actual_kind
920 ForSigCtxt _ -> isLiftedTypeKind actual_kind
921 other -> isSubArgTypeKind actual_kind
923 ubx_tup = case ctxt of
924 TySynCtxt _ | unboxed -> UT_Ok
925 ExprSigCtxt | unboxed -> UT_Ok
928 -- Check that the thing has kind Type, and is lifted if necessary
929 checkTc kind_ok (kindErr actual_kind) `thenM_`
931 -- Check the internal validity of the type itself
932 check_poly_type rank ubx_tup ty `thenM_`
934 traceTc (text "checkValidType done" <+> ppr ty)
939 data Rank = Rank Int | Arbitrary
941 decRank :: Rank -> Rank
942 decRank Arbitrary = Arbitrary
943 decRank (Rank n) = Rank (n-1)
945 ----------------------------------------
946 data UbxTupFlag = UT_Ok | UT_NotOk
947 -- The "Ok" version means "ok if -fglasgow-exts is on"
949 ----------------------------------------
950 check_poly_type :: Rank -> UbxTupFlag -> Type -> TcM ()
951 check_poly_type (Rank 0) ubx_tup ty
952 = check_tau_type (Rank 0) ubx_tup ty
954 check_poly_type rank ubx_tup ty
955 | null tvs && null theta
956 = check_tau_type rank ubx_tup ty
958 = do { check_valid_theta SigmaCtxt theta
959 ; check_poly_type rank ubx_tup tau -- Allow foralls to right of arrow
960 ; checkFreeness tvs theta
961 ; checkAmbiguity tvs theta (tyVarsOfType tau) }
963 (tvs, theta, tau) = tcSplitSigmaTy ty
965 ----------------------------------------
966 check_arg_type :: Type -> TcM ()
967 -- The sort of type that can instantiate a type variable,
968 -- or be the argument of a type constructor.
969 -- Not an unboxed tuple, but now *can* be a forall (since impredicativity)
970 -- Other unboxed types are very occasionally allowed as type
971 -- arguments depending on the kind of the type constructor
973 -- For example, we want to reject things like:
975 -- instance Ord a => Ord (forall s. T s a)
977 -- g :: T s (forall b.b)
979 -- NB: unboxed tuples can have polymorphic or unboxed args.
980 -- This happens in the workers for functions returning
981 -- product types with polymorphic components.
982 -- But not in user code.
983 -- Anyway, they are dealt with by a special case in check_tau_type
986 = check_poly_type Arbitrary UT_NotOk ty `thenM_`
987 checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
989 ----------------------------------------
990 check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
991 -- Rank is allowed rank for function args
992 -- No foralls otherwise
994 check_tau_type rank ubx_tup ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
995 check_tau_type rank ubx_tup ty@(FunTy (PredTy _) _) = failWithTc (forAllTyErr ty)
996 -- Reject e.g. (Maybe (?x::Int => Int)), with a decent error message
998 -- Naked PredTys don't usually show up, but they can as a result of
999 -- {-# SPECIALISE instance Ord Char #-}
1000 -- The Right Thing would be to fix the way that SPECIALISE instance pragmas
1001 -- are handled, but the quick thing is just to permit PredTys here.
1002 check_tau_type rank ubx_tup (PredTy sty) = getDOpts `thenM` \ dflags ->
1003 check_pred_ty dflags TypeCtxt sty
1005 check_tau_type rank ubx_tup (TyVarTy _) = returnM ()
1006 check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
1007 = check_poly_type (decRank rank) UT_NotOk arg_ty `thenM_`
1008 check_poly_type rank UT_Ok res_ty
1010 check_tau_type rank ubx_tup (AppTy ty1 ty2)
1011 = check_arg_type ty1 `thenM_` check_arg_type ty2
1013 check_tau_type rank ubx_tup (NoteTy other_note ty)
1014 = check_tau_type rank ubx_tup ty
1016 check_tau_type rank ubx_tup ty@(TyConApp tc tys)
1018 = do { -- It's OK to have an *over-applied* type synonym
1019 -- data Tree a b = ...
1020 -- type Foo a = Tree [a]
1021 -- f :: Foo a b -> ...
1023 Just ty' -> check_tau_type rank ubx_tup ty' -- Check expansion
1024 Nothing -> unless (isOpenTyCon tc -- No expansion if open
1025 && tyConArity tc <= length tys) $
1026 failWithTc arity_msg
1028 ; ok <- doptM Opt_PartiallyAppliedClosedTypeSynonyms
1029 ; if ok && not (isOpenTyCon tc) then
1030 -- Don't check the type arguments of *closed* synonyms.
1031 -- This allows us to instantiate a synonym defn with a
1032 -- for-all type, or with a partially-applied type synonym.
1033 -- e.g. type T a b = a
1036 -- Here, T is partially applied, so it's illegal in H98.
1037 -- But if you expand S first, then T we get just
1042 -- For H98, do check the type args
1043 mappM_ check_arg_type tys
1046 | isUnboxedTupleTyCon tc
1047 = doptM Opt_UnboxedTuples `thenM` \ ub_tuples_allowed ->
1048 checkTc (ubx_tup_ok ub_tuples_allowed) ubx_tup_msg `thenM_`
1049 mappM_ (check_tau_type (Rank 0) UT_Ok) tys
1050 -- Args are allowed to be unlifted, or
1051 -- more unboxed tuples, so can't use check_arg_ty
1054 = mappM_ check_arg_type tys
1057 ubx_tup_ok ub_tuples_allowed = case ubx_tup of { UT_Ok -> ub_tuples_allowed; other -> False }
1060 tc_arity = tyConArity tc
1062 arity_msg = arityErr "Type synonym" (tyConName tc) tc_arity n_args
1063 ubx_tup_msg = ubxArgTyErr ty
1065 ----------------------------------------
1066 forAllTyErr ty = ptext SLIT("Illegal polymorphic or qualified type:") <+> ppr ty
1067 unliftedArgErr ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr ty
1068 ubxArgTyErr ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr ty
1069 kindErr kind = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
1073 %************************************************************************
1075 \subsection{Checking a theta or source type}
1077 %************************************************************************
1080 -- Enumerate the contexts in which a "source type", <S>, can occur
1084 -- or (N a) where N is a newtype
1087 = ClassSCCtxt Name -- Superclasses of clas
1088 -- class <S> => C a where ...
1089 | SigmaCtxt -- Theta part of a normal for-all type
1090 -- f :: <S> => a -> a
1091 | DataTyCtxt Name -- Theta part of a data decl
1092 -- data <S> => T a = MkT a
1093 | TypeCtxt -- Source type in an ordinary type
1095 | InstThetaCtxt -- Context of an instance decl
1096 -- instance <S> => C [a] where ...
1098 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
1099 pprSourceTyCtxt SigmaCtxt = ptext SLIT("the context of a polymorphic type")
1100 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
1101 pprSourceTyCtxt InstThetaCtxt = ptext SLIT("the context of an instance declaration")
1102 pprSourceTyCtxt TypeCtxt = ptext SLIT("the context of a type")
1106 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
1107 checkValidTheta ctxt theta
1108 = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
1110 -------------------------
1111 check_valid_theta ctxt []
1113 check_valid_theta ctxt theta
1114 = getDOpts `thenM` \ dflags ->
1115 warnTc (notNull dups) (dupPredWarn dups) `thenM_`
1116 mappM_ (check_pred_ty dflags ctxt) theta
1118 (_,dups) = removeDups tcCmpPred theta
1120 -------------------------
1121 check_pred_ty :: DynFlags -> SourceTyCtxt -> PredType -> TcM ()
1122 check_pred_ty dflags ctxt pred@(ClassP cls tys)
1123 = do { -- Class predicates are valid in all contexts
1124 ; checkTc (arity == n_tys) arity_err
1126 -- Check the form of the argument types
1127 ; mappM_ check_arg_type tys
1128 ; checkTc (check_class_pred_tys dflags ctxt tys)
1129 (predTyVarErr pred $$ how_to_allow)
1132 class_name = className cls
1133 arity = classArity cls
1135 arity_err = arityErr "Class" class_name arity n_tys
1136 how_to_allow = parens (ptext SLIT("Use -XFlexibleContexts to permit this"))
1138 check_pred_ty dflags ctxt pred@(EqPred ty1 ty2)
1139 = do { -- Equational constraints are valid in all contexts if type
1140 -- families are permitted
1141 ; checkTc (dopt Opt_TypeFamilies dflags) (eqPredTyErr pred)
1143 -- Check the form of the argument types
1144 ; check_eq_arg_type ty1
1145 ; check_eq_arg_type ty2
1148 check_eq_arg_type = check_poly_type (Rank 0) UT_NotOk
1150 check_pred_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
1151 -- Implicit parameters only allowed in type
1152 -- signatures; not in instance decls, superclasses etc
1153 -- The reason for not allowing implicit params in instances is a bit
1155 -- If we allowed instance (?x::Int, Eq a) => Foo [a] where ...
1156 -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
1157 -- discharge all the potential usas of the ?x in e. For example, a
1158 -- constraint Foo [Int] might come out of e,and applying the
1159 -- instance decl would show up two uses of ?x.
1162 check_pred_ty dflags ctxt sty = failWithTc (badPredTyErr sty)
1164 -------------------------
1165 check_class_pred_tys :: DynFlags -> SourceTyCtxt -> [Type] -> Bool
1166 check_class_pred_tys dflags ctxt tys
1168 TypeCtxt -> True -- {-# SPECIALISE instance Eq (T Int) #-} is fine
1169 InstThetaCtxt -> flexible_contexts || undecidable_ok || all tcIsTyVarTy tys
1170 -- Further checks on head and theta in
1171 -- checkInstTermination
1172 other -> flexible_contexts || all tyvar_head tys
1174 flexible_contexts = dopt Opt_FlexibleContexts dflags
1175 undecidable_ok = dopt Opt_UndecidableInstances dflags
1177 -------------------------
1178 tyvar_head ty -- Haskell 98 allows predicates of form
1179 | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
1180 | otherwise -- where a is a type variable
1181 = case tcSplitAppTy_maybe ty of
1182 Just (ty, _) -> tyvar_head ty
1189 is ambiguous if P contains generic variables
1190 (i.e. one of the Vs) that are not mentioned in tau
1192 However, we need to take account of functional dependencies
1193 when we speak of 'mentioned in tau'. Example:
1194 class C a b | a -> b where ...
1196 forall x y. (C x y) => x
1197 is not ambiguous because x is mentioned and x determines y
1199 NB; the ambiguity check is only used for *user* types, not for types
1200 coming from inteface files. The latter can legitimately have
1201 ambiguous types. Example
1203 class S a where s :: a -> (Int,Int)
1204 instance S Char where s _ = (1,1)
1205 f:: S a => [a] -> Int -> (Int,Int)
1206 f (_::[a]) x = (a*x,b)
1207 where (a,b) = s (undefined::a)
1209 Here the worker for f gets the type
1210 fw :: forall a. S a => Int -> (# Int, Int #)
1212 If the list of tv_names is empty, we have a monotype, and then we
1213 don't need to check for ambiguity either, because the test can't fail
1218 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
1219 checkAmbiguity forall_tyvars theta tau_tyvars
1220 = mappM_ complain (filter is_ambig theta)
1222 complain pred = addErrTc (ambigErr pred)
1223 extended_tau_vars = grow theta tau_tyvars
1225 -- See Note [Implicit parameters and ambiguity] in TcSimplify
1226 is_ambig pred = isClassPred pred &&
1227 any ambig_var (varSetElems (tyVarsOfPred pred))
1229 ambig_var ct_var = (ct_var `elem` forall_tyvars) &&
1230 not (ct_var `elemVarSet` extended_tau_vars)
1233 = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
1234 nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
1235 ptext SLIT("must be reachable from the type after the '=>'"))]
1238 In addition, GHC insists that at least one type variable
1239 in each constraint is in V. So we disallow a type like
1240 forall a. Eq b => b -> b
1241 even in a scope where b is in scope.
1244 checkFreeness forall_tyvars theta
1245 = do { flexible_contexts <- doptM Opt_FlexibleContexts
1246 ; unless flexible_contexts $ mappM_ complain (filter is_free theta) }
1248 is_free pred = not (isIPPred pred)
1249 && not (any bound_var (varSetElems (tyVarsOfPred pred)))
1250 bound_var ct_var = ct_var `elem` forall_tyvars
1251 complain pred = addErrTc (freeErr pred)
1254 = sep [ ptext SLIT("All of the type variables in the constraint") <+>
1255 quotes (pprPred pred)
1256 , ptext SLIT("are already in scope") <+>
1257 ptext SLIT("(at least one must be universally quantified here)")
1259 ptext SLIT("(Use -XFlexibleContexts to lift this restriction)")
1264 checkThetaCtxt ctxt theta
1265 = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
1266 ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
1268 badPredTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
1269 eqPredTyErr sty = ptext SLIT("Illegal equational constraint") <+> pprPred sty
1271 parens (ptext SLIT("Use -XTypeFamilies to permit this"))
1272 predTyVarErr pred = sep [ptext SLIT("Non type-variable argument"),
1273 nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
1274 dupPredWarn dups = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
1276 arityErr kind name n m
1277 = hsep [ text kind, quotes (ppr name), ptext SLIT("should have"),
1278 n_arguments <> comma, text "but has been given", int m]
1280 n_arguments | n == 0 = ptext SLIT("no arguments")
1281 | n == 1 = ptext SLIT("1 argument")
1282 | True = hsep [int n, ptext SLIT("arguments")]
1286 = do { ty' <- zonkTcType ty
1287 ; env0 <- tcInitTidyEnv
1288 ; let (env1, tidy_ty) = tidyOpenType env0 ty'
1289 msg = ptext SLIT("Cannot match a monotype with") <+> quotes (ppr tidy_ty)
1290 ; failWithTcM (env1, msg) }
1293 = do { ty' <- zonkTcType ty
1294 ; env0 <- tcInitTidyEnv
1295 ; let (env1, tidy_ty) = tidyOpenType env0 ty'
1296 msg = ptext SLIT("Arguments of type synonym families must be monotypes") <+> quotes (ppr tidy_ty)
1297 ; failWithTcM (env1, msg) }
1301 %************************************************************************
1303 \subsection{Checking for a decent instance head type}
1305 %************************************************************************
1307 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1308 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1310 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1311 flag is on, or (2)~the instance is imported (they must have been
1312 compiled elsewhere). In these cases, we let them go through anyway.
1314 We can also have instances for functions: @instance Foo (a -> b) ...@.
1317 checkValidInstHead :: Type -> TcM (Class, [TcType])
1319 checkValidInstHead ty -- Should be a source type
1320 = case tcSplitPredTy_maybe ty of {
1321 Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
1324 case getClassPredTys_maybe pred of {
1325 Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
1328 getDOpts `thenM` \ dflags ->
1329 mappM_ check_arg_type tys `thenM_`
1330 check_inst_head dflags clas tys `thenM_`
1334 check_inst_head dflags clas tys
1335 -- If GlasgowExts then check at least one isn't a type variable
1336 = do checkTc (dopt Opt_TypeSynonymInstances dflags ||
1337 all tcInstHeadTyNotSynonym tys)
1338 (instTypeErr (pprClassPred clas tys) head_type_synonym_msg)
1339 checkTc (dopt Opt_FlexibleInstances dflags ||
1340 all tcInstHeadTyAppAllTyVars tys)
1341 (instTypeErr (pprClassPred clas tys) head_type_args_tyvars_msg)
1342 checkTc (dopt Opt_MultiParamTypeClasses dflags ||
1344 (instTypeErr (pprClassPred clas tys) head_one_type_msg)
1347 head_type_synonym_msg = parens (
1348 text "All instance types must be of the form (T t1 ... tn)" $$
1349 text "where T is not a synonym." $$
1350 text "Use -XTypeSynonymInstances if you want to disable this.")
1352 head_type_args_tyvars_msg = parens (
1353 text "All instance types must be of the form (T a1 ... an)" $$
1354 text "where a1 ... an are distinct type *variables*" $$
1355 text "Use -XFlexibleInstances if you want to disable this.")
1357 head_one_type_msg = parens (
1358 text "Only one type can be given in an instance head." $$
1359 text "Use -XMultiParamTypeClasses if you want to allow more.")
1361 -- For now, I only allow tau-types (not polytypes) in
1362 -- the head of an instance decl.
1363 -- E.g. instance C (forall a. a->a) is rejected
1364 -- One could imagine generalising that, but I'm not sure
1365 -- what all the consequences might be
1366 check_one ty = do { check_tau_type (Rank 0) UT_NotOk ty
1367 ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
1369 instTypeErr pp_ty msg
1370 = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,
1375 %************************************************************************
1377 \subsection{Checking instance for termination}
1379 %************************************************************************
1383 checkValidInstance :: [TyVar] -> ThetaType -> Class -> [TcType] -> TcM ()
1384 checkValidInstance tyvars theta clas inst_tys
1385 = do { undecidable_ok <- doptM Opt_UndecidableInstances
1387 ; checkValidTheta InstThetaCtxt theta
1388 ; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys)
1390 -- Check that instance inference will terminate (if we care)
1391 -- For Haskell 98 this will already have been done by checkValidTheta,
1392 -- but as we may be using other extensions we need to check.
1393 ; unless undecidable_ok $
1394 mapM_ addErrTc (checkInstTermination inst_tys theta)
1396 -- The Coverage Condition
1397 ; checkTc (undecidable_ok || checkInstCoverage clas inst_tys)
1398 (instTypeErr (pprClassPred clas inst_tys) msg)
1401 msg = parens (vcat [ptext SLIT("the Coverage Condition fails for one of the functional dependencies;"),
1405 Termination test: the so-called "Paterson conditions" (see Section 5 of
1406 "Understanding functionsl dependencies via Constraint Handling Rules,
1409 We check that each assertion in the context satisfies:
1410 (1) no variable has more occurrences in the assertion than in the head, and
1411 (2) the assertion has fewer constructors and variables (taken together
1412 and counting repetitions) than the head.
1413 This is only needed with -fglasgow-exts, as Haskell 98 restrictions
1414 (which have already been checked) guarantee termination.
1416 The underlying idea is that
1418 for any ground substitution, each assertion in the
1419 context has fewer type constructors than the head.
1423 checkInstTermination :: [TcType] -> ThetaType -> [Message]
1424 checkInstTermination tys theta
1425 = mapCatMaybes check theta
1428 size = sizeTypes tys
1430 | not (null (fvPred pred \\ fvs))
1431 = Just (predUndecErr pred nomoreMsg $$ parens undecidableMsg)
1432 | sizePred pred >= size
1433 = Just (predUndecErr pred smallerMsg $$ parens undecidableMsg)
1437 predUndecErr pred msg = sep [msg,
1438 nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
1440 nomoreMsg = ptext SLIT("Variable occurs more often in a constraint than in the instance head")
1441 smallerMsg = ptext SLIT("Constraint is no smaller than the instance head")
1442 undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
1446 %************************************************************************
1448 Checking the context of a derived instance declaration
1450 %************************************************************************
1452 Note [Exotic derived instance contexts]
1453 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1454 In a 'derived' instance declaration, we *infer* the context. It's a
1455 bit unclear what rules we should apply for this; the Haskell report is
1456 silent. Obviously, constraints like (Eq a) are fine, but what about
1457 data T f a = MkT (f a) deriving( Eq )
1458 where we'd get an Eq (f a) constraint. That's probably fine too.
1460 One could go further: consider
1461 data T a b c = MkT (Foo a b c) deriving( Eq )
1462 instance (C Int a, Eq b, Eq c) => Eq (Foo a b c)
1464 Notice that this instance (just) satisfies the Paterson termination
1465 conditions. Then we *could* derive an instance decl like this:
1467 instance (C Int a, Eq b, Eq c) => Eq (T a b c)
1469 even though there is no instance for (C Int a), because there just
1470 *might* be an instance for, say, (C Int Bool) at a site where we
1471 need the equality instance for T's.
1473 However, this seems pretty exotic, and it's quite tricky to allow
1474 this, and yet give sensible error messages in the (much more common)
1475 case where we really want that instance decl for C.
1477 So for now we simply require that the derived instance context
1478 should have only type-variable constraints.
1480 Here is another example:
1481 data Fix f = In (f (Fix f)) deriving( Eq )
1482 Here, if we are prepared to allow -fallow-undecidable-instances we
1483 could derive the instance
1484 instance Eq (f (Fix f)) => Eq (Fix f)
1485 but this is so delicate that I don't think it should happen inside
1486 'deriving'. If you want this, write it yourself!
1488 NB: if you want to lift this condition, make sure you still meet the
1489 termination conditions! If not, the deriving mechanism generates
1490 larger and larger constraints. Example:
1492 data Seq a = Cons a (Seq (Succ a)) | Nil deriving Show
1494 Note the lack of a Show instance for Succ. First we'll generate
1495 instance (Show (Succ a), Show a) => Show (Seq a)
1497 instance (Show (Succ (Succ a)), Show (Succ a), Show a) => Show (Seq a)
1498 and so on. Instead we want to complain of no instance for (Show (Succ a)).
1502 Allow constraints which consist only of type variables, with no repeats.
1505 validDerivPred :: PredType -> Bool
1506 validDerivPred (ClassP cls tys) = hasNoDups fvs && sizeTypes tys == length fvs
1507 where fvs = fvTypes tys
1508 validDerivPred otehr = False
1511 %************************************************************************
1513 Checking type instance well-formedness and termination
1515 %************************************************************************
1518 -- Check that a "type instance" is well-formed (which includes decidability
1519 -- unless -fallow-undecidable-instances is given).
1521 checkValidTypeInst :: [Type] -> Type -> TcM ()
1522 checkValidTypeInst typats rhs
1523 = do { -- left-hand side contains no type family applications
1524 -- (vanilla synonyms are fine, though)
1525 ; mappM_ checkTyFamFreeness typats
1527 -- the right-hand side is a tau type
1528 ; checkTc (isTauTy rhs) $
1531 -- we have a decidable instance unless otherwise permitted
1532 ; undecidable_ok <- doptM Opt_UndecidableInstances
1533 ; unless undecidable_ok $
1534 mapM_ addErrTc (checkFamInst typats (tyFamInsts rhs))
1537 -- Make sure that each type family instance is
1538 -- (1) strictly smaller than the lhs,
1539 -- (2) mentions no type variable more often than the lhs, and
1540 -- (3) does not contain any further type family instances.
1542 checkFamInst :: [Type] -- lhs
1543 -> [(TyCon, [Type])] -- type family instances
1545 checkFamInst lhsTys famInsts
1546 = mapCatMaybes check famInsts
1548 size = sizeTypes lhsTys
1549 fvs = fvTypes lhsTys
1551 | not (all isTyFamFree tys)
1552 = Just (famInstUndecErr famInst nestedMsg $$ parens undecidableMsg)
1553 | not (null (fvTypes tys \\ fvs))
1554 = Just (famInstUndecErr famInst nomoreVarMsg $$ parens undecidableMsg)
1555 | size <= sizeTypes tys
1556 = Just (famInstUndecErr famInst smallerAppMsg $$ parens undecidableMsg)
1560 famInst = TyConApp tc tys
1562 -- Ensure that no type family instances occur in a type.
1564 checkTyFamFreeness :: Type -> TcM ()
1565 checkTyFamFreeness ty
1566 = checkTc (isTyFamFree ty) $
1567 tyFamInstInIndexErr ty
1569 -- Check that a type does not contain any type family applications.
1571 isTyFamFree :: Type -> Bool
1572 isTyFamFree = null . tyFamInsts
1576 tyFamInstInIndexErr ty
1577 = hang (ptext SLIT("Illegal type family application in type instance") <>
1582 = hang (ptext SLIT("Illegal polymorphic type in type instance") <> colon) 4 $
1585 famInstUndecErr ty msg
1587 nest 2 (ptext SLIT("in the type family application:") <+>
1590 nestedMsg = ptext SLIT("Nested type family application")
1591 nomoreVarMsg = ptext SLIT("Variable occurs more often than in instance head")
1592 smallerAppMsg = ptext SLIT("Application is no smaller than the instance head")
1596 %************************************************************************
1598 \subsection{Auxiliary functions}
1600 %************************************************************************
1603 -- Free variables of a type, retaining repetitions, and expanding synonyms
1604 fvType :: Type -> [TyVar]
1605 fvType ty | Just exp_ty <- tcView ty = fvType exp_ty
1606 fvType (TyVarTy tv) = [tv]
1607 fvType (TyConApp _ tys) = fvTypes tys
1608 fvType (NoteTy _ ty) = fvType ty
1609 fvType (PredTy pred) = fvPred pred
1610 fvType (FunTy arg res) = fvType arg ++ fvType res
1611 fvType (AppTy fun arg) = fvType fun ++ fvType arg
1612 fvType (ForAllTy tyvar ty) = filter (/= tyvar) (fvType ty)
1614 fvTypes :: [Type] -> [TyVar]
1615 fvTypes tys = concat (map fvType tys)
1617 fvPred :: PredType -> [TyVar]
1618 fvPred (ClassP _ tys') = fvTypes tys'
1619 fvPred (IParam _ ty) = fvType ty
1620 fvPred (EqPred ty1 ty2) = fvType ty1 ++ fvType ty2
1622 -- Size of a type: the number of variables and constructors
1623 sizeType :: Type -> Int
1624 sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty
1625 sizeType (TyVarTy _) = 1
1626 sizeType (TyConApp _ tys) = sizeTypes tys + 1
1627 sizeType (NoteTy _ ty) = sizeType ty
1628 sizeType (PredTy pred) = sizePred pred
1629 sizeType (FunTy arg res) = sizeType arg + sizeType res + 1
1630 sizeType (AppTy fun arg) = sizeType fun + sizeType arg
1631 sizeType (ForAllTy _ ty) = sizeType ty
1633 sizeTypes :: [Type] -> Int
1634 sizeTypes xs = sum (map sizeType xs)
1636 sizePred :: PredType -> Int
1637 sizePred (ClassP _ tys') = sizeTypes tys'
1638 sizePred (IParam _ ty) = sizeType ty
1639 sizePred (EqPred ty1 ty2) = sizeType ty1 + sizeType ty2