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 -- The above warning supression flag is a temporary kludge.
14 -- While working on this module you are encouraged to remove it and fix
15 -- any warnings in the module. See
16 -- http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
20 TcTyVar, TcKind, TcType, TcTauType, TcThetaType, TcTyVarSet,
22 --------------------------------
23 -- Creating new mutable type variables
25 newFlexiTyVarTy, -- Kind -> TcM TcType
26 newFlexiTyVarTys, -- Int -> Kind -> TcM [TcType]
27 newKindVar, newKindVars,
28 lookupTcTyVar, LookupTyVarResult(..),
30 newMetaTyVar, readMetaTyVar, writeMetaTyVar, isFilledMetaTyVar,
32 --------------------------------
33 -- Boxy type variables
34 newBoxyTyVar, newBoxyTyVars, newBoxyTyVarTys, readFilledBox,
36 --------------------------------
37 -- Creating new coercion variables
38 newCoVars, newMetaCoVar,
40 --------------------------------
42 tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxyTyVar,
44 tcInstSkolTyVar, tcInstSkolTyVars, tcInstSkolType,
45 tcSkolSigType, tcSkolSigTyVars, occurCheckErr,
47 --------------------------------
48 -- Checking type validity
49 Rank, UserTypeCtxt(..), checkValidType, checkValidMonoType,
50 SourceTyCtxt(..), checkValidTheta, checkFreeness,
51 checkValidInstHead, checkValidInstance,
52 checkInstTermination, checkValidTypeInst, checkTyFamFreeness,
53 checkUpdateMeta, updateMeta, checkTauTvUpdate, fillBoxWithTau, unifyKindCtxt,
54 unifyKindMisMatch, validDerivPred, arityErr, notMonoType, notMonoArgs,
56 --------------------------------
58 zonkType, zonkTcPredType,
59 zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkSigTyVar,
60 zonkQuantifiedTyVar, zonkQuantifiedTyVars,
61 zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
62 zonkTcKindToKind, zonkTcKind, zonkTopTyVar,
64 readKindVar, writeKindVar
67 #include "HsVersions.h"
79 import TcRnMonad -- TcType, amongst others
93 import Control.Monad ( when, unless )
94 import Data.List ( (\\) )
98 %************************************************************************
100 Instantiation in general
102 %************************************************************************
105 tcInstType :: ([TyVar] -> TcM [TcTyVar]) -- How to instantiate the type variables
106 -> TcType -- Type to instantiate
107 -> TcM ([TcTyVar], TcThetaType, TcType) -- Result
108 -- (type vars (excl coercion vars), preds (incl equalities), rho)
109 tcInstType inst_tyvars ty
110 = case tcSplitForAllTys ty of
111 ([], rho) -> let -- There may be overloading despite no type variables;
112 -- (?x :: Int) => Int -> Int
113 (theta, tau) = tcSplitPhiTy rho
115 return ([], theta, tau)
117 (tyvars, rho) -> do { tyvars' <- inst_tyvars tyvars
119 ; let tenv = zipTopTvSubst tyvars (mkTyVarTys tyvars')
120 -- Either the tyvars are freshly made, by inst_tyvars,
121 -- or (in the call from tcSkolSigType) any nested foralls
122 -- have different binders. Either way, zipTopTvSubst is ok
124 ; let (theta, tau) = tcSplitPhiTy (substTy tenv rho)
125 ; return (tyvars', theta, tau) }
129 %************************************************************************
133 %************************************************************************
135 Can't be in TcUnify, as we also need it in TcTyFuns.
139 -- False <=> the two args are (actual, expected) respectively
140 -- True <=> the two args are (expected, actual) respectively
142 checkUpdateMeta :: SwapFlag
143 -> TcTyVar -> IORef MetaDetails -> TcType -> TcM ()
144 -- Update tv1, which is flexi; occurs check is alrady done
145 -- The 'check' version does a kind check too
146 -- We do a sub-kind check here: we might unify (a b) with (c d)
147 -- where b::*->* and d::*; this should fail
149 checkUpdateMeta swapped tv1 ref1 ty2
150 = do { checkKinds swapped tv1 ty2
151 ; updateMeta tv1 ref1 ty2 }
153 updateMeta :: TcTyVar -> IORef MetaDetails -> TcType -> TcM ()
154 updateMeta tv1 ref1 ty2
155 = ASSERT( isMetaTyVar tv1 )
156 ASSERT( isBoxyTyVar tv1 || isTauTy ty2 )
157 do { ASSERTM2( do { details <- readMetaTyVar tv1; return (isFlexi details) }, ppr tv1 )
158 ; traceTc (text "updateMeta" <+> ppr tv1 <+> text ":=" <+> ppr ty2)
159 ; writeMutVar ref1 (Indirect ty2)
163 checkKinds swapped tv1 ty2
164 -- We're about to unify a type variable tv1 with a non-tyvar-type ty2.
165 -- ty2 has been zonked at this stage, which ensures that
166 -- its kind has as much boxity information visible as possible.
167 | tk2 `isSubKind` tk1 = return ()
170 -- Either the kinds aren't compatible
171 -- (can happen if we unify (a b) with (c d))
172 -- or we are unifying a lifted type variable with an
173 -- unlifted type: e.g. (id 3#) is illegal
174 = addErrCtxtM (unifyKindCtxt swapped tv1 ty2) $
175 unifyKindMisMatch k1 k2
177 (k1,k2) | swapped = (tk2,tk1)
178 | otherwise = (tk1,tk2)
183 checkTauTvUpdate :: TcTyVar -> TcType -> TcM (Maybe TcType)
184 -- (checkTauTvUpdate tv ty)
185 -- We are about to update the TauTv tv with ty.
186 -- Check (a) that tv doesn't occur in ty (occurs check)
187 -- (b) that ty is a monotype
188 -- Furthermore, in the interest of (b), if you find an
189 -- empty box (BoxTv that is Flexi), fill it in with a TauTv
191 -- We have three possible outcomes:
192 -- (1) Return the (non-boxy) type to update the type variable with,
193 -- [we know the update is ok!]
194 -- (2) return Nothing, or
195 -- [we cannot tell whether the update is ok right now]
197 -- [the update is definitely invalid]
198 -- We return Nothing in case the tv occurs in ty *under* a type family
199 -- application. In this case, we must not update tv (to avoid a cyclic type
200 -- term), but we also cannot fail claiming an infinite type. Given
202 -- type instance F Int = Int
205 -- This is perfectly reasonable, if we later get a ~ Int.
207 checkTauTvUpdate orig_tv orig_ty
208 = do { result <- go orig_ty
210 Right ty -> return $ Just ty
211 Left True -> return $ Nothing
212 Left False -> occurCheckErr (mkTyVarTy orig_tv) orig_ty
215 go :: TcType -> TcM (Either Bool TcType)
217 -- Right ty if everything is fine
218 -- Left True if orig_tv occurs in orig_ty, but under a type family app
219 -- Left False if orig_tv occurs in orig_ty (with no type family app)
220 -- It fails if it encounters a forall type, except as an argument for a
221 -- closed type synonym that expands to a tau type.
223 | isSynTyCon tc = go_syn tc tys
224 | otherwise = do { tys' <- mapM go tys
225 ; return $ occurs (TyConApp tc) tys' }
226 go (PredTy p) = do { p' <- go_pred p
227 ; return $ occurs1 PredTy p' }
228 go (FunTy arg res) = do { arg' <- go arg
230 ; return $ occurs2 FunTy arg' res' }
231 go (AppTy fun arg) = do { fun' <- go fun
233 ; return $ occurs2 mkAppTy fun' arg' }
234 -- NB the mkAppTy; we might have instantiated a
235 -- type variable to a type constructor, so we need
236 -- to pull the TyConApp to the top.
237 go (ForAllTy tv ty) = notMonoType orig_ty -- (b)
240 | orig_tv == tv = return $ Left False -- (a)
241 | isTcTyVar tv = go_tyvar tv (tcTyVarDetails tv)
242 | otherwise = return $ Right (TyVarTy tv)
243 -- Ordinary (non Tc) tyvars
244 -- occur inside quantified types
246 go_pred (ClassP c tys) = do { tys' <- mapM go tys
247 ; return $ occurs (ClassP c) tys' }
248 go_pred (IParam n ty) = do { ty' <- go ty
249 ; return $ occurs1 (IParam n) ty' }
250 go_pred (EqPred t1 t2) = do { t1' <- go t1
252 ; return $ occurs2 EqPred t1' t2' }
254 go_tyvar tv (SkolemTv _) = return $ Right (TyVarTy tv)
255 go_tyvar tv (MetaTv box ref)
256 = do { cts <- readMutVar ref
260 BoxTv -> do { ty <- fillBoxWithTau tv ref
261 ; return $ Right ty }
262 other -> return $ Right (TyVarTy tv)
265 -- go_syn is called for synonyms only
266 -- See Note [Type synonyms and the occur check]
268 | not (isTauTyCon tc)
269 = notMonoType orig_ty -- (b) again
271 = do { (msgs, mb_tys') <- tryTc (mapM go tys)
274 -- we had a type error => forall in type parameters
276 | isOpenTyCon tc -> notMonoArgs (TyConApp tc tys)
277 -- Synonym families must have monotype args
278 | otherwise -> go (expectJust "checkTauTvUpdate(1)"
279 (tcView (TyConApp tc tys)))
280 -- Try again, expanding the synonym
282 -- no type error, but need to test whether occurs check happend
284 case occurs id tys' of
286 | isOpenTyCon tc -> return $ Left True
287 -- Variable occured under type family application
288 | otherwise -> go (expectJust "checkTauTvUpdate(2)"
289 (tcView (TyConApp tc tys)))
290 -- Try again, expanding the synonym
291 Right raw_tys' -> return $ Right (TyConApp tc raw_tys')
292 -- Retain the synonym (the common case)
295 -- Left results (= occurrence of orig_ty) dominate and
296 -- (Left False) (= fatal occurrence) dominates over (Left True)
297 occurs :: ([a] -> b) -> [Either Bool a] -> Either Bool b
298 occurs c = either Left (Right . c) . foldr combine (Right [])
300 combine (Left famInst1) (Left famInst2) = Left (famInst1 && famInst2)
301 combine (Right _ ) (Left famInst) = Left famInst
302 combine (Left famInst) (Right _) = Left famInst
303 combine (Right arg) (Right args) = Right (arg:args)
305 occurs1 c x = occurs (\[x'] -> c x') [x]
306 occurs2 c x y = occurs (\[x', y'] -> c x' y') [x, y]
308 fillBoxWithTau :: BoxyTyVar -> IORef MetaDetails -> TcM TcType
309 -- (fillBoxWithTau tv ref) fills ref with a freshly allocated
310 -- tau-type meta-variable, whose print-name is the same as tv
311 -- Choosing the same name is good: when we instantiate a function
312 -- we allocate boxy tyvars with the same print-name as the quantified
313 -- tyvar; and then we often fill the box with a tau-tyvar, and again
314 -- we want to choose the same name.
315 fillBoxWithTau tv ref
316 = do { tv' <- tcInstTyVar tv -- Do not gratuitously forget
317 ; let tau = mkTyVarTy tv' -- name of the type variable
318 ; writeMutVar ref (Indirect tau)
322 Note [Type synonyms and the occur check]
324 Basically we want to update tv1 := ps_ty2
325 because ps_ty2 has type-synonym info, which improves later error messages
330 f :: (A a -> a -> ()) -> ()
336 In the application (p x), we try to match "t" with "A t". If we go
337 ahead and bind t to A t (= ps_ty2), we'll lead the type checker into
338 an infinite loop later.
339 But we should not reject the program, because A t = ().
340 Rather, we should bind t to () (= non_var_ty2).
344 Error mesages in case of kind mismatch.
347 unifyKindMisMatch ty1 ty2 = do
348 ty1' <- zonkTcKind ty1
349 ty2' <- zonkTcKind ty2
351 msg = hang (ptext (sLit "Couldn't match kind"))
352 2 (sep [quotes (ppr ty1'),
353 ptext (sLit "against"),
357 unifyKindCtxt swapped tv1 ty2 tidy_env -- not swapped => tv1 expected, ty2 inferred
358 -- tv1 and ty2 are zonked already
361 msg = (env2, ptext (sLit "When matching the kinds of") <+>
362 sep [quotes pp_expected <+> ptext (sLit "and"), quotes pp_actual])
364 (pp_expected, pp_actual) | swapped = (pp2, pp1)
365 | otherwise = (pp1, pp2)
366 (env1, tv1') = tidyOpenTyVar tidy_env tv1
367 (env2, ty2') = tidyOpenType env1 ty2
368 pp1 = ppr tv1' <+> dcolon <+> ppr (tyVarKind tv1)
369 pp2 = ppr ty2' <+> dcolon <+> ppr (typeKind ty2)
372 Error message for failure due to an occurs check.
375 occurCheckErr :: TcType -> TcType -> TcM a
376 occurCheckErr ty containingTy
377 = do { env0 <- tcInitTidyEnv
378 ; ty' <- zonkTcType ty
379 ; containingTy' <- zonkTcType containingTy
380 ; let (env1, tidy_ty1) = tidyOpenType env0 ty'
381 (env2, tidy_ty2) = tidyOpenType env1 containingTy'
382 extra = sep [ppr tidy_ty1, char '=', ppr tidy_ty2]
383 ; failWithTcM (env2, hang msg 2 extra) }
385 msg = ptext (sLit "Occurs check: cannot construct the infinite type:")
388 %************************************************************************
392 %************************************************************************
395 newCoVars :: [(TcType,TcType)] -> TcM [CoVar]
397 = do { us <- newUniqueSupply
398 ; return [ mkCoVar (mkSysTvName uniq (fsLit "co"))
400 | ((ty1,ty2), uniq) <- spec `zip` uniqsFromSupply us] }
402 newMetaCoVar :: TcType -> TcType -> TcM TcTyVar
403 newMetaCoVar ty1 ty2 = newMetaTyVar TauTv (mkCoKind ty1 ty2)
405 newKindVar :: TcM TcKind
406 newKindVar = do { uniq <- newUnique
407 ; ref <- newMutVar Flexi
408 ; return (mkTyVarTy (mkKindVar uniq ref)) }
410 newKindVars :: Int -> TcM [TcKind]
411 newKindVars n = mapM (\ _ -> newKindVar) (nOfThem n ())
415 %************************************************************************
417 SkolemTvs (immutable)
419 %************************************************************************
422 mkSkolTyVar :: Name -> Kind -> SkolemInfo -> TcTyVar
423 mkSkolTyVar name kind info = mkTcTyVar name kind (SkolemTv info)
425 tcSkolSigType :: SkolemInfo -> Type -> TcM ([TcTyVar], TcThetaType, TcType)
426 -- Instantiate a type signature with skolem constants, but
427 -- do *not* give them fresh names, because we want the name to
428 -- be in the type environment -- it is lexically scoped.
429 tcSkolSigType info ty = tcInstType (\tvs -> return (tcSkolSigTyVars info tvs)) ty
431 tcSkolSigTyVars :: SkolemInfo -> [TyVar] -> [TcTyVar]
432 -- Make skolem constants, but do *not* give them new names, as above
433 tcSkolSigTyVars info tyvars = [ mkSkolTyVar (tyVarName tv) (tyVarKind tv) info
436 tcInstSkolTyVar :: SkolemInfo -> Maybe SrcSpan -> TyVar -> TcM TcTyVar
437 -- Instantiate the tyvar, using
438 -- * the occ-name and kind of the supplied tyvar,
439 -- * the unique from the monad,
440 -- * the location either from the tyvar (mb_loc = Nothing)
441 -- or from mb_loc (Just loc)
442 tcInstSkolTyVar info mb_loc tyvar
443 = do { uniq <- newUnique
444 ; let old_name = tyVarName tyvar
445 kind = tyVarKind tyvar
446 loc = mb_loc `orElse` getSrcSpan old_name
447 new_name = mkInternalName uniq (nameOccName old_name) loc
448 ; return (mkSkolTyVar new_name kind info) }
450 tcInstSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
451 -- Get the location from the monad
452 tcInstSkolTyVars info tyvars
453 = do { span <- getSrcSpanM
454 ; mapM (tcInstSkolTyVar info (Just span)) tyvars }
456 tcInstSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
457 -- Instantiate a type with fresh skolem constants
458 -- Binding location comes from the monad
459 tcInstSkolType info ty = tcInstType (tcInstSkolTyVars info) ty
463 %************************************************************************
465 MetaTvs (meta type variables; mutable)
467 %************************************************************************
470 newMetaTyVar :: BoxInfo -> Kind -> TcM TcTyVar
471 -- Make a new meta tyvar out of thin air
472 newMetaTyVar box_info kind
473 = do { uniq <- newUnique
474 ; ref <- newMutVar Flexi
475 ; let name = mkSysTvName uniq fs
476 fs = case box_info of
480 -- We give BoxTv and TauTv the same string, because
481 -- otherwise we get user-visible differences in error
482 -- messages, which are confusing. If you want to see
483 -- the box_info of each tyvar, use -dppr-debug
484 ; return (mkTcTyVar name kind (MetaTv box_info ref)) }
486 instMetaTyVar :: BoxInfo -> TyVar -> TcM TcTyVar
487 -- Make a new meta tyvar whose Name and Kind
488 -- come from an existing TyVar
489 instMetaTyVar box_info tyvar
490 = do { uniq <- newUnique
491 ; ref <- newMutVar Flexi
492 ; let name = setNameUnique (tyVarName tyvar) uniq
493 kind = tyVarKind tyvar
494 ; return (mkTcTyVar name kind (MetaTv box_info ref)) }
496 readMetaTyVar :: TyVar -> TcM MetaDetails
497 readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
498 readMutVar (metaTvRef tyvar)
500 isFilledMetaTyVar :: TyVar -> TcM Bool
501 -- True of a filled-in (Indirect) meta type variable
503 | not (isTcTyVar tv) = return False
504 | MetaTv _ ref <- tcTyVarDetails tv
505 = do { details <- readMutVar ref
506 ; return (isIndirect details) }
507 | otherwise = return False
509 writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
510 writeMetaTyVar tyvar ty
511 | not debugIsOn = writeMutVar (metaTvRef tyvar) (Indirect ty)
512 writeMetaTyVar tyvar ty
513 | not (isMetaTyVar tyvar)
514 = pprTrace "writeMetaTyVar" (ppr tyvar) $
517 = ASSERT( isMetaTyVar tyvar )
518 -- TOM: It should also work for coercions
519 -- ASSERT2( k2 `isSubKind` k1, (ppr tyvar <+> ppr k1) $$ (ppr ty <+> ppr k2) )
520 do { ASSERTM2( do { details <- readMetaTyVar tyvar; return (isFlexi details) }, ppr tyvar )
521 ; writeMutVar (metaTvRef tyvar) (Indirect ty) }
528 %************************************************************************
532 %************************************************************************
535 newFlexiTyVar :: Kind -> TcM TcTyVar
536 newFlexiTyVar kind = newMetaTyVar TauTv kind
538 newFlexiTyVarTy :: Kind -> TcM TcType
539 newFlexiTyVarTy kind = do
540 tc_tyvar <- newFlexiTyVar kind
541 return (TyVarTy tc_tyvar)
543 newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
544 newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind)
546 tcInstTyVar :: TyVar -> TcM TcTyVar
547 -- Instantiate with a META type variable
548 tcInstTyVar tyvar = instMetaTyVar TauTv tyvar
550 tcInstTyVars :: [TyVar] -> TcM ([TcTyVar], [TcType], TvSubst)
551 -- Instantiate with META type variables
553 = do { tc_tvs <- mapM tcInstTyVar tyvars
554 ; let tys = mkTyVarTys tc_tvs
555 ; return (tc_tvs, tys, zipTopTvSubst tyvars tys) }
556 -- Since the tyvars are freshly made,
557 -- they cannot possibly be captured by
558 -- any existing for-alls. Hence zipTopTvSubst
562 %************************************************************************
566 %************************************************************************
569 tcInstSigTyVars :: Bool -> SkolemInfo -> [TyVar] -> TcM [TcTyVar]
570 -- Instantiate with skolems or meta SigTvs; depending on use_skols
571 -- Always take location info from the supplied tyvars
572 tcInstSigTyVars use_skols skol_info tyvars
574 = mapM (tcInstSkolTyVar skol_info Nothing) tyvars
577 = mapM (instMetaTyVar (SigTv skol_info)) tyvars
579 zonkSigTyVar :: TcTyVar -> TcM TcTyVar
581 | isSkolemTyVar sig_tv
582 = return sig_tv -- Happens in the call in TcBinds.checkDistinctTyVars
584 = ASSERT( isSigTyVar sig_tv )
585 do { ty <- zonkTcTyVar sig_tv
586 ; return (tcGetTyVar "zonkSigTyVar" ty) }
587 -- 'ty' is bound to be a type variable, because SigTvs
588 -- can only be unified with type variables
592 %************************************************************************
596 %************************************************************************
599 newBoxyTyVar :: Kind -> TcM BoxyTyVar
600 newBoxyTyVar kind = newMetaTyVar BoxTv kind
602 newBoxyTyVars :: [Kind] -> TcM [BoxyTyVar]
603 newBoxyTyVars kinds = mapM newBoxyTyVar kinds
605 newBoxyTyVarTys :: [Kind] -> TcM [BoxyType]
606 newBoxyTyVarTys kinds = do { tvs <- mapM newBoxyTyVar kinds; return (mkTyVarTys tvs) }
608 readFilledBox :: BoxyTyVar -> TcM TcType
609 -- Read the contents of the box, which should be filled in by now
610 readFilledBox box_tv = ASSERT( isBoxyTyVar box_tv )
611 do { cts <- readMetaTyVar box_tv
613 Flexi -> pprPanic "readFilledBox" (ppr box_tv)
614 Indirect ty -> return ty }
616 tcInstBoxyTyVar :: TyVar -> TcM BoxyTyVar
617 -- Instantiate with a BOXY type variable
618 tcInstBoxyTyVar tyvar = instMetaTyVar BoxTv tyvar
622 %************************************************************************
624 \subsection{Putting and getting mutable type variables}
626 %************************************************************************
628 But it's more fun to short out indirections on the way: If this
629 version returns a TyVar, then that TyVar is unbound. If it returns
630 any other type, then there might be bound TyVars embedded inside it.
632 We return Nothing iff the original box was unbound.
635 data LookupTyVarResult -- The result of a lookupTcTyVar call
636 = DoneTv TcTyVarDetails -- SkolemTv or virgin MetaTv
639 lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult
641 = ASSERT2( isTcTyVar tyvar, ppr tyvar )
643 SkolemTv _ -> return (DoneTv details)
644 MetaTv _ ref -> do { meta_details <- readMutVar ref
645 ; case meta_details of
646 Indirect ty -> return (IndirectTv ty)
647 Flexi -> return (DoneTv details) }
649 details = tcTyVarDetails tyvar
652 -- gaw 2004 We aren't shorting anything out anymore, at least for now
654 | not (isTcTyVar tyvar)
655 = pprTrace "getTcTyVar" (ppr tyvar) $
656 return (Just (mkTyVarTy tyvar))
659 = ASSERT2( isTcTyVar tyvar, ppr tyvar ) do
660 maybe_ty <- readMetaTyVar tyvar
662 Just ty -> do ty' <- short_out ty
663 writeMetaTyVar tyvar (Just ty')
666 Nothing -> return Nothing
668 short_out :: TcType -> TcM TcType
669 short_out ty@(TyVarTy tyvar)
670 | not (isTcTyVar tyvar)
674 maybe_ty <- readMetaTyVar tyvar
676 Just ty' -> do ty' <- short_out ty'
677 writeMetaTyVar tyvar (Just ty')
682 short_out other_ty = return other_ty
687 %************************************************************************
689 \subsection{Zonking -- the exernal interfaces}
691 %************************************************************************
693 ----------------- Type variables
696 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
697 zonkTcTyVars tyvars = mapM zonkTcTyVar tyvars
699 zonkTcTyVarsAndFV :: [TcTyVar] -> TcM TcTyVarSet
700 zonkTcTyVarsAndFV tyvars = tyVarsOfTypes <$> mapM zonkTcTyVar tyvars
702 zonkTcTyVar :: TcTyVar -> TcM TcType
703 zonkTcTyVar tyvar = ASSERT2( isTcTyVar tyvar, ppr tyvar)
704 zonk_tc_tyvar (\ tv -> return (TyVarTy tv)) tyvar
707 ----------------- Types
710 zonkTcType :: TcType -> TcM TcType
711 zonkTcType ty = zonkType (\ tv -> return (TyVarTy tv)) ty
713 zonkTcTypes :: [TcType] -> TcM [TcType]
714 zonkTcTypes tys = mapM zonkTcType tys
716 zonkTcClassConstraints cts = mapM zonk cts
717 where zonk (clas, tys) = do
718 new_tys <- zonkTcTypes tys
719 return (clas, new_tys)
721 zonkTcThetaType :: TcThetaType -> TcM TcThetaType
722 zonkTcThetaType theta = mapM zonkTcPredType theta
724 zonkTcPredType :: TcPredType -> TcM TcPredType
725 zonkTcPredType (ClassP c ts) = ClassP c <$> zonkTcTypes ts
726 zonkTcPredType (IParam n t) = IParam n <$> zonkTcType t
727 zonkTcPredType (EqPred t1 t2) = EqPred <$> zonkTcType t1 <*> zonkTcType t2
730 ------------------- These ...ToType, ...ToKind versions
731 are used at the end of type checking
734 zonkTopTyVar :: TcTyVar -> TcM TcTyVar
735 -- zonkTopTyVar is used, at the top level, on any un-instantiated meta type variables
736 -- to default the kind of ? and ?? etc to *. This is important to ensure that
737 -- instance declarations match. For example consider
738 -- instance Show (a->b)
739 -- foo x = show (\_ -> True)
740 -- Then we'll get a constraint (Show (p ->q)) where p has argTypeKind (printed ??),
741 -- and that won't match the typeKind (*) in the instance decl.
743 -- Because we are at top level, no further constraints are going to affect these
744 -- type variables, so it's time to do it by hand. However we aren't ready
745 -- to default them fully to () or whatever, because the type-class defaulting
746 -- rules have yet to run.
749 | k `eqKind` default_k = return tv
751 = do { tv' <- newFlexiTyVar default_k
752 ; writeMetaTyVar tv (mkTyVarTy tv')
756 default_k = defaultKind k
758 zonkQuantifiedTyVars :: [TcTyVar] -> TcM [TcTyVar]
759 zonkQuantifiedTyVars = mapM zonkQuantifiedTyVar
761 zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar
762 -- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it.
764 -- The quantified type variables often include meta type variables
765 -- we want to freeze them into ordinary type variables, and
766 -- default their kind (e.g. from OpenTypeKind to TypeKind)
767 -- -- see notes with Kind.defaultKind
768 -- The meta tyvar is updated to point to the new skolem TyVar. Now any
769 -- bound occurences of the original type variable will get zonked to
770 -- the immutable version.
772 -- We leave skolem TyVars alone; they are immutable.
773 zonkQuantifiedTyVar tv
774 | ASSERT( isTcTyVar tv )
775 isSkolemTyVar tv = return tv
776 -- It might be a skolem type variable,
777 -- for example from a user type signature
779 | otherwise -- It's a meta-type-variable
780 = do { details <- readMetaTyVar tv
782 -- Create the new, frozen, skolem type variable
783 -- We zonk to a skolem, not to a regular TcVar
784 -- See Note [Zonking to Skolem]
785 ; let final_kind = defaultKind (tyVarKind tv)
786 final_tv = mkSkolTyVar (tyVarName tv) final_kind UnkSkol
788 -- Bind the meta tyvar to the new tyvar
790 Indirect ty -> WARN( True, ppr tv $$ ppr ty )
792 -- [Sept 04] I don't think this should happen
793 -- See note [Silly Type Synonym]
795 Flexi -> writeMetaTyVar tv (mkTyVarTy final_tv)
797 -- Return the new tyvar
801 Note [Silly Type Synonyms]
802 ~~~~~~~~~~~~~~~~~~~~~~~~~~
804 type C u a = u -- Note 'a' unused
806 foo :: (forall a. C u a -> C u a) -> u
810 bar = foo (\t -> t + t)
812 * From the (\t -> t+t) we get type {Num d} => d -> d
815 * Now unify with type of foo's arg, and we get:
816 {Num (C d a)} => C d a -> C d a
819 * Now abstract over the 'a', but float out the Num (C d a) constraint
820 because it does not 'really' mention a. (see exactTyVarsOfType)
821 The arg to foo becomes
824 * So we get a dict binding for Num (C d a), which is zonked to give
826 [Note Sept 04: now that we are zonking quantified type variables
827 on construction, the 'a' will be frozen as a regular tyvar on
828 quantification, so the floated dict will still have type (C d a).
829 Which renders this whole note moot; happily!]
831 * Then the /\a abstraction has a zonked 'a' in it.
833 All very silly. I think its harmless to ignore the problem. We'll end up with
834 a /\a in the final result but all the occurrences of a will be zonked to ()
836 Note [Zonking to Skolem]
837 ~~~~~~~~~~~~~~~~~~~~~~~~
838 We used to zonk quantified type variables to regular TyVars. However, this
839 leads to problems. Consider this program from the regression test suite:
841 eval :: Int -> String -> String -> String
842 eval 0 root actual = evalRHS 0 root actual
845 evalRHS 0 root actual = eval 0 root actual
847 It leads to the deferral of an equality
849 (String -> String -> String) ~ a
851 which is propagated up to the toplevel (see TcSimplify.tcSimplifyInferCheck).
852 In the meantime `a' is zonked and quantified to form `evalRHS's signature.
853 This has the *side effect* of also zonking the `a' in the deferred equality
854 (which at this point is being handed around wrapped in an implication
857 Finally, the equality (with the zonked `a') will be handed back to the
858 simplifier by TcRnDriver.tcRnSrcDecls calling TcSimplify.tcSimplifyTop.
859 If we zonk `a' with a regular type variable, we will have this regular type
860 variable now floating around in the simplifier, which in many places assumes to
861 only see proper TcTyVars.
863 We can avoid this problem by zonking with a skolem. The skolem is rigid
864 (which we requirefor a quantified variable), but is still a TcTyVar that the
865 simplifier knows how to deal with.
868 %************************************************************************
870 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
872 %* For internal use only! *
874 %************************************************************************
877 -- For unbound, mutable tyvars, zonkType uses the function given to it
878 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
879 -- type variable and zonks the kind too
881 zonkType :: (TcTyVar -> TcM Type) -- What to do with unbound mutable type variables
882 -- see zonkTcType, and zonkTcTypeToType
885 zonkType unbound_var_fn ty
888 go (TyConApp tc tys) = do tys' <- mapM go tys
889 return (TyConApp tc tys')
891 go (PredTy p) = do p' <- go_pred p
894 go (FunTy arg res) = do arg' <- go arg
896 return (FunTy arg' res')
898 go (AppTy fun arg) = do fun' <- go fun
900 return (mkAppTy fun' arg')
901 -- NB the mkAppTy; we might have instantiated a
902 -- type variable to a type constructor, so we need
903 -- to pull the TyConApp to the top.
905 -- The two interesting cases!
906 go (TyVarTy tyvar) | isTcTyVar tyvar = zonk_tc_tyvar unbound_var_fn tyvar
907 | otherwise = return (TyVarTy tyvar)
908 -- Ordinary (non Tc) tyvars occur inside quantified types
910 go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar ) do
912 return (ForAllTy tyvar ty')
914 go_pred (ClassP c tys) = do tys' <- mapM go tys
915 return (ClassP c tys')
916 go_pred (IParam n ty) = do ty' <- go ty
917 return (IParam n ty')
918 go_pred (EqPred ty1 ty2) = do ty1' <- go ty1
920 return (EqPred ty1' ty2')
922 zonk_tc_tyvar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable variable
923 -> TcTyVar -> TcM TcType
924 zonk_tc_tyvar unbound_var_fn tyvar
925 | not (isMetaTyVar tyvar) -- Skolems
926 = return (TyVarTy tyvar)
928 | otherwise -- Mutables
929 = do { cts <- readMetaTyVar tyvar
931 Flexi -> unbound_var_fn tyvar -- Unbound meta type variable
932 Indirect ty -> zonkType unbound_var_fn ty }
937 %************************************************************************
941 %************************************************************************
944 readKindVar :: KindVar -> TcM (MetaDetails)
945 writeKindVar :: KindVar -> TcKind -> TcM ()
946 readKindVar kv = readMutVar (kindVarRef kv)
947 writeKindVar kv val = writeMutVar (kindVarRef kv) (Indirect val)
950 zonkTcKind :: TcKind -> TcM TcKind
951 zonkTcKind k = zonkTcType k
954 zonkTcKindToKind :: TcKind -> TcM Kind
955 -- When zonking a TcKind to a kind, we need to instantiate kind variables,
956 -- Haskell specifies that * is to be used, so we follow that.
957 zonkTcKindToKind k = zonkType (\ _ -> return liftedTypeKind) k
960 %************************************************************************
962 \subsection{Checking a user type}
964 %************************************************************************
966 When dealing with a user-written type, we first translate it from an HsType
967 to a Type, performing kind checking, and then check various things that should
968 be true about it. We don't want to perform these checks at the same time
969 as the initial translation because (a) they are unnecessary for interface-file
970 types and (b) when checking a mutually recursive group of type and class decls,
971 we can't "look" at the tycons/classes yet. Also, the checks are are rather
972 diverse, and used to really mess up the other code.
974 One thing we check for is 'rank'.
976 Rank 0: monotypes (no foralls)
977 Rank 1: foralls at the front only, Rank 0 inside
978 Rank 2: foralls at the front, Rank 1 on left of fn arrow,
980 basic ::= tyvar | T basic ... basic
982 r2 ::= forall tvs. cxt => r2a
983 r2a ::= r1 -> r2a | basic
984 r1 ::= forall tvs. cxt => r0
985 r0 ::= r0 -> r0 | basic
987 Another thing is to check that type synonyms are saturated.
988 This might not necessarily show up in kind checking.
990 data T k = MkT (k Int)
995 checkValidType :: UserTypeCtxt -> Type -> TcM ()
996 -- Checks that the type is valid for the given context
997 checkValidType ctxt ty = do
998 traceTc (text "checkValidType" <+> ppr ty)
999 unboxed <- doptM Opt_UnboxedTuples
1000 rank2 <- doptM Opt_Rank2Types
1001 rankn <- doptM Opt_RankNTypes
1002 polycomp <- doptM Opt_PolymorphicComponents
1004 rank | rankn = Arbitrary
1007 = case ctxt of -- Haskell 98
1008 GenPatCtxt -> Rank 0
1009 LamPatSigCtxt -> Rank 0
1010 BindPatSigCtxt -> Rank 0
1011 DefaultDeclCtxt-> Rank 0
1012 ResSigCtxt -> Rank 0
1013 TySynCtxt _ -> Rank 0
1014 ExprSigCtxt -> Rank 1
1015 FunSigCtxt _ -> Rank 1
1016 ConArgCtxt _ -> if polycomp
1018 -- We are given the type of the entire
1019 -- constructor, hence rank 1
1021 ForSigCtxt _ -> Rank 1
1022 SpecInstCtxt -> Rank 1
1024 actual_kind = typeKind ty
1026 kind_ok = case ctxt of
1027 TySynCtxt _ -> True -- Any kind will do
1028 ResSigCtxt -> isSubOpenTypeKind actual_kind
1029 ExprSigCtxt -> isSubOpenTypeKind actual_kind
1030 GenPatCtxt -> isLiftedTypeKind actual_kind
1031 ForSigCtxt _ -> isLiftedTypeKind actual_kind
1032 other -> isSubArgTypeKind actual_kind
1034 ubx_tup = case ctxt of
1035 TySynCtxt _ | unboxed -> UT_Ok
1036 ExprSigCtxt | unboxed -> UT_Ok
1039 -- Check that the thing has kind Type, and is lifted if necessary
1040 checkTc kind_ok (kindErr actual_kind)
1042 -- Check the internal validity of the type itself
1043 check_type rank ubx_tup ty
1045 traceTc (text "checkValidType done" <+> ppr ty)
1047 checkValidMonoType :: Type -> TcM ()
1048 checkValidMonoType ty = check_mono_type ty
1053 data Rank = Rank Int | Arbitrary
1055 decRank :: Rank -> Rank
1056 decRank Arbitrary = Arbitrary
1057 decRank (Rank n) = Rank (n-1)
1059 nonZeroRank :: Rank -> Bool
1060 nonZeroRank (Rank 0) = False
1061 nonZeroRank _ = True
1063 ----------------------------------------
1064 data UbxTupFlag = UT_Ok | UT_NotOk
1065 -- The "Ok" version means "ok if -fglasgow-exts is on"
1067 ----------------------------------------
1068 check_mono_type :: Type -> TcM () -- No foralls anywhere
1069 -- No unlifted types of any kind
1071 = do { check_type (Rank 0) UT_NotOk ty
1072 ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
1074 check_type :: Rank -> UbxTupFlag -> Type -> TcM ()
1075 -- The args say what the *type* context requires, independent
1076 -- of *flag* settings. You test the flag settings at usage sites.
1078 -- Rank is allowed rank for function args
1079 -- Rank 0 means no for-alls anywhere
1081 check_type rank ubx_tup ty
1082 | not (null tvs && null theta)
1083 = do { checkTc (nonZeroRank rank) (forAllTyErr ty)
1084 -- Reject e.g. (Maybe (?x::Int => Int)),
1085 -- with a decent error message
1086 ; check_valid_theta SigmaCtxt theta
1087 ; check_type rank ubx_tup tau -- Allow foralls to right of arrow
1088 ; checkFreeness tvs theta
1089 ; checkAmbiguity tvs theta (tyVarsOfType tau) }
1091 (tvs, theta, tau) = tcSplitSigmaTy ty
1093 -- Naked PredTys don't usually show up, but they can as a result of
1094 -- {-# SPECIALISE instance Ord Char #-}
1095 -- The Right Thing would be to fix the way that SPECIALISE instance pragmas
1096 -- are handled, but the quick thing is just to permit PredTys here.
1097 check_type rank ubx_tup (PredTy sty)
1098 = do { dflags <- getDOpts
1099 ; check_pred_ty dflags TypeCtxt sty }
1101 check_type rank ubx_tup (TyVarTy _) = return ()
1102 check_type rank ubx_tup ty@(FunTy arg_ty res_ty)
1103 = do { check_type (decRank rank) UT_NotOk arg_ty
1104 ; check_type rank UT_Ok res_ty }
1106 check_type rank ubx_tup (AppTy ty1 ty2)
1107 = do { check_arg_type rank ty1
1108 ; check_arg_type rank ty2 }
1110 check_type rank ubx_tup ty@(TyConApp tc tys)
1112 = do { -- Check that the synonym has enough args
1113 -- This applies equally to open and closed synonyms
1114 -- It's OK to have an *over-applied* type synonym
1115 -- data Tree a b = ...
1116 -- type Foo a = Tree [a]
1117 -- f :: Foo a b -> ...
1118 checkTc (tyConArity tc <= length tys) arity_msg
1120 -- See Note [Liberal type synonyms]
1121 ; liberal <- doptM Opt_LiberalTypeSynonyms
1122 ; if not liberal || isOpenSynTyCon tc then
1123 -- For H98 and synonym families, do check the type args
1124 mapM_ check_mono_type tys
1126 else -- In the liberal case (only for closed syns), expand then check
1128 Just ty' -> check_type rank ubx_tup ty'
1129 Nothing -> pprPanic "check_tau_type" (ppr ty)
1132 | isUnboxedTupleTyCon tc
1133 = do { ub_tuples_allowed <- doptM Opt_UnboxedTuples
1134 ; checkTc (ubx_tup_ok ub_tuples_allowed) ubx_tup_msg
1136 ; impred <- doptM Opt_ImpredicativeTypes
1137 ; let rank' = if impred then rank else Rank 0
1138 -- c.f. check_arg_type
1139 -- However, args are allowed to be unlifted, or
1140 -- more unboxed tuples, so can't use check_arg_ty
1141 ; mapM_ (check_type rank' UT_Ok) tys }
1144 = mapM_ (check_arg_type rank) tys
1147 ubx_tup_ok ub_tuples_allowed = case ubx_tup of { UT_Ok -> ub_tuples_allowed; other -> False }
1150 tc_arity = tyConArity tc
1152 arity_msg = arityErr "Type synonym" (tyConName tc) tc_arity n_args
1153 ubx_tup_msg = ubxArgTyErr ty
1155 ----------------------------------------
1156 check_arg_type :: Rank -> Type -> TcM ()
1157 -- The sort of type that can instantiate a type variable,
1158 -- or be the argument of a type constructor.
1159 -- Not an unboxed tuple, but now *can* be a forall (since impredicativity)
1160 -- Other unboxed types are very occasionally allowed as type
1161 -- arguments depending on the kind of the type constructor
1163 -- For example, we want to reject things like:
1165 -- instance Ord a => Ord (forall s. T s a)
1167 -- g :: T s (forall b.b)
1169 -- NB: unboxed tuples can have polymorphic or unboxed args.
1170 -- This happens in the workers for functions returning
1171 -- product types with polymorphic components.
1172 -- But not in user code.
1173 -- Anyway, they are dealt with by a special case in check_tau_type
1175 check_arg_type rank ty
1176 = do { impred <- doptM Opt_ImpredicativeTypes
1177 ; let rank' = if impred then rank else Rank 0 -- Monotype unless impredicative
1178 ; check_type rank' UT_NotOk ty
1179 ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
1181 ----------------------------------------
1182 forAllTyErr ty = sep [ptext (sLit "Illegal polymorphic or qualified type:"), ppr ty]
1183 unliftedArgErr ty = sep [ptext (sLit "Illegal unlifted type:"), ppr ty]
1184 ubxArgTyErr ty = sep [ptext (sLit "Illegal unboxed tuple type as function argument:"), ppr ty]
1185 kindErr kind = sep [ptext (sLit "Expecting an ordinary type, but found a type of kind"), ppr kind]
1188 Note [Liberal type synonyms]
1189 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1190 If -XLiberalTypeSynonyms is on, expand closed type synonyms *before*
1191 doing validity checking. This allows us to instantiate a synonym defn
1192 with a for-all type, or with a partially-applied type synonym.
1196 Here, T is partially applied, so it's illegal in H98. But if you
1197 expand S first, then T we get just
1201 IMPORTANT: suppose T is a type synonym. Then we must do validity
1202 checking on an appliation (T ty1 ty2)
1204 *either* before expansion (i.e. check ty1, ty2)
1205 *or* after expansion (i.e. expand T ty1 ty2, and then check)
1208 If we do both, we get exponential behaviour!!
1210 data TIACons1 i r c = c i ::: r c
1211 type TIACons2 t x = TIACons1 t (TIACons1 t x)
1212 type TIACons3 t x = TIACons2 t (TIACons1 t x)
1213 type TIACons4 t x = TIACons2 t (TIACons2 t x)
1214 type TIACons7 t x = TIACons4 t (TIACons3 t x)
1217 %************************************************************************
1219 \subsection{Checking a theta or source type}
1221 %************************************************************************
1224 -- Enumerate the contexts in which a "source type", <S>, can occur
1228 -- or (N a) where N is a newtype
1231 = ClassSCCtxt Name -- Superclasses of clas
1232 -- class <S> => C a where ...
1233 | SigmaCtxt -- Theta part of a normal for-all type
1234 -- f :: <S> => a -> a
1235 | DataTyCtxt Name -- Theta part of a data decl
1236 -- data <S> => T a = MkT a
1237 | TypeCtxt -- Source type in an ordinary type
1239 | InstThetaCtxt -- Context of an instance decl
1240 -- instance <S> => C [a] where ...
1242 pprSourceTyCtxt (ClassSCCtxt c) = ptext (sLit "the super-classes of class") <+> quotes (ppr c)
1243 pprSourceTyCtxt SigmaCtxt = ptext (sLit "the context of a polymorphic type")
1244 pprSourceTyCtxt (DataTyCtxt tc) = ptext (sLit "the context of the data type declaration for") <+> quotes (ppr tc)
1245 pprSourceTyCtxt InstThetaCtxt = ptext (sLit "the context of an instance declaration")
1246 pprSourceTyCtxt TypeCtxt = ptext (sLit "the context of a type")
1250 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
1251 checkValidTheta ctxt theta
1252 = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
1254 -------------------------
1255 check_valid_theta ctxt []
1257 check_valid_theta ctxt theta = do
1259 warnTc (notNull dups) (dupPredWarn dups)
1260 mapM_ (check_pred_ty dflags ctxt) theta
1262 (_,dups) = removeDups tcCmpPred theta
1264 -------------------------
1265 check_pred_ty :: DynFlags -> SourceTyCtxt -> PredType -> TcM ()
1266 check_pred_ty dflags ctxt pred@(ClassP cls tys)
1267 = do { -- Class predicates are valid in all contexts
1268 ; checkTc (arity == n_tys) arity_err
1270 -- Check the form of the argument types
1271 ; mapM_ check_mono_type tys
1272 ; checkTc (check_class_pred_tys dflags ctxt tys)
1273 (predTyVarErr pred $$ how_to_allow)
1276 class_name = className cls
1277 arity = classArity cls
1279 arity_err = arityErr "Class" class_name arity n_tys
1280 how_to_allow = parens (ptext (sLit "Use -XFlexibleContexts to permit this"))
1282 check_pred_ty dflags ctxt pred@(EqPred ty1 ty2)
1283 = do { -- Equational constraints are valid in all contexts if type
1284 -- families are permitted
1285 ; checkTc (dopt Opt_TypeFamilies dflags) (eqPredTyErr pred)
1287 -- Check the form of the argument types
1288 ; check_mono_type ty1
1289 ; check_mono_type ty2
1292 check_pred_ty dflags SigmaCtxt (IParam _ ty) = check_mono_type ty
1293 -- Implicit parameters only allowed in type
1294 -- signatures; not in instance decls, superclasses etc
1295 -- The reason for not allowing implicit params in instances is a bit
1297 -- If we allowed instance (?x::Int, Eq a) => Foo [a] where ...
1298 -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
1299 -- discharge all the potential usas of the ?x in e. For example, a
1300 -- constraint Foo [Int] might come out of e,and applying the
1301 -- instance decl would show up two uses of ?x.
1304 check_pred_ty dflags ctxt sty = failWithTc (badPredTyErr sty)
1306 -------------------------
1307 check_class_pred_tys :: DynFlags -> SourceTyCtxt -> [Type] -> Bool
1308 check_class_pred_tys dflags ctxt tys
1310 TypeCtxt -> True -- {-# SPECIALISE instance Eq (T Int) #-} is fine
1311 InstThetaCtxt -> flexible_contexts || undecidable_ok || all tcIsTyVarTy tys
1312 -- Further checks on head and theta in
1313 -- checkInstTermination
1314 other -> flexible_contexts || all tyvar_head tys
1316 flexible_contexts = dopt Opt_FlexibleContexts dflags
1317 undecidable_ok = dopt Opt_UndecidableInstances dflags
1319 -------------------------
1320 tyvar_head ty -- Haskell 98 allows predicates of form
1321 | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
1322 | otherwise -- where a is a type variable
1323 = case tcSplitAppTy_maybe ty of
1324 Just (ty, _) -> tyvar_head ty
1331 is ambiguous if P contains generic variables
1332 (i.e. one of the Vs) that are not mentioned in tau
1334 However, we need to take account of functional dependencies
1335 when we speak of 'mentioned in tau'. Example:
1336 class C a b | a -> b where ...
1338 forall x y. (C x y) => x
1339 is not ambiguous because x is mentioned and x determines y
1341 NB; the ambiguity check is only used for *user* types, not for types
1342 coming from inteface files. The latter can legitimately have
1343 ambiguous types. Example
1345 class S a where s :: a -> (Int,Int)
1346 instance S Char where s _ = (1,1)
1347 f:: S a => [a] -> Int -> (Int,Int)
1348 f (_::[a]) x = (a*x,b)
1349 where (a,b) = s (undefined::a)
1351 Here the worker for f gets the type
1352 fw :: forall a. S a => Int -> (# Int, Int #)
1354 If the list of tv_names is empty, we have a monotype, and then we
1355 don't need to check for ambiguity either, because the test can't fail
1360 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
1361 checkAmbiguity forall_tyvars theta tau_tyvars
1362 = mapM_ complain (filter is_ambig theta)
1364 complain pred = addErrTc (ambigErr pred)
1365 extended_tau_vars = grow theta tau_tyvars
1367 -- See Note [Implicit parameters and ambiguity] in TcSimplify
1368 is_ambig pred = isClassPred pred &&
1369 any ambig_var (varSetElems (tyVarsOfPred pred))
1371 ambig_var ct_var = (ct_var `elem` forall_tyvars) &&
1372 not (ct_var `elemVarSet` extended_tau_vars)
1375 = sep [ptext (sLit "Ambiguous constraint") <+> quotes (pprPred pred),
1376 nest 4 (ptext (sLit "At least one of the forall'd type variables mentioned by the constraint") $$
1377 ptext (sLit "must be reachable from the type after the '=>'"))]
1380 In addition, GHC insists that at least one type variable
1381 in each constraint is in V. So we disallow a type like
1382 forall a. Eq b => b -> b
1383 even in a scope where b is in scope.
1386 checkFreeness forall_tyvars theta
1387 = do { flexible_contexts <- doptM Opt_FlexibleContexts
1388 ; unless flexible_contexts $ mapM_ complain (filter is_free theta) }
1390 is_free pred = not (isIPPred pred)
1391 && not (any bound_var (varSetElems (tyVarsOfPred pred)))
1392 bound_var ct_var = ct_var `elem` forall_tyvars
1393 complain pred = addErrTc (freeErr pred)
1396 = sep [ ptext (sLit "All of the type variables in the constraint") <+>
1397 quotes (pprPred pred)
1398 , ptext (sLit "are already in scope") <+>
1399 ptext (sLit "(at least one must be universally quantified here)")
1401 ptext (sLit "(Use -XFlexibleContexts to lift this restriction)")
1406 checkThetaCtxt ctxt theta
1407 = vcat [ptext (sLit "In the context:") <+> pprTheta theta,
1408 ptext (sLit "While checking") <+> pprSourceTyCtxt ctxt ]
1410 badPredTyErr sty = ptext (sLit "Illegal constraint") <+> pprPred sty
1411 eqPredTyErr sty = ptext (sLit "Illegal equational constraint") <+> pprPred sty
1413 parens (ptext (sLit "Use -XTypeFamilies to permit this"))
1414 predTyVarErr pred = sep [ptext (sLit "Non type-variable argument"),
1415 nest 2 (ptext (sLit "in the constraint:") <+> pprPred pred)]
1416 dupPredWarn dups = ptext (sLit "Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
1418 arityErr kind name n m
1419 = hsep [ text kind, quotes (ppr name), ptext (sLit "should have"),
1420 n_arguments <> comma, text "but has been given", int m]
1422 n_arguments | n == 0 = ptext (sLit "no arguments")
1423 | n == 1 = ptext (sLit "1 argument")
1424 | True = hsep [int n, ptext (sLit "arguments")]
1428 = do { ty' <- zonkTcType ty
1429 ; env0 <- tcInitTidyEnv
1430 ; let (env1, tidy_ty) = tidyOpenType env0 ty'
1431 msg = ptext (sLit "Cannot match a monotype with") <+> quotes (ppr tidy_ty)
1432 ; failWithTcM (env1, msg) }
1435 = do { ty' <- zonkTcType ty
1436 ; env0 <- tcInitTidyEnv
1437 ; let (env1, tidy_ty) = tidyOpenType env0 ty'
1438 msg = ptext (sLit "Arguments of type synonym families must be monotypes") <+> quotes (ppr tidy_ty)
1439 ; failWithTcM (env1, msg) }
1443 %************************************************************************
1445 \subsection{Checking for a decent instance head type}
1447 %************************************************************************
1449 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1450 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1452 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1453 flag is on, or (2)~the instance is imported (they must have been
1454 compiled elsewhere). In these cases, we let them go through anyway.
1456 We can also have instances for functions: @instance Foo (a -> b) ...@.
1459 checkValidInstHead :: Type -> TcM (Class, [TcType])
1461 checkValidInstHead ty -- Should be a source type
1462 = case tcSplitPredTy_maybe ty of {
1463 Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
1466 case getClassPredTys_maybe pred of {
1467 Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
1468 Just (clas,tys) -> do
1471 mapM_ check_mono_type tys
1472 check_inst_head dflags clas tys
1476 check_inst_head dflags clas tys
1477 -- If GlasgowExts then check at least one isn't a type variable
1478 = do checkTc (dopt Opt_TypeSynonymInstances dflags ||
1479 all tcInstHeadTyNotSynonym tys)
1480 (instTypeErr (pprClassPred clas tys) head_type_synonym_msg)
1481 checkTc (dopt Opt_FlexibleInstances dflags ||
1482 all tcInstHeadTyAppAllTyVars tys)
1483 (instTypeErr (pprClassPred clas tys) head_type_args_tyvars_msg)
1484 checkTc (dopt Opt_MultiParamTypeClasses dflags ||
1486 (instTypeErr (pprClassPred clas tys) head_one_type_msg)
1487 mapM_ check_mono_type tys
1488 -- For now, I only allow tau-types (not polytypes) in
1489 -- the head of an instance decl.
1490 -- E.g. instance C (forall a. a->a) is rejected
1491 -- One could imagine generalising that, but I'm not sure
1492 -- what all the consequences might be
1495 head_type_synonym_msg = parens (
1496 text "All instance types must be of the form (T t1 ... tn)" $$
1497 text "where T is not a synonym." $$
1498 text "Use -XTypeSynonymInstances if you want to disable this.")
1500 head_type_args_tyvars_msg = parens (vcat [
1501 text "All instance types must be of the form (T a1 ... an)",
1502 text "where a1 ... an are type *variables*,",
1503 text "and each type variable appears at most once in the instance head.",
1504 text "Use -XFlexibleInstances if you want to disable this."])
1506 head_one_type_msg = parens (
1507 text "Only one type can be given in an instance head." $$
1508 text "Use -XMultiParamTypeClasses if you want to allow more.")
1510 instTypeErr pp_ty msg
1511 = sep [ptext (sLit "Illegal instance declaration for") <+> quotes pp_ty,
1516 %************************************************************************
1518 \subsection{Checking instance for termination}
1520 %************************************************************************
1524 checkValidInstance :: [TyVar] -> ThetaType -> Class -> [TcType] -> TcM ()
1525 checkValidInstance tyvars theta clas inst_tys
1526 = do { undecidable_ok <- doptM Opt_UndecidableInstances
1528 ; checkValidTheta InstThetaCtxt theta
1529 ; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys)
1531 -- Check that instance inference will terminate (if we care)
1532 -- For Haskell 98 this will already have been done by checkValidTheta,
1533 -- but as we may be using other extensions we need to check.
1534 ; unless undecidable_ok $
1535 mapM_ addErrTc (checkInstTermination inst_tys theta)
1537 -- The Coverage Condition
1538 ; checkTc (undecidable_ok || checkInstCoverage clas inst_tys)
1539 (instTypeErr (pprClassPred clas inst_tys) msg)
1542 msg = parens (vcat [ptext (sLit "the Coverage Condition fails for one of the functional dependencies;"),
1546 Termination test: the so-called "Paterson conditions" (see Section 5 of
1547 "Understanding functionsl dependencies via Constraint Handling Rules,
1550 We check that each assertion in the context satisfies:
1551 (1) no variable has more occurrences in the assertion than in the head, and
1552 (2) the assertion has fewer constructors and variables (taken together
1553 and counting repetitions) than the head.
1554 This is only needed with -fglasgow-exts, as Haskell 98 restrictions
1555 (which have already been checked) guarantee termination.
1557 The underlying idea is that
1559 for any ground substitution, each assertion in the
1560 context has fewer type constructors than the head.
1564 checkInstTermination :: [TcType] -> ThetaType -> [Message]
1565 checkInstTermination tys theta
1566 = mapCatMaybes check theta
1569 size = sizeTypes tys
1571 | not (null (fvPred pred \\ fvs))
1572 = Just (predUndecErr pred nomoreMsg $$ parens undecidableMsg)
1573 | sizePred pred >= size
1574 = Just (predUndecErr pred smallerMsg $$ parens undecidableMsg)
1578 predUndecErr pred msg = sep [msg,
1579 nest 2 (ptext (sLit "in the constraint:") <+> pprPred pred)]
1581 nomoreMsg = ptext (sLit "Variable occurs more often in a constraint than in the instance head")
1582 smallerMsg = ptext (sLit "Constraint is no smaller than the instance head")
1583 undecidableMsg = ptext (sLit "Use -fallow-undecidable-instances to permit this")
1587 %************************************************************************
1589 Checking the context of a derived instance declaration
1591 %************************************************************************
1593 Note [Exotic derived instance contexts]
1594 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1595 In a 'derived' instance declaration, we *infer* the context. It's a
1596 bit unclear what rules we should apply for this; the Haskell report is
1597 silent. Obviously, constraints like (Eq a) are fine, but what about
1598 data T f a = MkT (f a) deriving( Eq )
1599 where we'd get an Eq (f a) constraint. That's probably fine too.
1601 One could go further: consider
1602 data T a b c = MkT (Foo a b c) deriving( Eq )
1603 instance (C Int a, Eq b, Eq c) => Eq (Foo a b c)
1605 Notice that this instance (just) satisfies the Paterson termination
1606 conditions. Then we *could* derive an instance decl like this:
1608 instance (C Int a, Eq b, Eq c) => Eq (T a b c)
1610 even though there is no instance for (C Int a), because there just
1611 *might* be an instance for, say, (C Int Bool) at a site where we
1612 need the equality instance for T's.
1614 However, this seems pretty exotic, and it's quite tricky to allow
1615 this, and yet give sensible error messages in the (much more common)
1616 case where we really want that instance decl for C.
1618 So for now we simply require that the derived instance context
1619 should have only type-variable constraints.
1621 Here is another example:
1622 data Fix f = In (f (Fix f)) deriving( Eq )
1623 Here, if we are prepared to allow -fallow-undecidable-instances we
1624 could derive the instance
1625 instance Eq (f (Fix f)) => Eq (Fix f)
1626 but this is so delicate that I don't think it should happen inside
1627 'deriving'. If you want this, write it yourself!
1629 NB: if you want to lift this condition, make sure you still meet the
1630 termination conditions! If not, the deriving mechanism generates
1631 larger and larger constraints. Example:
1633 data Seq a = Cons a (Seq (Succ a)) | Nil deriving Show
1635 Note the lack of a Show instance for Succ. First we'll generate
1636 instance (Show (Succ a), Show a) => Show (Seq a)
1638 instance (Show (Succ (Succ a)), Show (Succ a), Show a) => Show (Seq a)
1639 and so on. Instead we want to complain of no instance for (Show (Succ a)).
1643 Allow constraints which consist only of type variables, with no repeats.
1646 validDerivPred :: PredType -> Bool
1647 validDerivPred (ClassP cls tys) = hasNoDups fvs && sizeTypes tys == length fvs
1648 where fvs = fvTypes tys
1649 validDerivPred otehr = False
1652 %************************************************************************
1654 Checking type instance well-formedness and termination
1656 %************************************************************************
1659 -- Check that a "type instance" is well-formed (which includes decidability
1660 -- unless -fallow-undecidable-instances is given).
1662 checkValidTypeInst :: [Type] -> Type -> TcM ()
1663 checkValidTypeInst typats rhs
1664 = do { -- left-hand side contains no type family applications
1665 -- (vanilla synonyms are fine, though)
1666 ; mapM_ checkTyFamFreeness typats
1668 -- the right-hand side is a tau type
1669 ; checkTc (isTauTy rhs) $
1672 -- we have a decidable instance unless otherwise permitted
1673 ; undecidable_ok <- doptM Opt_UndecidableInstances
1674 ; unless undecidable_ok $
1675 mapM_ addErrTc (checkFamInst typats (tyFamInsts rhs))
1678 -- Make sure that each type family instance is
1679 -- (1) strictly smaller than the lhs,
1680 -- (2) mentions no type variable more often than the lhs, and
1681 -- (3) does not contain any further type family instances.
1683 checkFamInst :: [Type] -- lhs
1684 -> [(TyCon, [Type])] -- type family instances
1686 checkFamInst lhsTys famInsts
1687 = mapCatMaybes check famInsts
1689 size = sizeTypes lhsTys
1690 fvs = fvTypes lhsTys
1692 | not (all isTyFamFree tys)
1693 = Just (famInstUndecErr famInst nestedMsg $$ parens undecidableMsg)
1694 | not (null (fvTypes tys \\ fvs))
1695 = Just (famInstUndecErr famInst nomoreVarMsg $$ parens undecidableMsg)
1696 | size <= sizeTypes tys
1697 = Just (famInstUndecErr famInst smallerAppMsg $$ parens undecidableMsg)
1701 famInst = TyConApp tc tys
1703 -- Ensure that no type family instances occur in a type.
1705 checkTyFamFreeness :: Type -> TcM ()
1706 checkTyFamFreeness ty
1707 = checkTc (isTyFamFree ty) $
1708 tyFamInstInIndexErr ty
1710 -- Check that a type does not contain any type family applications.
1712 isTyFamFree :: Type -> Bool
1713 isTyFamFree = null . tyFamInsts
1717 tyFamInstInIndexErr ty
1718 = hang (ptext (sLit "Illegal type family application in type instance") <>
1723 = hang (ptext (sLit "Illegal polymorphic type in type instance") <> colon) 4 $
1726 famInstUndecErr ty msg
1728 nest 2 (ptext (sLit "in the type family application:") <+>
1731 nestedMsg = ptext (sLit "Nested type family application")
1732 nomoreVarMsg = ptext (sLit "Variable occurs more often than in instance head")
1733 smallerAppMsg = ptext (sLit "Application is no smaller than the instance head")
1737 %************************************************************************
1739 \subsection{Auxiliary functions}
1741 %************************************************************************
1744 -- Free variables of a type, retaining repetitions, and expanding synonyms
1745 fvType :: Type -> [TyVar]
1746 fvType ty | Just exp_ty <- tcView ty = fvType exp_ty
1747 fvType (TyVarTy tv) = [tv]
1748 fvType (TyConApp _ tys) = fvTypes tys
1749 fvType (PredTy pred) = fvPred pred
1750 fvType (FunTy arg res) = fvType arg ++ fvType res
1751 fvType (AppTy fun arg) = fvType fun ++ fvType arg
1752 fvType (ForAllTy tyvar ty) = filter (/= tyvar) (fvType ty)
1754 fvTypes :: [Type] -> [TyVar]
1755 fvTypes tys = concat (map fvType tys)
1757 fvPred :: PredType -> [TyVar]
1758 fvPred (ClassP _ tys') = fvTypes tys'
1759 fvPred (IParam _ ty) = fvType ty
1760 fvPred (EqPred ty1 ty2) = fvType ty1 ++ fvType ty2
1762 -- Size of a type: the number of variables and constructors
1763 sizeType :: Type -> Int
1764 sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty
1765 sizeType (TyVarTy _) = 1
1766 sizeType (TyConApp _ tys) = sizeTypes tys + 1
1767 sizeType (PredTy pred) = sizePred pred
1768 sizeType (FunTy arg res) = sizeType arg + sizeType res + 1
1769 sizeType (AppTy fun arg) = sizeType fun + sizeType arg
1770 sizeType (ForAllTy _ ty) = sizeType ty
1772 sizeTypes :: [Type] -> Int
1773 sizeTypes xs = sum (map sizeType xs)
1775 sizePred :: PredType -> Int
1776 sizePred (ClassP _ tys') = sizeTypes tys'
1777 sizePred (IParam _ ty) = sizeType ty
1778 sizePred (EqPred ty1 ty2) = sizeType ty1 + sizeType ty2