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