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