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 TcTyVar, TcKind, TcType, TcTauType, TcThetaType, TcTyVarSet,
15 --------------------------------
16 -- Creating new mutable type variables
18 newFlexiTyVarTy, -- Kind -> TcM TcType
19 newFlexiTyVarTys, -- Int -> Kind -> TcM [TcType]
20 newKindVar, newKindVars,
22 newMetaTyVar, readMetaTyVar, writeMetaTyVar, writeMetaTyVarRef,
23 isFilledMetaTyVar, isFlexiMetaTyVar,
25 --------------------------------
26 -- Creating new evidence variables
27 newEvVar, newCoVar, newEvVars,
28 newWantedCoVar, writeWantedCoVar, readWantedCoVar,
29 newIP, newDict, newSelfDict, isSelfDict,
31 newWantedEvVar, newWantedEvVars,
32 newTcEvBinds, addTcEvBind,
34 --------------------------------
36 tcInstTyVar, tcInstTyVars, tcInstSigTyVars,
37 tcInstType, tcInstSigType, instMetaTyVar,
38 tcInstSkolTyVars, tcInstSkolTyVar, tcInstSkolType,
39 tcSkolSigType, tcSkolSigTyVars,
41 --------------------------------
42 -- Checking type validity
43 Rank, UserTypeCtxt(..), checkValidType, checkValidMonoType,
44 SourceTyCtxt(..), checkValidTheta,
45 checkValidInstHead, checkValidInstance,
46 checkInstTermination, checkValidTypeInst, checkTyFamFreeness,
48 growPredTyVars, growThetaTyVars, validDerivPred,
50 --------------------------------
52 zonkType, mkZonkTcTyVar, zonkTcPredType,
53 zonkTcTypeCarefully, skolemiseUnboundMetaTyVar,
54 zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkSigTyVar,
55 zonkQuantifiedTyVar, zonkQuantifiedTyVars,
56 zonkTcType, zonkTcTypes, zonkTcThetaType,
57 zonkTcKindToKind, zonkTcKind,
58 zonkImplication, zonkWanted, zonkEvVar, zonkWantedEvVar,
62 readKindVar, writeKindVar
65 #include "HsVersions.h"
77 import HsSyn -- HsType
78 import TcRnMonad -- TcType, amongst others
95 import Data.List ( (\\) )
99 %************************************************************************
103 %************************************************************************
106 newKindVar :: TcM TcKind
107 newKindVar = do { uniq <- newUnique
108 ; ref <- newMutVar Flexi
109 ; return (mkTyVarTy (mkKindVar uniq ref)) }
111 newKindVars :: Int -> TcM [TcKind]
112 newKindVars n = mapM (\ _ -> newKindVar) (nOfThem n ())
116 %************************************************************************
118 Evidence variables; range over constraints we can abstract over
120 %************************************************************************
123 newEvVars :: TcThetaType -> TcM [EvVar]
124 newEvVars theta = mapM newEvVar theta
126 newWantedEvVar :: TcPredType -> TcM EvVar
127 newWantedEvVar (EqPred ty1 ty2) = newWantedCoVar ty1 ty2
128 newWantedEvVar (ClassP cls tys) = newDict cls tys
129 newWantedEvVar (IParam ip ty) = newIP ip ty
131 newWantedEvVars :: TcThetaType -> TcM [EvVar]
132 newWantedEvVars theta = mapM newWantedEvVar theta
134 newWantedCoVar :: TcType -> TcType -> TcM CoVar
135 newWantedCoVar ty1 ty2 = newCoVar ty1 ty2
138 newEvVar :: TcPredType -> TcM EvVar
139 -- Creates new *rigid* variables for predicates
140 newEvVar (EqPred ty1 ty2) = newCoVar ty1 ty2
141 newEvVar (ClassP cls tys) = newDict cls tys
142 newEvVar (IParam ip ty) = newIP ip ty
144 newCoVar :: TcType -> TcType -> TcM CoVar
146 = do { name <- newName (mkTyVarOccFS (fsLit "co"))
147 ; return (mkCoVar name (mkPredTy (EqPred ty1 ty2))) }
149 newIP :: IPName Name -> TcType -> TcM IpId
151 = do { name <- newName (getOccName (ipNameName ip))
152 ; return (mkLocalId name (mkPredTy (IParam ip ty))) }
154 newDict :: Class -> [TcType] -> TcM DictId
156 = do { name <- newName (mkDictOcc (getOccName cls))
157 ; return (mkLocalId name (mkPredTy (ClassP cls tys))) }
159 newName :: OccName -> TcM Name
161 = do { uniq <- newUnique
163 ; return (mkInternalName uniq occ loc) }
166 newSelfDict :: Class -> [TcType] -> TcM DictId
167 -- Make a dictionary for "self". It behaves just like a normal DictId
168 -- except that it responds True to isSelfDict
169 -- This is used only to suppress confusing error reports
171 = do { uniq <- newUnique
172 ; let name = mkSystemName uniq selfDictOcc
173 ; return (mkLocalId name (mkPredTy (ClassP cls tys))) }
175 selfDictOcc :: OccName
176 selfDictOcc = mkVarOcc "self"
178 isSelfDict :: EvVar -> Bool
179 isSelfDict v = isSystemName (Var.varName v)
180 -- Notice that all *other* evidence variables get Internal Names
184 %************************************************************************
186 SkolemTvs (immutable)
188 %************************************************************************
191 tcInstType :: ([TyVar] -> TcM [TcTyVar]) -- How to instantiate the type variables
192 -> TcType -- Type to instantiate
193 -> TcM ([TcTyVar], TcThetaType, TcType) -- Result
194 -- (type vars (excl coercion vars), preds (incl equalities), rho)
195 tcInstType inst_tyvars ty
196 = case tcSplitForAllTys ty of
197 ([], rho) -> let -- There may be overloading despite no type variables;
198 -- (?x :: Int) => Int -> Int
199 (theta, tau) = tcSplitPhiTy rho
201 return ([], theta, tau)
203 (tyvars, rho) -> do { tyvars' <- inst_tyvars tyvars
205 ; let tenv = zipTopTvSubst tyvars (mkTyVarTys tyvars')
206 -- Either the tyvars are freshly made, by inst_tyvars,
207 -- or (in the call from tcSkolSigType) any nested foralls
208 -- have different binders. Either way, zipTopTvSubst is ok
210 ; let (theta, tau) = tcSplitPhiTy (substTy tenv rho)
211 ; return (tyvars', theta, tau) }
213 mkSkolTyVar :: Name -> Kind -> SkolemInfo -> TcTyVar
214 mkSkolTyVar name kind info = mkTcTyVar name kind (SkolemTv info)
216 tcSkolSigType :: SkolemInfo -> Type -> TcM ([TcTyVar], TcThetaType, TcType)
217 -- Instantiate a type signature with skolem constants, but
218 -- do *not* give them fresh names, because we want the name to
219 -- be in the type environment: it is lexically scoped.
220 tcSkolSigType info ty = tcInstType (\tvs -> return (tcSkolSigTyVars info tvs)) ty
222 tcSkolSigTyVars :: SkolemInfo -> [TyVar] -> [TcTyVar]
223 -- Make skolem constants, but do *not* give them new names, as above
224 tcSkolSigTyVars info tyvars = [ mkSkolTyVar (tyVarName tv) (tyVarKind tv) info
227 tcInstSkolTyVar :: SkolemInfo -> TyVar -> TcM TcTyVar
228 -- Instantiate the tyvar, using
229 -- * the occ-name and kind of the supplied tyvar,
230 -- * the unique from the monad,
231 -- * the location either from the tyvar (skol_info = SigSkol)
232 -- or from the monad (otehrwise)
233 tcInstSkolTyVar skol_info tyvar
234 = do { uniq <- newUnique
235 ; loc <- case skol_info of
236 SigSkol {} -> return (getSrcSpan old_name)
238 ; let new_name = mkInternalName uniq occ loc
239 ; return (mkSkolTyVar new_name kind skol_info) }
241 old_name = tyVarName tyvar
242 occ = nameOccName old_name
243 kind = tyVarKind tyvar
245 tcInstSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
246 -- Get the location from the monad
247 tcInstSkolTyVars info tyvars
248 = mapM (tcInstSkolTyVar info) tyvars
250 tcInstSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
251 -- Instantiate a type with fresh skolem constants
252 -- Binding location comes from the monad
253 tcInstSkolType info ty = tcInstType (tcInstSkolTyVars info) ty
255 tcInstSigType :: Bool -> Name -> TcType -> TcM ([TcTyVar], TcThetaType, TcRhoType)
256 -- Instantiate with skolems or meta SigTvs; depending on use_skols
257 -- Always take location info from the supplied tyvars
258 tcInstSigType use_skols name ty
260 = tcInstType (tcInstSkolTyVars (SigSkol (FunSigCtxt name))) ty
262 = tcInstType tcInstSigTyVars ty
264 tcInstSigTyVars :: [TyVar] -> TcM [TcTyVar]
265 -- Make meta SigTv type variables for patten-bound scoped type varaibles
266 -- We use SigTvs for them, so that they can't unify with arbitrary types
267 tcInstSigTyVars = mapM (\tv -> instMetaTyVar (SigTv (tyVarName tv)) tv)
268 -- ToDo: the "function binding site is bogus
272 %************************************************************************
274 MetaTvs (meta type variables; mutable)
276 %************************************************************************
279 newMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar
280 -- Make a new meta tyvar out of thin air
281 newMetaTyVar meta_info kind
282 = do { uniq <- newMetaUnique
283 ; ref <- newMutVar Flexi
284 ; let name = mkSysTvName uniq fs
285 fs = case meta_info of
289 ; return (mkTcTyVar name kind (MetaTv meta_info ref)) }
291 instMetaTyVar :: MetaInfo -> TyVar -> TcM TcTyVar
292 -- Make a new meta tyvar whose Name and Kind
293 -- come from an existing TyVar
294 instMetaTyVar meta_info tyvar
295 = do { uniq <- newMetaUnique
296 ; ref <- newMutVar Flexi
297 ; let name = setNameUnique (tyVarName tyvar) uniq
298 kind = tyVarKind tyvar
299 ; return (mkTcTyVar name kind (MetaTv meta_info ref)) }
301 readMetaTyVar :: TyVar -> TcM MetaDetails
302 readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
303 readMutVar (metaTvRef tyvar)
305 readWantedCoVar :: CoVar -> TcM MetaDetails
306 readWantedCoVar covar = ASSERT2( isMetaTyVar covar, ppr covar )
307 readMutVar (metaTvRef covar)
311 isFilledMetaTyVar :: TyVar -> TcM Bool
312 -- True of a filled-in (Indirect) meta type variable
314 | not (isTcTyVar tv) = return False
315 | MetaTv _ ref <- tcTyVarDetails tv
316 = do { details <- readMutVar ref
317 ; return (isIndirect details) }
318 | otherwise = return False
320 isFlexiMetaTyVar :: TyVar -> TcM Bool
321 -- True of a un-filled-in (Flexi) meta type variable
323 | not (isTcTyVar tv) = return False
324 | MetaTv _ ref <- tcTyVarDetails tv
325 = do { details <- readMutVar ref
326 ; return (isFlexi details) }
327 | otherwise = return False
330 writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
331 -- Write into a currently-empty MetaTyVar
333 writeMetaTyVar tyvar ty
335 = writeMetaTyVarRef tyvar (metaTvRef tyvar) ty
337 -- Everything from here on only happens if DEBUG is on
338 | not (isTcTyVar tyvar)
339 = WARN( True, text "Writing to non-tc tyvar" <+> ppr tyvar )
342 | MetaTv _ ref <- tcTyVarDetails tyvar
343 = writeMetaTyVarRef tyvar ref ty
346 = WARN( True, text "Writing to non-meta tyvar" <+> ppr tyvar )
349 writeWantedCoVar :: CoVar -> Coercion -> TcM ()
350 writeWantedCoVar cv co = writeMetaTyVar cv co
353 writeMetaTyVarRef :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM ()
354 -- Here the tyvar is for error checking only;
355 -- the ref cell must be for the same tyvar
356 writeMetaTyVarRef tyvar ref ty
358 = do { traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
359 ; writeMutVar ref (Indirect ty) }
361 -- Everything from here on only happens if DEBUG is on
362 | not (isPredTy tv_kind) -- Don't check kinds for updates to coercion variables
363 , not (ty_kind `isSubKind` tv_kind)
364 = WARN( True, hang (text "Ill-kinded update to meta tyvar")
365 2 (ppr tyvar $$ ppr tv_kind $$ ppr ty $$ ppr ty_kind) )
369 = do { meta_details <- readMutVar ref;
370 ; WARN( not (isFlexi meta_details),
371 hang (text "Double update of meta tyvar")
372 2 (ppr tyvar $$ ppr meta_details) )
374 traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
375 ; writeMutVar ref (Indirect ty) }
377 tv_kind = tyVarKind tyvar
378 ty_kind = typeKind ty
382 %************************************************************************
386 %************************************************************************
389 newFlexiTyVar :: Kind -> TcM TcTyVar
390 newFlexiTyVar kind = newMetaTyVar TauTv kind
392 newFlexiTyVarTy :: Kind -> TcM TcType
393 newFlexiTyVarTy kind = do
394 tc_tyvar <- newFlexiTyVar kind
395 return (TyVarTy tc_tyvar)
397 newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
398 newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind)
400 tcInstTyVar :: TyVar -> TcM TcTyVar
401 -- Instantiate with a META type variable
402 tcInstTyVar tyvar = instMetaTyVar TauTv tyvar
404 tcInstTyVars :: [TyVar] -> TcM ([TcTyVar], [TcType], TvSubst)
405 -- Instantiate with META type variables
407 = do { tc_tvs <- mapM tcInstTyVar tyvars
408 ; let tys = mkTyVarTys tc_tvs
409 ; return (tc_tvs, tys, zipTopTvSubst tyvars tys) }
410 -- Since the tyvars are freshly made,
411 -- they cannot possibly be captured by
412 -- any existing for-alls. Hence zipTopTvSubst
416 %************************************************************************
420 %************************************************************************
423 zonkSigTyVar :: TcTyVar -> TcM TcTyVar
425 | isSkolemTyVar sig_tv
426 = return sig_tv -- Happens in the call in TcBinds.checkDistinctTyVars
428 = ASSERT( isSigTyVar sig_tv )
429 do { ty <- zonkTcTyVar sig_tv
430 ; return (tcGetTyVar "zonkSigTyVar" ty) }
431 -- 'ty' is bound to be a type variable, because SigTvs
432 -- can only be unified with type variables
437 %************************************************************************
439 \subsection{Zonking -- the exernal interfaces}
441 %************************************************************************
443 @tcGetGlobalTyVars@ returns a fully-zonked set of tyvars free in the environment.
444 To improve subsequent calls to the same function it writes the zonked set back into
448 tcGetGlobalTyVars :: TcM TcTyVarSet
450 = do { (TcLclEnv {tcl_tyvars = gtv_var}) <- getLclEnv
451 ; gbl_tvs <- readMutVar gtv_var
452 ; gbl_tvs' <- zonkTcTyVarsAndFV gbl_tvs
453 ; writeMutVar gtv_var gbl_tvs'
457 ----------------- Type variables
460 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
461 zonkTcTyVars tyvars = mapM zonkTcTyVar tyvars
463 zonkTcTyVarsAndFV :: TcTyVarSet -> TcM TcTyVarSet
464 zonkTcTyVarsAndFV tyvars = tyVarsOfTypes <$> mapM zonkTcTyVar (varSetElems tyvars)
466 ----------------- Types
468 zonkTcTypeCarefully :: TcType -> TcM TcType
469 -- Do not zonk type variables free in the environment
470 zonkTcTypeCarefully ty
471 = do { env_tvs <- tcGetGlobalTyVars
472 ; zonkType (zonk_tv env_tvs) ty }
475 | tv `elemVarSet` env_tvs
476 = return (TyVarTy tv)
478 = ASSERT( isTcTyVar tv )
479 case tcTyVarDetails tv of
480 SkolemTv {} -> return (TyVarTy tv)
481 FlatSkol ty -> zonkType (zonk_tv env_tvs) ty
482 MetaTv _ ref -> do { cts <- readMutVar ref
484 Flexi -> return (TyVarTy tv)
485 Indirect ty -> zonkType (zonk_tv env_tvs) ty }
487 zonkTcType :: TcType -> TcM TcType
488 -- Simply look through all Flexis
489 zonkTcType ty = zonkType zonkTcTyVar ty
491 zonkTcTyVar :: TcTyVar -> TcM TcType
492 -- Simply look through all Flexis
494 = ASSERT2( isTcTyVar tv, ppr tv )
495 case tcTyVarDetails tv of
496 SkolemTv {} -> return (TyVarTy tv)
497 FlatSkol ty -> zonkTcType ty
498 MetaTv _ ref -> do { cts <- readMutVar ref
500 Flexi -> return (TyVarTy tv)
501 Indirect ty -> zonkTcType ty }
503 zonkTcTypeAndSubst :: TvSubst -> TcType -> TcM TcType
504 -- Zonk, and simultaneously apply a non-necessarily-idempotent substitution
505 zonkTcTypeAndSubst subst ty = zonkType zonk_tv ty
508 = case tcTyVarDetails tv of
509 SkolemTv {} -> return (TyVarTy tv)
510 FlatSkol ty -> zonkType zonk_tv ty
511 MetaTv _ ref -> do { cts <- readMutVar ref
513 Flexi -> zonk_flexi tv
514 Indirect ty -> zonkType zonk_tv ty }
516 = case lookupTyVar subst tv of
517 Just ty -> zonkType zonk_tv ty
518 Nothing -> return (TyVarTy tv)
520 zonkTcTypes :: [TcType] -> TcM [TcType]
521 zonkTcTypes tys = mapM zonkTcType tys
523 zonkTcThetaType :: TcThetaType -> TcM TcThetaType
524 zonkTcThetaType theta = mapM zonkTcPredType theta
526 zonkTcPredType :: TcPredType -> TcM TcPredType
527 zonkTcPredType (ClassP c ts) = ClassP c <$> zonkTcTypes ts
528 zonkTcPredType (IParam n t) = IParam n <$> zonkTcType t
529 zonkTcPredType (EqPred t1 t2) = EqPred <$> zonkTcType t1 <*> zonkTcType t2
532 ------------------- These ...ToType, ...ToKind versions
533 are used at the end of type checking
536 zonkQuantifiedTyVars :: [TcTyVar] -> TcM [TcTyVar]
537 zonkQuantifiedTyVars = mapM zonkQuantifiedTyVar
539 zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar
540 -- The quantified type variables often include meta type variables
541 -- we want to freeze them into ordinary type variables, and
542 -- default their kind (e.g. from OpenTypeKind to TypeKind)
543 -- -- see notes with Kind.defaultKind
544 -- The meta tyvar is updated to point to the new skolem TyVar. Now any
545 -- bound occurences of the original type variable will get zonked to
546 -- the immutable version.
548 -- We leave skolem TyVars alone; they are immutable.
549 zonkQuantifiedTyVar tv
550 = ASSERT2( isTcTyVar tv, ppr tv )
551 case tcTyVarDetails tv of
552 FlatSkol {} -> pprPanic "zonkQuantifiedTyVar" (ppr tv)
553 SkolemTv {} -> do { kind <- zonkTcType (tyVarKind tv)
554 ; return $ setTyVarKind tv kind }
555 -- It might be a skolem type variable,
556 -- for example from a user type signature
560 -- [Sept 04] Check for non-empty.
561 -- See note [Silly Type Synonym]
562 (readMutVar _ref >>= \cts ->
565 Indirect ty -> WARN( True, ppr tv $$ ppr ty )
568 skolemiseUnboundMetaTyVar UnkSkol tv
570 skolemiseUnboundMetaTyVar :: SkolemInfo -> TcTyVar -> TcM TyVar
571 -- We have a Meta tyvar with a ref-cell inside it
572 -- Skolemise it, including giving it a new Name, so that
573 -- we are totally out of Meta-tyvar-land
574 -- We create a skolem TyVar, not a regular TyVar
575 -- See Note [Zonking to Skolem]
576 skolemiseUnboundMetaTyVar skol_info tv
577 = ASSERT2( isMetaTyVar tv, ppr tv )
578 do { uniq <- newUnique -- Remove it from TcMetaTyVar unique land
579 ; let final_kind = defaultKind (tyVarKind tv)
580 final_name = setNameUnique (tyVarName tv) uniq
581 final_tv = mkSkolTyVar final_name final_kind skol_info
582 ; writeMetaTyVar tv (mkTyVarTy final_tv)
587 zonkImplication :: Implication -> TcM Implication
588 zonkImplication implic@(Implic { ic_given = given
589 , ic_wanted = wanted })
590 = do { given' <- mapM zonkEvVar given
591 ; wanted' <- mapBagM zonkWanted wanted
592 ; return (implic { ic_given = given', ic_wanted = wanted' }) }
594 zonkEvVar :: EvVar -> TcM EvVar
595 zonkEvVar var = do { ty' <- zonkTcType (varType var)
596 ; return (setVarType var ty') }
598 zonkWanted :: WantedConstraint -> TcM WantedConstraint
599 zonkWanted (WcImplic imp) = do { imp' <- zonkImplication imp; return (WcImplic imp') }
600 zonkWanted (WcEvVar ev) = do { ev' <- zonkWantedEvVar ev; return (WcEvVar ev') }
602 zonkWantedEvVar :: WantedEvVar -> TcM WantedEvVar
603 zonkWantedEvVar (WantedEvVar v l) = do { v' <- zonkEvVar v; return (WantedEvVar v' l) }
607 Note [Silly Type Synonyms]
608 ~~~~~~~~~~~~~~~~~~~~~~~~~~
610 type C u a = u -- Note 'a' unused
612 foo :: (forall a. C u a -> C u a) -> u
616 bar = foo (\t -> t + t)
618 * From the (\t -> t+t) we get type {Num d} => d -> d
621 * Now unify with type of foo's arg, and we get:
622 {Num (C d a)} => C d a -> C d a
625 * Now abstract over the 'a', but float out the Num (C d a) constraint
626 because it does not 'really' mention a. (see exactTyVarsOfType)
627 The arg to foo becomes
630 * So we get a dict binding for Num (C d a), which is zonked to give
632 [Note Sept 04: now that we are zonking quantified type variables
633 on construction, the 'a' will be frozen as a regular tyvar on
634 quantification, so the floated dict will still have type (C d a).
635 Which renders this whole note moot; happily!]
637 * Then the \/\a abstraction has a zonked 'a' in it.
639 All very silly. I think its harmless to ignore the problem. We'll end up with
640 a \/\a in the final result but all the occurrences of a will be zonked to ()
642 Note [Zonking to Skolem]
643 ~~~~~~~~~~~~~~~~~~~~~~~~
644 We used to zonk quantified type variables to regular TyVars. However, this
645 leads to problems. Consider this program from the regression test suite:
647 eval :: Int -> String -> String -> String
648 eval 0 root actual = evalRHS 0 root actual
651 evalRHS 0 root actual = eval 0 root actual
653 It leads to the deferral of an equality (wrapped in an implication constraint)
655 forall a. (String -> String -> String) ~ a
657 which is propagated up to the toplevel (see TcSimplify.tcSimplifyInferCheck).
658 In the meantime `a' is zonked and quantified to form `evalRHS's signature.
659 This has the *side effect* of also zonking the `a' in the deferred equality
660 (which at this point is being handed around wrapped in an implication
663 Finally, the equality (with the zonked `a') will be handed back to the
664 simplifier by TcRnDriver.tcRnSrcDecls calling TcSimplify.tcSimplifyTop.
665 If we zonk `a' with a regular type variable, we will have this regular type
666 variable now floating around in the simplifier, which in many places assumes to
667 only see proper TcTyVars.
669 We can avoid this problem by zonking with a skolem. The skolem is rigid
670 (which we require for a quantified variable), but is still a TcTyVar that the
671 simplifier knows how to deal with.
674 %************************************************************************
676 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
678 %* For internal use only! *
680 %************************************************************************
683 -- For unbound, mutable tyvars, zonkType uses the function given to it
684 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
685 -- type variable and zonks the kind too
687 zonkType :: (TcTyVar -> TcM Type) -- What to do with TcTyVars
688 -> TcType -> TcM Type
689 zonkType zonk_tc_tyvar ty
692 go (TyConApp tc tys) = do tys' <- mapM go tys
693 return (TyConApp tc tys')
695 go (PredTy p) = do p' <- go_pred p
698 go (FunTy arg res) = do arg' <- go arg
700 return (FunTy arg' res')
702 go (AppTy fun arg) = do fun' <- go fun
704 return (mkAppTy fun' arg')
705 -- NB the mkAppTy; we might have instantiated a
706 -- type variable to a type constructor, so we need
707 -- to pull the TyConApp to the top.
709 -- The two interesting cases!
710 go (TyVarTy tyvar) | isTcTyVar tyvar = zonk_tc_tyvar tyvar
711 | otherwise = liftM TyVarTy $
712 zonkTyVar zonk_tc_tyvar tyvar
713 -- Ordinary (non Tc) tyvars occur inside quantified types
715 go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar ) do
717 tyvar' <- zonkTyVar zonk_tc_tyvar tyvar
718 return (ForAllTy tyvar' ty')
720 go_pred (ClassP c tys) = do tys' <- mapM go tys
721 return (ClassP c tys')
722 go_pred (IParam n ty) = do ty' <- go ty
723 return (IParam n ty')
724 go_pred (EqPred ty1 ty2) = do ty1' <- go ty1
726 return (EqPred ty1' ty2')
728 mkZonkTcTyVar :: (TcTyVar -> TcM Type) -- What to do for an *mutable Flexi* var
729 -> TcTyVar -> TcM TcType
730 mkZonkTcTyVar unbound_var_fn tyvar
731 = ASSERT( isTcTyVar tyvar )
732 case tcTyVarDetails tyvar of
733 SkolemTv {} -> return (TyVarTy tyvar)
734 FlatSkol ty -> zonkType (mkZonkTcTyVar unbound_var_fn) ty
735 MetaTv _ ref -> do { cts <- readMutVar ref
737 Flexi -> unbound_var_fn tyvar
738 Indirect ty -> zonkType (mkZonkTcTyVar unbound_var_fn) ty }
740 -- Zonk the kind of a non-TC tyvar in case it is a coercion variable
741 -- (their kind contains types).
742 zonkTyVar :: (TcTyVar -> TcM Type) -- What to do for a TcTyVar
743 -> TyVar -> TcM TyVar
744 zonkTyVar zonk_tc_tyvar tv
746 = do { kind <- zonkType zonk_tc_tyvar (tyVarKind tv)
747 ; return $ setTyVarKind tv kind }
748 | otherwise = return tv
753 %************************************************************************
757 %************************************************************************
760 readKindVar :: KindVar -> TcM (MetaDetails)
761 writeKindVar :: KindVar -> TcKind -> TcM ()
762 readKindVar kv = readMutVar (kindVarRef kv)
763 writeKindVar kv val = writeMutVar (kindVarRef kv) (Indirect val)
766 zonkTcKind :: TcKind -> TcM TcKind
767 zonkTcKind k = zonkTcType k
770 zonkTcKindToKind :: TcKind -> TcM Kind
771 -- When zonking a TcKind to a kind, we need to instantiate kind variables,
772 -- Haskell specifies that * is to be used, so we follow that.
774 = zonkType (mkZonkTcTyVar (\ _ -> return liftedTypeKind)) k
777 %************************************************************************
779 \subsection{Checking a user type}
781 %************************************************************************
783 When dealing with a user-written type, we first translate it from an HsType
784 to a Type, performing kind checking, and then check various things that should
785 be true about it. We don't want to perform these checks at the same time
786 as the initial translation because (a) they are unnecessary for interface-file
787 types and (b) when checking a mutually recursive group of type and class decls,
788 we can't "look" at the tycons/classes yet. Also, the checks are are rather
789 diverse, and used to really mess up the other code.
791 One thing we check for is 'rank'.
793 Rank 0: monotypes (no foralls)
794 Rank 1: foralls at the front only, Rank 0 inside
795 Rank 2: foralls at the front, Rank 1 on left of fn arrow,
797 basic ::= tyvar | T basic ... basic
799 r2 ::= forall tvs. cxt => r2a
800 r2a ::= r1 -> r2a | basic
801 r1 ::= forall tvs. cxt => r0
802 r0 ::= r0 -> r0 | basic
804 Another thing is to check that type synonyms are saturated.
805 This might not necessarily show up in kind checking.
807 data T k = MkT (k Int)
812 checkValidType :: UserTypeCtxt -> Type -> TcM ()
813 -- Checks that the type is valid for the given context
814 checkValidType ctxt ty = do
815 traceTc "checkValidType" (ppr ty)
816 unboxed <- xoptM Opt_UnboxedTuples
817 rank2 <- xoptM Opt_Rank2Types
818 rankn <- xoptM Opt_RankNTypes
819 polycomp <- xoptM Opt_PolymorphicComponents
821 gen_rank n | rankn = ArbitraryRank
826 DefaultDeclCtxt-> MustBeMonoType
827 ResSigCtxt -> MustBeMonoType
828 LamPatSigCtxt -> gen_rank 0
829 BindPatSigCtxt -> gen_rank 0
830 TySynCtxt _ -> gen_rank 0
831 GenPatCtxt -> gen_rank 1
832 -- This one is a bit of a hack
833 -- See the forall-wrapping in TcClassDcl.mkGenericInstance
835 ExprSigCtxt -> gen_rank 1
836 FunSigCtxt _ -> gen_rank 1
837 ConArgCtxt _ | polycomp -> gen_rank 2
838 -- We are given the type of the entire
839 -- constructor, hence rank 1
840 | otherwise -> gen_rank 1
842 ForSigCtxt _ -> gen_rank 1
843 SpecInstCtxt -> gen_rank 1
844 ThBrackCtxt -> gen_rank 1
846 actual_kind = typeKind ty
848 kind_ok = case ctxt of
849 TySynCtxt _ -> True -- Any kind will do
850 ThBrackCtxt -> True -- Any kind will do
851 ResSigCtxt -> isSubOpenTypeKind actual_kind
852 ExprSigCtxt -> isSubOpenTypeKind actual_kind
853 GenPatCtxt -> isLiftedTypeKind actual_kind
854 ForSigCtxt _ -> isLiftedTypeKind actual_kind
855 _ -> isSubArgTypeKind actual_kind
857 ubx_tup = case ctxt of
858 TySynCtxt _ | unboxed -> UT_Ok
859 ExprSigCtxt | unboxed -> UT_Ok
860 ThBrackCtxt | unboxed -> UT_Ok
863 -- Check the internal validity of the type itself
864 check_type rank ubx_tup ty
866 -- Check that the thing has kind Type, and is lifted if necessary
867 -- Do this second, becuase we can't usefully take the kind of an
868 -- ill-formed type such as (a~Int)
869 checkTc kind_ok (kindErr actual_kind)
871 traceTc "checkValidType done" (ppr ty)
873 checkValidMonoType :: Type -> TcM ()
874 checkValidMonoType ty = check_mono_type MustBeMonoType ty
879 data Rank = ArbitraryRank -- Any rank ok
880 | MustBeMonoType -- Monotype regardless of flags
881 | TyConArgMonoType -- Monotype but could be poly if -XImpredicativeTypes
882 | SynArgMonoType -- Monotype but could be poly if -XLiberalTypeSynonyms
883 | Rank Int -- Rank n, but could be more with -XRankNTypes
885 decRank :: Rank -> Rank -- Function arguments
886 decRank (Rank 0) = Rank 0
887 decRank (Rank n) = Rank (n-1)
888 decRank other_rank = other_rank
890 nonZeroRank :: Rank -> Bool
891 nonZeroRank ArbitraryRank = True
892 nonZeroRank (Rank n) = n>0
893 nonZeroRank _ = False
895 ----------------------------------------
896 data UbxTupFlag = UT_Ok | UT_NotOk
897 -- The "Ok" version means "ok if UnboxedTuples is on"
899 ----------------------------------------
900 check_mono_type :: Rank -> Type -> TcM () -- No foralls anywhere
901 -- No unlifted types of any kind
902 check_mono_type rank ty
903 = do { check_type rank UT_NotOk ty
904 ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
906 check_type :: Rank -> UbxTupFlag -> Type -> TcM ()
907 -- The args say what the *type context* requires, independent
908 -- of *flag* settings. You test the flag settings at usage sites.
910 -- Rank is allowed rank for function args
911 -- Rank 0 means no for-alls anywhere
913 check_type rank ubx_tup ty
914 | not (null tvs && null theta)
915 = do { checkTc (nonZeroRank rank) (forAllTyErr rank ty)
916 -- Reject e.g. (Maybe (?x::Int => Int)),
917 -- with a decent error message
918 ; check_valid_theta SigmaCtxt theta
919 ; check_type rank ubx_tup tau -- Allow foralls to right of arrow
920 ; checkAmbiguity tvs theta (tyVarsOfType tau) }
922 (tvs, theta, tau) = tcSplitSigmaTy ty
924 -- Naked PredTys should, I think, have been rejected before now
925 check_type _ _ ty@(PredTy {})
926 = failWithTc (text "Predicate" <+> ppr ty <+> text "used as a type")
928 check_type _ _ (TyVarTy _) = return ()
930 check_type rank _ (FunTy arg_ty res_ty)
931 = do { check_type (decRank rank) UT_NotOk arg_ty
932 ; check_type rank UT_Ok res_ty }
934 check_type rank _ (AppTy ty1 ty2)
935 = do { check_arg_type rank ty1
936 ; check_arg_type rank ty2 }
938 check_type rank ubx_tup ty@(TyConApp tc tys)
940 = do { -- Check that the synonym has enough args
941 -- This applies equally to open and closed synonyms
942 -- It's OK to have an *over-applied* type synonym
943 -- data Tree a b = ...
944 -- type Foo a = Tree [a]
945 -- f :: Foo a b -> ...
946 checkTc (tyConArity tc <= length tys) arity_msg
948 -- See Note [Liberal type synonyms]
949 ; liberal <- xoptM Opt_LiberalTypeSynonyms
950 ; if not liberal || isSynFamilyTyCon tc then
951 -- For H98 and synonym families, do check the type args
952 mapM_ (check_mono_type SynArgMonoType) tys
954 else -- In the liberal case (only for closed syns), expand then check
956 Just ty' -> check_type rank ubx_tup ty'
957 Nothing -> pprPanic "check_tau_type" (ppr ty)
960 | isUnboxedTupleTyCon tc
961 = do { ub_tuples_allowed <- xoptM Opt_UnboxedTuples
962 ; checkTc (ubx_tup_ok ub_tuples_allowed) ubx_tup_msg
964 ; impred <- xoptM Opt_ImpredicativeTypes
965 ; let rank' = if impred then ArbitraryRank else TyConArgMonoType
966 -- c.f. check_arg_type
967 -- However, args are allowed to be unlifted, or
968 -- more unboxed tuples, so can't use check_arg_ty
969 ; mapM_ (check_type rank' UT_Ok) tys }
972 = mapM_ (check_arg_type rank) tys
975 ubx_tup_ok ub_tuples_allowed = case ubx_tup of
976 UT_Ok -> ub_tuples_allowed
980 tc_arity = tyConArity tc
982 arity_msg = arityErr "Type synonym" (tyConName tc) tc_arity n_args
983 ubx_tup_msg = ubxArgTyErr ty
985 check_type _ _ ty = pprPanic "check_type" (ppr ty)
987 ----------------------------------------
988 check_arg_type :: Rank -> Type -> TcM ()
989 -- The sort of type that can instantiate a type variable,
990 -- or be the argument of a type constructor.
991 -- Not an unboxed tuple, but now *can* be a forall (since impredicativity)
992 -- Other unboxed types are very occasionally allowed as type
993 -- arguments depending on the kind of the type constructor
995 -- For example, we want to reject things like:
997 -- instance Ord a => Ord (forall s. T s a)
999 -- g :: T s (forall b.b)
1001 -- NB: unboxed tuples can have polymorphic or unboxed args.
1002 -- This happens in the workers for functions returning
1003 -- product types with polymorphic components.
1004 -- But not in user code.
1005 -- Anyway, they are dealt with by a special case in check_tau_type
1007 check_arg_type rank ty
1008 = do { impred <- xoptM Opt_ImpredicativeTypes
1009 ; let rank' = case rank of -- Predictive => must be monotype
1010 MustBeMonoType -> MustBeMonoType -- Monotype, regardless
1011 _other | impred -> ArbitraryRank
1012 | otherwise -> TyConArgMonoType
1013 -- Make sure that MustBeMonoType is propagated,
1014 -- so that we don't suggest -XImpredicativeTypes in
1015 -- (Ord (forall a.a)) => a -> a
1016 -- and so that if it Must be a monotype, we check that it is!
1018 ; check_type rank' UT_NotOk ty
1019 ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
1021 ----------------------------------------
1022 forAllTyErr :: Rank -> Type -> SDoc
1024 = vcat [ hang (ptext (sLit "Illegal polymorphic or qualified type:")) 2 (ppr ty)
1027 suggestion = case rank of
1028 Rank _ -> ptext (sLit "Perhaps you intended to use -XRankNTypes or -XRank2Types")
1029 TyConArgMonoType -> ptext (sLit "Perhaps you intended to use -XImpredicativeTypes")
1030 SynArgMonoType -> ptext (sLit "Perhaps you intended to use -XLiberalTypeSynonyms")
1031 _ -> empty -- Polytype is always illegal
1033 unliftedArgErr, ubxArgTyErr :: Type -> SDoc
1034 unliftedArgErr ty = sep [ptext (sLit "Illegal unlifted type:"), ppr ty]
1035 ubxArgTyErr ty = sep [ptext (sLit "Illegal unboxed tuple type as function argument:"), ppr ty]
1037 kindErr :: Kind -> SDoc
1038 kindErr kind = sep [ptext (sLit "Expecting an ordinary type, but found a type of kind"), ppr kind]
1041 Note [Liberal type synonyms]
1042 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1043 If -XLiberalTypeSynonyms is on, expand closed type synonyms *before*
1044 doing validity checking. This allows us to instantiate a synonym defn
1045 with a for-all type, or with a partially-applied type synonym.
1049 Here, T is partially applied, so it's illegal in H98. But if you
1050 expand S first, then T we get just
1054 IMPORTANT: suppose T is a type synonym. Then we must do validity
1055 checking on an appliation (T ty1 ty2)
1057 *either* before expansion (i.e. check ty1, ty2)
1058 *or* after expansion (i.e. expand T ty1 ty2, and then check)
1061 If we do both, we get exponential behaviour!!
1063 data TIACons1 i r c = c i ::: r c
1064 type TIACons2 t x = TIACons1 t (TIACons1 t x)
1065 type TIACons3 t x = TIACons2 t (TIACons1 t x)
1066 type TIACons4 t x = TIACons2 t (TIACons2 t x)
1067 type TIACons7 t x = TIACons4 t (TIACons3 t x)
1070 %************************************************************************
1072 \subsection{Checking a theta or source type}
1074 %************************************************************************
1077 -- Enumerate the contexts in which a "source type", <S>, can occur
1081 -- or (N a) where N is a newtype
1084 = ClassSCCtxt Name -- Superclasses of clas
1085 -- class <S> => C a where ...
1086 | SigmaCtxt -- Theta part of a normal for-all type
1087 -- f :: <S> => a -> a
1088 | DataTyCtxt Name -- Theta part of a data decl
1089 -- data <S> => T a = MkT a
1090 | TypeCtxt -- Source type in an ordinary type
1092 | InstThetaCtxt -- Context of an instance decl
1093 -- instance <S> => C [a] where ...
1095 pprSourceTyCtxt :: SourceTyCtxt -> SDoc
1096 pprSourceTyCtxt (ClassSCCtxt c) = ptext (sLit "the super-classes of class") <+> quotes (ppr c)
1097 pprSourceTyCtxt SigmaCtxt = ptext (sLit "the context of a polymorphic type")
1098 pprSourceTyCtxt (DataTyCtxt tc) = ptext (sLit "the context of the data type declaration for") <+> quotes (ppr tc)
1099 pprSourceTyCtxt InstThetaCtxt = ptext (sLit "the context of an instance declaration")
1100 pprSourceTyCtxt TypeCtxt = ptext (sLit "the context of a type")
1104 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
1105 checkValidTheta ctxt theta
1106 = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
1108 -------------------------
1109 check_valid_theta :: SourceTyCtxt -> [PredType] -> TcM ()
1110 check_valid_theta _ []
1112 check_valid_theta ctxt theta = do
1114 warnTc (notNull dups) (dupPredWarn dups)
1115 mapM_ (check_pred_ty dflags ctxt) theta
1117 (_,dups) = removeDups tcCmpPred theta
1119 -------------------------
1120 check_pred_ty :: DynFlags -> SourceTyCtxt -> PredType -> TcM ()
1121 check_pred_ty dflags ctxt pred@(ClassP cls tys)
1122 = do { -- Class predicates are valid in all contexts
1123 ; checkTc (arity == n_tys) arity_err
1125 -- Check the form of the argument types
1126 ; mapM_ checkValidMonoType tys
1127 ; checkTc (check_class_pred_tys dflags ctxt tys)
1128 (predTyVarErr pred $$ how_to_allow)
1131 class_name = className cls
1132 arity = classArity cls
1134 arity_err = arityErr "Class" class_name arity n_tys
1135 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 (xopt Opt_TypeFamilies dflags) (eqPredTyErr pred)
1142 ; checkTc (case ctxt of ClassSCCtxt {} -> False; _ -> True)
1143 (eqSuperClassErr pred)
1145 -- Check the form of the argument types
1146 ; checkValidMonoType ty1
1147 ; checkValidMonoType ty2
1150 check_pred_ty _ SigmaCtxt (IParam _ ty) = checkValidMonoType 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 _ _ 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 _ -> flexible_contexts || all tyvar_head tys
1174 flexible_contexts = xopt Opt_FlexibleContexts dflags
1175 undecidable_ok = xopt Opt_UndecidableInstances dflags
1177 -------------------------
1178 tyvar_head :: Type -> Bool
1179 tyvar_head ty -- Haskell 98 allows predicates of form
1180 | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
1181 | otherwise -- where a is a type variable
1182 = case tcSplitAppTy_maybe ty of
1183 Just (ty, _) -> tyvar_head ty
1190 is ambiguous if P contains generic variables
1191 (i.e. one of the Vs) that are not mentioned in tau
1193 However, we need to take account of functional dependencies
1194 when we speak of 'mentioned in tau'. Example:
1195 class C a b | a -> b where ...
1197 forall x y. (C x y) => x
1198 is not ambiguous because x is mentioned and x determines y
1200 NB; the ambiguity check is only used for *user* types, not for types
1201 coming from inteface files. The latter can legitimately have
1202 ambiguous types. Example
1204 class S a where s :: a -> (Int,Int)
1205 instance S Char where s _ = (1,1)
1206 f:: S a => [a] -> Int -> (Int,Int)
1207 f (_::[a]) x = (a*x,b)
1208 where (a,b) = s (undefined::a)
1210 Here the worker for f gets the type
1211 fw :: forall a. S a => Int -> (# Int, Int #)
1213 If the list of tv_names is empty, we have a monotype, and then we
1214 don't need to check for ambiguity either, because the test can't fail
1217 In addition, GHC insists that at least one type variable
1218 in each constraint is in V. So we disallow a type like
1219 forall a. Eq b => b -> b
1220 even in a scope where b is in scope.
1223 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
1224 checkAmbiguity forall_tyvars theta tau_tyvars
1225 = mapM_ complain (filter is_ambig theta)
1227 complain pred = addErrTc (ambigErr pred)
1228 extended_tau_vars = growThetaTyVars theta tau_tyvars
1230 -- See Note [Implicit parameters and ambiguity] in TcSimplify
1231 is_ambig pred = isClassPred pred &&
1232 any ambig_var (varSetElems (tyVarsOfPred pred))
1234 ambig_var ct_var = (ct_var `elem` forall_tyvars) &&
1235 not (ct_var `elemVarSet` extended_tau_vars)
1237 ambigErr :: PredType -> SDoc
1239 = sep [ptext (sLit "Ambiguous constraint") <+> quotes (pprPred pred),
1240 nest 2 (ptext (sLit "At least one of the forall'd type variables mentioned by the constraint") $$
1241 ptext (sLit "must be reachable from the type after the '=>'"))]
1244 Note [Growing the tau-tvs using constraints]
1245 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1246 (growInstsTyVars insts tvs) is the result of extending the set
1247 of tyvars tvs using all conceivable links from pred
1249 E.g. tvs = {a}, preds = {H [a] b, K (b,Int) c, Eq e}
1250 Then grow precs tvs = {a,b,c}
1253 growThetaTyVars :: TcThetaType -> TyVarSet -> TyVarSet
1254 -- See Note [Growing the tau-tvs using constraints]
1255 growThetaTyVars theta tvs
1257 | otherwise = fixVarSet mk_next tvs
1259 mk_next tvs = foldr grow_one tvs theta
1260 grow_one pred tvs = growPredTyVars pred tvs `unionVarSet` tvs
1262 growPredTyVars :: TcPredType
1263 -> TyVarSet -- The set to extend
1264 -> TyVarSet -- TyVars of the predicate if it intersects
1265 -- the set, or is implicit parameter
1266 growPredTyVars pred tvs
1267 | IParam {} <- pred = pred_tvs -- See Note [Implicit parameters and ambiguity]
1268 | pred_tvs `intersectsVarSet` tvs = pred_tvs
1269 | otherwise = emptyVarSet
1271 pred_tvs = tyVarsOfPred pred
1274 Note [Implicit parameters and ambiguity]
1275 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1276 Only a *class* predicate can give rise to ambiguity
1277 An *implicit parameter* cannot. For example:
1278 foo :: (?x :: [a]) => Int
1280 is fine. The call site will suppply a particular 'x'
1282 Furthermore, the type variables fixed by an implicit parameter
1283 propagate to the others. E.g.
1284 foo :: (Show a, ?x::[a]) => Int
1286 The type of foo looks ambiguous. But it isn't, because at a call site
1288 let ?x = 5::Int in foo
1289 and all is well. In effect, implicit parameters are, well, parameters,
1290 so we can take their type variables into account as part of the
1291 "tau-tvs" stuff. This is done in the function 'FunDeps.grow'.
1295 checkThetaCtxt :: SourceTyCtxt -> ThetaType -> SDoc
1296 checkThetaCtxt ctxt theta
1297 = vcat [ptext (sLit "In the context:") <+> pprTheta theta,
1298 ptext (sLit "While checking") <+> pprSourceTyCtxt ctxt ]
1300 eqSuperClassErr :: PredType -> SDoc
1301 eqSuperClassErr pred
1302 = hang (ptext (sLit "Alas, GHC 7.0 still cannot handle equality superclasses:"))
1305 badPredTyErr, eqPredTyErr, predTyVarErr :: PredType -> SDoc
1306 badPredTyErr pred = ptext (sLit "Illegal constraint") <+> pprPred pred
1307 eqPredTyErr pred = ptext (sLit "Illegal equational constraint") <+> pprPred pred
1309 parens (ptext (sLit "Use -XTypeFamilies to permit this"))
1310 predTyVarErr pred = sep [ptext (sLit "Non type-variable argument"),
1311 nest 2 (ptext (sLit "in the constraint:") <+> pprPred pred)]
1312 dupPredWarn :: [[PredType]] -> SDoc
1313 dupPredWarn dups = ptext (sLit "Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
1315 arityErr :: Outputable a => String -> a -> Int -> Int -> SDoc
1316 arityErr kind name n m
1317 = hsep [ text kind, quotes (ppr name), ptext (sLit "should have"),
1318 n_arguments <> comma, text "but has been given",
1319 if m==0 then text "none" else int m]
1321 n_arguments | n == 0 = ptext (sLit "no arguments")
1322 | n == 1 = ptext (sLit "1 argument")
1323 | True = hsep [int n, ptext (sLit "arguments")]
1326 %************************************************************************
1328 \subsection{Checking for a decent instance head type}
1330 %************************************************************************
1332 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1333 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1335 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1336 flag is on, or (2)~the instance is imported (they must have been
1337 compiled elsewhere). In these cases, we let them go through anyway.
1339 We can also have instances for functions: @instance Foo (a -> b) ...@.
1342 checkValidInstHead :: Type -> TcM (Class, [TcType])
1344 checkValidInstHead ty -- Should be a source type
1345 = case tcSplitPredTy_maybe ty of {
1346 Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
1349 case getClassPredTys_maybe pred of {
1350 Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
1351 Just (clas,tys) -> do
1354 check_inst_head dflags clas tys
1358 check_inst_head :: DynFlags -> Class -> [Type] -> TcM ()
1359 check_inst_head dflags clas tys
1360 = do { -- If GlasgowExts then check at least one isn't a type variable
1361 ; checkTc (xopt Opt_TypeSynonymInstances dflags ||
1362 all tcInstHeadTyNotSynonym tys)
1363 (instTypeErr (pprClassPred clas tys) head_type_synonym_msg)
1364 ; checkTc (xopt Opt_FlexibleInstances dflags ||
1365 all tcInstHeadTyAppAllTyVars tys)
1366 (instTypeErr (pprClassPred clas tys) head_type_args_tyvars_msg)
1367 ; checkTc (xopt Opt_MultiParamTypeClasses dflags ||
1369 (instTypeErr (pprClassPred clas tys) head_one_type_msg)
1370 -- May not contain type family applications
1371 ; mapM_ checkTyFamFreeness tys
1373 ; mapM_ checkValidMonoType tys
1374 -- For now, I only allow tau-types (not polytypes) in
1375 -- the head of an instance decl.
1376 -- E.g. instance C (forall a. a->a) is rejected
1377 -- One could imagine generalising that, but I'm not sure
1378 -- what all the consequences might be
1382 head_type_synonym_msg = parens (
1383 text "All instance types must be of the form (T t1 ... tn)" $$
1384 text "where T is not a synonym." $$
1385 text "Use -XTypeSynonymInstances if you want to disable this.")
1387 head_type_args_tyvars_msg = parens (vcat [
1388 text "All instance types must be of the form (T a1 ... an)",
1389 text "where a1 ... an are type *variables*,",
1390 text "and each type variable appears at most once in the instance head.",
1391 text "Use -XFlexibleInstances if you want to disable this."])
1393 head_one_type_msg = parens (
1394 text "Only one type can be given in an instance head." $$
1395 text "Use -XMultiParamTypeClasses if you want to allow more.")
1397 instTypeErr :: SDoc -> SDoc -> SDoc
1398 instTypeErr pp_ty msg
1399 = sep [ptext (sLit "Illegal instance declaration for") <+> quotes pp_ty,
1404 %************************************************************************
1406 \subsection{Checking instance for termination}
1408 %************************************************************************
1411 checkValidInstance :: LHsType Name -> [TyVar] -> ThetaType -> Type
1412 -> TcM (Class, [TcType])
1413 checkValidInstance hs_type tyvars theta tau
1414 = setSrcSpan (getLoc hs_type) $
1415 do { (clas, inst_tys) <- setSrcSpan head_loc $
1416 checkValidInstHead tau
1418 ; undecidable_ok <- xoptM Opt_UndecidableInstances
1420 ; checkValidTheta InstThetaCtxt theta
1421 ; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys)
1423 -- Check that instance inference will terminate (if we care)
1424 -- For Haskell 98 this will already have been done by checkValidTheta,
1425 -- but as we may be using other extensions we need to check.
1426 ; unless undecidable_ok $
1427 mapM_ addErrTc (checkInstTermination inst_tys theta)
1429 -- The Coverage Condition
1430 ; checkTc (undecidable_ok || checkInstCoverage clas inst_tys)
1431 (instTypeErr (pprClassPred clas inst_tys) msg)
1433 ; return (clas, inst_tys)
1436 msg = parens (vcat [ptext (sLit "the Coverage Condition fails for one of the functional dependencies;"),
1439 -- The location of the "head" of the instance
1440 head_loc = case hs_type of
1441 L _ (HsForAllTy _ _ _ (L loc _)) -> loc
1445 Termination test: the so-called "Paterson conditions" (see Section 5 of
1446 "Understanding functionsl dependencies via Constraint Handling Rules,
1449 We check that each assertion in the context satisfies:
1450 (1) no variable has more occurrences in the assertion than in the head, and
1451 (2) the assertion has fewer constructors and variables (taken together
1452 and counting repetitions) than the head.
1453 This is only needed with -fglasgow-exts, as Haskell 98 restrictions
1454 (which have already been checked) guarantee termination.
1456 The underlying idea is that
1458 for any ground substitution, each assertion in the
1459 context has fewer type constructors than the head.
1463 checkInstTermination :: [TcType] -> ThetaType -> [Message]
1464 checkInstTermination tys theta
1465 = mapCatMaybes check theta
1468 size = sizeTypes tys
1470 | not (null (fvPred pred \\ fvs))
1471 = Just (predUndecErr pred nomoreMsg $$ parens undecidableMsg)
1472 | sizePred pred >= size
1473 = Just (predUndecErr pred smallerMsg $$ parens undecidableMsg)
1477 predUndecErr :: PredType -> SDoc -> SDoc
1478 predUndecErr pred msg = sep [msg,
1479 nest 2 (ptext (sLit "in the constraint:") <+> pprPred pred)]
1481 nomoreMsg, smallerMsg, undecidableMsg :: SDoc
1482 nomoreMsg = ptext (sLit "Variable occurs more often in a constraint than in the instance head")
1483 smallerMsg = ptext (sLit "Constraint is no smaller than the instance head")
1484 undecidableMsg = ptext (sLit "Use -XUndecidableInstances to permit this")
1487 validDeivPred checks for OK 'deriving' context. See Note [Exotic
1488 derived instance contexts] in TcSimplify. However the predicate is
1489 here because it uses sizeTypes, fvTypes.
1492 validDerivPred :: PredType -> Bool
1493 validDerivPred (ClassP _ tys) = hasNoDups fvs && sizeTypes tys == length fvs
1494 where fvs = fvTypes tys
1495 validDerivPred _ = False
1499 %************************************************************************
1501 Checking type instance well-formedness and termination
1503 %************************************************************************
1506 -- Check that a "type instance" is well-formed (which includes decidability
1507 -- unless -XUndecidableInstances is given).
1509 checkValidTypeInst :: [Type] -> Type -> TcM ()
1510 checkValidTypeInst typats rhs
1511 = do { -- left-hand side contains no type family applications
1512 -- (vanilla synonyms are fine, though)
1513 ; mapM_ checkTyFamFreeness typats
1515 -- the right-hand side is a tau type
1516 ; checkValidMonoType rhs
1518 -- we have a decidable instance unless otherwise permitted
1519 ; undecidable_ok <- xoptM Opt_UndecidableInstances
1520 ; unless undecidable_ok $
1521 mapM_ addErrTc (checkFamInst typats (tyFamInsts rhs))
1524 -- Make sure that each type family instance is
1525 -- (1) strictly smaller than the lhs,
1526 -- (2) mentions no type variable more often than the lhs, and
1527 -- (3) does not contain any further type family instances.
1529 checkFamInst :: [Type] -- lhs
1530 -> [(TyCon, [Type])] -- type family instances
1532 checkFamInst lhsTys famInsts
1533 = mapCatMaybes check famInsts
1535 size = sizeTypes lhsTys
1536 fvs = fvTypes lhsTys
1538 | not (all isTyFamFree tys)
1539 = Just (famInstUndecErr famInst nestedMsg $$ parens undecidableMsg)
1540 | not (null (fvTypes tys \\ fvs))
1541 = Just (famInstUndecErr famInst nomoreVarMsg $$ parens undecidableMsg)
1542 | size <= sizeTypes tys
1543 = Just (famInstUndecErr famInst smallerAppMsg $$ parens undecidableMsg)
1547 famInst = TyConApp tc tys
1549 -- Ensure that no type family instances occur in a type.
1551 checkTyFamFreeness :: Type -> TcM ()
1552 checkTyFamFreeness ty
1553 = checkTc (isTyFamFree ty) $
1554 tyFamInstIllegalErr ty
1556 -- Check that a type does not contain any type family applications.
1558 isTyFamFree :: Type -> Bool
1559 isTyFamFree = null . tyFamInsts
1563 tyFamInstIllegalErr :: Type -> SDoc
1564 tyFamInstIllegalErr ty
1565 = hang (ptext (sLit "Illegal type synonym family application in instance") <>
1569 famInstUndecErr :: Type -> SDoc -> SDoc
1570 famInstUndecErr ty msg
1572 nest 2 (ptext (sLit "in the type family application:") <+>
1575 nestedMsg, nomoreVarMsg, smallerAppMsg :: SDoc
1576 nestedMsg = ptext (sLit "Nested type family application")
1577 nomoreVarMsg = ptext (sLit "Variable occurs more often than in instance head")
1578 smallerAppMsg = ptext (sLit "Application is no smaller than the instance head")
1582 %************************************************************************
1584 \subsection{Auxiliary functions}
1586 %************************************************************************
1589 -- Free variables of a type, retaining repetitions, and expanding synonyms
1590 fvType :: Type -> [TyVar]
1591 fvType ty | Just exp_ty <- tcView ty = fvType exp_ty
1592 fvType (TyVarTy tv) = [tv]
1593 fvType (TyConApp _ tys) = fvTypes tys
1594 fvType (PredTy pred) = fvPred pred
1595 fvType (FunTy arg res) = fvType arg ++ fvType res
1596 fvType (AppTy fun arg) = fvType fun ++ fvType arg
1597 fvType (ForAllTy tyvar ty) = filter (/= tyvar) (fvType ty)
1599 fvTypes :: [Type] -> [TyVar]
1600 fvTypes tys = concat (map fvType tys)
1602 fvPred :: PredType -> [TyVar]
1603 fvPred (ClassP _ tys') = fvTypes tys'
1604 fvPred (IParam _ ty) = fvType ty
1605 fvPred (EqPred ty1 ty2) = fvType ty1 ++ fvType ty2
1607 -- Size of a type: the number of variables and constructors
1608 sizeType :: Type -> Int
1609 sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty
1610 sizeType (TyVarTy _) = 1
1611 sizeType (TyConApp _ tys) = sizeTypes tys + 1
1612 sizeType (PredTy pred) = sizePred pred
1613 sizeType (FunTy arg res) = sizeType arg + sizeType res + 1
1614 sizeType (AppTy fun arg) = sizeType fun + sizeType arg
1615 sizeType (ForAllTy _ ty) = sizeType ty
1617 sizeTypes :: [Type] -> Int
1618 sizeTypes xs = sum (map sizeType xs)
1620 -- Size of a predicate
1622 -- We are considering whether *class* constraints terminate
1623 -- Once we get into an implicit parameter or equality we
1624 -- can't get back to a class constraint, so it's safe
1625 -- to say "size 0". See Trac #4200.
1626 sizePred :: PredType -> Int
1627 sizePred (ClassP _ tys') = sizeTypes tys'
1628 sizePred (IParam {}) = 0
1629 sizePred (EqPred {}) = 0