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,
33 newTcEvBinds, addTcEvBind,
35 --------------------------------
37 tcInstTyVar, tcInstTyVars, tcInstSigTyVars,
38 tcInstType, tcInstSigType,
39 tcInstSkolTyVars, tcInstSkolTyVar, tcInstSkolType,
40 tcSkolSigType, tcSkolSigTyVars,
42 --------------------------------
43 -- Checking type validity
44 Rank, UserTypeCtxt(..), checkValidType, checkValidMonoType,
45 SourceTyCtxt(..), checkValidTheta,
46 checkValidInstHead, checkValidInstance,
47 checkInstTermination, checkValidTypeInst, checkTyFamFreeness,
49 growPredTyVars, growThetaTyVars, validDerivPred,
51 --------------------------------
53 zonkType, mkZonkTcTyVar, zonkTcPredType,
55 zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkSigTyVar,
56 zonkQuantifiedTyVar, zonkQuantifiedTyVars,
57 zonkTcType, zonkTcTypes, zonkTcThetaType,
58 zonkTcKindToKind, zonkTcKind,
59 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
137 -- We used to create a mutable co-var
139 -- A wanted coercion variable is a MetaTyVar
140 -- that can be filled in with its binding
141 = do { uniq <- newUnique
142 ; ref <- newMutVar Flexi
143 ; let name = mkSysTvName uniq (fsLit "c")
144 kind = mkPredTy (EqPred ty1 ty2)
145 ; return (mkTcTyVar name kind (MetaTv TauTv ref)) }
149 newEvVar :: TcPredType -> TcM EvVar
150 -- Creates new *rigid* variables for predicates
151 newEvVar (EqPred ty1 ty2) = newCoVar ty1 ty2
152 newEvVar (ClassP cls tys) = newDict cls tys
153 newEvVar (IParam ip ty) = newIP ip ty
155 newCoVar :: TcType -> TcType -> TcM CoVar
157 = do { name <- newName (mkTyVarOccFS (fsLit "co"))
158 ; return (mkCoVar name (mkPredTy (EqPred ty1 ty2))) }
160 newIP :: IPName Name -> TcType -> TcM IpId
162 = do { name <- newName (getOccName (ipNameName ip))
163 ; return (mkLocalId name (mkPredTy (IParam ip ty))) }
165 newDict :: Class -> [TcType] -> TcM DictId
167 = do { name <- newName (mkDictOcc (getOccName cls))
168 ; return (mkLocalId name (mkPredTy (ClassP cls tys))) }
170 newName :: OccName -> TcM Name
172 = do { uniq <- newUnique
174 ; return (mkInternalName uniq occ loc) }
177 newKindConstraint :: Type -> Kind -> TcM (CoVar, Type)
178 -- Create a new wanted CoVar that constrains the type
179 -- to have the specified kind
180 newKindConstraint ty kind
181 = do { ty_k <- newFlexiTyVarTy kind
182 ; co_var <- newWantedCoVar ty ty_k
183 ; return (co_var, ty_k) }
186 newSelfDict :: Class -> [TcType] -> TcM DictId
187 -- Make a dictionary for "self". It behaves just like a normal DictId
188 -- except that it responds True to isSelfDict
189 -- This is used only to suppress confusing error reports
191 = do { uniq <- newUnique
192 ; let name = mkSystemName uniq selfDictOcc
193 ; return (mkLocalId name (mkPredTy (ClassP cls tys))) }
195 selfDictOcc :: OccName
196 selfDictOcc = mkVarOcc "self"
198 isSelfDict :: EvVar -> Bool
199 isSelfDict v = isSystemName (Var.varName v)
200 -- Notice that all *other* evidence variables get Internal Names
204 %************************************************************************
206 SkolemTvs (immutable)
208 %************************************************************************
211 tcInstType :: ([TyVar] -> TcM [TcTyVar]) -- How to instantiate the type variables
212 -> TcType -- Type to instantiate
213 -> TcM ([TcTyVar], TcThetaType, TcType) -- Result
214 -- (type vars (excl coercion vars), preds (incl equalities), rho)
215 tcInstType inst_tyvars ty
216 = case tcSplitForAllTys ty of
217 ([], rho) -> let -- There may be overloading despite no type variables;
218 -- (?x :: Int) => Int -> Int
219 (theta, tau) = tcSplitPhiTy rho
221 return ([], theta, tau)
223 (tyvars, rho) -> do { tyvars' <- inst_tyvars tyvars
225 ; let tenv = zipTopTvSubst tyvars (mkTyVarTys tyvars')
226 -- Either the tyvars are freshly made, by inst_tyvars,
227 -- or (in the call from tcSkolSigType) any nested foralls
228 -- have different binders. Either way, zipTopTvSubst is ok
230 ; let (theta, tau) = tcSplitPhiTy (substTy tenv rho)
231 ; return (tyvars', theta, tau) }
233 mkSkolTyVar :: Name -> Kind -> SkolemInfo -> TcTyVar
234 mkSkolTyVar name kind info = mkTcTyVar name kind (SkolemTv info)
236 tcSkolSigType :: SkolemInfo -> Type -> TcM ([TcTyVar], TcThetaType, TcType)
237 -- Instantiate a type signature with skolem constants, but
238 -- do *not* give them fresh names, because we want the name to
239 -- be in the type environment: it is lexically scoped.
240 tcSkolSigType info ty = tcInstType (\tvs -> return (tcSkolSigTyVars info tvs)) ty
242 tcSkolSigTyVars :: SkolemInfo -> [TyVar] -> [TcTyVar]
243 -- Make skolem constants, but do *not* give them new names, as above
244 tcSkolSigTyVars info tyvars = [ mkSkolTyVar (tyVarName tv) (tyVarKind tv) info
247 tcInstSkolTyVar :: SkolemInfo -> TyVar -> TcM TcTyVar
248 -- Instantiate the tyvar, using
249 -- * the occ-name and kind of the supplied tyvar,
250 -- * the unique from the monad,
251 -- * the location either from the tyvar (skol_info = SigSkol)
252 -- or from the monad (otehrwise)
253 tcInstSkolTyVar skol_info tyvar
254 = do { uniq <- newUnique
255 ; loc <- case skol_info of
256 SigSkol {} -> return (getSrcSpan old_name)
258 ; let new_name = mkInternalName uniq occ loc
259 ; return (mkSkolTyVar new_name kind skol_info) }
261 old_name = tyVarName tyvar
262 occ = nameOccName old_name
263 kind = tyVarKind tyvar
265 tcInstSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
266 -- Get the location from the monad
267 tcInstSkolTyVars info tyvars
268 = mapM (tcInstSkolTyVar info) tyvars
270 tcInstSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
271 -- Instantiate a type with fresh skolem constants
272 -- Binding location comes from the monad
273 tcInstSkolType info ty = tcInstType (tcInstSkolTyVars info) ty
275 tcInstSigType :: Bool -> Name -> TcType -> TcM ([TcTyVar], TcThetaType, TcRhoType)
276 -- Instantiate with skolems or meta SigTvs; depending on use_skols
277 -- Always take location info from the supplied tyvars
278 tcInstSigType use_skols name ty
280 = tcInstType (tcInstSkolTyVars (SigSkol (FunSigCtxt name))) ty
282 = tcInstType tcInstSigTyVars ty
284 tcInstSigTyVars :: [TyVar] -> TcM [TcTyVar]
285 -- Make meta SigTv type variables for patten-bound scoped type varaibles
286 -- We use SigTvs for them, so that they can't unify with arbitrary types
287 tcInstSigTyVars = mapM (\tv -> instMetaTyVar (SigTv (tyVarName tv)) tv)
288 -- ToDo: the "function binding site is bogus
292 %************************************************************************
294 MetaTvs (meta type variables; mutable)
296 %************************************************************************
299 newMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar
300 -- Make a new meta tyvar out of thin air
301 newMetaTyVar meta_info kind
302 = do { uniq <- newUnique
303 ; ref <- newMutVar Flexi
304 ; let name = mkSysTvName uniq fs
305 fs = case meta_info of
308 ; return (mkTcTyVar name kind (MetaTv meta_info ref)) }
310 instMetaTyVar :: MetaInfo -> TyVar -> TcM TcTyVar
311 -- Make a new meta tyvar whose Name and Kind
312 -- come from an existing TyVar
313 instMetaTyVar meta_info tyvar
314 = do { uniq <- newUnique
315 ; ref <- newMutVar Flexi
316 ; let name = setNameUnique (tyVarName tyvar) uniq
317 kind = tyVarKind tyvar
318 ; return (mkTcTyVar name kind (MetaTv meta_info ref)) }
320 readMetaTyVar :: TyVar -> TcM MetaDetails
321 readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
322 readMutVar (metaTvRef tyvar)
324 readWantedCoVar :: CoVar -> TcM MetaDetails
325 readWantedCoVar covar = ASSERT2( isMetaTyVar covar, ppr covar )
326 readMutVar (metaTvRef covar)
330 isFilledMetaTyVar :: TyVar -> TcM Bool
331 -- True of a filled-in (Indirect) meta type variable
333 | not (isTcTyVar tv) = return False
334 | MetaTv _ ref <- tcTyVarDetails tv
335 = do { details <- readMutVar ref
336 ; return (isIndirect details) }
337 | otherwise = return False
339 isFlexiMetaTyVar :: TyVar -> TcM Bool
340 -- True of a un-filled-in (Flexi) meta type variable
342 | not (isTcTyVar tv) = return False
343 | MetaTv _ ref <- tcTyVarDetails tv
344 = do { details <- readMutVar ref
345 ; return (isFlexi details) }
346 | otherwise = return False
349 writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
350 -- Write into a currently-empty MetaTyVar
352 writeMetaTyVar tyvar ty
354 = writeMetaTyVarRef tyvar (metaTvRef tyvar) ty
356 -- Everything from here on only happens if DEBUG is on
357 | not (isTcTyVar tyvar)
358 = WARN( True, text "Writing to non-tc tyvar" <+> ppr tyvar )
361 | MetaTv _ ref <- tcTyVarDetails tyvar
362 = writeMetaTyVarRef tyvar ref ty
365 = WARN( True, text "Writing to non-meta tyvar" <+> ppr tyvar )
368 writeWantedCoVar :: CoVar -> Coercion -> TcM ()
369 writeWantedCoVar cv co = writeMetaTyVar cv co
372 writeMetaTyVarRef :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM ()
373 -- Here the tyvar is for error checking only;
374 -- the ref cell must be for the same tyvar
375 writeMetaTyVarRef tyvar ref ty
377 = do { traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
378 ; writeMutVar ref (Indirect ty) }
380 -- Everything from here on only happens if DEBUG is on
381 | not (isPredTy tv_kind) -- Don't check kinds for updates to coercion variables
382 , not (ty_kind `isSubKind` tv_kind)
383 = WARN( True, hang (text "Ill-kinded update to meta tyvar")
384 2 (ppr tyvar $$ ppr tv_kind $$ ppr ty $$ ppr ty_kind) )
388 = do { meta_details <- readMutVar ref;
389 ; WARN( not (isFlexi meta_details),
390 hang (text "Double update of meta tyvar")
391 2 (ppr tyvar $$ ppr meta_details) )
393 traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
394 ; writeMutVar ref (Indirect ty) }
396 tv_kind = tyVarKind tyvar
397 ty_kind = typeKind ty
401 %************************************************************************
405 %************************************************************************
408 newFlexiTyVar :: Kind -> TcM TcTyVar
409 newFlexiTyVar kind = newMetaTyVar TauTv kind
411 newFlexiTyVarTy :: Kind -> TcM TcType
412 newFlexiTyVarTy kind = do
413 tc_tyvar <- newFlexiTyVar kind
414 return (TyVarTy tc_tyvar)
416 newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
417 newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind)
419 tcInstTyVar :: TyVar -> TcM TcTyVar
420 -- Instantiate with a META type variable
421 tcInstTyVar tyvar = instMetaTyVar TauTv tyvar
423 tcInstTyVars :: [TyVar] -> TcM ([TcTyVar], [TcType], TvSubst)
424 -- Instantiate with META type variables
426 = do { tc_tvs <- mapM tcInstTyVar tyvars
427 ; let tys = mkTyVarTys tc_tvs
428 ; return (tc_tvs, tys, zipTopTvSubst tyvars tys) }
429 -- Since the tyvars are freshly made,
430 -- they cannot possibly be captured by
431 -- any existing for-alls. Hence zipTopTvSubst
435 %************************************************************************
439 %************************************************************************
442 zonkSigTyVar :: TcTyVar -> TcM TcTyVar
444 | isSkolemTyVar sig_tv
445 = return sig_tv -- Happens in the call in TcBinds.checkDistinctTyVars
447 = ASSERT( isSigTyVar sig_tv )
448 do { ty <- zonkTcTyVar sig_tv
449 ; return (tcGetTyVar "zonkSigTyVar" ty) }
450 -- 'ty' is bound to be a type variable, because SigTvs
451 -- can only be unified with type variables
456 %************************************************************************
458 \subsection{Zonking -- the exernal interfaces}
460 %************************************************************************
462 @tcGetGlobalTyVars@ returns a fully-zonked set of tyvars free in the environment.
463 To improve subsequent calls to the same function it writes the zonked set back into
467 tcGetGlobalTyVars :: TcM TcTyVarSet
469 = do { (TcLclEnv {tcl_tyvars = gtv_var}) <- getLclEnv
470 ; gbl_tvs <- readMutVar gtv_var
471 ; gbl_tvs' <- zonkTcTyVarsAndFV (varSetElems gbl_tvs)
472 ; writeMutVar gtv_var gbl_tvs'
476 ----------------- Type variables
479 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
480 zonkTcTyVars tyvars = mapM zonkTcTyVar tyvars
482 zonkTcTyVarsAndFV :: [TcTyVar] -> TcM TcTyVarSet
483 zonkTcTyVarsAndFV tyvars = tyVarsOfTypes <$> mapM zonkTcTyVar tyvars
485 ----------------- Types
487 zonkTcTypeCarefully :: TcType -> TcM TcType
488 zonkTcTypeCarefully ty
489 = do { env_tvs <- tcGetGlobalTyVars
490 ; zonkType (zonkTcTyVarCarefully env_tvs) ty }
493 zonkTcTyVarCarefully :: TcTyVarSet -> TcTyVar -> TcM TcType
494 -- Do not zonk type variables free in the environment
495 zonkTcTyVarCarefully env_tvs tv
496 | tv `elemVarSet` env_tvs
497 = return (TyVarTy tv)
499 = ASSERT( isTcTyVar tv )
500 case tcTyVarDetails tv of
501 SkolemTv {} -> return (TyVarTy tv)
502 FlatSkol ty -> zonkType (zonkTcTyVarCarefully env_tvs) ty
503 MetaTv _ ref -> do { cts <- readMutVar ref
505 Flexi -> return (TyVarTy tv)
506 Indirect ty -> zonkType (zonkTcTyVarCarefully env_tvs) ty }
508 zonkTcType :: TcType -> TcM TcType
509 -- Simply look through all Flexis
510 zonkTcType ty = zonkType zonkTcTyVar ty
512 zonkTcTyVar :: TcTyVar -> TcM TcType
513 -- Simply look through all Flexis
515 = ASSERT2( isTcTyVar tv, ppr tv )
516 case tcTyVarDetails tv of
517 SkolemTv {} -> return (TyVarTy tv)
518 FlatSkol ty -> zonkTcType ty
519 MetaTv _ ref -> do { cts <- readMutVar ref
521 Flexi -> return (TyVarTy tv)
522 Indirect ty -> zonkTcType ty }
524 zonkTcTypes :: [TcType] -> TcM [TcType]
525 zonkTcTypes tys = mapM zonkTcType tys
527 zonkTcThetaType :: TcThetaType -> TcM TcThetaType
528 zonkTcThetaType theta = mapM zonkTcPredType theta
530 zonkTcPredType :: TcPredType -> TcM TcPredType
531 zonkTcPredType (ClassP c ts) = ClassP c <$> zonkTcTypes ts
532 zonkTcPredType (IParam n t) = IParam n <$> zonkTcType t
533 zonkTcPredType (EqPred t1 t2) = EqPred <$> zonkTcType t1 <*> zonkTcType t2
536 ------------------- These ...ToType, ...ToKind versions
537 are used at the end of type checking
540 zonkQuantifiedTyVars :: [TcTyVar] -> TcM [TcTyVar]
541 zonkQuantifiedTyVars = mapM zonkQuantifiedTyVar
543 zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar
544 -- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it.
546 -- The quantified type variables often include meta type variables
547 -- we want to freeze them into ordinary type variables, and
548 -- default their kind (e.g. from OpenTypeKind to TypeKind)
549 -- -- see notes with Kind.defaultKind
550 -- The meta tyvar is updated to point to the new skolem TyVar. Now any
551 -- bound occurences of the original type variable will get zonked to
552 -- the immutable version.
554 -- We leave skolem TyVars alone; they are immutable.
555 zonkQuantifiedTyVar tv
556 | ASSERT2( isTcTyVar tv, ppr tv )
558 = do { kind <- zonkTcType (tyVarKind tv)
559 ; return $ setTyVarKind tv kind
561 -- It might be a skolem type variable,
562 -- for example from a user type signature
564 | otherwise -- It's a meta-type-variable
565 = do { details <- readMetaTyVar tv
567 -- Create the new, frozen, skolem type variable
568 -- We zonk to a skolem, not to a regular TcVar
569 -- See Note [Zonking to Skolem]
570 ; let final_kind = defaultKind (tyVarKind tv)
571 final_tv = mkSkolTyVar (tyVarName tv) final_kind UnkSkol
573 -- Bind the meta tyvar to the new tyvar
575 Indirect ty -> WARN( True, ppr tv $$ ppr ty )
577 -- [Sept 04] I don't think this should happen
578 -- See note [Silly Type Synonym]
580 Flexi -> writeMetaTyVar tv (mkTyVarTy final_tv)
582 -- Return the new tyvar
587 zonkImplication :: Implication -> TcM Implication
588 zonkImplication implic@(Implic { ic_env_tvs = env_tvs, ic_given = given
589 , ic_wanted = wanted })
590 = do { env_tvs' <- zonkTcTyVarsAndFV (varSetElems env_tvs)
591 ; given' <- mapM zonkEvVar given
592 ; wanted' <- mapBagM zonkWanted wanted
593 ; return (implic { ic_env_tvs = env_tvs', ic_given = given'
594 , ic_wanted = wanted' }) }
596 zonkEvVar :: EvVar -> TcM EvVar
597 zonkEvVar var = do { ty' <- zonkTcType (varType var)
598 ; return (setVarType var ty') }
600 zonkWanted :: WantedConstraint -> TcM WantedConstraint
601 zonkWanted (WcImplic imp) = do { imp' <- zonkImplication imp; return (WcImplic imp') }
602 zonkWanted (WcEvVar ev) = do { ev' <- zonkWantedEvVar ev; return (WcEvVar ev') }
604 zonkWantedEvVar :: WantedEvVar -> TcM WantedEvVar
605 zonkWantedEvVar (WantedEvVar v l) = do { v' <- zonkEvVar v; return (WantedEvVar v' l) }
609 Note [Silly Type Synonyms]
610 ~~~~~~~~~~~~~~~~~~~~~~~~~~
612 type C u a = u -- Note 'a' unused
614 foo :: (forall a. C u a -> C u a) -> u
618 bar = foo (\t -> t + t)
620 * From the (\t -> t+t) we get type {Num d} => d -> d
623 * Now unify with type of foo's arg, and we get:
624 {Num (C d a)} => C d a -> C d a
627 * Now abstract over the 'a', but float out the Num (C d a) constraint
628 because it does not 'really' mention a. (see exactTyVarsOfType)
629 The arg to foo becomes
632 * So we get a dict binding for Num (C d a), which is zonked to give
634 [Note Sept 04: now that we are zonking quantified type variables
635 on construction, the 'a' will be frozen as a regular tyvar on
636 quantification, so the floated dict will still have type (C d a).
637 Which renders this whole note moot; happily!]
639 * Then the \/\a abstraction has a zonked 'a' in it.
641 All very silly. I think its harmless to ignore the problem. We'll end up with
642 a \/\a in the final result but all the occurrences of a will be zonked to ()
644 Note [Zonking to Skolem]
645 ~~~~~~~~~~~~~~~~~~~~~~~~
646 We used to zonk quantified type variables to regular TyVars. However, this
647 leads to problems. Consider this program from the regression test suite:
649 eval :: Int -> String -> String -> String
650 eval 0 root actual = evalRHS 0 root actual
653 evalRHS 0 root actual = eval 0 root actual
655 It leads to the deferral of an equality (wrapped in an implication constraint)
657 forall a. (String -> String -> String) ~ a
659 which is propagated up to the toplevel (see TcSimplify.tcSimplifyInferCheck).
660 In the meantime `a' is zonked and quantified to form `evalRHS's signature.
661 This has the *side effect* of also zonking the `a' in the deferred equality
662 (which at this point is being handed around wrapped in an implication
665 Finally, the equality (with the zonked `a') will be handed back to the
666 simplifier by TcRnDriver.tcRnSrcDecls calling TcSimplify.tcSimplifyTop.
667 If we zonk `a' with a regular type variable, we will have this regular type
668 variable now floating around in the simplifier, which in many places assumes to
669 only see proper TcTyVars.
671 We can avoid this problem by zonking with a skolem. The skolem is rigid
672 (which we require for a quantified variable), but is still a TcTyVar that the
673 simplifier knows how to deal with.
676 %************************************************************************
678 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
680 %* For internal use only! *
682 %************************************************************************
685 -- For unbound, mutable tyvars, zonkType uses the function given to it
686 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
687 -- type variable and zonks the kind too
689 zonkType :: (TcTyVar -> TcM Type) -- What to do with unbound mutable type variables
690 -- see zonkTcType, and zonkTcTypeToType
693 zonkType zonk_tc_tyvar ty
696 go (TyConApp tc tys) = do tys' <- mapM go tys
697 return (TyConApp tc tys')
699 go (PredTy p) = do p' <- go_pred p
702 go (FunTy arg res) = do arg' <- go arg
704 return (FunTy arg' res')
706 go (AppTy fun arg) = do fun' <- go fun
708 return (mkAppTy fun' arg')
709 -- NB the mkAppTy; we might have instantiated a
710 -- type variable to a type constructor, so we need
711 -- to pull the TyConApp to the top.
713 -- The two interesting cases!
714 go (TyVarTy tyvar) | isTcTyVar tyvar = zonk_tc_tyvar tyvar
715 | otherwise = liftM TyVarTy $
716 zonkTyVar zonk_tc_tyvar tyvar
717 -- Ordinary (non Tc) tyvars occur inside quantified types
719 go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar ) do
721 tyvar' <- zonkTyVar zonk_tc_tyvar tyvar
722 return (ForAllTy tyvar' ty')
724 go_pred (ClassP c tys) = do tys' <- mapM go tys
725 return (ClassP c tys')
726 go_pred (IParam n ty) = do ty' <- go ty
727 return (IParam n ty')
728 go_pred (EqPred ty1 ty2) = do ty1' <- go ty1
730 return (EqPred ty1' ty2')
732 mkZonkTcTyVar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable var
733 -> TcTyVar -> TcM TcType
734 mkZonkTcTyVar unbound_var_fn tyvar
735 = ASSERT( isTcTyVar tyvar )
736 case tcTyVarDetails tyvar of
737 SkolemTv {} -> return (TyVarTy tyvar)
738 FlatSkol ty -> zonkType (mkZonkTcTyVar unbound_var_fn) ty
739 MetaTv _ ref -> do { cts <- readMutVar ref
741 Flexi -> unbound_var_fn tyvar
742 Indirect ty -> zonkType (mkZonkTcTyVar unbound_var_fn) ty }
744 -- Zonk the kind of a non-TC tyvar in case it is a coercion variable
745 -- (their kind contains types).
746 zonkTyVar :: (TcTyVar -> TcM Type) -- What to do for a TcTyVar
747 -> TyVar -> TcM TyVar
748 zonkTyVar zonk_tc_tyvar tv
750 = do { kind <- zonkType zonk_tc_tyvar (tyVarKind tv)
751 ; return $ setTyVarKind tv kind }
752 | otherwise = return tv
757 %************************************************************************
761 %************************************************************************
764 readKindVar :: KindVar -> TcM (MetaDetails)
765 writeKindVar :: KindVar -> TcKind -> TcM ()
766 readKindVar kv = readMutVar (kindVarRef kv)
767 writeKindVar kv val = writeMutVar (kindVarRef kv) (Indirect val)
770 zonkTcKind :: TcKind -> TcM TcKind
771 zonkTcKind k = zonkTcType k
774 zonkTcKindToKind :: TcKind -> TcM Kind
775 -- When zonking a TcKind to a kind, we need to instantiate kind variables,
776 -- Haskell specifies that * is to be used, so we follow that.
778 = zonkType (mkZonkTcTyVar (\ _ -> return liftedTypeKind)) k
781 %************************************************************************
783 \subsection{Checking a user type}
785 %************************************************************************
787 When dealing with a user-written type, we first translate it from an HsType
788 to a Type, performing kind checking, and then check various things that should
789 be true about it. We don't want to perform these checks at the same time
790 as the initial translation because (a) they are unnecessary for interface-file
791 types and (b) when checking a mutually recursive group of type and class decls,
792 we can't "look" at the tycons/classes yet. Also, the checks are are rather
793 diverse, and used to really mess up the other code.
795 One thing we check for is 'rank'.
797 Rank 0: monotypes (no foralls)
798 Rank 1: foralls at the front only, Rank 0 inside
799 Rank 2: foralls at the front, Rank 1 on left of fn arrow,
801 basic ::= tyvar | T basic ... basic
803 r2 ::= forall tvs. cxt => r2a
804 r2a ::= r1 -> r2a | basic
805 r1 ::= forall tvs. cxt => r0
806 r0 ::= r0 -> r0 | basic
808 Another thing is to check that type synonyms are saturated.
809 This might not necessarily show up in kind checking.
811 data T k = MkT (k Int)
816 checkValidType :: UserTypeCtxt -> Type -> TcM ()
817 -- Checks that the type is valid for the given context
818 checkValidType ctxt ty = do
819 traceTc "checkValidType" (ppr ty)
820 unboxed <- doptM Opt_UnboxedTuples
821 rank2 <- doptM Opt_Rank2Types
822 rankn <- doptM Opt_RankNTypes
823 polycomp <- doptM Opt_PolymorphicComponents
825 gen_rank n | rankn = ArbitraryRank
830 DefaultDeclCtxt-> MustBeMonoType
831 ResSigCtxt -> MustBeMonoType
832 LamPatSigCtxt -> gen_rank 0
833 BindPatSigCtxt -> gen_rank 0
834 TySynCtxt _ -> gen_rank 0
835 GenPatCtxt -> gen_rank 1
836 -- This one is a bit of a hack
837 -- See the forall-wrapping in TcClassDcl.mkGenericInstance
839 ExprSigCtxt -> gen_rank 1
840 FunSigCtxt _ -> gen_rank 1
841 ConArgCtxt _ | polycomp -> gen_rank 2
842 -- We are given the type of the entire
843 -- constructor, hence rank 1
844 | otherwise -> gen_rank 1
846 ForSigCtxt _ -> gen_rank 1
847 SpecInstCtxt -> gen_rank 1
848 ThBrackCtxt -> gen_rank 1
850 actual_kind = typeKind ty
852 kind_ok = case ctxt of
853 TySynCtxt _ -> True -- Any kind will do
854 ThBrackCtxt -> True -- Any kind will do
855 ResSigCtxt -> isSubOpenTypeKind actual_kind
856 ExprSigCtxt -> isSubOpenTypeKind actual_kind
857 GenPatCtxt -> isLiftedTypeKind actual_kind
858 ForSigCtxt _ -> isLiftedTypeKind actual_kind
859 _ -> isSubArgTypeKind actual_kind
861 ubx_tup = case ctxt of
862 TySynCtxt _ | unboxed -> UT_Ok
863 ExprSigCtxt | unboxed -> UT_Ok
864 ThBrackCtxt | unboxed -> UT_Ok
867 -- Check the internal validity of the type itself
868 check_type rank ubx_tup ty
870 -- Check that the thing has kind Type, and is lifted if necessary
871 -- Do this second, becuase we can't usefully take the kind of an
872 -- ill-formed type such as (a~Int)
873 checkTc kind_ok (kindErr actual_kind)
875 traceTc "checkValidType done" (ppr ty)
877 checkValidMonoType :: Type -> TcM ()
878 checkValidMonoType ty = check_mono_type MustBeMonoType ty
883 data Rank = ArbitraryRank -- Any rank ok
884 | MustBeMonoType -- Monotype regardless of flags
885 | TyConArgMonoType -- Monotype but could be poly if -XImpredicativeTypes
886 | SynArgMonoType -- Monotype but could be poly if -XLiberalTypeSynonyms
887 | Rank Int -- Rank n, but could be more with -XRankNTypes
889 decRank :: Rank -> Rank -- Function arguments
890 decRank (Rank 0) = Rank 0
891 decRank (Rank n) = Rank (n-1)
892 decRank other_rank = other_rank
894 nonZeroRank :: Rank -> Bool
895 nonZeroRank ArbitraryRank = True
896 nonZeroRank (Rank n) = n>0
897 nonZeroRank _ = False
899 ----------------------------------------
900 data UbxTupFlag = UT_Ok | UT_NotOk
901 -- The "Ok" version means "ok if UnboxedTuples is on"
903 ----------------------------------------
904 check_mono_type :: Rank -> Type -> TcM () -- No foralls anywhere
905 -- No unlifted types of any kind
906 check_mono_type rank ty
907 = do { check_type rank UT_NotOk ty
908 ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
910 check_type :: Rank -> UbxTupFlag -> Type -> TcM ()
911 -- The args say what the *type context* requires, independent
912 -- of *flag* settings. You test the flag settings at usage sites.
914 -- Rank is allowed rank for function args
915 -- Rank 0 means no for-alls anywhere
917 check_type rank ubx_tup ty
918 | not (null tvs && null theta)
919 = do { checkTc (nonZeroRank rank) (forAllTyErr rank ty)
920 -- Reject e.g. (Maybe (?x::Int => Int)),
921 -- with a decent error message
922 ; check_valid_theta SigmaCtxt theta
923 ; check_type rank ubx_tup tau -- Allow foralls to right of arrow
924 ; checkAmbiguity tvs theta (tyVarsOfType tau) }
926 (tvs, theta, tau) = tcSplitSigmaTy ty
928 -- Naked PredTys should, I think, have been rejected before now
929 check_type _ _ ty@(PredTy {})
930 = failWithTc (text "Predicate" <+> ppr ty <+> text "used as a type")
932 check_type _ _ (TyVarTy _) = return ()
934 check_type rank _ (FunTy arg_ty res_ty)
935 = do { check_type (decRank rank) UT_NotOk arg_ty
936 ; check_type rank UT_Ok res_ty }
938 check_type rank _ (AppTy ty1 ty2)
939 = do { check_arg_type rank ty1
940 ; check_arg_type rank ty2 }
942 check_type rank ubx_tup ty@(TyConApp tc tys)
944 = do { -- Check that the synonym has enough args
945 -- This applies equally to open and closed synonyms
946 -- It's OK to have an *over-applied* type synonym
947 -- data Tree a b = ...
948 -- type Foo a = Tree [a]
949 -- f :: Foo a b -> ...
950 checkTc (tyConArity tc <= length tys) arity_msg
952 -- See Note [Liberal type synonyms]
953 ; liberal <- doptM Opt_LiberalTypeSynonyms
954 ; if not liberal || isSynFamilyTyCon tc then
955 -- For H98 and synonym families, do check the type args
956 mapM_ (check_mono_type SynArgMonoType) tys
958 else -- In the liberal case (only for closed syns), expand then check
960 Just ty' -> check_type rank ubx_tup ty'
961 Nothing -> pprPanic "check_tau_type" (ppr ty)
964 | isUnboxedTupleTyCon tc
965 = do { ub_tuples_allowed <- doptM Opt_UnboxedTuples
966 ; checkTc (ubx_tup_ok ub_tuples_allowed) ubx_tup_msg
968 ; impred <- doptM Opt_ImpredicativeTypes
969 ; let rank' = if impred then ArbitraryRank else TyConArgMonoType
970 -- c.f. check_arg_type
971 -- However, args are allowed to be unlifted, or
972 -- more unboxed tuples, so can't use check_arg_ty
973 ; mapM_ (check_type rank' UT_Ok) tys }
976 = mapM_ (check_arg_type rank) tys
979 ubx_tup_ok ub_tuples_allowed = case ubx_tup of
980 UT_Ok -> ub_tuples_allowed
984 tc_arity = tyConArity tc
986 arity_msg = arityErr "Type synonym" (tyConName tc) tc_arity n_args
987 ubx_tup_msg = ubxArgTyErr ty
989 check_type _ _ ty = pprPanic "check_type" (ppr ty)
991 ----------------------------------------
992 check_arg_type :: Rank -> Type -> TcM ()
993 -- The sort of type that can instantiate a type variable,
994 -- or be the argument of a type constructor.
995 -- Not an unboxed tuple, but now *can* be a forall (since impredicativity)
996 -- Other unboxed types are very occasionally allowed as type
997 -- arguments depending on the kind of the type constructor
999 -- For example, we want to reject things like:
1001 -- instance Ord a => Ord (forall s. T s a)
1003 -- g :: T s (forall b.b)
1005 -- NB: unboxed tuples can have polymorphic or unboxed args.
1006 -- This happens in the workers for functions returning
1007 -- product types with polymorphic components.
1008 -- But not in user code.
1009 -- Anyway, they are dealt with by a special case in check_tau_type
1011 check_arg_type rank ty
1012 = do { impred <- doptM Opt_ImpredicativeTypes
1013 ; let rank' = case rank of -- Predictive => must be monotype
1014 MustBeMonoType -> MustBeMonoType -- Monotype, regardless
1015 _other | impred -> ArbitraryRank
1016 | otherwise -> TyConArgMonoType
1017 -- Make sure that MustBeMonoType is propagated,
1018 -- so that we don't suggest -XImpredicativeTypes in
1019 -- (Ord (forall a.a)) => a -> a
1020 -- and so that if it Must be a monotype, we check that it is!
1022 ; check_type rank' UT_NotOk ty
1023 ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
1025 ----------------------------------------
1026 forAllTyErr :: Rank -> Type -> SDoc
1028 = vcat [ hang (ptext (sLit "Illegal polymorphic or qualified type:")) 2 (ppr ty)
1031 suggestion = case rank of
1032 Rank _ -> ptext (sLit "Perhaps you intended to use -XRankNTypes or -XRank2Types")
1033 TyConArgMonoType -> ptext (sLit "Perhaps you intended to use -XImpredicativeTypes")
1034 SynArgMonoType -> ptext (sLit "Perhaps you intended to use -XLiberalTypeSynonyms")
1035 _ -> empty -- Polytype is always illegal
1037 unliftedArgErr, ubxArgTyErr :: Type -> SDoc
1038 unliftedArgErr ty = sep [ptext (sLit "Illegal unlifted type:"), ppr ty]
1039 ubxArgTyErr ty = sep [ptext (sLit "Illegal unboxed tuple type as function argument:"), ppr ty]
1041 kindErr :: Kind -> SDoc
1042 kindErr kind = sep [ptext (sLit "Expecting an ordinary type, but found a type of kind"), ppr kind]
1045 Note [Liberal type synonyms]
1046 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1047 If -XLiberalTypeSynonyms is on, expand closed type synonyms *before*
1048 doing validity checking. This allows us to instantiate a synonym defn
1049 with a for-all type, or with a partially-applied type synonym.
1053 Here, T is partially applied, so it's illegal in H98. But if you
1054 expand S first, then T we get just
1058 IMPORTANT: suppose T is a type synonym. Then we must do validity
1059 checking on an appliation (T ty1 ty2)
1061 *either* before expansion (i.e. check ty1, ty2)
1062 *or* after expansion (i.e. expand T ty1 ty2, and then check)
1065 If we do both, we get exponential behaviour!!
1067 data TIACons1 i r c = c i ::: r c
1068 type TIACons2 t x = TIACons1 t (TIACons1 t x)
1069 type TIACons3 t x = TIACons2 t (TIACons1 t x)
1070 type TIACons4 t x = TIACons2 t (TIACons2 t x)
1071 type TIACons7 t x = TIACons4 t (TIACons3 t x)
1074 %************************************************************************
1076 \subsection{Checking a theta or source type}
1078 %************************************************************************
1081 -- Enumerate the contexts in which a "source type", <S>, can occur
1085 -- or (N a) where N is a newtype
1088 = ClassSCCtxt Name -- Superclasses of clas
1089 -- class <S> => C a where ...
1090 | SigmaCtxt -- Theta part of a normal for-all type
1091 -- f :: <S> => a -> a
1092 | DataTyCtxt Name -- Theta part of a data decl
1093 -- data <S> => T a = MkT a
1094 | TypeCtxt -- Source type in an ordinary type
1096 | InstThetaCtxt -- Context of an instance decl
1097 -- instance <S> => C [a] where ...
1099 pprSourceTyCtxt :: SourceTyCtxt -> SDoc
1100 pprSourceTyCtxt (ClassSCCtxt c) = ptext (sLit "the super-classes of class") <+> quotes (ppr c)
1101 pprSourceTyCtxt SigmaCtxt = ptext (sLit "the context of a polymorphic type")
1102 pprSourceTyCtxt (DataTyCtxt tc) = ptext (sLit "the context of the data type declaration for") <+> quotes (ppr tc)
1103 pprSourceTyCtxt InstThetaCtxt = ptext (sLit "the context of an instance declaration")
1104 pprSourceTyCtxt TypeCtxt = ptext (sLit "the context of a type")
1108 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
1109 checkValidTheta ctxt theta
1110 = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
1112 -------------------------
1113 check_valid_theta :: SourceTyCtxt -> [PredType] -> TcM ()
1114 check_valid_theta _ []
1116 check_valid_theta ctxt theta = do
1118 warnTc (notNull dups) (dupPredWarn dups)
1119 mapM_ (check_pred_ty dflags ctxt) theta
1121 (_,dups) = removeDups tcCmpPred theta
1123 -------------------------
1124 check_pred_ty :: DynFlags -> SourceTyCtxt -> PredType -> TcM ()
1125 check_pred_ty dflags ctxt pred@(ClassP cls tys)
1126 = do { -- Class predicates are valid in all contexts
1127 ; checkTc (arity == n_tys) arity_err
1129 -- Check the form of the argument types
1130 ; mapM_ checkValidMonoType tys
1131 ; checkTc (check_class_pred_tys dflags ctxt tys)
1132 (predTyVarErr pred $$ how_to_allow)
1135 class_name = className cls
1136 arity = classArity cls
1138 arity_err = arityErr "Class" class_name arity n_tys
1139 how_to_allow = parens (ptext (sLit "Use -XFlexibleContexts to permit this"))
1142 check_pred_ty dflags _ pred@(EqPred ty1 ty2)
1143 = do { -- Equational constraints are valid in all contexts if type
1144 -- families are permitted
1145 ; checkTc (dopt Opt_TypeFamilies dflags) (eqPredTyErr pred)
1147 -- Check the form of the argument types
1148 ; checkValidMonoType ty1
1149 ; checkValidMonoType ty2
1152 check_pred_ty _ SigmaCtxt (IParam _ ty) = checkValidMonoType ty
1153 -- Implicit parameters only allowed in type
1154 -- signatures; not in instance decls, superclasses etc
1155 -- The reason for not allowing implicit params in instances is a bit
1157 -- If we allowed instance (?x::Int, Eq a) => Foo [a] where ...
1158 -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
1159 -- discharge all the potential usas of the ?x in e. For example, a
1160 -- constraint Foo [Int] might come out of e,and applying the
1161 -- instance decl would show up two uses of ?x.
1164 check_pred_ty _ _ sty = failWithTc (badPredTyErr sty)
1166 -------------------------
1167 check_class_pred_tys :: DynFlags -> SourceTyCtxt -> [Type] -> Bool
1168 check_class_pred_tys dflags ctxt tys
1170 TypeCtxt -> True -- {-# SPECIALISE instance Eq (T Int) #-} is fine
1171 InstThetaCtxt -> flexible_contexts || undecidable_ok || all tcIsTyVarTy tys
1172 -- Further checks on head and theta in
1173 -- checkInstTermination
1174 _ -> flexible_contexts || all tyvar_head tys
1176 flexible_contexts = dopt Opt_FlexibleContexts dflags
1177 undecidable_ok = dopt Opt_UndecidableInstances dflags
1179 -------------------------
1180 tyvar_head :: Type -> Bool
1181 tyvar_head ty -- Haskell 98 allows predicates of form
1182 | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
1183 | otherwise -- where a is a type variable
1184 = case tcSplitAppTy_maybe ty of
1185 Just (ty, _) -> tyvar_head ty
1192 is ambiguous if P contains generic variables
1193 (i.e. one of the Vs) that are not mentioned in tau
1195 However, we need to take account of functional dependencies
1196 when we speak of 'mentioned in tau'. Example:
1197 class C a b | a -> b where ...
1199 forall x y. (C x y) => x
1200 is not ambiguous because x is mentioned and x determines y
1202 NB; the ambiguity check is only used for *user* types, not for types
1203 coming from inteface files. The latter can legitimately have
1204 ambiguous types. Example
1206 class S a where s :: a -> (Int,Int)
1207 instance S Char where s _ = (1,1)
1208 f:: S a => [a] -> Int -> (Int,Int)
1209 f (_::[a]) x = (a*x,b)
1210 where (a,b) = s (undefined::a)
1212 Here the worker for f gets the type
1213 fw :: forall a. S a => Int -> (# Int, Int #)
1215 If the list of tv_names is empty, we have a monotype, and then we
1216 don't need to check for ambiguity either, because the test can't fail
1219 In addition, GHC insists that at least one type variable
1220 in each constraint is in V. So we disallow a type like
1221 forall a. Eq b => b -> b
1222 even in a scope where b is in scope.
1225 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
1226 checkAmbiguity forall_tyvars theta tau_tyvars
1227 = mapM_ complain (filter is_ambig theta)
1229 complain pred = addErrTc (ambigErr pred)
1230 extended_tau_vars = growThetaTyVars theta tau_tyvars
1232 -- See Note [Implicit parameters and ambiguity] in TcSimplify
1233 is_ambig pred = isClassPred pred &&
1234 any ambig_var (varSetElems (tyVarsOfPred pred))
1236 ambig_var ct_var = (ct_var `elem` forall_tyvars) &&
1237 not (ct_var `elemVarSet` extended_tau_vars)
1239 ambigErr :: PredType -> SDoc
1241 = sep [ptext (sLit "Ambiguous constraint") <+> quotes (pprPred pred),
1242 nest 2 (ptext (sLit "At least one of the forall'd type variables mentioned by the constraint") $$
1243 ptext (sLit "must be reachable from the type after the '=>'"))]
1246 Note [Growing the tau-tvs using constraints]
1247 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1248 (growInstsTyVars insts tvs) is the result of extending the set
1249 of tyvars tvs using all conceivable links from pred
1251 E.g. tvs = {a}, preds = {H [a] b, K (b,Int) c, Eq e}
1252 Then grow precs tvs = {a,b,c}
1255 growThetaTyVars :: TcThetaType -> TyVarSet -> TyVarSet
1256 -- See Note [Growing the tau-tvs using constraints]
1257 growThetaTyVars theta tvs
1259 | otherwise = fixVarSet mk_next tvs
1261 mk_next tvs = foldr grow_one tvs theta
1262 grow_one pred tvs = growPredTyVars pred tvs `unionVarSet` tvs
1264 growPredTyVars :: TcPredType
1265 -> TyVarSet -- The set to extend
1266 -> TyVarSet -- TyVars of the predicate if it intersects
1267 -- the set, or is implicit parameter
1268 growPredTyVars pred tvs
1269 | IParam {} <- pred = pred_tvs -- See Note [Implicit parameters and ambiguity]
1270 | pred_tvs `intersectsVarSet` tvs = pred_tvs
1271 | otherwise = emptyVarSet
1273 pred_tvs = tyVarsOfPred pred
1276 Note [Implicit parameters and ambiguity]
1277 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1278 Only a *class* predicate can give rise to ambiguity
1279 An *implicit parameter* cannot. For example:
1280 foo :: (?x :: [a]) => Int
1282 is fine. The call site will suppply a particular 'x'
1284 Furthermore, the type variables fixed by an implicit parameter
1285 propagate to the others. E.g.
1286 foo :: (Show a, ?x::[a]) => Int
1288 The type of foo looks ambiguous. But it isn't, because at a call site
1290 let ?x = 5::Int in foo
1291 and all is well. In effect, implicit parameters are, well, parameters,
1292 so we can take their type variables into account as part of the
1293 "tau-tvs" stuff. This is done in the function 'FunDeps.grow'.
1297 checkThetaCtxt :: SourceTyCtxt -> ThetaType -> SDoc
1298 checkThetaCtxt ctxt theta
1299 = vcat [ptext (sLit "In the context:") <+> pprTheta theta,
1300 ptext (sLit "While checking") <+> pprSourceTyCtxt ctxt ]
1302 badPredTyErr, eqPredTyErr, predTyVarErr :: PredType -> SDoc
1303 badPredTyErr sty = ptext (sLit "Illegal constraint") <+> pprPred sty
1304 eqPredTyErr sty = ptext (sLit "Illegal equational constraint") <+> pprPred sty
1306 parens (ptext (sLit "Use -XTypeFamilies to permit this"))
1307 predTyVarErr pred = sep [ptext (sLit "Non type-variable argument"),
1308 nest 2 (ptext (sLit "in the constraint:") <+> pprPred pred)]
1309 dupPredWarn :: [[PredType]] -> SDoc
1310 dupPredWarn dups = ptext (sLit "Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
1312 arityErr :: Outputable a => String -> a -> Int -> Int -> SDoc
1313 arityErr kind name n m
1314 = hsep [ text kind, quotes (ppr name), ptext (sLit "should have"),
1315 n_arguments <> comma, text "but has been given",
1316 if m==0 then text "none" else int m]
1318 n_arguments | n == 0 = ptext (sLit "no arguments")
1319 | n == 1 = ptext (sLit "1 argument")
1320 | True = hsep [int n, ptext (sLit "arguments")]
1323 %************************************************************************
1325 \subsection{Checking for a decent instance head type}
1327 %************************************************************************
1329 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1330 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1332 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1333 flag is on, or (2)~the instance is imported (they must have been
1334 compiled elsewhere). In these cases, we let them go through anyway.
1336 We can also have instances for functions: @instance Foo (a -> b) ...@.
1339 checkValidInstHead :: Type -> TcM (Class, [TcType])
1341 checkValidInstHead ty -- Should be a source type
1342 = case tcSplitPredTy_maybe ty of {
1343 Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
1346 case getClassPredTys_maybe pred of {
1347 Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
1348 Just (clas,tys) -> do
1351 check_inst_head dflags clas tys
1355 check_inst_head :: DynFlags -> Class -> [Type] -> TcM ()
1356 check_inst_head dflags clas tys
1357 = do { -- If GlasgowExts then check at least one isn't a type variable
1358 ; checkTc (dopt Opt_TypeSynonymInstances dflags ||
1359 all tcInstHeadTyNotSynonym tys)
1360 (instTypeErr (pprClassPred clas tys) head_type_synonym_msg)
1361 ; checkTc (dopt Opt_FlexibleInstances dflags ||
1362 all tcInstHeadTyAppAllTyVars tys)
1363 (instTypeErr (pprClassPred clas tys) head_type_args_tyvars_msg)
1364 ; checkTc (dopt Opt_MultiParamTypeClasses dflags ||
1366 (instTypeErr (pprClassPred clas tys) head_one_type_msg)
1367 -- May not contain type family applications
1368 ; mapM_ checkTyFamFreeness tys
1370 ; mapM_ checkValidMonoType tys
1371 -- For now, I only allow tau-types (not polytypes) in
1372 -- the head of an instance decl.
1373 -- E.g. instance C (forall a. a->a) is rejected
1374 -- One could imagine generalising that, but I'm not sure
1375 -- what all the consequences might be
1379 head_type_synonym_msg = parens (
1380 text "All instance types must be of the form (T t1 ... tn)" $$
1381 text "where T is not a synonym." $$
1382 text "Use -XTypeSynonymInstances if you want to disable this.")
1384 head_type_args_tyvars_msg = parens (vcat [
1385 text "All instance types must be of the form (T a1 ... an)",
1386 text "where a1 ... an are type *variables*,",
1387 text "and each type variable appears at most once in the instance head.",
1388 text "Use -XFlexibleInstances if you want to disable this."])
1390 head_one_type_msg = parens (
1391 text "Only one type can be given in an instance head." $$
1392 text "Use -XMultiParamTypeClasses if you want to allow more.")
1394 instTypeErr :: SDoc -> SDoc -> SDoc
1395 instTypeErr pp_ty msg
1396 = sep [ptext (sLit "Illegal instance declaration for") <+> quotes pp_ty,
1401 %************************************************************************
1403 \subsection{Checking instance for termination}
1405 %************************************************************************
1408 checkValidInstance :: LHsType Name -> [TyVar] -> ThetaType -> Type
1409 -> TcM (Class, [TcType])
1410 checkValidInstance hs_type tyvars theta tau
1411 = setSrcSpan (getLoc hs_type) $
1412 do { (clas, inst_tys) <- setSrcSpan head_loc $
1413 checkValidInstHead tau
1415 ; undecidable_ok <- doptM Opt_UndecidableInstances
1417 ; checkValidTheta InstThetaCtxt theta
1418 ; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys)
1420 -- Check that instance inference will terminate (if we care)
1421 -- For Haskell 98 this will already have been done by checkValidTheta,
1422 -- but as we may be using other extensions we need to check.
1423 ; unless undecidable_ok $
1424 mapM_ addErrTc (checkInstTermination inst_tys theta)
1426 -- The Coverage Condition
1427 ; checkTc (undecidable_ok || checkInstCoverage clas inst_tys)
1428 (instTypeErr (pprClassPred clas inst_tys) msg)
1430 ; return (clas, inst_tys)
1433 msg = parens (vcat [ptext (sLit "the Coverage Condition fails for one of the functional dependencies;"),
1436 -- The location of the "head" of the instance
1437 head_loc = case hs_type of
1438 L _ (HsForAllTy _ _ _ (L loc _)) -> loc
1442 Termination test: the so-called "Paterson conditions" (see Section 5 of
1443 "Understanding functionsl dependencies via Constraint Handling Rules,
1446 We check that each assertion in the context satisfies:
1447 (1) no variable has more occurrences in the assertion than in the head, and
1448 (2) the assertion has fewer constructors and variables (taken together
1449 and counting repetitions) than the head.
1450 This is only needed with -fglasgow-exts, as Haskell 98 restrictions
1451 (which have already been checked) guarantee termination.
1453 The underlying idea is that
1455 for any ground substitution, each assertion in the
1456 context has fewer type constructors than the head.
1460 checkInstTermination :: [TcType] -> ThetaType -> [Message]
1461 checkInstTermination tys theta
1462 = mapCatMaybes check theta
1465 size = sizeTypes tys
1467 | not (null (fvPred pred \\ fvs))
1468 = Just (predUndecErr pred nomoreMsg $$ parens undecidableMsg)
1469 | sizePred pred >= size
1470 = Just (predUndecErr pred smallerMsg $$ parens undecidableMsg)
1474 predUndecErr :: PredType -> SDoc -> SDoc
1475 predUndecErr pred msg = sep [msg,
1476 nest 2 (ptext (sLit "in the constraint:") <+> pprPred pred)]
1478 nomoreMsg, smallerMsg, undecidableMsg :: SDoc
1479 nomoreMsg = ptext (sLit "Variable occurs more often in a constraint than in the instance head")
1480 smallerMsg = ptext (sLit "Constraint is no smaller than the instance head")
1481 undecidableMsg = ptext (sLit "Use -XUndecidableInstances to permit this")
1484 validDeivPred checks for OK 'deriving' context. See Note [Exotic
1485 derived instance contexts] in TcSimplify. However the predicate is
1486 here because it uses sizeTypes, fvTypes.
1489 validDerivPred :: PredType -> Bool
1490 validDerivPred (ClassP _ tys) = hasNoDups fvs && sizeTypes tys == length fvs
1491 where fvs = fvTypes tys
1492 validDerivPred _ = False
1496 %************************************************************************
1498 Checking type instance well-formedness and termination
1500 %************************************************************************
1503 -- Check that a "type instance" is well-formed (which includes decidability
1504 -- unless -XUndecidableInstances is given).
1506 checkValidTypeInst :: [Type] -> Type -> TcM ()
1507 checkValidTypeInst typats rhs
1508 = do { -- left-hand side contains no type family applications
1509 -- (vanilla synonyms are fine, though)
1510 ; mapM_ checkTyFamFreeness typats
1512 -- the right-hand side is a tau type
1513 ; checkValidMonoType rhs
1515 -- we have a decidable instance unless otherwise permitted
1516 ; undecidable_ok <- doptM Opt_UndecidableInstances
1517 ; unless undecidable_ok $
1518 mapM_ addErrTc (checkFamInst typats (tyFamInsts rhs))
1521 -- Make sure that each type family instance is
1522 -- (1) strictly smaller than the lhs,
1523 -- (2) mentions no type variable more often than the lhs, and
1524 -- (3) does not contain any further type family instances.
1526 checkFamInst :: [Type] -- lhs
1527 -> [(TyCon, [Type])] -- type family instances
1529 checkFamInst lhsTys famInsts
1530 = mapCatMaybes check famInsts
1532 size = sizeTypes lhsTys
1533 fvs = fvTypes lhsTys
1535 | not (all isTyFamFree tys)
1536 = Just (famInstUndecErr famInst nestedMsg $$ parens undecidableMsg)
1537 | not (null (fvTypes tys \\ fvs))
1538 = Just (famInstUndecErr famInst nomoreVarMsg $$ parens undecidableMsg)
1539 | size <= sizeTypes tys
1540 = Just (famInstUndecErr famInst smallerAppMsg $$ parens undecidableMsg)
1544 famInst = TyConApp tc tys
1546 -- Ensure that no type family instances occur in a type.
1548 checkTyFamFreeness :: Type -> TcM ()
1549 checkTyFamFreeness ty
1550 = checkTc (isTyFamFree ty) $
1551 tyFamInstIllegalErr ty
1553 -- Check that a type does not contain any type family applications.
1555 isTyFamFree :: Type -> Bool
1556 isTyFamFree = null . tyFamInsts
1560 tyFamInstIllegalErr :: Type -> SDoc
1561 tyFamInstIllegalErr ty
1562 = hang (ptext (sLit "Illegal type synonym family application in instance") <>
1566 famInstUndecErr :: Type -> SDoc -> SDoc
1567 famInstUndecErr ty msg
1569 nest 2 (ptext (sLit "in the type family application:") <+>
1572 nestedMsg, nomoreVarMsg, smallerAppMsg :: SDoc
1573 nestedMsg = ptext (sLit "Nested type family application")
1574 nomoreVarMsg = ptext (sLit "Variable occurs more often than in instance head")
1575 smallerAppMsg = ptext (sLit "Application is no smaller than the instance head")
1579 %************************************************************************
1581 \subsection{Auxiliary functions}
1583 %************************************************************************
1586 -- Free variables of a type, retaining repetitions, and expanding synonyms
1587 fvType :: Type -> [TyVar]
1588 fvType ty | Just exp_ty <- tcView ty = fvType exp_ty
1589 fvType (TyVarTy tv) = [tv]
1590 fvType (TyConApp _ tys) = fvTypes tys
1591 fvType (PredTy pred) = fvPred pred
1592 fvType (FunTy arg res) = fvType arg ++ fvType res
1593 fvType (AppTy fun arg) = fvType fun ++ fvType arg
1594 fvType (ForAllTy tyvar ty) = filter (/= tyvar) (fvType ty)
1596 fvTypes :: [Type] -> [TyVar]
1597 fvTypes tys = concat (map fvType tys)
1599 fvPred :: PredType -> [TyVar]
1600 fvPred (ClassP _ tys') = fvTypes tys'
1601 fvPred (IParam _ ty) = fvType ty
1602 fvPred (EqPred ty1 ty2) = fvType ty1 ++ fvType ty2
1604 -- Size of a type: the number of variables and constructors
1605 sizeType :: Type -> Int
1606 sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty
1607 sizeType (TyVarTy _) = 1
1608 sizeType (TyConApp _ tys) = sizeTypes tys + 1
1609 sizeType (PredTy pred) = sizePred pred
1610 sizeType (FunTy arg res) = sizeType arg + sizeType res + 1
1611 sizeType (AppTy fun arg) = sizeType fun + sizeType arg
1612 sizeType (ForAllTy _ ty) = sizeType ty
1614 sizeTypes :: [Type] -> Int
1615 sizeTypes xs = sum (map sizeType xs)
1617 -- Size of a predicate
1619 -- Equalities are a special case. The equality itself doesn't contribute to the
1620 -- size and as we do not count class predicates, we have to start with one less.
1621 -- This is easy to see considering that, given
1622 -- class C a b | a -> b
1624 -- constraints (C a b) and (F a ~ b) are equivalent in size.
1625 sizePred :: PredType -> Int
1626 sizePred (ClassP _ tys') = sizeTypes tys'
1627 sizePred (IParam _ ty) = sizeType ty
1628 sizePred (EqPred ty1 ty2) = sizeType ty1 + sizeType ty2 - 1