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