Comments, and remove export of checkAmbiguity
[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 -w #-}
13 -- The above warning supression flag is a temporary kludge.
14 -- While working on this module you are encouraged to remove it and fix
15 -- any warnings in the module. See
16 --     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
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   newKindVar, newKindVars, 
28   lookupTcTyVar, LookupTyVarResult(..),
29   newMetaTyVar, readMetaTyVar, writeMetaTyVar, 
30
31   --------------------------------
32   -- Boxy type variables
33   newBoxyTyVar, newBoxyTyVars, newBoxyTyVarTys, readFilledBox, 
34
35   --------------------------------
36   -- Creating new coercion variables
37   newCoVars,
38
39   --------------------------------
40   -- Instantiation
41   tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxyTyVar,
42   tcInstSigTyVars, zonkSigTyVar,
43   tcInstSkolTyVar, tcInstSkolTyVars, tcInstSkolType, 
44   tcSkolSigType, tcSkolSigTyVars,
45
46   --------------------------------
47   -- Checking type validity
48   Rank, UserTypeCtxt(..), checkValidType, 
49   SourceTyCtxt(..), checkValidTheta, checkFreeness,
50   checkValidInstHead, checkValidInstance, 
51   checkInstTermination, checkValidTypeInst, checkTyFamFreeness,
52   validDerivPred, arityErr, 
53
54   --------------------------------
55   -- Zonking
56   zonkType, zonkTcPredType, 
57   zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, 
58   zonkQuantifiedTyVar, zonkQuantifiedTyVars,
59   zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
60   zonkTcKindToKind, zonkTcKind, zonkTopTyVar,
61
62   readKindVar, writeKindVar
63   ) where
64
65 #include "HsVersions.h"
66
67 -- friends:
68 import TypeRep
69 import TcType
70 import Type
71 import Coercion
72 import Class
73 import TyCon
74 import Var
75
76 -- others:
77 import TcRnMonad          -- TcType, amongst others
78 import FunDeps
79 import Name
80 import VarSet
81 import ErrUtils
82 import DynFlags
83 import Util
84 import Maybes
85 import ListSetOps
86 import UniqSupply
87 import SrcLoc
88 import Outputable
89
90 import Control.Monad    ( when, unless )
91 import Data.List        ( (\\) )
92 \end{code}
93
94
95 %************************************************************************
96 %*                                                                      *
97         Instantiation in general
98 %*                                                                      *
99 %************************************************************************
100
101 \begin{code}
102 tcInstType :: ([TyVar] -> TcM [TcTyVar])                -- How to instantiate the type variables
103            -> TcType                                    -- Type to instantiate
104            -> TcM ([TcTyVar], TcThetaType, TcType)      -- Result
105 tcInstType inst_tyvars ty
106   = case tcSplitForAllTys ty of
107         ([],     rho) -> let    -- There may be overloading despite no type variables;
108                                 --      (?x :: Int) => Int -> Int
109                            (theta, tau) = tcSplitPhiTy rho
110                          in
111                          return ([], theta, tau)
112
113         (tyvars, rho) -> do { tyvars' <- inst_tyvars tyvars
114
115                             ; let  tenv = zipTopTvSubst tyvars (mkTyVarTys tyvars')
116                                 -- Either the tyvars are freshly made, by inst_tyvars,
117                                 -- or (in the call from tcSkolSigType) any nested foralls
118                                 -- have different binders.  Either way, zipTopTvSubst is ok
119
120                             ; let  (theta, tau) = tcSplitPhiTy (substTy tenv rho)
121                             ; return (tyvars', theta, tau) }
122 \end{code}
123
124
125 %************************************************************************
126 %*                                                                      *
127         Kind variables
128 %*                                                                      *
129 %************************************************************************
130
131 \begin{code}
132 newCoVars :: [(TcType,TcType)] -> TcM [CoVar]
133 newCoVars spec
134   = do  { us <- newUniqueSupply 
135         ; return [ mkCoVar (mkSysTvName uniq FSLIT("co"))
136                            (mkCoKind ty1 ty2)
137                  | ((ty1,ty2), uniq) <- spec `zip` uniqsFromSupply us] }
138
139 newKindVar :: TcM TcKind
140 newKindVar = do { uniq <- newUnique
141                 ; ref <- newMutVar Flexi
142                 ; return (mkTyVarTy (mkKindVar uniq ref)) }
143
144 newKindVars :: Int -> TcM [TcKind]
145 newKindVars n = mappM (\ _ -> newKindVar) (nOfThem n ())
146 \end{code}
147
148
149 %************************************************************************
150 %*                                                                      *
151         SkolemTvs (immutable)
152 %*                                                                      *
153 %************************************************************************
154
155 \begin{code}
156 mkSkolTyVar :: Name -> Kind -> SkolemInfo -> TcTyVar
157 mkSkolTyVar name kind info = mkTcTyVar name kind (SkolemTv info)
158
159 tcSkolSigType :: SkolemInfo -> Type -> TcM ([TcTyVar], TcThetaType, TcType)
160 -- Instantiate a type signature with skolem constants, but 
161 -- do *not* give them fresh names, because we want the name to
162 -- be in the type environment -- it is lexically scoped.
163 tcSkolSigType info ty = tcInstType (\tvs -> return (tcSkolSigTyVars info tvs)) ty
164
165 tcSkolSigTyVars :: SkolemInfo -> [TyVar] -> [TcTyVar]
166 -- Make skolem constants, but do *not* give them new names, as above
167 tcSkolSigTyVars info tyvars = [ mkSkolTyVar (tyVarName tv) (tyVarKind tv) info
168                               | tv <- tyvars ]
169
170 tcInstSkolTyVar :: SkolemInfo -> Maybe SrcSpan -> TyVar -> TcM TcTyVar
171 -- Instantiate the tyvar, using 
172 --      * the occ-name and kind of the supplied tyvar, 
173 --      * the unique from the monad,
174 --      * the location either from the tyvar (mb_loc = Nothing)
175 --        or from mb_loc (Just loc)
176 tcInstSkolTyVar info mb_loc tyvar
177   = do  { uniq <- newUnique
178         ; let old_name = tyVarName tyvar
179               kind     = tyVarKind tyvar
180               loc      = mb_loc `orElse` getSrcSpan old_name
181               new_name = mkInternalName uniq (nameOccName old_name) loc
182         ; return (mkSkolTyVar new_name kind info) }
183
184 tcInstSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
185 -- Get the location from the monad
186 tcInstSkolTyVars info tyvars 
187   = do  { span <- getSrcSpanM
188         ; mapM (tcInstSkolTyVar info (Just span)) tyvars }
189
190 tcInstSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
191 -- Instantiate a type with fresh skolem constants
192 -- Binding location comes from the monad
193 tcInstSkolType info ty = tcInstType (tcInstSkolTyVars info) ty
194 \end{code}
195
196
197 %************************************************************************
198 %*                                                                      *
199         MetaTvs (meta type variables; mutable)
200 %*                                                                      *
201 %************************************************************************
202
203 \begin{code}
204 newMetaTyVar :: BoxInfo -> Kind -> TcM TcTyVar
205 -- Make a new meta tyvar out of thin air
206 newMetaTyVar box_info kind
207   = do  { uniq <- newUnique
208         ; ref <- newMutVar Flexi
209         ; let name = mkSysTvName uniq fs 
210               fs = case box_info of
211                         BoxTv   -> FSLIT("t")
212                         TauTv   -> FSLIT("t")
213                         SigTv _ -> FSLIT("a")
214                 -- We give BoxTv and TauTv the same string, because
215                 -- otherwise we get user-visible differences in error
216                 -- messages, which are confusing.  If you want to see
217                 -- the box_info of each tyvar, use -dppr-debug
218         ; return (mkTcTyVar name kind (MetaTv box_info ref)) }
219
220 instMetaTyVar :: BoxInfo -> TyVar -> TcM TcTyVar
221 -- Make a new meta tyvar whose Name and Kind 
222 -- come from an existing TyVar
223 instMetaTyVar box_info tyvar
224   = do  { uniq <- newUnique
225         ; ref <- newMutVar Flexi
226         ; let name = setNameUnique (tyVarName tyvar) uniq
227               kind = tyVarKind tyvar
228         ; return (mkTcTyVar name kind (MetaTv box_info ref)) }
229
230 readMetaTyVar :: TyVar -> TcM MetaDetails
231 readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
232                       readMutVar (metaTvRef tyvar)
233
234 writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
235 #ifndef DEBUG
236 writeMetaTyVar tyvar ty = writeMutVar (metaTvRef tyvar) (Indirect ty)
237 #else
238 writeMetaTyVar tyvar ty
239   | not (isMetaTyVar tyvar)
240   = pprTrace "writeMetaTyVar" (ppr tyvar) $
241     returnM ()
242
243   | otherwise
244   = ASSERT( isMetaTyVar tyvar )
245     -- TOM: It should also work for coercions
246     -- ASSERT2( k2 `isSubKind` k1, (ppr tyvar <+> ppr k1) $$ (ppr ty <+> ppr k2) )
247     do  { ASSERTM2( do { details <- readMetaTyVar tyvar; return (isFlexi details) }, ppr tyvar )
248         ; writeMutVar (metaTvRef tyvar) (Indirect ty) }
249   where
250     k1 = tyVarKind tyvar
251     k2 = typeKind ty
252 #endif
253 \end{code}
254
255
256 %************************************************************************
257 %*                                                                      *
258         MetaTvs: TauTvs
259 %*                                                                      *
260 %************************************************************************
261
262 \begin{code}
263 newFlexiTyVar :: Kind -> TcM TcTyVar
264 newFlexiTyVar kind = newMetaTyVar TauTv kind
265
266 newFlexiTyVarTy  :: Kind -> TcM TcType
267 newFlexiTyVarTy kind
268   = newFlexiTyVar kind  `thenM` \ tc_tyvar ->
269     returnM (TyVarTy tc_tyvar)
270
271 newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
272 newFlexiTyVarTys n kind = mappM newFlexiTyVarTy (nOfThem n kind)
273
274 tcInstTyVar :: TyVar -> TcM TcTyVar
275 -- Instantiate with a META type variable
276 tcInstTyVar tyvar = instMetaTyVar TauTv tyvar
277
278 tcInstTyVars :: [TyVar] -> TcM ([TcTyVar], [TcType], TvSubst)
279 -- Instantiate with META type variables
280 tcInstTyVars tyvars
281   = do  { tc_tvs <- mapM tcInstTyVar tyvars
282         ; let tys = mkTyVarTys tc_tvs
283         ; returnM (tc_tvs, tys, zipTopTvSubst tyvars tys) }
284                 -- Since the tyvars are freshly made,
285                 -- they cannot possibly be captured by
286                 -- any existing for-alls.  Hence zipTopTvSubst
287 \end{code}
288
289
290 %************************************************************************
291 %*                                                                      *
292         MetaTvs: SigTvs
293 %*                                                                      *
294 %************************************************************************
295
296 \begin{code}
297 tcInstSigTyVars :: Bool -> SkolemInfo -> [TyVar] -> TcM [TcTyVar]
298 -- Instantiate with skolems or meta SigTvs; depending on use_skols
299 -- Always take location info from the supplied tyvars
300 tcInstSigTyVars use_skols skol_info tyvars 
301   | use_skols
302   = mapM (tcInstSkolTyVar skol_info Nothing) tyvars
303
304   | otherwise
305   = mapM (instMetaTyVar (SigTv skol_info)) tyvars
306
307 zonkSigTyVar :: TcTyVar -> TcM TcTyVar
308 zonkSigTyVar sig_tv 
309   | isSkolemTyVar sig_tv 
310   = return sig_tv       -- Happens in the call in TcBinds.checkDistinctTyVars
311   | otherwise
312   = ASSERT( isSigTyVar sig_tv )
313     do { ty <- zonkTcTyVar sig_tv
314        ; return (tcGetTyVar "zonkSigTyVar" ty) }
315         -- 'ty' is bound to be a type variable, because SigTvs
316         -- can only be unified with type variables
317 \end{code}
318
319
320 %************************************************************************
321 %*                                                                      *
322         MetaTvs: BoxTvs
323 %*                                                                      *
324 %************************************************************************
325
326 \begin{code}
327 newBoxyTyVar :: Kind -> TcM BoxyTyVar
328 newBoxyTyVar kind = newMetaTyVar BoxTv kind
329
330 newBoxyTyVars :: [Kind] -> TcM [BoxyTyVar]
331 newBoxyTyVars kinds = mapM newBoxyTyVar kinds
332
333 newBoxyTyVarTys :: [Kind] -> TcM [BoxyType]
334 newBoxyTyVarTys kinds = do { tvs <- mapM newBoxyTyVar kinds; return (mkTyVarTys tvs) }
335
336 readFilledBox :: BoxyTyVar -> TcM TcType
337 -- Read the contents of the box, which should be filled in by now
338 readFilledBox box_tv = ASSERT( isBoxyTyVar box_tv )
339                        do { cts <- readMetaTyVar box_tv
340                           ; case cts of
341                                 Flexi -> pprPanic "readFilledBox" (ppr box_tv)
342                                 Indirect ty -> return ty }
343
344 tcInstBoxyTyVar :: TyVar -> TcM BoxyTyVar
345 -- Instantiate with a BOXY type variable
346 tcInstBoxyTyVar tyvar = instMetaTyVar BoxTv tyvar
347 \end{code}
348
349
350 %************************************************************************
351 %*                                                                      *
352 \subsection{Putting and getting  mutable type variables}
353 %*                                                                      *
354 %************************************************************************
355
356 But it's more fun to short out indirections on the way: If this
357 version returns a TyVar, then that TyVar is unbound.  If it returns
358 any other type, then there might be bound TyVars embedded inside it.
359
360 We return Nothing iff the original box was unbound.
361
362 \begin{code}
363 data LookupTyVarResult  -- The result of a lookupTcTyVar call
364   = DoneTv TcTyVarDetails       -- SkolemTv or virgin MetaTv
365   | IndirectTv TcType
366
367 lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult
368 lookupTcTyVar tyvar 
369   = ASSERT2( isTcTyVar tyvar, ppr tyvar )
370     case details of
371       SkolemTv _   -> return (DoneTv details)
372       MetaTv _ ref -> do { meta_details <- readMutVar ref
373                          ; case meta_details of
374                             Indirect ty -> return (IndirectTv ty)
375                             Flexi -> return (DoneTv details) }
376   where
377     details =  tcTyVarDetails tyvar
378
379 {- 
380 -- gaw 2004 We aren't shorting anything out anymore, at least for now
381 getTcTyVar tyvar
382   | not (isTcTyVar tyvar)
383   = pprTrace "getTcTyVar" (ppr tyvar) $
384     returnM (Just (mkTyVarTy tyvar))
385
386   | otherwise
387   = ASSERT2( isTcTyVar tyvar, ppr tyvar )
388     readMetaTyVar tyvar                         `thenM` \ maybe_ty ->
389     case maybe_ty of
390         Just ty -> short_out ty                         `thenM` \ ty' ->
391                    writeMetaTyVar tyvar (Just ty')      `thenM_`
392                    returnM (Just ty')
393
394         Nothing    -> returnM Nothing
395
396 short_out :: TcType -> TcM TcType
397 short_out ty@(TyVarTy tyvar)
398   | not (isTcTyVar tyvar)
399   = returnM ty
400
401   | otherwise
402   = readMetaTyVar tyvar `thenM` \ maybe_ty ->
403     case maybe_ty of
404         Just ty' -> short_out ty'                       `thenM` \ ty' ->
405                     writeMetaTyVar tyvar (Just ty')     `thenM_`
406                     returnM ty'
407
408         other    -> returnM ty
409
410 short_out other_ty = returnM other_ty
411 -}
412 \end{code}
413
414
415 %************************************************************************
416 %*                                                                      *
417 \subsection{Zonking -- the exernal interfaces}
418 %*                                                                      *
419 %************************************************************************
420
421 -----------------  Type variables
422
423 \begin{code}
424 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
425 zonkTcTyVars tyvars = mappM zonkTcTyVar tyvars
426
427 zonkTcTyVarsAndFV :: [TcTyVar] -> TcM TcTyVarSet
428 zonkTcTyVarsAndFV tyvars = mappM zonkTcTyVar tyvars     `thenM` \ tys ->
429                            returnM (tyVarsOfTypes tys)
430
431 zonkTcTyVar :: TcTyVar -> TcM TcType
432 zonkTcTyVar tyvar = ASSERT2( isTcTyVar tyvar, ppr tyvar)
433                     zonk_tc_tyvar (\ tv -> returnM (TyVarTy tv)) tyvar
434 \end{code}
435
436 -----------------  Types
437
438 \begin{code}
439 zonkTcType :: TcType -> TcM TcType
440 zonkTcType ty = zonkType (\ tv -> returnM (TyVarTy tv)) ty
441
442 zonkTcTypes :: [TcType] -> TcM [TcType]
443 zonkTcTypes tys = mappM zonkTcType tys
444
445 zonkTcClassConstraints cts = mappM zonk cts
446     where zonk (clas, tys)
447             = zonkTcTypes tys   `thenM` \ new_tys ->
448               returnM (clas, new_tys)
449
450 zonkTcThetaType :: TcThetaType -> TcM TcThetaType
451 zonkTcThetaType theta = mappM zonkTcPredType theta
452
453 zonkTcPredType :: TcPredType -> TcM TcPredType
454 zonkTcPredType (ClassP c ts)
455   = zonkTcTypes ts      `thenM` \ new_ts ->
456     returnM (ClassP c new_ts)
457 zonkTcPredType (IParam n t)
458   = zonkTcType t        `thenM` \ new_t ->
459     returnM (IParam n new_t)
460 zonkTcPredType (EqPred t1 t2)
461   = zonkTcType t1       `thenM` \ new_t1 ->
462     zonkTcType t2       `thenM` \ new_t2 ->
463     returnM (EqPred new_t1 new_t2)
464 \end{code}
465
466 -------------------  These ...ToType, ...ToKind versions
467                      are used at the end of type checking
468
469 \begin{code}
470 zonkTopTyVar :: TcTyVar -> TcM TcTyVar
471 -- zonkTopTyVar is used, at the top level, on any un-instantiated meta type variables
472 -- to default the kind of ? and ?? etc to *.  This is important to ensure that
473 -- instance declarations match.  For example consider
474 --      instance Show (a->b)
475 --      foo x = show (\_ -> True)
476 -- Then we'll get a constraint (Show (p ->q)) where p has argTypeKind (printed ??), 
477 -- and that won't match the typeKind (*) in the instance decl.
478 --
479 -- Because we are at top level, no further constraints are going to affect these
480 -- type variables, so it's time to do it by hand.  However we aren't ready
481 -- to default them fully to () or whatever, because the type-class defaulting
482 -- rules have yet to run.
483
484 zonkTopTyVar tv
485   | k `eqKind` default_k = return tv
486   | otherwise
487   = do  { tv' <- newFlexiTyVar default_k
488         ; writeMetaTyVar tv (mkTyVarTy tv') 
489         ; return tv' }
490   where
491     k = tyVarKind tv
492     default_k = defaultKind k
493
494 zonkQuantifiedTyVars :: [TcTyVar] -> TcM [TyVar]
495 zonkQuantifiedTyVars = mappM zonkQuantifiedTyVar
496
497 zonkQuantifiedTyVar :: TcTyVar -> TcM TyVar
498 -- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it.
499 --
500 -- The quantified type variables often include meta type variables
501 -- we want to freeze them into ordinary type variables, and
502 -- default their kind (e.g. from OpenTypeKind to TypeKind)
503 --                      -- see notes with Kind.defaultKind
504 -- The meta tyvar is updated to point to the new regular TyVar.  Now any 
505 -- bound occurences of the original type variable will get zonked to 
506 -- the immutable version.
507 --
508 -- We leave skolem TyVars alone; they are immutable.
509 zonkQuantifiedTyVar tv
510   | ASSERT( isTcTyVar tv ) 
511     isSkolemTyVar tv = return tv
512         -- It might be a skolem type variable, 
513         -- for example from a user type signature
514
515   | otherwise   -- It's a meta-type-variable
516   = do  { details <- readMetaTyVar tv
517
518         -- Create the new, frozen, regular type variable
519         ; let final_kind = defaultKind (tyVarKind tv)
520               final_tv   = mkTyVar (tyVarName tv) final_kind
521
522         -- Bind the meta tyvar to the new tyvar
523         ; case details of
524             Indirect ty -> WARN( True, ppr tv $$ ppr ty ) 
525                            return ()
526                 -- [Sept 04] I don't think this should happen
527                 -- See note [Silly Type Synonym]
528
529             Flexi -> writeMetaTyVar tv (mkTyVarTy final_tv)
530
531         -- Return the new tyvar
532         ; return final_tv }
533 \end{code}
534
535 [Silly Type Synonyms]
536
537 Consider this:
538         type C u a = u  -- Note 'a' unused
539
540         foo :: (forall a. C u a -> C u a) -> u
541         foo x = ...
542
543         bar :: Num u => u
544         bar = foo (\t -> t + t)
545
546 * From the (\t -> t+t) we get type  {Num d} =>  d -> d
547   where d is fresh.
548
549 * Now unify with type of foo's arg, and we get:
550         {Num (C d a)} =>  C d a -> C d a
551   where a is fresh.
552
553 * Now abstract over the 'a', but float out the Num (C d a) constraint
554   because it does not 'really' mention a.  (see exactTyVarsOfType)
555   The arg to foo becomes
556         /\a -> \t -> t+t
557
558 * So we get a dict binding for Num (C d a), which is zonked to give
559         a = ()
560   [Note Sept 04: now that we are zonking quantified type variables
561   on construction, the 'a' will be frozen as a regular tyvar on
562   quantification, so the floated dict will still have type (C d a).
563   Which renders this whole note moot; happily!]
564
565 * Then the /\a abstraction has a zonked 'a' in it.
566
567 All very silly.   I think its harmless to ignore the problem.  We'll end up with
568 a /\a in the final result but all the occurrences of a will be zonked to ()
569
570
571 %************************************************************************
572 %*                                                                      *
573 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
574 %*                                                                      *
575 %*              For internal use only!                                  *
576 %*                                                                      *
577 %************************************************************************
578
579 \begin{code}
580 -- For unbound, mutable tyvars, zonkType uses the function given to it
581 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
582 --      type variable and zonks the kind too
583
584 zonkType :: (TcTyVar -> TcM Type)       -- What to do with unbound mutable type variables
585                                         -- see zonkTcType, and zonkTcTypeToType
586          -> TcType
587          -> TcM Type
588 zonkType unbound_var_fn ty
589   = go ty
590   where
591     go (NoteTy _ ty2)    = go ty2       -- Discard free-tyvar annotations
592                          
593     go (TyConApp tc tys) = mappM go tys `thenM` \ tys' ->
594                            returnM (TyConApp tc tys')
595                             
596     go (PredTy p)        = go_pred p            `thenM` \ p' ->
597                            returnM (PredTy p')
598                          
599     go (FunTy arg res)   = go arg               `thenM` \ arg' ->
600                            go res               `thenM` \ res' ->
601                            returnM (FunTy arg' res')
602                          
603     go (AppTy fun arg)   = go fun               `thenM` \ fun' ->
604                            go arg               `thenM` \ arg' ->
605                            returnM (mkAppTy fun' arg')
606                 -- NB the mkAppTy; we might have instantiated a
607                 -- type variable to a type constructor, so we need
608                 -- to pull the TyConApp to the top.
609
610         -- The two interesting cases!
611     go (TyVarTy tyvar) | isTcTyVar tyvar = zonk_tc_tyvar unbound_var_fn tyvar
612                        | otherwise       = return (TyVarTy tyvar)
613                 -- Ordinary (non Tc) tyvars occur inside quantified types
614
615     go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar )
616                              go ty              `thenM` \ ty' ->
617                              returnM (ForAllTy tyvar ty')
618
619     go_pred (ClassP c tys)   = mappM go tys     `thenM` \ tys' ->
620                                returnM (ClassP c tys')
621     go_pred (IParam n ty)    = go ty            `thenM` \ ty' ->
622                                returnM (IParam n ty')
623     go_pred (EqPred ty1 ty2) = go ty1           `thenM` \ ty1' ->
624                                go ty2           `thenM` \ ty2' ->
625                                returnM (EqPred ty1' ty2')
626
627 zonk_tc_tyvar :: (TcTyVar -> TcM Type)          -- What to do for an unbound mutable variable
628               -> TcTyVar -> TcM TcType
629 zonk_tc_tyvar unbound_var_fn tyvar 
630   | not (isMetaTyVar tyvar)     -- Skolems
631   = returnM (TyVarTy tyvar)
632
633   | otherwise                   -- Mutables
634   = do  { cts <- readMetaTyVar tyvar
635         ; case cts of
636             Flexi       -> unbound_var_fn tyvar    -- Unbound meta type variable
637             Indirect ty -> zonkType unbound_var_fn ty  }
638 \end{code}
639
640
641
642 %************************************************************************
643 %*                                                                      *
644                         Zonking kinds
645 %*                                                                      *
646 %************************************************************************
647
648 \begin{code}
649 readKindVar  :: KindVar -> TcM (MetaDetails)
650 writeKindVar :: KindVar -> TcKind -> TcM ()
651 readKindVar  kv = readMutVar (kindVarRef kv)
652 writeKindVar kv val = writeMutVar (kindVarRef kv) (Indirect val)
653
654 -------------
655 zonkTcKind :: TcKind -> TcM TcKind
656 zonkTcKind k = zonkTcType k
657
658 -------------
659 zonkTcKindToKind :: TcKind -> TcM Kind
660 -- When zonking a TcKind to a kind, we need to instantiate kind variables,
661 -- Haskell specifies that * is to be used, so we follow that.
662 zonkTcKindToKind k = zonkType (\ _ -> return liftedTypeKind) k
663 \end{code}
664                         
665 %************************************************************************
666 %*                                                                      *
667 \subsection{Checking a user type}
668 %*                                                                      *
669 %************************************************************************
670
671 When dealing with a user-written type, we first translate it from an HsType
672 to a Type, performing kind checking, and then check various things that should 
673 be true about it.  We don't want to perform these checks at the same time
674 as the initial translation because (a) they are unnecessary for interface-file
675 types and (b) when checking a mutually recursive group of type and class decls,
676 we can't "look" at the tycons/classes yet.  Also, the checks are are rather
677 diverse, and used to really mess up the other code.
678
679 One thing we check for is 'rank'.  
680
681         Rank 0:         monotypes (no foralls)
682         Rank 1:         foralls at the front only, Rank 0 inside
683         Rank 2:         foralls at the front, Rank 1 on left of fn arrow,
684
685         basic ::= tyvar | T basic ... basic
686
687         r2  ::= forall tvs. cxt => r2a
688         r2a ::= r1 -> r2a | basic
689         r1  ::= forall tvs. cxt => r0
690         r0  ::= r0 -> r0 | basic
691         
692 Another thing is to check that type synonyms are saturated. 
693 This might not necessarily show up in kind checking.
694         type A i = i
695         data T k = MkT (k Int)
696         f :: T A        -- BAD!
697
698         
699 \begin{code}
700 checkValidType :: UserTypeCtxt -> Type -> TcM ()
701 -- Checks that the type is valid for the given context
702 checkValidType ctxt ty
703   = traceTc (text "checkValidType" <+> ppr ty)  `thenM_`
704     doptM Opt_UnboxedTuples `thenM` \ unboxed ->
705     doptM Opt_Rank2Types        `thenM` \ rank2 ->
706     doptM Opt_RankNTypes        `thenM` \ rankn ->
707     doptM Opt_PolymorphicComponents     `thenM` \ polycomp ->
708     let 
709         rank | rankn = Arbitrary
710              | rank2 = Rank 2
711              | otherwise
712              = case ctxt of     -- Haskell 98
713                  GenPatCtxt     -> Rank 0
714                  LamPatSigCtxt  -> Rank 0
715                  BindPatSigCtxt -> Rank 0
716                  DefaultDeclCtxt-> Rank 0
717                  ResSigCtxt     -> Rank 0
718                  TySynCtxt _    -> Rank 0
719                  ExprSigCtxt    -> Rank 1
720                  FunSigCtxt _   -> Rank 1
721                  ConArgCtxt _   -> if polycomp
722                            then Rank 2
723                                 -- We are given the type of the entire
724                                 -- constructor, hence rank 1
725                            else Rank 1
726                  ForSigCtxt _   -> Rank 1
727                  SpecInstCtxt   -> Rank 1
728
729         actual_kind = typeKind ty
730
731         kind_ok = case ctxt of
732                         TySynCtxt _  -> True    -- Any kind will do
733                         ResSigCtxt   -> isSubOpenTypeKind        actual_kind
734                         ExprSigCtxt  -> isSubOpenTypeKind        actual_kind
735                         GenPatCtxt   -> isLiftedTypeKind actual_kind
736                         ForSigCtxt _ -> isLiftedTypeKind actual_kind
737                         other        -> isSubArgTypeKind    actual_kind
738         
739         ubx_tup = case ctxt of
740                       TySynCtxt _ | unboxed -> UT_Ok
741                       ExprSigCtxt | unboxed -> UT_Ok
742                       _                     -> UT_NotOk
743     in
744         -- Check that the thing has kind Type, and is lifted if necessary
745     checkTc kind_ok (kindErr actual_kind)       `thenM_`
746
747         -- Check the internal validity of the type itself
748     check_poly_type rank ubx_tup ty             `thenM_`
749
750     traceTc (text "checkValidType done" <+> ppr ty)
751 \end{code}
752
753
754 \begin{code}
755 data Rank = Rank Int | Arbitrary
756
757 decRank :: Rank -> Rank
758 decRank Arbitrary = Arbitrary
759 decRank (Rank n)  = Rank (n-1)
760
761 ----------------------------------------
762 data UbxTupFlag = UT_Ok | UT_NotOk
763         -- The "Ok" version means "ok if -fglasgow-exts is on"
764
765 ----------------------------------------
766 check_poly_type :: Rank -> UbxTupFlag -> Type -> TcM ()
767 check_poly_type (Rank 0) ubx_tup ty 
768   = check_tau_type (Rank 0) ubx_tup ty
769
770 check_poly_type rank ubx_tup ty 
771   | null tvs && null theta
772   = check_tau_type rank ubx_tup ty
773   | otherwise
774   = do  { check_valid_theta SigmaCtxt theta
775         ; check_poly_type rank ubx_tup tau      -- Allow foralls to right of arrow
776         ; checkFreeness tvs theta
777         ; checkAmbiguity tvs theta (tyVarsOfType tau) }
778   where
779     (tvs, theta, tau) = tcSplitSigmaTy ty
780    
781 ----------------------------------------
782 check_arg_type :: Type -> TcM ()
783 -- The sort of type that can instantiate a type variable,
784 -- or be the argument of a type constructor.
785 -- Not an unboxed tuple, but now *can* be a forall (since impredicativity)
786 -- Other unboxed types are very occasionally allowed as type
787 -- arguments depending on the kind of the type constructor
788 -- 
789 -- For example, we want to reject things like:
790 --
791 --      instance Ord a => Ord (forall s. T s a)
792 -- and
793 --      g :: T s (forall b.b)
794 --
795 -- NB: unboxed tuples can have polymorphic or unboxed args.
796 --     This happens in the workers for functions returning
797 --     product types with polymorphic components.
798 --     But not in user code.
799 -- Anyway, they are dealt with by a special case in check_tau_type
800
801 check_arg_type ty 
802   = check_poly_type Arbitrary UT_NotOk ty       `thenM_` 
803     checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
804
805 ----------------------------------------
806 check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
807 -- Rank is allowed rank for function args
808 -- No foralls otherwise
809
810 check_tau_type rank ubx_tup ty@(ForAllTy _ _)       = failWithTc (forAllTyErr ty)
811 check_tau_type rank ubx_tup ty@(FunTy (PredTy _) _) = failWithTc (forAllTyErr ty)
812         -- Reject e.g. (Maybe (?x::Int => Int)), with a decent error message
813
814 -- Naked PredTys don't usually show up, but they can as a result of
815 --      {-# SPECIALISE instance Ord Char #-}
816 -- The Right Thing would be to fix the way that SPECIALISE instance pragmas
817 -- are handled, but the quick thing is just to permit PredTys here.
818 check_tau_type rank ubx_tup (PredTy sty) = getDOpts             `thenM` \ dflags ->
819                                            check_pred_ty dflags TypeCtxt sty
820
821 check_tau_type rank ubx_tup (TyVarTy _)       = returnM ()
822 check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
823   = check_poly_type (decRank rank) UT_NotOk arg_ty      `thenM_`
824     check_poly_type rank           UT_Ok    res_ty
825
826 check_tau_type rank ubx_tup (AppTy ty1 ty2)
827   = check_arg_type ty1 `thenM_` check_arg_type ty2
828
829 check_tau_type rank ubx_tup (NoteTy other_note ty)
830   = check_tau_type rank ubx_tup ty
831
832 check_tau_type rank ubx_tup ty@(TyConApp tc tys)
833   | isSynTyCon tc       
834   = do  {       -- It's OK to have an *over-applied* type synonym
835                 --      data Tree a b = ...
836                 --      type Foo a = Tree [a]
837                 --      f :: Foo a b -> ...
838         ; case tcView ty of
839              Just ty' -> check_tau_type rank ubx_tup ty' -- Check expansion
840              Nothing -> unless (isOpenTyCon tc           -- No expansion if open
841                                 && tyConArity tc <= length tys) $
842                           failWithTc arity_msg
843
844         ; ok <- doptM Opt_PartiallyAppliedClosedTypeSynonyms
845         ; if ok && not (isOpenTyCon tc) then
846         -- Don't check the type arguments of *closed* synonyms.
847         -- This allows us to instantiate a synonym defn with a 
848         -- for-all type, or with a partially-applied type synonym.
849         --      e.g.   type T a b = a
850         --             type S m   = m ()
851         --             f :: S (T Int)
852         -- Here, T is partially applied, so it's illegal in H98.
853         -- But if you expand S first, then T we get just 
854         --             f :: Int
855         -- which is fine.
856                 returnM ()
857           else
858                 -- For H98, do check the type args
859                 mappM_ check_arg_type tys
860         }
861     
862   | isUnboxedTupleTyCon tc
863   = doptM Opt_UnboxedTuples `thenM` \ ub_tuples_allowed ->
864     checkTc (ubx_tup_ok ub_tuples_allowed) ubx_tup_msg  `thenM_`
865     mappM_ (check_tau_type (Rank 0) UT_Ok) tys  
866                 -- Args are allowed to be unlifted, or
867                 -- more unboxed tuples, so can't use check_arg_ty
868
869   | otherwise
870   = mappM_ check_arg_type tys
871
872   where
873     ubx_tup_ok ub_tuples_allowed = case ubx_tup of { UT_Ok -> ub_tuples_allowed; other -> False }
874
875     n_args    = length tys
876     tc_arity  = tyConArity tc
877
878     arity_msg   = arityErr "Type synonym" (tyConName tc) tc_arity n_args
879     ubx_tup_msg = ubxArgTyErr ty
880
881 ----------------------------------------
882 forAllTyErr     ty = ptext SLIT("Illegal polymorphic or qualified type:") <+> ppr ty
883 unliftedArgErr  ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr ty
884 ubxArgTyErr     ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr ty
885 kindErr kind       = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
886 \end{code}
887
888
889
890 %************************************************************************
891 %*                                                                      *
892 \subsection{Checking a theta or source type}
893 %*                                                                      *
894 %************************************************************************
895
896 \begin{code}
897 -- Enumerate the contexts in which a "source type", <S>, can occur
898 --      Eq a 
899 -- or   ?x::Int
900 -- or   r <: {x::Int}
901 -- or   (N a) where N is a newtype
902
903 data SourceTyCtxt
904   = ClassSCCtxt Name    -- Superclasses of clas
905                         --      class <S> => C a where ...
906   | SigmaCtxt           -- Theta part of a normal for-all type
907                         --      f :: <S> => a -> a
908   | DataTyCtxt Name     -- Theta part of a data decl
909                         --      data <S> => T a = MkT a
910   | TypeCtxt            -- Source type in an ordinary type
911                         --      f :: N a -> N a
912   | InstThetaCtxt       -- Context of an instance decl
913                         --      instance <S> => C [a] where ...
914                 
915 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
916 pprSourceTyCtxt SigmaCtxt       = ptext SLIT("the context of a polymorphic type")
917 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
918 pprSourceTyCtxt InstThetaCtxt   = ptext SLIT("the context of an instance declaration")
919 pprSourceTyCtxt TypeCtxt        = ptext SLIT("the context of a type")
920 \end{code}
921
922 \begin{code}
923 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
924 checkValidTheta ctxt theta 
925   = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
926
927 -------------------------
928 check_valid_theta ctxt []
929   = returnM ()
930 check_valid_theta ctxt theta
931   = getDOpts                                    `thenM` \ dflags ->
932     warnTc (notNull dups) (dupPredWarn dups)    `thenM_`
933     mappM_ (check_pred_ty dflags ctxt) theta
934   where
935     (_,dups) = removeDups tcCmpPred theta
936
937 -------------------------
938 check_pred_ty :: DynFlags -> SourceTyCtxt -> PredType -> TcM ()
939 check_pred_ty dflags ctxt pred@(ClassP cls tys)
940   = do {        -- Class predicates are valid in all contexts
941        ; checkTc (arity == n_tys) arity_err
942
943                 -- Check the form of the argument types
944        ; mappM_ check_arg_type tys
945        ; checkTc (check_class_pred_tys dflags ctxt tys)
946                  (predTyVarErr pred $$ how_to_allow)
947        }
948   where
949     class_name = className cls
950     arity      = classArity cls
951     n_tys      = length tys
952     arity_err  = arityErr "Class" class_name arity n_tys
953     how_to_allow = parens (ptext SLIT("Use -XFlexibleContexts to permit this"))
954
955 check_pred_ty dflags ctxt pred@(EqPred ty1 ty2)
956   = do {        -- Equational constraints are valid in all contexts if type
957                 -- families are permitted
958        ; checkTc (dopt Opt_TypeFamilies dflags) (eqPredTyErr pred)
959
960                 -- Check the form of the argument types
961        ; check_eq_arg_type ty1
962        ; check_eq_arg_type ty2
963        }
964   where 
965     check_eq_arg_type = check_poly_type (Rank 0) UT_NotOk
966
967 check_pred_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
968         -- Implicit parameters only allowed in type
969         -- signatures; not in instance decls, superclasses etc
970         -- The reason for not allowing implicit params in instances is a bit
971         -- subtle.
972         -- If we allowed        instance (?x::Int, Eq a) => Foo [a] where ...
973         -- then when we saw (e :: (?x::Int) => t) it would be unclear how to 
974         -- discharge all the potential usas of the ?x in e.   For example, a
975         -- constraint Foo [Int] might come out of e,and applying the
976         -- instance decl would show up two uses of ?x.
977
978 -- Catch-all
979 check_pred_ty dflags ctxt sty = failWithTc (badPredTyErr sty)
980
981 -------------------------
982 check_class_pred_tys :: DynFlags -> SourceTyCtxt -> [Type] -> Bool
983 check_class_pred_tys dflags ctxt tys 
984   = case ctxt of
985         TypeCtxt      -> True   -- {-# SPECIALISE instance Eq (T Int) #-} is fine
986         InstThetaCtxt -> flexible_contexts || undecidable_ok || all tcIsTyVarTy tys
987                                 -- Further checks on head and theta in
988                                 -- checkInstTermination
989         other         -> flexible_contexts || all tyvar_head tys
990   where
991     flexible_contexts = dopt Opt_FlexibleContexts dflags
992     undecidable_ok = dopt Opt_UndecidableInstances dflags
993
994 -------------------------
995 tyvar_head ty                   -- Haskell 98 allows predicates of form 
996   | tcIsTyVarTy ty = True       --      C (a ty1 .. tyn)
997   | otherwise                   -- where a is a type variable
998   = case tcSplitAppTy_maybe ty of
999         Just (ty, _) -> tyvar_head ty
1000         Nothing      -> False
1001 \end{code}
1002
1003 Check for ambiguity
1004 ~~~~~~~~~~~~~~~~~~~
1005           forall V. P => tau
1006 is ambiguous if P contains generic variables
1007 (i.e. one of the Vs) that are not mentioned in tau
1008
1009 However, we need to take account of functional dependencies
1010 when we speak of 'mentioned in tau'.  Example:
1011         class C a b | a -> b where ...
1012 Then the type
1013         forall x y. (C x y) => x
1014 is not ambiguous because x is mentioned and x determines y
1015
1016 NB; the ambiguity check is only used for *user* types, not for types
1017 coming from inteface files.  The latter can legitimately have
1018 ambiguous types. Example
1019
1020    class S a where s :: a -> (Int,Int)
1021    instance S Char where s _ = (1,1)
1022    f:: S a => [a] -> Int -> (Int,Int)
1023    f (_::[a]) x = (a*x,b)
1024         where (a,b) = s (undefined::a)
1025
1026 Here the worker for f gets the type
1027         fw :: forall a. S a => Int -> (# Int, Int #)
1028
1029 If the list of tv_names is empty, we have a monotype, and then we
1030 don't need to check for ambiguity either, because the test can't fail
1031 (see is_ambig).
1032
1033
1034 \begin{code}
1035 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
1036 checkAmbiguity forall_tyvars theta tau_tyvars
1037   = mappM_ complain (filter is_ambig theta)
1038   where
1039     complain pred     = addErrTc (ambigErr pred)
1040     extended_tau_vars = grow theta tau_tyvars
1041
1042         -- See Note [Implicit parameters and ambiguity] in TcSimplify
1043     is_ambig pred     = isClassPred  pred &&
1044                         any ambig_var (varSetElems (tyVarsOfPred pred))
1045
1046     ambig_var ct_var  = (ct_var `elem` forall_tyvars) &&
1047                         not (ct_var `elemVarSet` extended_tau_vars)
1048
1049 ambigErr pred
1050   = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
1051          nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
1052                  ptext SLIT("must be reachable from the type after the '=>'"))]
1053 \end{code}
1054     
1055 In addition, GHC insists that at least one type variable
1056 in each constraint is in V.  So we disallow a type like
1057         forall a. Eq b => b -> b
1058 even in a scope where b is in scope.
1059
1060 \begin{code}
1061 checkFreeness forall_tyvars theta
1062   = do  { flexible_contexts <- doptM Opt_FlexibleContexts
1063         ; unless flexible_contexts $ mappM_ complain (filter is_free theta) }
1064   where    
1065     is_free pred     =  not (isIPPred pred)
1066                      && not (any bound_var (varSetElems (tyVarsOfPred pred)))
1067     bound_var ct_var = ct_var `elem` forall_tyvars
1068     complain pred    = addErrTc (freeErr pred)
1069
1070 freeErr pred
1071   = sep [ ptext SLIT("All of the type variables in the constraint") <+> 
1072           quotes (pprPred pred)
1073         , ptext SLIT("are already in scope") <+>
1074           ptext SLIT("(at least one must be universally quantified here)")
1075         , nest 4 $
1076             ptext SLIT("(Use -XFlexibleContexts to lift this restriction)")
1077         ]
1078 \end{code}
1079
1080 \begin{code}
1081 checkThetaCtxt ctxt theta
1082   = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
1083           ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
1084
1085 badPredTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
1086 eqPredTyErr  sty = ptext SLIT("Illegal equational constraint") <+> pprPred sty
1087                    $$
1088                    parens (ptext SLIT("Use -XTypeFamilies to permit this"))
1089 predTyVarErr pred  = sep [ptext SLIT("Non type-variable argument"),
1090                           nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
1091 dupPredWarn dups   = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
1092
1093 arityErr kind name n m
1094   = hsep [ text kind, quotes (ppr name), ptext SLIT("should have"),
1095            n_arguments <> comma, text "but has been given", int m]
1096     where
1097         n_arguments | n == 0 = ptext SLIT("no arguments")
1098                     | n == 1 = ptext SLIT("1 argument")
1099                     | True   = hsep [int n, ptext SLIT("arguments")]
1100 \end{code}
1101
1102
1103 %************************************************************************
1104 %*                                                                      *
1105 \subsection{Checking for a decent instance head type}
1106 %*                                                                      *
1107 %************************************************************************
1108
1109 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1110 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1111
1112 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1113 flag is on, or (2)~the instance is imported (they must have been
1114 compiled elsewhere). In these cases, we let them go through anyway.
1115
1116 We can also have instances for functions: @instance Foo (a -> b) ...@.
1117
1118 \begin{code}
1119 checkValidInstHead :: Type -> TcM (Class, [TcType])
1120
1121 checkValidInstHead ty   -- Should be a source type
1122   = case tcSplitPredTy_maybe ty of {
1123         Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
1124         Just pred -> 
1125
1126     case getClassPredTys_maybe pred of {
1127         Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
1128         Just (clas,tys) ->
1129
1130     getDOpts                                    `thenM` \ dflags ->
1131     mappM_ check_arg_type tys                   `thenM_`
1132     check_inst_head dflags clas tys             `thenM_`
1133     returnM (clas, tys)
1134     }}
1135
1136 check_inst_head dflags clas tys
1137         -- If GlasgowExts then check at least one isn't a type variable
1138   = do checkTc (dopt Opt_TypeSynonymInstances dflags ||
1139                 all tcInstHeadTyNotSynonym tys)
1140                (instTypeErr (pprClassPred clas tys) head_type_synonym_msg)
1141        checkTc (dopt Opt_FlexibleInstances dflags ||
1142                 all tcInstHeadTyAppAllTyVars tys)
1143                (instTypeErr (pprClassPred clas tys) head_type_args_tyvars_msg)
1144        checkTc (dopt Opt_MultiParamTypeClasses dflags ||
1145                 isSingleton tys)
1146                (instTypeErr (pprClassPred clas tys) head_one_type_msg)
1147        mapM_ check_one tys
1148   where
1149     head_type_synonym_msg = parens (
1150                 text "All instance types must be of the form (T t1 ... tn)" $$
1151                 text "where T is not a synonym." $$
1152                 text "Use -XTypeSynonymInstances if you want to disable this.")
1153
1154     head_type_args_tyvars_msg = parens (
1155                 text "All instance types must be of the form (T a1 ... an)" $$
1156                 text "where a1 ... an are distinct type *variables*" $$
1157                 text "Use -XFlexibleInstances if you want to disable this.")
1158
1159     head_one_type_msg = parens (
1160                 text "Only one type can be given in an instance head." $$
1161                 text "Use -XMultiParamTypeClasses if you want to allow more.")
1162
1163         -- For now, I only allow tau-types (not polytypes) in 
1164         -- the head of an instance decl.  
1165         --      E.g.  instance C (forall a. a->a) is rejected
1166         -- One could imagine generalising that, but I'm not sure
1167         -- what all the consequences might be
1168     check_one ty = do { check_tau_type (Rank 0) UT_NotOk ty
1169                       ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
1170
1171 instTypeErr pp_ty msg
1172   = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty, 
1173          nest 4 msg]
1174 \end{code}
1175
1176
1177 %************************************************************************
1178 %*                                                                      *
1179 \subsection{Checking instance for termination}
1180 %*                                                                      *
1181 %************************************************************************
1182
1183
1184 \begin{code}
1185 checkValidInstance :: [TyVar] -> ThetaType -> Class -> [TcType] -> TcM ()
1186 checkValidInstance tyvars theta clas inst_tys
1187   = do  { undecidable_ok <- doptM Opt_UndecidableInstances
1188
1189         ; checkValidTheta InstThetaCtxt theta
1190         ; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys)
1191
1192         -- Check that instance inference will terminate (if we care)
1193         -- For Haskell 98 this will already have been done by checkValidTheta,
1194         -- but as we may be using other extensions we need to check.
1195         ; unless undecidable_ok $
1196           mapM_ addErrTc (checkInstTermination inst_tys theta)
1197         
1198         -- The Coverage Condition
1199         ; checkTc (undecidable_ok || checkInstCoverage clas inst_tys)
1200                   (instTypeErr (pprClassPred clas inst_tys) msg)
1201         }
1202   where
1203     msg  = parens (vcat [ptext SLIT("the Coverage Condition fails for one of the functional dependencies;"),
1204                          undecidableMsg])
1205 \end{code}
1206
1207 Termination test: the so-called "Paterson conditions" (see Section 5 of
1208 "Understanding functionsl dependencies via Constraint Handling Rules, 
1209 JFP Jan 2007).
1210
1211 We check that each assertion in the context satisfies:
1212  (1) no variable has more occurrences in the assertion than in the head, and
1213  (2) the assertion has fewer constructors and variables (taken together
1214      and counting repetitions) than the head.
1215 This is only needed with -fglasgow-exts, as Haskell 98 restrictions
1216 (which have already been checked) guarantee termination. 
1217
1218 The underlying idea is that 
1219
1220     for any ground substitution, each assertion in the
1221     context has fewer type constructors than the head.
1222
1223
1224 \begin{code}
1225 checkInstTermination :: [TcType] -> ThetaType -> [Message]
1226 checkInstTermination tys theta
1227   = mapCatMaybes check theta
1228   where
1229    fvs  = fvTypes tys
1230    size = sizeTypes tys
1231    check pred 
1232       | not (null (fvPred pred \\ fvs)) 
1233       = Just (predUndecErr pred nomoreMsg $$ parens undecidableMsg)
1234       | sizePred pred >= size
1235       = Just (predUndecErr pred smallerMsg $$ parens undecidableMsg)
1236       | otherwise
1237       = Nothing
1238
1239 predUndecErr pred msg = sep [msg,
1240                         nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
1241
1242 nomoreMsg = ptext SLIT("Variable occurs more often in a constraint than in the instance head")
1243 smallerMsg = ptext SLIT("Constraint is no smaller than the instance head")
1244 undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
1245 \end{code}
1246
1247
1248 %************************************************************************
1249 %*                                                                      *
1250         Checking the context of a derived instance declaration
1251 %*                                                                      *
1252 %************************************************************************
1253
1254 Note [Exotic derived instance contexts]
1255 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1256 In a 'derived' instance declaration, we *infer* the context.  It's a
1257 bit unclear what rules we should apply for this; the Haskell report is
1258 silent.  Obviously, constraints like (Eq a) are fine, but what about
1259         data T f a = MkT (f a) deriving( Eq )
1260 where we'd get an Eq (f a) constraint.  That's probably fine too.
1261
1262 One could go further: consider
1263         data T a b c = MkT (Foo a b c) deriving( Eq )
1264         instance (C Int a, Eq b, Eq c) => Eq (Foo a b c)
1265
1266 Notice that this instance (just) satisfies the Paterson termination 
1267 conditions.  Then we *could* derive an instance decl like this:
1268
1269         instance (C Int a, Eq b, Eq c) => Eq (T a b c) 
1270
1271 even though there is no instance for (C Int a), because there just
1272 *might* be an instance for, say, (C Int Bool) at a site where we
1273 need the equality instance for T's.  
1274
1275 However, this seems pretty exotic, and it's quite tricky to allow
1276 this, and yet give sensible error messages in the (much more common)
1277 case where we really want that instance decl for C.
1278
1279 So for now we simply require that the derived instance context
1280 should have only type-variable constraints.
1281
1282 Here is another example:
1283         data Fix f = In (f (Fix f)) deriving( Eq )
1284 Here, if we are prepared to allow -fallow-undecidable-instances we
1285 could derive the instance
1286         instance Eq (f (Fix f)) => Eq (Fix f)
1287 but this is so delicate that I don't think it should happen inside
1288 'deriving'. If you want this, write it yourself!
1289
1290 NB: if you want to lift this condition, make sure you still meet the
1291 termination conditions!  If not, the deriving mechanism generates
1292 larger and larger constraints.  Example:
1293   data Succ a = S a
1294   data Seq a = Cons a (Seq (Succ a)) | Nil deriving Show
1295
1296 Note the lack of a Show instance for Succ.  First we'll generate
1297   instance (Show (Succ a), Show a) => Show (Seq a)
1298 and then
1299   instance (Show (Succ (Succ a)), Show (Succ a), Show a) => Show (Seq a)
1300 and so on.  Instead we want to complain of no instance for (Show (Succ a)).
1301
1302 The bottom line
1303 ~~~~~~~~~~~~~~~
1304 Allow constraints which consist only of type variables, with no repeats.
1305
1306 \begin{code}
1307 validDerivPred :: PredType -> Bool
1308 validDerivPred (ClassP cls tys) = hasNoDups fvs && sizeTypes tys == length fvs
1309                                 where fvs = fvTypes tys
1310 validDerivPred otehr            = False
1311 \end{code}
1312
1313 %************************************************************************
1314 %*                                                                      *
1315         Checking type instance well-formedness and termination
1316 %*                                                                      *
1317 %************************************************************************
1318
1319 \begin{code}
1320 -- Check that a "type instance" is well-formed (which includes decidability
1321 -- unless -fallow-undecidable-instances is given).
1322 --
1323 checkValidTypeInst :: [Type] -> Type -> TcM ()
1324 checkValidTypeInst typats rhs
1325   = do { -- left-hand side contains no type family applications
1326          -- (vanilla synonyms are fine, though)
1327        ; mappM_ checkTyFamFreeness typats
1328
1329          -- the right-hand side is a tau type
1330        ; checkTc (isTauTy rhs) $ 
1331            polyTyErr rhs
1332
1333          -- we have a decidable instance unless otherwise permitted
1334        ; undecidable_ok <- doptM Opt_UndecidableInstances
1335        ; unless undecidable_ok $
1336            mapM_ addErrTc (checkFamInst typats (tyFamInsts rhs))
1337        }
1338
1339 -- Make sure that each type family instance is 
1340 --   (1) strictly smaller than the lhs,
1341 --   (2) mentions no type variable more often than the lhs, and
1342 --   (3) does not contain any further type family instances.
1343 --
1344 checkFamInst :: [Type]                  -- lhs
1345              -> [(TyCon, [Type])]       -- type family instances
1346              -> [Message]
1347 checkFamInst lhsTys famInsts
1348   = mapCatMaybes check famInsts
1349   where
1350    size = sizeTypes lhsTys
1351    fvs  = fvTypes lhsTys
1352    check (tc, tys)
1353       | not (all isTyFamFree tys)
1354       = Just (famInstUndecErr famInst nestedMsg $$ parens undecidableMsg)
1355       | not (null (fvTypes tys \\ fvs))
1356       = Just (famInstUndecErr famInst nomoreVarMsg $$ parens undecidableMsg)
1357       | size <= sizeTypes tys
1358       = Just (famInstUndecErr famInst smallerAppMsg $$ parens undecidableMsg)
1359       | otherwise
1360       = Nothing
1361       where
1362         famInst = TyConApp tc tys
1363
1364 -- Ensure that no type family instances occur in a type.
1365 --
1366 checkTyFamFreeness :: Type -> TcM ()
1367 checkTyFamFreeness ty
1368   = checkTc (isTyFamFree ty) $
1369       tyFamInstInIndexErr ty
1370
1371 -- Check that a type does not contain any type family applications.
1372 --
1373 isTyFamFree :: Type -> Bool
1374 isTyFamFree = null . tyFamInsts
1375
1376 -- Error messages
1377
1378 tyFamInstInIndexErr ty
1379   = hang (ptext SLIT("Illegal type family application in type instance") <> 
1380          colon) 4 $
1381       ppr ty
1382
1383 polyTyErr ty 
1384   = hang (ptext SLIT("Illegal polymorphic type in type instance") <> colon) 4 $
1385       ppr ty
1386
1387 famInstUndecErr ty msg 
1388   = sep [msg, 
1389          nest 2 (ptext SLIT("in the type family application:") <+> 
1390                  pprType ty)]
1391
1392 nestedMsg     = ptext SLIT("Nested type family application")
1393 nomoreVarMsg  = ptext SLIT("Variable occurs more often than in instance head")
1394 smallerAppMsg = ptext SLIT("Application is no smaller than the instance head")
1395 \end{code}
1396
1397
1398 %************************************************************************
1399 %*                                                                      *
1400 \subsection{Auxiliary functions}
1401 %*                                                                      *
1402 %************************************************************************
1403
1404 \begin{code}
1405 -- Free variables of a type, retaining repetitions, and expanding synonyms
1406 fvType :: Type -> [TyVar]
1407 fvType ty | Just exp_ty <- tcView ty = fvType exp_ty
1408 fvType (TyVarTy tv)        = [tv]
1409 fvType (TyConApp _ tys)    = fvTypes tys
1410 fvType (NoteTy _ ty)       = fvType ty
1411 fvType (PredTy pred)       = fvPred pred
1412 fvType (FunTy arg res)     = fvType arg ++ fvType res
1413 fvType (AppTy fun arg)     = fvType fun ++ fvType arg
1414 fvType (ForAllTy tyvar ty) = filter (/= tyvar) (fvType ty)
1415
1416 fvTypes :: [Type] -> [TyVar]
1417 fvTypes tys                = concat (map fvType tys)
1418
1419 fvPred :: PredType -> [TyVar]
1420 fvPred (ClassP _ tys')     = fvTypes tys'
1421 fvPred (IParam _ ty)       = fvType ty
1422 fvPred (EqPred ty1 ty2)    = fvType ty1 ++ fvType ty2
1423
1424 -- Size of a type: the number of variables and constructors
1425 sizeType :: Type -> Int
1426 sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty
1427 sizeType (TyVarTy _)       = 1
1428 sizeType (TyConApp _ tys)  = sizeTypes tys + 1
1429 sizeType (NoteTy _ ty)     = sizeType ty
1430 sizeType (PredTy pred)     = sizePred pred
1431 sizeType (FunTy arg res)   = sizeType arg + sizeType res + 1
1432 sizeType (AppTy fun arg)   = sizeType fun + sizeType arg
1433 sizeType (ForAllTy _ ty)   = sizeType ty
1434
1435 sizeTypes :: [Type] -> Int
1436 sizeTypes xs               = sum (map sizeType xs)
1437
1438 sizePred :: PredType -> Int
1439 sizePred (ClassP _ tys')   = sizeTypes tys'
1440 sizePred (IParam _ ty)     = sizeType ty
1441 sizePred (EqPred ty1 ty2)  = sizeType ty1 + sizeType ty2
1442 \end{code}