Add {-# OPTIONS_GHC -w #-} and some blurb to all compiler modules
[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_GHC -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/WorkingConventions#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, checkAmbiguity,
51   checkInstTermination, checkValidTypeInst, checkTyFamFreeness,
52   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 dflags ctxt pred@(ClassP cls tys)
939   = do {        -- Class predicates are valid in all contexts
940        ; checkTc (arity == n_tys) arity_err
941
942                 -- Check the form of the argument types
943        ; mappM_ check_arg_type tys
944        ; checkTc (check_class_pred_tys dflags ctxt tys)
945                  (predTyVarErr pred $$ how_to_allow)
946        }
947   where
948     class_name = className cls
949     arity      = classArity cls
950     n_tys      = length tys
951     arity_err  = arityErr "Class" class_name arity n_tys
952     how_to_allow = parens (ptext SLIT("Use -XFlexibleContexts to permit this"))
953
954 check_pred_ty dflags ctxt pred@(EqPred ty1 ty2)
955   = do {        -- Equational constraints are valid in all contexts if type
956                 -- families are permitted
957        ; checkTc (dopt Opt_TypeFamilies dflags) (eqPredTyErr pred)
958
959                 -- Check the form of the argument types
960        ; check_eq_arg_type ty1
961        ; check_eq_arg_type ty2
962        }
963   where 
964     check_eq_arg_type = check_poly_type (Rank 0) UT_NotOk
965
966 check_pred_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
967         -- Implicit parameters only allowed in type
968         -- signatures; not in instance decls, superclasses etc
969         -- The reason for not allowing implicit params in instances is a bit
970         -- subtle.
971         -- If we allowed        instance (?x::Int, Eq a) => Foo [a] where ...
972         -- then when we saw (e :: (?x::Int) => t) it would be unclear how to 
973         -- discharge all the potential usas of the ?x in e.   For example, a
974         -- constraint Foo [Int] might come out of e,and applying the
975         -- instance decl would show up two uses of ?x.
976
977 -- Catch-all
978 check_pred_ty dflags ctxt sty = failWithTc (badPredTyErr sty)
979
980 -------------------------
981 check_class_pred_tys dflags ctxt tys 
982   = case ctxt of
983         TypeCtxt      -> True   -- {-# SPECIALISE instance Eq (T Int) #-} is fine
984         InstThetaCtxt -> flexible_contexts || undecidable_ok || all tcIsTyVarTy tys
985                                 -- Further checks on head and theta in
986                                 -- checkInstTermination
987         other         -> flexible_contexts || all tyvar_head tys
988   where
989     flexible_contexts = dopt Opt_FlexibleContexts dflags
990     undecidable_ok = dopt Opt_UndecidableInstances dflags
991
992 -------------------------
993 tyvar_head ty                   -- Haskell 98 allows predicates of form 
994   | tcIsTyVarTy ty = True       --      C (a ty1 .. tyn)
995   | otherwise                   -- where a is a type variable
996   = case tcSplitAppTy_maybe ty of
997         Just (ty, _) -> tyvar_head ty
998         Nothing      -> False
999 \end{code}
1000
1001 Check for ambiguity
1002 ~~~~~~~~~~~~~~~~~~~
1003           forall V. P => tau
1004 is ambiguous if P contains generic variables
1005 (i.e. one of the Vs) that are not mentioned in tau
1006
1007 However, we need to take account of functional dependencies
1008 when we speak of 'mentioned in tau'.  Example:
1009         class C a b | a -> b where ...
1010 Then the type
1011         forall x y. (C x y) => x
1012 is not ambiguous because x is mentioned and x determines y
1013
1014 NB; the ambiguity check is only used for *user* types, not for types
1015 coming from inteface files.  The latter can legitimately have
1016 ambiguous types. Example
1017
1018    class S a where s :: a -> (Int,Int)
1019    instance S Char where s _ = (1,1)
1020    f:: S a => [a] -> Int -> (Int,Int)
1021    f (_::[a]) x = (a*x,b)
1022         where (a,b) = s (undefined::a)
1023
1024 Here the worker for f gets the type
1025         fw :: forall a. S a => Int -> (# Int, Int #)
1026
1027 If the list of tv_names is empty, we have a monotype, and then we
1028 don't need to check for ambiguity either, because the test can't fail
1029 (see is_ambig).
1030
1031 \begin{code}
1032 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
1033 checkAmbiguity forall_tyvars theta tau_tyvars
1034   = mappM_ complain (filter is_ambig theta)
1035   where
1036     complain pred     = addErrTc (ambigErr pred)
1037     extended_tau_vars = grow theta tau_tyvars
1038
1039         -- Only a *class* predicate can give rise to ambiguity
1040         -- An *implicit parameter* cannot.  For example:
1041         --      foo :: (?x :: [a]) => Int
1042         --      foo = length ?x
1043         -- is fine.  The call site will suppply a particular 'x'
1044     is_ambig pred     = isClassPred  pred &&
1045                         any ambig_var (varSetElems (tyVarsOfPred pred))
1046
1047     ambig_var ct_var  = (ct_var `elem` forall_tyvars) &&
1048                         not (ct_var `elemVarSet` extended_tau_vars)
1049
1050 ambigErr pred
1051   = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
1052          nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
1053                  ptext SLIT("must be reachable from the type after the '=>'"))]
1054 \end{code}
1055     
1056 In addition, GHC insists that at least one type variable
1057 in each constraint is in V.  So we disallow a type like
1058         forall a. Eq b => b -> b
1059 even in a scope where b is in scope.
1060
1061 \begin{code}
1062 checkFreeness forall_tyvars theta
1063   = do  { flexible_contexts <- doptM Opt_FlexibleContexts
1064         ; unless flexible_contexts $ mappM_ complain (filter is_free theta) }
1065   where    
1066     is_free pred     =  not (isIPPred pred)
1067                      && not (any bound_var (varSetElems (tyVarsOfPred pred)))
1068     bound_var ct_var = ct_var `elem` forall_tyvars
1069     complain pred    = addErrTc (freeErr pred)
1070
1071 freeErr pred
1072   = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
1073                    ptext SLIT("are already in scope"),
1074          nest 4 (ptext SLIT("(at least one must be universally quantified here)"))
1075     ]
1076 \end{code}
1077
1078 \begin{code}
1079 checkThetaCtxt ctxt theta
1080   = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
1081           ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
1082
1083 badPredTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
1084 eqPredTyErr  sty = ptext SLIT("Illegal equational constraint") <+> pprPred sty
1085                    $$
1086                    parens (ptext SLIT("Use -ftype-families to permit this"))
1087 predTyVarErr pred  = sep [ptext SLIT("Non type-variable argument"),
1088                           nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
1089 dupPredWarn dups   = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
1090
1091 arityErr kind name n m
1092   = hsep [ text kind, quotes (ppr name), ptext SLIT("should have"),
1093            n_arguments <> comma, text "but has been given", int m]
1094     where
1095         n_arguments | n == 0 = ptext SLIT("no arguments")
1096                     | n == 1 = ptext SLIT("1 argument")
1097                     | True   = hsep [int n, ptext SLIT("arguments")]
1098 \end{code}
1099
1100
1101 %************************************************************************
1102 %*                                                                      *
1103 \subsection{Checking for a decent instance head type}
1104 %*                                                                      *
1105 %************************************************************************
1106
1107 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1108 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1109
1110 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1111 flag is on, or (2)~the instance is imported (they must have been
1112 compiled elsewhere). In these cases, we let them go through anyway.
1113
1114 We can also have instances for functions: @instance Foo (a -> b) ...@.
1115
1116 \begin{code}
1117 checkValidInstHead :: Type -> TcM (Class, [TcType])
1118
1119 checkValidInstHead ty   -- Should be a source type
1120   = case tcSplitPredTy_maybe ty of {
1121         Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
1122         Just pred -> 
1123
1124     case getClassPredTys_maybe pred of {
1125         Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
1126         Just (clas,tys) ->
1127
1128     getDOpts                                    `thenM` \ dflags ->
1129     mappM_ check_arg_type tys                   `thenM_`
1130     check_inst_head dflags clas tys             `thenM_`
1131     returnM (clas, tys)
1132     }}
1133
1134 check_inst_head dflags clas tys
1135         -- If GlasgowExts then check at least one isn't a type variable
1136   = do checkTc (dopt Opt_TypeSynonymInstances dflags ||
1137                 all tcInstHeadTyNotSynonym tys)
1138                (instTypeErr (pprClassPred clas tys) head_type_synonym_msg)
1139        checkTc (dopt Opt_FlexibleInstances dflags ||
1140                 all tcInstHeadTyAppAllTyVars tys)
1141                (instTypeErr (pprClassPred clas tys) head_type_args_tyvars_msg)
1142        checkTc (dopt Opt_MultiParamTypeClasses dflags ||
1143                 isSingleton tys)
1144                (instTypeErr (pprClassPred clas tys) head_one_type_msg)
1145        mapM_ check_one tys
1146   where
1147     head_type_synonym_msg = parens (
1148                 text "All instance types must be of the form (T t1 ... tn)" $$
1149                 text "where T is not a synonym." $$
1150                 text "Use -XTypeSynonymInstances if you want to disable this.")
1151
1152     head_type_args_tyvars_msg = parens (
1153                 text "All instance types must be of the form (T a1 ... an)" $$
1154                 text "where a1 ... an are distinct type *variables*" $$
1155                 text "Use -XFlexibleInstances if you want to disable this.")
1156
1157     head_one_type_msg = parens (
1158                 text "Only one type can be given in an instance head." $$
1159                 text "Use -XMultiParamTypeClasses if you want to allow more.")
1160
1161         -- For now, I only allow tau-types (not polytypes) in 
1162         -- the head of an instance decl.  
1163         --      E.g.  instance C (forall a. a->a) is rejected
1164         -- One could imagine generalising that, but I'm not sure
1165         -- what all the consequences might be
1166     check_one ty = do { check_tau_type (Rank 0) UT_NotOk ty
1167                       ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
1168
1169 instTypeErr pp_ty msg
1170   = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty, 
1171          nest 4 msg]
1172 \end{code}
1173
1174
1175 %************************************************************************
1176 %*                                                                      *
1177 \subsection{Checking instance for termination}
1178 %*                                                                      *
1179 %************************************************************************
1180
1181
1182 \begin{code}
1183 checkValidInstance :: [TyVar] -> ThetaType -> Class -> [TcType] -> TcM ()
1184 checkValidInstance tyvars theta clas inst_tys
1185   = do  { undecidable_ok <- doptM Opt_UndecidableInstances
1186
1187         ; checkValidTheta InstThetaCtxt theta
1188         ; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys)
1189
1190         -- Check that instance inference will terminate (if we care)
1191         -- For Haskell 98 this will already have been done by checkValidTheta,
1192         -- but as we may be using other extensions we need to check.
1193         ; unless undecidable_ok $
1194           mapM_ addErrTc (checkInstTermination inst_tys theta)
1195         
1196         -- The Coverage Condition
1197         ; checkTc (undecidable_ok || checkInstCoverage clas inst_tys)
1198                   (instTypeErr (pprClassPred clas inst_tys) msg)
1199         }
1200   where
1201     msg  = parens (vcat [ptext SLIT("the Coverage Condition fails for one of the functional dependencies;"),
1202                          undecidableMsg])
1203 \end{code}
1204
1205 Termination test: the so-called "Paterson conditions" (see Section 5 of
1206 "Understanding functionsl dependencies via Constraint Handling Rules, 
1207 JFP Jan 2007).
1208
1209 We check that each assertion in the context satisfies:
1210  (1) no variable has more occurrences in the assertion than in the head, and
1211  (2) the assertion has fewer constructors and variables (taken together
1212      and counting repetitions) than the head.
1213 This is only needed with -fglasgow-exts, as Haskell 98 restrictions
1214 (which have already been checked) guarantee termination. 
1215
1216 The underlying idea is that 
1217
1218     for any ground substitution, each assertion in the
1219     context has fewer type constructors than the head.
1220
1221
1222 \begin{code}
1223 checkInstTermination :: [TcType] -> ThetaType -> [Message]
1224 checkInstTermination tys theta
1225   = mapCatMaybes check theta
1226   where
1227    fvs  = fvTypes tys
1228    size = sizeTypes tys
1229    check pred 
1230       | not (null (fvPred pred \\ fvs)) 
1231       = Just (predUndecErr pred nomoreMsg $$ parens undecidableMsg)
1232       | sizePred pred >= size
1233       = Just (predUndecErr pred smallerMsg $$ parens undecidableMsg)
1234       | otherwise
1235       = Nothing
1236
1237 predUndecErr pred msg = sep [msg,
1238                         nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
1239
1240 nomoreMsg = ptext SLIT("Variable occurs more often in a constraint than in the instance head")
1241 smallerMsg = ptext SLIT("Constraint is no smaller than the instance head")
1242 undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
1243 \end{code}
1244
1245
1246 %************************************************************************
1247 %*                                                                      *
1248 \subsection{Checking type instance well-formedness and termination}
1249 %*                                                                      *
1250 %************************************************************************
1251
1252 \begin{code}
1253 -- Check that a "type instance" is well-formed (which includes decidability
1254 -- unless -fallow-undecidable-instances is given).
1255 --
1256 checkValidTypeInst :: [Type] -> Type -> TcM ()
1257 checkValidTypeInst typats rhs
1258   = do { -- left-hand side contains no type family applications
1259          -- (vanilla synonyms are fine, though)
1260        ; mappM_ checkTyFamFreeness typats
1261
1262          -- the right-hand side is a tau type
1263        ; checkTc (isTauTy rhs) $ 
1264            polyTyErr rhs
1265
1266          -- we have a decidable instance unless otherwise permitted
1267        ; undecidable_ok <- doptM Opt_UndecidableInstances
1268        ; unless undecidable_ok $
1269            mapM_ addErrTc (checkFamInst typats (tyFamInsts rhs))
1270        }
1271
1272 -- Make sure that each type family instance is 
1273 --   (1) strictly smaller than the lhs,
1274 --   (2) mentions no type variable more often than the lhs, and
1275 --   (3) does not contain any further type family instances.
1276 --
1277 checkFamInst :: [Type]                  -- lhs
1278              -> [(TyCon, [Type])]       -- type family instances
1279              -> [Message]
1280 checkFamInst lhsTys famInsts
1281   = mapCatMaybes check famInsts
1282   where
1283    size = sizeTypes lhsTys
1284    fvs  = fvTypes lhsTys
1285    check (tc, tys)
1286       | not (all isTyFamFree tys)
1287       = Just (famInstUndecErr famInst nestedMsg $$ parens undecidableMsg)
1288       | not (null (fvTypes tys \\ fvs))
1289       = Just (famInstUndecErr famInst nomoreVarMsg $$ parens undecidableMsg)
1290       | size <= sizeTypes tys
1291       = Just (famInstUndecErr famInst smallerAppMsg $$ parens undecidableMsg)
1292       | otherwise
1293       = Nothing
1294       where
1295         famInst = TyConApp tc tys
1296
1297 -- Ensure that no type family instances occur in a type.
1298 --
1299 checkTyFamFreeness :: Type -> TcM ()
1300 checkTyFamFreeness ty
1301   = checkTc (isTyFamFree ty) $
1302       tyFamInstInIndexErr ty
1303
1304 -- Check that a type does not contain any type family applications.
1305 --
1306 isTyFamFree :: Type -> Bool
1307 isTyFamFree = null . tyFamInsts
1308
1309 -- Error messages
1310
1311 tyFamInstInIndexErr ty
1312   = hang (ptext SLIT("Illegal type family application in type instance") <> 
1313          colon) 4 $
1314       ppr ty
1315
1316 polyTyErr ty 
1317   = hang (ptext SLIT("Illegal polymorphic type in type instance") <> colon) 4 $
1318       ppr ty
1319
1320 famInstUndecErr ty msg 
1321   = sep [msg, 
1322          nest 2 (ptext SLIT("in the type family application:") <+> 
1323                  pprType ty)]
1324
1325 nestedMsg     = ptext SLIT("Nested type family application")
1326 nomoreVarMsg  = ptext SLIT("Variable occurs more often than in instance head")
1327 smallerAppMsg = ptext SLIT("Application is no smaller than the instance head")
1328 \end{code}
1329
1330
1331 %************************************************************************
1332 %*                                                                      *
1333 \subsection{Auxiliary functions}
1334 %*                                                                      *
1335 %************************************************************************
1336
1337 \begin{code}
1338 -- Free variables of a type, retaining repetitions, and expanding synonyms
1339 fvType :: Type -> [TyVar]
1340 fvType ty | Just exp_ty <- tcView ty = fvType exp_ty
1341 fvType (TyVarTy tv)        = [tv]
1342 fvType (TyConApp _ tys)    = fvTypes tys
1343 fvType (NoteTy _ ty)       = fvType ty
1344 fvType (PredTy pred)       = fvPred pred
1345 fvType (FunTy arg res)     = fvType arg ++ fvType res
1346 fvType (AppTy fun arg)     = fvType fun ++ fvType arg
1347 fvType (ForAllTy tyvar ty) = filter (/= tyvar) (fvType ty)
1348
1349 fvTypes :: [Type] -> [TyVar]
1350 fvTypes tys                = concat (map fvType tys)
1351
1352 fvPred :: PredType -> [TyVar]
1353 fvPred (ClassP _ tys')     = fvTypes tys'
1354 fvPred (IParam _ ty)       = fvType ty
1355 fvPred (EqPred ty1 ty2)    = fvType ty1 ++ fvType ty2
1356
1357 -- Size of a type: the number of variables and constructors
1358 sizeType :: Type -> Int
1359 sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty
1360 sizeType (TyVarTy _)       = 1
1361 sizeType (TyConApp _ tys)  = sizeTypes tys + 1
1362 sizeType (NoteTy _ ty)     = sizeType ty
1363 sizeType (PredTy pred)     = sizePred pred
1364 sizeType (FunTy arg res)   = sizeType arg + sizeType res + 1
1365 sizeType (AppTy fun arg)   = sizeType fun + sizeType arg
1366 sizeType (ForAllTy _ ty)   = sizeType ty
1367
1368 sizeTypes :: [Type] -> Int
1369 sizeTypes xs               = sum (map sizeType xs)
1370
1371 sizePred :: PredType -> Int
1372 sizePred (ClassP _ tys')   = sizeTypes tys'
1373 sizePred (IParam _ ty)     = sizeType ty
1374 sizePred (EqPred ty1 ty2)  = sizeType ty1 + sizeType ty2
1375
1376 -- Type family instances occuring in a type after expanding synonyms
1377 tyFamInsts :: Type -> [(TyCon, [Type])]
1378 tyFamInsts ty 
1379   | Just exp_ty <- tcView ty    = tyFamInsts exp_ty
1380 tyFamInsts (TyVarTy _)          = []
1381 tyFamInsts (TyConApp tc tys) 
1382   | isOpenSynTyCon tc           = [(tc, tys)]
1383   | otherwise                   = concat (map tyFamInsts tys)
1384 tyFamInsts (FunTy ty1 ty2)      = tyFamInsts ty1 ++ tyFamInsts ty2
1385 tyFamInsts (AppTy ty1 ty2)      = tyFamInsts ty1 ++ tyFamInsts ty2
1386 tyFamInsts (ForAllTy _ ty)      = tyFamInsts ty
1387 \end{code}