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