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