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