Refactoring around TyCon.isSynTyCon
[ghc.git] / compiler / typecheck / TcValidity.lhs
1 %
2 % (c) The University of Glasgow 2006
3 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 %
5
6 \begin{code}
7 {-# LANGUAGE CPP #-}
8
9 module TcValidity (
10   Rank, UserTypeCtxt(..), checkValidType, checkValidMonoType,
11   expectedKindInCtxt, 
12   checkValidTheta, checkValidFamPats,
13   checkValidInstance, validDerivPred,
14   checkInstTermination, checkValidTyFamInst, checkTyFamFreeness, 
15   checkConsistentFamInst,
16   arityErr, badATErr
17   ) where
18
19 #include "HsVersions.h"
20
21 -- friends:
22 import TcUnify    ( tcSubType )
23 import TcSimplify ( simplifyAmbiguityCheck )
24 import TypeRep
25 import TcType
26 import TcMType
27 import TysWiredIn ( coercibleClass )
28 import Type
29 import Unify( tcMatchTyX )
30 import Kind
31 import CoAxiom
32 import Class
33 import TyCon
34
35 -- others:
36 import HsSyn            -- HsType
37 import TcRnMonad        -- TcType, amongst others
38 import FunDeps
39 import Name
40 import VarEnv
41 import VarSet
42 import ErrUtils
43 import DynFlags
44 import Util
45 import ListSetOps
46 import SrcLoc
47 import Outputable
48 import FastString
49 import BasicTypes ( Arity )
50
51 import Control.Monad
52 import Data.Maybe
53 import Data.List        ( (\\) )
54 \end{code}
55  
56
57 %************************************************************************
58 %*                                                                      *
59           Checking for ambiguity
60 %*                                                                      *
61 %************************************************************************
62
63
64 \begin{code}
65 checkAmbiguity :: UserTypeCtxt -> Type -> TcM ()
66 checkAmbiguity ctxt ty
67   | GhciCtxt <- ctxt    -- Allow ambiguous types in GHCi's :kind command
68   = return ()           -- E.g.   type family T a :: *  -- T :: forall k. k -> *
69                         -- Then :k T should work in GHCi, not complain that
70                         -- (T k) is ambiguous!
71
72   | otherwise
73   = do { traceTc "Ambiguity check for" (ppr ty)
74        ; (subst, _tvs) <- tcInstSkolTyVars (varSetElems (tyVarsOfType ty))
75        ; let ty' = substTy subst ty
76               -- The type might have free TyVars,
77               -- so we skolemise them as TcTyVars
78               -- Tiresome; but the type inference engine expects TcTyVars
79
80          -- Solve the constraints eagerly because an ambiguous type
81          -- can cause a cascade of further errors.  Since the free
82          -- tyvars are skolemised, we can safely use tcSimplifyTop
83        ; (_wrap, wanted) <- addErrCtxtM (mk_msg ty') $
84                             captureConstraints $
85                             tcSubType (AmbigOrigin ctxt) ctxt ty' ty'
86        ; simplifyAmbiguityCheck ty wanted
87
88        ; traceTc "Done ambiguity check for" (ppr ty) }
89  where
90    mk_msg ty tidy_env
91      = do { allow_ambiguous <- xoptM Opt_AllowAmbiguousTypes
92           ; return (tidy_env', msg $$ ppWhen (not allow_ambiguous) ambig_msg) }
93      where
94        (tidy_env', tidy_ty) = tidyOpenType tidy_env ty
95        msg = hang (ptext (sLit "In the ambiguity check for:"))
96                 2 (ppr tidy_ty)
97        ambig_msg = ptext (sLit "To defer the ambiguity check to use sites, enable AllowAmbiguousTypes")
98 \end{code}
99
100
101 %************************************************************************
102 %*                                                                      *
103           Checking validity of a user-defined type
104 %*                                                                      *
105 %************************************************************************
106
107 When dealing with a user-written type, we first translate it from an HsType
108 to a Type, performing kind checking, and then check various things that should 
109 be true about it.  We don't want to perform these checks at the same time
110 as the initial translation because (a) they are unnecessary for interface-file
111 types and (b) when checking a mutually recursive group of type and class decls,
112 we can't "look" at the tycons/classes yet.  Also, the checks are are rather
113 diverse, and used to really mess up the other code.
114
115 One thing we check for is 'rank'.  
116
117         Rank 0:         monotypes (no foralls)
118         Rank 1:         foralls at the front only, Rank 0 inside
119         Rank 2:         foralls at the front, Rank 1 on left of fn arrow,
120
121         basic ::= tyvar | T basic ... basic
122
123         r2  ::= forall tvs. cxt => r2a
124         r2a ::= r1 -> r2a | basic
125         r1  ::= forall tvs. cxt => r0
126         r0  ::= r0 -> r0 | basic
127         
128 Another thing is to check that type synonyms are saturated. 
129 This might not necessarily show up in kind checking.
130         type A i = i
131         data T k = MkT (k Int)
132         f :: T A        -- BAD!
133
134         
135 \begin{code}
136 checkValidType :: UserTypeCtxt -> Type -> TcM ()
137 -- Checks that the type is valid for the given context
138 -- Not used for instance decls; checkValidInstance instead
139 checkValidType ctxt ty 
140   = do { traceTc "checkValidType" (ppr ty <+> text "::" <+> ppr (typeKind ty))
141        ; rankn_flag  <- xoptM Opt_RankNTypes
142        ; let gen_rank :: Rank -> Rank
143              gen_rank r | rankn_flag = ArbitraryRank
144                         | otherwise  = r
145
146              rank1 = gen_rank r1
147              rank0 = gen_rank r0
148
149              r0 = rankZeroMonoType
150              r1 = LimitedRank True r0
151
152              rank
153                = case ctxt of
154                  DefaultDeclCtxt-> MustBeMonoType
155                  ResSigCtxt     -> MustBeMonoType
156                  LamPatSigCtxt  -> rank0
157                  BindPatSigCtxt -> rank0
158                  RuleSigCtxt _  -> rank1
159                  TySynCtxt _    -> rank0
160
161                  ExprSigCtxt    -> rank1
162                  FunSigCtxt _   -> rank1
163                  InfSigCtxt _   -> ArbitraryRank        -- Inferred type
164                  ConArgCtxt _   -> rank1 -- We are given the type of the entire
165                                          -- constructor, hence rank 1
166
167                  ForSigCtxt _   -> rank1
168                  SpecInstCtxt   -> rank1
169                  ThBrackCtxt    -> rank1
170                  GhciCtxt       -> ArbitraryRank
171                  _              -> panic "checkValidType"
172                                           -- Can't happen; not used for *user* sigs
173
174         -- Check the internal validity of the type itself
175        ; check_type ctxt rank ty
176
177         -- Check that the thing has kind Type, and is lifted if necessary
178         -- Do this second, because we can't usefully take the kind of an 
179         -- ill-formed type such as (a~Int)
180        ; check_kind ctxt ty
181        ; traceTc "checkValidType done" (ppr ty <+> text "::" <+> ppr (typeKind ty)) }
182
183 checkValidMonoType :: Type -> TcM ()
184 checkValidMonoType ty = check_mono_type SigmaCtxt MustBeMonoType ty
185
186
187 check_kind :: UserTypeCtxt -> TcType -> TcM ()
188 -- Check that the type's kind is acceptable for the context
189 check_kind ctxt ty
190   | TySynCtxt {} <- ctxt
191   = do { ck <- xoptM Opt_ConstraintKinds
192        ; unless ck $
193          checkTc (not (returnsConstraintKind actual_kind)) 
194                  (constraintSynErr actual_kind) }
195
196   | Just k <- expectedKindInCtxt ctxt
197   = checkTc (tcIsSubKind actual_kind k) (kindErr actual_kind)
198
199   | otherwise
200   = return ()   -- Any kind will do
201   where
202     actual_kind = typeKind ty
203
204 -- Depending on the context, we might accept any kind (for instance, in a TH
205 -- splice), or only certain kinds (like in type signatures).
206 expectedKindInCtxt :: UserTypeCtxt -> Maybe Kind
207 expectedKindInCtxt (TySynCtxt _)  = Nothing -- Any kind will do
208 expectedKindInCtxt ThBrackCtxt    = Nothing
209 expectedKindInCtxt GhciCtxt       = Nothing
210 expectedKindInCtxt (ForSigCtxt _) = Just liftedTypeKind
211 expectedKindInCtxt InstDeclCtxt   = Just constraintKind
212 expectedKindInCtxt SpecInstCtxt   = Just constraintKind
213 expectedKindInCtxt _              = Just openTypeKind
214 \end{code}
215
216 Note [Higher rank types]
217 ~~~~~~~~~~~~~~~~~~~~~~~~
218 Technically 
219             Int -> forall a. a->a
220 is still a rank-1 type, but it's not Haskell 98 (Trac #5957).  So the
221 validity checker allow a forall after an arrow only if we allow it
222 before -- that is, with Rank2Types or RankNTypes
223
224 \begin{code}
225 data Rank = ArbitraryRank         -- Any rank ok
226
227           | LimitedRank   -- Note [Higher rank types]
228                  Bool     -- Forall ok at top
229                  Rank     -- Use for function arguments
230
231           | MonoType SDoc   -- Monotype, with a suggestion of how it could be a polytype
232   
233           | MustBeMonoType  -- Monotype regardless of flags
234
235 rankZeroMonoType, tyConArgMonoType, synArgMonoType :: Rank
236 rankZeroMonoType = MonoType (ptext (sLit "Perhaps you intended to use RankNTypes or Rank2Types"))
237 tyConArgMonoType = MonoType (ptext (sLit "Perhaps you intended to use ImpredicativeTypes"))
238 synArgMonoType   = MonoType (ptext (sLit "Perhaps you intended to use LiberalTypeSynonyms"))
239
240 funArgResRank :: Rank -> (Rank, Rank)             -- Function argument and result
241 funArgResRank (LimitedRank _ arg_rank) = (arg_rank, LimitedRank (forAllAllowed arg_rank) arg_rank)
242 funArgResRank other_rank               = (other_rank, other_rank)
243
244 forAllAllowed :: Rank -> Bool
245 forAllAllowed ArbitraryRank             = True
246 forAllAllowed (LimitedRank forall_ok _) = forall_ok
247 forAllAllowed _                         = False
248
249 ----------------------------------------
250 check_mono_type :: UserTypeCtxt -> Rank
251                 -> KindOrType -> TcM () -- No foralls anywhere
252                                         -- No unlifted types of any kind
253 check_mono_type ctxt rank ty
254   | isKind ty = return ()  -- IA0_NOTE: Do we need to check kinds?
255   | otherwise
256    = do { check_type ctxt rank ty
257         ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
258
259 check_type :: UserTypeCtxt -> Rank -> Type -> TcM ()
260 -- The args say what the *type context* requires, independent
261 -- of *flag* settings.  You test the flag settings at usage sites.
262 -- 
263 -- Rank is allowed rank for function args
264 -- Rank 0 means no for-alls anywhere
265
266 check_type ctxt rank ty
267   | not (null tvs && null theta)
268   = do  { checkTc (forAllAllowed rank) (forAllTyErr rank ty)
269                 -- Reject e.g. (Maybe (?x::Int => Int)), 
270                 -- with a decent error message
271         ; check_valid_theta ctxt theta
272         ; check_type ctxt rank tau      -- Allow foralls to right of arrow
273         ; checkAmbiguity ctxt ty }
274   where
275     (tvs, theta, tau) = tcSplitSigmaTy ty
276    
277 check_type _ _ (TyVarTy _) = return ()
278
279 check_type ctxt rank (FunTy arg_ty res_ty)
280   = do  { check_type ctxt arg_rank arg_ty
281         ; check_type ctxt res_rank res_ty }
282   where
283     (arg_rank, res_rank) = funArgResRank rank
284
285 check_type ctxt rank (AppTy ty1 ty2)
286   = do  { check_arg_type ctxt rank ty1
287         ; check_arg_type ctxt rank ty2 }
288
289 check_type ctxt rank ty@(TyConApp tc tys)
290   | isTypeSynonymTyCon tc  = check_syn_tc_app ctxt rank ty tc tys
291   | isUnboxedTupleTyCon tc = check_ubx_tuple  ctxt      ty    tys
292   | otherwise              = mapM_ (check_arg_type ctxt rank) tys
293
294 check_type _ _ (LitTy {}) = return ()
295
296 check_type _ _ ty = pprPanic "check_type" (ppr ty)
297
298 ----------------------------------------
299 check_syn_tc_app :: UserTypeCtxt -> Rank -> KindOrType 
300                  -> TyCon -> [KindOrType] -> TcM ()
301 check_syn_tc_app ctxt rank ty tc tys
302   | tc_arity <= n_args   -- Saturated
303        -- Check that the synonym has enough args
304        -- This applies equally to open and closed synonyms
305        -- It's OK to have an *over-applied* type synonym
306        --      data Tree a b = ...
307        --      type Foo a = Tree [a]
308        --      f :: Foo a b -> ...
309   = do  { -- See Note [Liberal type synonyms]
310         ; liberal <- xoptM Opt_LiberalTypeSynonyms
311         ; if not liberal || isSynFamilyTyCon tc then
312                 -- For H98 and synonym families, do check the type args
313                 mapM_ check_arg tys
314
315           else  -- In the liberal case (only for closed syns), expand then check
316           case tcView ty of   
317              Just ty' -> check_type ctxt rank ty' 
318              Nothing  -> pprPanic "check_tau_type" (ppr ty)  }
319
320   | GhciCtxt <- ctxt  -- Accept under-saturated type synonyms in 
321                       -- GHCi :kind commands; see Trac #7586
322   = mapM_ check_arg tys
323
324   | otherwise
325   = failWithTc (arityErr "Type synonym" (tyConName tc) tc_arity n_args)
326   where
327     n_args = length tys
328     tc_arity  = tyConArity tc
329     check_arg | isSynFamilyTyCon tc = check_arg_type  ctxt rank
330               | otherwise           = check_mono_type ctxt synArgMonoType
331          
332 ----------------------------------------
333 check_ubx_tuple :: UserTypeCtxt -> KindOrType 
334                 -> [KindOrType] -> TcM ()
335 check_ubx_tuple ctxt ty tys
336   = do  { ub_tuples_allowed <- xoptM Opt_UnboxedTuples
337         ; checkTc ub_tuples_allowed (ubxArgTyErr ty)
338
339         ; impred <- xoptM Opt_ImpredicativeTypes        
340         ; let rank' = if impred then ArbitraryRank else tyConArgMonoType
341                 -- c.f. check_arg_type
342                 -- However, args are allowed to be unlifted, or
343                 -- more unboxed tuples, so can't use check_arg_ty
344         ; mapM_ (check_type ctxt rank') tys }
345     
346 ----------------------------------------
347 check_arg_type :: UserTypeCtxt -> Rank -> KindOrType -> TcM ()
348 -- The sort of type that can instantiate a type variable,
349 -- or be the argument of a type constructor.
350 -- Not an unboxed tuple, but now *can* be a forall (since impredicativity)
351 -- Other unboxed types are very occasionally allowed as type
352 -- arguments depending on the kind of the type constructor
353 -- 
354 -- For example, we want to reject things like:
355 --
356 --      instance Ord a => Ord (forall s. T s a)
357 -- and
358 --      g :: T s (forall b.b)
359 --
360 -- NB: unboxed tuples can have polymorphic or unboxed args.
361 --     This happens in the workers for functions returning
362 --     product types with polymorphic components.
363 --     But not in user code.
364 -- Anyway, they are dealt with by a special case in check_tau_type
365
366 check_arg_type ctxt rank ty
367   | isKind ty = return ()  -- IA0_NOTE: Do we need to check a kind?
368   | otherwise
369   = do  { impred <- xoptM Opt_ImpredicativeTypes
370         ; let rank' = case rank of          -- Predictive => must be monotype
371                         MustBeMonoType     -> MustBeMonoType  -- Monotype, regardless
372                         _other | impred    -> ArbitraryRank
373                                | otherwise -> tyConArgMonoType
374                         -- Make sure that MustBeMonoType is propagated, 
375                         -- so that we don't suggest -XImpredicativeTypes in
376                         --    (Ord (forall a.a)) => a -> a
377                         -- and so that if it Must be a monotype, we check that it is!
378
379         ; check_type ctxt rank' ty
380         ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
381              -- NB the isUnLiftedType test also checks for 
382              --    T State#
383              -- where there is an illegal partial application of State# (which has
384              -- kind * -> #); see Note [The kind invariant] in TypeRep
385
386 ----------------------------------------
387 forAllTyErr :: Rank -> Type -> SDoc
388 forAllTyErr rank ty 
389    = vcat [ hang (ptext (sLit "Illegal polymorphic or qualified type:")) 2 (ppr ty)
390           , suggestion ]
391   where
392     suggestion = case rank of
393                    LimitedRank {} -> ptext (sLit "Perhaps you intended to use RankNTypes or Rank2Types")
394                    MonoType d     -> d
395                    _              -> empty      -- Polytype is always illegal
396
397 unliftedArgErr, ubxArgTyErr :: Type -> SDoc
398 unliftedArgErr  ty = sep [ptext (sLit "Illegal unlifted type:"), ppr ty]
399 ubxArgTyErr     ty = sep [ptext (sLit "Illegal unboxed tuple type as function argument:"), ppr ty]
400
401 kindErr :: Kind -> SDoc
402 kindErr kind = sep [ptext (sLit "Expecting an ordinary type, but found a type of kind"), ppr kind]
403 \end{code}
404
405 Note [Liberal type synonyms]
406 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
407 If -XLiberalTypeSynonyms is on, expand closed type synonyms *before*
408 doing validity checking.  This allows us to instantiate a synonym defn
409 with a for-all type, or with a partially-applied type synonym.
410         e.g.   type T a b = a
411                type S m   = m ()
412                f :: S (T Int)
413 Here, T is partially applied, so it's illegal in H98.  But if you
414 expand S first, then T we get just
415                f :: Int
416 which is fine.
417
418 IMPORTANT: suppose T is a type synonym.  Then we must do validity
419 checking on an appliation (T ty1 ty2)
420
421         *either* before expansion (i.e. check ty1, ty2)
422         *or* after expansion (i.e. expand T ty1 ty2, and then check)
423         BUT NOT BOTH
424
425 If we do both, we get exponential behaviour!!
426
427   data TIACons1 i r c = c i ::: r c
428   type TIACons2 t x = TIACons1 t (TIACons1 t x)
429   type TIACons3 t x = TIACons2 t (TIACons1 t x)
430   type TIACons4 t x = TIACons2 t (TIACons2 t x)
431   type TIACons7 t x = TIACons4 t (TIACons3 t x)
432
433
434 %************************************************************************
435 %*                                                                      *
436 \subsection{Checking a theta or source type}
437 %*                                                                      *
438 %************************************************************************
439
440 Note [Implicit parameters in instance decls]
441 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
442 Implicit parameters _only_ allowed in type signatures; not in instance
443 decls, superclasses etc. The reason for not allowing implicit params in
444 instances is a bit subtle.  If we allowed
445   instance (?x::Int, Eq a) => Foo [a] where ...
446 then when we saw
447      (e :: (?x::Int) => t)
448 it would be unclear how to discharge all the potential uses of the ?x
449 in e.  For example, a constraint Foo [Int] might come out of e, and
450 applying the instance decl would show up two uses of ?x.  Trac #8912.
451
452 \begin{code}
453 checkValidTheta :: UserTypeCtxt -> ThetaType -> TcM ()
454 checkValidTheta ctxt theta
455   = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
456
457 -------------------------
458 check_valid_theta :: UserTypeCtxt -> [PredType] -> TcM ()
459 check_valid_theta _ []
460   = return ()
461 check_valid_theta ctxt theta
462   = do { dflags <- getDynFlags
463        ; warnTc (wopt Opt_WarnDuplicateConstraints dflags &&
464                  notNull dups) (dupPredWarn dups)
465        ; mapM_ (check_pred_ty dflags ctxt) theta }
466   where
467     (_,dups) = removeDups cmpPred theta
468
469 -------------------------
470 check_pred_ty :: DynFlags -> UserTypeCtxt -> PredType -> TcM ()
471 -- Check the validity of a predicate in a signature
472 -- We look through any type synonyms; any constraint kinded
473 -- type synonyms have been checked at their definition site
474
475 check_pred_ty dflags ctxt pred
476   = case classifyPredType pred of
477       ClassPred cls tys -> check_class_pred dflags ctxt pred cls tys
478       EqPred ty1 ty2    -> check_eq_pred    dflags ctxt pred ty1 ty2
479       TuplePred tys     -> check_tuple_pred dflags ctxt pred tys
480       IrredPred _       -> check_irred_pred dflags ctxt pred
481
482
483 check_class_pred :: DynFlags -> UserTypeCtxt -> PredType -> Class -> [TcType] -> TcM ()
484 check_class_pred dflags ctxt pred cls tys
485   = do {        -- Class predicates are valid in all contexts
486        ; checkTc (arity == n_tys) arity_err
487
488        ; checkTc (not (isIPClass cls) || okIPCtxt ctxt)
489                  (badIPPred pred)
490
491                 -- Check the form of the argument types
492        ; mapM_ checkValidMonoType tys
493        ; checkTc (check_class_pred_tys dflags ctxt tys)
494                  (predTyVarErr (mkClassPred cls tys) $$ how_to_allow)
495        }
496   where
497     class_name = className cls
498     arity      = classArity cls
499     n_tys      = length tys
500     arity_err  = arityErr "Class" class_name arity n_tys
501     how_to_allow = parens (ptext (sLit "Use FlexibleContexts to permit this"))
502
503 okIPCtxt :: UserTypeCtxt -> Bool
504   -- See Note [Implicit parameters in instance decls]
505 okIPCtxt (ClassSCCtxt {})  = False
506 okIPCtxt (InstDeclCtxt {}) = False
507 okIPCtxt (SpecInstCtxt {}) = False
508 okIPCtxt _                 = True
509
510 badIPPred :: PredType -> SDoc
511 badIPPred pred = ptext (sLit "Illegal implict parameter") <+> quotes (ppr pred)
512
513
514 check_eq_pred :: DynFlags -> UserTypeCtxt -> PredType -> TcType -> TcType -> TcM ()
515 check_eq_pred dflags _ctxt pred ty1 ty2
516   = do {        -- Equational constraints are valid in all contexts if type
517                 -- families are permitted
518        ; checkTc (xopt Opt_TypeFamilies dflags || xopt Opt_GADTs dflags) 
519                  (eqPredTyErr pred)
520
521                 -- Check the form of the argument types
522        ; checkValidMonoType ty1
523        ; checkValidMonoType ty2
524        }
525
526 check_tuple_pred :: DynFlags -> UserTypeCtxt -> PredType -> [PredType] -> TcM ()
527 check_tuple_pred dflags ctxt pred ts
528   = do { checkTc (xopt Opt_ConstraintKinds dflags)
529                  (predTupleErr pred)
530        ; mapM_ (check_pred_ty dflags ctxt) ts }
531     -- This case will not normally be executed because 
532     -- without -XConstraintKinds tuple types are only kind-checked as *
533
534 check_irred_pred :: DynFlags -> UserTypeCtxt -> PredType -> TcM ()
535 check_irred_pred dflags ctxt pred
536     -- The predicate looks like (X t1 t2) or (x t1 t2) :: Constraint
537     -- But X is not a synonym; that's been expanded already
538     --
539     -- Allowing irreducible predicates in class superclasses is somewhat dangerous
540     -- because we can write:
541     --
542     --  type family Fooish x :: * -> Constraint
543     --  type instance Fooish () = Foo
544     --  class Fooish () a => Foo a where
545     --
546     -- This will cause the constraint simplifier to loop because every time we canonicalise a
547     -- (Foo a) class constraint we add a (Fooish () a) constraint which will be immediately
548     -- solved to add+canonicalise another (Foo a) constraint.
549     --
550     -- It is equally dangerous to allow them in instance heads because in that case the
551     -- Paterson conditions may not detect duplication of a type variable or size change.
552   = do { checkValidMonoType pred
553        ; checkTc (xopt Opt_ConstraintKinds dflags)
554                  (predIrredErr pred)
555        ; unless (xopt Opt_UndecidableInstances dflags) $
556                  -- Make sure it is OK to have an irred pred in this context
557          checkTc (case ctxt of ClassSCCtxt _ -> False; InstDeclCtxt -> False; _ -> True)
558                  (predIrredBadCtxtErr pred) }
559
560 -------------------------
561 check_class_pred_tys :: DynFlags -> UserTypeCtxt -> [KindOrType] -> Bool
562 check_class_pred_tys dflags ctxt kts
563   = case ctxt of
564         SpecInstCtxt -> True    -- {-# SPECIALISE instance Eq (T Int) #-} is fine
565         InstDeclCtxt -> flexible_contexts || undecidable_ok || all tcIsTyVarTy tys
566                                 -- Further checks on head and theta in
567                                 -- checkInstTermination
568         _             -> flexible_contexts || all tyvar_head tys
569   where
570     (_, tys) = span isKind kts  -- see Note [Kind polymorphic type classes]
571     flexible_contexts = xopt Opt_FlexibleContexts dflags
572     undecidable_ok = xopt Opt_UndecidableInstances dflags
573
574 -------------------------
575 tyvar_head :: Type -> Bool
576 tyvar_head ty                   -- Haskell 98 allows predicates of form 
577   | tcIsTyVarTy ty = True       --      C (a ty1 .. tyn)
578   | otherwise                   -- where a is a type variable
579   = case tcSplitAppTy_maybe ty of
580         Just (ty, _) -> tyvar_head ty
581         Nothing      -> False
582 \end{code}
583
584 Note [Kind polymorphic type classes]
585 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
586 MultiParam check:
587
588     class C f where...   -- C :: forall k. k -> Constraint
589     instance C Maybe where...
590
591   The dictionary gets type [C * Maybe] even if it's not a MultiParam
592   type class.
593
594 Flexibility check:
595
596     class C f where...   -- C :: forall k. k -> Constraint
597     data D a = D a
598     instance C D where
599
600   The dictionary gets type [C * (D *)]. IA0_TODO it should be
601   generalized actually.
602
603 Note [The ambiguity check for type signatures]
604 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
605 checkAmbiguity is a check on user-supplied type signatures.  It is
606 *purely* there to report functions that cannot possibly be called.  So for
607 example we want to reject:
608    f :: C a => Int
609 The idea is there can be no legal calls to 'f' because every call will
610 give rise to an ambiguous constraint.  We could soundly omit the
611 ambiguity check on type signatures entirely, at the expense of
612 delaying ambiguity errors to call sites.  Indeed, the flag 
613 -XAllowAmbiguousTypes switches off the ambiguity check.
614
615 What about things like this:
616    class D a b | a -> b where ..
617    h :: D Int b => Int 
618 The Int may well fix 'b' at the call site, so that signature should
619 not be rejected.  Moreover, using *visible* fundeps is too
620 conservative.  Consider
621    class X a b where ...
622    class D a b | a -> b where ...
623    instance D a b => X [a] b where...
624    h :: X a b => a -> a
625 Here h's type looks ambiguous in 'b', but here's a legal call:
626    ...(h [True])...
627 That gives rise to a (X [Bool] beta) constraint, and using the
628 instance means we need (D Bool beta) and that fixes 'beta' via D's
629 fundep!
630
631 Behind all these special cases there is a simple guiding principle. 
632 Consider
633
634   f :: <type>
635   f = ...blah...
636
637   g :: <type>
638   g = f
639
640 You would think that the definition of g would surely typecheck!
641 After all f has exactly the same type, and g=f. But in fact f's type
642 is instantiated and the instantiated constraints are solved against
643 the originals, so in the case an ambiguous type it won't work.
644 Consider our earlier example f :: C a => Int.  Then in g's definition,
645 we'll instantiate to (C alpha) and try to deduce (C alpha) from (C a),
646 and fail.  
647
648 So in fact we use this as our *definition* of ambiguity.  We use a
649 very similar test for *inferred* types, to ensure that they are
650 unambiguous. See Note [Impedence matching] in TcBinds.
651
652 This test is very conveniently implemented by calling
653     tcSubType <type> <type>
654 This neatly takes account of the functional dependecy stuff above, 
655 and implict parameter (see Note [Implicit parameters and ambiguity]).
656
657 What about this, though?
658    g :: C [a] => Int
659 Is every call to 'g' ambiguous?  After all, we might have
660    intance C [a] where ...
661 at the call site.  So maybe that type is ok!  Indeed even f's
662 quintessentially ambiguous type might, just possibly be callable: 
663 with -XFlexibleInstances we could have
664   instance C a where ...
665 and now a call could be legal after all!  Well, we'll reject this
666 unless the instance is available *here*.
667
668 Side note: the ambiguity check is only used for *user* types, not for
669 types coming from inteface files.  The latter can legitimately have
670 ambiguous types. Example
671
672    class S a where s :: a -> (Int,Int)
673    instance S Char where s _ = (1,1)
674    f:: S a => [a] -> Int -> (Int,Int)
675    f (_::[a]) x = (a*x,b)
676         where (a,b) = s (undefined::a)
677
678 Here the worker for f gets the type
679         fw :: forall a. S a => Int -> (# Int, Int #)
680
681 Note [Implicit parameters and ambiguity] 
682 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
683 Only a *class* predicate can give rise to ambiguity
684 An *implicit parameter* cannot.  For example:
685         foo :: (?x :: [a]) => Int
686         foo = length ?x
687 is fine.  The call site will suppply a particular 'x'
688
689 Furthermore, the type variables fixed by an implicit parameter
690 propagate to the others.  E.g.
691         foo :: (Show a, ?x::[a]) => Int
692         foo = show (?x++?x)
693 The type of foo looks ambiguous.  But it isn't, because at a call site
694 we might have
695         let ?x = 5::Int in foo
696 and all is well.  In effect, implicit parameters are, well, parameters,
697 so we can take their type variables into account as part of the
698 "tau-tvs" stuff.  This is done in the function 'FunDeps.grow'.
699 \begin{code}
700 checkThetaCtxt :: UserTypeCtxt -> ThetaType -> SDoc
701 checkThetaCtxt ctxt theta
702   = vcat [ptext (sLit "In the context:") <+> pprTheta theta,
703           ptext (sLit "While checking") <+> pprUserTypeCtxt ctxt ]
704
705 eqPredTyErr, predTyVarErr, predTupleErr, predIrredErr, predIrredBadCtxtErr :: PredType -> SDoc
706 eqPredTyErr  pred = ptext (sLit "Illegal equational constraint") <+> pprType pred
707                     $$
708                     parens (ptext (sLit "Use GADTs or TypeFamilies to permit this"))
709 predTyVarErr pred  = hang (ptext (sLit "Non type-variable argument"))
710                         2 (ptext (sLit "in the constraint:") <+> pprType pred)
711 predTupleErr pred  = hang (ptext (sLit "Illegal tuple constraint:") <+> pprType pred)
712                         2 (parens (ptext (sLit "Use ConstraintKinds to permit this")))
713 predIrredErr pred  = hang (ptext (sLit "Illegal constraint:") <+> pprType pred)
714                         2 (parens (ptext (sLit "Use ConstraintKinds to permit this")))
715 predIrredBadCtxtErr pred = hang (ptext (sLit "Illegal constraint") <+> quotes (pprType pred)
716                                  <+> ptext (sLit "in a superclass/instance context")) 
717                                2 (parens (ptext (sLit "Use UndecidableInstances to permit this")))
718
719 constraintSynErr :: Type -> SDoc
720 constraintSynErr kind = hang (ptext (sLit "Illegal constraint synonym of kind:") <+> quotes (ppr kind))
721                            2 (parens (ptext (sLit "Use ConstraintKinds to permit this")))
722
723 dupPredWarn :: [[PredType]] -> SDoc
724 dupPredWarn dups   = ptext (sLit "Duplicate constraint(s):") <+> pprWithCommas pprType (map head dups)
725
726 arityErr :: Outputable a => String -> a -> Int -> Int -> SDoc
727 arityErr kind name n m
728   = hsep [ text kind, quotes (ppr name), ptext (sLit "should have"),
729            n_arguments <> comma, text "but has been given", 
730            if m==0 then text "none" else int m]
731     where
732         n_arguments | n == 0 = ptext (sLit "no arguments")
733                     | n == 1 = ptext (sLit "1 argument")
734                     | True   = hsep [int n, ptext (sLit "arguments")]
735 \end{code}
736
737 %************************************************************************
738 %*                                                                      *
739 \subsection{Checking for a decent instance head type}
740 %*                                                                      *
741 %************************************************************************
742
743 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
744 it must normally look like: @instance Foo (Tycon a b c ...) ...@
745
746 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
747 flag is on, or (2)~the instance is imported (they must have been
748 compiled elsewhere). In these cases, we let them go through anyway.
749
750 We can also have instances for functions: @instance Foo (a -> b) ...@.
751
752 \begin{code}
753 checkValidInstHead :: UserTypeCtxt -> Class -> [Type] -> TcM ()
754 checkValidInstHead ctxt clas cls_args
755   = do { dflags <- getDynFlags
756
757        ; checkTc (clas `notElem` abstractClasses)
758                  (instTypeErr clas cls_args abstract_class_msg)
759
760            -- Check language restrictions; 
761            -- but not for SPECIALISE isntance pragmas
762        ; let ty_args = dropWhile isKind cls_args
763        ; unless spec_inst_prag $
764          do { checkTc (xopt Opt_TypeSynonymInstances dflags ||
765                        all tcInstHeadTyNotSynonym ty_args)
766                  (instTypeErr clas cls_args head_type_synonym_msg)
767             ; checkTc (xopt Opt_FlexibleInstances dflags ||
768                        all tcInstHeadTyAppAllTyVars ty_args)
769                  (instTypeErr clas cls_args head_type_args_tyvars_msg)
770             ; checkTc (xopt Opt_NullaryTypeClasses dflags ||
771                        not (null ty_args))
772                  (instTypeErr clas cls_args head_no_type_msg)
773             ; checkTc (xopt Opt_MultiParamTypeClasses dflags ||
774                        length ty_args <= 1)  -- Only count type arguments
775                  (instTypeErr clas cls_args head_one_type_msg) }
776
777          -- May not contain type family applications
778        ; mapM_ checkTyFamFreeness ty_args
779
780        ; mapM_ checkValidMonoType ty_args
781         -- For now, I only allow tau-types (not polytypes) in 
782         -- the head of an instance decl.  
783         --      E.g.  instance C (forall a. a->a) is rejected
784         -- One could imagine generalising that, but I'm not sure
785         -- what all the consequences might be
786        }
787
788   where
789     spec_inst_prag = case ctxt of { SpecInstCtxt -> True; _ -> False }
790
791     head_type_synonym_msg = parens (
792                 text "All instance types must be of the form (T t1 ... tn)" $$
793                 text "where T is not a synonym." $$
794                 text "Use TypeSynonymInstances if you want to disable this.")
795
796     head_type_args_tyvars_msg = parens (vcat [
797                 text "All instance types must be of the form (T a1 ... an)",
798                 text "where a1 ... an are *distinct type variables*,",
799                 text "and each type variable appears at most once in the instance head.",
800                 text "Use FlexibleInstances if you want to disable this."])
801
802     head_one_type_msg = parens (
803                 text "Only one type can be given in an instance head." $$
804                 text "Use MultiParamTypeClasses if you want to allow more.")
805
806     head_no_type_msg = parens (
807                 text "No parameters in the instance head." $$
808                 text "Use NullaryTypeClasses if you want to allow this.")
809
810     abstract_class_msg =
811                 text "The class is abstract, manual instances are not permitted."
812
813 abstractClasses :: [ Class ]
814 abstractClasses = [ coercibleClass ] -- See Note [Coercible Instances]
815
816 instTypeErr :: Class -> [Type] -> SDoc -> SDoc
817 instTypeErr cls tys msg
818   = hang (hang (ptext (sLit "Illegal instance declaration for"))
819              2 (quotes (pprClassPred cls tys)))
820        2 msg
821 \end{code}
822
823 validDeivPred checks for OK 'deriving' context.  See Note [Exotic
824 derived instance contexts] in TcSimplify.  However the predicate is
825 here because it uses sizeTypes, fvTypes.
826
827 Also check for a bizarre corner case, when the derived instance decl 
828 would look like
829     instance C a b => D (T a) where ...
830 Note that 'b' isn't a parameter of T.  This gives rise to all sorts of
831 problems; in particular, it's hard to compare solutions for equality
832 when finding the fixpoint, and that means the inferContext loop does
833 not converge.  See Trac #5287.
834
835 \begin{code}
836 validDerivPred :: TyVarSet -> PredType -> Bool
837 validDerivPred tv_set pred
838   = case classifyPredType pred of
839        ClassPred _ tys -> hasNoDups fvs 
840                        && sizeTypes tys == length fvs
841                        && all (`elemVarSet` tv_set) fvs
842        TuplePred ps -> all (validDerivPred tv_set) ps
843        _            -> True   -- Non-class predicates are ok
844   where
845     fvs = fvType pred
846 \end{code}
847
848
849 %************************************************************************
850 %*                                                                      *
851 \subsection{Checking instance for termination}
852 %*                                                                      *
853 %************************************************************************
854
855 \begin{code}
856 checkValidInstance :: UserTypeCtxt -> LHsType Name -> Type
857                    -> TcM ([TyVar], ThetaType, Class, [Type])
858 checkValidInstance ctxt hs_type ty
859   | Just (clas,inst_tys) <- getClassPredTys_maybe tau
860   , inst_tys `lengthIs` classArity clas
861   = do  { setSrcSpan head_loc (checkValidInstHead ctxt clas inst_tys)
862         ; checkValidTheta ctxt theta
863
864         -- The Termination and Coverate Conditions
865         -- Check that instance inference will terminate (if we care)
866         -- For Haskell 98 this will already have been done by checkValidTheta,
867         -- but as we may be using other extensions we need to check.
868         -- 
869         -- Note that the Termination Condition is *more conservative* than 
870         -- the checkAmbiguity test we do on other type signatures
871         --   e.g.  Bar a => Bar Int is ambiguous, but it also fails
872         --   the termination condition, because 'a' appears more often
873         --   in the constraint than in the head
874         ; undecidable_ok <- xoptM Opt_UndecidableInstances
875         ; if undecidable_ok 
876           then checkAmbiguity ctxt ty
877           else checkInstTermination inst_tys theta
878
879         ; case (checkInstCoverage undecidable_ok clas theta inst_tys) of
880             Nothing  -> return ()   -- Check succeeded
881             Just msg -> addErrTc (instTypeErr clas inst_tys msg)
882                   
883         ; return (tvs, theta, clas, inst_tys) } 
884
885   | otherwise 
886   = failWithTc (ptext (sLit "Malformed instance head:") <+> ppr tau)
887   where
888     (tvs, theta, tau) = tcSplitSigmaTy ty
889
890         -- The location of the "head" of the instance
891     head_loc = case hs_type of
892                  L _ (HsForAllTy _ _ _ (L loc _)) -> loc
893                  L loc _                          -> loc
894 \end{code}
895
896 Note [Paterson conditions]
897 ~~~~~~~~~~~~~~~~~~~~~~~~~~
898 Termination test: the so-called "Paterson conditions" (see Section 5 of
899 "Understanding functionsl dependencies via Constraint Handling Rules, 
900 JFP Jan 2007).
901
902 We check that each assertion in the context satisfies:
903  (1) no variable has more occurrences in the assertion than in the head, and
904  (2) the assertion has fewer constructors and variables (taken together
905      and counting repetitions) than the head.
906 This is only needed with -fglasgow-exts, as Haskell 98 restrictions
907 (which have already been checked) guarantee termination. 
908
909 The underlying idea is that 
910
911     for any ground substitution, each assertion in the
912     context has fewer type constructors than the head.
913
914
915 \begin{code}
916 checkInstTermination :: [TcType] -> ThetaType -> TcM ()
917 -- See Note [Paterson conditions]
918 checkInstTermination tys theta
919   = check_preds theta
920   where
921    fvs  = fvTypes tys
922    size = sizeTypes tys
923
924    check_preds :: [PredType] -> TcM ()
925    check_preds preds = mapM_ check preds
926
927    check :: PredType -> TcM ()
928    check pred 
929      = case classifyPredType pred of
930          TuplePred preds -> check_preds preds  -- Look inside tuple predicates; Trac #8359
931          EqPred {}       -> return ()          -- You can't get from equalities
932                                                -- to class predicates, so this is safe
933          _other      -- ClassPred, IrredPred
934            | not (null bad_tvs)
935            -> addErrTc (predUndecErr pred (nomoreMsg bad_tvs) $$ parens undecidableMsg)
936            | sizePred pred >= size
937            -> addErrTc (predUndecErr pred smallerMsg $$ parens undecidableMsg)
938            | otherwise
939            -> return ()
940      where
941         bad_tvs = filterOut isKindVar (fvType pred \\ fvs)
942              -- Rightly or wrongly, we only check for
943              -- excessive occurrences of *type* variables.
944              -- e.g. type instance Demote {T k} a = T (Demote {k} (Any {k}))
945
946 predUndecErr :: PredType -> SDoc -> SDoc
947 predUndecErr pred msg = sep [msg,
948                         nest 2 (ptext (sLit "in the constraint:") <+> pprType pred)]
949
950 nomoreMsg :: [TcTyVar] -> SDoc
951 nomoreMsg tvs 
952   = sep [ ptext (sLit "Variable") <> plural tvs <+> quotes (pprWithCommas ppr tvs) 
953         , (if isSingleton tvs then ptext (sLit "occurs")
954                                   else ptext (sLit "occur"))
955           <+> ptext (sLit "more often than in the instance head") ]
956
957 smallerMsg, undecidableMsg :: SDoc
958 smallerMsg = ptext (sLit "Constraint is no smaller than the instance head")
959 undecidableMsg = ptext (sLit "Use UndecidableInstances to permit this")
960 \end{code}
961
962
963
964 Note [Associated type instances]
965 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
966 We allow this:
967   class C a where
968     type T x a
969   instance C Int where
970     type T (S y) Int = y
971     type T Z     Int = Char
972
973 Note that 
974   a) The variable 'x' is not bound by the class decl
975   b) 'x' is instantiated to a non-type-variable in the instance
976   c) There are several type instance decls for T in the instance
977
978 All this is fine.  Of course, you can't give any *more* instances
979 for (T ty Int) elsewhere, because it's an *associated* type.
980
981 Note [Checking consistent instantiation]
982 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
983   class C a b where
984     type T a x b
985
986   instance C [p] Int
987     type T [p] y Int = (p,y,y)  -- Induces the family instance TyCon
988                                 --    type TR p y = (p,y,y)
989
990 So we 
991   * Form the mini-envt from the class type variables a,b
992     to the instance decl types [p],Int:   [a->[p], b->Int]
993
994   * Look at the tyvars a,x,b of the type family constructor T
995     (it shares tyvars with the class C)
996
997   * Apply the mini-evnt to them, and check that the result is
998     consistent with the instance types [p] y Int
999
1000 We do *not* assume (at this point) the the bound variables of 
1001 the assoicated type instance decl are the same as for the parent
1002 instance decl. So, for example,
1003
1004   instance C [p] Int
1005     type T [q] y Int = ...
1006
1007 would work equally well. Reason: making the *kind* variables line
1008 up is much harder. Example (Trac #7282):
1009   class Foo (xs :: [k]) where
1010      type Bar xs :: *
1011
1012    instance Foo '[] where
1013      type Bar '[] = Int
1014 Here the instance decl really looks like
1015    instance Foo k ('[] k) where
1016      type Bar k ('[] k) = Int
1017 but the k's are not scoped, and hence won't match Uniques.
1018
1019 So instead we just match structure, with tcMatchTyX, and check
1020 that distinct type variables match 1-1 with distinct type variables.
1021
1022 HOWEVER, we *still* make the instance type variables scope over the
1023 type instances, to pick up non-obvious kinds.  Eg
1024    class Foo (a :: k) where
1025       type F a
1026    instance Foo (b :: k -> k) where
1027       type F b = Int
1028 Here the instance is kind-indexed and really looks like
1029       type F (k->k) (b::k->k) = Int
1030 But if the 'b' didn't scope, we would make F's instance too
1031 poly-kinded.
1032
1033 \begin{code}
1034 checkConsistentFamInst 
1035                :: Maybe ( Class
1036                         , VarEnv Type )  -- ^ Class of associated type
1037                                          -- and instantiation of class TyVars
1038                -> TyCon              -- ^ Family tycon
1039                -> [TyVar]            -- ^ Type variables of the family instance
1040                -> [Type]             -- ^ Type patterns from instance
1041                -> TcM ()
1042 -- See Note [Checking consistent instantiation]
1043
1044 checkConsistentFamInst Nothing _ _ _ = return ()
1045 checkConsistentFamInst (Just (clas, mini_env)) fam_tc at_tvs at_tys
1046   = do { -- Check that the associated type indeed comes from this class
1047          checkTc (Just clas == tyConAssoc_maybe fam_tc)
1048                  (badATErr (className clas) (tyConName fam_tc))
1049
1050          -- See Note [Checking consistent instantiation] in TcTyClsDecls
1051          -- Check right to left, so that we spot type variable
1052          -- inconsistencies before (more confusing) kind variables
1053        ; discardResult $ foldrM check_arg emptyTvSubst $
1054                          tyConTyVars fam_tc `zip` at_tys }
1055   where
1056     at_tv_set = mkVarSet at_tvs
1057
1058     check_arg :: (TyVar, Type) -> TvSubst -> TcM TvSubst
1059     check_arg (fam_tc_tv, at_ty) subst
1060       | Just inst_ty <- lookupVarEnv mini_env fam_tc_tv
1061       = case tcMatchTyX at_tv_set subst at_ty inst_ty of
1062            Just subst | all_distinct subst -> return subst
1063            _ -> failWithTc $ wrongATArgErr at_ty inst_ty
1064                 -- No need to instantiate here, because the axiom
1065                 -- uses the same type variables as the assocated class
1066       | otherwise
1067       = return subst   -- Allow non-type-variable instantiation
1068                        -- See Note [Associated type instances]
1069
1070     all_distinct :: TvSubst -> Bool
1071     -- True if all the variables mapped the substitution 
1072     -- map to *distinct* type *variables*
1073     all_distinct subst = go [] at_tvs
1074        where
1075          go _   []       = True
1076          go acc (tv:tvs) = case lookupTyVar subst tv of
1077                              Nothing -> go acc tvs
1078                              Just ty | Just tv' <- tcGetTyVar_maybe ty
1079                                      , tv' `notElem` acc
1080                                      -> go (tv' : acc) tvs
1081                              _other -> False
1082
1083 badATErr :: Name -> Name -> SDoc
1084 badATErr clas op
1085   = hsep [ptext (sLit "Class"), quotes (ppr clas), 
1086           ptext (sLit "does not have an associated type"), quotes (ppr op)]
1087
1088 wrongATArgErr :: Type -> Type -> SDoc
1089 wrongATArgErr ty instTy =
1090   sep [ ptext (sLit "Type indexes must match class instance head")
1091       , ptext (sLit "Found") <+> quotes (ppr ty)
1092         <+> ptext (sLit "but expected") <+> quotes (ppr instTy)
1093       ]
1094 \end{code}
1095
1096
1097 %************************************************************************
1098 %*                                                                      *
1099         Checking type instance well-formedness and termination
1100 %*                                                                      *
1101 %************************************************************************
1102
1103 \begin{code}
1104 -- Check that a "type instance" is well-formed (which includes decidability
1105 -- unless -XUndecidableInstances is given).
1106 --
1107 checkValidTyFamInst :: Maybe ( Class, VarEnv Type )
1108                     -> TyCon -> CoAxBranch -> TcM ()
1109 checkValidTyFamInst mb_clsinfo fam_tc 
1110                     (CoAxBranch { cab_tvs = tvs, cab_lhs = typats
1111                                 , cab_rhs = rhs, cab_loc = loc })
1112   = setSrcSpan loc $ 
1113     do { checkValidFamPats fam_tc tvs typats
1114
1115          -- The right-hand side is a tau type
1116        ; checkValidMonoType rhs
1117
1118          -- We have a decidable instance unless otherwise permitted
1119        ; undecidable_ok <- xoptM Opt_UndecidableInstances
1120        ; unless undecidable_ok $
1121            mapM_ addErrTc (checkFamInstRhs typats (tcTyFamInsts rhs))
1122
1123          -- Check that type patterns match the class instance head
1124        ; checkConsistentFamInst mb_clsinfo fam_tc tvs typats }
1125
1126 -- Make sure that each type family application is 
1127 --   (1) strictly smaller than the lhs,
1128 --   (2) mentions no type variable more often than the lhs, and
1129 --   (3) does not contain any further type family instances.
1130 --
1131 checkFamInstRhs :: [Type]                  -- lhs
1132                 -> [(TyCon, [Type])]       -- type family instances
1133                 -> [MsgDoc]
1134 checkFamInstRhs lhsTys famInsts
1135   = mapMaybe check famInsts
1136   where
1137    size = sizeTypes lhsTys
1138    fvs  = fvTypes lhsTys
1139    check (tc, tys)
1140       | not (all isTyFamFree tys)
1141       = Just (famInstUndecErr famInst nestedMsg $$ parens undecidableMsg)
1142       | not (null bad_tvs)
1143       = Just (famInstUndecErr famInst (nomoreMsg bad_tvs) $$ parens undecidableMsg)
1144       | size <= sizeTypes tys
1145       = Just (famInstUndecErr famInst smallerAppMsg $$ parens undecidableMsg)
1146       | otherwise
1147       = Nothing
1148       where
1149         famInst = TyConApp tc tys
1150         bad_tvs = filterOut isKindVar (fvTypes tys \\ fvs)
1151              -- Rightly or wrongly, we only check for
1152              -- excessive occurrences of *type* variables.
1153              -- e.g. type instance Demote {T k} a = T (Demote {k} (Any {k}))
1154
1155 checkValidFamPats :: TyCon -> [TyVar] -> [Type] -> TcM ()
1156 -- Patterns in a 'type instance' or 'data instance' decl should
1157 -- a) contain no type family applications
1158 --    (vanilla synonyms are fine, though)
1159 -- b) properly bind all their free type variables
1160 --    e.g. we disallow (Trac #7536)
1161 --         type T a = Int
1162 --         type instance F (T a) = a
1163 -- c) Have the right number of patterns
1164 checkValidFamPats fam_tc tvs ty_pats
1165   = do { -- A family instance must have exactly the same number of type
1166          -- parameters as the family declaration.  You can't write
1167          --     type family F a :: * -> *
1168          --     type instance F Int y = y
1169          -- because then the type (F Int) would be like (\y.y)
1170          checkTc (length ty_pats == fam_arity) $
1171            wrongNumberOfParmsErr (fam_arity - length fam_kvs) -- report only types
1172        ; mapM_ checkTyFamFreeness ty_pats
1173        ; let unbound_tvs = filterOut (`elemVarSet` exactTyVarsOfTypes ty_pats) tvs
1174        ; checkTc (null unbound_tvs) (famPatErr fam_tc unbound_tvs ty_pats) }
1175   where fam_arity    = tyConArity fam_tc
1176         (fam_kvs, _) = splitForAllTys (tyConKind fam_tc)
1177
1178 wrongNumberOfParmsErr :: Arity -> SDoc
1179 wrongNumberOfParmsErr exp_arity
1180   = ptext (sLit "Number of parameters must match family declaration; expected")
1181     <+> ppr exp_arity
1182
1183 -- Ensure that no type family instances occur in a type.
1184 --
1185 checkTyFamFreeness :: Type -> TcM ()
1186 checkTyFamFreeness ty
1187   = checkTc (isTyFamFree ty) $
1188     tyFamInstIllegalErr ty
1189
1190 -- Check that a type does not contain any type family applications.
1191 --
1192 isTyFamFree :: Type -> Bool
1193 isTyFamFree = null . tcTyFamInsts
1194
1195 -- Error messages
1196
1197 tyFamInstIllegalErr :: Type -> SDoc
1198 tyFamInstIllegalErr ty
1199   = hang (ptext (sLit "Illegal type synonym family application in instance") <> 
1200          colon) 2 $
1201       ppr ty
1202
1203 famInstUndecErr :: Type -> SDoc -> SDoc
1204 famInstUndecErr ty msg 
1205   = sep [msg, 
1206          nest 2 (ptext (sLit "in the type family application:") <+> 
1207                  pprType ty)]
1208
1209 famPatErr :: TyCon -> [TyVar] -> [Type] -> SDoc
1210 famPatErr fam_tc tvs pats
1211   = hang (ptext (sLit "Family instance purports to bind type variable") <> plural tvs
1212           <+> pprQuotedList tvs)
1213        2 (hang (ptext (sLit "but the real LHS (expanding synonyms) is:"))
1214              2 (pprTypeApp fam_tc (map expandTypeSynonyms pats) <+> ptext (sLit "= ...")))
1215
1216 nestedMsg, smallerAppMsg :: SDoc
1217 nestedMsg     = ptext (sLit "Nested type family application")
1218 smallerAppMsg = ptext (sLit "Application is no smaller than the instance head")
1219 \end{code}
1220
1221 %************************************************************************
1222 %*                                                                      *
1223 \subsection{Auxiliary functions}
1224 %*                                                                      *
1225 %************************************************************************
1226
1227 \begin{code}
1228 -- Free variables of a type, retaining repetitions, and expanding synonyms
1229 fvType :: Type -> [TyVar]
1230 fvType ty | Just exp_ty <- tcView ty = fvType exp_ty
1231 fvType (TyVarTy tv)        = [tv]
1232 fvType (TyConApp _ tys)    = fvTypes tys
1233 fvType (LitTy {})          = []
1234 fvType (FunTy arg res)     = fvType arg ++ fvType res
1235 fvType (AppTy fun arg)     = fvType fun ++ fvType arg
1236 fvType (ForAllTy tyvar ty) = filter (/= tyvar) (fvType ty)
1237
1238 fvTypes :: [Type] -> [TyVar]
1239 fvTypes tys                = concat (map fvType tys)
1240
1241 sizeType :: Type -> Int
1242 -- Size of a type: the number of variables and constructors
1243 sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty
1244 sizeType (TyVarTy {})      = 1
1245 sizeType (TyConApp _ tys)  = sizeTypes tys + 1
1246 sizeType (LitTy {})        = 1
1247 sizeType (FunTy arg res)   = sizeType arg + sizeType res + 1
1248 sizeType (AppTy fun arg)   = sizeType fun + sizeType arg
1249 sizeType (ForAllTy _ ty)   = sizeType ty
1250
1251 sizeTypes :: [Type] -> Int
1252 -- IA0_NOTE: Avoid kinds.
1253 sizeTypes xs = sum (map sizeType tys)
1254   where tys = filter (not . isKind) xs
1255
1256 -- Size of a predicate
1257 --
1258 -- We are considering whether class constraints terminate.
1259 -- Equality constraints and constraints for the implicit
1260 -- parameter class always termiante so it is safe to say "size 0".
1261 -- (Implicit parameter constraints always terminate because
1262 -- there are no instances for them---they are only solved by
1263 -- "local instances" in expressions).
1264 -- See Trac #4200.
1265 sizePred :: PredType -> Int
1266 sizePred ty = goClass ty
1267   where
1268     goClass p | isIPPred p = 0
1269               | otherwise  = go (classifyPredType p)
1270
1271     go (ClassPred _ tys') = sizeTypes tys'
1272     go (EqPred {})        = 0
1273     go (TuplePred ts)     = sum (map goClass ts)
1274     go (IrredPred ty)     = sizeType ty
1275 \end{code}
1276
1277 Note [Paterson conditions on PredTypes]
1278 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1279 We are considering whether *class* constraints terminate
1280 (see Note [Paterson conditions]). Precisely, the Paterson conditions
1281 would have us check that "the constraint has fewer constructors and variables
1282 (taken together and counting repetitions) than the head.".
1283
1284 However, we can be a bit more refined by looking at which kind of constraint
1285 this actually is. There are two main tricks:
1286
1287  1. It seems like it should be OK not to count the tuple type constructor
1288     for a PredType like (Show a, Eq a) :: Constraint, since we don't
1289     count the "implicit" tuple in the ThetaType itself.
1290
1291     In fact, the Paterson test just checks *each component* of the top level
1292     ThetaType against the size bound, one at a time. By analogy, it should be
1293     OK to return the size of the *largest* tuple component as the size of the
1294     whole tuple.
1295
1296  2. Once we get into an implicit parameter or equality we
1297     can't get back to a class constraint, so it's safe
1298     to say "size 0".  See Trac #4200.
1299
1300 NB: we don't want to detect PredTypes in sizeType (and then call 
1301 sizePred on them), or we might get an infinite loop if that PredType
1302 is irreducible. See Trac #5581.