Change the last few (F)SLIT's into (f)sLit's
[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 {-# OPTIONS -w #-}
13 -- The above warning supression flag is a temporary kludge.
14 -- While working on this module you are encouraged to remove it and fix
15 -- any warnings in the module. See
16 --     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
17 -- for details
18
19 module TcMType (
20   TcTyVar, TcKind, TcType, TcTauType, TcThetaType, TcTyVarSet,
21
22   --------------------------------
23   -- Creating new mutable type variables
24   newFlexiTyVar,
25   newFlexiTyVarTy,              -- Kind -> TcM TcType
26   newFlexiTyVarTys,             -- Int -> Kind -> TcM [TcType]
27   newKindVar, newKindVars, 
28   lookupTcTyVar, LookupTyVarResult(..),
29
30   newMetaTyVar, readMetaTyVar, writeMetaTyVar, isFilledMetaTyVar,
31
32   --------------------------------
33   -- Boxy type variables
34   newBoxyTyVar, newBoxyTyVars, newBoxyTyVarTys, readFilledBox, 
35
36   --------------------------------
37   -- Creating new coercion variables
38   newCoVars, newMetaCoVar,
39
40   --------------------------------
41   -- Instantiation
42   tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxyTyVar,
43   tcInstSigTyVars,
44   tcInstSkolTyVar, tcInstSkolTyVars, tcInstSkolType, 
45   tcSkolSigType, tcSkolSigTyVars, occurCheckErr,
46
47   --------------------------------
48   -- Checking type validity
49   Rank, UserTypeCtxt(..), checkValidType, checkValidMonoType,
50   SourceTyCtxt(..), checkValidTheta, checkFreeness,
51   checkValidInstHead, checkValidInstance, 
52   checkInstTermination, checkValidTypeInst, checkTyFamFreeness,
53   checkUpdateMeta, updateMeta, checkTauTvUpdate, fillBoxWithTau, unifyKindCtxt,
54   unifyKindMisMatch, validDerivPred, arityErr, notMonoType, notMonoArgs,
55
56   --------------------------------
57   -- Zonking
58   zonkType, zonkTcPredType, 
59   zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkSigTyVar,
60   zonkQuantifiedTyVar, zonkQuantifiedTyVars,
61   zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
62   zonkTcKindToKind, zonkTcKind, zonkTopTyVar,
63
64   readKindVar, writeKindVar
65   ) where
66
67 #include "HsVersions.h"
68
69 -- friends:
70 import TypeRep
71 import TcType
72 import Type
73 import Coercion
74 import Class
75 import TyCon
76 import Var
77
78 -- others:
79 import TcRnMonad          -- TcType, amongst others
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 UniqSupply
89 import SrcLoc
90 import Outputable
91 import FastString
92
93 import Control.Monad    ( when, unless )
94 import Data.List        ( (\\) )
95 \end{code}
96
97
98 %************************************************************************
99 %*                                                                      *
100         Instantiation in general
101 %*                                                                      *
102 %************************************************************************
103
104 \begin{code}
105 tcInstType :: ([TyVar] -> TcM [TcTyVar])                -- How to instantiate the type variables
106            -> TcType                                    -- Type to instantiate
107            -> TcM ([TcTyVar], TcThetaType, TcType)      -- Result
108                 -- (type vars (excl coercion vars), preds (incl equalities), rho)
109 tcInstType inst_tyvars ty
110   = case tcSplitForAllTys ty of
111         ([],     rho) -> let    -- There may be overloading despite no type variables;
112                                 --      (?x :: Int) => Int -> Int
113                            (theta, tau) = tcSplitPhiTy rho
114                          in
115                          return ([], theta, tau)
116
117         (tyvars, rho) -> do { tyvars' <- inst_tyvars tyvars
118
119                             ; let  tenv = zipTopTvSubst tyvars (mkTyVarTys tyvars')
120                                 -- Either the tyvars are freshly made, by inst_tyvars,
121                                 -- or (in the call from tcSkolSigType) any nested foralls
122                                 -- have different binders.  Either way, zipTopTvSubst is ok
123
124                             ; let  (theta, tau) = tcSplitPhiTy (substTy tenv rho)
125                             ; return (tyvars', theta, tau) }
126 \end{code}
127
128
129 %************************************************************************
130 %*                                                                      *
131         Updating tau types
132 %*                                                                      *
133 %************************************************************************
134
135 Can't be in TcUnify, as we also need it in TcTyFuns.
136
137 \begin{code}
138 type SwapFlag = Bool
139         -- False <=> the two args are (actual, expected) respectively
140         -- True  <=> the two args are (expected, actual) respectively
141
142 checkUpdateMeta :: SwapFlag
143                 -> TcTyVar -> IORef MetaDetails -> TcType -> TcM ()
144 -- Update tv1, which is flexi; occurs check is alrady done
145 -- The 'check' version does a kind check too
146 -- We do a sub-kind check here: we might unify (a b) with (c d) 
147 --      where b::*->* and d::*; this should fail
148
149 checkUpdateMeta swapped tv1 ref1 ty2
150   = do  { checkKinds swapped tv1 ty2
151         ; updateMeta tv1 ref1 ty2 }
152
153 updateMeta :: TcTyVar -> IORef MetaDetails -> TcType -> TcM ()
154 updateMeta tv1 ref1 ty2
155   = ASSERT( isMetaTyVar tv1 )
156     ASSERT( isBoxyTyVar tv1 || isTauTy ty2 )
157     do  { ASSERTM2( do { details <- readMetaTyVar tv1; return (isFlexi details) }, ppr tv1 )
158         ; traceTc (text "updateMeta" <+> ppr tv1 <+> text ":=" <+> ppr ty2)
159         ; writeMutVar ref1 (Indirect ty2) 
160         }
161
162 ----------------
163 checkKinds swapped tv1 ty2
164 -- We're about to unify a type variable tv1 with a non-tyvar-type ty2.
165 -- ty2 has been zonked at this stage, which ensures that
166 -- its kind has as much boxity information visible as possible.
167   | tk2 `isSubKind` tk1 = return ()
168
169   | otherwise
170         -- Either the kinds aren't compatible
171         --      (can happen if we unify (a b) with (c d))
172         -- or we are unifying a lifted type variable with an
173         --      unlifted type: e.g.  (id 3#) is illegal
174   = addErrCtxtM (unifyKindCtxt swapped tv1 ty2) $
175     unifyKindMisMatch k1 k2
176   where
177     (k1,k2) | swapped   = (tk2,tk1)
178             | otherwise = (tk1,tk2)
179     tk1 = tyVarKind tv1
180     tk2 = typeKind ty2
181
182 ----------------
183 checkTauTvUpdate :: TcTyVar -> TcType -> TcM (Maybe TcType)
184 --    (checkTauTvUpdate tv ty)
185 -- We are about to update the TauTv tv with ty.
186 -- Check (a) that tv doesn't occur in ty (occurs check)
187 --       (b) that ty is a monotype
188 -- Furthermore, in the interest of (b), if you find an
189 -- empty box (BoxTv that is Flexi), fill it in with a TauTv
190 -- 
191 -- We have three possible outcomes:
192 -- (1) Return the (non-boxy) type to update the type variable with, 
193 --     [we know the update is ok!]
194 -- (2) return Nothing, or 
195 --     [we cannot tell whether the update is ok right now]
196 -- (3) fails.
197 --     [the update is definitely invalid]
198 -- We return Nothing in case the tv occurs in ty *under* a type family
199 -- application.  In this case, we must not update tv (to avoid a cyclic type
200 -- term), but we also cannot fail claiming an infinite type.  Given
201 --   type family F a
202 --   type instance F Int = Int
203 -- consider
204 --   a ~ F a
205 -- This is perfectly reasonable, if we later get a ~ Int.
206
207 checkTauTvUpdate orig_tv orig_ty
208   = do { result <- go orig_ty
209        ; case result of 
210            Right ty    -> return $ Just ty
211            Left  True  -> return $ Nothing
212            Left  False -> occurCheckErr (mkTyVarTy orig_tv) orig_ty
213        }
214   where
215     go :: TcType -> TcM (Either Bool TcType)
216     -- go returns
217     --   Right ty    if everything is fine
218     --   Left True   if orig_tv occurs in orig_ty, but under a type family app
219     --   Left False  if orig_tv occurs in orig_ty (with no type family app)
220     -- It fails if it encounters a forall type, except as an argument for a
221     -- closed type synonym that expands to a tau type.
222     go (TyConApp tc tys)
223         | isSynTyCon tc  = go_syn tc tys
224         | otherwise      = do { tys' <- mapM go tys
225                               ; return $ occurs (TyConApp tc) tys' }
226     go (PredTy p)        = do { p' <- go_pred p
227                               ; return $ occurs1 PredTy p' }
228     go (FunTy arg res)   = do { arg' <- go arg
229                               ; res' <- go res
230                               ; return $ occurs2 FunTy arg' res' }
231     go (AppTy fun arg)   = do { fun' <- go fun
232                               ; arg' <- go arg
233                               ; return $ occurs2 mkAppTy fun' arg' }
234                 -- NB the mkAppTy; we might have instantiated a
235                 -- type variable to a type constructor, so we need
236                 -- to pull the TyConApp to the top.
237     go (ForAllTy tv ty) = notMonoType orig_ty           -- (b)
238
239     go (TyVarTy tv)
240         | orig_tv == tv = return $ Left False           -- (a)
241         | isTcTyVar tv  = go_tyvar tv (tcTyVarDetails tv)
242         | otherwise     = return $ Right (TyVarTy tv)
243                  -- Ordinary (non Tc) tyvars
244                  -- occur inside quantified types
245
246     go_pred (ClassP c tys) = do { tys' <- mapM go tys
247                                 ; return $ occurs (ClassP c) tys' }
248     go_pred (IParam n ty)  = do { ty' <- go ty
249                                 ; return $ occurs1 (IParam n) ty' }
250     go_pred (EqPred t1 t2) = do { t1' <- go t1
251                                 ; t2' <- go t2
252                                 ; return $ occurs2 EqPred t1' t2' }
253
254     go_tyvar tv (SkolemTv _) = return $ Right (TyVarTy tv)
255     go_tyvar tv (MetaTv box ref)
256         = do { cts <- readMutVar ref
257              ; case cts of
258                   Indirect ty -> go ty 
259                   Flexi -> case box of
260                                 BoxTv -> do { ty <- fillBoxWithTau tv ref
261                                             ; return $ Right ty }
262                                 other -> return $ Right (TyVarTy tv)
263              }
264
265         -- go_syn is called for synonyms only
266         -- See Note [Type synonyms and the occur check]
267     go_syn tc tys
268         | not (isTauTyCon tc)
269         = notMonoType orig_ty   -- (b) again
270         | otherwise
271         = do { (msgs, mb_tys') <- tryTc (mapM go tys)
272              ; case mb_tys' of
273
274                 -- we had a type error => forall in type parameters
275                 Nothing 
276                   | isOpenTyCon tc -> notMonoArgs (TyConApp tc tys)
277                         -- Synonym families must have monotype args
278                   | otherwise      -> go (expectJust "checkTauTvUpdate(1)" 
279                                             (tcView (TyConApp tc tys)))
280                         -- Try again, expanding the synonym
281
282                 -- no type error, but need to test whether occurs check happend
283                 Just tys' -> 
284                   case occurs id tys' of
285                     Left _ 
286                       | isOpenTyCon tc -> return $ Left True
287                         -- Variable occured under type family application
288                       | otherwise      -> go (expectJust "checkTauTvUpdate(2)" 
289                                                (tcView (TyConApp tc tys)))
290                         -- Try again, expanding the synonym
291                     Right raw_tys'     -> return $ Right (TyConApp tc raw_tys')
292                         -- Retain the synonym (the common case)
293              }
294
295     -- Left results (= occurrence of orig_ty) dominate and
296     -- (Left False) (= fatal occurrence) dominates over (Left True)
297     occurs :: ([a] -> b) -> [Either Bool a] -> Either Bool b
298     occurs c = either Left (Right . c) . foldr combine (Right [])
299       where
300         combine (Left famInst1) (Left famInst2) = Left (famInst1 && famInst2)
301         combine (Right _      ) (Left famInst)  = Left famInst
302         combine (Left famInst)  (Right _)       = Left famInst
303         combine (Right arg)     (Right args)    = Right (arg:args)
304
305     occurs1 c x   = occurs (\[x']     -> c x')    [x]
306     occurs2 c x y = occurs (\[x', y'] -> c x' y') [x, y]
307
308 fillBoxWithTau :: BoxyTyVar -> IORef MetaDetails -> TcM TcType
309 -- (fillBoxWithTau tv ref) fills ref with a freshly allocated 
310 --  tau-type meta-variable, whose print-name is the same as tv
311 -- Choosing the same name is good: when we instantiate a function
312 -- we allocate boxy tyvars with the same print-name as the quantified
313 -- tyvar; and then we often fill the box with a tau-tyvar, and again
314 -- we want to choose the same name.
315 fillBoxWithTau tv ref 
316   = do  { tv' <- tcInstTyVar tv         -- Do not gratuitously forget
317         ; let tau = mkTyVarTy tv'       -- name of the type variable
318         ; writeMutVar ref (Indirect tau)
319         ; return tau }
320 \end{code}
321
322 Note [Type synonyms and the occur check]
323 ~~~~~~~~~~~~~~~~~~~~
324 Basically we want to update     tv1 := ps_ty2
325 because ps_ty2 has type-synonym info, which improves later error messages
326
327 But consider 
328         type A a = ()
329
330         f :: (A a -> a -> ()) -> ()
331         f = \ _ -> ()
332
333         x :: ()
334         x = f (\ x p -> p x)
335
336 In the application (p x), we try to match "t" with "A t".  If we go
337 ahead and bind t to A t (= ps_ty2), we'll lead the type checker into 
338 an infinite loop later.
339 But we should not reject the program, because A t = ().
340 Rather, we should bind t to () (= non_var_ty2).
341
342 --------------
343
344 Error mesages in case of kind mismatch.
345
346 \begin{code}
347 unifyKindMisMatch ty1 ty2 = do
348     ty1' <- zonkTcKind ty1
349     ty2' <- zonkTcKind ty2
350     let
351         msg = hang (ptext (sLit "Couldn't match kind"))
352                    2 (sep [quotes (ppr ty1'), 
353                            ptext (sLit "against"), 
354                            quotes (ppr ty2')])
355     failWithTc msg
356
357 unifyKindCtxt swapped tv1 ty2 tidy_env  -- not swapped => tv1 expected, ty2 inferred
358         -- tv1 and ty2 are zonked already
359   = return msg
360   where
361     msg = (env2, ptext (sLit "When matching the kinds of") <+> 
362                  sep [quotes pp_expected <+> ptext (sLit "and"), quotes pp_actual])
363
364     (pp_expected, pp_actual) | swapped   = (pp2, pp1)
365                              | otherwise = (pp1, pp2)
366     (env1, tv1') = tidyOpenTyVar tidy_env tv1
367     (env2, ty2') = tidyOpenType  env1 ty2
368     pp1 = ppr tv1' <+> dcolon <+> ppr (tyVarKind tv1)
369     pp2 = ppr ty2' <+> dcolon <+> ppr (typeKind ty2)
370 \end{code}
371
372 Error message for failure due to an occurs check.
373
374 \begin{code}
375 occurCheckErr :: TcType -> TcType -> TcM a
376 occurCheckErr ty containingTy
377   = do  { env0 <- tcInitTidyEnv
378         ; ty'           <- zonkTcType ty
379         ; containingTy' <- zonkTcType containingTy
380         ; let (env1, tidy_ty1) = tidyOpenType env0 ty'
381               (env2, tidy_ty2) = tidyOpenType env1 containingTy'
382               extra = sep [ppr tidy_ty1, char '=', ppr tidy_ty2]
383         ; failWithTcM (env2, hang msg 2 extra) }
384   where
385     msg = ptext (sLit "Occurs check: cannot construct the infinite type:")
386 \end{code}
387
388 %************************************************************************
389 %*                                                                      *
390         Kind variables
391 %*                                                                      *
392 %************************************************************************
393
394 \begin{code}
395 newCoVars :: [(TcType,TcType)] -> TcM [CoVar]
396 newCoVars spec
397   = do  { us <- newUniqueSupply 
398         ; return [ mkCoVar (mkSysTvName uniq (fsLit "co"))
399                            (mkCoKind ty1 ty2)
400                  | ((ty1,ty2), uniq) <- spec `zip` uniqsFromSupply us] }
401
402 newMetaCoVar :: TcType -> TcType -> TcM TcTyVar
403 newMetaCoVar ty1 ty2 = newMetaTyVar TauTv (mkCoKind ty1 ty2)
404
405 newKindVar :: TcM TcKind
406 newKindVar = do { uniq <- newUnique
407                 ; ref <- newMutVar Flexi
408                 ; return (mkTyVarTy (mkKindVar uniq ref)) }
409
410 newKindVars :: Int -> TcM [TcKind]
411 newKindVars n = mapM (\ _ -> newKindVar) (nOfThem n ())
412 \end{code}
413
414
415 %************************************************************************
416 %*                                                                      *
417         SkolemTvs (immutable)
418 %*                                                                      *
419 %************************************************************************
420
421 \begin{code}
422 mkSkolTyVar :: Name -> Kind -> SkolemInfo -> TcTyVar
423 mkSkolTyVar name kind info = mkTcTyVar name kind (SkolemTv info)
424
425 tcSkolSigType :: SkolemInfo -> Type -> TcM ([TcTyVar], TcThetaType, TcType)
426 -- Instantiate a type signature with skolem constants, but 
427 -- do *not* give them fresh names, because we want the name to
428 -- be in the type environment -- it is lexically scoped.
429 tcSkolSigType info ty = tcInstType (\tvs -> return (tcSkolSigTyVars info tvs)) ty
430
431 tcSkolSigTyVars :: SkolemInfo -> [TyVar] -> [TcTyVar]
432 -- Make skolem constants, but do *not* give them new names, as above
433 tcSkolSigTyVars info tyvars = [ mkSkolTyVar (tyVarName tv) (tyVarKind tv) info
434                               | tv <- tyvars ]
435
436 tcInstSkolTyVar :: SkolemInfo -> Maybe SrcSpan -> TyVar -> TcM TcTyVar
437 -- Instantiate the tyvar, using 
438 --      * the occ-name and kind of the supplied tyvar, 
439 --      * the unique from the monad,
440 --      * the location either from the tyvar (mb_loc = Nothing)
441 --        or from mb_loc (Just loc)
442 tcInstSkolTyVar info mb_loc tyvar
443   = do  { uniq <- newUnique
444         ; let old_name = tyVarName tyvar
445               kind     = tyVarKind tyvar
446               loc      = mb_loc `orElse` getSrcSpan old_name
447               new_name = mkInternalName uniq (nameOccName old_name) loc
448         ; return (mkSkolTyVar new_name kind info) }
449
450 tcInstSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
451 -- Get the location from the monad
452 tcInstSkolTyVars info tyvars 
453   = do  { span <- getSrcSpanM
454         ; mapM (tcInstSkolTyVar info (Just span)) tyvars }
455
456 tcInstSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
457 -- Instantiate a type with fresh skolem constants
458 -- Binding location comes from the monad
459 tcInstSkolType info ty = tcInstType (tcInstSkolTyVars info) ty
460 \end{code}
461
462
463 %************************************************************************
464 %*                                                                      *
465         MetaTvs (meta type variables; mutable)
466 %*                                                                      *
467 %************************************************************************
468
469 \begin{code}
470 newMetaTyVar :: BoxInfo -> Kind -> TcM TcTyVar
471 -- Make a new meta tyvar out of thin air
472 newMetaTyVar box_info kind
473   = do  { uniq <- newUnique
474         ; ref <- newMutVar Flexi
475         ; let name = mkSysTvName uniq fs 
476               fs = case box_info of
477                         BoxTv   -> fsLit "t"
478                         TauTv   -> fsLit "t"
479                         SigTv _ -> fsLit "a"
480                 -- We give BoxTv and TauTv the same string, because
481                 -- otherwise we get user-visible differences in error
482                 -- messages, which are confusing.  If you want to see
483                 -- the box_info of each tyvar, use -dppr-debug
484         ; return (mkTcTyVar name kind (MetaTv box_info ref)) }
485
486 instMetaTyVar :: BoxInfo -> TyVar -> TcM TcTyVar
487 -- Make a new meta tyvar whose Name and Kind 
488 -- come from an existing TyVar
489 instMetaTyVar box_info tyvar
490   = do  { uniq <- newUnique
491         ; ref <- newMutVar Flexi
492         ; let name = setNameUnique (tyVarName tyvar) uniq
493               kind = tyVarKind tyvar
494         ; return (mkTcTyVar name kind (MetaTv box_info ref)) }
495
496 readMetaTyVar :: TyVar -> TcM MetaDetails
497 readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
498                       readMutVar (metaTvRef tyvar)
499
500 isFilledMetaTyVar :: TyVar -> TcM Bool
501 -- True of a filled-in (Indirect) meta type variable
502 isFilledMetaTyVar tv
503   | not (isTcTyVar tv) = return False
504   | MetaTv _ ref <- tcTyVarDetails tv
505   = do  { details <- readMutVar ref
506         ; return (isIndirect details) }
507   | otherwise = return False
508
509 writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
510 writeMetaTyVar tyvar ty
511   | not debugIsOn = writeMutVar (metaTvRef tyvar) (Indirect ty)
512 writeMetaTyVar tyvar ty
513   | not (isMetaTyVar tyvar)
514   = pprTrace "writeMetaTyVar" (ppr tyvar) $
515     return ()
516   | otherwise
517   = ASSERT( isMetaTyVar tyvar )
518     -- TOM: It should also work for coercions
519     -- ASSERT2( k2 `isSubKind` k1, (ppr tyvar <+> ppr k1) $$ (ppr ty <+> ppr k2) )
520     do  { ASSERTM2( do { details <- readMetaTyVar tyvar; return (isFlexi details) }, ppr tyvar )
521         ; writeMutVar (metaTvRef tyvar) (Indirect ty) }
522   where
523     k1 = tyVarKind tyvar
524     k2 = typeKind ty
525 \end{code}
526
527
528 %************************************************************************
529 %*                                                                      *
530         MetaTvs: TauTvs
531 %*                                                                      *
532 %************************************************************************
533
534 \begin{code}
535 newFlexiTyVar :: Kind -> TcM TcTyVar
536 newFlexiTyVar kind = newMetaTyVar TauTv kind
537
538 newFlexiTyVarTy  :: Kind -> TcM TcType
539 newFlexiTyVarTy kind = do
540     tc_tyvar <- newFlexiTyVar kind
541     return (TyVarTy tc_tyvar)
542
543 newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
544 newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind)
545
546 tcInstTyVar :: TyVar -> TcM TcTyVar
547 -- Instantiate with a META type variable
548 tcInstTyVar tyvar = instMetaTyVar TauTv tyvar
549
550 tcInstTyVars :: [TyVar] -> TcM ([TcTyVar], [TcType], TvSubst)
551 -- Instantiate with META type variables
552 tcInstTyVars tyvars
553   = do  { tc_tvs <- mapM tcInstTyVar tyvars
554         ; let tys = mkTyVarTys tc_tvs
555         ; return (tc_tvs, tys, zipTopTvSubst tyvars tys) }
556                 -- Since the tyvars are freshly made,
557                 -- they cannot possibly be captured by
558                 -- any existing for-alls.  Hence zipTopTvSubst
559 \end{code}
560
561
562 %************************************************************************
563 %*                                                                      *
564         MetaTvs: SigTvs
565 %*                                                                      *
566 %************************************************************************
567
568 \begin{code}
569 tcInstSigTyVars :: Bool -> SkolemInfo -> [TyVar] -> TcM [TcTyVar]
570 -- Instantiate with skolems or meta SigTvs; depending on use_skols
571 -- Always take location info from the supplied tyvars
572 tcInstSigTyVars use_skols skol_info tyvars 
573   | use_skols
574   = mapM (tcInstSkolTyVar skol_info Nothing) tyvars
575
576   | otherwise
577   = mapM (instMetaTyVar (SigTv skol_info)) tyvars
578
579 zonkSigTyVar :: TcTyVar -> TcM TcTyVar
580 zonkSigTyVar sig_tv 
581   | isSkolemTyVar sig_tv 
582   = return sig_tv       -- Happens in the call in TcBinds.checkDistinctTyVars
583   | otherwise
584   = ASSERT( isSigTyVar sig_tv )
585     do { ty <- zonkTcTyVar sig_tv
586        ; return (tcGetTyVar "zonkSigTyVar" ty) }
587         -- 'ty' is bound to be a type variable, because SigTvs
588         -- can only be unified with type variables
589 \end{code}
590
591
592 %************************************************************************
593 %*                                                                      *
594         MetaTvs: BoxTvs
595 %*                                                                      *
596 %************************************************************************
597
598 \begin{code}
599 newBoxyTyVar :: Kind -> TcM BoxyTyVar
600 newBoxyTyVar kind = newMetaTyVar BoxTv kind
601
602 newBoxyTyVars :: [Kind] -> TcM [BoxyTyVar]
603 newBoxyTyVars kinds = mapM newBoxyTyVar kinds
604
605 newBoxyTyVarTys :: [Kind] -> TcM [BoxyType]
606 newBoxyTyVarTys kinds = do { tvs <- mapM newBoxyTyVar kinds; return (mkTyVarTys tvs) }
607
608 readFilledBox :: BoxyTyVar -> TcM TcType
609 -- Read the contents of the box, which should be filled in by now
610 readFilledBox box_tv = ASSERT( isBoxyTyVar box_tv )
611                        do { cts <- readMetaTyVar box_tv
612                           ; case cts of
613                                 Flexi -> pprPanic "readFilledBox" (ppr box_tv)
614                                 Indirect ty -> return ty }
615
616 tcInstBoxyTyVar :: TyVar -> TcM BoxyTyVar
617 -- Instantiate with a BOXY type variable
618 tcInstBoxyTyVar tyvar = instMetaTyVar BoxTv tyvar
619 \end{code}
620
621
622 %************************************************************************
623 %*                                                                      *
624 \subsection{Putting and getting  mutable type variables}
625 %*                                                                      *
626 %************************************************************************
627
628 But it's more fun to short out indirections on the way: If this
629 version returns a TyVar, then that TyVar is unbound.  If it returns
630 any other type, then there might be bound TyVars embedded inside it.
631
632 We return Nothing iff the original box was unbound.
633
634 \begin{code}
635 data LookupTyVarResult  -- The result of a lookupTcTyVar call
636   = DoneTv TcTyVarDetails       -- SkolemTv or virgin MetaTv
637   | IndirectTv TcType
638
639 lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult
640 lookupTcTyVar tyvar 
641   = ASSERT2( isTcTyVar tyvar, ppr tyvar )
642     case details of
643       SkolemTv _   -> return (DoneTv details)
644       MetaTv _ ref -> do { meta_details <- readMutVar ref
645                          ; case meta_details of
646                             Indirect ty -> return (IndirectTv ty)
647                             Flexi -> return (DoneTv details) }
648   where
649     details =  tcTyVarDetails tyvar
650
651 {- 
652 -- gaw 2004 We aren't shorting anything out anymore, at least for now
653 getTcTyVar tyvar
654   | not (isTcTyVar tyvar)
655   = pprTrace "getTcTyVar" (ppr tyvar) $
656     return (Just (mkTyVarTy tyvar))
657
658   | otherwise
659   = ASSERT2( isTcTyVar tyvar, ppr tyvar ) do
660     maybe_ty <- readMetaTyVar tyvar
661     case maybe_ty of
662         Just ty -> do ty' <- short_out ty
663                       writeMetaTyVar tyvar (Just ty')
664                       return (Just ty')
665
666         Nothing    -> return Nothing
667
668 short_out :: TcType -> TcM TcType
669 short_out ty@(TyVarTy tyvar)
670   | not (isTcTyVar tyvar)
671   = return ty
672
673   | otherwise = do
674     maybe_ty <- readMetaTyVar tyvar
675     case maybe_ty of
676         Just ty' -> do ty' <- short_out ty'
677                        writeMetaTyVar tyvar (Just ty')
678                        return ty'
679
680         other    -> return ty
681
682 short_out other_ty = return other_ty
683 -}
684 \end{code}
685
686
687 %************************************************************************
688 %*                                                                      *
689 \subsection{Zonking -- the exernal interfaces}
690 %*                                                                      *
691 %************************************************************************
692
693 -----------------  Type variables
694
695 \begin{code}
696 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
697 zonkTcTyVars tyvars = mapM zonkTcTyVar tyvars
698
699 zonkTcTyVarsAndFV :: [TcTyVar] -> TcM TcTyVarSet
700 zonkTcTyVarsAndFV tyvars = tyVarsOfTypes <$> mapM zonkTcTyVar tyvars
701
702 zonkTcTyVar :: TcTyVar -> TcM TcType
703 zonkTcTyVar tyvar = ASSERT2( isTcTyVar tyvar, ppr tyvar)
704                     zonk_tc_tyvar (\ tv -> return (TyVarTy tv)) tyvar
705 \end{code}
706
707 -----------------  Types
708
709 \begin{code}
710 zonkTcType :: TcType -> TcM TcType
711 zonkTcType ty = zonkType (\ tv -> return (TyVarTy tv)) ty
712
713 zonkTcTypes :: [TcType] -> TcM [TcType]
714 zonkTcTypes tys = mapM zonkTcType tys
715
716 zonkTcClassConstraints cts = mapM zonk cts
717     where zonk (clas, tys) = do
718               new_tys <- zonkTcTypes tys
719               return (clas, new_tys)
720
721 zonkTcThetaType :: TcThetaType -> TcM TcThetaType
722 zonkTcThetaType theta = mapM zonkTcPredType theta
723
724 zonkTcPredType :: TcPredType -> TcM TcPredType
725 zonkTcPredType (ClassP c ts)  = ClassP c <$> zonkTcTypes ts
726 zonkTcPredType (IParam n t)   = IParam n <$> zonkTcType t
727 zonkTcPredType (EqPred t1 t2) = EqPred <$> zonkTcType t1 <*> zonkTcType t2
728 \end{code}
729
730 -------------------  These ...ToType, ...ToKind versions
731                      are used at the end of type checking
732
733 \begin{code}
734 zonkTopTyVar :: TcTyVar -> TcM TcTyVar
735 -- zonkTopTyVar is used, at the top level, on any un-instantiated meta type variables
736 -- to default the kind of ? and ?? etc to *.  This is important to ensure that
737 -- instance declarations match.  For example consider
738 --      instance Show (a->b)
739 --      foo x = show (\_ -> True)
740 -- Then we'll get a constraint (Show (p ->q)) where p has argTypeKind (printed ??), 
741 -- and that won't match the typeKind (*) in the instance decl.
742 --
743 -- Because we are at top level, no further constraints are going to affect these
744 -- type variables, so it's time to do it by hand.  However we aren't ready
745 -- to default them fully to () or whatever, because the type-class defaulting
746 -- rules have yet to run.
747
748 zonkTopTyVar tv
749   | k `eqKind` default_k = return tv
750   | otherwise
751   = do  { tv' <- newFlexiTyVar default_k
752         ; writeMetaTyVar tv (mkTyVarTy tv') 
753         ; return tv' }
754   where
755     k = tyVarKind tv
756     default_k = defaultKind k
757
758 zonkQuantifiedTyVars :: [TcTyVar] -> TcM [TcTyVar]
759 zonkQuantifiedTyVars = mapM zonkQuantifiedTyVar
760
761 zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar
762 -- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it.
763 --
764 -- The quantified type variables often include meta type variables
765 -- we want to freeze them into ordinary type variables, and
766 -- default their kind (e.g. from OpenTypeKind to TypeKind)
767 --                      -- see notes with Kind.defaultKind
768 -- The meta tyvar is updated to point to the new skolem TyVar.  Now any 
769 -- bound occurences of the original type variable will get zonked to 
770 -- the immutable version.
771 --
772 -- We leave skolem TyVars alone; they are immutable.
773 zonkQuantifiedTyVar tv
774   | ASSERT( isTcTyVar tv ) 
775     isSkolemTyVar tv = return tv
776         -- It might be a skolem type variable, 
777         -- for example from a user type signature
778
779   | otherwise   -- It's a meta-type-variable
780   = do  { details <- readMetaTyVar tv
781
782         -- Create the new, frozen, skolem type variable
783         -- We zonk to a skolem, not to a regular TcVar
784         -- See Note [Zonking to Skolem]
785         ; let final_kind = defaultKind (tyVarKind tv)
786               final_tv   = mkSkolTyVar (tyVarName tv) final_kind UnkSkol
787
788         -- Bind the meta tyvar to the new tyvar
789         ; case details of
790             Indirect ty -> WARN( True, ppr tv $$ ppr ty ) 
791                            return ()
792                 -- [Sept 04] I don't think this should happen
793                 -- See note [Silly Type Synonym]
794
795             Flexi -> writeMetaTyVar tv (mkTyVarTy final_tv)
796
797         -- Return the new tyvar
798         ; return final_tv }
799 \end{code}
800
801 Note [Silly Type Synonyms]
802 ~~~~~~~~~~~~~~~~~~~~~~~~~~
803 Consider this:
804         type C u a = u  -- Note 'a' unused
805
806         foo :: (forall a. C u a -> C u a) -> u
807         foo x = ...
808
809         bar :: Num u => u
810         bar = foo (\t -> t + t)
811
812 * From the (\t -> t+t) we get type  {Num d} =>  d -> d
813   where d is fresh.
814
815 * Now unify with type of foo's arg, and we get:
816         {Num (C d a)} =>  C d a -> C d a
817   where a is fresh.
818
819 * Now abstract over the 'a', but float out the Num (C d a) constraint
820   because it does not 'really' mention a.  (see exactTyVarsOfType)
821   The arg to foo becomes
822         /\a -> \t -> t+t
823
824 * So we get a dict binding for Num (C d a), which is zonked to give
825         a = ()
826   [Note Sept 04: now that we are zonking quantified type variables
827   on construction, the 'a' will be frozen as a regular tyvar on
828   quantification, so the floated dict will still have type (C d a).
829   Which renders this whole note moot; happily!]
830
831 * Then the /\a abstraction has a zonked 'a' in it.
832
833 All very silly.   I think its harmless to ignore the problem.  We'll end up with
834 a /\a in the final result but all the occurrences of a will be zonked to ()
835
836 Note [Zonking to Skolem]
837 ~~~~~~~~~~~~~~~~~~~~~~~~
838 We used to zonk quantified type variables to regular TyVars.  However, this
839 leads to problems.  Consider this program from the regression test suite:
840
841   eval :: Int -> String -> String -> String
842   eval 0 root actual = evalRHS 0 root actual
843
844   evalRHS :: Int -> a
845   evalRHS 0 root actual = eval 0 root actual
846
847 It leads to the deferral of an equality
848
849   (String -> String -> String) ~ a
850
851 which is propagated up to the toplevel (see TcSimplify.tcSimplifyInferCheck).
852 In the meantime `a' is zonked and quantified to form `evalRHS's signature.
853 This has the *side effect* of also zonking the `a' in the deferred equality
854 (which at this point is being handed around wrapped in an implication
855 constraint).
856
857 Finally, the equality (with the zonked `a') will be handed back to the
858 simplifier by TcRnDriver.tcRnSrcDecls calling TcSimplify.tcSimplifyTop.
859 If we zonk `a' with a regular type variable, we will have this regular type
860 variable now floating around in the simplifier, which in many places assumes to
861 only see proper TcTyVars.
862
863 We can avoid this problem by zonking with a skolem.  The skolem is rigid
864 (which we requirefor a quantified variable), but is still a TcTyVar that the
865 simplifier knows how to deal with.
866
867
868 %************************************************************************
869 %*                                                                      *
870 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
871 %*                                                                      *
872 %*              For internal use only!                                  *
873 %*                                                                      *
874 %************************************************************************
875
876 \begin{code}
877 -- For unbound, mutable tyvars, zonkType uses the function given to it
878 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
879 --      type variable and zonks the kind too
880
881 zonkType :: (TcTyVar -> TcM Type)       -- What to do with unbound mutable type variables
882                                         -- see zonkTcType, and zonkTcTypeToType
883          -> TcType
884          -> TcM Type
885 zonkType unbound_var_fn ty
886   = go ty
887   where
888     go (TyConApp tc tys) = do tys' <- mapM go tys
889                               return (TyConApp tc tys')
890
891     go (PredTy p)        = do p' <- go_pred p
892                               return (PredTy p')
893
894     go (FunTy arg res)   = do arg' <- go arg
895                               res' <- go res
896                               return (FunTy arg' res')
897
898     go (AppTy fun arg)   = do fun' <- go fun
899                               arg' <- go arg
900                               return (mkAppTy fun' arg')
901                 -- NB the mkAppTy; we might have instantiated a
902                 -- type variable to a type constructor, so we need
903                 -- to pull the TyConApp to the top.
904
905         -- The two interesting cases!
906     go (TyVarTy tyvar) | isTcTyVar tyvar = zonk_tc_tyvar unbound_var_fn tyvar
907                        | otherwise       = return (TyVarTy tyvar)
908                 -- Ordinary (non Tc) tyvars occur inside quantified types
909
910     go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar ) do
911                              ty' <- go ty
912                              return (ForAllTy tyvar ty')
913
914     go_pred (ClassP c tys)   = do tys' <- mapM go tys
915                                   return (ClassP c tys')
916     go_pred (IParam n ty)    = do ty' <- go ty
917                                   return (IParam n ty')
918     go_pred (EqPred ty1 ty2) = do ty1' <- go ty1
919                                   ty2' <- go ty2
920                                   return (EqPred ty1' ty2')
921
922 zonk_tc_tyvar :: (TcTyVar -> TcM Type)          -- What to do for an unbound mutable variable
923               -> TcTyVar -> TcM TcType
924 zonk_tc_tyvar unbound_var_fn tyvar 
925   | not (isMetaTyVar tyvar)     -- Skolems
926   = return (TyVarTy tyvar)
927
928   | otherwise                   -- Mutables
929   = do  { cts <- readMetaTyVar tyvar
930         ; case cts of
931             Flexi       -> unbound_var_fn tyvar    -- Unbound meta type variable
932             Indirect ty -> zonkType unbound_var_fn ty  }
933 \end{code}
934
935
936
937 %************************************************************************
938 %*                                                                      *
939                         Zonking kinds
940 %*                                                                      *
941 %************************************************************************
942
943 \begin{code}
944 readKindVar  :: KindVar -> TcM (MetaDetails)
945 writeKindVar :: KindVar -> TcKind -> TcM ()
946 readKindVar  kv = readMutVar (kindVarRef kv)
947 writeKindVar kv val = writeMutVar (kindVarRef kv) (Indirect val)
948
949 -------------
950 zonkTcKind :: TcKind -> TcM TcKind
951 zonkTcKind k = zonkTcType k
952
953 -------------
954 zonkTcKindToKind :: TcKind -> TcM Kind
955 -- When zonking a TcKind to a kind, we need to instantiate kind variables,
956 -- Haskell specifies that * is to be used, so we follow that.
957 zonkTcKindToKind k = zonkType (\ _ -> return liftedTypeKind) k
958 \end{code}
959                         
960 %************************************************************************
961 %*                                                                      *
962 \subsection{Checking a user type}
963 %*                                                                      *
964 %************************************************************************
965
966 When dealing with a user-written type, we first translate it from an HsType
967 to a Type, performing kind checking, and then check various things that should 
968 be true about it.  We don't want to perform these checks at the same time
969 as the initial translation because (a) they are unnecessary for interface-file
970 types and (b) when checking a mutually recursive group of type and class decls,
971 we can't "look" at the tycons/classes yet.  Also, the checks are are rather
972 diverse, and used to really mess up the other code.
973
974 One thing we check for is 'rank'.  
975
976         Rank 0:         monotypes (no foralls)
977         Rank 1:         foralls at the front only, Rank 0 inside
978         Rank 2:         foralls at the front, Rank 1 on left of fn arrow,
979
980         basic ::= tyvar | T basic ... basic
981
982         r2  ::= forall tvs. cxt => r2a
983         r2a ::= r1 -> r2a | basic
984         r1  ::= forall tvs. cxt => r0
985         r0  ::= r0 -> r0 | basic
986         
987 Another thing is to check that type synonyms are saturated. 
988 This might not necessarily show up in kind checking.
989         type A i = i
990         data T k = MkT (k Int)
991         f :: T A        -- BAD!
992
993         
994 \begin{code}
995 checkValidType :: UserTypeCtxt -> Type -> TcM ()
996 -- Checks that the type is valid for the given context
997 checkValidType ctxt ty = do
998     traceTc (text "checkValidType" <+> ppr ty)
999     unboxed  <- doptM Opt_UnboxedTuples
1000     rank2    <- doptM Opt_Rank2Types
1001     rankn    <- doptM Opt_RankNTypes
1002     polycomp <- doptM Opt_PolymorphicComponents
1003     let 
1004         rank | rankn = Arbitrary
1005              | rank2 = Rank 2
1006              | otherwise
1007              = case ctxt of     -- Haskell 98
1008                  GenPatCtxt     -> Rank 0
1009                  LamPatSigCtxt  -> Rank 0
1010                  BindPatSigCtxt -> Rank 0
1011                  DefaultDeclCtxt-> Rank 0
1012                  ResSigCtxt     -> Rank 0
1013                  TySynCtxt _    -> Rank 0
1014                  ExprSigCtxt    -> Rank 1
1015                  FunSigCtxt _   -> Rank 1
1016                  ConArgCtxt _   -> if polycomp
1017                            then Rank 2
1018                                 -- We are given the type of the entire
1019                                 -- constructor, hence rank 1
1020                            else Rank 1
1021                  ForSigCtxt _   -> Rank 1
1022                  SpecInstCtxt   -> Rank 1
1023
1024         actual_kind = typeKind ty
1025
1026         kind_ok = case ctxt of
1027                         TySynCtxt _  -> True    -- Any kind will do
1028                         ResSigCtxt   -> isSubOpenTypeKind        actual_kind
1029                         ExprSigCtxt  -> isSubOpenTypeKind        actual_kind
1030                         GenPatCtxt   -> isLiftedTypeKind actual_kind
1031                         ForSigCtxt _ -> isLiftedTypeKind actual_kind
1032                         other        -> isSubArgTypeKind    actual_kind
1033         
1034         ubx_tup = case ctxt of
1035                       TySynCtxt _ | unboxed -> UT_Ok
1036                       ExprSigCtxt | unboxed -> UT_Ok
1037                       _                     -> UT_NotOk
1038
1039         -- Check that the thing has kind Type, and is lifted if necessary
1040     checkTc kind_ok (kindErr actual_kind)
1041
1042         -- Check the internal validity of the type itself
1043     check_type rank ubx_tup ty
1044
1045     traceTc (text "checkValidType done" <+> ppr ty)
1046
1047 checkValidMonoType :: Type -> TcM ()
1048 checkValidMonoType ty = check_mono_type ty
1049 \end{code}
1050
1051
1052 \begin{code}
1053 data Rank = Rank Int | Arbitrary
1054
1055 decRank :: Rank -> Rank
1056 decRank Arbitrary = Arbitrary
1057 decRank (Rank n)  = Rank (n-1)
1058
1059 nonZeroRank :: Rank -> Bool
1060 nonZeroRank (Rank 0) = False
1061 nonZeroRank _        = True
1062
1063 ----------------------------------------
1064 data UbxTupFlag = UT_Ok | UT_NotOk
1065         -- The "Ok" version means "ok if -fglasgow-exts is on"
1066
1067 ----------------------------------------
1068 check_mono_type :: Type -> TcM ()       -- No foralls anywhere
1069                                         -- No unlifted types of any kind
1070 check_mono_type ty
1071    = do { check_type (Rank 0) UT_NotOk ty
1072         ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
1073
1074 check_type :: Rank -> UbxTupFlag -> Type -> TcM ()
1075 -- The args say what the *type* context requires, independent
1076 -- of *flag* settings.  You test the flag settings at usage sites.
1077 -- 
1078 -- Rank is allowed rank for function args
1079 -- Rank 0 means no for-alls anywhere
1080
1081 check_type rank ubx_tup ty
1082   | not (null tvs && null theta)
1083   = do  { checkTc (nonZeroRank rank) (forAllTyErr ty)
1084                 -- Reject e.g. (Maybe (?x::Int => Int)), 
1085                 -- with a decent error message
1086         ; check_valid_theta SigmaCtxt theta
1087         ; check_type rank ubx_tup tau   -- Allow foralls to right of arrow
1088         ; checkFreeness tvs theta
1089         ; checkAmbiguity tvs theta (tyVarsOfType tau) }
1090   where
1091     (tvs, theta, tau) = tcSplitSigmaTy ty
1092    
1093 -- Naked PredTys don't usually show up, but they can as a result of
1094 --      {-# SPECIALISE instance Ord Char #-}
1095 -- The Right Thing would be to fix the way that SPECIALISE instance pragmas
1096 -- are handled, but the quick thing is just to permit PredTys here.
1097 check_type rank ubx_tup (PredTy sty)
1098   = do  { dflags <- getDOpts
1099         ; check_pred_ty dflags TypeCtxt sty }
1100
1101 check_type rank ubx_tup (TyVarTy _)       = return ()
1102 check_type rank ubx_tup ty@(FunTy arg_ty res_ty)
1103   = do  { check_type (decRank rank) UT_NotOk arg_ty
1104         ; check_type rank           UT_Ok    res_ty }
1105
1106 check_type rank ubx_tup (AppTy ty1 ty2)
1107   = do  { check_arg_type rank ty1
1108         ; check_arg_type rank ty2 }
1109
1110 check_type rank ubx_tup ty@(TyConApp tc tys)
1111   | isSynTyCon tc
1112   = do  {       -- Check that the synonym has enough args
1113                 -- This applies equally to open and closed synonyms
1114                 -- It's OK to have an *over-applied* type synonym
1115                 --      data Tree a b = ...
1116                 --      type Foo a = Tree [a]
1117                 --      f :: Foo a b -> ...
1118           checkTc (tyConArity tc <= length tys) arity_msg
1119
1120         -- See Note [Liberal type synonyms]
1121         ; liberal <- doptM Opt_LiberalTypeSynonyms
1122         ; if not liberal || isOpenSynTyCon tc then
1123                 -- For H98 and synonym families, do check the type args
1124                 mapM_ check_mono_type tys
1125
1126           else  -- In the liberal case (only for closed syns), expand then check
1127           case tcView ty of   
1128              Just ty' -> check_type rank ubx_tup ty' 
1129              Nothing  -> pprPanic "check_tau_type" (ppr ty)
1130     }
1131     
1132   | isUnboxedTupleTyCon tc
1133   = do  { ub_tuples_allowed <- doptM Opt_UnboxedTuples
1134         ; checkTc (ubx_tup_ok ub_tuples_allowed) ubx_tup_msg
1135
1136         ; impred <- doptM Opt_ImpredicativeTypes        
1137         ; let rank' = if impred then rank else Rank 0
1138                 -- c.f. check_arg_type
1139                 -- However, args are allowed to be unlifted, or
1140                 -- more unboxed tuples, so can't use check_arg_ty
1141         ; mapM_ (check_type rank' UT_Ok) tys }
1142
1143   | otherwise
1144   = mapM_ (check_arg_type rank) tys
1145
1146   where
1147     ubx_tup_ok ub_tuples_allowed = case ubx_tup of { UT_Ok -> ub_tuples_allowed; other -> False }
1148
1149     n_args    = length tys
1150     tc_arity  = tyConArity tc
1151
1152     arity_msg   = arityErr "Type synonym" (tyConName tc) tc_arity n_args
1153     ubx_tup_msg = ubxArgTyErr ty
1154
1155 ----------------------------------------
1156 check_arg_type :: Rank -> Type -> TcM ()
1157 -- The sort of type that can instantiate a type variable,
1158 -- or be the argument of a type constructor.
1159 -- Not an unboxed tuple, but now *can* be a forall (since impredicativity)
1160 -- Other unboxed types are very occasionally allowed as type
1161 -- arguments depending on the kind of the type constructor
1162 -- 
1163 -- For example, we want to reject things like:
1164 --
1165 --      instance Ord a => Ord (forall s. T s a)
1166 -- and
1167 --      g :: T s (forall b.b)
1168 --
1169 -- NB: unboxed tuples can have polymorphic or unboxed args.
1170 --     This happens in the workers for functions returning
1171 --     product types with polymorphic components.
1172 --     But not in user code.
1173 -- Anyway, they are dealt with by a special case in check_tau_type
1174
1175 check_arg_type rank ty 
1176   = do  { impred <- doptM Opt_ImpredicativeTypes
1177         ; let rank' = if impred then rank else Rank 0   -- Monotype unless impredicative
1178         ; check_type rank' UT_NotOk ty
1179         ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
1180
1181 ----------------------------------------
1182 forAllTyErr     ty = sep [ptext (sLit "Illegal polymorphic or qualified type:"), ppr ty]
1183 unliftedArgErr  ty = sep [ptext (sLit "Illegal unlifted type:"), ppr ty]
1184 ubxArgTyErr     ty = sep [ptext (sLit "Illegal unboxed tuple type as function argument:"), ppr ty]
1185 kindErr kind       = sep [ptext (sLit "Expecting an ordinary type, but found a type of kind"), ppr kind]
1186 \end{code}
1187
1188 Note [Liberal type synonyms]
1189 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1190 If -XLiberalTypeSynonyms is on, expand closed type synonyms *before*
1191 doing validity checking.  This allows us to instantiate a synonym defn
1192 with a for-all type, or with a partially-applied type synonym.
1193         e.g.   type T a b = a
1194                type S m   = m ()
1195                f :: S (T Int)
1196 Here, T is partially applied, so it's illegal in H98.  But if you
1197 expand S first, then T we get just
1198                f :: Int
1199 which is fine.
1200
1201 IMPORTANT: suppose T is a type synonym.  Then we must do validity
1202 checking on an appliation (T ty1 ty2)
1203
1204         *either* before expansion (i.e. check ty1, ty2)
1205         *or* after expansion (i.e. expand T ty1 ty2, and then check)
1206         BUT NOT BOTH
1207
1208 If we do both, we get exponential behaviour!!
1209
1210   data TIACons1 i r c = c i ::: r c
1211   type TIACons2 t x = TIACons1 t (TIACons1 t x)
1212   type TIACons3 t x = TIACons2 t (TIACons1 t x)
1213   type TIACons4 t x = TIACons2 t (TIACons2 t x)
1214   type TIACons7 t x = TIACons4 t (TIACons3 t x)
1215
1216
1217 %************************************************************************
1218 %*                                                                      *
1219 \subsection{Checking a theta or source type}
1220 %*                                                                      *
1221 %************************************************************************
1222
1223 \begin{code}
1224 -- Enumerate the contexts in which a "source type", <S>, can occur
1225 --      Eq a 
1226 -- or   ?x::Int
1227 -- or   r <: {x::Int}
1228 -- or   (N a) where N is a newtype
1229
1230 data SourceTyCtxt
1231   = ClassSCCtxt Name    -- Superclasses of clas
1232                         --      class <S> => C a where ...
1233   | SigmaCtxt           -- Theta part of a normal for-all type
1234                         --      f :: <S> => a -> a
1235   | DataTyCtxt Name     -- Theta part of a data decl
1236                         --      data <S> => T a = MkT a
1237   | TypeCtxt            -- Source type in an ordinary type
1238                         --      f :: N a -> N a
1239   | InstThetaCtxt       -- Context of an instance decl
1240                         --      instance <S> => C [a] where ...
1241                 
1242 pprSourceTyCtxt (ClassSCCtxt c) = ptext (sLit "the super-classes of class") <+> quotes (ppr c)
1243 pprSourceTyCtxt SigmaCtxt       = ptext (sLit "the context of a polymorphic type")
1244 pprSourceTyCtxt (DataTyCtxt tc) = ptext (sLit "the context of the data type declaration for") <+> quotes (ppr tc)
1245 pprSourceTyCtxt InstThetaCtxt   = ptext (sLit "the context of an instance declaration")
1246 pprSourceTyCtxt TypeCtxt        = ptext (sLit "the context of a type")
1247 \end{code}
1248
1249 \begin{code}
1250 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
1251 checkValidTheta ctxt theta 
1252   = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
1253
1254 -------------------------
1255 check_valid_theta ctxt []
1256   = return ()
1257 check_valid_theta ctxt theta = do
1258     dflags <- getDOpts
1259     warnTc (notNull dups) (dupPredWarn dups)
1260     mapM_ (check_pred_ty dflags ctxt) theta
1261   where
1262     (_,dups) = removeDups tcCmpPred theta
1263
1264 -------------------------
1265 check_pred_ty :: DynFlags -> SourceTyCtxt -> PredType -> TcM ()
1266 check_pred_ty dflags ctxt pred@(ClassP cls tys)
1267   = do {        -- Class predicates are valid in all contexts
1268        ; checkTc (arity == n_tys) arity_err
1269
1270                 -- Check the form of the argument types
1271        ; mapM_ check_mono_type tys
1272        ; checkTc (check_class_pred_tys dflags ctxt tys)
1273                  (predTyVarErr pred $$ how_to_allow)
1274        }
1275   where
1276     class_name = className cls
1277     arity      = classArity cls
1278     n_tys      = length tys
1279     arity_err  = arityErr "Class" class_name arity n_tys
1280     how_to_allow = parens (ptext (sLit "Use -XFlexibleContexts to permit this"))
1281
1282 check_pred_ty dflags ctxt pred@(EqPred ty1 ty2)
1283   = do {        -- Equational constraints are valid in all contexts if type
1284                 -- families are permitted
1285        ; checkTc (dopt Opt_TypeFamilies dflags) (eqPredTyErr pred)
1286
1287                 -- Check the form of the argument types
1288        ; check_mono_type ty1
1289        ; check_mono_type ty2
1290        }
1291
1292 check_pred_ty dflags SigmaCtxt (IParam _ ty) = check_mono_type ty
1293         -- Implicit parameters only allowed in type
1294         -- signatures; not in instance decls, superclasses etc
1295         -- The reason for not allowing implicit params in instances is a bit
1296         -- subtle.
1297         -- If we allowed        instance (?x::Int, Eq a) => Foo [a] where ...
1298         -- then when we saw (e :: (?x::Int) => t) it would be unclear how to 
1299         -- discharge all the potential usas of the ?x in e.   For example, a
1300         -- constraint Foo [Int] might come out of e,and applying the
1301         -- instance decl would show up two uses of ?x.
1302
1303 -- Catch-all
1304 check_pred_ty dflags ctxt sty = failWithTc (badPredTyErr sty)
1305
1306 -------------------------
1307 check_class_pred_tys :: DynFlags -> SourceTyCtxt -> [Type] -> Bool
1308 check_class_pred_tys dflags ctxt tys 
1309   = case ctxt of
1310         TypeCtxt      -> True   -- {-# SPECIALISE instance Eq (T Int) #-} is fine
1311         InstThetaCtxt -> flexible_contexts || undecidable_ok || all tcIsTyVarTy tys
1312                                 -- Further checks on head and theta in
1313                                 -- checkInstTermination
1314         other         -> flexible_contexts || all tyvar_head tys
1315   where
1316     flexible_contexts = dopt Opt_FlexibleContexts dflags
1317     undecidable_ok = dopt Opt_UndecidableInstances dflags
1318
1319 -------------------------
1320 tyvar_head ty                   -- Haskell 98 allows predicates of form 
1321   | tcIsTyVarTy ty = True       --      C (a ty1 .. tyn)
1322   | otherwise                   -- where a is a type variable
1323   = case tcSplitAppTy_maybe ty of
1324         Just (ty, _) -> tyvar_head ty
1325         Nothing      -> False
1326 \end{code}
1327
1328 Check for ambiguity
1329 ~~~~~~~~~~~~~~~~~~~
1330           forall V. P => tau
1331 is ambiguous if P contains generic variables
1332 (i.e. one of the Vs) that are not mentioned in tau
1333
1334 However, we need to take account of functional dependencies
1335 when we speak of 'mentioned in tau'.  Example:
1336         class C a b | a -> b where ...
1337 Then the type
1338         forall x y. (C x y) => x
1339 is not ambiguous because x is mentioned and x determines y
1340
1341 NB; the ambiguity check is only used for *user* types, not for types
1342 coming from inteface files.  The latter can legitimately have
1343 ambiguous types. Example
1344
1345    class S a where s :: a -> (Int,Int)
1346    instance S Char where s _ = (1,1)
1347    f:: S a => [a] -> Int -> (Int,Int)
1348    f (_::[a]) x = (a*x,b)
1349         where (a,b) = s (undefined::a)
1350
1351 Here the worker for f gets the type
1352         fw :: forall a. S a => Int -> (# Int, Int #)
1353
1354 If the list of tv_names is empty, we have a monotype, and then we
1355 don't need to check for ambiguity either, because the test can't fail
1356 (see is_ambig).
1357
1358
1359 \begin{code}
1360 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
1361 checkAmbiguity forall_tyvars theta tau_tyvars
1362   = mapM_ complain (filter is_ambig theta)
1363   where
1364     complain pred     = addErrTc (ambigErr pred)
1365     extended_tau_vars = grow theta tau_tyvars
1366
1367         -- See Note [Implicit parameters and ambiguity] in TcSimplify
1368     is_ambig pred     = isClassPred  pred &&
1369                         any ambig_var (varSetElems (tyVarsOfPred pred))
1370
1371     ambig_var ct_var  = (ct_var `elem` forall_tyvars) &&
1372                         not (ct_var `elemVarSet` extended_tau_vars)
1373
1374 ambigErr pred
1375   = sep [ptext (sLit "Ambiguous constraint") <+> quotes (pprPred pred),
1376          nest 4 (ptext (sLit "At least one of the forall'd type variables mentioned by the constraint") $$
1377                  ptext (sLit "must be reachable from the type after the '=>'"))]
1378 \end{code}
1379     
1380 In addition, GHC insists that at least one type variable
1381 in each constraint is in V.  So we disallow a type like
1382         forall a. Eq b => b -> b
1383 even in a scope where b is in scope.
1384
1385 \begin{code}
1386 checkFreeness forall_tyvars theta
1387   = do  { flexible_contexts <- doptM Opt_FlexibleContexts
1388         ; unless flexible_contexts $ mapM_ complain (filter is_free theta) }
1389   where    
1390     is_free pred     =  not (isIPPred pred)
1391                      && not (any bound_var (varSetElems (tyVarsOfPred pred)))
1392     bound_var ct_var = ct_var `elem` forall_tyvars
1393     complain pred    = addErrTc (freeErr pred)
1394
1395 freeErr pred
1396   = sep [ ptext (sLit "All of the type variables in the constraint") <+> 
1397           quotes (pprPred pred)
1398         , ptext (sLit "are already in scope") <+>
1399           ptext (sLit "(at least one must be universally quantified here)")
1400         , nest 4 $
1401             ptext (sLit "(Use -XFlexibleContexts to lift this restriction)")
1402         ]
1403 \end{code}
1404
1405 \begin{code}
1406 checkThetaCtxt ctxt theta
1407   = vcat [ptext (sLit "In the context:") <+> pprTheta theta,
1408           ptext (sLit "While checking") <+> pprSourceTyCtxt ctxt ]
1409
1410 badPredTyErr sty = ptext (sLit "Illegal constraint") <+> pprPred sty
1411 eqPredTyErr  sty = ptext (sLit "Illegal equational constraint") <+> pprPred sty
1412                    $$
1413                    parens (ptext (sLit "Use -XTypeFamilies to permit this"))
1414 predTyVarErr pred  = sep [ptext (sLit "Non type-variable argument"),
1415                           nest 2 (ptext (sLit "in the constraint:") <+> pprPred pred)]
1416 dupPredWarn dups   = ptext (sLit "Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
1417
1418 arityErr kind name n m
1419   = hsep [ text kind, quotes (ppr name), ptext (sLit "should have"),
1420            n_arguments <> comma, text "but has been given", int m]
1421     where
1422         n_arguments | n == 0 = ptext (sLit "no arguments")
1423                     | n == 1 = ptext (sLit "1 argument")
1424                     | True   = hsep [int n, ptext (sLit "arguments")]
1425
1426 -----------------
1427 notMonoType ty
1428   = do  { ty' <- zonkTcType ty
1429         ; env0 <- tcInitTidyEnv
1430         ; let (env1, tidy_ty) = tidyOpenType env0 ty'
1431               msg = ptext (sLit "Cannot match a monotype with") <+> quotes (ppr tidy_ty)
1432         ; failWithTcM (env1, msg) }
1433
1434 notMonoArgs ty
1435   = do  { ty' <- zonkTcType ty
1436         ; env0 <- tcInitTidyEnv
1437         ; let (env1, tidy_ty) = tidyOpenType env0 ty'
1438               msg = ptext (sLit "Arguments of type synonym families must be monotypes") <+> quotes (ppr tidy_ty)
1439         ; failWithTcM (env1, msg) }
1440 \end{code}
1441
1442
1443 %************************************************************************
1444 %*                                                                      *
1445 \subsection{Checking for a decent instance head type}
1446 %*                                                                      *
1447 %************************************************************************
1448
1449 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1450 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1451
1452 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1453 flag is on, or (2)~the instance is imported (they must have been
1454 compiled elsewhere). In these cases, we let them go through anyway.
1455
1456 We can also have instances for functions: @instance Foo (a -> b) ...@.
1457
1458 \begin{code}
1459 checkValidInstHead :: Type -> TcM (Class, [TcType])
1460
1461 checkValidInstHead ty   -- Should be a source type
1462   = case tcSplitPredTy_maybe ty of {
1463         Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
1464         Just pred -> 
1465
1466     case getClassPredTys_maybe pred of {
1467         Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
1468         Just (clas,tys) -> do
1469
1470     dflags <- getDOpts
1471     mapM_ check_mono_type tys
1472     check_inst_head dflags clas tys
1473     return (clas, tys)
1474     }}
1475
1476 check_inst_head dflags clas tys
1477         -- If GlasgowExts then check at least one isn't a type variable
1478   = do checkTc (dopt Opt_TypeSynonymInstances dflags ||
1479                 all tcInstHeadTyNotSynonym tys)
1480                (instTypeErr (pprClassPred clas tys) head_type_synonym_msg)
1481        checkTc (dopt Opt_FlexibleInstances dflags ||
1482                 all tcInstHeadTyAppAllTyVars tys)
1483                (instTypeErr (pprClassPred clas tys) head_type_args_tyvars_msg)
1484        checkTc (dopt Opt_MultiParamTypeClasses dflags ||
1485                 isSingleton tys)
1486                (instTypeErr (pprClassPred clas tys) head_one_type_msg)
1487        mapM_ check_mono_type tys
1488         -- For now, I only allow tau-types (not polytypes) in 
1489         -- the head of an instance decl.  
1490         --      E.g.  instance C (forall a. a->a) is rejected
1491         -- One could imagine generalising that, but I'm not sure
1492         -- what all the consequences might be
1493
1494   where
1495     head_type_synonym_msg = parens (
1496                 text "All instance types must be of the form (T t1 ... tn)" $$
1497                 text "where T is not a synonym." $$
1498                 text "Use -XTypeSynonymInstances if you want to disable this.")
1499
1500     head_type_args_tyvars_msg = parens (vcat [
1501                 text "All instance types must be of the form (T a1 ... an)",
1502                 text "where a1 ... an are type *variables*,",
1503                 text "and each type variable appears at most once in the instance head.",
1504                 text "Use -XFlexibleInstances if you want to disable this."])
1505
1506     head_one_type_msg = parens (
1507                 text "Only one type can be given in an instance head." $$
1508                 text "Use -XMultiParamTypeClasses if you want to allow more.")
1509
1510 instTypeErr pp_ty msg
1511   = sep [ptext (sLit "Illegal instance declaration for") <+> quotes pp_ty, 
1512          nest 4 msg]
1513 \end{code}
1514
1515
1516 %************************************************************************
1517 %*                                                                      *
1518 \subsection{Checking instance for termination}
1519 %*                                                                      *
1520 %************************************************************************
1521
1522
1523 \begin{code}
1524 checkValidInstance :: [TyVar] -> ThetaType -> Class -> [TcType] -> TcM ()
1525 checkValidInstance tyvars theta clas inst_tys
1526   = do  { undecidable_ok <- doptM Opt_UndecidableInstances
1527
1528         ; checkValidTheta InstThetaCtxt theta
1529         ; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys)
1530
1531         -- Check that instance inference will terminate (if we care)
1532         -- For Haskell 98 this will already have been done by checkValidTheta,
1533         -- but as we may be using other extensions we need to check.
1534         ; unless undecidable_ok $
1535           mapM_ addErrTc (checkInstTermination inst_tys theta)
1536         
1537         -- The Coverage Condition
1538         ; checkTc (undecidable_ok || checkInstCoverage clas inst_tys)
1539                   (instTypeErr (pprClassPred clas inst_tys) msg)
1540         }
1541   where
1542     msg  = parens (vcat [ptext (sLit "the Coverage Condition fails for one of the functional dependencies;"),
1543                          undecidableMsg])
1544 \end{code}
1545
1546 Termination test: the so-called "Paterson conditions" (see Section 5 of
1547 "Understanding functionsl dependencies via Constraint Handling Rules, 
1548 JFP Jan 2007).
1549
1550 We check that each assertion in the context satisfies:
1551  (1) no variable has more occurrences in the assertion than in the head, and
1552  (2) the assertion has fewer constructors and variables (taken together
1553      and counting repetitions) than the head.
1554 This is only needed with -fglasgow-exts, as Haskell 98 restrictions
1555 (which have already been checked) guarantee termination. 
1556
1557 The underlying idea is that 
1558
1559     for any ground substitution, each assertion in the
1560     context has fewer type constructors than the head.
1561
1562
1563 \begin{code}
1564 checkInstTermination :: [TcType] -> ThetaType -> [Message]
1565 checkInstTermination tys theta
1566   = mapCatMaybes check theta
1567   where
1568    fvs  = fvTypes tys
1569    size = sizeTypes tys
1570    check pred 
1571       | not (null (fvPred pred \\ fvs)) 
1572       = Just (predUndecErr pred nomoreMsg $$ parens undecidableMsg)
1573       | sizePred pred >= size
1574       = Just (predUndecErr pred smallerMsg $$ parens undecidableMsg)
1575       | otherwise
1576       = Nothing
1577
1578 predUndecErr pred msg = sep [msg,
1579                         nest 2 (ptext (sLit "in the constraint:") <+> pprPred pred)]
1580
1581 nomoreMsg = ptext (sLit "Variable occurs more often in a constraint than in the instance head")
1582 smallerMsg = ptext (sLit "Constraint is no smaller than the instance head")
1583 undecidableMsg = ptext (sLit "Use -fallow-undecidable-instances to permit this")
1584 \end{code}
1585
1586
1587 %************************************************************************
1588 %*                                                                      *
1589         Checking the context of a derived instance declaration
1590 %*                                                                      *
1591 %************************************************************************
1592
1593 Note [Exotic derived instance contexts]
1594 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1595 In a 'derived' instance declaration, we *infer* the context.  It's a
1596 bit unclear what rules we should apply for this; the Haskell report is
1597 silent.  Obviously, constraints like (Eq a) are fine, but what about
1598         data T f a = MkT (f a) deriving( Eq )
1599 where we'd get an Eq (f a) constraint.  That's probably fine too.
1600
1601 One could go further: consider
1602         data T a b c = MkT (Foo a b c) deriving( Eq )
1603         instance (C Int a, Eq b, Eq c) => Eq (Foo a b c)
1604
1605 Notice that this instance (just) satisfies the Paterson termination 
1606 conditions.  Then we *could* derive an instance decl like this:
1607
1608         instance (C Int a, Eq b, Eq c) => Eq (T a b c) 
1609
1610 even though there is no instance for (C Int a), because there just
1611 *might* be an instance for, say, (C Int Bool) at a site where we
1612 need the equality instance for T's.  
1613
1614 However, this seems pretty exotic, and it's quite tricky to allow
1615 this, and yet give sensible error messages in the (much more common)
1616 case where we really want that instance decl for C.
1617
1618 So for now we simply require that the derived instance context
1619 should have only type-variable constraints.
1620
1621 Here is another example:
1622         data Fix f = In (f (Fix f)) deriving( Eq )
1623 Here, if we are prepared to allow -fallow-undecidable-instances we
1624 could derive the instance
1625         instance Eq (f (Fix f)) => Eq (Fix f)
1626 but this is so delicate that I don't think it should happen inside
1627 'deriving'. If you want this, write it yourself!
1628
1629 NB: if you want to lift this condition, make sure you still meet the
1630 termination conditions!  If not, the deriving mechanism generates
1631 larger and larger constraints.  Example:
1632   data Succ a = S a
1633   data Seq a = Cons a (Seq (Succ a)) | Nil deriving Show
1634
1635 Note the lack of a Show instance for Succ.  First we'll generate
1636   instance (Show (Succ a), Show a) => Show (Seq a)
1637 and then
1638   instance (Show (Succ (Succ a)), Show (Succ a), Show a) => Show (Seq a)
1639 and so on.  Instead we want to complain of no instance for (Show (Succ a)).
1640
1641 The bottom line
1642 ~~~~~~~~~~~~~~~
1643 Allow constraints which consist only of type variables, with no repeats.
1644
1645 \begin{code}
1646 validDerivPred :: PredType -> Bool
1647 validDerivPred (ClassP cls tys) = hasNoDups fvs && sizeTypes tys == length fvs
1648                                 where fvs = fvTypes tys
1649 validDerivPred otehr            = False
1650 \end{code}
1651
1652 %************************************************************************
1653 %*                                                                      *
1654         Checking type instance well-formedness and termination
1655 %*                                                                      *
1656 %************************************************************************
1657
1658 \begin{code}
1659 -- Check that a "type instance" is well-formed (which includes decidability
1660 -- unless -fallow-undecidable-instances is given).
1661 --
1662 checkValidTypeInst :: [Type] -> Type -> TcM ()
1663 checkValidTypeInst typats rhs
1664   = do { -- left-hand side contains no type family applications
1665          -- (vanilla synonyms are fine, though)
1666        ; mapM_ checkTyFamFreeness typats
1667
1668          -- the right-hand side is a tau type
1669        ; checkTc (isTauTy rhs) $ 
1670            polyTyErr rhs
1671
1672          -- we have a decidable instance unless otherwise permitted
1673        ; undecidable_ok <- doptM Opt_UndecidableInstances
1674        ; unless undecidable_ok $
1675            mapM_ addErrTc (checkFamInst typats (tyFamInsts rhs))
1676        }
1677
1678 -- Make sure that each type family instance is 
1679 --   (1) strictly smaller than the lhs,
1680 --   (2) mentions no type variable more often than the lhs, and
1681 --   (3) does not contain any further type family instances.
1682 --
1683 checkFamInst :: [Type]                  -- lhs
1684              -> [(TyCon, [Type])]       -- type family instances
1685              -> [Message]
1686 checkFamInst lhsTys famInsts
1687   = mapCatMaybes check famInsts
1688   where
1689    size = sizeTypes lhsTys
1690    fvs  = fvTypes lhsTys
1691    check (tc, tys)
1692       | not (all isTyFamFree tys)
1693       = Just (famInstUndecErr famInst nestedMsg $$ parens undecidableMsg)
1694       | not (null (fvTypes tys \\ fvs))
1695       = Just (famInstUndecErr famInst nomoreVarMsg $$ parens undecidableMsg)
1696       | size <= sizeTypes tys
1697       = Just (famInstUndecErr famInst smallerAppMsg $$ parens undecidableMsg)
1698       | otherwise
1699       = Nothing
1700       where
1701         famInst = TyConApp tc tys
1702
1703 -- Ensure that no type family instances occur in a type.
1704 --
1705 checkTyFamFreeness :: Type -> TcM ()
1706 checkTyFamFreeness ty
1707   = checkTc (isTyFamFree ty) $
1708       tyFamInstInIndexErr ty
1709
1710 -- Check that a type does not contain any type family applications.
1711 --
1712 isTyFamFree :: Type -> Bool
1713 isTyFamFree = null . tyFamInsts
1714
1715 -- Error messages
1716
1717 tyFamInstInIndexErr ty
1718   = hang (ptext (sLit "Illegal type family application in type instance") <> 
1719          colon) 4 $
1720       ppr ty
1721
1722 polyTyErr ty 
1723   = hang (ptext (sLit "Illegal polymorphic type in type instance") <> colon) 4 $
1724       ppr ty
1725
1726 famInstUndecErr ty msg 
1727   = sep [msg, 
1728          nest 2 (ptext (sLit "in the type family application:") <+> 
1729                  pprType ty)]
1730
1731 nestedMsg     = ptext (sLit "Nested type family application")
1732 nomoreVarMsg  = ptext (sLit "Variable occurs more often than in instance head")
1733 smallerAppMsg = ptext (sLit "Application is no smaller than the instance head")
1734 \end{code}
1735
1736
1737 %************************************************************************
1738 %*                                                                      *
1739 \subsection{Auxiliary functions}
1740 %*                                                                      *
1741 %************************************************************************
1742
1743 \begin{code}
1744 -- Free variables of a type, retaining repetitions, and expanding synonyms
1745 fvType :: Type -> [TyVar]
1746 fvType ty | Just exp_ty <- tcView ty = fvType exp_ty
1747 fvType (TyVarTy tv)        = [tv]
1748 fvType (TyConApp _ tys)    = fvTypes tys
1749 fvType (PredTy pred)       = fvPred pred
1750 fvType (FunTy arg res)     = fvType arg ++ fvType res
1751 fvType (AppTy fun arg)     = fvType fun ++ fvType arg
1752 fvType (ForAllTy tyvar ty) = filter (/= tyvar) (fvType ty)
1753
1754 fvTypes :: [Type] -> [TyVar]
1755 fvTypes tys                = concat (map fvType tys)
1756
1757 fvPred :: PredType -> [TyVar]
1758 fvPred (ClassP _ tys')     = fvTypes tys'
1759 fvPred (IParam _ ty)       = fvType ty
1760 fvPred (EqPred ty1 ty2)    = fvType ty1 ++ fvType ty2
1761
1762 -- Size of a type: the number of variables and constructors
1763 sizeType :: Type -> Int
1764 sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty
1765 sizeType (TyVarTy _)       = 1
1766 sizeType (TyConApp _ tys)  = sizeTypes tys + 1
1767 sizeType (PredTy pred)     = sizePred pred
1768 sizeType (FunTy arg res)   = sizeType arg + sizeType res + 1
1769 sizeType (AppTy fun arg)   = sizeType fun + sizeType arg
1770 sizeType (ForAllTy _ ty)   = sizeType ty
1771
1772 sizeTypes :: [Type] -> Int
1773 sizeTypes xs               = sum (map sizeType xs)
1774
1775 sizePred :: PredType -> Int
1776 sizePred (ClassP _ tys')   = sizeTypes tys'
1777 sizePred (IParam _ ty)     = sizeType ty
1778 sizePred (EqPred ty1 ty2)  = sizeType ty1 + sizeType ty2
1779 \end{code}