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, instMetaTyVar,
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,
63 readKindVar, writeKindVar
66 #include "HsVersions.h"
78 import HsSyn -- HsType
79 import TcRnMonad -- TcType, amongst others
96 import Data.List ( (\\) )
100 %************************************************************************
104 %************************************************************************
107 newKindVar :: TcM TcKind
108 newKindVar = do { uniq <- newUnique
109 ; ref <- newMutVar Flexi
110 ; return (mkTyVarTy (mkKindVar uniq ref)) }
112 newKindVars :: Int -> TcM [TcKind]
113 newKindVars n = mapM (\ _ -> newKindVar) (nOfThem n ())
117 %************************************************************************
119 Evidence variables; range over constraints we can abstract over
121 %************************************************************************
124 newEvVars :: TcThetaType -> TcM [EvVar]
125 newEvVars theta = mapM newEvVar theta
127 newWantedEvVar :: TcPredType -> TcM EvVar
128 newWantedEvVar (EqPred ty1 ty2) = newWantedCoVar ty1 ty2
129 newWantedEvVar (ClassP cls tys) = newDict cls tys
130 newWantedEvVar (IParam ip ty) = newIP ip ty
132 newWantedEvVars :: TcThetaType -> TcM [EvVar]
133 newWantedEvVars theta = mapM newWantedEvVar theta
135 newWantedCoVar :: TcType -> TcType -> TcM CoVar
136 newWantedCoVar ty1 ty2 = newCoVar ty1 ty2
138 -- We used to create a mutable co-var
140 -- A wanted coercion variable is a MetaTyVar
141 -- that can be filled in with its binding
142 = do { uniq <- newUnique
143 ; ref <- newMutVar Flexi
144 ; let name = mkSysTvName uniq (fsLit "c")
145 kind = mkPredTy (EqPred ty1 ty2)
146 ; return (mkTcTyVar name kind (MetaTv TauTv ref)) }
150 newEvVar :: TcPredType -> TcM EvVar
151 -- Creates new *rigid* variables for predicates
152 newEvVar (EqPred ty1 ty2) = newCoVar ty1 ty2
153 newEvVar (ClassP cls tys) = newDict cls tys
154 newEvVar (IParam ip ty) = newIP ip ty
156 newCoVar :: TcType -> TcType -> TcM CoVar
158 = do { name <- newName (mkTyVarOccFS (fsLit "co"))
159 ; return (mkCoVar name (mkPredTy (EqPred ty1 ty2))) }
161 newIP :: IPName Name -> TcType -> TcM IpId
163 = do { name <- newName (getOccName (ipNameName ip))
164 ; return (mkLocalId name (mkPredTy (IParam ip ty))) }
166 newDict :: Class -> [TcType] -> TcM DictId
168 = do { name <- newName (mkDictOcc (getOccName cls))
169 ; return (mkLocalId name (mkPredTy (ClassP cls tys))) }
171 newName :: OccName -> TcM Name
173 = do { uniq <- newUnique
175 ; return (mkInternalName uniq occ loc) }
178 newKindConstraint :: Type -> Kind -> TcM (CoVar, Type)
179 -- Create a new wanted CoVar that constrains the type
180 -- to have the specified kind
181 newKindConstraint ty kind
182 = do { ty_k <- newFlexiTyVarTy kind
183 ; co_var <- newWantedCoVar ty ty_k
184 ; return (co_var, ty_k) }
187 newSelfDict :: Class -> [TcType] -> TcM DictId
188 -- Make a dictionary for "self". It behaves just like a normal DictId
189 -- except that it responds True to isSelfDict
190 -- This is used only to suppress confusing error reports
192 = do { uniq <- newUnique
193 ; let name = mkSystemName uniq selfDictOcc
194 ; return (mkLocalId name (mkPredTy (ClassP cls tys))) }
196 selfDictOcc :: OccName
197 selfDictOcc = mkVarOcc "self"
199 isSelfDict :: EvVar -> Bool
200 isSelfDict v = isSystemName (Var.varName v)
201 -- Notice that all *other* evidence variables get Internal Names
205 %************************************************************************
207 SkolemTvs (immutable)
209 %************************************************************************
212 tcInstType :: ([TyVar] -> TcM [TcTyVar]) -- How to instantiate the type variables
213 -> TcType -- Type to instantiate
214 -> TcM ([TcTyVar], TcThetaType, TcType) -- Result
215 -- (type vars (excl coercion vars), preds (incl equalities), rho)
216 tcInstType inst_tyvars ty
217 = case tcSplitForAllTys ty of
218 ([], rho) -> let -- There may be overloading despite no type variables;
219 -- (?x :: Int) => Int -> Int
220 (theta, tau) = tcSplitPhiTy rho
222 return ([], theta, tau)
224 (tyvars, rho) -> do { tyvars' <- inst_tyvars tyvars
226 ; let tenv = zipTopTvSubst tyvars (mkTyVarTys tyvars')
227 -- Either the tyvars are freshly made, by inst_tyvars,
228 -- or (in the call from tcSkolSigType) any nested foralls
229 -- have different binders. Either way, zipTopTvSubst is ok
231 ; let (theta, tau) = tcSplitPhiTy (substTy tenv rho)
232 ; return (tyvars', theta, tau) }
234 mkSkolTyVar :: Name -> Kind -> SkolemInfo -> TcTyVar
235 mkSkolTyVar name kind info = mkTcTyVar name kind (SkolemTv info)
237 tcSkolSigType :: SkolemInfo -> Type -> TcM ([TcTyVar], TcThetaType, TcType)
238 -- Instantiate a type signature with skolem constants, but
239 -- do *not* give them fresh names, because we want the name to
240 -- be in the type environment: it is lexically scoped.
241 tcSkolSigType info ty = tcInstType (\tvs -> return (tcSkolSigTyVars info tvs)) ty
243 tcSkolSigTyVars :: SkolemInfo -> [TyVar] -> [TcTyVar]
244 -- Make skolem constants, but do *not* give them new names, as above
245 tcSkolSigTyVars info tyvars = [ mkSkolTyVar (tyVarName tv) (tyVarKind tv) info
248 tcInstSkolTyVar :: SkolemInfo -> TyVar -> TcM TcTyVar
249 -- Instantiate the tyvar, using
250 -- * the occ-name and kind of the supplied tyvar,
251 -- * the unique from the monad,
252 -- * the location either from the tyvar (skol_info = SigSkol)
253 -- or from the monad (otehrwise)
254 tcInstSkolTyVar skol_info tyvar
255 = do { uniq <- newUnique
256 ; loc <- case skol_info of
257 SigSkol {} -> return (getSrcSpan old_name)
259 ; let new_name = mkInternalName uniq occ loc
260 ; return (mkSkolTyVar new_name kind skol_info) }
262 old_name = tyVarName tyvar
263 occ = nameOccName old_name
264 kind = tyVarKind tyvar
266 tcInstSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
267 -- Get the location from the monad
268 tcInstSkolTyVars info tyvars
269 = mapM (tcInstSkolTyVar info) tyvars
271 tcInstSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
272 -- Instantiate a type with fresh skolem constants
273 -- Binding location comes from the monad
274 tcInstSkolType info ty = tcInstType (tcInstSkolTyVars info) ty
276 tcInstSigType :: Bool -> Name -> TcType -> TcM ([TcTyVar], TcThetaType, TcRhoType)
277 -- Instantiate with skolems or meta SigTvs; depending on use_skols
278 -- Always take location info from the supplied tyvars
279 tcInstSigType use_skols name ty
281 = tcInstType (tcInstSkolTyVars (SigSkol (FunSigCtxt name))) ty
283 = tcInstType tcInstSigTyVars ty
285 tcInstSigTyVars :: [TyVar] -> TcM [TcTyVar]
286 -- Make meta SigTv type variables for patten-bound scoped type varaibles
287 -- We use SigTvs for them, so that they can't unify with arbitrary types
288 tcInstSigTyVars = mapM (\tv -> instMetaTyVar (SigTv (tyVarName tv)) tv)
289 -- ToDo: the "function binding site is bogus
293 %************************************************************************
295 MetaTvs (meta type variables; mutable)
297 %************************************************************************
300 newMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar
301 -- Make a new meta tyvar out of thin air
302 newMetaTyVar meta_info kind
303 = do { uniq <- newMetaUnique
304 ; ref <- newMutVar Flexi
305 ; let name = mkSysTvName uniq fs
306 fs = case meta_info of
310 ; return (mkTcTyVar name kind (MetaTv meta_info ref)) }
312 instMetaTyVar :: MetaInfo -> TyVar -> TcM TcTyVar
313 -- Make a new meta tyvar whose Name and Kind
314 -- come from an existing TyVar
315 instMetaTyVar meta_info tyvar
316 = do { uniq <- newMetaUnique
317 ; ref <- newMutVar Flexi
318 ; let name = setNameUnique (tyVarName tyvar) uniq
319 kind = tyVarKind tyvar
320 ; return (mkTcTyVar name kind (MetaTv meta_info ref)) }
322 readMetaTyVar :: TyVar -> TcM MetaDetails
323 readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
324 readMutVar (metaTvRef tyvar)
326 readWantedCoVar :: CoVar -> TcM MetaDetails
327 readWantedCoVar covar = ASSERT2( isMetaTyVar covar, ppr covar )
328 readMutVar (metaTvRef covar)
332 isFilledMetaTyVar :: TyVar -> TcM Bool
333 -- True of a filled-in (Indirect) meta type variable
335 | not (isTcTyVar tv) = return False
336 | MetaTv _ ref <- tcTyVarDetails tv
337 = do { details <- readMutVar ref
338 ; return (isIndirect details) }
339 | otherwise = return False
341 isFlexiMetaTyVar :: TyVar -> TcM Bool
342 -- True of a un-filled-in (Flexi) meta type variable
344 | not (isTcTyVar tv) = return False
345 | MetaTv _ ref <- tcTyVarDetails tv
346 = do { details <- readMutVar ref
347 ; return (isFlexi details) }
348 | otherwise = return False
351 writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
352 -- Write into a currently-empty MetaTyVar
354 writeMetaTyVar tyvar ty
356 = writeMetaTyVarRef tyvar (metaTvRef tyvar) ty
358 -- Everything from here on only happens if DEBUG is on
359 | not (isTcTyVar tyvar)
360 = WARN( True, text "Writing to non-tc tyvar" <+> ppr tyvar )
363 | MetaTv _ ref <- tcTyVarDetails tyvar
364 = writeMetaTyVarRef tyvar ref ty
367 = WARN( True, text "Writing to non-meta tyvar" <+> ppr tyvar )
370 writeWantedCoVar :: CoVar -> Coercion -> TcM ()
371 writeWantedCoVar cv co = writeMetaTyVar cv co
374 writeMetaTyVarRef :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM ()
375 -- Here the tyvar is for error checking only;
376 -- the ref cell must be for the same tyvar
377 writeMetaTyVarRef tyvar ref ty
379 = do { traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
380 ; writeMutVar ref (Indirect ty) }
382 -- Everything from here on only happens if DEBUG is on
383 | not (isPredTy tv_kind) -- Don't check kinds for updates to coercion variables
384 , not (ty_kind `isSubKind` tv_kind)
385 = WARN( True, hang (text "Ill-kinded update to meta tyvar")
386 2 (ppr tyvar $$ ppr tv_kind $$ ppr ty $$ ppr ty_kind) )
390 = do { meta_details <- readMutVar ref;
391 ; WARN( not (isFlexi meta_details),
392 hang (text "Double update of meta tyvar")
393 2 (ppr tyvar $$ ppr meta_details) )
395 traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
396 ; writeMutVar ref (Indirect ty) }
398 tv_kind = tyVarKind tyvar
399 ty_kind = typeKind ty
403 %************************************************************************
407 %************************************************************************
410 newFlexiTyVar :: Kind -> TcM TcTyVar
411 newFlexiTyVar kind = newMetaTyVar TauTv kind
413 newFlexiTyVarTy :: Kind -> TcM TcType
414 newFlexiTyVarTy kind = do
415 tc_tyvar <- newFlexiTyVar kind
416 return (TyVarTy tc_tyvar)
418 newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
419 newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind)
421 tcInstTyVar :: TyVar -> TcM TcTyVar
422 -- Instantiate with a META type variable
423 tcInstTyVar tyvar = instMetaTyVar TauTv tyvar
425 tcInstTyVars :: [TyVar] -> TcM ([TcTyVar], [TcType], TvSubst)
426 -- Instantiate with META type variables
428 = do { tc_tvs <- mapM tcInstTyVar tyvars
429 ; let tys = mkTyVarTys tc_tvs
430 ; return (tc_tvs, tys, zipTopTvSubst tyvars tys) }
431 -- Since the tyvars are freshly made,
432 -- they cannot possibly be captured by
433 -- any existing for-alls. Hence zipTopTvSubst
437 %************************************************************************
441 %************************************************************************
444 zonkSigTyVar :: TcTyVar -> TcM TcTyVar
446 | isSkolemTyVar sig_tv
447 = return sig_tv -- Happens in the call in TcBinds.checkDistinctTyVars
449 = ASSERT( isSigTyVar sig_tv )
450 do { ty <- zonkTcTyVar sig_tv
451 ; return (tcGetTyVar "zonkSigTyVar" ty) }
452 -- 'ty' is bound to be a type variable, because SigTvs
453 -- can only be unified with type variables
458 %************************************************************************
460 \subsection{Zonking -- the exernal interfaces}
462 %************************************************************************
464 @tcGetGlobalTyVars@ returns a fully-zonked set of tyvars free in the environment.
465 To improve subsequent calls to the same function it writes the zonked set back into
469 tcGetGlobalTyVars :: TcM TcTyVarSet
471 = do { (TcLclEnv {tcl_tyvars = gtv_var}) <- getLclEnv
472 ; gbl_tvs <- readMutVar gtv_var
473 ; gbl_tvs' <- zonkTcTyVarsAndFV gbl_tvs
474 ; writeMutVar gtv_var gbl_tvs'
478 ----------------- Type variables
481 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
482 zonkTcTyVars tyvars = mapM zonkTcTyVar tyvars
484 zonkTcTyVarsAndFV :: TcTyVarSet -> TcM TcTyVarSet
485 zonkTcTyVarsAndFV tyvars = tyVarsOfTypes <$> mapM zonkTcTyVar (varSetElems tyvars)
487 ----------------- Types
489 zonkTcTypeCarefully :: TcType -> TcM TcType
490 -- Do not zonk type variables free in the environment
491 zonkTcTypeCarefully ty
492 = do { env_tvs <- tcGetGlobalTyVars
493 ; zonkType (zonk_tv env_tvs) ty }
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 (zonk_tv env_tvs) ty
503 MetaTv _ ref -> do { cts <- readMutVar ref
505 Flexi -> return (TyVarTy tv)
506 Indirect ty -> zonkType (zonk_tv 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 zonkTcTypeAndSubst :: TvSubst -> TcType -> TcM TcType
525 -- Zonk, and simultaneously apply a non-necessarily-idempotent substitution
526 zonkTcTypeAndSubst subst ty = zonkType zonk_tv ty
529 = case tcTyVarDetails tv of
530 SkolemTv {} -> return (TyVarTy tv)
531 FlatSkol ty -> zonkType zonk_tv ty
532 MetaTv _ ref -> do { cts <- readMutVar ref
534 Flexi -> zonk_flexi tv
535 Indirect ty -> zonkType zonk_tv ty }
537 = case lookupTyVar subst tv of
538 Just ty -> zonkType zonk_tv ty
539 Nothing -> return (TyVarTy tv)
541 zonkTcTypes :: [TcType] -> TcM [TcType]
542 zonkTcTypes tys = mapM zonkTcType tys
544 zonkTcThetaType :: TcThetaType -> TcM TcThetaType
545 zonkTcThetaType theta = mapM zonkTcPredType theta
547 zonkTcPredType :: TcPredType -> TcM TcPredType
548 zonkTcPredType (ClassP c ts) = ClassP c <$> zonkTcTypes ts
549 zonkTcPredType (IParam n t) = IParam n <$> zonkTcType t
550 zonkTcPredType (EqPred t1 t2) = EqPred <$> zonkTcType t1 <*> zonkTcType t2
553 ------------------- These ...ToType, ...ToKind versions
554 are used at the end of type checking
557 zonkQuantifiedTyVars :: [TcTyVar] -> TcM [TcTyVar]
558 zonkQuantifiedTyVars = mapM zonkQuantifiedTyVar
560 zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar
561 -- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it.
563 -- The quantified type variables often include meta type variables
564 -- we want to freeze them into ordinary type variables, and
565 -- default their kind (e.g. from OpenTypeKind to TypeKind)
566 -- -- see notes with Kind.defaultKind
567 -- The meta tyvar is updated to point to the new skolem TyVar. Now any
568 -- bound occurences of the original type variable will get zonked to
569 -- the immutable version.
571 -- We leave skolem TyVars alone; they are immutable.
572 zonkQuantifiedTyVar tv
573 | ASSERT2( isTcTyVar tv, ppr tv )
575 = do { kind <- zonkTcType (tyVarKind tv)
576 ; return $ setTyVarKind tv kind
578 -- It might be a skolem type variable,
579 -- for example from a user type signature
581 | otherwise -- It's a meta-type-variable
582 = do { details <- readMetaTyVar tv
584 -- Create the new, frozen, skolem type variable
585 -- We zonk to a skolem, not to a regular TcVar
586 -- See Note [Zonking to Skolem]
587 ; uniq <- newUnique -- Remove it from TcMetaTyVar unique land
588 ; let final_kind = defaultKind (tyVarKind tv)
589 final_name = setNameUnique (tyVarName tv) uniq
590 final_tv = mkSkolTyVar final_name final_kind UnkSkol
592 -- Bind the meta tyvar to the new tyvar
594 Indirect ty -> WARN( True, ppr tv $$ ppr ty )
596 -- [Sept 04] I don't think this should happen
597 -- See note [Silly Type Synonym]
599 Flexi -> writeMetaTyVar tv (mkTyVarTy final_tv)
601 -- Return the new tyvar
606 zonkImplication :: Implication -> TcM Implication
607 zonkImplication implic@(Implic { ic_given = given
608 , ic_wanted = wanted })
609 = do { given' <- mapM zonkEvVar given
610 ; wanted' <- mapBagM zonkWanted wanted
611 ; return (implic { ic_given = given', ic_wanted = wanted' }) }
613 zonkEvVar :: EvVar -> TcM EvVar
614 zonkEvVar var = do { ty' <- zonkTcType (varType var)
615 ; return (setVarType var ty') }
617 zonkWanted :: WantedConstraint -> TcM WantedConstraint
618 zonkWanted (WcImplic imp) = do { imp' <- zonkImplication imp; return (WcImplic imp') }
619 zonkWanted (WcEvVar ev) = do { ev' <- zonkWantedEvVar ev; return (WcEvVar ev') }
621 zonkWantedEvVar :: WantedEvVar -> TcM WantedEvVar
622 zonkWantedEvVar (WantedEvVar v l) = do { v' <- zonkEvVar v; return (WantedEvVar v' l) }
626 Note [Silly Type Synonyms]
627 ~~~~~~~~~~~~~~~~~~~~~~~~~~
629 type C u a = u -- Note 'a' unused
631 foo :: (forall a. C u a -> C u a) -> u
635 bar = foo (\t -> t + t)
637 * From the (\t -> t+t) we get type {Num d} => d -> d
640 * Now unify with type of foo's arg, and we get:
641 {Num (C d a)} => C d a -> C d a
644 * Now abstract over the 'a', but float out the Num (C d a) constraint
645 because it does not 'really' mention a. (see exactTyVarsOfType)
646 The arg to foo becomes
649 * So we get a dict binding for Num (C d a), which is zonked to give
651 [Note Sept 04: now that we are zonking quantified type variables
652 on construction, the 'a' will be frozen as a regular tyvar on
653 quantification, so the floated dict will still have type (C d a).
654 Which renders this whole note moot; happily!]
656 * Then the \/\a abstraction has a zonked 'a' in it.
658 All very silly. I think its harmless to ignore the problem. We'll end up with
659 a \/\a in the final result but all the occurrences of a will be zonked to ()
661 Note [Zonking to Skolem]
662 ~~~~~~~~~~~~~~~~~~~~~~~~
663 We used to zonk quantified type variables to regular TyVars. However, this
664 leads to problems. Consider this program from the regression test suite:
666 eval :: Int -> String -> String -> String
667 eval 0 root actual = evalRHS 0 root actual
670 evalRHS 0 root actual = eval 0 root actual
672 It leads to the deferral of an equality (wrapped in an implication constraint)
674 forall a. (String -> String -> String) ~ a
676 which is propagated up to the toplevel (see TcSimplify.tcSimplifyInferCheck).
677 In the meantime `a' is zonked and quantified to form `evalRHS's signature.
678 This has the *side effect* of also zonking the `a' in the deferred equality
679 (which at this point is being handed around wrapped in an implication
682 Finally, the equality (with the zonked `a') will be handed back to the
683 simplifier by TcRnDriver.tcRnSrcDecls calling TcSimplify.tcSimplifyTop.
684 If we zonk `a' with a regular type variable, we will have this regular type
685 variable now floating around in the simplifier, which in many places assumes to
686 only see proper TcTyVars.
688 We can avoid this problem by zonking with a skolem. The skolem is rigid
689 (which we require for a quantified variable), but is still a TcTyVar that the
690 simplifier knows how to deal with.
693 %************************************************************************
695 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
697 %* For internal use only! *
699 %************************************************************************
702 -- For unbound, mutable tyvars, zonkType uses the function given to it
703 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
704 -- type variable and zonks the kind too
706 zonkType :: (TcTyVar -> TcM Type) -- What to do with unbound mutable type variables
707 -- see zonkTcType, and zonkTcTypeToType
710 zonkType zonk_tc_tyvar ty
713 go (TyConApp tc tys) = do tys' <- mapM go tys
714 return (TyConApp tc tys')
716 go (PredTy p) = do p' <- go_pred p
719 go (FunTy arg res) = do arg' <- go arg
721 return (FunTy arg' res')
723 go (AppTy fun arg) = do fun' <- go fun
725 return (mkAppTy fun' arg')
726 -- NB the mkAppTy; we might have instantiated a
727 -- type variable to a type constructor, so we need
728 -- to pull the TyConApp to the top.
730 -- The two interesting cases!
731 go (TyVarTy tyvar) | isTcTyVar tyvar = zonk_tc_tyvar tyvar
732 | otherwise = liftM TyVarTy $
733 zonkTyVar zonk_tc_tyvar tyvar
734 -- Ordinary (non Tc) tyvars occur inside quantified types
736 go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar ) do
738 tyvar' <- zonkTyVar zonk_tc_tyvar tyvar
739 return (ForAllTy tyvar' ty')
741 go_pred (ClassP c tys) = do tys' <- mapM go tys
742 return (ClassP c tys')
743 go_pred (IParam n ty) = do ty' <- go ty
744 return (IParam n ty')
745 go_pred (EqPred ty1 ty2) = do ty1' <- go ty1
747 return (EqPred ty1' ty2')
749 mkZonkTcTyVar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable var
750 -> TcTyVar -> TcM TcType
751 mkZonkTcTyVar unbound_var_fn tyvar
752 = ASSERT( isTcTyVar tyvar )
753 case tcTyVarDetails tyvar of
754 SkolemTv {} -> return (TyVarTy tyvar)
755 FlatSkol ty -> zonkType (mkZonkTcTyVar unbound_var_fn) ty
756 MetaTv _ ref -> do { cts <- readMutVar ref
758 Flexi -> unbound_var_fn tyvar
759 Indirect ty -> zonkType (mkZonkTcTyVar unbound_var_fn) ty }
761 -- Zonk the kind of a non-TC tyvar in case it is a coercion variable
762 -- (their kind contains types).
763 zonkTyVar :: (TcTyVar -> TcM Type) -- What to do for a TcTyVar
764 -> TyVar -> TcM TyVar
765 zonkTyVar zonk_tc_tyvar tv
767 = do { kind <- zonkType zonk_tc_tyvar (tyVarKind tv)
768 ; return $ setTyVarKind tv kind }
769 | otherwise = return tv
774 %************************************************************************
778 %************************************************************************
781 readKindVar :: KindVar -> TcM (MetaDetails)
782 writeKindVar :: KindVar -> TcKind -> TcM ()
783 readKindVar kv = readMutVar (kindVarRef kv)
784 writeKindVar kv val = writeMutVar (kindVarRef kv) (Indirect val)
787 zonkTcKind :: TcKind -> TcM TcKind
788 zonkTcKind k = zonkTcType k
791 zonkTcKindToKind :: TcKind -> TcM Kind
792 -- When zonking a TcKind to a kind, we need to instantiate kind variables,
793 -- Haskell specifies that * is to be used, so we follow that.
795 = zonkType (mkZonkTcTyVar (\ _ -> return liftedTypeKind)) k
798 %************************************************************************
800 \subsection{Checking a user type}
802 %************************************************************************
804 When dealing with a user-written type, we first translate it from an HsType
805 to a Type, performing kind checking, and then check various things that should
806 be true about it. We don't want to perform these checks at the same time
807 as the initial translation because (a) they are unnecessary for interface-file
808 types and (b) when checking a mutually recursive group of type and class decls,
809 we can't "look" at the tycons/classes yet. Also, the checks are are rather
810 diverse, and used to really mess up the other code.
812 One thing we check for is 'rank'.
814 Rank 0: monotypes (no foralls)
815 Rank 1: foralls at the front only, Rank 0 inside
816 Rank 2: foralls at the front, Rank 1 on left of fn arrow,
818 basic ::= tyvar | T basic ... basic
820 r2 ::= forall tvs. cxt => r2a
821 r2a ::= r1 -> r2a | basic
822 r1 ::= forall tvs. cxt => r0
823 r0 ::= r0 -> r0 | basic
825 Another thing is to check that type synonyms are saturated.
826 This might not necessarily show up in kind checking.
828 data T k = MkT (k Int)
833 checkValidType :: UserTypeCtxt -> Type -> TcM ()
834 -- Checks that the type is valid for the given context
835 checkValidType ctxt ty = do
836 traceTc "checkValidType" (ppr ty)
837 unboxed <- xoptM Opt_UnboxedTuples
838 rank2 <- xoptM Opt_Rank2Types
839 rankn <- xoptM Opt_RankNTypes
840 polycomp <- xoptM Opt_PolymorphicComponents
842 gen_rank n | rankn = ArbitraryRank
847 DefaultDeclCtxt-> MustBeMonoType
848 ResSigCtxt -> MustBeMonoType
849 LamPatSigCtxt -> gen_rank 0
850 BindPatSigCtxt -> gen_rank 0
851 TySynCtxt _ -> gen_rank 0
852 GenPatCtxt -> gen_rank 1
853 -- This one is a bit of a hack
854 -- See the forall-wrapping in TcClassDcl.mkGenericInstance
856 ExprSigCtxt -> gen_rank 1
857 FunSigCtxt _ -> gen_rank 1
858 ConArgCtxt _ | polycomp -> gen_rank 2
859 -- We are given the type of the entire
860 -- constructor, hence rank 1
861 | otherwise -> gen_rank 1
863 ForSigCtxt _ -> gen_rank 1
864 SpecInstCtxt -> gen_rank 1
865 ThBrackCtxt -> gen_rank 1
867 actual_kind = typeKind ty
869 kind_ok = case ctxt of
870 TySynCtxt _ -> True -- Any kind will do
871 ThBrackCtxt -> True -- Any kind will do
872 ResSigCtxt -> isSubOpenTypeKind actual_kind
873 ExprSigCtxt -> isSubOpenTypeKind actual_kind
874 GenPatCtxt -> isLiftedTypeKind actual_kind
875 ForSigCtxt _ -> isLiftedTypeKind actual_kind
876 _ -> isSubArgTypeKind actual_kind
878 ubx_tup = case ctxt of
879 TySynCtxt _ | unboxed -> UT_Ok
880 ExprSigCtxt | unboxed -> UT_Ok
881 ThBrackCtxt | unboxed -> UT_Ok
884 -- Check the internal validity of the type itself
885 check_type rank ubx_tup ty
887 -- Check that the thing has kind Type, and is lifted if necessary
888 -- Do this second, becuase we can't usefully take the kind of an
889 -- ill-formed type such as (a~Int)
890 checkTc kind_ok (kindErr actual_kind)
892 traceTc "checkValidType done" (ppr ty)
894 checkValidMonoType :: Type -> TcM ()
895 checkValidMonoType ty = check_mono_type MustBeMonoType ty
900 data Rank = ArbitraryRank -- Any rank ok
901 | MustBeMonoType -- Monotype regardless of flags
902 | TyConArgMonoType -- Monotype but could be poly if -XImpredicativeTypes
903 | SynArgMonoType -- Monotype but could be poly if -XLiberalTypeSynonyms
904 | Rank Int -- Rank n, but could be more with -XRankNTypes
906 decRank :: Rank -> Rank -- Function arguments
907 decRank (Rank 0) = Rank 0
908 decRank (Rank n) = Rank (n-1)
909 decRank other_rank = other_rank
911 nonZeroRank :: Rank -> Bool
912 nonZeroRank ArbitraryRank = True
913 nonZeroRank (Rank n) = n>0
914 nonZeroRank _ = False
916 ----------------------------------------
917 data UbxTupFlag = UT_Ok | UT_NotOk
918 -- The "Ok" version means "ok if UnboxedTuples is on"
920 ----------------------------------------
921 check_mono_type :: Rank -> Type -> TcM () -- No foralls anywhere
922 -- No unlifted types of any kind
923 check_mono_type rank ty
924 = do { check_type rank UT_NotOk ty
925 ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
927 check_type :: Rank -> UbxTupFlag -> Type -> TcM ()
928 -- The args say what the *type context* requires, independent
929 -- of *flag* settings. You test the flag settings at usage sites.
931 -- Rank is allowed rank for function args
932 -- Rank 0 means no for-alls anywhere
934 check_type rank ubx_tup ty
935 | not (null tvs && null theta)
936 = do { checkTc (nonZeroRank rank) (forAllTyErr rank ty)
937 -- Reject e.g. (Maybe (?x::Int => Int)),
938 -- with a decent error message
939 ; check_valid_theta SigmaCtxt theta
940 ; check_type rank ubx_tup tau -- Allow foralls to right of arrow
941 ; checkAmbiguity tvs theta (tyVarsOfType tau) }
943 (tvs, theta, tau) = tcSplitSigmaTy ty
945 -- Naked PredTys should, I think, have been rejected before now
946 check_type _ _ ty@(PredTy {})
947 = failWithTc (text "Predicate" <+> ppr ty <+> text "used as a type")
949 check_type _ _ (TyVarTy _) = return ()
951 check_type rank _ (FunTy arg_ty res_ty)
952 = do { check_type (decRank rank) UT_NotOk arg_ty
953 ; check_type rank UT_Ok res_ty }
955 check_type rank _ (AppTy ty1 ty2)
956 = do { check_arg_type rank ty1
957 ; check_arg_type rank ty2 }
959 check_type rank ubx_tup ty@(TyConApp tc tys)
961 = do { -- Check that the synonym has enough args
962 -- This applies equally to open and closed synonyms
963 -- It's OK to have an *over-applied* type synonym
964 -- data Tree a b = ...
965 -- type Foo a = Tree [a]
966 -- f :: Foo a b -> ...
967 checkTc (tyConArity tc <= length tys) arity_msg
969 -- See Note [Liberal type synonyms]
970 ; liberal <- xoptM Opt_LiberalTypeSynonyms
971 ; if not liberal || isSynFamilyTyCon tc then
972 -- For H98 and synonym families, do check the type args
973 mapM_ (check_mono_type SynArgMonoType) tys
975 else -- In the liberal case (only for closed syns), expand then check
977 Just ty' -> check_type rank ubx_tup ty'
978 Nothing -> pprPanic "check_tau_type" (ppr ty)
981 | isUnboxedTupleTyCon tc
982 = do { ub_tuples_allowed <- xoptM Opt_UnboxedTuples
983 ; checkTc (ubx_tup_ok ub_tuples_allowed) ubx_tup_msg
985 ; impred <- xoptM Opt_ImpredicativeTypes
986 ; let rank' = if impred then ArbitraryRank else TyConArgMonoType
987 -- c.f. check_arg_type
988 -- However, args are allowed to be unlifted, or
989 -- more unboxed tuples, so can't use check_arg_ty
990 ; mapM_ (check_type rank' UT_Ok) tys }
993 = mapM_ (check_arg_type rank) tys
996 ubx_tup_ok ub_tuples_allowed = case ubx_tup of
997 UT_Ok -> ub_tuples_allowed
1001 tc_arity = tyConArity tc
1003 arity_msg = arityErr "Type synonym" (tyConName tc) tc_arity n_args
1004 ubx_tup_msg = ubxArgTyErr ty
1006 check_type _ _ ty = pprPanic "check_type" (ppr ty)
1008 ----------------------------------------
1009 check_arg_type :: Rank -> Type -> TcM ()
1010 -- The sort of type that can instantiate a type variable,
1011 -- or be the argument of a type constructor.
1012 -- Not an unboxed tuple, but now *can* be a forall (since impredicativity)
1013 -- Other unboxed types are very occasionally allowed as type
1014 -- arguments depending on the kind of the type constructor
1016 -- For example, we want to reject things like:
1018 -- instance Ord a => Ord (forall s. T s a)
1020 -- g :: T s (forall b.b)
1022 -- NB: unboxed tuples can have polymorphic or unboxed args.
1023 -- This happens in the workers for functions returning
1024 -- product types with polymorphic components.
1025 -- But not in user code.
1026 -- Anyway, they are dealt with by a special case in check_tau_type
1028 check_arg_type rank ty
1029 = do { impred <- xoptM Opt_ImpredicativeTypes
1030 ; let rank' = case rank of -- Predictive => must be monotype
1031 MustBeMonoType -> MustBeMonoType -- Monotype, regardless
1032 _other | impred -> ArbitraryRank
1033 | otherwise -> TyConArgMonoType
1034 -- Make sure that MustBeMonoType is propagated,
1035 -- so that we don't suggest -XImpredicativeTypes in
1036 -- (Ord (forall a.a)) => a -> a
1037 -- and so that if it Must be a monotype, we check that it is!
1039 ; check_type rank' UT_NotOk ty
1040 ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
1042 ----------------------------------------
1043 forAllTyErr :: Rank -> Type -> SDoc
1045 = vcat [ hang (ptext (sLit "Illegal polymorphic or qualified type:")) 2 (ppr ty)
1048 suggestion = case rank of
1049 Rank _ -> ptext (sLit "Perhaps you intended to use -XRankNTypes or -XRank2Types")
1050 TyConArgMonoType -> ptext (sLit "Perhaps you intended to use -XImpredicativeTypes")
1051 SynArgMonoType -> ptext (sLit "Perhaps you intended to use -XLiberalTypeSynonyms")
1052 _ -> empty -- Polytype is always illegal
1054 unliftedArgErr, ubxArgTyErr :: Type -> SDoc
1055 unliftedArgErr ty = sep [ptext (sLit "Illegal unlifted type:"), ppr ty]
1056 ubxArgTyErr ty = sep [ptext (sLit "Illegal unboxed tuple type as function argument:"), ppr ty]
1058 kindErr :: Kind -> SDoc
1059 kindErr kind = sep [ptext (sLit "Expecting an ordinary type, but found a type of kind"), ppr kind]
1062 Note [Liberal type synonyms]
1063 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1064 If -XLiberalTypeSynonyms is on, expand closed type synonyms *before*
1065 doing validity checking. This allows us to instantiate a synonym defn
1066 with a for-all type, or with a partially-applied type synonym.
1070 Here, T is partially applied, so it's illegal in H98. But if you
1071 expand S first, then T we get just
1075 IMPORTANT: suppose T is a type synonym. Then we must do validity
1076 checking on an appliation (T ty1 ty2)
1078 *either* before expansion (i.e. check ty1, ty2)
1079 *or* after expansion (i.e. expand T ty1 ty2, and then check)
1082 If we do both, we get exponential behaviour!!
1084 data TIACons1 i r c = c i ::: r c
1085 type TIACons2 t x = TIACons1 t (TIACons1 t x)
1086 type TIACons3 t x = TIACons2 t (TIACons1 t x)
1087 type TIACons4 t x = TIACons2 t (TIACons2 t x)
1088 type TIACons7 t x = TIACons4 t (TIACons3 t x)
1091 %************************************************************************
1093 \subsection{Checking a theta or source type}
1095 %************************************************************************
1098 -- Enumerate the contexts in which a "source type", <S>, can occur
1102 -- or (N a) where N is a newtype
1105 = ClassSCCtxt Name -- Superclasses of clas
1106 -- class <S> => C a where ...
1107 | SigmaCtxt -- Theta part of a normal for-all type
1108 -- f :: <S> => a -> a
1109 | DataTyCtxt Name -- Theta part of a data decl
1110 -- data <S> => T a = MkT a
1111 | TypeCtxt -- Source type in an ordinary type
1113 | InstThetaCtxt -- Context of an instance decl
1114 -- instance <S> => C [a] where ...
1116 pprSourceTyCtxt :: SourceTyCtxt -> SDoc
1117 pprSourceTyCtxt (ClassSCCtxt c) = ptext (sLit "the super-classes of class") <+> quotes (ppr c)
1118 pprSourceTyCtxt SigmaCtxt = ptext (sLit "the context of a polymorphic type")
1119 pprSourceTyCtxt (DataTyCtxt tc) = ptext (sLit "the context of the data type declaration for") <+> quotes (ppr tc)
1120 pprSourceTyCtxt InstThetaCtxt = ptext (sLit "the context of an instance declaration")
1121 pprSourceTyCtxt TypeCtxt = ptext (sLit "the context of a type")
1125 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
1126 checkValidTheta ctxt theta
1127 = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
1129 -------------------------
1130 check_valid_theta :: SourceTyCtxt -> [PredType] -> TcM ()
1131 check_valid_theta _ []
1133 check_valid_theta ctxt theta = do
1135 warnTc (notNull dups) (dupPredWarn dups)
1136 mapM_ (check_pred_ty dflags ctxt) theta
1138 (_,dups) = removeDups tcCmpPred theta
1140 -------------------------
1141 check_pred_ty :: DynFlags -> SourceTyCtxt -> PredType -> TcM ()
1142 check_pred_ty dflags ctxt pred@(ClassP cls tys)
1143 = do { -- Class predicates are valid in all contexts
1144 ; checkTc (arity == n_tys) arity_err
1146 -- Check the form of the argument types
1147 ; mapM_ checkValidMonoType tys
1148 ; checkTc (check_class_pred_tys dflags ctxt tys)
1149 (predTyVarErr pred $$ how_to_allow)
1152 class_name = className cls
1153 arity = classArity cls
1155 arity_err = arityErr "Class" class_name arity n_tys
1156 how_to_allow = parens (ptext (sLit "Use -XFlexibleContexts to permit this"))
1159 check_pred_ty dflags _ pred@(EqPred ty1 ty2)
1160 = do { -- Equational constraints are valid in all contexts if type
1161 -- families are permitted
1162 ; checkTc (xopt Opt_TypeFamilies dflags) (eqPredTyErr pred)
1164 -- Check the form of the argument types
1165 ; checkValidMonoType ty1
1166 ; checkValidMonoType ty2
1169 check_pred_ty _ SigmaCtxt (IParam _ ty) = checkValidMonoType ty
1170 -- Implicit parameters only allowed in type
1171 -- signatures; not in instance decls, superclasses etc
1172 -- The reason for not allowing implicit params in instances is a bit
1174 -- If we allowed instance (?x::Int, Eq a) => Foo [a] where ...
1175 -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
1176 -- discharge all the potential usas of the ?x in e. For example, a
1177 -- constraint Foo [Int] might come out of e,and applying the
1178 -- instance decl would show up two uses of ?x.
1181 check_pred_ty _ _ sty = failWithTc (badPredTyErr sty)
1183 -------------------------
1184 check_class_pred_tys :: DynFlags -> SourceTyCtxt -> [Type] -> Bool
1185 check_class_pred_tys dflags ctxt tys
1187 TypeCtxt -> True -- {-# SPECIALISE instance Eq (T Int) #-} is fine
1188 InstThetaCtxt -> flexible_contexts || undecidable_ok || all tcIsTyVarTy tys
1189 -- Further checks on head and theta in
1190 -- checkInstTermination
1191 _ -> flexible_contexts || all tyvar_head tys
1193 flexible_contexts = xopt Opt_FlexibleContexts dflags
1194 undecidable_ok = xopt Opt_UndecidableInstances dflags
1196 -------------------------
1197 tyvar_head :: Type -> Bool
1198 tyvar_head ty -- Haskell 98 allows predicates of form
1199 | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
1200 | otherwise -- where a is a type variable
1201 = case tcSplitAppTy_maybe ty of
1202 Just (ty, _) -> tyvar_head ty
1209 is ambiguous if P contains generic variables
1210 (i.e. one of the Vs) that are not mentioned in tau
1212 However, we need to take account of functional dependencies
1213 when we speak of 'mentioned in tau'. Example:
1214 class C a b | a -> b where ...
1216 forall x y. (C x y) => x
1217 is not ambiguous because x is mentioned and x determines y
1219 NB; the ambiguity check is only used for *user* types, not for types
1220 coming from inteface files. The latter can legitimately have
1221 ambiguous types. Example
1223 class S a where s :: a -> (Int,Int)
1224 instance S Char where s _ = (1,1)
1225 f:: S a => [a] -> Int -> (Int,Int)
1226 f (_::[a]) x = (a*x,b)
1227 where (a,b) = s (undefined::a)
1229 Here the worker for f gets the type
1230 fw :: forall a. S a => Int -> (# Int, Int #)
1232 If the list of tv_names is empty, we have a monotype, and then we
1233 don't need to check for ambiguity either, because the test can't fail
1236 In addition, GHC insists that at least one type variable
1237 in each constraint is in V. So we disallow a type like
1238 forall a. Eq b => b -> b
1239 even in a scope where b is in scope.
1242 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
1243 checkAmbiguity forall_tyvars theta tau_tyvars
1244 = mapM_ complain (filter is_ambig theta)
1246 complain pred = addErrTc (ambigErr pred)
1247 extended_tau_vars = growThetaTyVars theta tau_tyvars
1249 -- See Note [Implicit parameters and ambiguity] in TcSimplify
1250 is_ambig pred = isClassPred pred &&
1251 any ambig_var (varSetElems (tyVarsOfPred pred))
1253 ambig_var ct_var = (ct_var `elem` forall_tyvars) &&
1254 not (ct_var `elemVarSet` extended_tau_vars)
1256 ambigErr :: PredType -> SDoc
1258 = sep [ptext (sLit "Ambiguous constraint") <+> quotes (pprPred pred),
1259 nest 2 (ptext (sLit "At least one of the forall'd type variables mentioned by the constraint") $$
1260 ptext (sLit "must be reachable from the type after the '=>'"))]
1263 Note [Growing the tau-tvs using constraints]
1264 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1265 (growInstsTyVars insts tvs) is the result of extending the set
1266 of tyvars tvs using all conceivable links from pred
1268 E.g. tvs = {a}, preds = {H [a] b, K (b,Int) c, Eq e}
1269 Then grow precs tvs = {a,b,c}
1272 growThetaTyVars :: TcThetaType -> TyVarSet -> TyVarSet
1273 -- See Note [Growing the tau-tvs using constraints]
1274 growThetaTyVars theta tvs
1276 | otherwise = fixVarSet mk_next tvs
1278 mk_next tvs = foldr grow_one tvs theta
1279 grow_one pred tvs = growPredTyVars pred tvs `unionVarSet` tvs
1281 growPredTyVars :: TcPredType
1282 -> TyVarSet -- The set to extend
1283 -> TyVarSet -- TyVars of the predicate if it intersects
1284 -- the set, or is implicit parameter
1285 growPredTyVars pred tvs
1286 | IParam {} <- pred = pred_tvs -- See Note [Implicit parameters and ambiguity]
1287 | pred_tvs `intersectsVarSet` tvs = pred_tvs
1288 | otherwise = emptyVarSet
1290 pred_tvs = tyVarsOfPred pred
1293 Note [Implicit parameters and ambiguity]
1294 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1295 Only a *class* predicate can give rise to ambiguity
1296 An *implicit parameter* cannot. For example:
1297 foo :: (?x :: [a]) => Int
1299 is fine. The call site will suppply a particular 'x'
1301 Furthermore, the type variables fixed by an implicit parameter
1302 propagate to the others. E.g.
1303 foo :: (Show a, ?x::[a]) => Int
1305 The type of foo looks ambiguous. But it isn't, because at a call site
1307 let ?x = 5::Int in foo
1308 and all is well. In effect, implicit parameters are, well, parameters,
1309 so we can take their type variables into account as part of the
1310 "tau-tvs" stuff. This is done in the function 'FunDeps.grow'.
1314 checkThetaCtxt :: SourceTyCtxt -> ThetaType -> SDoc
1315 checkThetaCtxt ctxt theta
1316 = vcat [ptext (sLit "In the context:") <+> pprTheta theta,
1317 ptext (sLit "While checking") <+> pprSourceTyCtxt ctxt ]
1319 badPredTyErr, eqPredTyErr, predTyVarErr :: PredType -> SDoc
1320 badPredTyErr sty = ptext (sLit "Illegal constraint") <+> pprPred sty
1321 eqPredTyErr sty = ptext (sLit "Illegal equational constraint") <+> pprPred sty
1323 parens (ptext (sLit "Use -XTypeFamilies to permit this"))
1324 predTyVarErr pred = sep [ptext (sLit "Non type-variable argument"),
1325 nest 2 (ptext (sLit "in the constraint:") <+> pprPred pred)]
1326 dupPredWarn :: [[PredType]] -> SDoc
1327 dupPredWarn dups = ptext (sLit "Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
1329 arityErr :: Outputable a => String -> a -> Int -> Int -> SDoc
1330 arityErr kind name n m
1331 = hsep [ text kind, quotes (ppr name), ptext (sLit "should have"),
1332 n_arguments <> comma, text "but has been given",
1333 if m==0 then text "none" else int m]
1335 n_arguments | n == 0 = ptext (sLit "no arguments")
1336 | n == 1 = ptext (sLit "1 argument")
1337 | True = hsep [int n, ptext (sLit "arguments")]
1340 %************************************************************************
1342 \subsection{Checking for a decent instance head type}
1344 %************************************************************************
1346 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1347 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1349 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1350 flag is on, or (2)~the instance is imported (they must have been
1351 compiled elsewhere). In these cases, we let them go through anyway.
1353 We can also have instances for functions: @instance Foo (a -> b) ...@.
1356 checkValidInstHead :: Type -> TcM (Class, [TcType])
1358 checkValidInstHead ty -- Should be a source type
1359 = case tcSplitPredTy_maybe ty of {
1360 Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
1363 case getClassPredTys_maybe pred of {
1364 Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
1365 Just (clas,tys) -> do
1368 check_inst_head dflags clas tys
1372 check_inst_head :: DynFlags -> Class -> [Type] -> TcM ()
1373 check_inst_head dflags clas tys
1374 = do { -- If GlasgowExts then check at least one isn't a type variable
1375 ; checkTc (xopt Opt_TypeSynonymInstances dflags ||
1376 all tcInstHeadTyNotSynonym tys)
1377 (instTypeErr (pprClassPred clas tys) head_type_synonym_msg)
1378 ; checkTc (xopt Opt_FlexibleInstances dflags ||
1379 all tcInstHeadTyAppAllTyVars tys)
1380 (instTypeErr (pprClassPred clas tys) head_type_args_tyvars_msg)
1381 ; checkTc (xopt Opt_MultiParamTypeClasses dflags ||
1383 (instTypeErr (pprClassPred clas tys) head_one_type_msg)
1384 -- May not contain type family applications
1385 ; mapM_ checkTyFamFreeness tys
1387 ; mapM_ checkValidMonoType tys
1388 -- For now, I only allow tau-types (not polytypes) in
1389 -- the head of an instance decl.
1390 -- E.g. instance C (forall a. a->a) is rejected
1391 -- One could imagine generalising that, but I'm not sure
1392 -- what all the consequences might be
1396 head_type_synonym_msg = parens (
1397 text "All instance types must be of the form (T t1 ... tn)" $$
1398 text "where T is not a synonym." $$
1399 text "Use -XTypeSynonymInstances if you want to disable this.")
1401 head_type_args_tyvars_msg = parens (vcat [
1402 text "All instance types must be of the form (T a1 ... an)",
1403 text "where a1 ... an are type *variables*,",
1404 text "and each type variable appears at most once in the instance head.",
1405 text "Use -XFlexibleInstances if you want to disable this."])
1407 head_one_type_msg = parens (
1408 text "Only one type can be given in an instance head." $$
1409 text "Use -XMultiParamTypeClasses if you want to allow more.")
1411 instTypeErr :: SDoc -> SDoc -> SDoc
1412 instTypeErr pp_ty msg
1413 = sep [ptext (sLit "Illegal instance declaration for") <+> quotes pp_ty,
1418 %************************************************************************
1420 \subsection{Checking instance for termination}
1422 %************************************************************************
1425 checkValidInstance :: LHsType Name -> [TyVar] -> ThetaType -> Type
1426 -> TcM (Class, [TcType])
1427 checkValidInstance hs_type tyvars theta tau
1428 = setSrcSpan (getLoc hs_type) $
1429 do { (clas, inst_tys) <- setSrcSpan head_loc $
1430 checkValidInstHead tau
1432 ; undecidable_ok <- xoptM Opt_UndecidableInstances
1434 ; checkValidTheta InstThetaCtxt theta
1435 ; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys)
1437 -- Check that instance inference will terminate (if we care)
1438 -- For Haskell 98 this will already have been done by checkValidTheta,
1439 -- but as we may be using other extensions we need to check.
1440 ; unless undecidable_ok $
1441 mapM_ addErrTc (checkInstTermination inst_tys theta)
1443 -- The Coverage Condition
1444 ; checkTc (undecidable_ok || checkInstCoverage clas inst_tys)
1445 (instTypeErr (pprClassPred clas inst_tys) msg)
1447 ; return (clas, inst_tys)
1450 msg = parens (vcat [ptext (sLit "the Coverage Condition fails for one of the functional dependencies;"),
1453 -- The location of the "head" of the instance
1454 head_loc = case hs_type of
1455 L _ (HsForAllTy _ _ _ (L loc _)) -> loc
1459 Termination test: the so-called "Paterson conditions" (see Section 5 of
1460 "Understanding functionsl dependencies via Constraint Handling Rules,
1463 We check that each assertion in the context satisfies:
1464 (1) no variable has more occurrences in the assertion than in the head, and
1465 (2) the assertion has fewer constructors and variables (taken together
1466 and counting repetitions) than the head.
1467 This is only needed with -fglasgow-exts, as Haskell 98 restrictions
1468 (which have already been checked) guarantee termination.
1470 The underlying idea is that
1472 for any ground substitution, each assertion in the
1473 context has fewer type constructors than the head.
1477 checkInstTermination :: [TcType] -> ThetaType -> [Message]
1478 checkInstTermination tys theta
1479 = mapCatMaybes check theta
1482 size = sizeTypes tys
1484 | not (null (fvPred pred \\ fvs))
1485 = Just (predUndecErr pred nomoreMsg $$ parens undecidableMsg)
1486 | sizePred pred >= size
1487 = Just (predUndecErr pred smallerMsg $$ parens undecidableMsg)
1491 predUndecErr :: PredType -> SDoc -> SDoc
1492 predUndecErr pred msg = sep [msg,
1493 nest 2 (ptext (sLit "in the constraint:") <+> pprPred pred)]
1495 nomoreMsg, smallerMsg, undecidableMsg :: SDoc
1496 nomoreMsg = ptext (sLit "Variable occurs more often in a constraint than in the instance head")
1497 smallerMsg = ptext (sLit "Constraint is no smaller than the instance head")
1498 undecidableMsg = ptext (sLit "Use -XUndecidableInstances to permit this")
1501 validDeivPred checks for OK 'deriving' context. See Note [Exotic
1502 derived instance contexts] in TcSimplify. However the predicate is
1503 here because it uses sizeTypes, fvTypes.
1506 validDerivPred :: PredType -> Bool
1507 validDerivPred (ClassP _ tys) = hasNoDups fvs && sizeTypes tys == length fvs
1508 where fvs = fvTypes tys
1509 validDerivPred _ = False
1513 %************************************************************************
1515 Checking type instance well-formedness and termination
1517 %************************************************************************
1520 -- Check that a "type instance" is well-formed (which includes decidability
1521 -- unless -XUndecidableInstances is given).
1523 checkValidTypeInst :: [Type] -> Type -> TcM ()
1524 checkValidTypeInst typats rhs
1525 = do { -- left-hand side contains no type family applications
1526 -- (vanilla synonyms are fine, though)
1527 ; mapM_ checkTyFamFreeness typats
1529 -- the right-hand side is a tau type
1530 ; checkValidMonoType rhs
1532 -- we have a decidable instance unless otherwise permitted
1533 ; undecidable_ok <- xoptM Opt_UndecidableInstances
1534 ; unless undecidable_ok $
1535 mapM_ addErrTc (checkFamInst typats (tyFamInsts rhs))
1538 -- Make sure that each type family instance is
1539 -- (1) strictly smaller than the lhs,
1540 -- (2) mentions no type variable more often than the lhs, and
1541 -- (3) does not contain any further type family instances.
1543 checkFamInst :: [Type] -- lhs
1544 -> [(TyCon, [Type])] -- type family instances
1546 checkFamInst lhsTys famInsts
1547 = mapCatMaybes check famInsts
1549 size = sizeTypes lhsTys
1550 fvs = fvTypes lhsTys
1552 | not (all isTyFamFree tys)
1553 = Just (famInstUndecErr famInst nestedMsg $$ parens undecidableMsg)
1554 | not (null (fvTypes tys \\ fvs))
1555 = Just (famInstUndecErr famInst nomoreVarMsg $$ parens undecidableMsg)
1556 | size <= sizeTypes tys
1557 = Just (famInstUndecErr famInst smallerAppMsg $$ parens undecidableMsg)
1561 famInst = TyConApp tc tys
1563 -- Ensure that no type family instances occur in a type.
1565 checkTyFamFreeness :: Type -> TcM ()
1566 checkTyFamFreeness ty
1567 = checkTc (isTyFamFree ty) $
1568 tyFamInstIllegalErr ty
1570 -- Check that a type does not contain any type family applications.
1572 isTyFamFree :: Type -> Bool
1573 isTyFamFree = null . tyFamInsts
1577 tyFamInstIllegalErr :: Type -> SDoc
1578 tyFamInstIllegalErr ty
1579 = hang (ptext (sLit "Illegal type synonym family application in instance") <>
1583 famInstUndecErr :: Type -> SDoc -> SDoc
1584 famInstUndecErr ty msg
1586 nest 2 (ptext (sLit "in the type family application:") <+>
1589 nestedMsg, nomoreVarMsg, smallerAppMsg :: SDoc
1590 nestedMsg = ptext (sLit "Nested type family application")
1591 nomoreVarMsg = ptext (sLit "Variable occurs more often than in instance head")
1592 smallerAppMsg = ptext (sLit "Application is no smaller than the instance head")
1596 %************************************************************************
1598 \subsection{Auxiliary functions}
1600 %************************************************************************
1603 -- Free variables of a type, retaining repetitions, and expanding synonyms
1604 fvType :: Type -> [TyVar]
1605 fvType ty | Just exp_ty <- tcView ty = fvType exp_ty
1606 fvType (TyVarTy tv) = [tv]
1607 fvType (TyConApp _ tys) = fvTypes tys
1608 fvType (PredTy pred) = fvPred pred
1609 fvType (FunTy arg res) = fvType arg ++ fvType res
1610 fvType (AppTy fun arg) = fvType fun ++ fvType arg
1611 fvType (ForAllTy tyvar ty) = filter (/= tyvar) (fvType ty)
1613 fvTypes :: [Type] -> [TyVar]
1614 fvTypes tys = concat (map fvType tys)
1616 fvPred :: PredType -> [TyVar]
1617 fvPred (ClassP _ tys') = fvTypes tys'
1618 fvPred (IParam _ ty) = fvType ty
1619 fvPred (EqPred ty1 ty2) = fvType ty1 ++ fvType ty2
1621 -- Size of a type: the number of variables and constructors
1622 sizeType :: Type -> Int
1623 sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty
1624 sizeType (TyVarTy _) = 1
1625 sizeType (TyConApp _ tys) = sizeTypes tys + 1
1626 sizeType (PredTy pred) = sizePred pred
1627 sizeType (FunTy arg res) = sizeType arg + sizeType res + 1
1628 sizeType (AppTy fun arg) = sizeType fun + sizeType arg
1629 sizeType (ForAllTy _ ty) = sizeType ty
1631 sizeTypes :: [Type] -> Int
1632 sizeTypes xs = sum (map sizeType xs)
1634 -- Size of a predicate
1636 -- We are considering whether *class* constraints terminate
1637 -- Once we get into an implicit parameter or equality we
1638 -- can't get back to a class constraint, so it's safe
1639 -- to say "size 0". See Trac #4200.
1640 sizePred :: PredType -> Int
1641 sizePred (ClassP _ tys') = sizeTypes tys'
1642 sizePred (IParam {}) = 0
1643 sizePred (EqPred {}) = 0