Merge branch 'master' of http://darcs.haskell.org/ghc into ghc-new-flavor
[ghc.git] / compiler / typecheck / TcMType.lhs
1 %
2 % (c) The University of Glasgow 2006
3 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 %
5
6 Monadic type operations
7
8 This module contains monadic operations over types that contain
9 mutable type variables
10
11 \begin{code}
12 {-# OPTIONS -fno-warn-tabs #-}
13 -- The above warning supression flag is a temporary kludge.
14 -- While working on this module you are encouraged to remove it and
15 -- detab the module (please do the detabbing in a separate patch). See
16 --     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces
17 -- for details
18
19 module TcMType (
20   TcTyVar, TcKind, TcType, TcTauType, TcThetaType, TcTyVarSet,
21
22   --------------------------------
23   -- Creating new mutable type variables
24   newFlexiTyVar,
25   newFlexiTyVarTy,              -- Kind -> TcM TcType
26   newFlexiTyVarTys,             -- Int -> Kind -> TcM [TcType]
27   newMetaKindVar, newMetaKindVars, mkKindSigVar,
28   mkTcTyVarName,
29
30   newMetaTyVar, readMetaTyVar, writeMetaTyVar, writeMetaTyVarRef,
31   isFilledMetaTyVar, isFlexiMetaTyVar,
32
33   --------------------------------
34   -- Creating new evidence variables
35   newEvVar, newEvVars,
36   newEq, newIP, newDict,
37
38   newWantedEvVar, newWantedEvVars,
39   newTcEvBinds, addTcEvBind,
40
41   --------------------------------
42   -- Instantiation
43   tcInstTyVars, tcInstSigTyVars,
44   tcInstType, 
45   tcInstSkolTyVars, tcInstSuperSkolTyVars,
46   tcInstSkolTyVarsX, tcInstSuperSkolTyVarsX,
47   tcInstSkolTyVar, tcInstSkolType,
48   tcSkolDFunType, tcSuperSkolTyVars,
49
50   --------------------------------
51   -- Checking type validity
52   Rank, UserTypeCtxt(..), checkValidType, checkValidMonoType,
53   expectedKindInCtxt, 
54   checkValidTheta, 
55   checkValidInstHead, checkValidInstance, validDerivPred,
56   checkInstTermination, checkValidFamInst, checkTyFamFreeness, 
57   arityErr, 
58   growPredTyVars, growThetaTyVars, 
59
60   --------------------------------
61   -- Zonking
62   zonkType, zonkKind, zonkTcPredType, 
63   skolemiseSigTv, skolemiseUnboundMetaTyVar,
64   zonkTcTyVar, zonkTcTyVars, zonkTyVarsAndFV, zonkSigTyVar,
65   zonkQuantifiedTyVar, zonkQuantifiedTyVars,
66   zonkTcType, zonkTcTypes, zonkTcThetaType,
67
68   zonkTcKind, defaultKindVarToStar, zonkCt, zonkCts,
69   zonkImplication, zonkEvVar, zonkWC, 
70
71   zonkTcTypeAndSubst,
72   tcGetGlobalTyVars, 
73   ) where
74
75 #include "HsVersions.h"
76
77 -- friends:
78 import TypeRep
79 import TcType
80 import Type
81 import Kind
82 import Class
83 import TyCon
84 import Var
85
86 -- others:
87 import HsSyn            -- HsType
88 import TcRnMonad        -- TcType, amongst others
89 import IParam
90 import Id
91 import FunDeps
92 import Name
93 import VarSet
94 import ErrUtils
95 import DynFlags
96 import Util
97 import Maybes
98 import ListSetOps
99 import BasicTypes
100 import SrcLoc
101 import Outputable
102 import FastString
103 import Unique( Unique )
104 import Bag
105
106 import Control.Monad
107 import Data.List        ( (\\), partition, mapAccumL )
108 \end{code}
109
110
111 %************************************************************************
112 %*                                                                      *
113         Kind variables
114 %*                                                                      *
115 %************************************************************************
116
117 \begin{code}
118 newMetaKindVar :: TcM TcKind
119 newMetaKindVar = do { uniq <- newUnique
120                     ; ref <- newMutVar Flexi
121                     ; return (mkTyVarTy (mkMetaKindVar uniq ref)) }
122
123 newMetaKindVars :: Int -> TcM [TcKind]
124 newMetaKindVars n = mapM (\ _ -> newMetaKindVar) (nOfThem n ())
125
126 mkKindSigVar :: Name -> KindVar
127 -- Use the specified name; don't clone it
128 mkKindSigVar n = mkTcTyVar n superKind (SkolemTv False)
129 \end{code}
130
131
132 %************************************************************************
133 %*                                                                      *
134      Evidence variables; range over constraints we can abstract over
135 %*                                                                      *
136 %************************************************************************
137
138 \begin{code}
139 newEvVars :: TcThetaType -> TcM [EvVar]
140 newEvVars theta = mapM newEvVar theta
141
142 newWantedEvVar :: TcPredType -> TcM EvVar 
143 newWantedEvVar = newEvVar
144
145 newWantedEvVars :: TcThetaType -> TcM [EvVar] 
146 newWantedEvVars theta = mapM newWantedEvVar theta 
147
148 --------------
149
150 newEvVar :: TcPredType -> TcM EvVar
151 -- Creates new *rigid* variables for predicates
152 newEvVar ty = do { name <- newName (predTypeOccName ty) 
153                  ; return (mkLocalId name ty) }
154
155 newEq :: TcType -> TcType -> TcM EvVar
156 newEq ty1 ty2
157   = do { name <- newName (mkVarOccFS (fsLit "cobox"))
158        ; return (mkLocalId name (mkTcEqPred ty1 ty2)) }
159
160 newIP :: IPName Name -> TcType -> TcM IpId
161 newIP ip ty
162   = do  { name <- newName (mkVarOccFS (ipFastString ip))
163         ; return (mkLocalId name (mkIPPred ip ty)) }
164
165 newDict :: Class -> [TcType] -> TcM DictId
166 newDict cls tys 
167   = do { name <- newName (mkDictOcc (getOccName cls))
168        ; return (mkLocalId name (mkClassPred cls tys)) }
169
170 predTypeOccName :: PredType -> OccName
171 predTypeOccName ty = case classifyPredType ty of
172     ClassPred cls _ -> mkDictOcc (getOccName cls)
173     IPPred ip _     -> mkVarOccFS (ipFastString ip)
174     EqPred _ _      -> mkVarOccFS (fsLit "cobox")
175     TuplePred _     -> mkVarOccFS (fsLit "tup")
176     IrredPred _     -> mkVarOccFS (fsLit "irred")
177 \end{code}
178
179
180 %************************************************************************
181 %*                                                                      *
182         SkolemTvs (immutable)
183 %*                                                                      *
184 %************************************************************************
185
186 \begin{code}
187 tcInstType :: ([TyVar] -> TcM (TvSubst, [TcTyVar]))     -- How to instantiate the type variables
188            -> TcType                                    -- Type to instantiate
189            -> TcM ([TcTyVar], TcThetaType, TcType)      -- Result
190                 -- (type vars (excl coercion vars), preds (incl equalities), rho)
191 tcInstType inst_tyvars ty
192   = case tcSplitForAllTys ty of
193         ([],     rho) -> let    -- There may be overloading despite no type variables;
194                                 --      (?x :: Int) => Int -> Int
195                            (theta, tau) = tcSplitPhiTy rho
196                          in
197                          return ([], theta, tau)
198
199         (tyvars, rho) -> do { (subst, tyvars') <- inst_tyvars tyvars
200                             ; let (theta, tau) = tcSplitPhiTy (substTy subst rho)
201                             ; return (tyvars', theta, tau) }
202
203 tcSkolDFunType :: Type -> TcM ([TcTyVar], TcThetaType, TcType)
204 -- Instantiate a type signature with skolem constants, but 
205 -- do *not* give them fresh names, because we want the name to
206 -- be in the type environment: it is lexically scoped.
207 tcSkolDFunType ty = tcInstType (\tvs -> return (tcSuperSkolTyVars tvs)) ty
208
209 tcSuperSkolTyVars :: [TyVar] -> (TvSubst, [TcTyVar])
210 -- Make skolem constants, but do *not* give them new names, as above
211 -- Moreover, make them "super skolems"; see comments with superSkolemTv
212 -- see Note [Kind substitution when instantiating]
213 -- Precondition: tyvars should be ordered (kind vars first)
214 tcSuperSkolTyVars = mapAccumL tcSuperSkolTyVar (mkTopTvSubst [])
215
216 tcSuperSkolTyVar :: TvSubst -> TyVar -> (TvSubst, TcTyVar)
217 tcSuperSkolTyVar subst tv
218   = (extendTvSubst subst tv (mkTyVarTy new_tv), new_tv)
219   where
220     kind   = substTy subst (tyVarKind tv)
221     new_tv = mkTcTyVar (tyVarName tv) kind superSkolemTv
222
223 tcInstSkolTyVar :: Bool -> TvSubst -> TyVar -> TcM (TvSubst, TcTyVar)
224 -- Instantiate the tyvar, using 
225 --      * the occ-name and kind of the supplied tyvar, 
226 --      * the unique from the monad,
227 --      * the location either from the tyvar (skol_info = SigSkol)
228 --                     or from the monad (otherwise)
229 tcInstSkolTyVar overlappable subst tyvar
230   = do  { uniq <- newUnique
231         ; loc  <- getSrcSpanM
232         ; let new_name = mkInternalName uniq occ loc
233               new_tv   = mkTcTyVar new_name kind (SkolemTv overlappable)
234         ; return (extendTvSubst subst tyvar (mkTyVarTy new_tv), new_tv) }
235   where
236     old_name = tyVarName tyvar
237     occ      = nameOccName old_name
238     kind     = substTy subst (tyVarKind tyvar)
239
240 -- Wrappers
241 tcInstSkolTyVars :: [TyVar] -> TcM (TvSubst, [TcTyVar])
242 tcInstSkolTyVars = tcInstSkolTyVarsX (mkTopTvSubst [])
243
244 tcInstSuperSkolTyVars :: [TyVar] -> TcM [TcTyVar]
245 tcInstSuperSkolTyVars = fmap snd . tcInstSkolTyVars' True  (mkTopTvSubst [])
246
247 tcInstSkolTyVarsX, tcInstSuperSkolTyVarsX
248   :: TvSubst -> [TyVar] -> TcM (TvSubst, [TcTyVar])
249 tcInstSkolTyVarsX      subst = tcInstSkolTyVars' False subst
250 tcInstSuperSkolTyVarsX subst = tcInstSkolTyVars' True  subst
251
252 tcInstSkolTyVars' :: Bool -> TvSubst -> [TyVar] -> TcM (TvSubst, [TcTyVar])
253 -- Precondition: tyvars should be ordered (kind vars first)
254 -- see Note [Kind substitution when instantiating]
255 tcInstSkolTyVars' isSuperSkol = mapAccumLM (tcInstSkolTyVar isSuperSkol)
256
257 tcInstSkolType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType)
258 -- Instantiate a type with fresh skolem constants
259 -- Binding location comes from the monad
260 tcInstSkolType ty = tcInstType tcInstSkolTyVars ty
261
262 tcInstSigTyVars :: [TyVar] -> TcM (TvSubst, [TcTyVar])
263 -- Make meta SigTv type variables for patten-bound scoped type varaibles
264 -- We use SigTvs for them, so that they can't unify with arbitrary types
265 -- Precondition: tyvars should be ordered (kind vars first)
266 -- see Note [Kind substitution when instantiating]
267 tcInstSigTyVars = mapAccumLM tcInstSigTyVar (mkTopTvSubst [])
268         -- The tyvars are freshly made, by tcInstSigTyVar
269         -- So mkTopTvSubst [] is ok
270
271 tcInstSigTyVar :: TvSubst -> TyVar -> TcM (TvSubst, TcTyVar)
272 tcInstSigTyVar subst tv
273   = do { uniq <- newMetaUnique
274        ; ref <- newMutVar Flexi
275        ; let name   = setNameUnique (tyVarName tv) uniq
276                       -- Use the same OccName so that the tidy-er
277                       -- doesn't rename 'a' to 'a0' etc
278              kind   = substTy subst (tyVarKind tv)
279              new_tv = mkTcTyVar name kind (MetaTv SigTv ref)
280        ; return (extendTvSubst subst tv (mkTyVarTy new_tv), new_tv) }
281 \end{code}
282
283 Note [Kind substitution when instantiating]
284 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
285 When we instantiate a bunch of kind and type variables, first we
286 expect them to be sorted (kind variables first, then type variables).
287 Then we have to instantiate the kind variables, build a substitution
288 from old variables to the new variables, then instantiate the type
289 variables substituting the original kind.
290
291 Exemple: If we want to instantiate
292   [(k1 :: BOX), (k2 :: BOX), (a :: k1 -> k2), (b :: k1)]
293 we want
294   [(?k1 :: BOX), (?k2 :: BOX), (?a :: ?k1 -> ?k2), (?b :: ?k1)]
295 instead of the buggous
296   [(?k1 :: BOX), (?k2 :: BOX), (?a :: k1 -> k2), (?b :: k1)]
297
298
299 %************************************************************************
300 %*                                                                      *
301         MetaTvs (meta type variables; mutable)
302 %*                                                                      *
303 %************************************************************************
304
305 \begin{code}
306 newMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar
307 -- Make a new meta tyvar out of thin air
308 newMetaTyVar meta_info kind
309   = do  { uniq <- newMetaUnique
310         ; ref <- newMutVar Flexi
311         ; let name = mkTcTyVarName uniq s
312               s = case meta_info of
313                         TauTv -> fsLit "t"
314                         TcsTv -> fsLit "u"
315                         SigTv -> fsLit "a"
316         ; return (mkTcTyVar name kind (MetaTv meta_info ref)) }
317
318 mkTcTyVarName :: Unique -> FastString -> Name
319 -- Make sure that fresh TcTyVar names finish with a digit
320 -- leaving the un-cluttered names free for user names
321 mkTcTyVarName uniq str = mkSysTvName uniq str
322
323 -- Works for both type and kind variables
324 readMetaTyVar :: TyVar -> TcM MetaDetails
325 readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
326                       readMutVar (metaTvRef tyvar)
327
328 isFilledMetaTyVar :: TyVar -> TcM Bool
329 -- True of a filled-in (Indirect) meta type variable
330 isFilledMetaTyVar tv
331   | not (isTcTyVar tv) = return False
332   | MetaTv _ ref <- tcTyVarDetails tv
333   = do  { details <- readMutVar ref
334         ; return (isIndirect details) }
335   | otherwise = return False
336
337 isFlexiMetaTyVar :: TyVar -> TcM Bool
338 -- True of a un-filled-in (Flexi) meta type variable
339 isFlexiMetaTyVar tv
340   | not (isTcTyVar tv) = return False
341   | MetaTv _ ref <- tcTyVarDetails tv
342   = do  { details <- readMutVar ref
343         ; return (isFlexi details) }
344   | otherwise = return False
345
346 --------------------
347 -- Works with both type and kind variables
348 writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
349 -- Write into a currently-empty MetaTyVar
350
351 writeMetaTyVar tyvar ty
352   | not debugIsOn 
353   = writeMetaTyVarRef tyvar (metaTvRef tyvar) ty
354
355 -- Everything from here on only happens if DEBUG is on
356   | not (isTcTyVar tyvar)
357   = WARN( True, text "Writing to non-tc tyvar" <+> ppr tyvar )
358     return ()
359
360   | MetaTv _ ref <- tcTyVarDetails tyvar
361   = writeMetaTyVarRef tyvar ref ty
362
363   | otherwise
364   = WARN( True, text "Writing to non-meta tyvar" <+> ppr tyvar )
365     return ()
366
367 --------------------
368 writeMetaTyVarRef :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM ()
369 -- Here the tyvar is for error checking only; 
370 -- the ref cell must be for the same tyvar
371 writeMetaTyVarRef tyvar ref ty
372   | not debugIsOn 
373   = do { traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
374        ; writeMutVar ref (Indirect ty) }
375
376 -- Everything from here on only happens if DEBUG is on
377   | otherwise
378   = do { meta_details <- readMutVar ref; 
379        -- Zonk kinds to allow the error check to work
380        ; zonked_tv_kind <- zonkTcKind tv_kind 
381        ; zonked_ty_kind <- zonkTcKind ty_kind
382
383        -- Check for double updates
384        ; ASSERT2( isFlexi meta_details, 
385                   hang (text "Double update of meta tyvar")
386                    2 (ppr tyvar $$ ppr meta_details) )
387
388          traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
389        ; writeMutVar ref (Indirect ty) 
390        ; when (   not (isPredTy tv_kind) 
391                     -- Don't check kinds for updates to coercion variables
392                && not (zonked_ty_kind `tcIsSubKind` zonked_tv_kind))
393        $ WARN( True, hang (text "Ill-kinded update to meta tyvar")
394                         2 (    ppr tyvar <+> text "::" <+> ppr tv_kind 
395                            <+> text ":=" 
396                            <+> ppr ty    <+> text "::" <+> ppr ty_kind) )
397          (return ()) }
398   where
399     tv_kind = tyVarKind tyvar
400     ty_kind = typeKind ty
401 \end{code}
402
403
404 %************************************************************************
405 %*                                                                      *
406         MetaTvs: TauTvs
407 %*                                                                      *
408 %************************************************************************
409
410 \begin{code}
411 newFlexiTyVar :: Kind -> TcM TcTyVar
412 newFlexiTyVar kind = newMetaTyVar TauTv kind
413
414 newFlexiTyVarTy  :: Kind -> TcM TcType
415 newFlexiTyVarTy kind = do
416     tc_tyvar <- newFlexiTyVar kind
417     return (TyVarTy tc_tyvar)
418
419 newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
420 newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind)
421
422 tcInstTyVars :: [TKVar] -> TcM ([TcTyVar], [TcType], TvSubst)
423 -- Instantiate with META type variables
424 -- Note that this works for a sequence of kind and type
425 -- variables.  Eg    [ (k:BOX), (a:k->k) ]
426 --             Gives [ (k7:BOX), (a8:k7->k7) ]
427 tcInstTyVars tyvars = tcInstTyVarsX emptyTvSubst tyvars
428     -- emptyTvSubst has an empty in-scope set, but that's fine here
429     -- Since the tyvars are freshly made, they cannot possibly be
430     -- captured by any existing for-alls.
431
432 tcInstTyVarsX :: TvSubst -> [TKVar] -> TcM ([TcTyVar], [TcType], TvSubst)
433 -- The "X" part is because of extending the substitution
434 tcInstTyVarsX subst tyvars =
435   do { (subst', tyvars') <- mapAccumLM tcInstTyVarX subst tyvars
436      ; return (tyvars', mkTyVarTys tyvars', subst') }
437
438 tcInstTyVarX :: TvSubst -> TKVar -> TcM (TvSubst, TcTyVar)
439 -- Make a new unification variable tyvar whose Name and Kind come from
440 -- an existing TyVar. We substitute kind variables in the kind.
441 tcInstTyVarX subst tyvar
442   = do  { uniq <- newMetaUnique
443         ; ref <- newMutVar Flexi
444         ; let name   = mkSystemName uniq (getOccName tyvar)
445               kind   = substTy subst (tyVarKind tyvar)
446               new_tv = mkTcTyVar name kind (MetaTv TauTv ref)
447         ; return (extendTvSubst subst tyvar (mkTyVarTy new_tv), new_tv) }
448 \end{code}
449
450
451 %************************************************************************
452 %*                                                                      *
453         MetaTvs: SigTvs
454 %*                                                                      *
455 %************************************************************************
456
457 \begin{code}
458 zonkSigTyVar :: TcTyVar -> TcM TcTyVar
459 zonkSigTyVar sig_tv 
460   | isSkolemTyVar sig_tv 
461   = return sig_tv       -- Happens in the call in TcBinds.checkDistinctTyVars
462   | otherwise
463   = ASSERT( isSigTyVar sig_tv )
464     do { ty <- zonkTcTyVar sig_tv
465        ; return (tcGetTyVar "zonkSigTyVar" ty) }
466         -- 'ty' is bound to be a type variable, because SigTvs
467         -- can only be unified with type variables
468 \end{code}
469
470
471
472 %************************************************************************
473 %*                                                                      *
474 \subsection{Zonking -- the exernal interfaces}
475 %*                                                                      *
476 %************************************************************************
477
478 @tcGetGlobalTyVars@ returns a fully-zonked set of tyvars free in the environment.
479 To improve subsequent calls to the same function it writes the zonked set back into
480 the environment.
481
482 \begin{code}
483 tcGetGlobalTyVars :: TcM TcTyVarSet
484 tcGetGlobalTyVars
485   = do { (TcLclEnv {tcl_tyvars = gtv_var}) <- getLclEnv
486        ; gbl_tvs  <- readMutVar gtv_var
487        ; gbl_tvs' <- zonkTyVarsAndFV gbl_tvs
488        ; writeMutVar gtv_var gbl_tvs'
489        ; return gbl_tvs' }
490   where
491 \end{code}
492
493 -----------------  Type variables
494
495 \begin{code}
496 zonkTyVar :: TyVar -> TcM TcType
497 -- Works on TyVars and TcTyVars
498 zonkTyVar tv | isTcTyVar tv = zonkTcTyVar tv
499              | otherwise    = return (mkTyVarTy tv)
500    -- Hackily, when typechecking type and class decls
501    -- we have TyVars in scopeadded (only) in 
502    -- TcHsType.tcTyClTyVars, but it seems
503    -- painful to make them into TcTyVars there
504
505 zonkTyVarsAndFV :: TyVarSet -> TcM TyVarSet
506 zonkTyVarsAndFV tyvars = tyVarsOfTypes <$> mapM zonkTyVar (varSetElems tyvars)
507
508 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
509 zonkTcTyVars tyvars = mapM zonkTcTyVar tyvars
510
511 -----------------  Types
512 zonkTcType :: TcType -> TcM TcType
513 -- Simply look through all Flexis
514 zonkTcType ty = zonkType zonkTcTyVar ty
515
516 zonkTcTyVar :: TcTyVar -> TcM TcType
517 -- Simply look through all Flexis
518 zonkTcTyVar tv
519   = ASSERT2( isTcTyVar tv, ppr tv ) do
520     case tcTyVarDetails tv of
521       SkolemTv {}   -> zonk_kind_and_return
522       RuntimeUnk {} -> zonk_kind_and_return
523       FlatSkol ty   -> zonkTcType ty
524       MetaTv _ ref  -> do { cts <- readMutVar ref
525                           ; case cts of
526                                Flexi       -> zonk_kind_and_return
527                                Indirect ty -> zonkTcType ty }
528   where
529     zonk_kind_and_return = do { z_tv <- zonkTyVarKind tv
530                               ; return (TyVarTy z_tv) }
531
532 zonkTyVarKind :: TyVar -> TcM TyVar
533 zonkTyVarKind tv = do { kind' <- zonkTcKind (tyVarKind tv)
534                       ; return (setTyVarKind tv kind') }
535
536 zonkTcTypeAndSubst :: TvSubst -> TcType -> TcM TcType
537 -- Zonk, and simultaneously apply a non-necessarily-idempotent substitution
538 zonkTcTypeAndSubst subst ty = zonkType zonk_tv ty
539   where
540     zonk_tv tv
541       = do { z_tv <- updateTyVarKindM zonkTcKind tv
542            ; ASSERT ( isTcTyVar tv )
543              case tcTyVarDetails tv of
544                 SkolemTv {}   -> return (TyVarTy z_tv)
545                 RuntimeUnk {} -> return (TyVarTy z_tv)
546                 FlatSkol ty   -> zonkType zonk_tv ty
547                 MetaTv _ ref  -> do { cts <- readMutVar ref
548                                     ; case cts of
549                                    Flexi       -> zonk_flexi z_tv
550                                    Indirect ty -> zonkType zonk_tv ty } }
551     zonk_flexi tv
552       = case lookupTyVar subst tv of
553           Just ty -> zonkType zonk_tv ty
554           Nothing -> return (TyVarTy tv)
555
556 zonkTcTypes :: [TcType] -> TcM [TcType]
557 zonkTcTypes tys = mapM zonkTcType tys
558
559 zonkTcThetaType :: TcThetaType -> TcM TcThetaType
560 zonkTcThetaType theta = mapM zonkTcPredType theta
561
562 zonkTcPredType :: TcPredType -> TcM TcPredType
563 zonkTcPredType = zonkTcType
564 \end{code}
565
566 -------------------  These ...ToType, ...ToKind versions
567                      are used at the end of type checking
568
569 \begin{code}
570 defaultKindVarToStar :: TcTyVar -> TcM Kind
571 -- We have a meta-kind: unify it with '*'
572 defaultKindVarToStar kv 
573   = do { ASSERT ( isKindVar kv && isMetaTyVar kv )
574          writeMetaTyVar kv liftedTypeKind
575        ; return liftedTypeKind }
576
577 zonkQuantifiedTyVars :: [TcTyVar] -> TcM [TcTyVar]
578 -- A kind variable k may occur *after* a tyvar mentioning k in its kind
579 zonkQuantifiedTyVars tyvars
580   = do { let (kvs, tvs) = partition isKindVar tyvars
581        ; poly_kinds <- xoptM Opt_PolyKinds
582        ; if poly_kinds then
583              mapM zonkQuantifiedTyVar (kvs ++ tvs)
584            -- Because of the order, any kind variables
585            -- mentioned in the kinds of the type variables refer to
586            -- the now-quantified versions
587          else
588              -- In the non-PolyKinds case, default the kind variables
589              -- to *, and zonk the tyvars as usual.  Notice that this
590              -- may make zonkQuantifiedTyVars return a shorter list
591              -- than it was passed, but that's ok
592              do { let (meta_kvs, skolem_kvs) = partition isMetaTyVar kvs
593                 ; WARN ( not (null skolem_kvs), ppr skolem_kvs )
594                   mapM_ defaultKindVarToStar meta_kvs
595                 ; mapM zonkQuantifiedTyVar (skolem_kvs ++ tvs) } }
596
597 zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar
598 -- The quantified type variables often include meta type variables
599 -- we want to freeze them into ordinary type variables, and
600 -- default their kind (e.g. from OpenTypeKind to TypeKind)
601 --                      -- see notes with Kind.defaultKind
602 -- The meta tyvar is updated to point to the new skolem TyVar.  Now any 
603 -- bound occurences of the original type variable will get zonked to 
604 -- the immutable version.
605 --
606 -- We leave skolem TyVars alone; they are immutable.
607 --
608 -- This function is called on both kind and type variables,
609 -- but kind variables *only* if PolyKinds is on.
610 zonkQuantifiedTyVar tv
611   = ASSERT2( isTcTyVar tv, ppr tv ) 
612     case tcTyVarDetails tv of
613       SkolemTv {} -> do { kind <- zonkTcKind (tyVarKind tv)
614                         ; return $ setTyVarKind tv kind }
615         -- It might be a skolem type variable, 
616         -- for example from a user type signature
617
618       MetaTv _ ref ->
619           do when debugIsOn $ do
620                  -- [Sept 04] Check for non-empty.
621                  -- See note [Silly Type Synonym]
622                  cts <- readMutVar ref
623                  case cts of
624                      Flexi -> return ()
625                      Indirect ty -> WARN( True, ppr tv $$ ppr ty )
626                                     return ()
627              skolemiseUnboundMetaTyVar tv vanillaSkolemTv
628       _other -> pprPanic "zonkQuantifiedTyVar" (ppr tv) -- FlatSkol, RuntimeUnk
629
630 skolemiseUnboundMetaTyVar :: TcTyVar -> TcTyVarDetails -> TcM TyVar
631 -- We have a Meta tyvar with a ref-cell inside it
632 -- Skolemise it, including giving it a new Name, so that
633 --   we are totally out of Meta-tyvar-land
634 -- We create a skolem TyVar, not a regular TyVar
635 --   See Note [Zonking to Skolem]
636 skolemiseUnboundMetaTyVar tv details
637   = ASSERT2( isMetaTyVar tv, ppr tv ) 
638     do  { span <- getSrcSpanM    -- Get the location from "here"
639                                  -- ie where we are generalising
640         ; uniq <- newUnique      -- Remove it from TcMetaTyVar unique land
641         ; kind <- zonkTcKind (tyVarKind tv)
642         ; let final_kind = defaultKind kind
643               final_name = mkInternalName uniq (getOccName tv) span
644               final_tv   = mkTcTyVar final_name final_kind details
645
646         ; writeMetaTyVar tv (mkTyVarTy final_tv)
647         ; return final_tv }
648
649 skolemiseSigTv :: TcTyVar -> TcM TcTyVar
650 -- In TcBinds we create SigTvs for type signatures
651 -- but for singleton groups we want them to really be skolems
652 -- which do not unify with each other
653 skolemiseSigTv tv  
654   = ASSERT2( isSigTyVar tv, ppr tv )
655     do { writeMetaTyVarRef tv (metaTvRef tv) (mkTyVarTy skol_tv)
656        ; return skol_tv }
657   where
658     skol_tv = setTcTyVarDetails tv (SkolemTv False)
659 \end{code}
660
661 \begin{code}
662 zonkImplication :: Implication -> TcM Implication
663 zonkImplication implic@(Implic { ic_given = given 
664                                , ic_wanted = wanted
665                                , ic_loc = loc })
666   = do {    -- No need to zonk the skolems
667        ; given'  <- mapM zonkEvVar given
668        ; loc'    <- zonkGivenLoc loc
669        ; wanted' <- zonkWC wanted
670        ; return (implic { ic_given = given'
671                         , ic_wanted = wanted'
672                         , ic_loc = loc' }) }
673
674 zonkEvVar :: EvVar -> TcM EvVar
675 zonkEvVar var = do { ty' <- zonkTcType (varType var)
676                    ; return (setVarType var ty') }
677
678
679 zonkWC :: WantedConstraints -> TcM WantedConstraints
680 zonkWC (WC { wc_flat = flat, wc_impl = implic, wc_insol = insol })
681   = do { flat'   <- mapBagM zonkCt flat 
682        ; implic' <- mapBagM zonkImplication implic
683        ; insol'  <- mapBagM zonkCt insol
684        ; return (WC { wc_flat = flat', wc_impl = implic', wc_insol = insol' }) }
685
686 zonkCt :: Ct -> TcM Ct 
687 -- Zonking a Ct conservatively gives back a CNonCanonical
688 zonkCt ct 
689   = do { fl' <- zonkFlavor (cc_flavor ct)
690        ; return $ 
691          CNonCanonical { cc_flavor = fl'
692                        , cc_depth = cc_depth ct } }
693 zonkCts :: Cts -> TcM Cts
694 zonkCts = mapBagM zonkCt
695
696 zonkFlavor :: CtFlavor -> TcM CtFlavor
697 zonkFlavor (Given loc evar) 
698   = do { loc' <- zonkGivenLoc loc
699        ; evar' <- zonkEvVar evar
700        ; return (Given loc' evar') }
701 zonkFlavor (Solved loc evar) 
702   = do { loc' <- zonkGivenLoc loc
703        ; evar' <- zonkEvVar evar
704        ; return (Solved loc' evar') }
705 zonkFlavor (Wanted loc evar)
706   = do { evar' <- zonkEvVar evar
707        ; return (Wanted loc evar') }
708 zonkFlavor (Derived loc pty)
709   = do { pty' <- zonkTcType pty
710        ; return (Derived loc pty') }
711
712
713 zonkGivenLoc :: GivenLoc -> TcM GivenLoc
714 -- GivenLocs may have unification variables inside them!
715 zonkGivenLoc (CtLoc skol_info span ctxt)
716   = do { skol_info' <- zonkSkolemInfo skol_info
717        ; return (CtLoc skol_info' span ctxt) }
718
719 zonkSkolemInfo :: SkolemInfo -> TcM SkolemInfo
720 zonkSkolemInfo (SigSkol cx ty)  = do { ty' <- zonkTcType ty
721                                      ; return (SigSkol cx ty') }
722 zonkSkolemInfo (InferSkol ntys) = do { ntys' <- mapM do_one ntys
723                                      ; return (InferSkol ntys') }
724   where
725     do_one (n, ty) = do { ty' <- zonkTcType ty; return (n, ty') }
726 zonkSkolemInfo skol_info = return skol_info
727 \end{code}
728
729 Note [Silly Type Synonyms]
730 ~~~~~~~~~~~~~~~~~~~~~~~~~~
731 Consider this:
732         type C u a = u  -- Note 'a' unused
733
734         foo :: (forall a. C u a -> C u a) -> u
735         foo x = ...
736
737         bar :: Num u => u
738         bar = foo (\t -> t + t)
739
740 * From the (\t -> t+t) we get type  {Num d} =>  d -> d
741   where d is fresh.
742
743 * Now unify with type of foo's arg, and we get:
744         {Num (C d a)} =>  C d a -> C d a
745   where a is fresh.
746
747 * Now abstract over the 'a', but float out the Num (C d a) constraint
748   because it does not 'really' mention a.  (see exactTyVarsOfType)
749   The arg to foo becomes
750         \/\a -> \t -> t+t
751
752 * So we get a dict binding for Num (C d a), which is zonked to give
753         a = ()
754   [Note Sept 04: now that we are zonking quantified type variables
755   on construction, the 'a' will be frozen as a regular tyvar on
756   quantification, so the floated dict will still have type (C d a).
757   Which renders this whole note moot; happily!]
758
759 * Then the \/\a abstraction has a zonked 'a' in it.
760
761 All very silly.   I think its harmless to ignore the problem.  We'll end up with
762 a \/\a in the final result but all the occurrences of a will be zonked to ()
763
764 Note [Zonking to Skolem]
765 ~~~~~~~~~~~~~~~~~~~~~~~~
766 We used to zonk quantified type variables to regular TyVars.  However, this
767 leads to problems.  Consider this program from the regression test suite:
768
769   eval :: Int -> String -> String -> String
770   eval 0 root actual = evalRHS 0 root actual
771
772   evalRHS :: Int -> a
773   evalRHS 0 root actual = eval 0 root actual
774
775 It leads to the deferral of an equality (wrapped in an implication constraint)
776
777   forall a. () => ((String -> String -> String) ~ a)
778
779 which is propagated up to the toplevel (see TcSimplify.tcSimplifyInferCheck).
780 In the meantime `a' is zonked and quantified to form `evalRHS's signature.
781 This has the *side effect* of also zonking the `a' in the deferred equality
782 (which at this point is being handed around wrapped in an implication
783 constraint).
784
785 Finally, the equality (with the zonked `a') will be handed back to the
786 simplifier by TcRnDriver.tcRnSrcDecls calling TcSimplify.tcSimplifyTop.
787 If we zonk `a' with a regular type variable, we will have this regular type
788 variable now floating around in the simplifier, which in many places assumes to
789 only see proper TcTyVars.
790
791 We can avoid this problem by zonking with a skolem.  The skolem is rigid
792 (which we require for a quantified variable), but is still a TcTyVar that the
793 simplifier knows how to deal with.
794
795
796 %************************************************************************
797 %*                                                                      *
798 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
799 %*                                                                      *
800 %*              For internal use only!                                  *
801 %*                                                                      *
802 %************************************************************************
803
804 \begin{code}
805 -- For unbound, mutable tyvars, zonkType uses the function given to it
806 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
807 --      type variable and zonks the kind too
808
809 zonkKind :: (TcTyVar -> TcM Kind) -> TcKind -> TcM Kind
810 zonkKind = zonkType
811
812 zonkType :: (TcTyVar -> TcM Type)  -- What to do with TcTyVars
813          -> TcType -> TcM Type
814 zonkType zonk_tc_tyvar ty
815   = go ty
816   where
817     go (TyConApp tc tys) = do tys' <- mapM go tys
818                               return (TyConApp tc tys')
819
820     go (LitTy n)         = return (LitTy n)
821
822     go (FunTy arg res)   = do arg' <- go arg
823                               res' <- go res
824                               return (FunTy arg' res')
825
826     go (AppTy fun arg)   = do fun' <- go fun
827                               arg' <- go arg
828                               return (mkAppTy fun' arg')
829                 -- NB the mkAppTy; we might have instantiated a
830                 -- type variable to a type constructor, so we need
831                 -- to pull the TyConApp to the top.
832
833         -- The two interesting cases!
834     go (TyVarTy tyvar) | isTcTyVar tyvar = zonk_tc_tyvar tyvar
835                        | otherwise       = TyVarTy <$> updateTyVarKindM go tyvar
836                 -- Ordinary (non Tc) tyvars occur inside quantified types
837
838     go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar ) do
839                              ty' <- go ty
840                              tyvar' <- updateTyVarKindM go tyvar
841                              return (ForAllTy tyvar' ty')
842 \end{code}
843
844
845
846 %************************************************************************
847 %*                                                                      *
848                         Zonking kinds
849 %*                                                                      *
850 %************************************************************************
851
852 \begin{code}
853 zonkTcKind :: TcKind -> TcM TcKind
854 zonkTcKind k = zonkTcType k
855 \end{code}
856                         
857 %************************************************************************
858 %*                                                                      *
859 \subsection{Checking a user type}
860 %*                                                                      *
861 %************************************************************************
862
863 When dealing with a user-written type, we first translate it from an HsType
864 to a Type, performing kind checking, and then check various things that should 
865 be true about it.  We don't want to perform these checks at the same time
866 as the initial translation because (a) they are unnecessary for interface-file
867 types and (b) when checking a mutually recursive group of type and class decls,
868 we can't "look" at the tycons/classes yet.  Also, the checks are are rather
869 diverse, and used to really mess up the other code.
870
871 One thing we check for is 'rank'.  
872
873         Rank 0:         monotypes (no foralls)
874         Rank 1:         foralls at the front only, Rank 0 inside
875         Rank 2:         foralls at the front, Rank 1 on left of fn arrow,
876
877         basic ::= tyvar | T basic ... basic
878
879         r2  ::= forall tvs. cxt => r2a
880         r2a ::= r1 -> r2a | basic
881         r1  ::= forall tvs. cxt => r0
882         r0  ::= r0 -> r0 | basic
883         
884 Another thing is to check that type synonyms are saturated. 
885 This might not necessarily show up in kind checking.
886         type A i = i
887         data T k = MkT (k Int)
888         f :: T A        -- BAD!
889
890         
891 \begin{code}
892 -- Depending on the context, we might accept any kind (for instance, in a TH
893 -- splice), or only certain kinds (like in type signatures).
894 expectedKindInCtxt :: UserTypeCtxt -> Maybe Kind
895 expectedKindInCtxt (TySynCtxt _)  = Nothing -- Any kind will do
896 expectedKindInCtxt ThBrackCtxt    = Nothing
897 expectedKindInCtxt GhciCtxt       = Nothing
898 expectedKindInCtxt ResSigCtxt     = Just openTypeKind
899 expectedKindInCtxt ExprSigCtxt    = Just openTypeKind
900 expectedKindInCtxt (ForSigCtxt _) = Just liftedTypeKind
901 expectedKindInCtxt InstDeclCtxt   = Just constraintKind
902 expectedKindInCtxt SpecInstCtxt   = Just constraintKind
903 expectedKindInCtxt _              = Just argTypeKind
904
905 checkValidType :: UserTypeCtxt -> Type -> TcM ()
906 -- Checks that the type is valid for the given context
907 -- Not used for instance decls; checkValidInstance instead
908 checkValidType ctxt ty 
909   = do { traceTc "checkValidType" (ppr ty <+> text "::" <+> ppr (typeKind ty))
910        ; unboxed         <- xoptM Opt_UnboxedTuples
911        ; rank2_flag      <- xoptM Opt_Rank2Types
912        ; rankn_flag      <- xoptM Opt_RankNTypes
913        ; polycomp        <- xoptM Opt_PolymorphicComponents
914        ; constraintKinds <- xoptM Opt_ConstraintKinds
915        ; let gen_rank :: Rank -> Rank
916              gen_rank r | rankn_flag = ArbitraryRank
917                         | rank2_flag = r2
918                         | otherwise  = r
919
920              rank2 = gen_rank r2
921              rank1 = gen_rank r1
922              rank0 = gen_rank r0
923
924              r0 = rankZeroMonoType
925              r1 = LimitedRank True r0
926              r2 = LimitedRank True r1
927
928              rank
929                = case ctxt of
930                  DefaultDeclCtxt-> MustBeMonoType
931                  ResSigCtxt     -> MustBeMonoType
932                  LamPatSigCtxt  -> rank0
933                  BindPatSigCtxt -> rank0
934                  TySynCtxt _    -> rank0
935
936                  ExprSigCtxt    -> rank1
937                  FunSigCtxt _   -> rank1
938                  InfSigCtxt _   -> ArbitraryRank        -- Inferred type
939                  ConArgCtxt _   | polycomp -> rank2
940                                      -- We are given the type of the entire
941                                      -- constructor, hence rank 1
942                                 | otherwise -> rank1
943
944                  ForSigCtxt _   -> rank1
945                  SpecInstCtxt   -> rank1
946                  ThBrackCtxt    -> rank1
947                  GhciCtxt       -> ArbitraryRank
948                  _              -> panic "checkValidType"
949                                           -- Can't happen; not used for *user* sigs
950
951              actual_kind = typeKind ty
952
953              kind_ok = case expectedKindInCtxt ctxt of
954                          Nothing -> True
955                          Just k  -> tcIsSubKind actual_kind k
956         
957              ubx_tup 
958               | not unboxed = UT_NotOk
959               | otherwise   = case ctxt of
960                                    TySynCtxt _ -> UT_Ok
961                                    ExprSigCtxt -> UT_Ok
962                                    ThBrackCtxt -> UT_Ok
963                                    GhciCtxt    -> UT_Ok
964                                    _           -> UT_NotOk
965
966         -- Check the internal validity of the type itself
967        ; check_type rank ubx_tup ty
968
969         -- Check that the thing has kind Type, and is lifted if necessary
970         -- Do this second, because we can't usefully take the kind of an 
971         -- ill-formed type such as (a~Int)
972        ; checkTc kind_ok (kindErr actual_kind)
973
974         -- Check that the thing does not have kind Constraint,
975         -- if -XConstraintKinds isn't enabled
976        ; unless constraintKinds $
977          checkTc (not (isConstraintKind actual_kind)) (predTupleErr ty)
978        }
979
980 checkValidMonoType :: Type -> TcM ()
981 checkValidMonoType ty = check_mono_type MustBeMonoType ty
982 \end{code}
983
984 Note [Higher rank types]
985 ~~~~~~~~~~~~~~~~~~~~~~~~
986 Technically 
987             Int -> forall a. a->a
988 is still a rank-1 type, but it's not Haskell 98 (Trac #5957).  So the
989 validity checker allow a forall after an arrow only if we allow it
990 before -- that is, with Rank2Types or RankNTypes
991
992 \begin{code}
993 data Rank = ArbitraryRank         -- Any rank ok
994
995           | LimitedRank   -- Note [Higher rank types]
996                  Bool     -- Forall ok at top
997                  Rank     -- Use for function arguments
998
999           | MonoType SDoc   -- Monotype, with a suggestion of how it could be a polytype
1000   
1001           | MustBeMonoType  -- Monotype regardless of flags
1002
1003 rankZeroMonoType, tyConArgMonoType, synArgMonoType :: Rank
1004 rankZeroMonoType = MonoType (ptext (sLit "Perhaps you intended to use -XRankNTypes or -XRank2Types"))
1005 tyConArgMonoType = MonoType (ptext (sLit "Perhaps you intended to use -XImpredicativeTypes"))
1006 synArgMonoType   = MonoType (ptext (sLit "Perhaps you intended to use -XLiberalTypeSynonyms"))
1007
1008 funArgResRank :: Rank -> (Rank, Rank)             -- Function argument and result
1009 funArgResRank (LimitedRank _ arg_rank) = (arg_rank, LimitedRank (forAllAllowed arg_rank) arg_rank)
1010 funArgResRank other_rank               = (other_rank, other_rank)
1011
1012 forAllAllowed :: Rank -> Bool
1013 forAllAllowed ArbitraryRank             = True
1014 forAllAllowed (LimitedRank forall_ok _) = forall_ok
1015 forAllAllowed _                         = False
1016
1017 ----------------------------------------
1018 data UbxTupFlag = UT_Ok | UT_NotOk
1019         -- The "Ok" version means "ok if UnboxedTuples is on"
1020
1021 ----------------------------------------
1022 check_mono_type :: Rank -> KindOrType -> TcM () -- No foralls anywhere
1023                                                 -- No unlifted types of any kind
1024 check_mono_type rank ty
1025   | isKind ty = return ()  -- IA0_NOTE: Do we need to check kinds?
1026   | otherwise
1027    = do { check_type rank UT_NotOk ty
1028         ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
1029
1030 check_type :: Rank -> UbxTupFlag -> Type -> TcM ()
1031 -- The args say what the *type context* requires, independent
1032 -- of *flag* settings.  You test the flag settings at usage sites.
1033 -- 
1034 -- Rank is allowed rank for function args
1035 -- Rank 0 means no for-alls anywhere
1036
1037 check_type rank ubx_tup ty
1038   | not (null tvs && null theta)
1039   = do  { checkTc (forAllAllowed rank) (forAllTyErr rank ty)
1040                 -- Reject e.g. (Maybe (?x::Int => Int)), 
1041                 -- with a decent error message
1042         ; check_valid_theta SigmaCtxt theta
1043         ; check_type rank ubx_tup tau   -- Allow foralls to right of arrow
1044         ; checkAmbiguity tvs theta (tyVarsOfType tau) }
1045   where
1046     (tvs, theta, tau) = tcSplitSigmaTy ty
1047    
1048 check_type _ _ (TyVarTy _) = return ()
1049
1050 check_type rank _ (FunTy arg_ty res_ty)
1051   = do  { check_type arg_rank UT_NotOk arg_ty
1052         ; check_type res_rank UT_Ok    res_ty }
1053   where
1054     (arg_rank, res_rank) = funArgResRank rank
1055
1056 check_type rank _ (AppTy ty1 ty2)
1057   = do  { check_arg_type rank ty1
1058         ; check_arg_type rank ty2 }
1059
1060 check_type rank ubx_tup ty@(TyConApp tc tys)
1061   | isSynTyCon tc
1062   = do  {       -- Check that the synonym has enough args
1063                 -- This applies equally to open and closed synonyms
1064                 -- It's OK to have an *over-applied* type synonym
1065                 --      data Tree a b = ...
1066                 --      type Foo a = Tree [a]
1067                 --      f :: Foo a b -> ...
1068           checkTc (tyConArity tc <= length tys) arity_msg
1069
1070         -- See Note [Liberal type synonyms]
1071         ; liberal <- xoptM Opt_LiberalTypeSynonyms
1072         ; if not liberal || isSynFamilyTyCon tc then
1073                 -- For H98 and synonym families, do check the type args
1074                 mapM_ (check_mono_type synArgMonoType) tys
1075
1076           else  -- In the liberal case (only for closed syns), expand then check
1077           case tcView ty of   
1078              Just ty' -> check_type rank ubx_tup ty' 
1079              Nothing  -> pprPanic "check_tau_type" (ppr ty)
1080     }
1081     
1082   | isUnboxedTupleTyCon tc
1083   = do  { ub_tuples_allowed <- xoptM Opt_UnboxedTuples
1084         ; checkTc (ubx_tup_ok ub_tuples_allowed) ubx_tup_msg
1085
1086         ; impred <- xoptM Opt_ImpredicativeTypes        
1087         ; let rank' = if impred then ArbitraryRank else tyConArgMonoType
1088                 -- c.f. check_arg_type
1089                 -- However, args are allowed to be unlifted, or
1090                 -- more unboxed tuples, so can't use check_arg_ty
1091         ; mapM_ (check_type rank' UT_Ok) tys }
1092
1093   | otherwise
1094   = mapM_ (check_arg_type rank) tys
1095
1096   where
1097     ubx_tup_ok ub_tuples_allowed = case ubx_tup of
1098                                    UT_Ok -> ub_tuples_allowed
1099                                    _     -> False
1100
1101     n_args    = length tys
1102     tc_arity  = tyConArity tc
1103
1104     arity_msg   = arityErr "Type synonym" (tyConName tc) tc_arity n_args
1105     ubx_tup_msg = ubxArgTyErr ty
1106
1107 check_type _ _ (LitTy {}) = return ()
1108
1109 check_type _ _ ty = pprPanic "check_type" (ppr ty)
1110
1111 ----------------------------------------
1112 check_arg_type :: Rank -> KindOrType -> TcM ()
1113 -- The sort of type that can instantiate a type variable,
1114 -- or be the argument of a type constructor.
1115 -- Not an unboxed tuple, but now *can* be a forall (since impredicativity)
1116 -- Other unboxed types are very occasionally allowed as type
1117 -- arguments depending on the kind of the type constructor
1118 -- 
1119 -- For example, we want to reject things like:
1120 --
1121 --      instance Ord a => Ord (forall s. T s a)
1122 -- and
1123 --      g :: T s (forall b.b)
1124 --
1125 -- NB: unboxed tuples can have polymorphic or unboxed args.
1126 --     This happens in the workers for functions returning
1127 --     product types with polymorphic components.
1128 --     But not in user code.
1129 -- Anyway, they are dealt with by a special case in check_tau_type
1130
1131 check_arg_type rank ty
1132   | isKind ty = return ()  -- IA0_NOTE: Do we need to check a kind?
1133   | otherwise
1134   = do  { impred <- xoptM Opt_ImpredicativeTypes
1135         ; let rank' = case rank of          -- Predictive => must be monotype
1136                         MustBeMonoType     -> MustBeMonoType  -- Monotype, regardless
1137                         _other | impred    -> ArbitraryRank
1138                                | otherwise -> tyConArgMonoType
1139                         -- Make sure that MustBeMonoType is propagated, 
1140                         -- so that we don't suggest -XImpredicativeTypes in
1141                         --    (Ord (forall a.a)) => a -> a
1142                         -- and so that if it Must be a monotype, we check that it is!
1143
1144         ; check_type rank' UT_NotOk ty
1145         ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
1146              -- NB the isUnLiftedType test also checks for 
1147              --    T State#
1148              -- where there is an illegal partial application of State# (which has
1149              -- kind * -> #); see Note [The kind invariant] in TypeRep
1150
1151 ----------------------------------------
1152 forAllTyErr :: Rank -> Type -> SDoc
1153 forAllTyErr rank ty 
1154    = vcat [ hang (ptext (sLit "Illegal polymorphic or qualified type:")) 2 (ppr ty)
1155           , suggestion ]
1156   where
1157     suggestion = case rank of
1158                    LimitedRank {} -> ptext (sLit "Perhaps you intended to use -XRankNTypes or -XRank2Types")
1159                    MonoType d     -> d
1160                    _              -> empty      -- Polytype is always illegal
1161
1162 unliftedArgErr, ubxArgTyErr :: Type -> SDoc
1163 unliftedArgErr  ty = sep [ptext (sLit "Illegal unlifted type:"), ppr ty]
1164 ubxArgTyErr     ty = sep [ptext (sLit "Illegal unboxed tuple type as function argument:"), ppr ty]
1165
1166 kindErr :: Kind -> SDoc
1167 kindErr kind       = sep [ptext (sLit "Expecting an ordinary type, but found a type of kind"), ppr kind]
1168 \end{code}
1169
1170 Note [Liberal type synonyms]
1171 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1172 If -XLiberalTypeSynonyms is on, expand closed type synonyms *before*
1173 doing validity checking.  This allows us to instantiate a synonym defn
1174 with a for-all type, or with a partially-applied type synonym.
1175         e.g.   type T a b = a
1176                type S m   = m ()
1177                f :: S (T Int)
1178 Here, T is partially applied, so it's illegal in H98.  But if you
1179 expand S first, then T we get just
1180                f :: Int
1181 which is fine.
1182
1183 IMPORTANT: suppose T is a type synonym.  Then we must do validity
1184 checking on an appliation (T ty1 ty2)
1185
1186         *either* before expansion (i.e. check ty1, ty2)
1187         *or* after expansion (i.e. expand T ty1 ty2, and then check)
1188         BUT NOT BOTH
1189
1190 If we do both, we get exponential behaviour!!
1191
1192   data TIACons1 i r c = c i ::: r c
1193   type TIACons2 t x = TIACons1 t (TIACons1 t x)
1194   type TIACons3 t x = TIACons2 t (TIACons1 t x)
1195   type TIACons4 t x = TIACons2 t (TIACons2 t x)
1196   type TIACons7 t x = TIACons4 t (TIACons3 t x)
1197
1198
1199 %************************************************************************
1200 %*                                                                      *
1201 \subsection{Checking a theta or source type}
1202 %*                                                                      *
1203 %************************************************************************
1204
1205 \begin{code}
1206 checkValidTheta :: UserTypeCtxt -> ThetaType -> TcM ()
1207 checkValidTheta ctxt theta 
1208   = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
1209
1210 -------------------------
1211 check_valid_theta :: UserTypeCtxt -> [PredType] -> TcM ()
1212 check_valid_theta _ []
1213   = return ()
1214 check_valid_theta ctxt theta = do
1215     dflags <- getDynFlags
1216     warnTc (notNull dups) (dupPredWarn dups)
1217     mapM_ (check_pred_ty dflags ctxt) theta
1218   where
1219     (_,dups) = removeDups cmpPred theta
1220
1221 -------------------------
1222 check_pred_ty :: DynFlags -> UserTypeCtxt -> PredType -> TcM ()
1223 check_pred_ty dflags ctxt pred = check_pred_ty' dflags ctxt (shallowPredTypePredTree pred)
1224
1225 check_pred_ty' :: DynFlags -> UserTypeCtxt -> PredTree -> TcM ()
1226 check_pred_ty' dflags ctxt (ClassPred cls tys)
1227   = do {        -- Class predicates are valid in all contexts
1228        ; checkTc (arity == n_tys) arity_err
1229
1230                 -- Check the form of the argument types
1231        ; mapM_ checkValidMonoType tys
1232        ; checkTc (check_class_pred_tys dflags ctxt tys)
1233                  (predTyVarErr (mkClassPred cls tys) $$ how_to_allow)
1234        }
1235   where
1236     class_name = className cls
1237     arity      = classArity cls
1238     n_tys      = length tys
1239     arity_err  = arityErr "Class" class_name arity n_tys
1240     how_to_allow = parens (ptext (sLit "Use -XFlexibleContexts to permit this"))
1241
1242
1243 check_pred_ty' dflags _ctxt (EqPred ty1 ty2)
1244   = do {        -- Equational constraints are valid in all contexts if type
1245                 -- families are permitted
1246        ; checkTc (xopt Opt_TypeFamilies dflags || xopt Opt_GADTs dflags) 
1247                  (eqPredTyErr (mkEqPred ty1 ty2))
1248
1249                 -- Check the form of the argument types
1250        ; checkValidMonoType ty1
1251        ; checkValidMonoType ty2
1252        }
1253
1254 check_pred_ty' _ _ctxt (IPPred _ ty) = checkValidMonoType ty
1255         -- Contrary to GHC 7.2 and below, we allow implicit parameters not only
1256         -- in type signatures but also in instance decls, superclasses etc
1257         -- The reason we didn't allow implicit params in instances is a bit
1258         -- subtle:
1259         -- If we allowed        instance (?x::Int, Eq a) => Foo [a] where ...
1260         -- then when we saw (e :: (?x::Int) => t) it would be unclear how to 
1261         -- discharge all the potential usas of the ?x in e.   For example, a
1262         -- constraint Foo [Int] might come out of e,and applying the
1263         -- instance decl would show up two uses of ?x.
1264         --
1265         -- Happily this is not an issue in the new constraint solver.
1266
1267 check_pred_ty' dflags ctxt t@(TuplePred ts)
1268   = do { checkTc (xopt Opt_ConstraintKinds dflags)
1269                  (predTupleErr (predTreePredType t))
1270        ; mapM_ (check_pred_ty dflags ctxt) ts }
1271     -- This case will not normally be executed because without -XConstraintKinds
1272     -- tuple types are only kind-checked as *
1273
1274 check_pred_ty' dflags ctxt (IrredPred pred)
1275     -- Allowing irreducible predicates in class superclasses is somewhat dangerous
1276     -- because we can write:
1277     --
1278     --  type family Fooish x :: * -> Constraint
1279     --  type instance Fooish () = Foo
1280     --  class Fooish () a => Foo a where
1281     --
1282     -- This will cause the constraint simplifier to loop because every time we canonicalise a
1283     -- (Foo a) class constraint we add a (Fooish () a) constraint which will be immediately
1284     -- solved to add+canonicalise another (Foo a) constraint.
1285     --
1286     -- It is equally dangerous to allow them in instance heads because in that case the
1287     -- Paterson conditions may not detect duplication of a type variable or size change.
1288     --
1289     -- In both cases it's OK if the predicate is actually a synonym, though.
1290     -- We'll also allow it if
1291   = do checkTc (xopt Opt_ConstraintKinds dflags)
1292                (predIrredErr pred)
1293        case tcView pred of
1294          Just pred' -> 
1295            -- Synonym: just look through
1296            check_pred_ty dflags ctxt pred'
1297          Nothing
1298            | xopt Opt_UndecidableInstances dflags -> return ()
1299            | otherwise -> do
1300              -- Make sure it is OK to have an irred pred in this context
1301              checkTc (case ctxt of ClassSCCtxt _ -> False; InstDeclCtxt -> False; _ -> True)
1302                      (predIrredBadCtxtErr pred)
1303
1304 -------------------------
1305 check_class_pred_tys :: DynFlags -> UserTypeCtxt -> [KindOrType] -> Bool
1306 check_class_pred_tys dflags ctxt kts
1307   = case ctxt of
1308         SpecInstCtxt -> True    -- {-# SPECIALISE instance Eq (T Int) #-} is fine
1309         InstDeclCtxt -> flexible_contexts || undecidable_ok || all tcIsTyVarTy tys
1310                                 -- Further checks on head and theta in
1311                                 -- checkInstTermination
1312         _             -> flexible_contexts || all tyvar_head tys
1313   where
1314     (_, tys) = span isKind kts  -- see Note [Kind polymorphic type classes]
1315     flexible_contexts = xopt Opt_FlexibleContexts dflags
1316     undecidable_ok = xopt Opt_UndecidableInstances dflags
1317
1318 {-
1319 Note [Kind polymorphic type classes]
1320 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1321
1322 class C f where
1323   empty :: f a
1324 -- C :: forall k. k -> Constraint
1325 -- empty :: forall (a :: k). f a
1326
1327 MultiParam:
1328 ~~~~~~~~~~~
1329
1330 instance C Maybe where
1331   empty = Nothing
1332
1333 The dictionary gets type [C * Maybe] even if it's not a MultiParam
1334 type class.
1335
1336 Flexible:
1337 ~~~~~~~~~
1338
1339 data D a = D
1340 -- D :: forall k. k -> *
1341
1342 instance C D where
1343   empty = D
1344
1345 The dictionary gets type [C * (D *)]. IA0_TODO it should be
1346 generalized actually.
1347
1348 -}
1349
1350 -------------------------
1351 tyvar_head :: Type -> Bool
1352 tyvar_head ty                   -- Haskell 98 allows predicates of form 
1353   | tcIsTyVarTy ty = True       --      C (a ty1 .. tyn)
1354   | otherwise                   -- where a is a type variable
1355   = case tcSplitAppTy_maybe ty of
1356         Just (ty, _) -> tyvar_head ty
1357         Nothing      -> False
1358 \end{code}
1359
1360 Check for ambiguity
1361 ~~~~~~~~~~~~~~~~~~~
1362           forall V. P => tau
1363 is ambiguous if P contains generic variables
1364 (i.e. one of the Vs) that are not mentioned in tau
1365
1366 However, we need to take account of functional dependencies
1367 when we speak of 'mentioned in tau'.  Example:
1368         class C a b | a -> b where ...
1369 Then the type
1370         forall x y. (C x y) => x
1371 is not ambiguous because x is mentioned and x determines y
1372
1373 NB; the ambiguity check is only used for *user* types, not for types
1374 coming from inteface files.  The latter can legitimately have
1375 ambiguous types. Example
1376
1377    class S a where s :: a -> (Int,Int)
1378    instance S Char where s _ = (1,1)
1379    f:: S a => [a] -> Int -> (Int,Int)
1380    f (_::[a]) x = (a*x,b)
1381         where (a,b) = s (undefined::a)
1382
1383 Here the worker for f gets the type
1384         fw :: forall a. S a => Int -> (# Int, Int #)
1385
1386 If the list of tv_names is empty, we have a monotype, and then we
1387 don't need to check for ambiguity either, because the test can't fail
1388 (see is_ambig).
1389
1390 In addition, GHC insists that at least one type variable
1391 in each constraint is in V.  So we disallow a type like
1392         forall a. Eq b => b -> b
1393 even in a scope where b is in scope.
1394
1395 \begin{code}
1396 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
1397 checkAmbiguity forall_tyvars theta tau_tyvars
1398   = mapM_ complain (filter is_ambig theta)
1399   where
1400     complain pred     = addErrTc (ambigErr pred)
1401     extended_tau_vars = growThetaTyVars theta tau_tyvars
1402
1403         -- See Note [Implicit parameters and ambiguity] in TcSimplify
1404     is_ambig pred     = isClassPred  pred &&
1405                         any ambig_var (varSetElems (tyVarsOfType pred))
1406
1407     ambig_var ct_var  = (ct_var `elem` forall_tyvars) &&
1408                         not (ct_var `elemVarSet` extended_tau_vars)
1409
1410 ambigErr :: PredType -> SDoc
1411 ambigErr pred
1412   = sep [ptext (sLit "Ambiguous constraint") <+> quotes (pprType pred),
1413          nest 2 (ptext (sLit "At least one of the forall'd type variables mentioned by the constraint") $$
1414                  ptext (sLit "must be reachable from the type after the '=>'"))]
1415 \end{code}
1416
1417 Note [Growing the tau-tvs using constraints]
1418 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1419 (growInstsTyVars insts tvs) is the result of extending the set 
1420     of tyvars tvs using all conceivable links from pred
1421
1422 E.g. tvs = {a}, preds = {H [a] b, K (b,Int) c, Eq e}
1423 Then grow precs tvs = {a,b,c}
1424
1425 \begin{code}
1426 growThetaTyVars :: TcThetaType -> TyVarSet -> TyVarSet
1427 -- See Note [Growing the tau-tvs using constraints]
1428 growThetaTyVars theta tvs
1429   | null theta = tvs
1430   | otherwise  = fixVarSet mk_next tvs
1431   where
1432     mk_next tvs = foldr grow_one tvs theta
1433     grow_one pred tvs = growPredTyVars pred tvs `unionVarSet` tvs
1434
1435 growPredTyVars :: TcPredType
1436                -> TyVarSet      -- The set to extend
1437                -> TyVarSet      -- TyVars of the predicate if it intersects
1438                                 -- the set, or is implicit parameter
1439 growPredTyVars pred tvs = go (classifyPredType pred)
1440   where
1441     grow pred_tvs | pred_tvs `intersectsVarSet` tvs = pred_tvs
1442                   | otherwise                       = emptyVarSet
1443
1444     go (IPPred _ ty)     = tyVarsOfType ty -- See Note [Implicit parameters and ambiguity]
1445     go (ClassPred _ tys) = grow (tyVarsOfTypes tys)
1446     go (EqPred ty1 ty2)  = grow (tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2)
1447     go (TuplePred ts)    = unionVarSets (map (go . classifyPredType) ts)
1448     go (IrredPred ty)    = grow (tyVarsOfType ty)
1449 \end{code}
1450     
1451 Note [Implicit parameters and ambiguity] 
1452 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1453 Only a *class* predicate can give rise to ambiguity
1454 An *implicit parameter* cannot.  For example:
1455         foo :: (?x :: [a]) => Int
1456         foo = length ?x
1457 is fine.  The call site will suppply a particular 'x'
1458
1459 Furthermore, the type variables fixed by an implicit parameter
1460 propagate to the others.  E.g.
1461         foo :: (Show a, ?x::[a]) => Int
1462         foo = show (?x++?x)
1463 The type of foo looks ambiguous.  But it isn't, because at a call site
1464 we might have
1465         let ?x = 5::Int in foo
1466 and all is well.  In effect, implicit parameters are, well, parameters,
1467 so we can take their type variables into account as part of the
1468 "tau-tvs" stuff.  This is done in the function 'FunDeps.grow'.
1469
1470
1471 \begin{code}
1472 checkThetaCtxt :: UserTypeCtxt -> ThetaType -> SDoc
1473 checkThetaCtxt ctxt theta
1474   = vcat [ptext (sLit "In the context:") <+> pprTheta theta,
1475           ptext (sLit "While checking") <+> pprUserTypeCtxt ctxt ]
1476
1477 eqPredTyErr, predTyVarErr, predTupleErr, predIrredErr, predIrredBadCtxtErr :: PredType -> SDoc
1478 eqPredTyErr  pred = ptext (sLit "Illegal equational constraint") <+> pprType pred
1479                     $$
1480                     parens (ptext (sLit "Use -XGADTs or -XTypeFamilies to permit this"))
1481 predTyVarErr pred  = sep [ptext (sLit "Non type-variable argument"),
1482                           nest 2 (ptext (sLit "in the constraint:") <+> pprType pred)]
1483 predTupleErr pred  = ptext (sLit "Illegal tuple constraint") <+> pprType pred $$
1484                      parens (ptext (sLit "Use -XConstraintKinds to permit this"))
1485 predIrredErr pred  = ptext (sLit "Illegal irreducible constraint") <+> pprType pred $$
1486                      parens (ptext (sLit "Use -XConstraintKinds to permit this"))
1487 predIrredBadCtxtErr pred = ptext (sLit "Illegal irreducible constraint") <+> pprType pred $$
1488                            ptext (sLit "in superclass/instance head context") <+>
1489                            parens (ptext (sLit "Use -XUndecidableInstances to permit this"))
1490 dupPredWarn :: [[PredType]] -> SDoc
1491 dupPredWarn dups   = ptext (sLit "Duplicate constraint(s):") <+> pprWithCommas pprType (map head dups)
1492
1493 arityErr :: Outputable a => String -> a -> Int -> Int -> SDoc
1494 arityErr kind name n m
1495   = hsep [ text kind, quotes (ppr name), ptext (sLit "should have"),
1496            n_arguments <> comma, text "but has been given", 
1497            if m==0 then text "none" else int m]
1498     where
1499         n_arguments | n == 0 = ptext (sLit "no arguments")
1500                     | n == 1 = ptext (sLit "1 argument")
1501                     | True   = hsep [int n, ptext (sLit "arguments")]
1502 \end{code}
1503
1504 %************************************************************************
1505 %*                                                                      *
1506 \subsection{Checking for a decent instance head type}
1507 %*                                                                      *
1508 %************************************************************************
1509
1510 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1511 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1512
1513 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1514 flag is on, or (2)~the instance is imported (they must have been
1515 compiled elsewhere). In these cases, we let them go through anyway.
1516
1517 We can also have instances for functions: @instance Foo (a -> b) ...@.
1518
1519 \begin{code}
1520 checkValidInstHead :: UserTypeCtxt -> Class -> [Type] -> TcM ()
1521 checkValidInstHead ctxt clas cls_args
1522   = do { dflags <- getDynFlags
1523
1524            -- Check language restrictions; 
1525            -- but not for SPECIALISE isntance pragmas
1526        ; let ty_args = dropWhile isKind cls_args
1527        ; unless spec_inst_prag $
1528          do { checkTc (xopt Opt_TypeSynonymInstances dflags ||
1529                        all tcInstHeadTyNotSynonym ty_args)
1530                  (instTypeErr pp_pred head_type_synonym_msg)
1531             ; checkTc (xopt Opt_FlexibleInstances dflags ||
1532                        all tcInstHeadTyAppAllTyVars ty_args)
1533                  (instTypeErr pp_pred head_type_args_tyvars_msg)
1534             ; checkTc (xopt Opt_MultiParamTypeClasses dflags ||
1535                        isSingleton ty_args)  -- Only count type arguments
1536                  (instTypeErr pp_pred head_one_type_msg) }
1537
1538          -- May not contain type family applications
1539        ; mapM_ checkTyFamFreeness ty_args
1540
1541        ; mapM_ checkValidMonoType ty_args
1542         -- For now, I only allow tau-types (not polytypes) in 
1543         -- the head of an instance decl.  
1544         --      E.g.  instance C (forall a. a->a) is rejected
1545         -- One could imagine generalising that, but I'm not sure
1546         -- what all the consequences might be
1547        }
1548
1549   where
1550     spec_inst_prag = case ctxt of { SpecInstCtxt -> True; _ -> False }
1551
1552     pp_pred = pprClassPred clas cls_args
1553     head_type_synonym_msg = parens (
1554                 text "All instance types must be of the form (T t1 ... tn)" $$
1555                 text "where T is not a synonym." $$
1556                 text "Use -XTypeSynonymInstances if you want to disable this.")
1557
1558     head_type_args_tyvars_msg = parens (vcat [
1559                 text "All instance types must be of the form (T a1 ... an)",
1560                 text "where a1 ... an are *distinct type variables*,",
1561                 text "and each type variable appears at most once in the instance head.",
1562                 text "Use -XFlexibleInstances if you want to disable this."])
1563
1564     head_one_type_msg = parens (
1565                 text "Only one type can be given in an instance head." $$
1566                 text "Use -XMultiParamTypeClasses if you want to allow more.")
1567
1568 instTypeErr :: SDoc -> SDoc -> SDoc
1569 instTypeErr pp_ty msg
1570   = sep [ptext (sLit "Illegal instance declaration for") <+> quotes pp_ty, 
1571          nest 2 msg]
1572 \end{code}
1573
1574 validDeivPred checks for OK 'deriving' context.  See Note [Exotic
1575 derived instance contexts] in TcSimplify.  However the predicate is
1576 here because it uses sizeTypes, fvTypes.
1577
1578 Also check for a bizarre corner case, when the derived instance decl 
1579 would look like
1580     instance C a b => D (T a) where ...
1581 Note that 'b' isn't a parameter of T.  This gives rise to all sorts of
1582 problems; in particular, it's hard to compare solutions for equality
1583 when finding the fixpoint, and that means the inferContext loop does
1584 not converge.  See Trac #5287.
1585
1586 \begin{code}
1587 validDerivPred :: TyVarSet -> PredType -> Bool
1588 validDerivPred tv_set ty = case getClassPredTys_maybe ty of
1589   Just (_, tys) | let fvs = fvTypes tys
1590                 -> hasNoDups fvs 
1591                 && sizeTypes tys == length fvs
1592                 && all (`elemVarSet` tv_set) fvs
1593   _ -> False
1594 \end{code}
1595
1596
1597 %************************************************************************
1598 %*                                                                      *
1599 \subsection{Checking instance for termination}
1600 %*                                                                      *
1601 %************************************************************************
1602
1603 \begin{code}
1604 checkValidInstance :: UserTypeCtxt -> LHsType Name -> Type
1605                    -> TcM ([TyVar], ThetaType, Class, [Type])
1606 checkValidInstance ctxt hs_type ty
1607   = do { let (tvs, theta, tau) = tcSplitSigmaTy ty
1608        ; case getClassPredTys_maybe tau of {
1609            Nothing          -> failWithTc (ptext (sLit "Malformed instance type")) ;
1610            Just (clas,inst_tys)  -> 
1611     do  { setSrcSpan head_loc (checkValidInstHead ctxt clas inst_tys)
1612         ; checkValidTheta ctxt theta
1613         ; checkAmbiguity tvs theta (tyVarsOfTypes inst_tys)
1614
1615         -- Check that instance inference will terminate (if we care)
1616         -- For Haskell 98 this will already have been done by checkValidTheta,
1617         -- but as we may be using other extensions we need to check.
1618         ; undecidable_ok <- xoptM Opt_UndecidableInstances
1619         ; unless undecidable_ok $
1620           mapM_ addErrTc (checkInstTermination inst_tys theta)
1621         
1622         -- The Coverage Condition
1623         ; checkTc (undecidable_ok || checkInstCoverage clas inst_tys)
1624                   (instTypeErr (pprClassPred clas inst_tys) msg)
1625         ; return (tvs, theta, clas, inst_tys) } } }
1626   where
1627     msg  = parens (vcat [ptext (sLit "the Coverage Condition fails for one of the functional dependencies;"),
1628                          undecidableMsg])
1629
1630         -- The location of the "head" of the instance
1631     head_loc = case hs_type of
1632                  L _ (HsForAllTy _ _ _ (L loc _)) -> loc
1633                  L loc _                          -> loc
1634 \end{code}
1635
1636 Note [Paterson conditions]
1637 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1638
1639 Termination test: the so-called "Paterson conditions" (see Section 5 of
1640 "Understanding functionsl dependencies via Constraint Handling Rules, 
1641 JFP Jan 2007).
1642
1643 We check that each assertion in the context satisfies:
1644  (1) no variable has more occurrences in the assertion than in the head, and
1645  (2) the assertion has fewer constructors and variables (taken together
1646      and counting repetitions) than the head.
1647 This is only needed with -fglasgow-exts, as Haskell 98 restrictions
1648 (which have already been checked) guarantee termination. 
1649
1650 The underlying idea is that 
1651
1652     for any ground substitution, each assertion in the
1653     context has fewer type constructors than the head.
1654
1655
1656 \begin{code}
1657 checkInstTermination :: [TcType] -> ThetaType -> [MsgDoc]
1658 checkInstTermination tys theta
1659   = mapCatMaybes check theta
1660   where
1661    fvs  = fvTypes tys
1662    size = sizeTypes tys
1663    check pred 
1664       | not (null (fvType pred \\ fvs)) 
1665       = Just (predUndecErr pred nomoreMsg $$ parens undecidableMsg)
1666       | sizePred pred >= size
1667       = Just (predUndecErr pred smallerMsg $$ parens undecidableMsg)
1668       | otherwise
1669       = Nothing
1670
1671 predUndecErr :: PredType -> SDoc -> SDoc
1672 predUndecErr pred msg = sep [msg,
1673                         nest 2 (ptext (sLit "in the constraint:") <+> pprType pred)]
1674
1675 nomoreMsg, smallerMsg, undecidableMsg :: SDoc
1676 nomoreMsg = ptext (sLit "Variable occurs more often in a constraint than in the instance head")
1677 smallerMsg = ptext (sLit "Constraint is no smaller than the instance head")
1678 undecidableMsg = ptext (sLit "Use -XUndecidableInstances to permit this")
1679 \end{code}
1680
1681
1682 %************************************************************************
1683 %*                                                                      *
1684         Checking type instance well-formedness and termination
1685 %*                                                                      *
1686 %************************************************************************
1687
1688 \begin{code}
1689 -- Check that a "type instance" is well-formed (which includes decidability
1690 -- unless -XUndecidableInstances is given).
1691 --
1692 checkValidFamInst :: [Type] -> Type -> TcM ()
1693 checkValidFamInst typats rhs
1694   = do { -- left-hand side contains no type family applications
1695          -- (vanilla synonyms are fine, though)
1696        ; mapM_ checkTyFamFreeness typats
1697
1698          -- the right-hand side is a tau type
1699        ; checkValidMonoType rhs
1700
1701          -- we have a decidable instance unless otherwise permitted
1702        ; undecidable_ok <- xoptM Opt_UndecidableInstances
1703        ; unless undecidable_ok $
1704            mapM_ addErrTc (checkFamInstRhs typats (tcTyFamInsts rhs))
1705        }
1706
1707 -- Make sure that each type family instance is 
1708 --   (1) strictly smaller than the lhs,
1709 --   (2) mentions no type variable more often than the lhs, and
1710 --   (3) does not contain any further type family instances.
1711 --
1712 checkFamInstRhs :: [Type]                  -- lhs
1713                 -> [(TyCon, [Type])]       -- type family instances
1714                 -> [MsgDoc]
1715 checkFamInstRhs lhsTys famInsts
1716   = mapCatMaybes check famInsts
1717   where
1718    size = sizeTypes lhsTys
1719    fvs  = fvTypes lhsTys
1720    check (tc, tys)
1721       | not (all isTyFamFree tys)
1722       = Just (famInstUndecErr famInst nestedMsg $$ parens undecidableMsg)
1723       | not (null (fvTypes tys \\ fvs))
1724       = Just (famInstUndecErr famInst nomoreVarMsg $$ parens undecidableMsg)
1725       | size <= sizeTypes tys
1726       = Just (famInstUndecErr famInst smallerAppMsg $$ parens undecidableMsg)
1727       | otherwise
1728       = Nothing
1729       where
1730         famInst = TyConApp tc tys
1731
1732 -- Ensure that no type family instances occur in a type.
1733 --
1734 checkTyFamFreeness :: Type -> TcM ()
1735 checkTyFamFreeness ty
1736   = checkTc (isTyFamFree ty) $
1737       tyFamInstIllegalErr ty
1738
1739 -- Check that a type does not contain any type family applications.
1740 --
1741 isTyFamFree :: Type -> Bool
1742 isTyFamFree = null . tcTyFamInsts
1743
1744 -- Error messages
1745
1746 tyFamInstIllegalErr :: Type -> SDoc
1747 tyFamInstIllegalErr ty
1748   = hang (ptext (sLit "Illegal type synonym family application in instance") <> 
1749          colon) 2 $
1750       ppr ty
1751
1752 famInstUndecErr :: Type -> SDoc -> SDoc
1753 famInstUndecErr ty msg 
1754   = sep [msg, 
1755          nest 2 (ptext (sLit "in the type family application:") <+> 
1756                  pprType ty)]
1757
1758 nestedMsg, nomoreVarMsg, smallerAppMsg :: SDoc
1759 nestedMsg     = ptext (sLit "Nested type family application")
1760 nomoreVarMsg  = ptext (sLit "Variable occurs more often than in instance head")
1761 smallerAppMsg = ptext (sLit "Application is no smaller than the instance head")
1762 \end{code}
1763
1764
1765 %************************************************************************
1766 %*                                                                      *
1767 \subsection{Auxiliary functions}
1768 %*                                                                      *
1769 %************************************************************************
1770
1771 \begin{code}
1772 -- Free variables of a type, retaining repetitions, and expanding synonyms
1773 fvType :: Type -> [TyVar]
1774 fvType ty | Just exp_ty <- tcView ty = fvType exp_ty
1775 fvType (TyVarTy tv)        = [tv]
1776 fvType (TyConApp _ tys)    = fvTypes tys
1777 fvType (LitTy {})          = []
1778 fvType (FunTy arg res)     = fvType arg ++ fvType res
1779 fvType (AppTy fun arg)     = fvType fun ++ fvType arg
1780 fvType (ForAllTy tyvar ty) = filter (/= tyvar) (fvType ty)
1781
1782 fvTypes :: [Type] -> [TyVar]
1783 fvTypes tys                = concat (map fvType tys)
1784
1785 sizeType :: Type -> Int
1786 -- Size of a type: the number of variables and constructors
1787 sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty
1788 sizeType (TyVarTy {})      = 1
1789 sizeType (TyConApp _ tys)  = sizeTypes tys + 1
1790 sizeType (LitTy {})        = 1
1791 sizeType (FunTy arg res)   = sizeType arg + sizeType res + 1
1792 sizeType (AppTy fun arg)   = sizeType fun + sizeType arg
1793 sizeType (ForAllTy _ ty)   = sizeType ty
1794
1795 sizeTypes :: [Type] -> Int
1796 -- IA0_NOTE: Avoid kinds.
1797 sizeTypes xs = sum (map sizeType tys)
1798   where tys = filter (not . isKind) xs
1799
1800 -- Size of a predicate
1801 --
1802 -- We are considering whether *class* constraints terminate
1803 -- Once we get into an implicit parameter or equality we
1804 -- can't get back to a class constraint, so it's safe
1805 -- to say "size 0".  See Trac #4200.
1806 sizePred :: PredType -> Int
1807 sizePred ty = go (classifyPredType ty)
1808   where
1809     go (ClassPred _ tys') = sizeTypes tys'
1810     go (IPPred {})        = 0
1811     go (EqPred {})        = 0
1812     go (TuplePred ts)     = sum (map (go . classifyPredType) ts)
1813     go (IrredPred ty)     = sizeType ty
1814 \end{code}
1815
1816 Note [Paterson conditions on PredTypes]
1817 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1818 We are considering whether *class* constraints terminate
1819 (see Note [Paterson conditions]). Precisely, the Paterson conditions
1820 would have us check that "the constraint has fewer constructors and variables
1821 (taken together and counting repetitions) than the head.".
1822
1823 However, we can be a bit more refined by looking at which kind of constraint
1824 this actually is. There are two main tricks:
1825
1826  1. It seems like it should be OK not to count the tuple type constructor
1827     for a PredType like (Show a, Eq a) :: Constraint, since we don't
1828     count the "implicit" tuple in the ThetaType itself.
1829
1830     In fact, the Paterson test just checks *each component* of the top level
1831     ThetaType against the size bound, one at a time. By analogy, it should be
1832     OK to return the size of the *largest* tuple component as the size of the
1833     whole tuple.
1834
1835  2. Once we get into an implicit parameter or equality we
1836     can't get back to a class constraint, so it's safe
1837     to say "size 0".  See Trac #4200.
1838
1839 NB: we don't want to detect PredTypes in sizeType (and then call 
1840 sizePred on them), or we might get an infinite loop if that PredType
1841 is irreducible. See Trac #5581.