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