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,
23 newMetaTyVar, readMetaTyVar, writeMetaTyVar, writeMetaTyVarRef,
24 isFilledMetaTyVar, isFlexiMetaTyVar,
26 --------------------------------
27 -- Creating new evidence variables
28 newEvVar, newCoVar, newEvVars,
29 writeWantedCoVar, readWantedCoVar,
30 newIP, newDict, newSilentGiven, isSilentEvVar,
32 newWantedEvVar, newWantedEvVars,
33 newTcEvBinds, addTcEvBind,
35 --------------------------------
37 tcInstTyVar, tcInstTyVars, tcInstSigTyVars,
38 tcInstType, instMetaTyVar,
39 tcInstSkolTyVars, tcInstSuperSkolTyVars, tcInstSkolTyVar, tcInstSkolType,
40 tcSkolDFunType, tcSuperSkolTyVars,
42 --------------------------------
43 -- Checking type validity
44 Rank, UserTypeCtxt(..), checkValidType, checkValidMonoType,
45 SourceTyCtxt(..), checkValidTheta,
47 checkValidTypeInst, checkTyFamFreeness,
49 growPredTyVars, growThetaTyVars, validDerivPred,
51 --------------------------------
53 zonkType, mkZonkTcTyVar, zonkTcPredType,
55 skolemiseUnboundMetaTyVar,
56 zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkSigTyVar,
57 zonkQuantifiedTyVar, zonkQuantifiedTyVars,
58 zonkTcType, zonkTcTypes, zonkTcThetaType,
59 zonkTcKindToKind, zonkTcKind,
60 zonkImplication, zonkEvVar, zonkWantedEvVar, zonkFlavoredEvVar,
61 zonkWC, zonkWantedEvVars,
66 readKindVar, writeKindVar
69 #include "HsVersions.h"
81 import HsSyn -- HsType
82 import TcRnMonad -- TcType, amongst others
96 import Unique( Unique )
100 import Data.List ( (\\) )
104 %************************************************************************
108 %************************************************************************
111 newKindVar :: TcM TcKind
112 newKindVar = do { uniq <- newUnique
113 ; ref <- newMutVar Flexi
114 ; return (mkTyVarTy (mkKindVar uniq ref)) }
116 newKindVars :: Int -> TcM [TcKind]
117 newKindVars n = mapM (\ _ -> newKindVar) (nOfThem n ())
121 %************************************************************************
123 Evidence variables; range over constraints we can abstract over
125 %************************************************************************
128 newEvVars :: TcThetaType -> TcM [EvVar]
129 newEvVars theta = mapM newEvVar theta
131 newWantedEvVar :: TcPredType -> TcM EvVar
132 newWantedEvVar (EqPred ty1 ty2) = newCoVar ty1 ty2
133 newWantedEvVar (ClassP cls tys) = newDict cls tys
134 newWantedEvVar (IParam ip ty) = newIP ip ty
136 newWantedEvVars :: TcThetaType -> TcM [EvVar]
137 newWantedEvVars theta = mapM newWantedEvVar theta
140 newEvVar :: TcPredType -> TcM EvVar
141 -- Creates new *rigid* variables for predicates
142 newEvVar (EqPred ty1 ty2) = newCoVar ty1 ty2
143 newEvVar (ClassP cls tys) = newDict cls tys
144 newEvVar (IParam ip ty) = newIP ip ty
146 newCoVar :: TcType -> TcType -> TcM CoVar
148 = do { name <- newName (mkTyVarOccFS (fsLit "co"))
149 ; return (mkCoVar name (mkPredTy (EqPred ty1 ty2))) }
151 newIP :: IPName Name -> TcType -> TcM IpId
153 = do { name <- newName (getOccName (ipNameName ip))
154 ; return (mkLocalId name (mkPredTy (IParam ip ty))) }
156 newDict :: Class -> [TcType] -> TcM DictId
158 = do { name <- newName (mkDictOcc (getOccName cls))
159 ; return (mkLocalId name (mkPredTy (ClassP cls tys))) }
161 newName :: OccName -> TcM Name
163 = do { uniq <- newUnique
165 ; return (mkInternalName uniq occ loc) }
168 newSilentGiven :: PredType -> TcM EvVar
169 -- Make a dictionary for a "silent" given dictionary
170 -- Behaves just like any EvVar except that it responds True to isSilentDict
171 -- This is used only to suppress confusing error reports
172 newSilentGiven (ClassP cls tys)
173 = do { uniq <- newUnique
174 ; let name = mkSystemName uniq (mkDictOcc (getOccName cls))
175 ; return (mkLocalId name (mkPredTy (ClassP cls tys))) }
176 newSilentGiven (EqPred ty1 ty2)
177 = do { uniq <- newUnique
178 ; let name = mkSystemName uniq (mkTyVarOccFS (fsLit "co"))
179 ; return (mkCoVar name (mkPredTy (EqPred ty1 ty2))) }
180 newSilentGiven pred@(IParam {})
181 = pprPanic "newSilentDict" (ppr pred) -- Implicit parameters rejected earlier
183 isSilentEvVar :: EvVar -> Bool
184 isSilentEvVar v = isSystemName (Var.varName v)
185 -- Notice that all *other* evidence variables get Internal Names
189 %************************************************************************
191 SkolemTvs (immutable)
193 %************************************************************************
196 tcInstType :: ([TyVar] -> TcM [TcTyVar]) -- How to instantiate the type variables
197 -> TcType -- Type to instantiate
198 -> TcM ([TcTyVar], TcThetaType, TcType) -- Result
199 -- (type vars (excl coercion vars), preds (incl equalities), rho)
200 tcInstType inst_tyvars ty
201 = case tcSplitForAllTys ty of
202 ([], rho) -> let -- There may be overloading despite no type variables;
203 -- (?x :: Int) => Int -> Int
204 (theta, tau) = tcSplitPhiTy rho
206 return ([], theta, tau)
208 (tyvars, rho) -> do { tyvars' <- inst_tyvars tyvars
210 ; let tenv = zipTopTvSubst tyvars (mkTyVarTys tyvars')
211 -- Either the tyvars are freshly made, by inst_tyvars,
212 -- or any nested foralls have different binders.
213 -- Either way, zipTopTvSubst is ok
215 ; let (theta, tau) = tcSplitPhiTy (substTy tenv rho)
216 ; return (tyvars', theta, tau) }
218 tcSkolDFunType :: Type -> TcM ([TcTyVar], TcThetaType, TcType)
219 -- Instantiate a type signature with skolem constants, but
220 -- do *not* give them fresh names, because we want the name to
221 -- be in the type environment: it is lexically scoped.
222 tcSkolDFunType ty = tcInstType (\tvs -> return (tcSuperSkolTyVars tvs)) ty
224 tcSuperSkolTyVars :: [TyVar] -> [TcTyVar]
225 -- Make skolem constants, but do *not* give them new names, as above
226 -- Moreover, make them "super skolems"; see comments with superSkolemTv
227 tcSuperSkolTyVars tyvars
228 = [ mkTcTyVar (tyVarName tv) (tyVarKind tv) superSkolemTv
231 tcInstSkolTyVar :: Bool -> TyVar -> TcM TcTyVar
232 -- Instantiate the tyvar, using
233 -- * the occ-name and kind of the supplied tyvar,
234 -- * the unique from the monad,
235 -- * the location either from the tyvar (skol_info = SigSkol)
236 -- or from the monad (otherwise)
237 tcInstSkolTyVar overlappable tyvar
238 = do { uniq <- newUnique
240 ; let new_name = mkInternalName uniq occ loc
241 ; return (mkTcTyVar new_name kind (SkolemTv overlappable)) }
243 old_name = tyVarName tyvar
244 occ = nameOccName old_name
245 kind = tyVarKind tyvar
247 tcInstSkolTyVars :: [TyVar] -> TcM [TcTyVar]
248 tcInstSkolTyVars tyvars = mapM (tcInstSkolTyVar False) tyvars
250 tcInstSuperSkolTyVars :: [TyVar] -> TcM [TcTyVar]
251 tcInstSuperSkolTyVars tyvars = mapM (tcInstSkolTyVar True) tyvars
253 tcInstSkolType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType)
254 -- Instantiate a type with fresh skolem constants
255 -- Binding location comes from the monad
256 tcInstSkolType ty = tcInstType tcInstSkolTyVars ty
258 tcInstSigTyVars :: [TyVar] -> TcM [TcTyVar]
259 -- Make meta SigTv type variables for patten-bound scoped type varaibles
260 -- We use SigTvs for them, so that they can't unify with arbitrary types
261 tcInstSigTyVars = mapM (\tv -> instMetaTyVar (SigTv (tyVarName tv)) tv)
262 -- ToDo: the "function binding site is bogus
266 %************************************************************************
268 MetaTvs (meta type variables; mutable)
270 %************************************************************************
273 newMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar
274 -- Make a new meta tyvar out of thin air
275 newMetaTyVar meta_info kind
276 = do { uniq <- newMetaUnique
277 ; ref <- newMutVar Flexi
278 ; let name = mkTcTyVarName uniq s
279 s = case meta_info of
283 ; return (mkTcTyVar name kind (MetaTv meta_info ref)) }
285 mkTcTyVarName :: Unique -> FastString -> Name
286 -- Make sure that fresh TcTyVar names finish with a digit
287 -- leaving the un-cluttered names free for user names
288 mkTcTyVarName uniq str = mkSysTvName uniq str
290 instMetaTyVar :: MetaInfo -> TyVar -> TcM TcTyVar
291 -- Make a new meta tyvar whose Name and Kind
292 -- come from an existing TyVar
293 instMetaTyVar meta_info tyvar
294 = do { uniq <- newMetaUnique
295 ; ref <- newMutVar Flexi
296 ; let name = mkSystemName uniq (getOccName tyvar)
297 kind = tyVarKind tyvar
298 ; return (mkTcTyVar name kind (MetaTv meta_info ref)) }
300 readMetaTyVar :: TyVar -> TcM MetaDetails
301 readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
302 readMutVar (metaTvRef tyvar)
304 readWantedCoVar :: CoVar -> TcM MetaDetails
305 readWantedCoVar covar = ASSERT2( isMetaTyVar covar, ppr covar )
306 readMutVar (metaTvRef covar)
308 isFilledMetaTyVar :: TyVar -> TcM Bool
309 -- True of a filled-in (Indirect) meta type variable
311 | not (isTcTyVar tv) = return False
312 | MetaTv _ ref <- tcTyVarDetails tv
313 = do { details <- readMutVar ref
314 ; return (isIndirect details) }
315 | otherwise = return False
317 isFlexiMetaTyVar :: TyVar -> TcM Bool
318 -- True of a un-filled-in (Flexi) meta type variable
320 | not (isTcTyVar tv) = return False
321 | MetaTv _ ref <- tcTyVarDetails tv
322 = do { details <- readMutVar ref
323 ; return (isFlexi details) }
324 | otherwise = return False
327 writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
328 -- Write into a currently-empty MetaTyVar
330 writeMetaTyVar tyvar ty
332 = writeMetaTyVarRef tyvar (metaTvRef tyvar) ty
334 -- Everything from here on only happens if DEBUG is on
335 | not (isTcTyVar tyvar)
336 = WARN( True, text "Writing to non-tc tyvar" <+> ppr tyvar )
339 | MetaTv _ ref <- tcTyVarDetails tyvar
340 = writeMetaTyVarRef tyvar ref ty
343 = WARN( True, text "Writing to non-meta tyvar" <+> ppr tyvar )
346 writeWantedCoVar :: CoVar -> Coercion -> TcM ()
347 writeWantedCoVar cv co = writeMetaTyVar cv co
350 writeMetaTyVarRef :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM ()
351 -- Here the tyvar is for error checking only;
352 -- the ref cell must be for the same tyvar
353 writeMetaTyVarRef tyvar ref ty
355 = do { traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
356 ; writeMutVar ref (Indirect ty) }
358 -- Everything from here on only happens if DEBUG is on
359 | not (isPredTy tv_kind) -- Don't check kinds for updates to coercion variables
360 , not (ty_kind `isSubKind` tv_kind)
361 = WARN( True, hang (text "Ill-kinded update to meta tyvar")
362 2 (ppr tyvar $$ ppr tv_kind $$ ppr ty $$ ppr ty_kind) )
366 = do { meta_details <- readMutVar ref;
367 ; ASSERT2( isFlexi meta_details,
368 hang (text "Double update of meta tyvar")
369 2 (ppr tyvar $$ ppr meta_details) )
371 traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
372 ; writeMutVar ref (Indirect ty) }
374 tv_kind = tyVarKind tyvar
375 ty_kind = typeKind ty
379 %************************************************************************
383 %************************************************************************
386 newFlexiTyVar :: Kind -> TcM TcTyVar
387 newFlexiTyVar kind = newMetaTyVar TauTv kind
389 newFlexiTyVarTy :: Kind -> TcM TcType
390 newFlexiTyVarTy kind = do
391 tc_tyvar <- newFlexiTyVar kind
392 return (TyVarTy tc_tyvar)
394 newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
395 newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind)
397 tcInstTyVar :: TyVar -> TcM TcTyVar
398 -- Instantiate with a META type variable
399 tcInstTyVar tyvar = instMetaTyVar TauTv tyvar
401 tcInstTyVars :: [TyVar] -> TcM ([TcTyVar], [TcType], TvSubst)
402 -- Instantiate with META type variables
404 = do { tc_tvs <- mapM tcInstTyVar tyvars
405 ; let tys = mkTyVarTys tc_tvs
406 ; return (tc_tvs, tys, zipTopTvSubst tyvars tys) }
407 -- Since the tyvars are freshly made,
408 -- they cannot possibly be captured by
409 -- any existing for-alls. Hence zipTopTvSubst
413 %************************************************************************
417 %************************************************************************
420 zonkSigTyVar :: TcTyVar -> TcM TcTyVar
422 | isSkolemTyVar sig_tv
423 = return sig_tv -- Happens in the call in TcBinds.checkDistinctTyVars
425 = ASSERT( isSigTyVar sig_tv )
426 do { ty <- zonkTcTyVar sig_tv
427 ; return (tcGetTyVar "zonkSigTyVar" ty) }
428 -- 'ty' is bound to be a type variable, because SigTvs
429 -- can only be unified with type variables
434 %************************************************************************
436 \subsection{Zonking -- the exernal interfaces}
438 %************************************************************************
440 @tcGetGlobalTyVars@ returns a fully-zonked set of tyvars free in the environment.
441 To improve subsequent calls to the same function it writes the zonked set back into
445 tcGetGlobalTyVars :: TcM TcTyVarSet
447 = do { (TcLclEnv {tcl_tyvars = gtv_var}) <- getLclEnv
448 ; gbl_tvs <- readMutVar gtv_var
449 ; gbl_tvs' <- zonkTcTyVarsAndFV gbl_tvs
450 ; writeMutVar gtv_var gbl_tvs'
454 ----------------- Type variables
457 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
458 zonkTcTyVars tyvars = mapM zonkTcTyVar tyvars
460 zonkTcTyVarsAndFV :: TcTyVarSet -> TcM TcTyVarSet
461 zonkTcTyVarsAndFV tyvars = tyVarsOfTypes <$> mapM zonkTcTyVar (varSetElems tyvars)
463 ----------------- Types
464 zonkTcTypeCarefully :: TcType -> TcM TcType
465 -- Do not zonk type variables free in the environment
466 zonkTcTypeCarefully ty
467 = do { env_tvs <- tcGetGlobalTyVars
468 ; zonkType (zonk_tv env_tvs) ty }
471 | tv `elemVarSet` env_tvs
472 = return (TyVarTy tv)
474 = ASSERT( isTcTyVar tv )
475 case tcTyVarDetails tv of
476 SkolemTv {} -> return (TyVarTy tv)
477 RuntimeUnk {} -> return (TyVarTy tv)
478 FlatSkol ty -> zonkType (zonk_tv env_tvs) ty
479 MetaTv _ ref -> do { cts <- readMutVar ref
481 Flexi -> return (TyVarTy tv)
482 Indirect ty -> zonkType (zonk_tv env_tvs) ty }
484 zonkTcType :: TcType -> TcM TcType
485 -- Simply look through all Flexis
486 zonkTcType ty = zonkType zonkTcTyVar ty
488 zonkTcTyVar :: TcTyVar -> TcM TcType
489 -- Simply look through all Flexis
491 = ASSERT2( isTcTyVar tv, ppr tv )
492 case tcTyVarDetails tv of
493 SkolemTv {} -> return (TyVarTy tv)
494 RuntimeUnk {} -> return (TyVarTy tv)
495 FlatSkol ty -> zonkTcType ty
496 MetaTv _ ref -> do { cts <- readMutVar ref
498 Flexi -> return (TyVarTy tv)
499 Indirect ty -> zonkTcType ty }
501 zonkTcTypeAndSubst :: TvSubst -> TcType -> TcM TcType
502 -- Zonk, and simultaneously apply a non-necessarily-idempotent substitution
503 zonkTcTypeAndSubst subst ty = zonkType zonk_tv ty
506 = case tcTyVarDetails tv of
507 SkolemTv {} -> return (TyVarTy tv)
508 RuntimeUnk {} -> return (TyVarTy tv)
509 FlatSkol ty -> zonkType zonk_tv ty
510 MetaTv _ ref -> do { cts <- readMutVar ref
512 Flexi -> zonk_flexi tv
513 Indirect ty -> zonkType zonk_tv ty }
515 = case lookupTyVar subst tv of
516 Just ty -> zonkType zonk_tv ty
517 Nothing -> return (TyVarTy tv)
519 zonkTcTypes :: [TcType] -> TcM [TcType]
520 zonkTcTypes tys = mapM zonkTcType tys
522 zonkTcThetaType :: TcThetaType -> TcM TcThetaType
523 zonkTcThetaType theta = mapM zonkTcPredType theta
525 zonkTcPredType :: TcPredType -> TcM TcPredType
526 zonkTcPredType (ClassP c ts) = ClassP c <$> zonkTcTypes ts
527 zonkTcPredType (IParam n t) = IParam n <$> zonkTcType t
528 zonkTcPredType (EqPred t1 t2) = EqPred <$> zonkTcType t1 <*> zonkTcType t2
531 ------------------- These ...ToType, ...ToKind versions
532 are used at the end of type checking
535 zonkQuantifiedTyVars :: [TcTyVar] -> TcM [TcTyVar]
536 zonkQuantifiedTyVars = mapM zonkQuantifiedTyVar
538 zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar
539 -- The quantified type variables often include meta type variables
540 -- we want to freeze them into ordinary type variables, and
541 -- default their kind (e.g. from OpenTypeKind to TypeKind)
542 -- -- see notes with Kind.defaultKind
543 -- The meta tyvar is updated to point to the new skolem TyVar. Now any
544 -- bound occurences of the original type variable will get zonked to
545 -- the immutable version.
547 -- We leave skolem TyVars alone; they are immutable.
548 zonkQuantifiedTyVar tv
549 = ASSERT2( isTcTyVar tv, ppr tv )
550 case tcTyVarDetails tv of
551 SkolemTv {} -> WARN( True, ppr tv ) -- Dec10: Can this really happen?
552 do { kind <- zonkTcType (tyVarKind tv)
553 ; return $ setTyVarKind tv kind }
554 -- It might be a skolem type variable,
555 -- for example from a user type signature
559 -- [Sept 04] Check for non-empty.
560 -- See note [Silly Type Synonym]
561 (readMutVar _ref >>= \cts ->
564 Indirect ty -> WARN( True, ppr tv $$ ppr ty )
567 skolemiseUnboundMetaTyVar tv vanillaSkolemTv
568 _other -> pprPanic "zonkQuantifiedTyVar" (ppr tv) -- FlatSkol, RuntimeUnk
570 skolemiseUnboundMetaTyVar :: TcTyVar -> TcTyVarDetails -> 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 tv details
577 = ASSERT2( isMetaTyVar tv, ppr tv )
578 do { span <- getSrcSpanM -- Get the location from "here"
579 -- ie where we are generalising
580 ; uniq <- newUnique -- Remove it from TcMetaTyVar unique land
581 ; let final_kind = defaultKind (tyVarKind tv)
582 final_name = mkInternalName uniq (getOccName tv) span
583 final_tv = mkTcTyVar final_name final_kind details
584 ; writeMetaTyVar tv (mkTyVarTy final_tv)
589 zonkImplication :: Implication -> TcM Implication
590 zonkImplication implic@(Implic { ic_given = given
593 = do { -- No need to zonk the skolems
594 ; given' <- mapM zonkEvVar given
595 ; loc' <- zonkGivenLoc loc
596 ; wanted' <- zonkWC wanted
597 ; return (implic { ic_given = given'
598 , ic_wanted = wanted'
601 zonkEvVar :: EvVar -> TcM EvVar
602 zonkEvVar var = do { ty' <- zonkTcType (varType var)
603 ; return (setVarType var ty') }
605 zonkFlavoredEvVar :: FlavoredEvVar -> TcM FlavoredEvVar
606 zonkFlavoredEvVar (EvVarX ev fl)
607 = do { ev' <- zonkEvVar ev
608 ; fl' <- zonkFlavor fl
609 ; return (EvVarX ev' fl') }
611 zonkWC :: WantedConstraints -> TcM WantedConstraints
612 zonkWC (WC { wc_flat = flat, wc_impl = implic, wc_insol = insol })
613 = do { flat' <- zonkWantedEvVars flat
614 ; implic' <- mapBagM zonkImplication implic
615 ; insol' <- mapBagM zonkFlavoredEvVar insol
616 ; return (WC { wc_flat = flat', wc_impl = implic', wc_insol = insol' }) }
618 zonkWantedEvVars :: Bag WantedEvVar -> TcM (Bag WantedEvVar)
619 zonkWantedEvVars = mapBagM zonkWantedEvVar
621 zonkWantedEvVar :: WantedEvVar -> TcM WantedEvVar
622 zonkWantedEvVar (EvVarX v l) = do { v' <- zonkEvVar v; return (EvVarX v' l) }
624 zonkFlavor :: CtFlavor -> TcM CtFlavor
625 zonkFlavor (Given loc) = do { loc' <- zonkGivenLoc loc; return (Given loc') }
626 zonkFlavor fl = return fl
628 zonkGivenLoc :: GivenLoc -> TcM GivenLoc
629 -- GivenLocs may have unification variables inside them!
630 zonkGivenLoc (CtLoc skol_info span ctxt)
631 = do { skol_info' <- zonkSkolemInfo skol_info
632 ; return (CtLoc skol_info' span ctxt) }
634 zonkSkolemInfo :: SkolemInfo -> TcM SkolemInfo
635 zonkSkolemInfo (SigSkol cx ty) = do { ty' <- zonkTcType ty
636 ; return (SigSkol cx ty') }
637 zonkSkolemInfo (InferSkol ntys) = do { ntys' <- mapM do_one ntys
638 ; return (InferSkol ntys') }
640 do_one (n, ty) = do { ty' <- zonkTcType ty; return (n, ty') }
641 zonkSkolemInfo skol_info = return skol_info
644 Note [Silly Type Synonyms]
645 ~~~~~~~~~~~~~~~~~~~~~~~~~~
647 type C u a = u -- Note 'a' unused
649 foo :: (forall a. C u a -> C u a) -> u
653 bar = foo (\t -> t + t)
655 * From the (\t -> t+t) we get type {Num d} => d -> d
658 * Now unify with type of foo's arg, and we get:
659 {Num (C d a)} => C d a -> C d a
662 * Now abstract over the 'a', but float out the Num (C d a) constraint
663 because it does not 'really' mention a. (see exactTyVarsOfType)
664 The arg to foo becomes
667 * So we get a dict binding for Num (C d a), which is zonked to give
669 [Note Sept 04: now that we are zonking quantified type variables
670 on construction, the 'a' will be frozen as a regular tyvar on
671 quantification, so the floated dict will still have type (C d a).
672 Which renders this whole note moot; happily!]
674 * Then the \/\a abstraction has a zonked 'a' in it.
676 All very silly. I think its harmless to ignore the problem. We'll end up with
677 a \/\a in the final result but all the occurrences of a will be zonked to ()
679 Note [Zonking to Skolem]
680 ~~~~~~~~~~~~~~~~~~~~~~~~
681 We used to zonk quantified type variables to regular TyVars. However, this
682 leads to problems. Consider this program from the regression test suite:
684 eval :: Int -> String -> String -> String
685 eval 0 root actual = evalRHS 0 root actual
688 evalRHS 0 root actual = eval 0 root actual
690 It leads to the deferral of an equality (wrapped in an implication constraint)
692 forall a. (String -> String -> String) ~ a
694 which is propagated up to the toplevel (see TcSimplify.tcSimplifyInferCheck).
695 In the meantime `a' is zonked and quantified to form `evalRHS's signature.
696 This has the *side effect* of also zonking the `a' in the deferred equality
697 (which at this point is being handed around wrapped in an implication
700 Finally, the equality (with the zonked `a') will be handed back to the
701 simplifier by TcRnDriver.tcRnSrcDecls calling TcSimplify.tcSimplifyTop.
702 If we zonk `a' with a regular type variable, we will have this regular type
703 variable now floating around in the simplifier, which in many places assumes to
704 only see proper TcTyVars.
706 We can avoid this problem by zonking with a skolem. The skolem is rigid
707 (which we require for a quantified variable), but is still a TcTyVar that the
708 simplifier knows how to deal with.
711 %************************************************************************
713 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
715 %* For internal use only! *
717 %************************************************************************
720 -- For unbound, mutable tyvars, zonkType uses the function given to it
721 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
722 -- type variable and zonks the kind too
724 zonkType :: (TcTyVar -> TcM Type) -- What to do with TcTyVars
725 -> TcType -> TcM Type
726 zonkType zonk_tc_tyvar ty
729 go (TyConApp tc tys) = do tys' <- mapM go tys
730 return (TyConApp tc tys')
732 go (PredTy p) = do p' <- go_pred p
735 go (FunTy arg res) = do arg' <- go arg
737 return (FunTy arg' res')
739 go (AppTy fun arg) = do fun' <- go fun
741 return (mkAppTy fun' arg')
742 -- NB the mkAppTy; we might have instantiated a
743 -- type variable to a type constructor, so we need
744 -- to pull the TyConApp to the top.
746 -- The two interesting cases!
747 go (TyVarTy tyvar) | isTcTyVar tyvar = zonk_tc_tyvar tyvar
748 | otherwise = liftM TyVarTy $
749 zonkTyVar zonk_tc_tyvar tyvar
750 -- Ordinary (non Tc) tyvars occur inside quantified types
752 go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar ) do
754 tyvar' <- zonkTyVar zonk_tc_tyvar tyvar
755 return (ForAllTy tyvar' ty')
757 go_pred (ClassP c tys) = do tys' <- mapM go tys
758 return (ClassP c tys')
759 go_pred (IParam n ty) = do ty' <- go ty
760 return (IParam n ty')
761 go_pred (EqPred ty1 ty2) = do ty1' <- go ty1
763 return (EqPred ty1' ty2')
765 mkZonkTcTyVar :: (TcTyVar -> TcM Type) -- What to do for an *mutable Flexi* var
766 -> TcTyVar -> TcM TcType
767 mkZonkTcTyVar unbound_var_fn tyvar
768 = ASSERT( isTcTyVar tyvar )
769 case tcTyVarDetails tyvar of
770 SkolemTv {} -> return (TyVarTy tyvar)
771 RuntimeUnk {} -> return (TyVarTy tyvar)
772 FlatSkol ty -> zonkType (mkZonkTcTyVar unbound_var_fn) ty
773 MetaTv _ ref -> do { cts <- readMutVar ref
775 Flexi -> unbound_var_fn tyvar
776 Indirect ty -> zonkType (mkZonkTcTyVar unbound_var_fn) ty }
778 -- Zonk the kind of a non-TC tyvar in case it is a coercion variable
779 -- (their kind contains types).
780 zonkTyVar :: (TcTyVar -> TcM Type) -- What to do for a TcTyVar
781 -> TyVar -> TcM TyVar
782 zonkTyVar zonk_tc_tyvar tv
784 = do { kind <- zonkType zonk_tc_tyvar (tyVarKind tv)
785 ; return $ setTyVarKind tv kind }
786 | otherwise = return tv
791 %************************************************************************
795 %************************************************************************
798 readKindVar :: KindVar -> TcM (MetaDetails)
799 writeKindVar :: KindVar -> TcKind -> TcM ()
800 readKindVar kv = readMutVar (kindVarRef kv)
801 writeKindVar kv val = writeMutVar (kindVarRef kv) (Indirect val)
804 zonkTcKind :: TcKind -> TcM TcKind
805 zonkTcKind k = zonkTcType k
808 zonkTcKindToKind :: TcKind -> TcM Kind
809 -- When zonking a TcKind to a kind, we need to instantiate kind variables,
810 -- Haskell specifies that * is to be used, so we follow that.
812 = zonkType (mkZonkTcTyVar (\ _ -> return liftedTypeKind)) k
815 %************************************************************************
817 \subsection{Checking a user type}
819 %************************************************************************
821 When dealing with a user-written type, we first translate it from an HsType
822 to a Type, performing kind checking, and then check various things that should
823 be true about it. We don't want to perform these checks at the same time
824 as the initial translation because (a) they are unnecessary for interface-file
825 types and (b) when checking a mutually recursive group of type and class decls,
826 we can't "look" at the tycons/classes yet. Also, the checks are are rather
827 diverse, and used to really mess up the other code.
829 One thing we check for is 'rank'.
831 Rank 0: monotypes (no foralls)
832 Rank 1: foralls at the front only, Rank 0 inside
833 Rank 2: foralls at the front, Rank 1 on left of fn arrow,
835 basic ::= tyvar | T basic ... basic
837 r2 ::= forall tvs. cxt => r2a
838 r2a ::= r1 -> r2a | basic
839 r1 ::= forall tvs. cxt => r0
840 r0 ::= r0 -> r0 | basic
842 Another thing is to check that type synonyms are saturated.
843 This might not necessarily show up in kind checking.
845 data T k = MkT (k Int)
850 checkValidType :: UserTypeCtxt -> Type -> TcM ()
851 -- Checks that the type is valid for the given context
852 checkValidType ctxt ty = do
853 traceTc "checkValidType" (ppr ty)
854 unboxed <- xoptM Opt_UnboxedTuples
855 rank2 <- xoptM Opt_Rank2Types
856 rankn <- xoptM Opt_RankNTypes
857 polycomp <- xoptM Opt_PolymorphicComponents
859 gen_rank n | rankn = ArbitraryRank
864 DefaultDeclCtxt-> MustBeMonoType
865 ResSigCtxt -> MustBeMonoType
866 LamPatSigCtxt -> gen_rank 0
867 BindPatSigCtxt -> gen_rank 0
868 TySynCtxt _ -> gen_rank 0
869 GenPatCtxt -> gen_rank 1
870 -- This one is a bit of a hack
871 -- See the forall-wrapping in TcClassDcl.mkGenericInstance
873 ExprSigCtxt -> gen_rank 1
874 FunSigCtxt _ -> gen_rank 1
875 ConArgCtxt _ | polycomp -> gen_rank 2
876 -- We are given the type of the entire
877 -- constructor, hence rank 1
878 | otherwise -> gen_rank 1
880 ForSigCtxt _ -> gen_rank 1
881 SpecInstCtxt -> gen_rank 1
882 ThBrackCtxt -> gen_rank 1
883 GenSigCtxt -> panic "checkValidType"
884 -- Can't happen; GenSigCtxt not used for *user* sigs
886 actual_kind = typeKind ty
888 kind_ok = case ctxt of
889 TySynCtxt _ -> True -- Any kind will do
890 ThBrackCtxt -> True -- Any kind will do
891 ResSigCtxt -> isSubOpenTypeKind actual_kind
892 ExprSigCtxt -> isSubOpenTypeKind actual_kind
893 GenPatCtxt -> isLiftedTypeKind actual_kind
894 ForSigCtxt _ -> isLiftedTypeKind actual_kind
895 _ -> isSubArgTypeKind actual_kind
897 ubx_tup = case ctxt of
898 TySynCtxt _ | unboxed -> UT_Ok
899 ExprSigCtxt | unboxed -> UT_Ok
900 ThBrackCtxt | unboxed -> UT_Ok
903 -- Check the internal validity of the type itself
904 check_type rank ubx_tup ty
906 -- Check that the thing has kind Type, and is lifted if necessary
907 -- Do this second, becuase we can't usefully take the kind of an
908 -- ill-formed type such as (a~Int)
909 checkTc kind_ok (kindErr actual_kind)
911 traceTc "checkValidType done" (ppr ty)
913 checkValidMonoType :: Type -> TcM ()
914 checkValidMonoType ty = check_mono_type MustBeMonoType ty
919 data Rank = ArbitraryRank -- Any rank ok
920 | MustBeMonoType -- Monotype regardless of flags
921 | TyConArgMonoType -- Monotype but could be poly if -XImpredicativeTypes
922 | SynArgMonoType -- Monotype but could be poly if -XLiberalTypeSynonyms
923 | Rank Int -- Rank n, but could be more with -XRankNTypes
925 decRank :: Rank -> Rank -- Function arguments
926 decRank (Rank 0) = Rank 0
927 decRank (Rank n) = Rank (n-1)
928 decRank other_rank = other_rank
930 nonZeroRank :: Rank -> Bool
931 nonZeroRank ArbitraryRank = True
932 nonZeroRank (Rank n) = n>0
933 nonZeroRank _ = False
935 ----------------------------------------
936 data UbxTupFlag = UT_Ok | UT_NotOk
937 -- The "Ok" version means "ok if UnboxedTuples is on"
939 ----------------------------------------
940 check_mono_type :: Rank -> Type -> TcM () -- No foralls anywhere
941 -- No unlifted types of any kind
942 check_mono_type rank ty
943 = do { check_type rank UT_NotOk ty
944 ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
946 check_type :: Rank -> UbxTupFlag -> Type -> TcM ()
947 -- The args say what the *type context* requires, independent
948 -- of *flag* settings. You test the flag settings at usage sites.
950 -- Rank is allowed rank for function args
951 -- Rank 0 means no for-alls anywhere
953 check_type rank ubx_tup ty
954 | not (null tvs && null theta)
955 = do { checkTc (nonZeroRank rank) (forAllTyErr rank ty)
956 -- Reject e.g. (Maybe (?x::Int => Int)),
957 -- with a decent error message
958 ; check_valid_theta SigmaCtxt theta
959 ; check_type rank ubx_tup tau -- Allow foralls to right of arrow
960 ; checkAmbiguity tvs theta (tyVarsOfType tau) }
962 (tvs, theta, tau) = tcSplitSigmaTy ty
964 -- Naked PredTys should, I think, have been rejected before now
965 check_type _ _ ty@(PredTy {})
966 = failWithTc (text "Predicate" <+> ppr ty <+> text "used as a type")
968 check_type _ _ (TyVarTy _) = return ()
970 check_type rank _ (FunTy arg_ty res_ty)
971 = do { check_type (decRank rank) UT_NotOk arg_ty
972 ; check_type rank UT_Ok res_ty }
974 check_type rank _ (AppTy ty1 ty2)
975 = do { check_arg_type rank ty1
976 ; check_arg_type rank ty2 }
978 check_type rank ubx_tup ty@(TyConApp tc tys)
980 = do { -- Check that the synonym has enough args
981 -- This applies equally to open and closed synonyms
982 -- It's OK to have an *over-applied* type synonym
983 -- data Tree a b = ...
984 -- type Foo a = Tree [a]
985 -- f :: Foo a b -> ...
986 checkTc (tyConArity tc <= length tys) arity_msg
988 -- See Note [Liberal type synonyms]
989 ; liberal <- xoptM Opt_LiberalTypeSynonyms
990 ; if not liberal || isSynFamilyTyCon tc then
991 -- For H98 and synonym families, do check the type args
992 mapM_ (check_mono_type SynArgMonoType) tys
994 else -- In the liberal case (only for closed syns), expand then check
996 Just ty' -> check_type rank ubx_tup ty'
997 Nothing -> pprPanic "check_tau_type" (ppr ty)
1000 | isUnboxedTupleTyCon tc
1001 = do { ub_tuples_allowed <- xoptM Opt_UnboxedTuples
1002 ; checkTc (ubx_tup_ok ub_tuples_allowed) ubx_tup_msg
1004 ; impred <- xoptM Opt_ImpredicativeTypes
1005 ; let rank' = if impred then ArbitraryRank else TyConArgMonoType
1006 -- c.f. check_arg_type
1007 -- However, args are allowed to be unlifted, or
1008 -- more unboxed tuples, so can't use check_arg_ty
1009 ; mapM_ (check_type rank' UT_Ok) tys }
1012 = mapM_ (check_arg_type rank) tys
1015 ubx_tup_ok ub_tuples_allowed = case ubx_tup of
1016 UT_Ok -> ub_tuples_allowed
1020 tc_arity = tyConArity tc
1022 arity_msg = arityErr "Type synonym" (tyConName tc) tc_arity n_args
1023 ubx_tup_msg = ubxArgTyErr ty
1025 check_type _ _ ty = pprPanic "check_type" (ppr ty)
1027 ----------------------------------------
1028 check_arg_type :: Rank -> Type -> TcM ()
1029 -- The sort of type that can instantiate a type variable,
1030 -- or be the argument of a type constructor.
1031 -- Not an unboxed tuple, but now *can* be a forall (since impredicativity)
1032 -- Other unboxed types are very occasionally allowed as type
1033 -- arguments depending on the kind of the type constructor
1035 -- For example, we want to reject things like:
1037 -- instance Ord a => Ord (forall s. T s a)
1039 -- g :: T s (forall b.b)
1041 -- NB: unboxed tuples can have polymorphic or unboxed args.
1042 -- This happens in the workers for functions returning
1043 -- product types with polymorphic components.
1044 -- But not in user code.
1045 -- Anyway, they are dealt with by a special case in check_tau_type
1047 check_arg_type rank ty
1048 = do { impred <- xoptM Opt_ImpredicativeTypes
1049 ; let rank' = case rank of -- Predictive => must be monotype
1050 MustBeMonoType -> MustBeMonoType -- Monotype, regardless
1051 _other | impred -> ArbitraryRank
1052 | otherwise -> TyConArgMonoType
1053 -- Make sure that MustBeMonoType is propagated,
1054 -- so that we don't suggest -XImpredicativeTypes in
1055 -- (Ord (forall a.a)) => a -> a
1056 -- and so that if it Must be a monotype, we check that it is!
1058 ; check_type rank' UT_NotOk ty
1059 ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
1061 ----------------------------------------
1062 forAllTyErr :: Rank -> Type -> SDoc
1064 = vcat [ hang (ptext (sLit "Illegal polymorphic or qualified type:")) 2 (ppr ty)
1067 suggestion = case rank of
1068 Rank _ -> ptext (sLit "Perhaps you intended to use -XRankNTypes or -XRank2Types")
1069 TyConArgMonoType -> ptext (sLit "Perhaps you intended to use -XImpredicativeTypes")
1070 SynArgMonoType -> ptext (sLit "Perhaps you intended to use -XLiberalTypeSynonyms")
1071 _ -> empty -- Polytype is always illegal
1073 unliftedArgErr, ubxArgTyErr :: Type -> SDoc
1074 unliftedArgErr ty = sep [ptext (sLit "Illegal unlifted type:"), ppr ty]
1075 ubxArgTyErr ty = sep [ptext (sLit "Illegal unboxed tuple type as function argument:"), ppr ty]
1077 kindErr :: Kind -> SDoc
1078 kindErr kind = sep [ptext (sLit "Expecting an ordinary type, but found a type of kind"), ppr kind]
1081 Note [Liberal type synonyms]
1082 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1083 If -XLiberalTypeSynonyms is on, expand closed type synonyms *before*
1084 doing validity checking. This allows us to instantiate a synonym defn
1085 with a for-all type, or with a partially-applied type synonym.
1089 Here, T is partially applied, so it's illegal in H98. But if you
1090 expand S first, then T we get just
1094 IMPORTANT: suppose T is a type synonym. Then we must do validity
1095 checking on an appliation (T ty1 ty2)
1097 *either* before expansion (i.e. check ty1, ty2)
1098 *or* after expansion (i.e. expand T ty1 ty2, and then check)
1101 If we do both, we get exponential behaviour!!
1103 data TIACons1 i r c = c i ::: r c
1104 type TIACons2 t x = TIACons1 t (TIACons1 t x)
1105 type TIACons3 t x = TIACons2 t (TIACons1 t x)
1106 type TIACons4 t x = TIACons2 t (TIACons2 t x)
1107 type TIACons7 t x = TIACons4 t (TIACons3 t x)
1110 %************************************************************************
1112 \subsection{Checking a theta or source type}
1114 %************************************************************************
1117 -- Enumerate the contexts in which a "source type", <S>, can occur
1121 -- or (N a) where N is a newtype
1124 = ClassSCCtxt Name -- Superclasses of clas
1125 -- class <S> => C a where ...
1126 | SigmaCtxt -- Theta part of a normal for-all type
1127 -- f :: <S> => a -> a
1128 | DataTyCtxt Name -- Theta part of a data decl
1129 -- data <S> => T a = MkT a
1130 | TypeCtxt -- Source type in an ordinary type
1132 | InstThetaCtxt -- Context of an instance decl
1133 -- instance <S> => C [a] where ...
1135 pprSourceTyCtxt :: SourceTyCtxt -> SDoc
1136 pprSourceTyCtxt (ClassSCCtxt c) = ptext (sLit "the super-classes of class") <+> quotes (ppr c)
1137 pprSourceTyCtxt SigmaCtxt = ptext (sLit "the context of a polymorphic type")
1138 pprSourceTyCtxt (DataTyCtxt tc) = ptext (sLit "the context of the data type declaration for") <+> quotes (ppr tc)
1139 pprSourceTyCtxt InstThetaCtxt = ptext (sLit "the context of an instance declaration")
1140 pprSourceTyCtxt TypeCtxt = ptext (sLit "the context of a type")
1144 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
1145 checkValidTheta ctxt theta
1146 = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
1148 -------------------------
1149 check_valid_theta :: SourceTyCtxt -> [PredType] -> TcM ()
1150 check_valid_theta _ []
1152 check_valid_theta ctxt theta = do
1154 warnTc (notNull dups) (dupPredWarn dups)
1155 mapM_ (check_pred_ty dflags ctxt) theta
1157 (_,dups) = removeDups tcCmpPred theta
1159 -------------------------
1160 check_pred_ty :: DynFlags -> SourceTyCtxt -> PredType -> TcM ()
1161 check_pred_ty dflags ctxt pred@(ClassP cls tys)
1162 = do { -- Class predicates are valid in all contexts
1163 ; checkTc (arity == n_tys) arity_err
1165 -- Check the form of the argument types
1166 ; mapM_ checkValidMonoType tys
1167 ; checkTc (check_class_pred_tys dflags ctxt tys)
1168 (predTyVarErr pred $$ how_to_allow)
1171 class_name = className cls
1172 arity = classArity cls
1174 arity_err = arityErr "Class" class_name arity n_tys
1175 how_to_allow = parens (ptext (sLit "Use -XFlexibleContexts to permit this"))
1178 check_pred_ty dflags ctxt pred@(EqPred ty1 ty2)
1179 = do { -- Equational constraints are valid in all contexts if type
1180 -- families are permitted
1181 ; checkTc (xopt Opt_TypeFamilies dflags) (eqPredTyErr pred)
1182 ; checkTc (case ctxt of ClassSCCtxt {} -> False; _ -> True)
1183 (eqSuperClassErr pred)
1185 -- Check the form of the argument types
1186 ; checkValidMonoType ty1
1187 ; checkValidMonoType ty2
1190 check_pred_ty _ SigmaCtxt (IParam _ ty) = checkValidMonoType ty
1191 -- Implicit parameters only allowed in type
1192 -- signatures; not in instance decls, superclasses etc
1193 -- The reason for not allowing implicit params in instances is a bit
1195 -- If we allowed instance (?x::Int, Eq a) => Foo [a] where ...
1196 -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
1197 -- discharge all the potential usas of the ?x in e. For example, a
1198 -- constraint Foo [Int] might come out of e,and applying the
1199 -- instance decl would show up two uses of ?x.
1202 check_pred_ty _ _ sty = failWithTc (badPredTyErr sty)
1204 -------------------------
1205 check_class_pred_tys :: DynFlags -> SourceTyCtxt -> [Type] -> Bool
1206 check_class_pred_tys dflags ctxt tys
1208 TypeCtxt -> True -- {-# SPECIALISE instance Eq (T Int) #-} is fine
1209 InstThetaCtxt -> flexible_contexts || undecidable_ok || all tcIsTyVarTy tys
1210 -- Further checks on head and theta in
1211 -- checkInstTermination
1212 _ -> flexible_contexts || all tyvar_head tys
1214 flexible_contexts = xopt Opt_FlexibleContexts dflags
1215 undecidable_ok = xopt Opt_UndecidableInstances dflags
1217 -------------------------
1218 tyvar_head :: Type -> Bool
1219 tyvar_head ty -- Haskell 98 allows predicates of form
1220 | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
1221 | otherwise -- where a is a type variable
1222 = case tcSplitAppTy_maybe ty of
1223 Just (ty, _) -> tyvar_head ty
1230 is ambiguous if P contains generic variables
1231 (i.e. one of the Vs) that are not mentioned in tau
1233 However, we need to take account of functional dependencies
1234 when we speak of 'mentioned in tau'. Example:
1235 class C a b | a -> b where ...
1237 forall x y. (C x y) => x
1238 is not ambiguous because x is mentioned and x determines y
1240 NB; the ambiguity check is only used for *user* types, not for types
1241 coming from inteface files. The latter can legitimately have
1242 ambiguous types. Example
1244 class S a where s :: a -> (Int,Int)
1245 instance S Char where s _ = (1,1)
1246 f:: S a => [a] -> Int -> (Int,Int)
1247 f (_::[a]) x = (a*x,b)
1248 where (a,b) = s (undefined::a)
1250 Here the worker for f gets the type
1251 fw :: forall a. S a => Int -> (# Int, Int #)
1253 If the list of tv_names is empty, we have a monotype, and then we
1254 don't need to check for ambiguity either, because the test can't fail
1257 In addition, GHC insists that at least one type variable
1258 in each constraint is in V. So we disallow a type like
1259 forall a. Eq b => b -> b
1260 even in a scope where b is in scope.
1263 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
1264 checkAmbiguity forall_tyvars theta tau_tyvars
1265 = mapM_ complain (filter is_ambig theta)
1267 complain pred = addErrTc (ambigErr pred)
1268 extended_tau_vars = growThetaTyVars theta tau_tyvars
1270 -- See Note [Implicit parameters and ambiguity] in TcSimplify
1271 is_ambig pred = isClassPred pred &&
1272 any ambig_var (varSetElems (tyVarsOfPred pred))
1274 ambig_var ct_var = (ct_var `elem` forall_tyvars) &&
1275 not (ct_var `elemVarSet` extended_tau_vars)
1277 ambigErr :: PredType -> SDoc
1279 = sep [ptext (sLit "Ambiguous constraint") <+> quotes (pprPred pred),
1280 nest 2 (ptext (sLit "At least one of the forall'd type variables mentioned by the constraint") $$
1281 ptext (sLit "must be reachable from the type after the '=>'"))]
1284 Note [Growing the tau-tvs using constraints]
1285 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1286 (growInstsTyVars insts tvs) is the result of extending the set
1287 of tyvars tvs using all conceivable links from pred
1289 E.g. tvs = {a}, preds = {H [a] b, K (b,Int) c, Eq e}
1290 Then grow precs tvs = {a,b,c}
1293 growThetaTyVars :: TcThetaType -> TyVarSet -> TyVarSet
1294 -- See Note [Growing the tau-tvs using constraints]
1295 growThetaTyVars theta tvs
1297 | otherwise = fixVarSet mk_next tvs
1299 mk_next tvs = foldr grow_one tvs theta
1300 grow_one pred tvs = growPredTyVars pred tvs `unionVarSet` tvs
1302 growPredTyVars :: TcPredType
1303 -> TyVarSet -- The set to extend
1304 -> TyVarSet -- TyVars of the predicate if it intersects
1305 -- the set, or is implicit parameter
1306 growPredTyVars pred tvs
1307 | IParam {} <- pred = pred_tvs -- See Note [Implicit parameters and ambiguity]
1308 | pred_tvs `intersectsVarSet` tvs = pred_tvs
1309 | otherwise = emptyVarSet
1311 pred_tvs = tyVarsOfPred pred
1314 Note [Implicit parameters and ambiguity]
1315 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1316 Only a *class* predicate can give rise to ambiguity
1317 An *implicit parameter* cannot. For example:
1318 foo :: (?x :: [a]) => Int
1320 is fine. The call site will suppply a particular 'x'
1322 Furthermore, the type variables fixed by an implicit parameter
1323 propagate to the others. E.g.
1324 foo :: (Show a, ?x::[a]) => Int
1326 The type of foo looks ambiguous. But it isn't, because at a call site
1328 let ?x = 5::Int in foo
1329 and all is well. In effect, implicit parameters are, well, parameters,
1330 so we can take their type variables into account as part of the
1331 "tau-tvs" stuff. This is done in the function 'FunDeps.grow'.
1335 checkThetaCtxt :: SourceTyCtxt -> ThetaType -> SDoc
1336 checkThetaCtxt ctxt theta
1337 = vcat [ptext (sLit "In the context:") <+> pprTheta theta,
1338 ptext (sLit "While checking") <+> pprSourceTyCtxt ctxt ]
1340 eqSuperClassErr :: PredType -> SDoc
1341 eqSuperClassErr pred
1342 = hang (ptext (sLit "Alas, GHC 7.0 still cannot handle equality superclasses:"))
1345 badPredTyErr, eqPredTyErr, predTyVarErr :: PredType -> SDoc
1346 badPredTyErr pred = ptext (sLit "Illegal constraint") <+> pprPred pred
1347 eqPredTyErr pred = ptext (sLit "Illegal equational constraint") <+> pprPred pred
1349 parens (ptext (sLit "Use -XTypeFamilies to permit this"))
1350 predTyVarErr pred = sep [ptext (sLit "Non type-variable argument"),
1351 nest 2 (ptext (sLit "in the constraint:") <+> pprPred pred)]
1352 dupPredWarn :: [[PredType]] -> SDoc
1353 dupPredWarn dups = ptext (sLit "Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
1355 arityErr :: Outputable a => String -> a -> Int -> Int -> SDoc
1356 arityErr kind name n m
1357 = hsep [ text kind, quotes (ppr name), ptext (sLit "should have"),
1358 n_arguments <> comma, text "but has been given",
1359 if m==0 then text "none" else int m]
1361 n_arguments | n == 0 = ptext (sLit "no arguments")
1362 | n == 1 = ptext (sLit "1 argument")
1363 | True = hsep [int n, ptext (sLit "arguments")]
1366 %************************************************************************
1368 \subsection{Checking for a decent instance head type}
1370 %************************************************************************
1372 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1373 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1375 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1376 flag is on, or (2)~the instance is imported (they must have been
1377 compiled elsewhere). In these cases, we let them go through anyway.
1379 We can also have instances for functions: @instance Foo (a -> b) ...@.
1382 checkValidInstHead :: Class -> [Type] -> TcM ()
1383 checkValidInstHead clas tys
1384 = do { dflags <- getDOpts
1386 -- If GlasgowExts then check at least one isn't a type variable
1387 ; checkTc (xopt Opt_TypeSynonymInstances dflags ||
1388 all tcInstHeadTyNotSynonym tys)
1389 (instTypeErr pp_pred head_type_synonym_msg)
1390 ; checkTc (xopt Opt_FlexibleInstances dflags ||
1391 all tcInstHeadTyAppAllTyVars tys)
1392 (instTypeErr pp_pred head_type_args_tyvars_msg)
1393 ; checkTc (xopt Opt_MultiParamTypeClasses dflags ||
1395 (instTypeErr pp_pred head_one_type_msg)
1396 -- May not contain type family applications
1397 ; mapM_ checkTyFamFreeness tys
1399 ; mapM_ checkValidMonoType tys
1400 -- For now, I only allow tau-types (not polytypes) in
1401 -- the head of an instance decl.
1402 -- E.g. instance C (forall a. a->a) is rejected
1403 -- One could imagine generalising that, but I'm not sure
1404 -- what all the consequences might be
1408 pp_pred = pprClassPred clas tys
1409 head_type_synonym_msg = parens (
1410 text "All instance types must be of the form (T t1 ... tn)" $$
1411 text "where T is not a synonym." $$
1412 text "Use -XTypeSynonymInstances if you want to disable this.")
1414 head_type_args_tyvars_msg = parens (vcat [
1415 text "All instance types must be of the form (T a1 ... an)",
1416 text "where a1 ... an are *distinct type variables*,",
1417 text "and each type variable appears at most once in the instance head.",
1418 text "Use -XFlexibleInstances if you want to disable this."])
1420 head_one_type_msg = parens (
1421 text "Only one type can be given in an instance head." $$
1422 text "Use -XMultiParamTypeClasses if you want to allow more.")
1424 instTypeErr :: SDoc -> SDoc -> SDoc
1425 instTypeErr pp_ty msg
1426 = sep [ptext (sLit "Illegal instance declaration for") <+> quotes pp_ty,
1431 %************************************************************************
1433 \subsection{Checking instance for termination}
1435 %************************************************************************
1438 checkValidInstance :: LHsType Name -> [TyVar] -> ThetaType
1439 -> Class -> [TcType] -> TcM ()
1440 checkValidInstance hs_type tyvars theta clas inst_tys
1441 = setSrcSpan (getLoc hs_type) $
1442 do { setSrcSpan head_loc (checkValidInstHead clas inst_tys)
1443 ; checkValidTheta InstThetaCtxt theta
1444 ; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys)
1446 -- Check that instance inference will terminate (if we care)
1447 -- For Haskell 98 this will already have been done by checkValidTheta,
1448 -- but as we may be using other extensions we need to check.
1449 ; undecidable_ok <- xoptM Opt_UndecidableInstances
1450 ; unless undecidable_ok $
1451 mapM_ addErrTc (checkInstTermination inst_tys theta)
1453 -- The Coverage Condition
1454 ; checkTc (undecidable_ok || checkInstCoverage clas inst_tys)
1455 (instTypeErr (pprClassPred clas inst_tys) msg)
1458 msg = parens (vcat [ptext (sLit "the Coverage Condition fails for one of the functional dependencies;"),
1461 -- The location of the "head" of the instance
1462 head_loc = case hs_type of
1463 L _ (HsForAllTy _ _ _ (L loc _)) -> loc
1467 Termination test: the so-called "Paterson conditions" (see Section 5 of
1468 "Understanding functionsl dependencies via Constraint Handling Rules,
1471 We check that each assertion in the context satisfies:
1472 (1) no variable has more occurrences in the assertion than in the head, and
1473 (2) the assertion has fewer constructors and variables (taken together
1474 and counting repetitions) than the head.
1475 This is only needed with -fglasgow-exts, as Haskell 98 restrictions
1476 (which have already been checked) guarantee termination.
1478 The underlying idea is that
1480 for any ground substitution, each assertion in the
1481 context has fewer type constructors than the head.
1485 checkInstTermination :: [TcType] -> ThetaType -> [Message]
1486 checkInstTermination tys theta
1487 = mapCatMaybes check theta
1490 size = sizeTypes tys
1492 | not (null (fvPred pred \\ fvs))
1493 = Just (predUndecErr pred nomoreMsg $$ parens undecidableMsg)
1494 | sizePred pred >= size
1495 = Just (predUndecErr pred smallerMsg $$ parens undecidableMsg)
1499 predUndecErr :: PredType -> SDoc -> SDoc
1500 predUndecErr pred msg = sep [msg,
1501 nest 2 (ptext (sLit "in the constraint:") <+> pprPred pred)]
1503 nomoreMsg, smallerMsg, undecidableMsg :: SDoc
1504 nomoreMsg = ptext (sLit "Variable occurs more often in a constraint than in the instance head")
1505 smallerMsg = ptext (sLit "Constraint is no smaller than the instance head")
1506 undecidableMsg = ptext (sLit "Use -XUndecidableInstances to permit this")
1509 validDeivPred checks for OK 'deriving' context. See Note [Exotic
1510 derived instance contexts] in TcSimplify. However the predicate is
1511 here because it uses sizeTypes, fvTypes.
1514 validDerivPred :: PredType -> Bool
1515 validDerivPred (ClassP _ tys) = hasNoDups fvs && sizeTypes tys == length fvs
1516 where fvs = fvTypes tys
1517 validDerivPred _ = False
1521 %************************************************************************
1523 Checking type instance well-formedness and termination
1525 %************************************************************************
1528 -- Check that a "type instance" is well-formed (which includes decidability
1529 -- unless -XUndecidableInstances is given).
1531 checkValidTypeInst :: [Type] -> Type -> TcM ()
1532 checkValidTypeInst typats rhs
1533 = do { -- left-hand side contains no type family applications
1534 -- (vanilla synonyms are fine, though)
1535 ; mapM_ checkTyFamFreeness typats
1537 -- the right-hand side is a tau type
1538 ; checkValidMonoType rhs
1540 -- we have a decidable instance unless otherwise permitted
1541 ; undecidable_ok <- xoptM Opt_UndecidableInstances
1542 ; unless undecidable_ok $
1543 mapM_ addErrTc (checkFamInst typats (tyFamInsts rhs))
1546 -- Make sure that each type family instance is
1547 -- (1) strictly smaller than the lhs,
1548 -- (2) mentions no type variable more often than the lhs, and
1549 -- (3) does not contain any further type family instances.
1551 checkFamInst :: [Type] -- lhs
1552 -> [(TyCon, [Type])] -- type family instances
1554 checkFamInst lhsTys famInsts
1555 = mapCatMaybes check famInsts
1557 size = sizeTypes lhsTys
1558 fvs = fvTypes lhsTys
1560 | not (all isTyFamFree tys)
1561 = Just (famInstUndecErr famInst nestedMsg $$ parens undecidableMsg)
1562 | not (null (fvTypes tys \\ fvs))
1563 = Just (famInstUndecErr famInst nomoreVarMsg $$ parens undecidableMsg)
1564 | size <= sizeTypes tys
1565 = Just (famInstUndecErr famInst smallerAppMsg $$ parens undecidableMsg)
1569 famInst = TyConApp tc tys
1571 -- Ensure that no type family instances occur in a type.
1573 checkTyFamFreeness :: Type -> TcM ()
1574 checkTyFamFreeness ty
1575 = checkTc (isTyFamFree ty) $
1576 tyFamInstIllegalErr ty
1578 -- Check that a type does not contain any type family applications.
1580 isTyFamFree :: Type -> Bool
1581 isTyFamFree = null . tyFamInsts
1585 tyFamInstIllegalErr :: Type -> SDoc
1586 tyFamInstIllegalErr ty
1587 = hang (ptext (sLit "Illegal type synonym family application in instance") <>
1591 famInstUndecErr :: Type -> SDoc -> SDoc
1592 famInstUndecErr ty msg
1594 nest 2 (ptext (sLit "in the type family application:") <+>
1597 nestedMsg, nomoreVarMsg, smallerAppMsg :: SDoc
1598 nestedMsg = ptext (sLit "Nested type family application")
1599 nomoreVarMsg = ptext (sLit "Variable occurs more often than in instance head")
1600 smallerAppMsg = ptext (sLit "Application is no smaller than the instance head")
1604 %************************************************************************
1606 \subsection{Auxiliary functions}
1608 %************************************************************************
1611 -- Free variables of a type, retaining repetitions, and expanding synonyms
1612 fvType :: Type -> [TyVar]
1613 fvType ty | Just exp_ty <- tcView ty = fvType exp_ty
1614 fvType (TyVarTy tv) = [tv]
1615 fvType (TyConApp _ tys) = fvTypes tys
1616 fvType (PredTy pred) = fvPred pred
1617 fvType (FunTy arg res) = fvType arg ++ fvType res
1618 fvType (AppTy fun arg) = fvType fun ++ fvType arg
1619 fvType (ForAllTy tyvar ty) = filter (/= tyvar) (fvType ty)
1621 fvTypes :: [Type] -> [TyVar]
1622 fvTypes tys = concat (map fvType tys)
1624 fvPred :: PredType -> [TyVar]
1625 fvPred (ClassP _ tys') = fvTypes tys'
1626 fvPred (IParam _ ty) = fvType ty
1627 fvPred (EqPred ty1 ty2) = fvType ty1 ++ fvType ty2
1629 -- Size of a type: the number of variables and constructors
1630 sizeType :: Type -> Int
1631 sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty
1632 sizeType (TyVarTy _) = 1
1633 sizeType (TyConApp _ tys) = sizeTypes tys + 1
1634 sizeType (PredTy pred) = sizePred pred
1635 sizeType (FunTy arg res) = sizeType arg + sizeType res + 1
1636 sizeType (AppTy fun arg) = sizeType fun + sizeType arg
1637 sizeType (ForAllTy _ ty) = sizeType ty
1639 sizeTypes :: [Type] -> Int
1640 sizeTypes xs = sum (map sizeType xs)
1642 -- Size of a predicate
1644 -- We are considering whether *class* constraints terminate
1645 -- Once we get into an implicit parameter or equality we
1646 -- can't get back to a class constraint, so it's safe
1647 -- to say "size 0". See Trac #4200.
1648 sizePred :: PredType -> Int
1649 sizePred (ClassP _ tys') = sizeTypes tys'
1650 sizePred (IParam {}) = 0
1651 sizePred (EqPred {}) = 0