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