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,
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 <- newUnique
304 ; ref <- newMutVar Flexi
305 ; let name = mkSysTvName uniq fs
306 fs = case meta_info of
309 ; return (mkTcTyVar name kind (MetaTv meta_info ref)) }
311 instMetaTyVar :: MetaInfo -> TyVar -> TcM TcTyVar
312 -- Make a new meta tyvar whose Name and Kind
313 -- come from an existing TyVar
314 instMetaTyVar meta_info tyvar
315 = do { uniq <- newUnique
316 ; ref <- newMutVar Flexi
317 ; let name = setNameUnique (tyVarName tyvar) uniq
318 kind = tyVarKind tyvar
319 ; return (mkTcTyVar name kind (MetaTv meta_info ref)) }
321 readMetaTyVar :: TyVar -> TcM MetaDetails
322 readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
323 readMutVar (metaTvRef tyvar)
325 readWantedCoVar :: CoVar -> TcM MetaDetails
326 readWantedCoVar covar = ASSERT2( isMetaTyVar covar, ppr covar )
327 readMutVar (metaTvRef covar)
331 isFilledMetaTyVar :: TyVar -> TcM Bool
332 -- True of a filled-in (Indirect) meta type variable
334 | not (isTcTyVar tv) = return False
335 | MetaTv _ ref <- tcTyVarDetails tv
336 = do { details <- readMutVar ref
337 ; return (isIndirect details) }
338 | otherwise = return False
340 isFlexiMetaTyVar :: TyVar -> TcM Bool
341 -- True of a un-filled-in (Flexi) meta type variable
343 | not (isTcTyVar tv) = return False
344 | MetaTv _ ref <- tcTyVarDetails tv
345 = do { details <- readMutVar ref
346 ; return (isFlexi details) }
347 | otherwise = return False
350 writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
351 -- Write into a currently-empty MetaTyVar
353 writeMetaTyVar tyvar ty
355 = writeMetaTyVarRef tyvar (metaTvRef tyvar) ty
357 -- Everything from here on only happens if DEBUG is on
358 | not (isTcTyVar tyvar)
359 = WARN( True, text "Writing to non-tc tyvar" <+> ppr tyvar )
362 | MetaTv _ ref <- tcTyVarDetails tyvar
363 = writeMetaTyVarRef tyvar ref ty
366 = WARN( True, text "Writing to non-meta tyvar" <+> ppr tyvar )
369 writeWantedCoVar :: CoVar -> Coercion -> TcM ()
370 writeWantedCoVar cv co = writeMetaTyVar cv co
373 writeMetaTyVarRef :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM ()
374 -- Here the tyvar is for error checking only;
375 -- the ref cell must be for the same tyvar
376 writeMetaTyVarRef tyvar ref ty
378 = do { traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
379 ; writeMutVar ref (Indirect ty) }
381 -- Everything from here on only happens if DEBUG is on
382 | not (isPredTy tv_kind) -- Don't check kinds for updates to coercion variables
383 , not (ty_kind `isSubKind` tv_kind)
384 = WARN( True, hang (text "Ill-kinded update to meta tyvar")
385 2 (ppr tyvar $$ ppr tv_kind $$ ppr ty $$ ppr ty_kind) )
389 = do { meta_details <- readMutVar ref;
390 ; WARN( not (isFlexi meta_details),
391 hang (text "Double update of meta tyvar")
392 2 (ppr tyvar $$ ppr meta_details) )
394 traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
395 ; writeMutVar ref (Indirect ty) }
397 tv_kind = tyVarKind tyvar
398 ty_kind = typeKind ty
402 %************************************************************************
406 %************************************************************************
409 newFlexiTyVar :: Kind -> TcM TcTyVar
410 newFlexiTyVar kind = newMetaTyVar TauTv kind
412 newFlexiTyVarTy :: Kind -> TcM TcType
413 newFlexiTyVarTy kind = do
414 tc_tyvar <- newFlexiTyVar kind
415 return (TyVarTy tc_tyvar)
417 newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
418 newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind)
420 tcInstTyVar :: TyVar -> TcM TcTyVar
421 -- Instantiate with a META type variable
422 tcInstTyVar tyvar = instMetaTyVar TauTv tyvar
424 tcInstTyVars :: [TyVar] -> TcM ([TcTyVar], [TcType], TvSubst)
425 -- Instantiate with META type variables
427 = do { tc_tvs <- mapM tcInstTyVar tyvars
428 ; let tys = mkTyVarTys tc_tvs
429 ; return (tc_tvs, tys, zipTopTvSubst tyvars tys) }
430 -- Since the tyvars are freshly made,
431 -- they cannot possibly be captured by
432 -- any existing for-alls. Hence zipTopTvSubst
436 %************************************************************************
440 %************************************************************************
443 zonkSigTyVar :: TcTyVar -> TcM TcTyVar
445 | isSkolemTyVar sig_tv
446 = return sig_tv -- Happens in the call in TcBinds.checkDistinctTyVars
448 = ASSERT( isSigTyVar sig_tv )
449 do { ty <- zonkTcTyVar sig_tv
450 ; return (tcGetTyVar "zonkSigTyVar" ty) }
451 -- 'ty' is bound to be a type variable, because SigTvs
452 -- can only be unified with type variables
457 %************************************************************************
459 \subsection{Zonking -- the exernal interfaces}
461 %************************************************************************
463 @tcGetGlobalTyVars@ returns a fully-zonked set of tyvars free in the environment.
464 To improve subsequent calls to the same function it writes the zonked set back into
468 tcGetGlobalTyVars :: TcM TcTyVarSet
470 = do { (TcLclEnv {tcl_tyvars = gtv_var}) <- getLclEnv
471 ; gbl_tvs <- readMutVar gtv_var
472 ; gbl_tvs' <- zonkTcTyVarsAndFV (varSetElems gbl_tvs)
473 ; writeMutVar gtv_var gbl_tvs'
477 ----------------- Type variables
480 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
481 zonkTcTyVars tyvars = mapM zonkTcTyVar tyvars
483 zonkTcTyVarsAndFV :: [TcTyVar] -> TcM TcTyVarSet
484 zonkTcTyVarsAndFV tyvars = tyVarsOfTypes <$> mapM zonkTcTyVar tyvars
486 ----------------- Types
488 zonkTcTypeCarefully :: TcType -> TcM TcType
489 -- Do not zonk type variables free in the environment
490 zonkTcTypeCarefully ty
491 = do { env_tvs <- tcGetGlobalTyVars
492 ; zonkType (zonk_tv env_tvs) ty }
495 | tv `elemVarSet` env_tvs
496 = return (TyVarTy tv)
498 = ASSERT( isTcTyVar tv )
499 case tcTyVarDetails tv of
500 SkolemTv {} -> return (TyVarTy tv)
501 FlatSkol ty -> zonkType (zonk_tv env_tvs) ty
502 MetaTv _ ref -> do { cts <- readMutVar ref
504 Flexi -> return (TyVarTy tv)
505 Indirect ty -> zonkType (zonk_tv env_tvs) ty }
507 zonkTcType :: TcType -> TcM TcType
508 -- Simply look through all Flexis
509 zonkTcType ty = zonkType zonkTcTyVar ty
511 zonkTcTyVar :: TcTyVar -> TcM TcType
512 -- Simply look through all Flexis
514 = ASSERT2( isTcTyVar tv, ppr tv )
515 case tcTyVarDetails tv of
516 SkolemTv {} -> return (TyVarTy tv)
517 FlatSkol ty -> zonkTcType ty
518 MetaTv _ ref -> do { cts <- readMutVar ref
520 Flexi -> return (TyVarTy tv)
521 Indirect ty -> zonkTcType ty }
523 zonkTcTypeAndSubst :: TvSubst -> TcType -> TcM TcType
524 -- Zonk, and simultaneously apply a non-necessarily-idempotent substitution
525 zonkTcTypeAndSubst subst ty = zonkType zonk_tv ty
528 = case tcTyVarDetails tv of
529 SkolemTv {} -> return (TyVarTy tv)
530 FlatSkol ty -> zonkType zonk_tv ty
531 MetaTv _ ref -> do { cts <- readMutVar ref
533 Flexi -> zonk_flexi tv
534 Indirect ty -> zonkType zonk_tv ty }
536 = case lookupTyVar subst tv of
537 Just ty -> zonkType zonk_tv ty
538 Nothing -> return (TyVarTy tv)
540 zonkTcTypes :: [TcType] -> TcM [TcType]
541 zonkTcTypes tys = mapM zonkTcType tys
543 zonkTcThetaType :: TcThetaType -> TcM TcThetaType
544 zonkTcThetaType theta = mapM zonkTcPredType theta
546 zonkTcPredType :: TcPredType -> TcM TcPredType
547 zonkTcPredType (ClassP c ts) = ClassP c <$> zonkTcTypes ts
548 zonkTcPredType (IParam n t) = IParam n <$> zonkTcType t
549 zonkTcPredType (EqPred t1 t2) = EqPred <$> zonkTcType t1 <*> zonkTcType t2
552 ------------------- These ...ToType, ...ToKind versions
553 are used at the end of type checking
556 zonkQuantifiedTyVars :: [TcTyVar] -> TcM [TcTyVar]
557 zonkQuantifiedTyVars = mapM zonkQuantifiedTyVar
559 zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar
560 -- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it.
562 -- The quantified type variables often include meta type variables
563 -- we want to freeze them into ordinary type variables, and
564 -- default their kind (e.g. from OpenTypeKind to TypeKind)
565 -- -- see notes with Kind.defaultKind
566 -- The meta tyvar is updated to point to the new skolem TyVar. Now any
567 -- bound occurences of the original type variable will get zonked to
568 -- the immutable version.
570 -- We leave skolem TyVars alone; they are immutable.
571 zonkQuantifiedTyVar tv
572 | ASSERT2( isTcTyVar tv, ppr tv )
574 = do { kind <- zonkTcType (tyVarKind tv)
575 ; return $ setTyVarKind tv kind
577 -- It might be a skolem type variable,
578 -- for example from a user type signature
580 | otherwise -- It's a meta-type-variable
581 = do { details <- readMetaTyVar tv
583 -- Create the new, frozen, skolem type variable
584 -- We zonk to a skolem, not to a regular TcVar
585 -- See Note [Zonking to Skolem]
586 ; let final_kind = defaultKind (tyVarKind tv)
587 final_tv = mkSkolTyVar (tyVarName tv) final_kind UnkSkol
589 -- Bind the meta tyvar to the new tyvar
591 Indirect ty -> WARN( True, ppr tv $$ ppr ty )
593 -- [Sept 04] I don't think this should happen
594 -- See note [Silly Type Synonym]
596 Flexi -> writeMetaTyVar tv (mkTyVarTy final_tv)
598 -- Return the new tyvar
603 zonkImplication :: Implication -> TcM Implication
604 zonkImplication implic@(Implic { ic_env_tvs = env_tvs, ic_given = given
605 , ic_wanted = wanted })
606 = do { env_tvs' <- zonkTcTyVarsAndFV (varSetElems env_tvs)
607 ; given' <- mapM zonkEvVar given
608 ; wanted' <- mapBagM zonkWanted wanted
609 ; return (implic { ic_env_tvs = env_tvs', ic_given = given'
610 , ic_wanted = wanted' }) }
612 zonkEvVar :: EvVar -> TcM EvVar
613 zonkEvVar var = do { ty' <- zonkTcType (varType var)
614 ; return (setVarType var ty') }
616 zonkWanted :: WantedConstraint -> TcM WantedConstraint
617 zonkWanted (WcImplic imp) = do { imp' <- zonkImplication imp; return (WcImplic imp') }
618 zonkWanted (WcEvVar ev) = do { ev' <- zonkWantedEvVar ev; return (WcEvVar ev') }
620 zonkWantedEvVar :: WantedEvVar -> TcM WantedEvVar
621 zonkWantedEvVar (WantedEvVar v l) = do { v' <- zonkEvVar v; return (WantedEvVar v' l) }
625 Note [Silly Type Synonyms]
626 ~~~~~~~~~~~~~~~~~~~~~~~~~~
628 type C u a = u -- Note 'a' unused
630 foo :: (forall a. C u a -> C u a) -> u
634 bar = foo (\t -> t + t)
636 * From the (\t -> t+t) we get type {Num d} => d -> d
639 * Now unify with type of foo's arg, and we get:
640 {Num (C d a)} => C d a -> C d a
643 * Now abstract over the 'a', but float out the Num (C d a) constraint
644 because it does not 'really' mention a. (see exactTyVarsOfType)
645 The arg to foo becomes
648 * So we get a dict binding for Num (C d a), which is zonked to give
650 [Note Sept 04: now that we are zonking quantified type variables
651 on construction, the 'a' will be frozen as a regular tyvar on
652 quantification, so the floated dict will still have type (C d a).
653 Which renders this whole note moot; happily!]
655 * Then the \/\a abstraction has a zonked 'a' in it.
657 All very silly. I think its harmless to ignore the problem. We'll end up with
658 a \/\a in the final result but all the occurrences of a will be zonked to ()
660 Note [Zonking to Skolem]
661 ~~~~~~~~~~~~~~~~~~~~~~~~
662 We used to zonk quantified type variables to regular TyVars. However, this
663 leads to problems. Consider this program from the regression test suite:
665 eval :: Int -> String -> String -> String
666 eval 0 root actual = evalRHS 0 root actual
669 evalRHS 0 root actual = eval 0 root actual
671 It leads to the deferral of an equality (wrapped in an implication constraint)
673 forall a. (String -> String -> String) ~ a
675 which is propagated up to the toplevel (see TcSimplify.tcSimplifyInferCheck).
676 In the meantime `a' is zonked and quantified to form `evalRHS's signature.
677 This has the *side effect* of also zonking the `a' in the deferred equality
678 (which at this point is being handed around wrapped in an implication
681 Finally, the equality (with the zonked `a') will be handed back to the
682 simplifier by TcRnDriver.tcRnSrcDecls calling TcSimplify.tcSimplifyTop.
683 If we zonk `a' with a regular type variable, we will have this regular type
684 variable now floating around in the simplifier, which in many places assumes to
685 only see proper TcTyVars.
687 We can avoid this problem by zonking with a skolem. The skolem is rigid
688 (which we require for a quantified variable), but is still a TcTyVar that the
689 simplifier knows how to deal with.
692 %************************************************************************
694 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
696 %* For internal use only! *
698 %************************************************************************
701 -- For unbound, mutable tyvars, zonkType uses the function given to it
702 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
703 -- type variable and zonks the kind too
705 zonkType :: (TcTyVar -> TcM Type) -- What to do with unbound mutable type variables
706 -- see zonkTcType, and zonkTcTypeToType
709 zonkType zonk_tc_tyvar ty
712 go (TyConApp tc tys) = do tys' <- mapM go tys
713 return (TyConApp tc tys')
715 go (PredTy p) = do p' <- go_pred p
718 go (FunTy arg res) = do arg' <- go arg
720 return (FunTy arg' res')
722 go (AppTy fun arg) = do fun' <- go fun
724 return (mkAppTy fun' arg')
725 -- NB the mkAppTy; we might have instantiated a
726 -- type variable to a type constructor, so we need
727 -- to pull the TyConApp to the top.
729 -- The two interesting cases!
730 go (TyVarTy tyvar) | isTcTyVar tyvar = zonk_tc_tyvar tyvar
731 | otherwise = liftM TyVarTy $
732 zonkTyVar zonk_tc_tyvar tyvar
733 -- Ordinary (non Tc) tyvars occur inside quantified types
735 go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar ) do
737 tyvar' <- zonkTyVar zonk_tc_tyvar tyvar
738 return (ForAllTy tyvar' ty')
740 go_pred (ClassP c tys) = do tys' <- mapM go tys
741 return (ClassP c tys')
742 go_pred (IParam n ty) = do ty' <- go ty
743 return (IParam n ty')
744 go_pred (EqPred ty1 ty2) = do ty1' <- go ty1
746 return (EqPred ty1' ty2')
748 mkZonkTcTyVar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable var
749 -> TcTyVar -> TcM TcType
750 mkZonkTcTyVar unbound_var_fn tyvar
751 = ASSERT( isTcTyVar tyvar )
752 case tcTyVarDetails tyvar of
753 SkolemTv {} -> return (TyVarTy tyvar)
754 FlatSkol ty -> zonkType (mkZonkTcTyVar unbound_var_fn) ty
755 MetaTv _ ref -> do { cts <- readMutVar ref
757 Flexi -> unbound_var_fn tyvar
758 Indirect ty -> zonkType (mkZonkTcTyVar unbound_var_fn) ty }
760 -- Zonk the kind of a non-TC tyvar in case it is a coercion variable
761 -- (their kind contains types).
762 zonkTyVar :: (TcTyVar -> TcM Type) -- What to do for a TcTyVar
763 -> TyVar -> TcM TyVar
764 zonkTyVar zonk_tc_tyvar tv
766 = do { kind <- zonkType zonk_tc_tyvar (tyVarKind tv)
767 ; return $ setTyVarKind tv kind }
768 | otherwise = return tv
773 %************************************************************************
777 %************************************************************************
780 readKindVar :: KindVar -> TcM (MetaDetails)
781 writeKindVar :: KindVar -> TcKind -> TcM ()
782 readKindVar kv = readMutVar (kindVarRef kv)
783 writeKindVar kv val = writeMutVar (kindVarRef kv) (Indirect val)
786 zonkTcKind :: TcKind -> TcM TcKind
787 zonkTcKind k = zonkTcType k
790 zonkTcKindToKind :: TcKind -> TcM Kind
791 -- When zonking a TcKind to a kind, we need to instantiate kind variables,
792 -- Haskell specifies that * is to be used, so we follow that.
794 = zonkType (mkZonkTcTyVar (\ _ -> return liftedTypeKind)) k
797 %************************************************************************
799 \subsection{Checking a user type}
801 %************************************************************************
803 When dealing with a user-written type, we first translate it from an HsType
804 to a Type, performing kind checking, and then check various things that should
805 be true about it. We don't want to perform these checks at the same time
806 as the initial translation because (a) they are unnecessary for interface-file
807 types and (b) when checking a mutually recursive group of type and class decls,
808 we can't "look" at the tycons/classes yet. Also, the checks are are rather
809 diverse, and used to really mess up the other code.
811 One thing we check for is 'rank'.
813 Rank 0: monotypes (no foralls)
814 Rank 1: foralls at the front only, Rank 0 inside
815 Rank 2: foralls at the front, Rank 1 on left of fn arrow,
817 basic ::= tyvar | T basic ... basic
819 r2 ::= forall tvs. cxt => r2a
820 r2a ::= r1 -> r2a | basic
821 r1 ::= forall tvs. cxt => r0
822 r0 ::= r0 -> r0 | basic
824 Another thing is to check that type synonyms are saturated.
825 This might not necessarily show up in kind checking.
827 data T k = MkT (k Int)
832 checkValidType :: UserTypeCtxt -> Type -> TcM ()
833 -- Checks that the type is valid for the given context
834 checkValidType ctxt ty = do
835 traceTc "checkValidType" (ppr ty)
836 unboxed <- xoptM Opt_UnboxedTuples
837 rank2 <- xoptM Opt_Rank2Types
838 rankn <- xoptM Opt_RankNTypes
839 polycomp <- xoptM Opt_PolymorphicComponents
841 gen_rank n | rankn = ArbitraryRank
846 DefaultDeclCtxt-> MustBeMonoType
847 ResSigCtxt -> MustBeMonoType
848 LamPatSigCtxt -> gen_rank 0
849 BindPatSigCtxt -> gen_rank 0
850 TySynCtxt _ -> gen_rank 0
851 GenPatCtxt -> gen_rank 1
852 -- This one is a bit of a hack
853 -- See the forall-wrapping in TcClassDcl.mkGenericInstance
855 ExprSigCtxt -> gen_rank 1
856 FunSigCtxt _ -> gen_rank 1
857 ConArgCtxt _ | polycomp -> gen_rank 2
858 -- We are given the type of the entire
859 -- constructor, hence rank 1
860 | otherwise -> gen_rank 1
862 ForSigCtxt _ -> gen_rank 1
863 SpecInstCtxt -> gen_rank 1
864 ThBrackCtxt -> gen_rank 1
866 actual_kind = typeKind ty
868 kind_ok = case ctxt of
869 TySynCtxt _ -> True -- Any kind will do
870 ThBrackCtxt -> True -- Any kind will do
871 ResSigCtxt -> isSubOpenTypeKind actual_kind
872 ExprSigCtxt -> isSubOpenTypeKind actual_kind
873 GenPatCtxt -> isLiftedTypeKind actual_kind
874 ForSigCtxt _ -> isLiftedTypeKind actual_kind
875 _ -> isSubArgTypeKind actual_kind
877 ubx_tup = case ctxt of
878 TySynCtxt _ | unboxed -> UT_Ok
879 ExprSigCtxt | unboxed -> UT_Ok
880 ThBrackCtxt | unboxed -> UT_Ok
883 -- Check the internal validity of the type itself
884 check_type rank ubx_tup ty
886 -- Check that the thing has kind Type, and is lifted if necessary
887 -- Do this second, becuase we can't usefully take the kind of an
888 -- ill-formed type such as (a~Int)
889 checkTc kind_ok (kindErr actual_kind)
891 traceTc "checkValidType done" (ppr ty)
893 checkValidMonoType :: Type -> TcM ()
894 checkValidMonoType ty = check_mono_type MustBeMonoType ty
899 data Rank = ArbitraryRank -- Any rank ok
900 | MustBeMonoType -- Monotype regardless of flags
901 | TyConArgMonoType -- Monotype but could be poly if -XImpredicativeTypes
902 | SynArgMonoType -- Monotype but could be poly if -XLiberalTypeSynonyms
903 | Rank Int -- Rank n, but could be more with -XRankNTypes
905 decRank :: Rank -> Rank -- Function arguments
906 decRank (Rank 0) = Rank 0
907 decRank (Rank n) = Rank (n-1)
908 decRank other_rank = other_rank
910 nonZeroRank :: Rank -> Bool
911 nonZeroRank ArbitraryRank = True
912 nonZeroRank (Rank n) = n>0
913 nonZeroRank _ = False
915 ----------------------------------------
916 data UbxTupFlag = UT_Ok | UT_NotOk
917 -- The "Ok" version means "ok if UnboxedTuples is on"
919 ----------------------------------------
920 check_mono_type :: Rank -> Type -> TcM () -- No foralls anywhere
921 -- No unlifted types of any kind
922 check_mono_type rank ty
923 = do { check_type rank UT_NotOk ty
924 ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
926 check_type :: Rank -> UbxTupFlag -> Type -> TcM ()
927 -- The args say what the *type context* requires, independent
928 -- of *flag* settings. You test the flag settings at usage sites.
930 -- Rank is allowed rank for function args
931 -- Rank 0 means no for-alls anywhere
933 check_type rank ubx_tup ty
934 | not (null tvs && null theta)
935 = do { checkTc (nonZeroRank rank) (forAllTyErr rank ty)
936 -- Reject e.g. (Maybe (?x::Int => Int)),
937 -- with a decent error message
938 ; check_valid_theta SigmaCtxt theta
939 ; check_type rank ubx_tup tau -- Allow foralls to right of arrow
940 ; checkAmbiguity tvs theta (tyVarsOfType tau) }
942 (tvs, theta, tau) = tcSplitSigmaTy ty
944 -- Naked PredTys should, I think, have been rejected before now
945 check_type _ _ ty@(PredTy {})
946 = failWithTc (text "Predicate" <+> ppr ty <+> text "used as a type")
948 check_type _ _ (TyVarTy _) = return ()
950 check_type rank _ (FunTy arg_ty res_ty)
951 = do { check_type (decRank rank) UT_NotOk arg_ty
952 ; check_type rank UT_Ok res_ty }
954 check_type rank _ (AppTy ty1 ty2)
955 = do { check_arg_type rank ty1
956 ; check_arg_type rank ty2 }
958 check_type rank ubx_tup ty@(TyConApp tc tys)
960 = do { -- Check that the synonym has enough args
961 -- This applies equally to open and closed synonyms
962 -- It's OK to have an *over-applied* type synonym
963 -- data Tree a b = ...
964 -- type Foo a = Tree [a]
965 -- f :: Foo a b -> ...
966 checkTc (tyConArity tc <= length tys) arity_msg
968 -- See Note [Liberal type synonyms]
969 ; liberal <- xoptM Opt_LiberalTypeSynonyms
970 ; if not liberal || isSynFamilyTyCon tc then
971 -- For H98 and synonym families, do check the type args
972 mapM_ (check_mono_type SynArgMonoType) tys
974 else -- In the liberal case (only for closed syns), expand then check
976 Just ty' -> check_type rank ubx_tup ty'
977 Nothing -> pprPanic "check_tau_type" (ppr ty)
980 | isUnboxedTupleTyCon tc
981 = do { ub_tuples_allowed <- xoptM Opt_UnboxedTuples
982 ; checkTc (ubx_tup_ok ub_tuples_allowed) ubx_tup_msg
984 ; impred <- xoptM Opt_ImpredicativeTypes
985 ; let rank' = if impred then ArbitraryRank else TyConArgMonoType
986 -- c.f. check_arg_type
987 -- However, args are allowed to be unlifted, or
988 -- more unboxed tuples, so can't use check_arg_ty
989 ; mapM_ (check_type rank' UT_Ok) tys }
992 = mapM_ (check_arg_type rank) tys
995 ubx_tup_ok ub_tuples_allowed = case ubx_tup of
996 UT_Ok -> ub_tuples_allowed
1000 tc_arity = tyConArity tc
1002 arity_msg = arityErr "Type synonym" (tyConName tc) tc_arity n_args
1003 ubx_tup_msg = ubxArgTyErr ty
1005 check_type _ _ ty = pprPanic "check_type" (ppr ty)
1007 ----------------------------------------
1008 check_arg_type :: Rank -> Type -> TcM ()
1009 -- The sort of type that can instantiate a type variable,
1010 -- or be the argument of a type constructor.
1011 -- Not an unboxed tuple, but now *can* be a forall (since impredicativity)
1012 -- Other unboxed types are very occasionally allowed as type
1013 -- arguments depending on the kind of the type constructor
1015 -- For example, we want to reject things like:
1017 -- instance Ord a => Ord (forall s. T s a)
1019 -- g :: T s (forall b.b)
1021 -- NB: unboxed tuples can have polymorphic or unboxed args.
1022 -- This happens in the workers for functions returning
1023 -- product types with polymorphic components.
1024 -- But not in user code.
1025 -- Anyway, they are dealt with by a special case in check_tau_type
1027 check_arg_type rank ty
1028 = do { impred <- xoptM Opt_ImpredicativeTypes
1029 ; let rank' = case rank of -- Predictive => must be monotype
1030 MustBeMonoType -> MustBeMonoType -- Monotype, regardless
1031 _other | impred -> ArbitraryRank
1032 | otherwise -> TyConArgMonoType
1033 -- Make sure that MustBeMonoType is propagated,
1034 -- so that we don't suggest -XImpredicativeTypes in
1035 -- (Ord (forall a.a)) => a -> a
1036 -- and so that if it Must be a monotype, we check that it is!
1038 ; check_type rank' UT_NotOk ty
1039 ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
1041 ----------------------------------------
1042 forAllTyErr :: Rank -> Type -> SDoc
1044 = vcat [ hang (ptext (sLit "Illegal polymorphic or qualified type:")) 2 (ppr ty)
1047 suggestion = case rank of
1048 Rank _ -> ptext (sLit "Perhaps you intended to use -XRankNTypes or -XRank2Types")
1049 TyConArgMonoType -> ptext (sLit "Perhaps you intended to use -XImpredicativeTypes")
1050 SynArgMonoType -> ptext (sLit "Perhaps you intended to use -XLiberalTypeSynonyms")
1051 _ -> empty -- Polytype is always illegal
1053 unliftedArgErr, ubxArgTyErr :: Type -> SDoc
1054 unliftedArgErr ty = sep [ptext (sLit "Illegal unlifted type:"), ppr ty]
1055 ubxArgTyErr ty = sep [ptext (sLit "Illegal unboxed tuple type as function argument:"), ppr ty]
1057 kindErr :: Kind -> SDoc
1058 kindErr kind = sep [ptext (sLit "Expecting an ordinary type, but found a type of kind"), ppr kind]
1061 Note [Liberal type synonyms]
1062 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1063 If -XLiberalTypeSynonyms is on, expand closed type synonyms *before*
1064 doing validity checking. This allows us to instantiate a synonym defn
1065 with a for-all type, or with a partially-applied type synonym.
1069 Here, T is partially applied, so it's illegal in H98. But if you
1070 expand S first, then T we get just
1074 IMPORTANT: suppose T is a type synonym. Then we must do validity
1075 checking on an appliation (T ty1 ty2)
1077 *either* before expansion (i.e. check ty1, ty2)
1078 *or* after expansion (i.e. expand T ty1 ty2, and then check)
1081 If we do both, we get exponential behaviour!!
1083 data TIACons1 i r c = c i ::: r c
1084 type TIACons2 t x = TIACons1 t (TIACons1 t x)
1085 type TIACons3 t x = TIACons2 t (TIACons1 t x)
1086 type TIACons4 t x = TIACons2 t (TIACons2 t x)
1087 type TIACons7 t x = TIACons4 t (TIACons3 t x)
1090 %************************************************************************
1092 \subsection{Checking a theta or source type}
1094 %************************************************************************
1097 -- Enumerate the contexts in which a "source type", <S>, can occur
1101 -- or (N a) where N is a newtype
1104 = ClassSCCtxt Name -- Superclasses of clas
1105 -- class <S> => C a where ...
1106 | SigmaCtxt -- Theta part of a normal for-all type
1107 -- f :: <S> => a -> a
1108 | DataTyCtxt Name -- Theta part of a data decl
1109 -- data <S> => T a = MkT a
1110 | TypeCtxt -- Source type in an ordinary type
1112 | InstThetaCtxt -- Context of an instance decl
1113 -- instance <S> => C [a] where ...
1115 pprSourceTyCtxt :: SourceTyCtxt -> SDoc
1116 pprSourceTyCtxt (ClassSCCtxt c) = ptext (sLit "the super-classes of class") <+> quotes (ppr c)
1117 pprSourceTyCtxt SigmaCtxt = ptext (sLit "the context of a polymorphic type")
1118 pprSourceTyCtxt (DataTyCtxt tc) = ptext (sLit "the context of the data type declaration for") <+> quotes (ppr tc)
1119 pprSourceTyCtxt InstThetaCtxt = ptext (sLit "the context of an instance declaration")
1120 pprSourceTyCtxt TypeCtxt = ptext (sLit "the context of a type")
1124 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
1125 checkValidTheta ctxt theta
1126 = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
1128 -------------------------
1129 check_valid_theta :: SourceTyCtxt -> [PredType] -> TcM ()
1130 check_valid_theta _ []
1132 check_valid_theta ctxt theta = do
1134 warnTc (notNull dups) (dupPredWarn dups)
1135 mapM_ (check_pred_ty dflags ctxt) theta
1137 (_,dups) = removeDups tcCmpPred theta
1139 -------------------------
1140 check_pred_ty :: DynFlags -> SourceTyCtxt -> PredType -> TcM ()
1141 check_pred_ty dflags ctxt pred@(ClassP cls tys)
1142 = do { -- Class predicates are valid in all contexts
1143 ; checkTc (arity == n_tys) arity_err
1145 -- Check the form of the argument types
1146 ; mapM_ checkValidMonoType tys
1147 ; checkTc (check_class_pred_tys dflags ctxt tys)
1148 (predTyVarErr pred $$ how_to_allow)
1151 class_name = className cls
1152 arity = classArity cls
1154 arity_err = arityErr "Class" class_name arity n_tys
1155 how_to_allow = parens (ptext (sLit "Use -XFlexibleContexts to permit this"))
1158 check_pred_ty dflags _ pred@(EqPred ty1 ty2)
1159 = do { -- Equational constraints are valid in all contexts if type
1160 -- families are permitted
1161 ; checkTc (xopt Opt_TypeFamilies dflags) (eqPredTyErr pred)
1163 -- Check the form of the argument types
1164 ; checkValidMonoType ty1
1165 ; checkValidMonoType ty2
1168 check_pred_ty _ SigmaCtxt (IParam _ ty) = checkValidMonoType ty
1169 -- Implicit parameters only allowed in type
1170 -- signatures; not in instance decls, superclasses etc
1171 -- The reason for not allowing implicit params in instances is a bit
1173 -- If we allowed instance (?x::Int, Eq a) => Foo [a] where ...
1174 -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
1175 -- discharge all the potential usas of the ?x in e. For example, a
1176 -- constraint Foo [Int] might come out of e,and applying the
1177 -- instance decl would show up two uses of ?x.
1180 check_pred_ty _ _ sty = failWithTc (badPredTyErr sty)
1182 -------------------------
1183 check_class_pred_tys :: DynFlags -> SourceTyCtxt -> [Type] -> Bool
1184 check_class_pred_tys dflags ctxt tys
1186 TypeCtxt -> True -- {-# SPECIALISE instance Eq (T Int) #-} is fine
1187 InstThetaCtxt -> flexible_contexts || undecidable_ok || all tcIsTyVarTy tys
1188 -- Further checks on head and theta in
1189 -- checkInstTermination
1190 _ -> flexible_contexts || all tyvar_head tys
1192 flexible_contexts = xopt Opt_FlexibleContexts dflags
1193 undecidable_ok = xopt Opt_UndecidableInstances dflags
1195 -------------------------
1196 tyvar_head :: Type -> Bool
1197 tyvar_head ty -- Haskell 98 allows predicates of form
1198 | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
1199 | otherwise -- where a is a type variable
1200 = case tcSplitAppTy_maybe ty of
1201 Just (ty, _) -> tyvar_head ty
1208 is ambiguous if P contains generic variables
1209 (i.e. one of the Vs) that are not mentioned in tau
1211 However, we need to take account of functional dependencies
1212 when we speak of 'mentioned in tau'. Example:
1213 class C a b | a -> b where ...
1215 forall x y. (C x y) => x
1216 is not ambiguous because x is mentioned and x determines y
1218 NB; the ambiguity check is only used for *user* types, not for types
1219 coming from inteface files. The latter can legitimately have
1220 ambiguous types. Example
1222 class S a where s :: a -> (Int,Int)
1223 instance S Char where s _ = (1,1)
1224 f:: S a => [a] -> Int -> (Int,Int)
1225 f (_::[a]) x = (a*x,b)
1226 where (a,b) = s (undefined::a)
1228 Here the worker for f gets the type
1229 fw :: forall a. S a => Int -> (# Int, Int #)
1231 If the list of tv_names is empty, we have a monotype, and then we
1232 don't need to check for ambiguity either, because the test can't fail
1235 In addition, GHC insists that at least one type variable
1236 in each constraint is in V. So we disallow a type like
1237 forall a. Eq b => b -> b
1238 even in a scope where b is in scope.
1241 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
1242 checkAmbiguity forall_tyvars theta tau_tyvars
1243 = mapM_ complain (filter is_ambig theta)
1245 complain pred = addErrTc (ambigErr pred)
1246 extended_tau_vars = growThetaTyVars theta tau_tyvars
1248 -- See Note [Implicit parameters and ambiguity] in TcSimplify
1249 is_ambig pred = isClassPred pred &&
1250 any ambig_var (varSetElems (tyVarsOfPred pred))
1252 ambig_var ct_var = (ct_var `elem` forall_tyvars) &&
1253 not (ct_var `elemVarSet` extended_tau_vars)
1255 ambigErr :: PredType -> SDoc
1257 = sep [ptext (sLit "Ambiguous constraint") <+> quotes (pprPred pred),
1258 nest 2 (ptext (sLit "At least one of the forall'd type variables mentioned by the constraint") $$
1259 ptext (sLit "must be reachable from the type after the '=>'"))]
1262 Note [Growing the tau-tvs using constraints]
1263 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1264 (growInstsTyVars insts tvs) is the result of extending the set
1265 of tyvars tvs using all conceivable links from pred
1267 E.g. tvs = {a}, preds = {H [a] b, K (b,Int) c, Eq e}
1268 Then grow precs tvs = {a,b,c}
1271 growThetaTyVars :: TcThetaType -> TyVarSet -> TyVarSet
1272 -- See Note [Growing the tau-tvs using constraints]
1273 growThetaTyVars theta tvs
1275 | otherwise = fixVarSet mk_next tvs
1277 mk_next tvs = foldr grow_one tvs theta
1278 grow_one pred tvs = growPredTyVars pred tvs `unionVarSet` tvs
1280 growPredTyVars :: TcPredType
1281 -> TyVarSet -- The set to extend
1282 -> TyVarSet -- TyVars of the predicate if it intersects
1283 -- the set, or is implicit parameter
1284 growPredTyVars pred tvs
1285 | IParam {} <- pred = pred_tvs -- See Note [Implicit parameters and ambiguity]
1286 | pred_tvs `intersectsVarSet` tvs = pred_tvs
1287 | otherwise = emptyVarSet
1289 pred_tvs = tyVarsOfPred pred
1292 Note [Implicit parameters and ambiguity]
1293 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1294 Only a *class* predicate can give rise to ambiguity
1295 An *implicit parameter* cannot. For example:
1296 foo :: (?x :: [a]) => Int
1298 is fine. The call site will suppply a particular 'x'
1300 Furthermore, the type variables fixed by an implicit parameter
1301 propagate to the others. E.g.
1302 foo :: (Show a, ?x::[a]) => Int
1304 The type of foo looks ambiguous. But it isn't, because at a call site
1306 let ?x = 5::Int in foo
1307 and all is well. In effect, implicit parameters are, well, parameters,
1308 so we can take their type variables into account as part of the
1309 "tau-tvs" stuff. This is done in the function 'FunDeps.grow'.
1313 checkThetaCtxt :: SourceTyCtxt -> ThetaType -> SDoc
1314 checkThetaCtxt ctxt theta
1315 = vcat [ptext (sLit "In the context:") <+> pprTheta theta,
1316 ptext (sLit "While checking") <+> pprSourceTyCtxt ctxt ]
1318 badPredTyErr, eqPredTyErr, predTyVarErr :: PredType -> SDoc
1319 badPredTyErr sty = ptext (sLit "Illegal constraint") <+> pprPred sty
1320 eqPredTyErr sty = ptext (sLit "Illegal equational constraint") <+> pprPred sty
1322 parens (ptext (sLit "Use -XTypeFamilies to permit this"))
1323 predTyVarErr pred = sep [ptext (sLit "Non type-variable argument"),
1324 nest 2 (ptext (sLit "in the constraint:") <+> pprPred pred)]
1325 dupPredWarn :: [[PredType]] -> SDoc
1326 dupPredWarn dups = ptext (sLit "Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
1328 arityErr :: Outputable a => String -> a -> Int -> Int -> SDoc
1329 arityErr kind name n m
1330 = hsep [ text kind, quotes (ppr name), ptext (sLit "should have"),
1331 n_arguments <> comma, text "but has been given",
1332 if m==0 then text "none" else int m]
1334 n_arguments | n == 0 = ptext (sLit "no arguments")
1335 | n == 1 = ptext (sLit "1 argument")
1336 | True = hsep [int n, ptext (sLit "arguments")]
1339 %************************************************************************
1341 \subsection{Checking for a decent instance head type}
1343 %************************************************************************
1345 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1346 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1348 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1349 flag is on, or (2)~the instance is imported (they must have been
1350 compiled elsewhere). In these cases, we let them go through anyway.
1352 We can also have instances for functions: @instance Foo (a -> b) ...@.
1355 checkValidInstHead :: Type -> TcM (Class, [TcType])
1357 checkValidInstHead ty -- Should be a source type
1358 = case tcSplitPredTy_maybe ty of {
1359 Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
1362 case getClassPredTys_maybe pred of {
1363 Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
1364 Just (clas,tys) -> do
1367 check_inst_head dflags clas tys
1371 check_inst_head :: DynFlags -> Class -> [Type] -> TcM ()
1372 check_inst_head dflags clas tys
1373 = do { -- If GlasgowExts then check at least one isn't a type variable
1374 ; checkTc (xopt Opt_TypeSynonymInstances dflags ||
1375 all tcInstHeadTyNotSynonym tys)
1376 (instTypeErr (pprClassPred clas tys) head_type_synonym_msg)
1377 ; checkTc (xopt Opt_FlexibleInstances dflags ||
1378 all tcInstHeadTyAppAllTyVars tys)
1379 (instTypeErr (pprClassPred clas tys) head_type_args_tyvars_msg)
1380 ; checkTc (xopt Opt_MultiParamTypeClasses dflags ||
1382 (instTypeErr (pprClassPred clas tys) head_one_type_msg)
1383 -- May not contain type family applications
1384 ; mapM_ checkTyFamFreeness tys
1386 ; mapM_ checkValidMonoType tys
1387 -- For now, I only allow tau-types (not polytypes) in
1388 -- the head of an instance decl.
1389 -- E.g. instance C (forall a. a->a) is rejected
1390 -- One could imagine generalising that, but I'm not sure
1391 -- what all the consequences might be
1395 head_type_synonym_msg = parens (
1396 text "All instance types must be of the form (T t1 ... tn)" $$
1397 text "where T is not a synonym." $$
1398 text "Use -XTypeSynonymInstances if you want to disable this.")
1400 head_type_args_tyvars_msg = parens (vcat [
1401 text "All instance types must be of the form (T a1 ... an)",
1402 text "where a1 ... an are type *variables*,",
1403 text "and each type variable appears at most once in the instance head.",
1404 text "Use -XFlexibleInstances if you want to disable this."])
1406 head_one_type_msg = parens (
1407 text "Only one type can be given in an instance head." $$
1408 text "Use -XMultiParamTypeClasses if you want to allow more.")
1410 instTypeErr :: SDoc -> SDoc -> SDoc
1411 instTypeErr pp_ty msg
1412 = sep [ptext (sLit "Illegal instance declaration for") <+> quotes pp_ty,
1417 %************************************************************************
1419 \subsection{Checking instance for termination}
1421 %************************************************************************
1424 checkValidInstance :: LHsType Name -> [TyVar] -> ThetaType -> Type
1425 -> TcM (Class, [TcType])
1426 checkValidInstance hs_type tyvars theta tau
1427 = setSrcSpan (getLoc hs_type) $
1428 do { (clas, inst_tys) <- setSrcSpan head_loc $
1429 checkValidInstHead tau
1431 ; undecidable_ok <- xoptM Opt_UndecidableInstances
1433 ; checkValidTheta InstThetaCtxt theta
1434 ; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys)
1436 -- Check that instance inference will terminate (if we care)
1437 -- For Haskell 98 this will already have been done by checkValidTheta,
1438 -- but as we may be using other extensions we need to check.
1439 ; unless undecidable_ok $
1440 mapM_ addErrTc (checkInstTermination inst_tys theta)
1442 -- The Coverage Condition
1443 ; checkTc (undecidable_ok || checkInstCoverage clas inst_tys)
1444 (instTypeErr (pprClassPred clas inst_tys) msg)
1446 ; return (clas, inst_tys)
1449 msg = parens (vcat [ptext (sLit "the Coverage Condition fails for one of the functional dependencies;"),
1452 -- The location of the "head" of the instance
1453 head_loc = case hs_type of
1454 L _ (HsForAllTy _ _ _ (L loc _)) -> loc
1458 Termination test: the so-called "Paterson conditions" (see Section 5 of
1459 "Understanding functionsl dependencies via Constraint Handling Rules,
1462 We check that each assertion in the context satisfies:
1463 (1) no variable has more occurrences in the assertion than in the head, and
1464 (2) the assertion has fewer constructors and variables (taken together
1465 and counting repetitions) than the head.
1466 This is only needed with -fglasgow-exts, as Haskell 98 restrictions
1467 (which have already been checked) guarantee termination.
1469 The underlying idea is that
1471 for any ground substitution, each assertion in the
1472 context has fewer type constructors than the head.
1476 checkInstTermination :: [TcType] -> ThetaType -> [Message]
1477 checkInstTermination tys theta
1478 = mapCatMaybes check theta
1481 size = sizeTypes tys
1483 | not (null (fvPred pred \\ fvs))
1484 = Just (predUndecErr pred nomoreMsg $$ parens undecidableMsg)
1485 | sizePred pred >= size
1486 = Just (predUndecErr pred smallerMsg $$ parens undecidableMsg)
1490 predUndecErr :: PredType -> SDoc -> SDoc
1491 predUndecErr pred msg = sep [msg,
1492 nest 2 (ptext (sLit "in the constraint:") <+> pprPred pred)]
1494 nomoreMsg, smallerMsg, undecidableMsg :: SDoc
1495 nomoreMsg = ptext (sLit "Variable occurs more often in a constraint than in the instance head")
1496 smallerMsg = ptext (sLit "Constraint is no smaller than the instance head")
1497 undecidableMsg = ptext (sLit "Use -XUndecidableInstances to permit this")
1500 validDeivPred checks for OK 'deriving' context. See Note [Exotic
1501 derived instance contexts] in TcSimplify. However the predicate is
1502 here because it uses sizeTypes, fvTypes.
1505 validDerivPred :: PredType -> Bool
1506 validDerivPred (ClassP _ tys) = hasNoDups fvs && sizeTypes tys == length fvs
1507 where fvs = fvTypes tys
1508 validDerivPred _ = False
1512 %************************************************************************
1514 Checking type instance well-formedness and termination
1516 %************************************************************************
1519 -- Check that a "type instance" is well-formed (which includes decidability
1520 -- unless -XUndecidableInstances is given).
1522 checkValidTypeInst :: [Type] -> Type -> TcM ()
1523 checkValidTypeInst typats rhs
1524 = do { -- left-hand side contains no type family applications
1525 -- (vanilla synonyms are fine, though)
1526 ; mapM_ checkTyFamFreeness typats
1528 -- the right-hand side is a tau type
1529 ; checkValidMonoType rhs
1531 -- we have a decidable instance unless otherwise permitted
1532 ; undecidable_ok <- xoptM Opt_UndecidableInstances
1533 ; unless undecidable_ok $
1534 mapM_ addErrTc (checkFamInst typats (tyFamInsts rhs))
1537 -- Make sure that each type family instance is
1538 -- (1) strictly smaller than the lhs,
1539 -- (2) mentions no type variable more often than the lhs, and
1540 -- (3) does not contain any further type family instances.
1542 checkFamInst :: [Type] -- lhs
1543 -> [(TyCon, [Type])] -- type family instances
1545 checkFamInst lhsTys famInsts
1546 = mapCatMaybes check famInsts
1548 size = sizeTypes lhsTys
1549 fvs = fvTypes lhsTys
1551 | not (all isTyFamFree tys)
1552 = Just (famInstUndecErr famInst nestedMsg $$ parens undecidableMsg)
1553 | not (null (fvTypes tys \\ fvs))
1554 = Just (famInstUndecErr famInst nomoreVarMsg $$ parens undecidableMsg)
1555 | size <= sizeTypes tys
1556 = Just (famInstUndecErr famInst smallerAppMsg $$ parens undecidableMsg)
1560 famInst = TyConApp tc tys
1562 -- Ensure that no type family instances occur in a type.
1564 checkTyFamFreeness :: Type -> TcM ()
1565 checkTyFamFreeness ty
1566 = checkTc (isTyFamFree ty) $
1567 tyFamInstIllegalErr ty
1569 -- Check that a type does not contain any type family applications.
1571 isTyFamFree :: Type -> Bool
1572 isTyFamFree = null . tyFamInsts
1576 tyFamInstIllegalErr :: Type -> SDoc
1577 tyFamInstIllegalErr ty
1578 = hang (ptext (sLit "Illegal type synonym family application in instance") <>
1582 famInstUndecErr :: Type -> SDoc -> SDoc
1583 famInstUndecErr ty msg
1585 nest 2 (ptext (sLit "in the type family application:") <+>
1588 nestedMsg, nomoreVarMsg, smallerAppMsg :: SDoc
1589 nestedMsg = ptext (sLit "Nested type family application")
1590 nomoreVarMsg = ptext (sLit "Variable occurs more often than in instance head")
1591 smallerAppMsg = ptext (sLit "Application is no smaller than the instance head")
1595 %************************************************************************
1597 \subsection{Auxiliary functions}
1599 %************************************************************************
1602 -- Free variables of a type, retaining repetitions, and expanding synonyms
1603 fvType :: Type -> [TyVar]
1604 fvType ty | Just exp_ty <- tcView ty = fvType exp_ty
1605 fvType (TyVarTy tv) = [tv]
1606 fvType (TyConApp _ tys) = fvTypes tys
1607 fvType (PredTy pred) = fvPred pred
1608 fvType (FunTy arg res) = fvType arg ++ fvType res
1609 fvType (AppTy fun arg) = fvType fun ++ fvType arg
1610 fvType (ForAllTy tyvar ty) = filter (/= tyvar) (fvType ty)
1612 fvTypes :: [Type] -> [TyVar]
1613 fvTypes tys = concat (map fvType tys)
1615 fvPred :: PredType -> [TyVar]
1616 fvPred (ClassP _ tys') = fvTypes tys'
1617 fvPred (IParam _ ty) = fvType ty
1618 fvPred (EqPred ty1 ty2) = fvType ty1 ++ fvType ty2
1620 -- Size of a type: the number of variables and constructors
1621 sizeType :: Type -> Int
1622 sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty
1623 sizeType (TyVarTy _) = 1
1624 sizeType (TyConApp _ tys) = sizeTypes tys + 1
1625 sizeType (PredTy pred) = sizePred pred
1626 sizeType (FunTy arg res) = sizeType arg + sizeType res + 1
1627 sizeType (AppTy fun arg) = sizeType fun + sizeType arg
1628 sizeType (ForAllTy _ ty) = sizeType ty
1630 sizeTypes :: [Type] -> Int
1631 sizeTypes xs = sum (map sizeType xs)
1633 -- Size of a predicate
1635 -- We are considering whether *class* constraints terminate
1636 -- Once we get into an implicit parameter or equality we
1637 -- can't get back to a class constraint, so it's safe
1638 -- to say "size 0". See Trac #4200.
1639 sizePred :: PredType -> Int
1640 sizePred (ClassP _ tys') = sizeTypes tys'
1641 sizePred (IParam {}) = 0
1642 sizePred (EqPred {}) = 0