Loosen the conditions for -XUndecidableInstances; fixes Trac #4200
[ghc.git] / compiler / typecheck / TcMType.lhs
1 %
2 % (c) The University of Glasgow 2006
3 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 %
5
6 Monadic type operations
7
8 This module contains monadic operations over types that contain
9 mutable type variables
10
11 \begin{code}
12 module TcMType (
13   TcTyVar, TcKind, TcType, TcTauType, TcThetaType, TcTyVarSet,
14
15   --------------------------------
16   -- Creating new mutable type variables
17   newFlexiTyVar,
18   newFlexiTyVarTy,              -- Kind -> TcM TcType
19   newFlexiTyVarTys,             -- Int -> Kind -> TcM [TcType]
20   newKindVar, newKindVars, 
21
22   newMetaTyVar, readMetaTyVar, writeMetaTyVar, writeMetaTyVarRef,
23   isFilledMetaTyVar, isFlexiMetaTyVar,
24
25   --------------------------------
26   -- Creating new evidence variables
27   newEvVar, newCoVar, newEvVars,
28   newWantedCoVar, writeWantedCoVar, readWantedCoVar, 
29   newIP, newDict, newSelfDict, isSelfDict,
30
31   newWantedEvVar, newWantedEvVars, 
32   newKindConstraint,
33   newTcEvBinds, addTcEvBind,
34
35   --------------------------------
36   -- Instantiation
37   tcInstTyVar, tcInstTyVars, tcInstSigTyVars,
38   tcInstType, tcInstSigType,
39   tcInstSkolTyVars, tcInstSkolTyVar, tcInstSkolType, 
40   tcSkolSigType, tcSkolSigTyVars, 
41
42   --------------------------------
43   -- Checking type validity
44   Rank, UserTypeCtxt(..), checkValidType, checkValidMonoType,
45   SourceTyCtxt(..), checkValidTheta, 
46   checkValidInstHead, checkValidInstance, 
47   checkInstTermination, checkValidTypeInst, checkTyFamFreeness, 
48   arityErr, 
49   growPredTyVars, growThetaTyVars, validDerivPred,
50
51   --------------------------------
52   -- Zonking
53   zonkType, mkZonkTcTyVar, zonkTcPredType, 
54   zonkTcTypeCarefully,
55   zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkSigTyVar,
56   zonkQuantifiedTyVar, zonkQuantifiedTyVars,
57   zonkTcType, zonkTcTypes, zonkTcThetaType,
58   zonkTcKindToKind, zonkTcKind, 
59   zonkImplication, zonkWanted, zonkEvVar, zonkWantedEvVar,
60   zonkTcTypeAndSubst,
61   tcGetGlobalTyVars, 
62
63   readKindVar, writeKindVar
64   ) where
65
66 #include "HsVersions.h"
67
68 -- friends:
69 import TypeRep
70 import TcType
71 import Type
72 import Coercion
73 import Class
74 import TyCon
75 import Var
76
77 -- others:
78 import HsSyn            -- HsType
79 import TcRnMonad        -- TcType, amongst others
80 import Id
81 import FunDeps
82 import Name
83 import VarSet
84 import ErrUtils
85 import DynFlags
86 import Util
87 import Maybes
88 import ListSetOps
89 import BasicTypes
90 import SrcLoc
91 import Outputable
92 import FastString
93 import Bag
94
95 import Control.Monad
96 import Data.List        ( (\\) )
97 \end{code}
98
99
100 %************************************************************************
101 %*                                                                      *
102         Kind variables
103 %*                                                                      *
104 %************************************************************************
105
106 \begin{code}
107 newKindVar :: TcM TcKind
108 newKindVar = do { uniq <- newUnique
109                 ; ref <- newMutVar Flexi
110                 ; return (mkTyVarTy (mkKindVar uniq ref)) }
111
112 newKindVars :: Int -> TcM [TcKind]
113 newKindVars n = mapM (\ _ -> newKindVar) (nOfThem n ())
114 \end{code}
115
116
117 %************************************************************************
118 %*                                                                      *
119      Evidence variables; range over constraints we can abstract over
120 %*                                                                      *
121 %************************************************************************
122
123 \begin{code}
124 newEvVars :: TcThetaType -> TcM [EvVar]
125 newEvVars theta = mapM newEvVar theta
126
127 newWantedEvVar :: TcPredType -> TcM EvVar 
128 newWantedEvVar (EqPred ty1 ty2) = newWantedCoVar ty1 ty2
129 newWantedEvVar (ClassP cls tys) = newDict cls tys
130 newWantedEvVar (IParam ip ty)   = newIP ip ty
131
132 newWantedEvVars :: TcThetaType -> TcM [EvVar] 
133 newWantedEvVars theta = mapM newWantedEvVar theta 
134
135 newWantedCoVar :: TcType -> TcType -> TcM CoVar 
136 newWantedCoVar ty1 ty2 = newCoVar ty1 ty2
137
138 -- We used to create a mutable co-var
139 {-
140 -- A wanted coercion variable is a MetaTyVar
141 -- that can be filled in with its binding
142   = do { uniq <- newUnique 
143        ; ref <- newMutVar Flexi 
144        ; let name = mkSysTvName uniq (fsLit "c")
145              kind = mkPredTy (EqPred ty1 ty2) 
146        ; return (mkTcTyVar name kind (MetaTv TauTv ref)) }
147 -}
148
149 --------------
150 newEvVar :: TcPredType -> TcM EvVar
151 -- Creates new *rigid* variables for predicates
152 newEvVar (EqPred ty1 ty2) = newCoVar ty1 ty2
153 newEvVar (ClassP cls tys) = newDict  cls tys
154 newEvVar (IParam ip ty)   = newIP    ip ty
155
156 newCoVar :: TcType -> TcType -> TcM CoVar
157 newCoVar ty1 ty2
158   = do { name <- newName (mkTyVarOccFS (fsLit "co"))
159        ; return (mkCoVar name (mkPredTy (EqPred ty1 ty2))) }
160
161 newIP :: IPName Name -> TcType -> TcM IpId
162 newIP ip ty
163   = do  { name <- newName (getOccName (ipNameName ip))
164         ; return (mkLocalId name (mkPredTy (IParam ip ty))) }
165
166 newDict :: Class -> [TcType] -> TcM DictId
167 newDict cls tys 
168   = do { name <- newName (mkDictOcc (getOccName cls))
169        ; return (mkLocalId name (mkPredTy (ClassP cls tys))) }
170
171 newName :: OccName -> TcM Name
172 newName occ
173   = do { uniq <- newUnique
174        ; loc  <- getSrcSpanM
175        ; return (mkInternalName uniq occ loc) }
176
177 -----------------
178 newKindConstraint :: Type -> Kind -> TcM (CoVar, Type)
179 -- Create a new wanted CoVar that constrains the type
180 -- to have the specified kind
181 newKindConstraint ty kind
182   = do { ty_k <- newFlexiTyVarTy kind
183        ; co_var <- newWantedCoVar ty ty_k
184        ; return (co_var, ty_k) }
185
186 -----------------
187 newSelfDict :: Class -> [TcType] -> TcM DictId
188 -- Make a dictionary for "self". It behaves just like a normal DictId
189 -- except that it responds True to isSelfDict
190 -- This is used only to suppress confusing error reports
191 newSelfDict cls tys 
192   = do { uniq <- newUnique
193        ; let name = mkSystemName uniq selfDictOcc
194        ; return (mkLocalId name (mkPredTy (ClassP cls tys))) }
195
196 selfDictOcc :: OccName
197 selfDictOcc = mkVarOcc "self"
198
199 isSelfDict :: EvVar -> Bool
200 isSelfDict v = isSystemName (Var.varName v)
201   -- Notice that all *other* evidence variables get Internal Names
202 \end{code}
203
204
205 %************************************************************************
206 %*                                                                      *
207         SkolemTvs (immutable)
208 %*                                                                      *
209 %************************************************************************
210
211 \begin{code}
212 tcInstType :: ([TyVar] -> TcM [TcTyVar])                -- How to instantiate the type variables
213            -> TcType                                    -- Type to instantiate
214            -> TcM ([TcTyVar], TcThetaType, TcType)      -- Result
215                 -- (type vars (excl coercion vars), preds (incl equalities), rho)
216 tcInstType inst_tyvars ty
217   = case tcSplitForAllTys ty of
218         ([],     rho) -> let    -- There may be overloading despite no type variables;
219                                 --      (?x :: Int) => Int -> Int
220                            (theta, tau) = tcSplitPhiTy rho
221                          in
222                          return ([], theta, tau)
223
224         (tyvars, rho) -> do { tyvars' <- inst_tyvars tyvars
225
226                             ; let  tenv = zipTopTvSubst tyvars (mkTyVarTys tyvars')
227                                 -- Either the tyvars are freshly made, by inst_tyvars,
228                                 -- or (in the call from tcSkolSigType) any nested foralls
229                                 -- have different binders.  Either way, zipTopTvSubst is ok
230
231                             ; let  (theta, tau) = tcSplitPhiTy (substTy tenv rho)
232                             ; return (tyvars', theta, tau) }
233
234 mkSkolTyVar :: Name -> Kind -> SkolemInfo -> TcTyVar
235 mkSkolTyVar name kind info = mkTcTyVar name kind (SkolemTv info)
236
237 tcSkolSigType :: SkolemInfo -> Type -> TcM ([TcTyVar], TcThetaType, TcType)
238 -- Instantiate a type signature with skolem constants, but 
239 -- do *not* give them fresh names, because we want the name to
240 -- be in the type environment: it is lexically scoped.
241 tcSkolSigType info ty = tcInstType (\tvs -> return (tcSkolSigTyVars info tvs)) ty
242
243 tcSkolSigTyVars :: SkolemInfo -> [TyVar] -> [TcTyVar]
244 -- Make skolem constants, but do *not* give them new names, as above
245 tcSkolSigTyVars info tyvars = [ mkSkolTyVar (tyVarName tv) (tyVarKind tv) info
246                               | tv <- tyvars ]
247
248 tcInstSkolTyVar :: SkolemInfo -> TyVar -> TcM TcTyVar
249 -- Instantiate the tyvar, using 
250 --      * the occ-name and kind of the supplied tyvar, 
251 --      * the unique from the monad,
252 --      * the location either from the tyvar (skol_info = SigSkol)
253 --                     or from the monad (otehrwise)
254 tcInstSkolTyVar skol_info tyvar
255   = do  { uniq <- newUnique
256         ; loc <- case skol_info of
257                     SigSkol {} -> return (getSrcSpan old_name)
258                     _          -> getSrcSpanM
259         ; let new_name = mkInternalName uniq occ loc
260         ; return (mkSkolTyVar new_name kind skol_info) }
261   where
262     old_name = tyVarName tyvar
263     occ      = nameOccName old_name
264     kind     = tyVarKind tyvar
265
266 tcInstSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
267 -- Get the location from the monad
268 tcInstSkolTyVars info tyvars 
269   = mapM (tcInstSkolTyVar info) tyvars
270
271 tcInstSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
272 -- Instantiate a type with fresh skolem constants
273 -- Binding location comes from the monad
274 tcInstSkolType info ty = tcInstType (tcInstSkolTyVars info) ty
275
276 tcInstSigType :: Bool -> Name -> TcType -> TcM ([TcTyVar], TcThetaType, TcRhoType)
277 -- Instantiate with skolems or meta SigTvs; depending on use_skols
278 -- Always take location info from the supplied tyvars
279 tcInstSigType use_skols name ty
280   | use_skols
281   = tcInstType (tcInstSkolTyVars (SigSkol (FunSigCtxt name))) ty
282   | otherwise
283   = tcInstType tcInstSigTyVars ty
284
285 tcInstSigTyVars :: [TyVar] -> TcM [TcTyVar]
286 -- Make meta SigTv type variables for patten-bound scoped type varaibles
287 -- We use SigTvs for them, so that they can't unify with arbitrary types
288 tcInstSigTyVars = mapM (\tv -> instMetaTyVar (SigTv (tyVarName tv)) tv)
289                 -- ToDo: the "function binding site is bogus
290 \end{code}
291
292
293 %************************************************************************
294 %*                                                                      *
295         MetaTvs (meta type variables; mutable)
296 %*                                                                      *
297 %************************************************************************
298
299 \begin{code}
300 newMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar
301 -- Make a new meta tyvar out of thin air
302 newMetaTyVar meta_info kind
303   = do  { uniq <- newUnique
304         ; ref <- newMutVar Flexi
305         ; let name = mkSysTvName uniq fs 
306               fs = case meta_info of
307                         TauTv   -> fsLit "t"
308                         SigTv _ -> fsLit "a"
309         ; return (mkTcTyVar name kind (MetaTv meta_info ref)) }
310
311 instMetaTyVar :: MetaInfo -> TyVar -> TcM TcTyVar
312 -- Make a new meta tyvar whose Name and Kind 
313 -- come from an existing TyVar
314 instMetaTyVar meta_info tyvar
315   = do  { uniq <- newUnique
316         ; ref <- newMutVar Flexi
317         ; let name = setNameUnique (tyVarName tyvar) uniq
318               kind = tyVarKind tyvar
319         ; return (mkTcTyVar name kind (MetaTv meta_info ref)) }
320
321 readMetaTyVar :: TyVar -> TcM MetaDetails
322 readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
323                       readMutVar (metaTvRef tyvar)
324
325 readWantedCoVar :: CoVar -> TcM MetaDetails
326 readWantedCoVar covar = ASSERT2( isMetaTyVar covar, ppr covar )
327                         readMutVar (metaTvRef covar)
328
329
330
331 isFilledMetaTyVar :: TyVar -> TcM Bool
332 -- True of a filled-in (Indirect) meta type variable
333 isFilledMetaTyVar tv
334   | not (isTcTyVar tv) = return False
335   | MetaTv _ ref <- tcTyVarDetails tv
336   = do  { details <- readMutVar ref
337         ; return (isIndirect details) }
338   | otherwise = return False
339
340 isFlexiMetaTyVar :: TyVar -> TcM Bool
341 -- True of a un-filled-in (Flexi) meta type variable
342 isFlexiMetaTyVar tv
343   | not (isTcTyVar tv) = return False
344   | MetaTv _ ref <- tcTyVarDetails tv
345   = do  { details <- readMutVar ref
346         ; return (isFlexi details) }
347   | otherwise = return False
348
349 --------------------
350 writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
351 -- Write into a currently-empty MetaTyVar
352
353 writeMetaTyVar tyvar ty
354   | not debugIsOn 
355   = writeMetaTyVarRef tyvar (metaTvRef tyvar) ty
356
357 -- Everything from here on only happens if DEBUG is on
358   | not (isTcTyVar tyvar)
359   = WARN( True, text "Writing to non-tc tyvar" <+> ppr tyvar )
360     return ()
361
362   | MetaTv _ ref <- tcTyVarDetails tyvar
363   = writeMetaTyVarRef tyvar ref ty
364
365   | otherwise
366   = WARN( True, text "Writing to non-meta tyvar" <+> ppr tyvar )
367     return ()
368
369 writeWantedCoVar :: CoVar -> Coercion -> TcM () 
370 writeWantedCoVar cv co = writeMetaTyVar cv co 
371
372 --------------------
373 writeMetaTyVarRef :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM ()
374 -- Here the tyvar is for error checking only; 
375 -- the ref cell must be for the same tyvar
376 writeMetaTyVarRef tyvar ref ty
377   | not debugIsOn 
378   = do { traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
379        ; writeMutVar ref (Indirect ty) }
380
381 -- Everything from here on only happens if DEBUG is on
382   | not (isPredTy tv_kind)   -- Don't check kinds for updates to coercion variables
383   , not (ty_kind `isSubKind` tv_kind)
384   = WARN( True, hang (text "Ill-kinded update to meta tyvar")
385                    2 (ppr tyvar $$ ppr tv_kind $$ ppr ty $$ ppr ty_kind) )
386     return ()
387
388   | otherwise
389   = do { meta_details <- readMutVar ref; 
390        ; WARN( not (isFlexi meta_details), 
391                 hang (text "Double update of meta tyvar")
392                    2 (ppr tyvar $$ ppr meta_details) )
393
394          traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
395        ; writeMutVar ref (Indirect ty) }
396   where
397     tv_kind = tyVarKind tyvar
398     ty_kind = typeKind ty
399 \end{code}
400
401
402 %************************************************************************
403 %*                                                                      *
404         MetaTvs: TauTvs
405 %*                                                                      *
406 %************************************************************************
407
408 \begin{code}
409 newFlexiTyVar :: Kind -> TcM TcTyVar
410 newFlexiTyVar kind = newMetaTyVar TauTv kind
411
412 newFlexiTyVarTy  :: Kind -> TcM TcType
413 newFlexiTyVarTy kind = do
414     tc_tyvar <- newFlexiTyVar kind
415     return (TyVarTy tc_tyvar)
416
417 newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
418 newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind)
419
420 tcInstTyVar :: TyVar -> TcM TcTyVar
421 -- Instantiate with a META type variable
422 tcInstTyVar tyvar = instMetaTyVar TauTv tyvar
423
424 tcInstTyVars :: [TyVar] -> TcM ([TcTyVar], [TcType], TvSubst)
425 -- Instantiate with META type variables
426 tcInstTyVars tyvars
427   = do  { tc_tvs <- mapM tcInstTyVar tyvars
428         ; let tys = mkTyVarTys tc_tvs
429         ; return (tc_tvs, tys, zipTopTvSubst tyvars tys) }
430                 -- Since the tyvars are freshly made,
431                 -- they cannot possibly be captured by
432                 -- any existing for-alls.  Hence zipTopTvSubst
433 \end{code}
434
435
436 %************************************************************************
437 %*                                                                      *
438         MetaTvs: SigTvs
439 %*                                                                      *
440 %************************************************************************
441
442 \begin{code}
443 zonkSigTyVar :: TcTyVar -> TcM TcTyVar
444 zonkSigTyVar sig_tv 
445   | isSkolemTyVar sig_tv 
446   = return sig_tv       -- Happens in the call in TcBinds.checkDistinctTyVars
447   | otherwise
448   = ASSERT( isSigTyVar sig_tv )
449     do { ty <- zonkTcTyVar sig_tv
450        ; return (tcGetTyVar "zonkSigTyVar" ty) }
451         -- 'ty' is bound to be a type variable, because SigTvs
452         -- can only be unified with type variables
453 \end{code}
454
455
456
457 %************************************************************************
458 %*                                                                      *
459 \subsection{Zonking -- the exernal interfaces}
460 %*                                                                      *
461 %************************************************************************
462
463 @tcGetGlobalTyVars@ returns a fully-zonked set of tyvars free in the environment.
464 To improve subsequent calls to the same function it writes the zonked set back into
465 the environment.
466
467 \begin{code}
468 tcGetGlobalTyVars :: TcM TcTyVarSet
469 tcGetGlobalTyVars
470   = do { (TcLclEnv {tcl_tyvars = gtv_var}) <- getLclEnv
471        ; gbl_tvs  <- readMutVar gtv_var
472        ; gbl_tvs' <- zonkTcTyVarsAndFV (varSetElems gbl_tvs)
473        ; writeMutVar gtv_var gbl_tvs'
474        ; return gbl_tvs' }
475 \end{code}
476
477 -----------------  Type variables
478
479 \begin{code}
480 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
481 zonkTcTyVars tyvars = mapM zonkTcTyVar tyvars
482
483 zonkTcTyVarsAndFV :: [TcTyVar] -> TcM TcTyVarSet
484 zonkTcTyVarsAndFV tyvars = tyVarsOfTypes <$> mapM zonkTcTyVar tyvars
485
486 -----------------  Types
487
488 zonkTcTypeCarefully :: TcType -> TcM TcType
489 -- Do not zonk type variables free in the environment
490 zonkTcTypeCarefully ty
491   = do { env_tvs <- tcGetGlobalTyVars
492        ; zonkType (zonk_tv env_tvs) ty }
493   where
494     zonk_tv env_tvs tv
495       | tv `elemVarSet` env_tvs 
496       = return (TyVarTy tv)
497       | otherwise
498       = ASSERT( isTcTyVar tv )
499         case tcTyVarDetails tv of
500           SkolemTv {}  -> return (TyVarTy tv)
501           FlatSkol ty  -> zonkType (zonk_tv env_tvs) ty
502           MetaTv _ ref -> do { cts <- readMutVar ref
503                              ; case cts of    
504                                  Flexi       -> return (TyVarTy tv)
505                                  Indirect ty -> zonkType (zonk_tv env_tvs) ty }
506
507 zonkTcType :: TcType -> TcM TcType
508 -- Simply look through all Flexis
509 zonkTcType ty = zonkType zonkTcTyVar ty
510
511 zonkTcTyVar :: TcTyVar -> TcM TcType
512 -- Simply look through all Flexis
513 zonkTcTyVar tv
514   = ASSERT2( isTcTyVar tv, ppr tv )
515     case tcTyVarDetails tv of
516       SkolemTv {}  -> return (TyVarTy tv)
517       FlatSkol ty  -> zonkTcType ty
518       MetaTv _ ref -> do { cts <- readMutVar ref
519                          ; case cts of    
520                              Flexi       -> return (TyVarTy tv)
521                              Indirect ty -> zonkTcType ty }
522
523 zonkTcTypeAndSubst :: TvSubst -> TcType -> TcM TcType
524 -- Zonk, and simultaneously apply a non-necessarily-idempotent substitution
525 zonkTcTypeAndSubst subst ty = zonkType zonk_tv ty
526   where
527     zonk_tv tv 
528       = case tcTyVarDetails tv of
529           SkolemTv {}  -> return (TyVarTy tv)
530           FlatSkol ty  -> zonkType zonk_tv ty
531           MetaTv _ ref -> do { cts <- readMutVar ref
532                              ; case cts of    
533                                  Flexi       -> zonk_flexi tv
534                                  Indirect ty -> zonkType zonk_tv ty }
535     zonk_flexi tv
536       = case lookupTyVar subst tv of
537           Just ty -> zonkType zonk_tv ty
538           Nothing -> return (TyVarTy tv)
539
540 zonkTcTypes :: [TcType] -> TcM [TcType]
541 zonkTcTypes tys = mapM zonkTcType tys
542
543 zonkTcThetaType :: TcThetaType -> TcM TcThetaType
544 zonkTcThetaType theta = mapM zonkTcPredType theta
545
546 zonkTcPredType :: TcPredType -> TcM TcPredType
547 zonkTcPredType (ClassP c ts)  = ClassP c <$> zonkTcTypes ts
548 zonkTcPredType (IParam n t)   = IParam n <$> zonkTcType t
549 zonkTcPredType (EqPred t1 t2) = EqPred <$> zonkTcType t1 <*> zonkTcType t2
550 \end{code}
551
552 -------------------  These ...ToType, ...ToKind versions
553                      are used at the end of type checking
554
555 \begin{code}
556 zonkQuantifiedTyVars :: [TcTyVar] -> TcM [TcTyVar]
557 zonkQuantifiedTyVars = mapM zonkQuantifiedTyVar
558
559 zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar
560 -- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it.
561 --
562 -- The quantified type variables often include meta type variables
563 -- we want to freeze them into ordinary type variables, and
564 -- default their kind (e.g. from OpenTypeKind to TypeKind)
565 --                      -- see notes with Kind.defaultKind
566 -- The meta tyvar is updated to point to the new skolem TyVar.  Now any 
567 -- bound occurences of the original type variable will get zonked to 
568 -- the immutable version.
569 --
570 -- We leave skolem TyVars alone; they are immutable.
571 zonkQuantifiedTyVar tv
572   | ASSERT2( isTcTyVar tv, ppr tv ) 
573     isSkolemTyVar tv 
574   = do { kind <- zonkTcType (tyVarKind tv)
575        ; return $ setTyVarKind tv kind
576        }
577         -- It might be a skolem type variable, 
578         -- for example from a user type signature
579
580   | otherwise   -- It's a meta-type-variable
581   = do  { details <- readMetaTyVar tv
582
583         -- Create the new, frozen, skolem type variable
584         -- We zonk to a skolem, not to a regular TcVar
585         -- See Note [Zonking to Skolem]
586         ; let final_kind = defaultKind (tyVarKind tv)
587               final_tv   = mkSkolTyVar (tyVarName tv) final_kind UnkSkol
588
589         -- Bind the meta tyvar to the new tyvar
590         ; case details of
591             Indirect ty -> WARN( True, ppr tv $$ ppr ty ) 
592                            return ()
593                 -- [Sept 04] I don't think this should happen
594                 -- See note [Silly Type Synonym]
595
596             Flexi -> writeMetaTyVar tv (mkTyVarTy final_tv)
597
598         -- Return the new tyvar
599         ; return final_tv }
600 \end{code}
601
602 \begin{code}
603 zonkImplication :: Implication -> TcM Implication
604 zonkImplication implic@(Implic { ic_env_tvs = env_tvs, ic_given = given 
605                                , ic_wanted = wanted })
606   = do { env_tvs' <- zonkTcTyVarsAndFV (varSetElems env_tvs)
607        ; given'   <- mapM zonkEvVar given
608        ; wanted'  <- mapBagM zonkWanted wanted
609        ; return (implic { ic_env_tvs = env_tvs', ic_given = given'
610                         , ic_wanted = wanted' }) }
611
612 zonkEvVar :: EvVar -> TcM EvVar
613 zonkEvVar var = do { ty' <- zonkTcType (varType var)
614                    ; return (setVarType var ty') }
615
616 zonkWanted :: WantedConstraint -> TcM WantedConstraint
617 zonkWanted (WcImplic imp) = do { imp' <- zonkImplication imp; return (WcImplic imp') }
618 zonkWanted (WcEvVar ev)   = do { ev' <- zonkWantedEvVar ev; return (WcEvVar ev') }
619
620 zonkWantedEvVar :: WantedEvVar -> TcM WantedEvVar
621 zonkWantedEvVar (WantedEvVar v l) = do { v' <- zonkEvVar v; return (WantedEvVar v' l) }
622 \end{code}
623
624
625 Note [Silly Type Synonyms]
626 ~~~~~~~~~~~~~~~~~~~~~~~~~~
627 Consider this:
628         type C u a = u  -- Note 'a' unused
629
630         foo :: (forall a. C u a -> C u a) -> u
631         foo x = ...
632
633         bar :: Num u => u
634         bar = foo (\t -> t + t)
635
636 * From the (\t -> t+t) we get type  {Num d} =>  d -> d
637   where d is fresh.
638
639 * Now unify with type of foo's arg, and we get:
640         {Num (C d a)} =>  C d a -> C d a
641   where a is fresh.
642
643 * Now abstract over the 'a', but float out the Num (C d a) constraint
644   because it does not 'really' mention a.  (see exactTyVarsOfType)
645   The arg to foo becomes
646         \/\a -> \t -> t+t
647
648 * So we get a dict binding for Num (C d a), which is zonked to give
649         a = ()
650   [Note Sept 04: now that we are zonking quantified type variables
651   on construction, the 'a' will be frozen as a regular tyvar on
652   quantification, so the floated dict will still have type (C d a).
653   Which renders this whole note moot; happily!]
654
655 * Then the \/\a abstraction has a zonked 'a' in it.
656
657 All very silly.   I think its harmless to ignore the problem.  We'll end up with
658 a \/\a in the final result but all the occurrences of a will be zonked to ()
659
660 Note [Zonking to Skolem]
661 ~~~~~~~~~~~~~~~~~~~~~~~~
662 We used to zonk quantified type variables to regular TyVars.  However, this
663 leads to problems.  Consider this program from the regression test suite:
664
665   eval :: Int -> String -> String -> String
666   eval 0 root actual = evalRHS 0 root actual
667
668   evalRHS :: Int -> a
669   evalRHS 0 root actual = eval 0 root actual
670
671 It leads to the deferral of an equality (wrapped in an implication constraint)
672
673   forall a. (String -> String -> String) ~ a
674
675 which is propagated up to the toplevel (see TcSimplify.tcSimplifyInferCheck).
676 In the meantime `a' is zonked and quantified to form `evalRHS's signature.
677 This has the *side effect* of also zonking the `a' in the deferred equality
678 (which at this point is being handed around wrapped in an implication
679 constraint).
680
681 Finally, the equality (with the zonked `a') will be handed back to the
682 simplifier by TcRnDriver.tcRnSrcDecls calling TcSimplify.tcSimplifyTop.
683 If we zonk `a' with a regular type variable, we will have this regular type
684 variable now floating around in the simplifier, which in many places assumes to
685 only see proper TcTyVars.
686
687 We can avoid this problem by zonking with a skolem.  The skolem is rigid
688 (which we require for a quantified variable), but is still a TcTyVar that the
689 simplifier knows how to deal with.
690
691
692 %************************************************************************
693 %*                                                                      *
694 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
695 %*                                                                      *
696 %*              For internal use only!                                  *
697 %*                                                                      *
698 %************************************************************************
699
700 \begin{code}
701 -- For unbound, mutable tyvars, zonkType uses the function given to it
702 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
703 --      type variable and zonks the kind too
704
705 zonkType :: (TcTyVar -> TcM Type)       -- What to do with unbound mutable type variables
706                                         -- see zonkTcType, and zonkTcTypeToType
707          -> TcType
708          -> TcM Type
709 zonkType zonk_tc_tyvar ty
710   = go ty
711   where
712     go (TyConApp tc tys) = do tys' <- mapM go tys
713                               return (TyConApp tc tys')
714
715     go (PredTy p)        = do p' <- go_pred p
716                               return (PredTy p')
717
718     go (FunTy arg res)   = do arg' <- go arg
719                               res' <- go res
720                               return (FunTy arg' res')
721
722     go (AppTy fun arg)   = do fun' <- go fun
723                               arg' <- go arg
724                               return (mkAppTy fun' arg')
725                 -- NB the mkAppTy; we might have instantiated a
726                 -- type variable to a type constructor, so we need
727                 -- to pull the TyConApp to the top.
728
729         -- The two interesting cases!
730     go (TyVarTy tyvar) | isTcTyVar tyvar = zonk_tc_tyvar tyvar
731                        | otherwise       = liftM TyVarTy $ 
732                                            zonkTyVar zonk_tc_tyvar tyvar
733                 -- Ordinary (non Tc) tyvars occur inside quantified types
734
735     go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar ) do
736                              ty' <- go ty
737                              tyvar' <- zonkTyVar zonk_tc_tyvar tyvar
738                              return (ForAllTy tyvar' ty')
739
740     go_pred (ClassP c tys)   = do tys' <- mapM go tys
741                                   return (ClassP c tys')
742     go_pred (IParam n ty)    = do ty' <- go ty
743                                   return (IParam n ty')
744     go_pred (EqPred ty1 ty2) = do ty1' <- go ty1
745                                   ty2' <- go ty2
746                                   return (EqPred ty1' ty2')
747
748 mkZonkTcTyVar :: (TcTyVar -> TcM Type)  -- What to do for an unbound mutable var
749               -> TcTyVar -> TcM TcType
750 mkZonkTcTyVar unbound_var_fn tyvar 
751   = ASSERT( isTcTyVar tyvar )
752     case tcTyVarDetails tyvar of
753       SkolemTv {}  -> return (TyVarTy tyvar)
754       FlatSkol ty  -> zonkType (mkZonkTcTyVar unbound_var_fn) ty
755       MetaTv _ ref -> do { cts <- readMutVar ref
756                          ; case cts of    
757                              Flexi       -> unbound_var_fn tyvar  
758                              Indirect ty -> zonkType (mkZonkTcTyVar unbound_var_fn) ty }
759
760 -- Zonk the kind of a non-TC tyvar in case it is a coercion variable 
761 -- (their kind contains types).
762 zonkTyVar :: (TcTyVar -> TcM Type)      -- What to do for a TcTyVar
763           -> TyVar -> TcM TyVar
764 zonkTyVar zonk_tc_tyvar tv 
765   | isCoVar tv
766   = do { kind <- zonkType zonk_tc_tyvar (tyVarKind tv)
767        ; return $ setTyVarKind tv kind }
768   | otherwise = return tv
769 \end{code}
770
771
772
773 %************************************************************************
774 %*                                                                      *
775                         Zonking kinds
776 %*                                                                      *
777 %************************************************************************
778
779 \begin{code}
780 readKindVar  :: KindVar -> TcM (MetaDetails)
781 writeKindVar :: KindVar -> TcKind -> TcM ()
782 readKindVar  kv = readMutVar (kindVarRef kv)
783 writeKindVar kv val = writeMutVar (kindVarRef kv) (Indirect val)
784
785 -------------
786 zonkTcKind :: TcKind -> TcM TcKind
787 zonkTcKind k = zonkTcType k
788
789 -------------
790 zonkTcKindToKind :: TcKind -> TcM Kind
791 -- When zonking a TcKind to a kind, we need to instantiate kind variables,
792 -- Haskell specifies that * is to be used, so we follow that.
793 zonkTcKindToKind k 
794   = zonkType (mkZonkTcTyVar (\ _ -> return liftedTypeKind)) k
795 \end{code}
796                         
797 %************************************************************************
798 %*                                                                      *
799 \subsection{Checking a user type}
800 %*                                                                      *
801 %************************************************************************
802
803 When dealing with a user-written type, we first translate it from an HsType
804 to a Type, performing kind checking, and then check various things that should 
805 be true about it.  We don't want to perform these checks at the same time
806 as the initial translation because (a) they are unnecessary for interface-file
807 types and (b) when checking a mutually recursive group of type and class decls,
808 we can't "look" at the tycons/classes yet.  Also, the checks are are rather
809 diverse, and used to really mess up the other code.
810
811 One thing we check for is 'rank'.  
812
813         Rank 0:         monotypes (no foralls)
814         Rank 1:         foralls at the front only, Rank 0 inside
815         Rank 2:         foralls at the front, Rank 1 on left of fn arrow,
816
817         basic ::= tyvar | T basic ... basic
818
819         r2  ::= forall tvs. cxt => r2a
820         r2a ::= r1 -> r2a | basic
821         r1  ::= forall tvs. cxt => r0
822         r0  ::= r0 -> r0 | basic
823         
824 Another thing is to check that type synonyms are saturated. 
825 This might not necessarily show up in kind checking.
826         type A i = i
827         data T k = MkT (k Int)
828         f :: T A        -- BAD!
829
830         
831 \begin{code}
832 checkValidType :: UserTypeCtxt -> Type -> TcM ()
833 -- Checks that the type is valid for the given context
834 checkValidType ctxt ty = do
835     traceTc "checkValidType" (ppr ty)
836     unboxed  <- xoptM Opt_UnboxedTuples
837     rank2    <- xoptM Opt_Rank2Types
838     rankn    <- xoptM Opt_RankNTypes
839     polycomp <- xoptM Opt_PolymorphicComponents
840     let 
841         gen_rank n | rankn     = ArbitraryRank
842                    | rank2     = Rank 2
843                    | otherwise = Rank n
844         rank
845           = case ctxt of
846                  DefaultDeclCtxt-> MustBeMonoType
847                  ResSigCtxt     -> MustBeMonoType
848                  LamPatSigCtxt  -> gen_rank 0
849                  BindPatSigCtxt -> gen_rank 0
850                  TySynCtxt _    -> gen_rank 0
851                  GenPatCtxt     -> gen_rank 1
852                         -- This one is a bit of a hack
853                         -- See the forall-wrapping in TcClassDcl.mkGenericInstance              
854
855                  ExprSigCtxt    -> gen_rank 1
856                  FunSigCtxt _   -> gen_rank 1
857                  ConArgCtxt _   | polycomp -> gen_rank 2
858                                 -- We are given the type of the entire
859                                 -- constructor, hence rank 1
860                                 | otherwise -> gen_rank 1
861
862                  ForSigCtxt _   -> gen_rank 1
863                  SpecInstCtxt   -> gen_rank 1
864                  ThBrackCtxt    -> gen_rank 1
865
866         actual_kind = typeKind ty
867
868         kind_ok = case ctxt of
869                         TySynCtxt _  -> True -- Any kind will do
870                         ThBrackCtxt  -> True -- Any kind will do
871                         ResSigCtxt   -> isSubOpenTypeKind actual_kind
872                         ExprSigCtxt  -> isSubOpenTypeKind actual_kind
873                         GenPatCtxt   -> isLiftedTypeKind actual_kind
874                         ForSigCtxt _ -> isLiftedTypeKind actual_kind
875                         _            -> isSubArgTypeKind actual_kind
876         
877         ubx_tup = case ctxt of
878                       TySynCtxt _ | unboxed -> UT_Ok
879                       ExprSigCtxt | unboxed -> UT_Ok
880                       ThBrackCtxt | unboxed -> UT_Ok
881                       _                     -> UT_NotOk
882
883         -- Check the internal validity of the type itself
884     check_type rank ubx_tup ty
885
886         -- Check that the thing has kind Type, and is lifted if necessary
887         -- Do this second, becuase we can't usefully take the kind of an 
888         -- ill-formed type such as (a~Int)
889     checkTc kind_ok (kindErr actual_kind)
890
891     traceTc "checkValidType done" (ppr ty)
892
893 checkValidMonoType :: Type -> TcM ()
894 checkValidMonoType ty = check_mono_type MustBeMonoType ty
895 \end{code}
896
897
898 \begin{code}
899 data Rank = ArbitraryRank         -- Any rank ok
900           | MustBeMonoType        -- Monotype regardless of flags
901           | TyConArgMonoType      -- Monotype but could be poly if -XImpredicativeTypes
902           | SynArgMonoType        -- Monotype but could be poly if -XLiberalTypeSynonyms
903           | Rank Int              -- Rank n, but could be more with -XRankNTypes
904
905 decRank :: Rank -> Rank           -- Function arguments
906 decRank (Rank 0)   = Rank 0
907 decRank (Rank n)   = Rank (n-1)
908 decRank other_rank = other_rank
909
910 nonZeroRank :: Rank -> Bool
911 nonZeroRank ArbitraryRank = True
912 nonZeroRank (Rank n)      = n>0
913 nonZeroRank _             = False
914
915 ----------------------------------------
916 data UbxTupFlag = UT_Ok | UT_NotOk
917         -- The "Ok" version means "ok if UnboxedTuples is on"
918
919 ----------------------------------------
920 check_mono_type :: Rank -> Type -> TcM ()       -- No foralls anywhere
921                                                 -- No unlifted types of any kind
922 check_mono_type rank ty
923    = do { check_type rank UT_NotOk ty
924         ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
925
926 check_type :: Rank -> UbxTupFlag -> Type -> TcM ()
927 -- The args say what the *type context* requires, independent
928 -- of *flag* settings.  You test the flag settings at usage sites.
929 -- 
930 -- Rank is allowed rank for function args
931 -- Rank 0 means no for-alls anywhere
932
933 check_type rank ubx_tup ty
934   | not (null tvs && null theta)
935   = do  { checkTc (nonZeroRank rank) (forAllTyErr rank ty)
936                 -- Reject e.g. (Maybe (?x::Int => Int)), 
937                 -- with a decent error message
938         ; check_valid_theta SigmaCtxt theta
939         ; check_type rank ubx_tup tau   -- Allow foralls to right of arrow
940         ; checkAmbiguity tvs theta (tyVarsOfType tau) }
941   where
942     (tvs, theta, tau) = tcSplitSigmaTy ty
943    
944 -- Naked PredTys should, I think, have been rejected before now
945 check_type _ _ ty@(PredTy {})
946   = failWithTc (text "Predicate" <+> ppr ty <+> text "used as a type") 
947
948 check_type _ _ (TyVarTy _) = return ()
949
950 check_type rank _ (FunTy arg_ty res_ty)
951   = do  { check_type (decRank rank) UT_NotOk arg_ty
952         ; check_type rank           UT_Ok    res_ty }
953
954 check_type rank _ (AppTy ty1 ty2)
955   = do  { check_arg_type rank ty1
956         ; check_arg_type rank ty2 }
957
958 check_type rank ubx_tup ty@(TyConApp tc tys)
959   | isSynTyCon tc
960   = do  {       -- Check that the synonym has enough args
961                 -- This applies equally to open and closed synonyms
962                 -- It's OK to have an *over-applied* type synonym
963                 --      data Tree a b = ...
964                 --      type Foo a = Tree [a]
965                 --      f :: Foo a b -> ...
966           checkTc (tyConArity tc <= length tys) arity_msg
967
968         -- See Note [Liberal type synonyms]
969         ; liberal <- xoptM Opt_LiberalTypeSynonyms
970         ; if not liberal || isSynFamilyTyCon tc then
971                 -- For H98 and synonym families, do check the type args
972                 mapM_ (check_mono_type SynArgMonoType) tys
973
974           else  -- In the liberal case (only for closed syns), expand then check
975           case tcView ty of   
976              Just ty' -> check_type rank ubx_tup ty' 
977              Nothing  -> pprPanic "check_tau_type" (ppr ty)
978     }
979     
980   | isUnboxedTupleTyCon tc
981   = do  { ub_tuples_allowed <- xoptM Opt_UnboxedTuples
982         ; checkTc (ubx_tup_ok ub_tuples_allowed) ubx_tup_msg
983
984         ; impred <- xoptM Opt_ImpredicativeTypes        
985         ; let rank' = if impred then ArbitraryRank else TyConArgMonoType
986                 -- c.f. check_arg_type
987                 -- However, args are allowed to be unlifted, or
988                 -- more unboxed tuples, so can't use check_arg_ty
989         ; mapM_ (check_type rank' UT_Ok) tys }
990
991   | otherwise
992   = mapM_ (check_arg_type rank) tys
993
994   where
995     ubx_tup_ok ub_tuples_allowed = case ubx_tup of
996                                    UT_Ok -> ub_tuples_allowed
997                                    _     -> False
998
999     n_args    = length tys
1000     tc_arity  = tyConArity tc
1001
1002     arity_msg   = arityErr "Type synonym" (tyConName tc) tc_arity n_args
1003     ubx_tup_msg = ubxArgTyErr ty
1004
1005 check_type _ _ ty = pprPanic "check_type" (ppr ty)
1006
1007 ----------------------------------------
1008 check_arg_type :: Rank -> Type -> TcM ()
1009 -- The sort of type that can instantiate a type variable,
1010 -- or be the argument of a type constructor.
1011 -- Not an unboxed tuple, but now *can* be a forall (since impredicativity)
1012 -- Other unboxed types are very occasionally allowed as type
1013 -- arguments depending on the kind of the type constructor
1014 -- 
1015 -- For example, we want to reject things like:
1016 --
1017 --      instance Ord a => Ord (forall s. T s a)
1018 -- and
1019 --      g :: T s (forall b.b)
1020 --
1021 -- NB: unboxed tuples can have polymorphic or unboxed args.
1022 --     This happens in the workers for functions returning
1023 --     product types with polymorphic components.
1024 --     But not in user code.
1025 -- Anyway, they are dealt with by a special case in check_tau_type
1026
1027 check_arg_type rank ty 
1028   = do  { impred <- xoptM Opt_ImpredicativeTypes
1029         ; let rank' = case rank of          -- Predictive => must be monotype
1030                         MustBeMonoType     -> MustBeMonoType  -- Monotype, regardless
1031                         _other | impred    -> ArbitraryRank
1032                                | otherwise -> TyConArgMonoType
1033                         -- Make sure that MustBeMonoType is propagated, 
1034                         -- so that we don't suggest -XImpredicativeTypes in
1035                         --    (Ord (forall a.a)) => a -> a
1036                         -- and so that if it Must be a monotype, we check that it is!
1037
1038         ; check_type rank' UT_NotOk ty
1039         ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
1040
1041 ----------------------------------------
1042 forAllTyErr :: Rank -> Type -> SDoc
1043 forAllTyErr rank ty 
1044    = vcat [ hang (ptext (sLit "Illegal polymorphic or qualified type:")) 2 (ppr ty)
1045           , suggestion ]
1046   where
1047     suggestion = case rank of
1048                    Rank _ -> ptext (sLit "Perhaps you intended to use -XRankNTypes or -XRank2Types")
1049                    TyConArgMonoType -> ptext (sLit "Perhaps you intended to use -XImpredicativeTypes")
1050                    SynArgMonoType -> ptext (sLit "Perhaps you intended to use -XLiberalTypeSynonyms")
1051                    _ -> empty      -- Polytype is always illegal
1052
1053 unliftedArgErr, ubxArgTyErr :: Type -> SDoc
1054 unliftedArgErr  ty = sep [ptext (sLit "Illegal unlifted type:"), ppr ty]
1055 ubxArgTyErr     ty = sep [ptext (sLit "Illegal unboxed tuple type as function argument:"), ppr ty]
1056
1057 kindErr :: Kind -> SDoc
1058 kindErr kind       = sep [ptext (sLit "Expecting an ordinary type, but found a type of kind"), ppr kind]
1059 \end{code}
1060
1061 Note [Liberal type synonyms]
1062 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1063 If -XLiberalTypeSynonyms is on, expand closed type synonyms *before*
1064 doing validity checking.  This allows us to instantiate a synonym defn
1065 with a for-all type, or with a partially-applied type synonym.
1066         e.g.   type T a b = a
1067                type S m   = m ()
1068                f :: S (T Int)
1069 Here, T is partially applied, so it's illegal in H98.  But if you
1070 expand S first, then T we get just
1071                f :: Int
1072 which is fine.
1073
1074 IMPORTANT: suppose T is a type synonym.  Then we must do validity
1075 checking on an appliation (T ty1 ty2)
1076
1077         *either* before expansion (i.e. check ty1, ty2)
1078         *or* after expansion (i.e. expand T ty1 ty2, and then check)
1079         BUT NOT BOTH
1080
1081 If we do both, we get exponential behaviour!!
1082
1083   data TIACons1 i r c = c i ::: r c
1084   type TIACons2 t x = TIACons1 t (TIACons1 t x)
1085   type TIACons3 t x = TIACons2 t (TIACons1 t x)
1086   type TIACons4 t x = TIACons2 t (TIACons2 t x)
1087   type TIACons7 t x = TIACons4 t (TIACons3 t x)
1088
1089
1090 %************************************************************************
1091 %*                                                                      *
1092 \subsection{Checking a theta or source type}
1093 %*                                                                      *
1094 %************************************************************************
1095
1096 \begin{code}
1097 -- Enumerate the contexts in which a "source type", <S>, can occur
1098 --      Eq a 
1099 -- or   ?x::Int
1100 -- or   r <: {x::Int}
1101 -- or   (N a) where N is a newtype
1102
1103 data SourceTyCtxt
1104   = ClassSCCtxt Name    -- Superclasses of clas
1105                         --      class <S> => C a where ...
1106   | SigmaCtxt           -- Theta part of a normal for-all type
1107                         --      f :: <S> => a -> a
1108   | DataTyCtxt Name     -- Theta part of a data decl
1109                         --      data <S> => T a = MkT a
1110   | TypeCtxt            -- Source type in an ordinary type
1111                         --      f :: N a -> N a
1112   | InstThetaCtxt       -- Context of an instance decl
1113                         --      instance <S> => C [a] where ...
1114                 
1115 pprSourceTyCtxt :: SourceTyCtxt -> SDoc
1116 pprSourceTyCtxt (ClassSCCtxt c) = ptext (sLit "the super-classes of class") <+> quotes (ppr c)
1117 pprSourceTyCtxt SigmaCtxt       = ptext (sLit "the context of a polymorphic type")
1118 pprSourceTyCtxt (DataTyCtxt tc) = ptext (sLit "the context of the data type declaration for") <+> quotes (ppr tc)
1119 pprSourceTyCtxt InstThetaCtxt   = ptext (sLit "the context of an instance declaration")
1120 pprSourceTyCtxt TypeCtxt        = ptext (sLit "the context of a type")
1121 \end{code}
1122
1123 \begin{code}
1124 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
1125 checkValidTheta ctxt theta 
1126   = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
1127
1128 -------------------------
1129 check_valid_theta :: SourceTyCtxt -> [PredType] -> TcM ()
1130 check_valid_theta _ []
1131   = return ()
1132 check_valid_theta ctxt theta = do
1133     dflags <- getDOpts
1134     warnTc (notNull dups) (dupPredWarn dups)
1135     mapM_ (check_pred_ty dflags ctxt) theta
1136   where
1137     (_,dups) = removeDups tcCmpPred theta
1138
1139 -------------------------
1140 check_pred_ty :: DynFlags -> SourceTyCtxt -> PredType -> TcM ()
1141 check_pred_ty dflags ctxt pred@(ClassP cls tys)
1142   = do {        -- Class predicates are valid in all contexts
1143        ; checkTc (arity == n_tys) arity_err
1144
1145                 -- Check the form of the argument types
1146        ; mapM_ checkValidMonoType tys
1147        ; checkTc (check_class_pred_tys dflags ctxt tys)
1148                  (predTyVarErr pred $$ how_to_allow)
1149        }
1150   where
1151     class_name = className cls
1152     arity      = classArity cls
1153     n_tys      = length tys
1154     arity_err  = arityErr "Class" class_name arity n_tys
1155     how_to_allow = parens (ptext (sLit "Use -XFlexibleContexts to permit this"))
1156
1157
1158 check_pred_ty dflags _ pred@(EqPred ty1 ty2)
1159   = do {        -- Equational constraints are valid in all contexts if type
1160                 -- families are permitted
1161        ; checkTc (xopt Opt_TypeFamilies dflags) (eqPredTyErr pred)
1162
1163                 -- Check the form of the argument types
1164        ; checkValidMonoType ty1
1165        ; checkValidMonoType ty2
1166        }
1167
1168 check_pred_ty _ SigmaCtxt (IParam _ ty) = checkValidMonoType ty
1169         -- Implicit parameters only allowed in type
1170         -- signatures; not in instance decls, superclasses etc
1171         -- The reason for not allowing implicit params in instances is a bit
1172         -- subtle.
1173         -- If we allowed        instance (?x::Int, Eq a) => Foo [a] where ...
1174         -- then when we saw (e :: (?x::Int) => t) it would be unclear how to 
1175         -- discharge all the potential usas of the ?x in e.   For example, a
1176         -- constraint Foo [Int] might come out of e,and applying the
1177         -- instance decl would show up two uses of ?x.
1178
1179 -- Catch-all
1180 check_pred_ty _ _ sty = failWithTc (badPredTyErr sty)
1181
1182 -------------------------
1183 check_class_pred_tys :: DynFlags -> SourceTyCtxt -> [Type] -> Bool
1184 check_class_pred_tys dflags ctxt tys 
1185   = case ctxt of
1186         TypeCtxt      -> True   -- {-# SPECIALISE instance Eq (T Int) #-} is fine
1187         InstThetaCtxt -> flexible_contexts || undecidable_ok || all tcIsTyVarTy tys
1188                                 -- Further checks on head and theta in
1189                                 -- checkInstTermination
1190         _             -> flexible_contexts || all tyvar_head tys
1191   where
1192     flexible_contexts = xopt Opt_FlexibleContexts dflags
1193     undecidable_ok = xopt Opt_UndecidableInstances dflags
1194
1195 -------------------------
1196 tyvar_head :: Type -> Bool
1197 tyvar_head ty                   -- Haskell 98 allows predicates of form 
1198   | tcIsTyVarTy ty = True       --      C (a ty1 .. tyn)
1199   | otherwise                   -- where a is a type variable
1200   = case tcSplitAppTy_maybe ty of
1201         Just (ty, _) -> tyvar_head ty
1202         Nothing      -> False
1203 \end{code}
1204
1205 Check for ambiguity
1206 ~~~~~~~~~~~~~~~~~~~
1207           forall V. P => tau
1208 is ambiguous if P contains generic variables
1209 (i.e. one of the Vs) that are not mentioned in tau
1210
1211 However, we need to take account of functional dependencies
1212 when we speak of 'mentioned in tau'.  Example:
1213         class C a b | a -> b where ...
1214 Then the type
1215         forall x y. (C x y) => x
1216 is not ambiguous because x is mentioned and x determines y
1217
1218 NB; the ambiguity check is only used for *user* types, not for types
1219 coming from inteface files.  The latter can legitimately have
1220 ambiguous types. Example
1221
1222    class S a where s :: a -> (Int,Int)
1223    instance S Char where s _ = (1,1)
1224    f:: S a => [a] -> Int -> (Int,Int)
1225    f (_::[a]) x = (a*x,b)
1226         where (a,b) = s (undefined::a)
1227
1228 Here the worker for f gets the type
1229         fw :: forall a. S a => Int -> (# Int, Int #)
1230
1231 If the list of tv_names is empty, we have a monotype, and then we
1232 don't need to check for ambiguity either, because the test can't fail
1233 (see is_ambig).
1234
1235 In addition, GHC insists that at least one type variable
1236 in each constraint is in V.  So we disallow a type like
1237         forall a. Eq b => b -> b
1238 even in a scope where b is in scope.
1239
1240 \begin{code}
1241 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
1242 checkAmbiguity forall_tyvars theta tau_tyvars
1243   = mapM_ complain (filter is_ambig theta)
1244   where
1245     complain pred     = addErrTc (ambigErr pred)
1246     extended_tau_vars = growThetaTyVars theta tau_tyvars
1247
1248         -- See Note [Implicit parameters and ambiguity] in TcSimplify
1249     is_ambig pred     = isClassPred  pred &&
1250                         any ambig_var (varSetElems (tyVarsOfPred pred))
1251
1252     ambig_var ct_var  = (ct_var `elem` forall_tyvars) &&
1253                         not (ct_var `elemVarSet` extended_tau_vars)
1254
1255 ambigErr :: PredType -> SDoc
1256 ambigErr pred
1257   = sep [ptext (sLit "Ambiguous constraint") <+> quotes (pprPred pred),
1258          nest 2 (ptext (sLit "At least one of the forall'd type variables mentioned by the constraint") $$
1259                  ptext (sLit "must be reachable from the type after the '=>'"))]
1260 \end{code}
1261
1262 Note [Growing the tau-tvs using constraints]
1263 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1264 (growInstsTyVars insts tvs) is the result of extending the set 
1265     of tyvars tvs using all conceivable links from pred
1266
1267 E.g. tvs = {a}, preds = {H [a] b, K (b,Int) c, Eq e}
1268 Then grow precs tvs = {a,b,c}
1269
1270 \begin{code}
1271 growThetaTyVars :: TcThetaType -> TyVarSet -> TyVarSet
1272 -- See Note [Growing the tau-tvs using constraints]
1273 growThetaTyVars theta tvs
1274   | null theta = tvs
1275   | otherwise  = fixVarSet mk_next tvs
1276   where
1277     mk_next tvs = foldr grow_one tvs theta
1278     grow_one pred tvs = growPredTyVars pred tvs `unionVarSet` tvs
1279
1280 growPredTyVars :: TcPredType
1281                -> TyVarSet      -- The set to extend
1282                -> TyVarSet      -- TyVars of the predicate if it intersects
1283                                 -- the set, or is implicit parameter
1284 growPredTyVars pred tvs 
1285   | IParam {} <- pred               = pred_tvs  -- See Note [Implicit parameters and ambiguity]
1286   | pred_tvs `intersectsVarSet` tvs = pred_tvs
1287   | otherwise                       = emptyVarSet
1288   where
1289     pred_tvs = tyVarsOfPred pred
1290 \end{code}
1291     
1292 Note [Implicit parameters and ambiguity] 
1293 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1294 Only a *class* predicate can give rise to ambiguity
1295 An *implicit parameter* cannot.  For example:
1296         foo :: (?x :: [a]) => Int
1297         foo = length ?x
1298 is fine.  The call site will suppply a particular 'x'
1299
1300 Furthermore, the type variables fixed by an implicit parameter
1301 propagate to the others.  E.g.
1302         foo :: (Show a, ?x::[a]) => Int
1303         foo = show (?x++?x)
1304 The type of foo looks ambiguous.  But it isn't, because at a call site
1305 we might have
1306         let ?x = 5::Int in foo
1307 and all is well.  In effect, implicit parameters are, well, parameters,
1308 so we can take their type variables into account as part of the
1309 "tau-tvs" stuff.  This is done in the function 'FunDeps.grow'.
1310
1311
1312 \begin{code}
1313 checkThetaCtxt :: SourceTyCtxt -> ThetaType -> SDoc
1314 checkThetaCtxt ctxt theta
1315   = vcat [ptext (sLit "In the context:") <+> pprTheta theta,
1316           ptext (sLit "While checking") <+> pprSourceTyCtxt ctxt ]
1317
1318 badPredTyErr, eqPredTyErr, predTyVarErr :: PredType -> SDoc
1319 badPredTyErr sty = ptext (sLit "Illegal constraint") <+> pprPred sty
1320 eqPredTyErr  sty = ptext (sLit "Illegal equational constraint") <+> pprPred sty
1321                    $$
1322                    parens (ptext (sLit "Use -XTypeFamilies to permit this"))
1323 predTyVarErr pred  = sep [ptext (sLit "Non type-variable argument"),
1324                           nest 2 (ptext (sLit "in the constraint:") <+> pprPred pred)]
1325 dupPredWarn :: [[PredType]] -> SDoc
1326 dupPredWarn dups   = ptext (sLit "Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
1327
1328 arityErr :: Outputable a => String -> a -> Int -> Int -> SDoc
1329 arityErr kind name n m
1330   = hsep [ text kind, quotes (ppr name), ptext (sLit "should have"),
1331            n_arguments <> comma, text "but has been given", 
1332            if m==0 then text "none" else int m]
1333     where
1334         n_arguments | n == 0 = ptext (sLit "no arguments")
1335                     | n == 1 = ptext (sLit "1 argument")
1336                     | True   = hsep [int n, ptext (sLit "arguments")]
1337 \end{code}
1338
1339 %************************************************************************
1340 %*                                                                      *
1341 \subsection{Checking for a decent instance head type}
1342 %*                                                                      *
1343 %************************************************************************
1344
1345 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1346 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1347
1348 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1349 flag is on, or (2)~the instance is imported (they must have been
1350 compiled elsewhere). In these cases, we let them go through anyway.
1351
1352 We can also have instances for functions: @instance Foo (a -> b) ...@.
1353
1354 \begin{code}
1355 checkValidInstHead :: Type -> TcM (Class, [TcType])
1356
1357 checkValidInstHead ty   -- Should be a source type
1358   = case tcSplitPredTy_maybe ty of {
1359         Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
1360         Just pred -> 
1361
1362     case getClassPredTys_maybe pred of {
1363         Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
1364         Just (clas,tys) -> do
1365
1366     dflags <- getDOpts
1367     check_inst_head dflags clas tys
1368     return (clas, tys)
1369     }}
1370
1371 check_inst_head :: DynFlags -> Class -> [Type] -> TcM ()
1372 check_inst_head dflags clas tys
1373   = do { -- If GlasgowExts then check at least one isn't a type variable
1374        ; checkTc (xopt Opt_TypeSynonymInstances dflags ||
1375                   all tcInstHeadTyNotSynonym tys)
1376                  (instTypeErr (pprClassPred clas tys) head_type_synonym_msg)
1377        ; checkTc (xopt Opt_FlexibleInstances dflags ||
1378                   all tcInstHeadTyAppAllTyVars tys)
1379                  (instTypeErr (pprClassPred clas tys) head_type_args_tyvars_msg)
1380        ; checkTc (xopt Opt_MultiParamTypeClasses dflags ||
1381                   isSingleton tys)
1382                  (instTypeErr (pprClassPred clas tys) head_one_type_msg)
1383          -- May not contain type family applications
1384        ; mapM_ checkTyFamFreeness tys
1385
1386        ; mapM_ checkValidMonoType tys
1387         -- For now, I only allow tau-types (not polytypes) in 
1388         -- the head of an instance decl.  
1389         --      E.g.  instance C (forall a. a->a) is rejected
1390         -- One could imagine generalising that, but I'm not sure
1391         -- what all the consequences might be
1392        }
1393
1394   where
1395     head_type_synonym_msg = parens (
1396                 text "All instance types must be of the form (T t1 ... tn)" $$
1397                 text "where T is not a synonym." $$
1398                 text "Use -XTypeSynonymInstances if you want to disable this.")
1399
1400     head_type_args_tyvars_msg = parens (vcat [
1401                 text "All instance types must be of the form (T a1 ... an)",
1402                 text "where a1 ... an are type *variables*,",
1403                 text "and each type variable appears at most once in the instance head.",
1404                 text "Use -XFlexibleInstances if you want to disable this."])
1405
1406     head_one_type_msg = parens (
1407                 text "Only one type can be given in an instance head." $$
1408                 text "Use -XMultiParamTypeClasses if you want to allow more.")
1409
1410 instTypeErr :: SDoc -> SDoc -> SDoc
1411 instTypeErr pp_ty msg
1412   = sep [ptext (sLit "Illegal instance declaration for") <+> quotes pp_ty, 
1413          nest 2 msg]
1414 \end{code}
1415
1416
1417 %************************************************************************
1418 %*                                                                      *
1419 \subsection{Checking instance for termination}
1420 %*                                                                      *
1421 %************************************************************************
1422
1423 \begin{code}
1424 checkValidInstance :: LHsType Name -> [TyVar] -> ThetaType -> Type 
1425                    -> TcM (Class, [TcType])
1426 checkValidInstance hs_type tyvars theta tau
1427   = setSrcSpan (getLoc hs_type) $
1428     do  { (clas, inst_tys) <- setSrcSpan head_loc $
1429                               checkValidInstHead tau
1430
1431         ; undecidable_ok <- xoptM Opt_UndecidableInstances
1432
1433         ; checkValidTheta InstThetaCtxt theta
1434         ; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys)
1435
1436         -- Check that instance inference will terminate (if we care)
1437         -- For Haskell 98 this will already have been done by checkValidTheta,
1438         -- but as we may be using other extensions we need to check.
1439         ; unless undecidable_ok $
1440           mapM_ addErrTc (checkInstTermination inst_tys theta)
1441         
1442         -- The Coverage Condition
1443         ; checkTc (undecidable_ok || checkInstCoverage clas inst_tys)
1444                   (instTypeErr (pprClassPred clas inst_tys) msg)
1445
1446         ; return (clas, inst_tys)
1447         }
1448   where
1449     msg  = parens (vcat [ptext (sLit "the Coverage Condition fails for one of the functional dependencies;"),
1450                          undecidableMsg])
1451
1452         -- The location of the "head" of the instance
1453     head_loc = case hs_type of
1454                  L _ (HsForAllTy _ _ _ (L loc _)) -> loc
1455                  L loc _                          -> loc
1456 \end{code}
1457
1458 Termination test: the so-called "Paterson conditions" (see Section 5 of
1459 "Understanding functionsl dependencies via Constraint Handling Rules, 
1460 JFP Jan 2007).
1461
1462 We check that each assertion in the context satisfies:
1463  (1) no variable has more occurrences in the assertion than in the head, and
1464  (2) the assertion has fewer constructors and variables (taken together
1465      and counting repetitions) than the head.
1466 This is only needed with -fglasgow-exts, as Haskell 98 restrictions
1467 (which have already been checked) guarantee termination. 
1468
1469 The underlying idea is that 
1470
1471     for any ground substitution, each assertion in the
1472     context has fewer type constructors than the head.
1473
1474
1475 \begin{code}
1476 checkInstTermination :: [TcType] -> ThetaType -> [Message]
1477 checkInstTermination tys theta
1478   = mapCatMaybes check theta
1479   where
1480    fvs  = fvTypes tys
1481    size = sizeTypes tys
1482    check pred 
1483       | not (null (fvPred pred \\ fvs)) 
1484       = Just (predUndecErr pred nomoreMsg $$ parens undecidableMsg)
1485       | sizePred pred >= size
1486       = Just (predUndecErr pred smallerMsg $$ parens undecidableMsg)
1487       | otherwise
1488       = Nothing
1489
1490 predUndecErr :: PredType -> SDoc -> SDoc
1491 predUndecErr pred msg = sep [msg,
1492                         nest 2 (ptext (sLit "in the constraint:") <+> pprPred pred)]
1493
1494 nomoreMsg, smallerMsg, undecidableMsg :: SDoc
1495 nomoreMsg = ptext (sLit "Variable occurs more often in a constraint than in the instance head")
1496 smallerMsg = ptext (sLit "Constraint is no smaller than the instance head")
1497 undecidableMsg = ptext (sLit "Use -XUndecidableInstances to permit this")
1498 \end{code}
1499
1500 validDeivPred checks for OK 'deriving' context.  See Note [Exotic
1501 derived instance contexts] in TcSimplify.  However the predicate is
1502 here because it uses sizeTypes, fvTypes.
1503
1504 \begin{code}
1505 validDerivPred :: PredType -> Bool
1506 validDerivPred (ClassP _ tys) = hasNoDups fvs && sizeTypes tys == length fvs
1507                               where fvs = fvTypes tys
1508 validDerivPred _              = False
1509 \end{code}
1510
1511
1512 %************************************************************************
1513 %*                                                                      *
1514         Checking type instance well-formedness and termination
1515 %*                                                                      *
1516 %************************************************************************
1517
1518 \begin{code}
1519 -- Check that a "type instance" is well-formed (which includes decidability
1520 -- unless -XUndecidableInstances is given).
1521 --
1522 checkValidTypeInst :: [Type] -> Type -> TcM ()
1523 checkValidTypeInst typats rhs
1524   = do { -- left-hand side contains no type family applications
1525          -- (vanilla synonyms are fine, though)
1526        ; mapM_ checkTyFamFreeness typats
1527
1528          -- the right-hand side is a tau type
1529        ; checkValidMonoType rhs
1530
1531          -- we have a decidable instance unless otherwise permitted
1532        ; undecidable_ok <- xoptM Opt_UndecidableInstances
1533        ; unless undecidable_ok $
1534            mapM_ addErrTc (checkFamInst typats (tyFamInsts rhs))
1535        }
1536
1537 -- Make sure that each type family instance is 
1538 --   (1) strictly smaller than the lhs,
1539 --   (2) mentions no type variable more often than the lhs, and
1540 --   (3) does not contain any further type family instances.
1541 --
1542 checkFamInst :: [Type]                  -- lhs
1543              -> [(TyCon, [Type])]       -- type family instances
1544              -> [Message]
1545 checkFamInst lhsTys famInsts
1546   = mapCatMaybes check famInsts
1547   where
1548    size = sizeTypes lhsTys
1549    fvs  = fvTypes lhsTys
1550    check (tc, tys)
1551       | not (all isTyFamFree tys)
1552       = Just (famInstUndecErr famInst nestedMsg $$ parens undecidableMsg)
1553       | not (null (fvTypes tys \\ fvs))
1554       = Just (famInstUndecErr famInst nomoreVarMsg $$ parens undecidableMsg)
1555       | size <= sizeTypes tys
1556       = Just (famInstUndecErr famInst smallerAppMsg $$ parens undecidableMsg)
1557       | otherwise
1558       = Nothing
1559       where
1560         famInst = TyConApp tc tys
1561
1562 -- Ensure that no type family instances occur in a type.
1563 --
1564 checkTyFamFreeness :: Type -> TcM ()
1565 checkTyFamFreeness ty
1566   = checkTc (isTyFamFree ty) $
1567       tyFamInstIllegalErr ty
1568
1569 -- Check that a type does not contain any type family applications.
1570 --
1571 isTyFamFree :: Type -> Bool
1572 isTyFamFree = null . tyFamInsts
1573
1574 -- Error messages
1575
1576 tyFamInstIllegalErr :: Type -> SDoc
1577 tyFamInstIllegalErr ty
1578   = hang (ptext (sLit "Illegal type synonym family application in instance") <> 
1579          colon) 2 $
1580       ppr ty
1581
1582 famInstUndecErr :: Type -> SDoc -> SDoc
1583 famInstUndecErr ty msg 
1584   = sep [msg, 
1585          nest 2 (ptext (sLit "in the type family application:") <+> 
1586                  pprType ty)]
1587
1588 nestedMsg, nomoreVarMsg, smallerAppMsg :: SDoc
1589 nestedMsg     = ptext (sLit "Nested type family application")
1590 nomoreVarMsg  = ptext (sLit "Variable occurs more often than in instance head")
1591 smallerAppMsg = ptext (sLit "Application is no smaller than the instance head")
1592 \end{code}
1593
1594
1595 %************************************************************************
1596 %*                                                                      *
1597 \subsection{Auxiliary functions}
1598 %*                                                                      *
1599 %************************************************************************
1600
1601 \begin{code}
1602 -- Free variables of a type, retaining repetitions, and expanding synonyms
1603 fvType :: Type -> [TyVar]
1604 fvType ty | Just exp_ty <- tcView ty = fvType exp_ty
1605 fvType (TyVarTy tv)        = [tv]
1606 fvType (TyConApp _ tys)    = fvTypes tys
1607 fvType (PredTy pred)       = fvPred pred
1608 fvType (FunTy arg res)     = fvType arg ++ fvType res
1609 fvType (AppTy fun arg)     = fvType fun ++ fvType arg
1610 fvType (ForAllTy tyvar ty) = filter (/= tyvar) (fvType ty)
1611
1612 fvTypes :: [Type] -> [TyVar]
1613 fvTypes tys                = concat (map fvType tys)
1614
1615 fvPred :: PredType -> [TyVar]
1616 fvPred (ClassP _ tys')     = fvTypes tys'
1617 fvPred (IParam _ ty)       = fvType ty
1618 fvPred (EqPred ty1 ty2)    = fvType ty1 ++ fvType ty2
1619
1620 -- Size of a type: the number of variables and constructors
1621 sizeType :: Type -> Int
1622 sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty
1623 sizeType (TyVarTy _)       = 1
1624 sizeType (TyConApp _ tys)  = sizeTypes tys + 1
1625 sizeType (PredTy pred)     = sizePred pred
1626 sizeType (FunTy arg res)   = sizeType arg + sizeType res + 1
1627 sizeType (AppTy fun arg)   = sizeType fun + sizeType arg
1628 sizeType (ForAllTy _ ty)   = sizeType ty
1629
1630 sizeTypes :: [Type] -> Int
1631 sizeTypes xs               = sum (map sizeType xs)
1632
1633 -- Size of a predicate
1634 --
1635 -- We are considering whether *class* constraints terminate
1636 -- Once we get into an implicit parameter or equality we
1637 -- can't get back to a class constraint, so it's safe
1638 -- to say "size 0".  See Trac #4200.
1639 sizePred :: PredType -> Int
1640 sizePred (ClassP _ tys')   = sizeTypes tys'
1641 sizePred (IParam {})       = 0
1642 sizePred (EqPred {})       = 0
1643 \end{code}