Fix rank-validity testing
[ghc.git] / compiler / typecheck / TcMType.lhs
1 %
2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
3 %
4 \section{Monadic type operations}
5
6 This module contains monadic operations over types that contain mutable type variables
7
8 \begin{code}
9 module TcMType (
10   TcTyVar, TcKind, TcType, TcTauType, TcThetaType, TcTyVarSet,
11
12   --------------------------------
13   -- Creating new mutable type variables
14   newFlexiTyVar,
15   newFlexiTyVarTy,              -- Kind -> TcM TcType
16   newFlexiTyVarTys,             -- Int -> Kind -> TcM [TcType]
17   newKindVar, newKindVars, 
18   lookupTcTyVar, LookupTyVarResult(..),
19   newMetaTyVar, readMetaTyVar, writeMetaTyVar, 
20
21   --------------------------------
22   -- Boxy type variables
23   newBoxyTyVar, newBoxyTyVars, newBoxyTyVarTys, readFilledBox, 
24
25   --------------------------------
26   -- Instantiation
27   tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxy, tcInstBoxyTyVar,
28   tcInstSigTyVars, zonkSigTyVar,
29   tcInstSkolTyVar, tcInstSkolTyVars, tcInstSkolType, 
30   tcSkolSigType, tcSkolSigTyVars,
31
32   --------------------------------
33   -- Checking type validity
34   Rank, UserTypeCtxt(..), checkValidType, 
35   SourceTyCtxt(..), checkValidTheta, checkFreeness,
36   checkValidInstHead, checkValidInstance, checkAmbiguity,
37   checkInstTermination,
38   arityErr, 
39
40   --------------------------------
41   -- Zonking
42   zonkType, zonkTcPredType, 
43   zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkQuantifiedTyVar,
44   zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
45   zonkTcKindToKind, zonkTcKind,
46
47   readKindVar, writeKindVar
48
49   ) where
50
51 #include "HsVersions.h"
52
53
54 -- friends:
55 import TypeRep          ( Type(..), PredType(..),  -- Friend; can see representation
56                           ThetaType
57                         ) 
58 import TcType           ( TcType, TcThetaType, TcTauType, TcPredType,
59                           TcTyVarSet, TcKind, TcTyVar, TcTyVarDetails(..), 
60                           MetaDetails(..), SkolemInfo(..), BoxInfo(..), 
61                           BoxyTyVar, BoxyType, BoxyThetaType, BoxySigmaType, 
62                           UserTypeCtxt(..),
63                           isMetaTyVar, isSigTyVar, metaTvRef,
64                           tcCmpPred, isClassPred, tcGetTyVar,
65                           tcSplitPhiTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe, 
66                           tcValidInstHeadTy, tcSplitForAllTys,
67                           tcIsTyVarTy, tcSplitSigmaTy, 
68                           isUnLiftedType, isIPPred, 
69                           typeKind, isSkolemTyVar,
70                           mkAppTy, mkTyVarTy, mkTyVarTys, 
71                           tyVarsOfPred, getClassPredTys_maybe,
72                           tyVarsOfType, tyVarsOfTypes, tcView,
73                           pprPred, pprTheta, pprClassPred )
74 import Kind             ( Kind(..), KindVar, kindVarRef, mkKindVar, 
75                           isLiftedTypeKind, isArgTypeKind, isOpenTypeKind,
76                           liftedTypeKind, defaultKind
77                         )
78 import Type             ( TvSubst, zipTopTvSubst, substTy )
79 import Class            ( Class, classArity, className )
80 import TyCon            ( TyCon, isSynTyCon, isUnboxedTupleTyCon, 
81                           tyConArity, tyConName )
82 import Var              ( TyVar, tyVarKind, tyVarName, isTcTyVar, 
83                           mkTyVar, mkTcTyVar, tcTyVarDetails )
84
85         -- Assertions
86 #ifdef DEBUG
87 import TcType           ( isFlexi, isBoxyTyVar, isImmutableTyVar )
88 import Kind             ( isSubKind )
89 #endif
90
91 -- others:
92 import TcRnMonad          -- TcType, amongst others
93 import FunDeps          ( grow, checkInstCoverage )
94 import Name             ( Name, setNameUnique, mkSysTvName )
95 import VarSet
96 import DynFlags         ( dopt, DynFlag(..) )
97 import Util             ( nOfThem, isSingleton, notNull )
98 import ListSetOps       ( removeDups )
99 import Outputable
100
101 import Control.Monad    ( when )
102 import Data.List        ( (\\) )
103 \end{code}
104
105
106 %************************************************************************
107 %*                                                                      *
108         Instantiation in general
109 %*                                                                      *
110 %************************************************************************
111
112 \begin{code}
113 tcInstType :: ([TyVar] -> TcM [TcTyVar])                -- How to instantiate the type variables
114            -> TcType                                    -- Type to instantiate
115            -> TcM ([TcTyVar], TcThetaType, TcType)      -- Result
116 tcInstType inst_tyvars ty
117   = case tcSplitForAllTys ty of
118         ([],     rho) -> let    -- There may be overloading despite no type variables;
119                                 --      (?x :: Int) => Int -> Int
120                            (theta, tau) = tcSplitPhiTy rho
121                          in
122                          return ([], theta, tau)
123
124         (tyvars, rho) -> do { tyvars' <- inst_tyvars tyvars
125
126                             ; let  tenv = zipTopTvSubst tyvars (mkTyVarTys tyvars')
127                                 -- Either the tyvars are freshly made, by inst_tyvars,
128                                 -- or (in the call from tcSkolSigType) any nested foralls
129                                 -- have different binders.  Either way, zipTopTvSubst is ok
130
131                             ; let  (theta, tau) = tcSplitPhiTy (substTy tenv rho)
132                             ; return (tyvars', theta, tau) }
133 \end{code}
134
135
136 %************************************************************************
137 %*                                                                      *
138         Kind variables
139 %*                                                                      *
140 %************************************************************************
141
142 \begin{code}
143 newKindVar :: TcM TcKind
144 newKindVar = do { uniq <- newUnique
145                 ; ref <- newMutVar Nothing
146                 ; return (KindVar (mkKindVar uniq ref)) }
147
148 newKindVars :: Int -> TcM [TcKind]
149 newKindVars n = mappM (\ _ -> newKindVar) (nOfThem n ())
150 \end{code}
151
152
153 %************************************************************************
154 %*                                                                      *
155         SkolemTvs (immutable)
156 %*                                                                      *
157 %************************************************************************
158
159 \begin{code}
160 mkSkolTyVar :: Name -> Kind -> SkolemInfo -> TcTyVar
161 mkSkolTyVar name kind info = mkTcTyVar name kind (SkolemTv info)
162
163 tcSkolSigType :: SkolemInfo -> Type -> TcM ([TcTyVar], TcThetaType, TcType)
164 -- Instantiate a type signature with skolem constants, but 
165 -- do *not* give them fresh names, because we want the name to
166 -- be in the type environment -- it is lexically scoped.
167 tcSkolSigType info ty = tcInstType (\tvs -> return (tcSkolSigTyVars info tvs)) ty
168
169 tcSkolSigTyVars :: SkolemInfo -> [TyVar] -> [TcTyVar]
170 -- Make skolem constants, but do *not* give them new names, as above
171 tcSkolSigTyVars info tyvars = [ mkSkolTyVar (tyVarName tv) (tyVarKind tv) info
172                               | tv <- tyvars ]
173
174 tcInstSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
175 -- Instantiate a type with fresh skolem constants
176 tcInstSkolType info ty = tcInstType (tcInstSkolTyVars info) ty
177
178 tcInstSkolTyVar :: SkolemInfo -> TyVar -> TcM TcTyVar
179 tcInstSkolTyVar info tyvar
180   = do  { uniq <- newUnique
181         ; let name = setNameUnique (tyVarName tyvar) uniq
182               kind = tyVarKind tyvar
183         ; return (mkSkolTyVar name kind info) }
184
185 tcInstSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
186 tcInstSkolTyVars info tyvars = mapM (tcInstSkolTyVar info) tyvars
187 \end{code}
188
189
190 %************************************************************************
191 %*                                                                      *
192         MetaTvs (meta type variables; mutable)
193 %*                                                                      *
194 %************************************************************************
195
196 \begin{code}
197 newMetaTyVar :: BoxInfo -> Kind -> TcM TcTyVar
198 -- Make a new meta tyvar out of thin air
199 newMetaTyVar box_info kind
200   = do  { uniq <- newUnique
201         ; ref <- newMutVar Flexi ;
202         ; let name = mkSysTvName uniq fs 
203               fs = case box_info of
204                         BoxTv   -> FSLIT("bx")
205                         TauTv   -> FSLIT("t")
206                         SigTv _ -> FSLIT("a")
207         ; return (mkTcTyVar name kind (MetaTv box_info ref)) }
208
209 instMetaTyVar :: BoxInfo -> TyVar -> TcM TcTyVar
210 -- Make a new meta tyvar whose Name and Kind 
211 -- come from an existing TyVar
212 instMetaTyVar box_info tyvar
213   = do  { uniq <- newUnique
214         ; ref <- newMutVar Flexi ;
215         ; let name = setNameUnique (tyVarName tyvar) uniq
216               kind = tyVarKind tyvar
217         ; return (mkTcTyVar name kind (MetaTv box_info ref)) }
218
219 readMetaTyVar :: TyVar -> TcM MetaDetails
220 readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
221                       readMutVar (metaTvRef tyvar)
222
223 writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
224 #ifndef DEBUG
225 writeMetaTyVar tyvar ty = writeMutVar (metaTvRef tyvar) (Indirect ty)
226 #else
227 writeMetaTyVar tyvar ty
228   | not (isMetaTyVar tyvar)
229   = pprTrace "writeMetaTyVar" (ppr tyvar) $
230     returnM ()
231
232   | otherwise
233   = ASSERT( isMetaTyVar tyvar )
234     ASSERT2( k2 `isSubKind` k1, (ppr tyvar <+> ppr k1) $$ (ppr ty <+> ppr k2) )
235     do  { ASSERTM2( do { details <- readMetaTyVar tyvar; return (isFlexi details) }, ppr tyvar )
236         ; writeMutVar (metaTvRef tyvar) (Indirect ty) }
237   where
238     k1 = tyVarKind tyvar
239     k2 = typeKind ty
240 #endif
241 \end{code}
242
243
244 %************************************************************************
245 %*                                                                      *
246         MetaTvs: TauTvs
247 %*                                                                      *
248 %************************************************************************
249
250 \begin{code}
251 newFlexiTyVar :: Kind -> TcM TcTyVar
252 newFlexiTyVar kind = newMetaTyVar TauTv kind
253
254 newFlexiTyVarTy  :: Kind -> TcM TcType
255 newFlexiTyVarTy kind
256   = newFlexiTyVar kind  `thenM` \ tc_tyvar ->
257     returnM (TyVarTy tc_tyvar)
258
259 newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
260 newFlexiTyVarTys n kind = mappM newFlexiTyVarTy (nOfThem n kind)
261
262 tcInstTyVar :: TyVar -> TcM TcTyVar
263 -- Instantiate with a META type variable
264 tcInstTyVar tyvar = instMetaTyVar TauTv tyvar
265
266 tcInstTyVars :: [TyVar] -> TcM ([TcTyVar], [TcType], TvSubst)
267 -- Instantiate with META type variables
268 tcInstTyVars tyvars
269   = do  { tc_tvs <- mapM tcInstTyVar tyvars
270         ; let tys = mkTyVarTys tc_tvs
271         ; returnM (tc_tvs, tys, zipTopTvSubst tyvars tys) }
272                 -- Since the tyvars are freshly made,
273                 -- they cannot possibly be captured by
274                 -- any existing for-alls.  Hence zipTopTvSubst
275 \end{code}
276
277
278 %************************************************************************
279 %*                                                                      *
280         MetaTvs: SigTvs
281 %*                                                                      *
282 %************************************************************************
283
284 \begin{code}
285 tcInstSigTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
286 -- Instantiate with meta SigTvs
287 tcInstSigTyVars skol_info tyvars 
288   = mapM (instMetaTyVar (SigTv skol_info)) tyvars
289
290 zonkSigTyVar :: TcTyVar -> TcM TcTyVar
291 zonkSigTyVar sig_tv 
292   | isSkolemTyVar sig_tv 
293   = return sig_tv       -- Happens in the call in TcBinds.checkDistinctTyVars
294   | otherwise
295   = ASSERT( isSigTyVar sig_tv )
296     do { ty <- zonkTcTyVar sig_tv
297        ; return (tcGetTyVar "zonkSigTyVar" ty) }
298         -- 'ty' is bound to be a type variable, because SigTvs
299         -- can only be unified with type variables
300 \end{code}
301
302
303 %************************************************************************
304 %*                                                                      *
305         MetaTvs: BoxTvs
306 %*                                                                      *
307 %************************************************************************
308
309 \begin{code}
310 newBoxyTyVar :: Kind -> TcM BoxyTyVar
311 newBoxyTyVar kind = newMetaTyVar BoxTv kind
312
313 newBoxyTyVars :: [Kind] -> TcM [BoxyTyVar]
314 newBoxyTyVars kinds = mapM newBoxyTyVar kinds
315
316 newBoxyTyVarTys :: [Kind] -> TcM [BoxyType]
317 newBoxyTyVarTys kinds = do { tvs <- mapM newBoxyTyVar kinds; return (mkTyVarTys tvs) }
318
319 readFilledBox :: BoxyTyVar -> TcM TcType
320 -- Read the contents of the box, which should be filled in by now
321 readFilledBox box_tv = ASSERT( isBoxyTyVar box_tv )
322                        do { cts <- readMetaTyVar box_tv
323                           ; case cts of
324                                 Flexi       -> pprPanic "readFilledBox" (ppr box_tv)
325                                 Indirect ty -> return ty }
326
327 tcInstBoxyTyVar :: TyVar -> TcM BoxyTyVar
328 -- Instantiate with a BOXY type variable
329 tcInstBoxyTyVar tyvar = instMetaTyVar BoxTv tyvar
330
331 tcInstBoxy :: TcType -> TcM ([BoxyTyVar], BoxyThetaType, BoxySigmaType)
332 -- tcInstType instantiates the outer-level for-alls of a TcType with
333 -- fresh BOXY type variables, splits off the dictionary part, 
334 -- and returns the pieces.
335 tcInstBoxy ty = tcInstType (mapM tcInstBoxyTyVar) ty
336 \end{code}
337
338
339 %************************************************************************
340 %*                                                                      *
341 \subsection{Putting and getting  mutable type variables}
342 %*                                                                      *
343 %************************************************************************
344
345 But it's more fun to short out indirections on the way: If this
346 version returns a TyVar, then that TyVar is unbound.  If it returns
347 any other type, then there might be bound TyVars embedded inside it.
348
349 We return Nothing iff the original box was unbound.
350
351 \begin{code}
352 data LookupTyVarResult  -- The result of a lookupTcTyVar call
353   = DoneTv TcTyVarDetails       -- SkolemTv or virgin MetaTv
354   | IndirectTv TcType
355
356 lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult
357 lookupTcTyVar tyvar 
358   = case details of
359       SkolemTv _   -> return (DoneTv details)
360       MetaTv _ ref -> do { meta_details <- readMutVar ref
361                          ; case meta_details of
362                             Indirect ty -> return (IndirectTv ty)
363                             Flexi       -> return (DoneTv details) }
364   where
365     details =  tcTyVarDetails tyvar
366
367 {- 
368 -- gaw 2004 We aren't shorting anything out anymore, at least for now
369 getTcTyVar tyvar
370   | not (isTcTyVar tyvar)
371   = pprTrace "getTcTyVar" (ppr tyvar) $
372     returnM (Just (mkTyVarTy tyvar))
373
374   | otherwise
375   = ASSERT2( isTcTyVar tyvar, ppr tyvar )
376     readMetaTyVar tyvar                         `thenM` \ maybe_ty ->
377     case maybe_ty of
378         Just ty -> short_out ty                         `thenM` \ ty' ->
379                    writeMetaTyVar tyvar (Just ty')      `thenM_`
380                    returnM (Just ty')
381
382         Nothing    -> returnM Nothing
383
384 short_out :: TcType -> TcM TcType
385 short_out ty@(TyVarTy tyvar)
386   | not (isTcTyVar tyvar)
387   = returnM ty
388
389   | otherwise
390   = readMetaTyVar tyvar `thenM` \ maybe_ty ->
391     case maybe_ty of
392         Just ty' -> short_out ty'                       `thenM` \ ty' ->
393                     writeMetaTyVar tyvar (Just ty')     `thenM_`
394                     returnM ty'
395
396         other    -> returnM ty
397
398 short_out other_ty = returnM other_ty
399 -}
400 \end{code}
401
402
403 %************************************************************************
404 %*                                                                      *
405 \subsection{Zonking -- the exernal interfaces}
406 %*                                                                      *
407 %************************************************************************
408
409 -----------------  Type variables
410
411 \begin{code}
412 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
413 zonkTcTyVars tyvars = mappM zonkTcTyVar tyvars
414
415 zonkTcTyVarsAndFV :: [TcTyVar] -> TcM TcTyVarSet
416 zonkTcTyVarsAndFV tyvars = mappM zonkTcTyVar tyvars     `thenM` \ tys ->
417                            returnM (tyVarsOfTypes tys)
418
419 zonkTcTyVar :: TcTyVar -> TcM TcType
420 zonkTcTyVar tyvar = ASSERT( isTcTyVar tyvar )
421                     zonk_tc_tyvar (\ tv -> returnM (TyVarTy tv)) tyvar
422 \end{code}
423
424 -----------------  Types
425
426 \begin{code}
427 zonkTcType :: TcType -> TcM TcType
428 zonkTcType ty = zonkType (\ tv -> returnM (TyVarTy tv)) ty
429
430 zonkTcTypes :: [TcType] -> TcM [TcType]
431 zonkTcTypes tys = mappM zonkTcType tys
432
433 zonkTcClassConstraints cts = mappM zonk cts
434     where zonk (clas, tys)
435             = zonkTcTypes tys   `thenM` \ new_tys ->
436               returnM (clas, new_tys)
437
438 zonkTcThetaType :: TcThetaType -> TcM TcThetaType
439 zonkTcThetaType theta = mappM zonkTcPredType theta
440
441 zonkTcPredType :: TcPredType -> TcM TcPredType
442 zonkTcPredType (ClassP c ts)
443   = zonkTcTypes ts      `thenM` \ new_ts ->
444     returnM (ClassP c new_ts)
445 zonkTcPredType (IParam n t)
446   = zonkTcType t        `thenM` \ new_t ->
447     returnM (IParam n new_t)
448 \end{code}
449
450 -------------------  These ...ToType, ...ToKind versions
451                      are used at the end of type checking
452
453 \begin{code}
454 zonkQuantifiedTyVar :: TcTyVar -> TcM TyVar
455 -- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it.
456 -- It might be a meta TyVar, in which case we freeze it into an ordinary TyVar.
457 -- When we do this, we also default the kind -- see notes with Kind.defaultKind
458 -- The meta tyvar is updated to point to the new regular TyVar.  Now any 
459 -- bound occurences of the original type variable will get zonked to 
460 -- the immutable version.
461 --
462 -- We leave skolem TyVars alone; they are immutable.
463 zonkQuantifiedTyVar tv
464   | isSkolemTyVar tv = return tv
465         -- It might be a skolem type variable, 
466         -- for example from a user type signature
467
468   | otherwise   -- It's a meta-type-variable
469   = do  { details <- readMetaTyVar tv
470
471         -- Create the new, frozen, regular type variable
472         ; let final_kind = defaultKind (tyVarKind tv)
473               final_tv   = mkTyVar (tyVarName tv) final_kind
474
475         -- Bind the meta tyvar to the new tyvar
476         ; case details of
477             Indirect ty -> WARN( True, ppr tv $$ ppr ty ) 
478                            return ()
479                 -- [Sept 04] I don't think this should happen
480                 -- See note [Silly Type Synonym]
481
482             Flexi -> writeMetaTyVar tv (mkTyVarTy final_tv)
483
484         -- Return the new tyvar
485         ; return final_tv }
486 \end{code}
487
488 [Silly Type Synonyms]
489
490 Consider this:
491         type C u a = u  -- Note 'a' unused
492
493         foo :: (forall a. C u a -> C u a) -> u
494         foo x = ...
495
496         bar :: Num u => u
497         bar = foo (\t -> t + t)
498
499 * From the (\t -> t+t) we get type  {Num d} =>  d -> d
500   where d is fresh.
501
502 * Now unify with type of foo's arg, and we get:
503         {Num (C d a)} =>  C d a -> C d a
504   where a is fresh.
505
506 * Now abstract over the 'a', but float out the Num (C d a) constraint
507   because it does not 'really' mention a.  (see exactTyVarsOfType)
508   The arg to foo becomes
509         /\a -> \t -> t+t
510
511 * So we get a dict binding for Num (C d a), which is zonked to give
512         a = ()
513   [Note Sept 04: now that we are zonking quantified type variables
514   on construction, the 'a' will be frozen as a regular tyvar on
515   quantification, so the floated dict will still have type (C d a).
516   Which renders this whole note moot; happily!]
517
518 * Then the /\a abstraction has a zonked 'a' in it.
519
520 All very silly.   I think its harmless to ignore the problem.  We'll end up with
521 a /\a in the final result but all the occurrences of a will be zonked to ()
522
523
524 %************************************************************************
525 %*                                                                      *
526 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
527 %*                                                                      *
528 %*              For internal use only!                                  *
529 %*                                                                      *
530 %************************************************************************
531
532 \begin{code}
533 -- For unbound, mutable tyvars, zonkType uses the function given to it
534 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
535 --      type variable and zonks the kind too
536
537 zonkType :: (TcTyVar -> TcM Type)       -- What to do with unbound mutable type variables
538                                         -- see zonkTcType, and zonkTcTypeToType
539          -> TcType
540          -> TcM Type
541 zonkType unbound_var_fn ty
542   = go ty
543   where
544     go (NoteTy _ ty2)    = go ty2       -- Discard free-tyvar annotations
545                          
546     go (TyConApp tc tys) = mappM go tys `thenM` \ tys' ->
547                            returnM (TyConApp tc tys')
548                             
549     go (PredTy p)        = go_pred p            `thenM` \ p' ->
550                            returnM (PredTy p')
551                          
552     go (FunTy arg res)   = go arg               `thenM` \ arg' ->
553                            go res               `thenM` \ res' ->
554                            returnM (FunTy arg' res')
555                          
556     go (AppTy fun arg)   = go fun               `thenM` \ fun' ->
557                            go arg               `thenM` \ arg' ->
558                            returnM (mkAppTy fun' arg')
559                 -- NB the mkAppTy; we might have instantiated a
560                 -- type variable to a type constructor, so we need
561                 -- to pull the TyConApp to the top.
562
563         -- The two interesting cases!
564     go (TyVarTy tyvar) | isTcTyVar tyvar = zonk_tc_tyvar unbound_var_fn tyvar
565                        | otherwise       = return (TyVarTy tyvar)
566                 -- Ordinary (non Tc) tyvars occur inside quantified types
567
568     go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar )
569                              go ty              `thenM` \ ty' ->
570                              returnM (ForAllTy tyvar ty')
571
572     go_pred (ClassP c tys) = mappM go tys       `thenM` \ tys' ->
573                              returnM (ClassP c tys')
574     go_pred (IParam n ty)  = go ty              `thenM` \ ty' ->
575                              returnM (IParam n ty')
576
577 zonk_tc_tyvar :: (TcTyVar -> TcM Type)          -- What to do for an unbound mutable variable
578               -> TcTyVar -> TcM TcType
579 zonk_tc_tyvar unbound_var_fn tyvar 
580   | not (isMetaTyVar tyvar)     -- Skolems
581   = returnM (TyVarTy tyvar)
582
583   | otherwise                   -- Mutables
584   = do  { cts <- readMetaTyVar tyvar
585         ; case cts of
586             Flexi       -> unbound_var_fn tyvar    -- Unbound meta type variable
587             Indirect ty -> zonkType unbound_var_fn ty  }
588 \end{code}
589
590
591
592 %************************************************************************
593 %*                                                                      *
594                         Zonking kinds
595 %*                                                                      *
596 %************************************************************************
597
598 \begin{code}
599 readKindVar  :: KindVar -> TcM (Maybe TcKind)
600 writeKindVar :: KindVar -> TcKind -> TcM ()
601 readKindVar  kv = readMutVar (kindVarRef kv)
602 writeKindVar kv val = writeMutVar (kindVarRef kv) (Just val)
603
604 -------------
605 zonkTcKind :: TcKind -> TcM TcKind
606 zonkTcKind (FunKind k1 k2) = do { k1' <- zonkTcKind k1
607                                 ; k2' <- zonkTcKind k2
608                                 ; returnM (FunKind k1' k2') }
609 zonkTcKind k@(KindVar kv) = do { mb_kind <- readKindVar kv 
610                                ; case mb_kind of
611                                     Nothing -> returnM k
612                                     Just k  -> zonkTcKind k }
613 zonkTcKind other_kind = returnM other_kind
614
615 -------------
616 zonkTcKindToKind :: TcKind -> TcM Kind
617 zonkTcKindToKind (FunKind k1 k2) = do { k1' <- zonkTcKindToKind k1
618                                       ; k2' <- zonkTcKindToKind k2
619                                       ; returnM (FunKind k1' k2') }
620
621 zonkTcKindToKind (KindVar kv) = do { mb_kind <- readKindVar kv 
622                                    ; case mb_kind of
623                                        Nothing -> return liftedTypeKind
624                                        Just k  -> zonkTcKindToKind k }
625
626 zonkTcKindToKind OpenTypeKind = returnM liftedTypeKind  -- An "Open" kind defaults to *
627 zonkTcKindToKind other_kind   = returnM other_kind
628 \end{code}
629                         
630 %************************************************************************
631 %*                                                                      *
632 \subsection{Checking a user type}
633 %*                                                                      *
634 %************************************************************************
635
636 When dealing with a user-written type, we first translate it from an HsType
637 to a Type, performing kind checking, and then check various things that should 
638 be true about it.  We don't want to perform these checks at the same time
639 as the initial translation because (a) they are unnecessary for interface-file
640 types and (b) when checking a mutually recursive group of type and class decls,
641 we can't "look" at the tycons/classes yet.  Also, the checks are are rather
642 diverse, and used to really mess up the other code.
643
644 One thing we check for is 'rank'.  
645
646         Rank 0:         monotypes (no foralls)
647         Rank 1:         foralls at the front only, Rank 0 inside
648         Rank 2:         foralls at the front, Rank 1 on left of fn arrow,
649
650         basic ::= tyvar | T basic ... basic
651
652         r2  ::= forall tvs. cxt => r2a
653         r2a ::= r1 -> r2a | basic
654         r1  ::= forall tvs. cxt => r0
655         r0  ::= r0 -> r0 | basic
656         
657 Another thing is to check that type synonyms are saturated. 
658 This might not necessarily show up in kind checking.
659         type A i = i
660         data T k = MkT (k Int)
661         f :: T A        -- BAD!
662
663         
664 \begin{code}
665 checkValidType :: UserTypeCtxt -> Type -> TcM ()
666 -- Checks that the type is valid for the given context
667 checkValidType ctxt ty
668   = traceTc (text "checkValidType" <+> ppr ty)  `thenM_`
669     doptM Opt_GlasgowExts       `thenM` \ gla_exts ->
670     let 
671         rank | gla_exts = Arbitrary
672              | otherwise
673              = case ctxt of     -- Haskell 98
674                  GenPatCtxt     -> Rank 0
675                  LamPatSigCtxt  -> Rank 0
676                  BindPatSigCtxt -> Rank 0
677                  DefaultDeclCtxt-> Rank 0
678                  ResSigCtxt     -> Rank 0
679                  TySynCtxt _    -> Rank 0
680                  ExprSigCtxt    -> Rank 1
681                  FunSigCtxt _   -> Rank 1
682                  ConArgCtxt _   -> Rank 1       -- We are given the type of the entire
683                                                 -- constructor, hence rank 1
684                  ForSigCtxt _   -> Rank 1
685                  RuleSigCtxt _  -> Rank 1
686                  SpecInstCtxt   -> Rank 1
687
688         actual_kind = typeKind ty
689
690         kind_ok = case ctxt of
691                         TySynCtxt _  -> True    -- Any kind will do
692                         ResSigCtxt   -> isOpenTypeKind   actual_kind
693                         ExprSigCtxt  -> isOpenTypeKind   actual_kind
694                         GenPatCtxt   -> isLiftedTypeKind actual_kind
695                         ForSigCtxt _ -> isLiftedTypeKind actual_kind
696                         other        -> isArgTypeKind    actual_kind
697         
698         ubx_tup | not gla_exts = UT_NotOk
699                 | otherwise    = case ctxt of
700                                    TySynCtxt _ -> UT_Ok
701                                    ExprSigCtxt -> UT_Ok
702                                    other       -> UT_NotOk
703                 -- Unboxed tuples ok in function results,
704                 -- but for type synonyms we allow them even at
705                 -- top level
706     in
707         -- Check that the thing has kind Type, and is lifted if necessary
708     checkTc kind_ok (kindErr actual_kind)       `thenM_`
709
710         -- Check the internal validity of the type itself
711     check_poly_type rank ubx_tup ty             `thenM_`
712
713     traceTc (text "checkValidType done" <+> ppr ty)
714 \end{code}
715
716
717 \begin{code}
718 data Rank = Rank Int | Arbitrary
719
720 decRank :: Rank -> Rank
721 decRank Arbitrary = Arbitrary
722 decRank (Rank n)  = Rank (n-1)
723
724 ----------------------------------------
725 data UbxTupFlag = UT_Ok | UT_NotOk
726         -- The "Ok" version means "ok if -fglasgow-exts is on"
727
728 ----------------------------------------
729 check_poly_type :: Rank -> UbxTupFlag -> Type -> TcM ()
730 check_poly_type (Rank 0) ubx_tup ty 
731   = check_tau_type (Rank 0) ubx_tup ty
732
733 check_poly_type rank ubx_tup ty 
734   | null tvs && null theta
735   = check_tau_type rank ubx_tup ty
736   | otherwise
737   = do  { check_valid_theta SigmaCtxt theta
738         ; check_poly_type rank ubx_tup tau      -- Allow foralls to right of arrow
739         ; checkFreeness tvs theta
740         ; checkAmbiguity tvs theta (tyVarsOfType tau) }
741   where
742     (tvs, theta, tau) = tcSplitSigmaTy ty
743    
744 ----------------------------------------
745 check_arg_type :: Type -> TcM ()
746 -- The sort of type that can instantiate a type variable,
747 -- or be the argument of a type constructor.
748 -- Not an unboxed tuple, but now *can* be a forall (since impredicativity)
749 -- Other unboxed types are very occasionally allowed as type
750 -- arguments depending on the kind of the type constructor
751 -- 
752 -- For example, we want to reject things like:
753 --
754 --      instance Ord a => Ord (forall s. T s a)
755 -- and
756 --      g :: T s (forall b.b)
757 --
758 -- NB: unboxed tuples can have polymorphic or unboxed args.
759 --     This happens in the workers for functions returning
760 --     product types with polymorphic components.
761 --     But not in user code.
762 -- Anyway, they are dealt with by a special case in check_tau_type
763
764 check_arg_type ty 
765   = check_poly_type Arbitrary UT_NotOk ty       `thenM_` 
766     checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
767
768 ----------------------------------------
769 check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
770 -- Rank is allowed rank for function args
771 -- No foralls otherwise
772
773 check_tau_type rank ubx_tup ty@(ForAllTy _ _)       = failWithTc (forAllTyErr ty)
774 check_tau_type rank ubx_tup ty@(FunTy (PredTy _) _) = failWithTc (forAllTyErr ty)
775         -- Reject e.g. (Maybe (?x::Int => Int)), with a decent error message
776
777 -- Naked PredTys don't usually show up, but they can as a result of
778 --      {-# SPECIALISE instance Ord Char #-}
779 -- The Right Thing would be to fix the way that SPECIALISE instance pragmas
780 -- are handled, but the quick thing is just to permit PredTys here.
781 check_tau_type rank ubx_tup (PredTy sty) = getDOpts             `thenM` \ dflags ->
782                                            check_source_ty dflags TypeCtxt sty
783
784 check_tau_type rank ubx_tup (TyVarTy _)       = returnM ()
785 check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
786   = check_poly_type (decRank rank) UT_NotOk arg_ty      `thenM_`
787     check_poly_type rank           UT_Ok    res_ty
788
789 check_tau_type rank ubx_tup (AppTy ty1 ty2)
790   = check_arg_type ty1 `thenM_` check_arg_type ty2
791
792 check_tau_type rank ubx_tup (NoteTy other_note ty)
793   = check_tau_type rank ubx_tup ty
794
795 check_tau_type rank ubx_tup ty@(TyConApp tc tys)
796   | isSynTyCon tc       
797   = do  {       -- It's OK to have an *over-applied* type synonym
798                 --      data Tree a b = ...
799                 --      type Foo a = Tree [a]
800                 --      f :: Foo a b -> ...
801         ; case tcView ty of
802              Just ty' -> check_tau_type rank ubx_tup ty'        -- Check expansion
803              Nothing  -> failWithTc arity_msg
804
805         ; gla_exts <- doptM Opt_GlasgowExts
806         ; if gla_exts then
807         -- If -fglasgow-exts then don't check the type arguments
808         -- This allows us to instantiate a synonym defn with a 
809         -- for-all type, or with a partially-applied type synonym.
810         --      e.g.   type T a b = a
811         --             type S m   = m ()
812         --             f :: S (T Int)
813         -- Here, T is partially applied, so it's illegal in H98.
814         -- But if you expand S first, then T we get just 
815         --             f :: Int
816         -- which is fine.
817                 returnM ()
818           else
819                 -- For H98, do check the type args
820                 mappM_ check_arg_type tys
821         }
822     
823   | isUnboxedTupleTyCon tc
824   = doptM Opt_GlasgowExts                       `thenM` \ gla_exts ->
825     checkTc (ubx_tup_ok gla_exts) ubx_tup_msg   `thenM_`
826     mappM_ (check_tau_type (Rank 0) UT_Ok) tys  
827                 -- Args are allowed to be unlifted, or
828                 -- more unboxed tuples, so can't use check_arg_ty
829
830   | otherwise
831   = mappM_ check_arg_type tys
832
833   where
834     ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
835
836     n_args    = length tys
837     tc_arity  = tyConArity tc
838
839     arity_msg   = arityErr "Type synonym" (tyConName tc) tc_arity n_args
840     ubx_tup_msg = ubxArgTyErr ty
841
842 ----------------------------------------
843 forAllTyErr     ty = ptext SLIT("Illegal polymorphic or qualified type:") <+> ppr ty
844 unliftedArgErr  ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr ty
845 ubxArgTyErr     ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr ty
846 kindErr kind       = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
847 \end{code}
848
849
850
851 %************************************************************************
852 %*                                                                      *
853 \subsection{Checking a theta or source type}
854 %*                                                                      *
855 %************************************************************************
856
857 \begin{code}
858 -- Enumerate the contexts in which a "source type", <S>, can occur
859 --      Eq a 
860 -- or   ?x::Int
861 -- or   r <: {x::Int}
862 -- or   (N a) where N is a newtype
863
864 data SourceTyCtxt
865   = ClassSCCtxt Name    -- Superclasses of clas
866                         --      class <S> => C a where ...
867   | SigmaCtxt           -- Theta part of a normal for-all type
868                         --      f :: <S> => a -> a
869   | DataTyCtxt Name     -- Theta part of a data decl
870                         --      data <S> => T a = MkT a
871   | TypeCtxt            -- Source type in an ordinary type
872                         --      f :: N a -> N a
873   | InstThetaCtxt       -- Context of an instance decl
874                         --      instance <S> => C [a] where ...
875                 
876 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
877 pprSourceTyCtxt SigmaCtxt       = ptext SLIT("the context of a polymorphic type")
878 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
879 pprSourceTyCtxt InstThetaCtxt   = ptext SLIT("the context of an instance declaration")
880 pprSourceTyCtxt TypeCtxt        = ptext SLIT("the context of a type")
881 \end{code}
882
883 \begin{code}
884 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
885 checkValidTheta ctxt theta 
886   = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
887
888 -------------------------
889 check_valid_theta ctxt []
890   = returnM ()
891 check_valid_theta ctxt theta
892   = getDOpts                                    `thenM` \ dflags ->
893     warnTc (notNull dups) (dupPredWarn dups)    `thenM_`
894     mappM_ (check_source_ty dflags ctxt) theta
895   where
896     (_,dups) = removeDups tcCmpPred theta
897
898 -------------------------
899 check_source_ty dflags ctxt pred@(ClassP cls tys)
900   =     -- Class predicates are valid in all contexts
901     checkTc (arity == n_tys) arity_err          `thenM_`
902
903         -- Check the form of the argument types
904     mappM_ check_arg_type tys                           `thenM_`
905     checkTc (check_class_pred_tys dflags ctxt tys)
906             (predTyVarErr pred $$ how_to_allow)
907
908   where
909     class_name = className cls
910     arity      = classArity cls
911     n_tys      = length tys
912     arity_err  = arityErr "Class" class_name arity n_tys
913     how_to_allow = parens (ptext SLIT("Use -fglasgow-exts to permit this"))
914
915 check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
916         -- Implicit parameters only allows in type
917         -- signatures; not in instance decls, superclasses etc
918         -- The reason for not allowing implicit params in instances is a bit subtle
919         -- If we allowed        instance (?x::Int, Eq a) => Foo [a] where ...
920         -- then when we saw (e :: (?x::Int) => t) it would be unclear how to 
921         -- discharge all the potential usas of the ?x in e.   For example, a
922         -- constraint Foo [Int] might come out of e,and applying the
923         -- instance decl would show up two uses of ?x.
924
925 -- Catch-all
926 check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
927
928 -------------------------
929 check_class_pred_tys dflags ctxt tys 
930   = case ctxt of
931         TypeCtxt      -> True   -- {-# SPECIALISE instance Eq (T Int) #-} is fine
932         InstThetaCtxt -> gla_exts || undecidable_ok || all tcIsTyVarTy tys
933                                 -- Further checks on head and theta in
934                                 -- checkInstTermination
935         other         -> gla_exts || all tyvar_head tys
936   where
937     gla_exts       = dopt Opt_GlasgowExts dflags
938     undecidable_ok = dopt Opt_AllowUndecidableInstances dflags
939
940 -------------------------
941 tyvar_head ty                   -- Haskell 98 allows predicates of form 
942   | tcIsTyVarTy ty = True       --      C (a ty1 .. tyn)
943   | otherwise                   -- where a is a type variable
944   = case tcSplitAppTy_maybe ty of
945         Just (ty, _) -> tyvar_head ty
946         Nothing      -> False
947 \end{code}
948
949 Check for ambiguity
950 ~~~~~~~~~~~~~~~~~~~
951           forall V. P => tau
952 is ambiguous if P contains generic variables
953 (i.e. one of the Vs) that are not mentioned in tau
954
955 However, we need to take account of functional dependencies
956 when we speak of 'mentioned in tau'.  Example:
957         class C a b | a -> b where ...
958 Then the type
959         forall x y. (C x y) => x
960 is not ambiguous because x is mentioned and x determines y
961
962 NB; the ambiguity check is only used for *user* types, not for types
963 coming from inteface files.  The latter can legitimately have
964 ambiguous types. Example
965
966    class S a where s :: a -> (Int,Int)
967    instance S Char where s _ = (1,1)
968    f:: S a => [a] -> Int -> (Int,Int)
969    f (_::[a]) x = (a*x,b)
970         where (a,b) = s (undefined::a)
971
972 Here the worker for f gets the type
973         fw :: forall a. S a => Int -> (# Int, Int #)
974
975 If the list of tv_names is empty, we have a monotype, and then we
976 don't need to check for ambiguity either, because the test can't fail
977 (see is_ambig).
978
979 \begin{code}
980 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
981 checkAmbiguity forall_tyvars theta tau_tyvars
982   = mappM_ complain (filter is_ambig theta)
983   where
984     complain pred     = addErrTc (ambigErr pred)
985     extended_tau_vars = grow theta tau_tyvars
986
987         -- Only a *class* predicate can give rise to ambiguity
988         -- An *implicit parameter* cannot.  For example:
989         --      foo :: (?x :: [a]) => Int
990         --      foo = length ?x
991         -- is fine.  The call site will suppply a particular 'x'
992     is_ambig pred     = isClassPred  pred &&
993                         any ambig_var (varSetElems (tyVarsOfPred pred))
994
995     ambig_var ct_var  = (ct_var `elem` forall_tyvars) &&
996                         not (ct_var `elemVarSet` extended_tau_vars)
997
998 ambigErr pred
999   = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
1000          nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
1001                  ptext SLIT("must be reachable from the type after the '=>'"))]
1002 \end{code}
1003     
1004 In addition, GHC insists that at least one type variable
1005 in each constraint is in V.  So we disallow a type like
1006         forall a. Eq b => b -> b
1007 even in a scope where b is in scope.
1008
1009 \begin{code}
1010 checkFreeness forall_tyvars theta
1011   = mappM_ complain (filter is_free theta)
1012   where    
1013     is_free pred     =  not (isIPPred pred)
1014                      && not (any bound_var (varSetElems (tyVarsOfPred pred)))
1015     bound_var ct_var = ct_var `elem` forall_tyvars
1016     complain pred    = addErrTc (freeErr pred)
1017
1018 freeErr pred
1019   = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
1020                    ptext SLIT("are already in scope"),
1021          nest 4 (ptext SLIT("(at least one must be universally quantified here)"))
1022     ]
1023 \end{code}
1024
1025 \begin{code}
1026 checkThetaCtxt ctxt theta
1027   = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
1028           ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
1029
1030 badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
1031 predTyVarErr pred  = sep [ptext SLIT("Non type-variable argument"),
1032                           nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
1033 dupPredWarn dups   = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
1034
1035 arityErr kind name n m
1036   = hsep [ text kind, quotes (ppr name), ptext SLIT("should have"),
1037            n_arguments <> comma, text "but has been given", int m]
1038     where
1039         n_arguments | n == 0 = ptext SLIT("no arguments")
1040                     | n == 1 = ptext SLIT("1 argument")
1041                     | True   = hsep [int n, ptext SLIT("arguments")]
1042 \end{code}
1043
1044
1045 %************************************************************************
1046 %*                                                                      *
1047 \subsection{Checking for a decent instance head type}
1048 %*                                                                      *
1049 %************************************************************************
1050
1051 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1052 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1053
1054 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1055 flag is on, or (2)~the instance is imported (they must have been
1056 compiled elsewhere). In these cases, we let them go through anyway.
1057
1058 We can also have instances for functions: @instance Foo (a -> b) ...@.
1059
1060 \begin{code}
1061 checkValidInstHead :: Type -> TcM (Class, [TcType])
1062
1063 checkValidInstHead ty   -- Should be a source type
1064   = case tcSplitPredTy_maybe ty of {
1065         Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
1066         Just pred -> 
1067
1068     case getClassPredTys_maybe pred of {
1069         Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
1070         Just (clas,tys) ->
1071
1072     getDOpts                                    `thenM` \ dflags ->
1073     mappM_ check_arg_type tys                   `thenM_`
1074     check_inst_head dflags clas tys             `thenM_`
1075     returnM (clas, tys)
1076     }}
1077
1078 check_inst_head dflags clas tys
1079         -- If GlasgowExts then check at least one isn't a type variable
1080   | dopt Opt_GlasgowExts dflags
1081   = mapM_ check_one tys
1082
1083         -- WITH HASKELL 98, MUST HAVE C (T a b c)
1084   | otherwise
1085   = checkTc (isSingleton tys && tcValidInstHeadTy first_ty)
1086             (instTypeErr (pprClassPred clas tys) head_shape_msg)
1087
1088   where
1089     (first_ty : _) = tys
1090
1091     head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
1092                              text "where T is not a synonym, and a,b,c are distinct type variables")
1093
1094         -- For now, I only allow tau-types (not polytypes) in 
1095         -- the head of an instance decl.  
1096         --      E.g.  instance C (forall a. a->a) is rejected
1097         -- One could imagine generalising that, but I'm not sure
1098         -- what all the consequences might be
1099     check_one ty = do { check_tau_type (Rank 0) UT_NotOk ty
1100                       ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
1101
1102 instTypeErr pp_ty msg
1103   = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty, 
1104          nest 4 msg]
1105 \end{code}
1106
1107
1108 %************************************************************************
1109 %*                                                                      *
1110 \subsection{Checking instance for termination}
1111 %*                                                                      *
1112 %************************************************************************
1113
1114
1115 \begin{code}
1116 checkValidInstance :: [TyVar] -> ThetaType -> Class -> [TcType] -> TcM ()
1117 checkValidInstance tyvars theta clas inst_tys
1118   = do  { gla_exts <- doptM Opt_GlasgowExts
1119         ; undecidable_ok <- doptM Opt_AllowUndecidableInstances
1120
1121         ; checkValidTheta InstThetaCtxt theta
1122         ; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys)
1123
1124         -- Check that instance inference will terminate (if we care)
1125         -- For Haskell 98, checkValidTheta has already done that
1126         ; when (gla_exts && not undecidable_ok) $
1127                checkInstTermination theta inst_tys
1128         
1129         -- The Coverage Condition
1130         ; checkTc (undecidable_ok || checkInstCoverage clas inst_tys)
1131                   (instTypeErr (pprClassPred clas inst_tys) msg)
1132         }
1133   where
1134     msg  = parens (ptext SLIT("the Coverage Condition fails for one of the functional dependencies"))
1135 \end{code}
1136
1137 Termination test: each assertion in the context satisfies
1138  (1) no variable has more occurrences in the assertion than in the head, and
1139  (2) the assertion has fewer constructors and variables (taken together
1140      and counting repetitions) than the head.
1141 This is only needed with -fglasgow-exts, as Haskell 98 restrictions
1142 (which have already been checked) guarantee termination. 
1143
1144 The underlying idea is that 
1145
1146     for any ground substitution, each assertion in the
1147     context has fewer type constructors than the head.
1148
1149
1150 \begin{code}
1151 checkInstTermination :: ThetaType -> [TcType] -> TcM ()
1152 checkInstTermination theta tys
1153   = do  { mappM_ (check_nomore (fvTypes tys))    theta
1154         ; mappM_ (check_smaller (sizeTypes tys)) theta }
1155
1156 check_nomore :: [TyVar] -> PredType -> TcM ()
1157 check_nomore fvs pred
1158   = checkTc (null (fvPred pred \\ fvs))
1159             (predUndecErr pred nomoreMsg $$ parens undecidableMsg)
1160
1161 check_smaller :: Int -> PredType -> TcM ()
1162 check_smaller n pred
1163   = checkTc (sizePred pred < n)
1164             (predUndecErr pred smallerMsg $$ parens undecidableMsg)
1165
1166 predUndecErr pred msg = sep [msg,
1167                         nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
1168
1169 nomoreMsg = ptext SLIT("Variable occurs more often in a constraint than in the instance head")
1170 smallerMsg = ptext SLIT("Constraint is no smaller than the instance head")
1171 undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
1172
1173 -- Free variables of a type, retaining repetitions, and expanding synonyms
1174 fvType :: Type -> [TyVar]
1175 fvType ty | Just exp_ty <- tcView ty = fvType exp_ty
1176 fvType (TyVarTy tv)        = [tv]
1177 fvType (TyConApp _ tys)    = fvTypes tys
1178 fvType (NoteTy _ ty)       = fvType ty
1179 fvType (PredTy pred)       = fvPred pred
1180 fvType (FunTy arg res)     = fvType arg ++ fvType res
1181 fvType (AppTy fun arg)     = fvType fun ++ fvType arg
1182 fvType (ForAllTy tyvar ty) = filter (/= tyvar) (fvType ty)
1183
1184 fvTypes :: [Type] -> [TyVar]
1185 fvTypes tys                = concat (map fvType tys)
1186
1187 fvPred :: PredType -> [TyVar]
1188 fvPred (ClassP _ tys')     = fvTypes tys'
1189 fvPred (IParam _ ty)       = fvType ty
1190
1191 -- Size of a type: the number of variables and constructors
1192 sizeType :: Type -> Int
1193 sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty
1194 sizeType (TyVarTy _)       = 1
1195 sizeType (TyConApp _ tys)  = sizeTypes tys + 1
1196 sizeType (NoteTy _ ty)     = sizeType ty
1197 sizeType (PredTy pred)     = sizePred pred
1198 sizeType (FunTy arg res)   = sizeType arg + sizeType res + 1
1199 sizeType (AppTy fun arg)   = sizeType fun + sizeType arg
1200 sizeType (ForAllTy _ ty)   = sizeType ty
1201
1202 sizeTypes :: [Type] -> Int
1203 sizeTypes xs               = sum (map sizeType xs)
1204
1205 sizePred :: PredType -> Int
1206 sizePred (ClassP _ tys')   = sizeTypes tys'
1207 sizePred (IParam _ ty)     = sizeType ty
1208 \end{code}