Fix #11355.
[ghc.git] / compiler / typecheck / TcValidity.hs
1 {-
2 (c) The University of Glasgow 2006
3 (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 -}
5
6 {-# LANGUAGE CPP, TupleSections, ViewPatterns #-}
7
8 module TcValidity (
9 Rank, UserTypeCtxt(..), checkValidType, checkValidMonoType,
10 ContextKind(..), expectedKindInCtxt,
11 checkValidTheta, checkValidFamPats,
12 checkValidInstance, validDerivPred,
13 checkInstTermination,
14 ClsInfo, checkValidCoAxiom, checkValidCoAxBranch,
15 checkValidTyFamEqn,
16 checkConsistentFamInst,
17 arityErr, badATErr,
18 checkValidTelescope, checkZonkValidTelescope, checkValidInferredKinds
19 ) where
20
21 #include "HsVersions.h"
22
23 -- friends:
24 import TcUnify ( tcSubType_NC )
25 import TcSimplify ( simplifyAmbiguityCheck )
26 import TyCoRep
27 import TcType hiding ( sizeType, sizeTypes )
28 import TcMType
29 import PrelNames
30 import Type
31 import Coercion
32 import Unify( tcMatchTyX )
33 import Kind
34 import CoAxiom
35 import Class
36 import TyCon
37
38 -- others:
39 import HsSyn -- HsType
40 import TcRnMonad -- TcType, amongst others
41 import FunDeps
42 import FamInstEnv ( isDominatedBy, injectiveBranches,
43 InjectivityCheckResult(..) )
44 import FamInst ( makeInjectivityErrors )
45 import Name
46 import VarEnv
47 import VarSet
48 import ErrUtils
49 import DynFlags
50 import Util
51 import ListSetOps
52 import SrcLoc
53 import Outputable
54 import FastString
55 import BasicTypes
56 import Module
57 import qualified GHC.LanguageExtensions as LangExt
58
59 import Control.Monad
60 import Data.Maybe
61 import Data.List ( (\\) )
62
63 {-
64 ************************************************************************
65 * *
66 Checking for ambiguity
67 * *
68 ************************************************************************
69
70 Note [The ambiguity check for type signatures]
71 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
72 checkAmbiguity is a check on *user-supplied type signatures*. It is
73 *purely* there to report functions that cannot possibly be called. So for
74 example we want to reject:
75 f :: C a => Int
76 The idea is there can be no legal calls to 'f' because every call will
77 give rise to an ambiguous constraint. We could soundly omit the
78 ambiguity check on type signatures entirely, at the expense of
79 delaying ambiguity errors to call sites. Indeed, the flag
80 -XAllowAmbiguousTypes switches off the ambiguity check.
81
82 What about things like this:
83 class D a b | a -> b where ..
84 h :: D Int b => Int
85 The Int may well fix 'b' at the call site, so that signature should
86 not be rejected. Moreover, using *visible* fundeps is too
87 conservative. Consider
88 class X a b where ...
89 class D a b | a -> b where ...
90 instance D a b => X [a] b where...
91 h :: X a b => a -> a
92 Here h's type looks ambiguous in 'b', but here's a legal call:
93 ...(h [True])...
94 That gives rise to a (X [Bool] beta) constraint, and using the
95 instance means we need (D Bool beta) and that fixes 'beta' via D's
96 fundep!
97
98 Behind all these special cases there is a simple guiding principle.
99 Consider
100
101 f :: <type>
102 f = ...blah...
103
104 g :: <type>
105 g = f
106
107 You would think that the definition of g would surely typecheck!
108 After all f has exactly the same type, and g=f. But in fact f's type
109 is instantiated and the instantiated constraints are solved against
110 the originals, so in the case an ambiguous type it won't work.
111 Consider our earlier example f :: C a => Int. Then in g's definition,
112 we'll instantiate to (C alpha) and try to deduce (C alpha) from (C a),
113 and fail.
114
115 So in fact we use this as our *definition* of ambiguity. We use a
116 very similar test for *inferred* types, to ensure that they are
117 unambiguous. See Note [Impedence matching] in TcBinds.
118
119 This test is very conveniently implemented by calling
120 tcSubType <type> <type>
121 This neatly takes account of the functional dependecy stuff above,
122 and implicit parameter (see Note [Implicit parameters and ambiguity]).
123 And this is what checkAmbiguity does.
124
125 What about this, though?
126 g :: C [a] => Int
127 Is every call to 'g' ambiguous? After all, we might have
128 intance C [a] where ...
129 at the call site. So maybe that type is ok! Indeed even f's
130 quintessentially ambiguous type might, just possibly be callable:
131 with -XFlexibleInstances we could have
132 instance C a where ...
133 and now a call could be legal after all! Well, we'll reject this
134 unless the instance is available *here*.
135
136 Note [When to call checkAmbiguity]
137 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
138 We call checkAmbiguity
139 (a) on user-specified type signatures
140 (b) in checkValidType
141
142 Conncerning (b), you might wonder about nested foralls. What about
143 f :: forall b. (forall a. Eq a => b) -> b
144 The nested forall is ambiguous. Originally we called checkAmbiguity
145 in the forall case of check_type, but that had two bad consequences:
146 * We got two error messages about (Eq b) in a nested forall like this:
147 g :: forall a. Eq a => forall b. Eq b => a -> a
148 * If we try to check for ambiguity of an nested forall like
149 (forall a. Eq a => b), the implication constraint doesn't bind
150 all the skolems, which results in "No skolem info" in error
151 messages (see Trac #10432).
152
153 To avoid this, we call checkAmbiguity once, at the top, in checkValidType.
154 (I'm still a bit worried about unbound skolems when the type mentions
155 in-scope type variables.)
156
157 In fact, because of the co/contra-variance implemented in tcSubType,
158 this *does* catch function f above. too.
159
160 Concerning (a) the ambiguity check is only used for *user* types, not
161 for types coming from inteface files. The latter can legitimately
162 have ambiguous types. Example
163
164 class S a where s :: a -> (Int,Int)
165 instance S Char where s _ = (1,1)
166 f:: S a => [a] -> Int -> (Int,Int)
167 f (_::[a]) x = (a*x,b)
168 where (a,b) = s (undefined::a)
169
170 Here the worker for f gets the type
171 fw :: forall a. S a => Int -> (# Int, Int #)
172
173
174 Note [Implicit parameters and ambiguity]
175 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
176 Only a *class* predicate can give rise to ambiguity
177 An *implicit parameter* cannot. For example:
178 foo :: (?x :: [a]) => Int
179 foo = length ?x
180 is fine. The call site will supply a particular 'x'
181
182 Furthermore, the type variables fixed by an implicit parameter
183 propagate to the others. E.g.
184 foo :: (Show a, ?x::[a]) => Int
185 foo = show (?x++?x)
186 The type of foo looks ambiguous. But it isn't, because at a call site
187 we might have
188 let ?x = 5::Int in foo
189 and all is well. In effect, implicit parameters are, well, parameters,
190 so we can take their type variables into account as part of the
191 "tau-tvs" stuff. This is done in the function 'FunDeps.grow'.
192 -}
193
194 checkAmbiguity :: UserTypeCtxt -> Type -> TcM ()
195 checkAmbiguity ctxt ty
196 | wantAmbiguityCheck ctxt
197 = do { traceTc "Ambiguity check for" (ppr ty)
198 -- Solve the constraints eagerly because an ambiguous type
199 -- can cause a cascade of further errors. Since the free
200 -- tyvars are skolemised, we can safely use tcSimplifyTop
201 ; allow_ambiguous <- xoptM LangExt.AllowAmbiguousTypes
202 ; (_wrap, wanted) <- addErrCtxt (mk_msg allow_ambiguous) $
203 captureConstraints $
204 tcSubType_NC ctxt ty ty
205 ; simplifyAmbiguityCheck ty wanted
206
207 ; traceTc "Done ambiguity check for" (ppr ty) }
208
209 | otherwise
210 = return ()
211 where
212 mk_msg allow_ambiguous
213 = vcat [ ptext (sLit "In the ambiguity check for") <+> what
214 , ppUnless allow_ambiguous ambig_msg ]
215 ambig_msg = ptext (sLit "To defer the ambiguity check to use sites, enable AllowAmbiguousTypes")
216 what | Just n <- isSigMaybe ctxt = quotes (ppr n)
217 | otherwise = pprUserTypeCtxt ctxt
218
219 wantAmbiguityCheck :: UserTypeCtxt -> Bool
220 wantAmbiguityCheck ctxt
221 = case ctxt of
222 GhciCtxt -> False -- Allow ambiguous types in GHCi's :kind command
223 -- E.g. type family T a :: * -- T :: forall k. k -> *
224 -- Then :k T should work in GHCi, not complain that
225 -- (T k) is ambiguous!
226 _ -> True
227
228
229 checkUserTypeError :: Type -> TcM ()
230 -- Check to see if the type signature mentions "TypeError blah"
231 -- anywhere in it, and fail if so.
232 --
233 -- Very unsatisfactorily (Trac #11144) we need to tidy the type
234 -- because it may have come from an /inferred/ signature, not a
235 -- user-supplied one. This is really only a half-baked fix;
236 -- the other errors in checkValidType don't do tidying, and so
237 -- may give bad error messages when given an inferred type.
238 checkUserTypeError = check
239 where
240 check ty
241 | Just msg <- userTypeError_maybe ty = fail_with msg
242 | Just (_,ts) <- splitTyConApp_maybe ty = mapM_ check ts
243 | Just (t1,t2) <- splitAppTy_maybe ty = check t1 >> check t2
244 | Just (_,t1) <- splitForAllTy_maybe ty = check t1
245 | otherwise = return ()
246
247 fail_with msg = do { env0 <- tcInitTidyEnv
248 ; let (env1, tidy_msg) = tidyOpenType env0 msg
249 ; failWithTcM (env1, pprUserTypeErrorTy tidy_msg) }
250
251
252 {-
253 ************************************************************************
254 * *
255 Checking validity of a user-defined type
256 * *
257 ************************************************************************
258
259 When dealing with a user-written type, we first translate it from an HsType
260 to a Type, performing kind checking, and then check various things that should
261 be true about it. We don't want to perform these checks at the same time
262 as the initial translation because (a) they are unnecessary for interface-file
263 types and (b) when checking a mutually recursive group of type and class decls,
264 we can't "look" at the tycons/classes yet. Also, the checks are rather
265 diverse, and used to really mess up the other code.
266
267 One thing we check for is 'rank'.
268
269 Rank 0: monotypes (no foralls)
270 Rank 1: foralls at the front only, Rank 0 inside
271 Rank 2: foralls at the front, Rank 1 on left of fn arrow,
272
273 basic ::= tyvar | T basic ... basic
274
275 r2 ::= forall tvs. cxt => r2a
276 r2a ::= r1 -> r2a | basic
277 r1 ::= forall tvs. cxt => r0
278 r0 ::= r0 -> r0 | basic
279
280 Another thing is to check that type synonyms are saturated.
281 This might not necessarily show up in kind checking.
282 type A i = i
283 data T k = MkT (k Int)
284 f :: T A -- BAD!
285 -}
286
287 checkValidType :: UserTypeCtxt -> Type -> TcM ()
288 -- Checks that a user-written type is valid for the given context
289 -- Assumes arguemt is fully zonked
290 -- Not used for instance decls; checkValidInstance instead
291 checkValidType ctxt ty
292 = do { traceTc "checkValidType" (ppr ty <+> text "::" <+> ppr (typeKind ty))
293 ; rankn_flag <- xoptM LangExt.RankNTypes
294 ; impred_flag <- xoptM LangExt.ImpredicativeTypes
295 ; let gen_rank :: Rank -> Rank
296 gen_rank r | rankn_flag = ArbitraryRank
297 | otherwise = r
298
299 rank1 = gen_rank r1
300 rank0 = gen_rank r0
301
302 r0 = rankZeroMonoType
303 r1 = LimitedRank True r0
304
305 rank
306 = case ctxt of
307 DefaultDeclCtxt-> MustBeMonoType
308 ResSigCtxt -> MustBeMonoType
309 PatSigCtxt -> rank0
310 RuleSigCtxt _ -> rank1
311 TySynCtxt _ -> rank0
312
313 ExprSigCtxt -> rank1
314 TypeAppCtxt | impred_flag -> ArbitraryRank
315 | otherwise -> tyConArgMonoType
316 -- Normally, ImpredicativeTypes is handled in check_arg_type,
317 -- but visible type applications don't go through there.
318 -- So we do this check here.
319
320 FunSigCtxt {} -> rank1
321 InfSigCtxt _ -> ArbitraryRank -- Inferred type
322 ConArgCtxt _ -> rank1 -- We are given the type of the entire
323 -- constructor, hence rank 1
324
325 ForSigCtxt _ -> rank1
326 SpecInstCtxt -> rank1
327 ThBrackCtxt -> rank1
328 GhciCtxt -> ArbitraryRank
329 _ -> panic "checkValidType"
330 -- Can't happen; not used for *user* sigs
331
332 ; env <- tcInitOpenTidyEnv (tyCoVarsOfType ty)
333
334 -- Check the internal validity of the type itself
335 ; check_type env ctxt rank ty
336
337 -- Check that the thing has kind Type, and is lifted if necessary.
338 -- Do this *after* check_type, because we can't usefully take
339 -- the kind of an ill-formed type such as (a~Int)
340 ; check_kind env ctxt ty
341
342 ; checkUserTypeError ty
343
344 -- Check for ambiguous types. See Note [When to call checkAmbiguity]
345 -- NB: this will happen even for monotypes, but that should be cheap;
346 -- and there may be nested foralls for the subtype test to examine
347 ; checkAmbiguity ctxt ty
348
349 ; traceTc "checkValidType done" (ppr ty <+> text "::" <+> ppr (typeKind ty)) }
350
351 checkValidMonoType :: Type -> TcM ()
352 -- Assumes arguemt is fully zonked
353 checkValidMonoType ty
354 = do { env <- tcInitOpenTidyEnv (tyCoVarsOfType ty)
355 ; check_type env SigmaCtxt MustBeMonoType ty }
356
357 check_kind :: TidyEnv -> UserTypeCtxt -> TcType -> TcM ()
358 -- Check that the type's kind is acceptable for the context
359 check_kind env ctxt ty
360 | TySynCtxt {} <- ctxt
361 , returnsConstraintKind actual_kind
362 = do { ck <- xoptM LangExt.ConstraintKinds
363 ; if ck
364 then when (isConstraintKind actual_kind)
365 (do { dflags <- getDynFlags
366 ; check_pred_ty env dflags ctxt ty })
367 else addErrTcM (constraintSynErr env actual_kind) }
368
369 | otherwise
370 = case expectedKindInCtxt ctxt of
371 TheKind k -> checkTcM (tcEqType actual_kind k) (kindErr env actual_kind)
372 OpenKind -> checkTcM (classifiesTypeWithValues actual_kind) (kindErr env actual_kind)
373 AnythingKind -> return ()
374 where
375 actual_kind = typeKind ty
376
377 -- | The kind expected in a certain context.
378 data ContextKind = TheKind Kind -- ^ a specific kind
379 | AnythingKind -- ^ any kind will do
380 | OpenKind -- ^ something of the form @TYPE _@
381
382 -- Depending on the context, we might accept any kind (for instance, in a TH
383 -- splice), or only certain kinds (like in type signatures).
384 expectedKindInCtxt :: UserTypeCtxt -> ContextKind
385 expectedKindInCtxt (TySynCtxt _) = AnythingKind
386 expectedKindInCtxt ThBrackCtxt = AnythingKind
387 expectedKindInCtxt GhciCtxt = AnythingKind
388 -- The types in a 'default' decl can have varying kinds
389 -- See Note [Extended defaults]" in TcEnv
390 expectedKindInCtxt DefaultDeclCtxt = AnythingKind
391 expectedKindInCtxt TypeAppCtxt = AnythingKind
392 expectedKindInCtxt (ForSigCtxt _) = TheKind liftedTypeKind
393 expectedKindInCtxt InstDeclCtxt = TheKind constraintKind
394 expectedKindInCtxt SpecInstCtxt = TheKind constraintKind
395 expectedKindInCtxt _ = OpenKind
396
397 {-
398 Note [Higher rank types]
399 ~~~~~~~~~~~~~~~~~~~~~~~~
400 Technically
401 Int -> forall a. a->a
402 is still a rank-1 type, but it's not Haskell 98 (Trac #5957). So the
403 validity checker allow a forall after an arrow only if we allow it
404 before -- that is, with Rank2Types or RankNTypes
405 -}
406
407 data Rank = ArbitraryRank -- Any rank ok
408
409 | LimitedRank -- Note [Higher rank types]
410 Bool -- Forall ok at top
411 Rank -- Use for function arguments
412
413 | MonoType SDoc -- Monotype, with a suggestion of how it could be a polytype
414
415 | MustBeMonoType -- Monotype regardless of flags
416
417 rankZeroMonoType, tyConArgMonoType, synArgMonoType :: Rank
418 rankZeroMonoType = MonoType (ptext (sLit "Perhaps you intended to use RankNTypes or Rank2Types"))
419 tyConArgMonoType = MonoType (ptext (sLit "GHC doesn't yet support impredicative polymorphism"))
420 synArgMonoType = MonoType (ptext (sLit "Perhaps you intended to use LiberalTypeSynonyms"))
421
422 funArgResRank :: Rank -> (Rank, Rank) -- Function argument and result
423 funArgResRank (LimitedRank _ arg_rank) = (arg_rank, LimitedRank (forAllAllowed arg_rank) arg_rank)
424 funArgResRank other_rank = (other_rank, other_rank)
425
426 forAllAllowed :: Rank -> Bool
427 forAllAllowed ArbitraryRank = True
428 forAllAllowed (LimitedRank forall_ok _) = forall_ok
429 forAllAllowed _ = False
430
431 ----------------------------------------
432 -- | Fail with error message if the type is unlifted
433 check_lifted :: TidyEnv -> Type -> TcM ()
434 check_lifted env ty
435 = checkTcM (not (isUnLiftedType ty)) (unliftedArgErr env ty)
436
437 check_type :: TidyEnv -> UserTypeCtxt -> Rank -> Type -> TcM ()
438 -- The args say what the *type context* requires, independent
439 -- of *flag* settings. You test the flag settings at usage sites.
440 --
441 -- Rank is allowed rank for function args
442 -- Rank 0 means no for-alls anywhere
443
444 check_type env ctxt rank ty
445 | not (null tvs && null theta)
446 = do { checkTcM (forAllAllowed rank) (forAllTyErr env' rank ty)
447 -- Reject e.g. (Maybe (?x::Int => Int)),
448 -- with a decent error message
449
450 ; check_valid_theta env' SigmaCtxt theta
451 -- Allow type T = ?x::Int => Int -> Int
452 -- but not type T = ?x::Int
453
454 ; check_type env' ctxt rank tau -- Allow foralls to right of arrow
455 ; checkTcM (not (any (`elemVarSet` tyCoVarsOfType tau_kind) tvs))
456 (forAllEscapeErr env' ty tau_kind)
457 }
458 where
459 (tvs, theta, tau) = tcSplitSigmaTy ty
460 tau_kind = typeKind tau
461 (env', _) = tidyTyCoVarBndrs env tvs
462
463 check_type _ _ _ (TyVarTy _) = return ()
464
465 check_type env ctxt rank (ForAllTy (Anon arg_ty) res_ty)
466 = do { check_type env ctxt arg_rank arg_ty
467 ; check_type env ctxt res_rank res_ty }
468 where
469 (arg_rank, res_rank) = funArgResRank rank
470
471 check_type env ctxt rank (AppTy ty1 ty2)
472 = do { check_arg_type env ctxt rank ty1
473 ; check_arg_type env ctxt rank ty2 }
474
475 check_type env ctxt rank ty@(TyConApp tc tys)
476 | isTypeSynonymTyCon tc || isTypeFamilyTyCon tc
477 = check_syn_tc_app env ctxt rank ty tc tys
478 | isUnboxedTupleTyCon tc = check_ubx_tuple env ctxt ty tys
479 | otherwise = mapM_ (check_arg_type env ctxt rank) tys
480
481 check_type _ _ _ (LitTy {}) = return ()
482
483 check_type env ctxt rank (CastTy ty _) = check_type env ctxt rank ty
484
485 check_type _ _ _ ty = pprPanic "check_type" (ppr ty)
486
487 ----------------------------------------
488 check_syn_tc_app :: TidyEnv -> UserTypeCtxt -> Rank -> KindOrType
489 -> TyCon -> [KindOrType] -> TcM ()
490 -- Used for type synonyms and type synonym families,
491 -- which must be saturated,
492 -- but not data families, which need not be saturated
493 check_syn_tc_app env ctxt rank ty tc tys
494 | tc_arity <= length tys -- Saturated
495 -- Check that the synonym has enough args
496 -- This applies equally to open and closed synonyms
497 -- It's OK to have an *over-applied* type synonym
498 -- data Tree a b = ...
499 -- type Foo a = Tree [a]
500 -- f :: Foo a b -> ...
501 = do { -- See Note [Liberal type synonyms]
502 ; liberal <- xoptM LangExt.LiberalTypeSynonyms
503 ; if not liberal || isTypeFamilyTyCon tc then
504 -- For H98 and synonym families, do check the type args
505 mapM_ check_arg tys
506
507 else -- In the liberal case (only for closed syns), expand then check
508 case coreView ty of
509 Just ty' -> check_type env ctxt rank ty'
510 Nothing -> pprPanic "check_tau_type" (ppr ty) }
511
512 | GhciCtxt <- ctxt -- Accept under-saturated type synonyms in
513 -- GHCi :kind commands; see Trac #7586
514 = mapM_ check_arg tys
515
516 | otherwise
517 = failWithTc (tyConArityErr tc tys)
518 where
519 tc_arity = tyConArity tc
520 check_arg | isTypeFamilyTyCon tc = check_arg_type env ctxt rank
521 | otherwise = check_type env ctxt synArgMonoType
522
523 ----------------------------------------
524 check_ubx_tuple :: TidyEnv -> UserTypeCtxt -> KindOrType
525 -> [KindOrType] -> TcM ()
526 check_ubx_tuple env ctxt ty tys
527 = do { ub_tuples_allowed <- xoptM LangExt.UnboxedTuples
528 ; checkTcM ub_tuples_allowed (ubxArgTyErr env ty)
529
530 ; impred <- xoptM LangExt.ImpredicativeTypes
531 ; let rank' = if impred then ArbitraryRank else tyConArgMonoType
532 -- c.f. check_arg_type
533 -- However, args are allowed to be unlifted, or
534 -- more unboxed tuples, so can't use check_arg_ty
535 ; mapM_ (check_type env ctxt rank') tys }
536
537 ----------------------------------------
538 check_arg_type :: TidyEnv -> UserTypeCtxt -> Rank -> KindOrType -> TcM ()
539 -- The sort of type that can instantiate a type variable,
540 -- or be the argument of a type constructor.
541 -- Not an unboxed tuple, but now *can* be a forall (since impredicativity)
542 -- Other unboxed types are very occasionally allowed as type
543 -- arguments depending on the kind of the type constructor
544 --
545 -- For example, we want to reject things like:
546 --
547 -- instance Ord a => Ord (forall s. T s a)
548 -- and
549 -- g :: T s (forall b.b)
550 --
551 -- NB: unboxed tuples can have polymorphic or unboxed args.
552 -- This happens in the workers for functions returning
553 -- product types with polymorphic components.
554 -- But not in user code.
555 -- Anyway, they are dealt with by a special case in check_tau_type
556
557 check_arg_type _ _ _ (CoercionTy {}) = return ()
558
559 check_arg_type env ctxt rank ty
560 = do { impred <- xoptM LangExt.ImpredicativeTypes
561 ; let rank' = case rank of -- Predictive => must be monotype
562 MustBeMonoType -> MustBeMonoType -- Monotype, regardless
563 _other | impred -> ArbitraryRank
564 | otherwise -> tyConArgMonoType
565 -- Make sure that MustBeMonoType is propagated,
566 -- so that we don't suggest -XImpredicativeTypes in
567 -- (Ord (forall a.a)) => a -> a
568 -- and so that if it Must be a monotype, we check that it is!
569
570 ; check_type env ctxt rank' ty
571 ; check_lifted env ty }
572 -- NB the isUnLiftedType test also checks for
573 -- T State#
574 -- where there is an illegal partial application of State# (which has
575 -- kind * -> #); see Note [The kind invariant] in TyCoRep
576
577 ----------------------------------------
578 forAllTyErr :: TidyEnv -> Rank -> Type -> (TidyEnv, SDoc)
579 forAllTyErr env rank ty
580 = ( env
581 , vcat [ hang (ptext (sLit "Illegal polymorphic or qualified type:")) 2 (ppr_tidy env ty)
582 , suggestion ] )
583 where
584 suggestion = case rank of
585 LimitedRank {} -> ptext (sLit "Perhaps you intended to use RankNTypes or Rank2Types")
586 MonoType d -> d
587 _ -> Outputable.empty -- Polytype is always illegal
588
589 forAllEscapeErr :: TidyEnv -> Type -> Kind -> (TidyEnv, SDoc)
590 forAllEscapeErr env ty tau_kind
591 = ( env
592 , hang (vcat [ text "Quantified type's kind mentions quantified type variable"
593 , text "(skolem escape)" ])
594 2 (vcat [ text " type:" <+> ppr_tidy env ty
595 , text "of kind:" <+> ppr_tidy env tau_kind ]) )
596
597 unliftedArgErr, ubxArgTyErr :: TidyEnv -> Type -> (TidyEnv, SDoc)
598 unliftedArgErr env ty = (env, sep [ptext (sLit "Illegal unlifted type:"), ppr_tidy env ty])
599 ubxArgTyErr env ty = (env, sep [ptext (sLit "Illegal unboxed tuple type as function argument:"), ppr_tidy env ty])
600
601 kindErr :: TidyEnv -> Kind -> (TidyEnv, SDoc)
602 kindErr env kind = (env, sep [ptext (sLit "Expecting an ordinary type, but found a type of kind"), ppr_tidy env kind])
603
604 {-
605 Note [Liberal type synonyms]
606 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
607 If -XLiberalTypeSynonyms is on, expand closed type synonyms *before*
608 doing validity checking. This allows us to instantiate a synonym defn
609 with a for-all type, or with a partially-applied type synonym.
610 e.g. type T a b = a
611 type S m = m ()
612 f :: S (T Int)
613 Here, T is partially applied, so it's illegal in H98. But if you
614 expand S first, then T we get just
615 f :: Int
616 which is fine.
617
618 IMPORTANT: suppose T is a type synonym. Then we must do validity
619 checking on an appliation (T ty1 ty2)
620
621 *either* before expansion (i.e. check ty1, ty2)
622 *or* after expansion (i.e. expand T ty1 ty2, and then check)
623 BUT NOT BOTH
624
625 If we do both, we get exponential behaviour!!
626
627 data TIACons1 i r c = c i ::: r c
628 type TIACons2 t x = TIACons1 t (TIACons1 t x)
629 type TIACons3 t x = TIACons2 t (TIACons1 t x)
630 type TIACons4 t x = TIACons2 t (TIACons2 t x)
631 type TIACons7 t x = TIACons4 t (TIACons3 t x)
632
633
634 ************************************************************************
635 * *
636 \subsection{Checking a theta or source type}
637 * *
638 ************************************************************************
639
640 Note [Implicit parameters in instance decls]
641 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
642 Implicit parameters _only_ allowed in type signatures; not in instance
643 decls, superclasses etc. The reason for not allowing implicit params in
644 instances is a bit subtle. If we allowed
645 instance (?x::Int, Eq a) => Foo [a] where ...
646 then when we saw
647 (e :: (?x::Int) => t)
648 it would be unclear how to discharge all the potential uses of the ?x
649 in e. For example, a constraint Foo [Int] might come out of e, and
650 applying the instance decl would show up two uses of ?x. Trac #8912.
651 -}
652
653 checkValidTheta :: UserTypeCtxt -> ThetaType -> TcM ()
654 -- Assumes arguemt is fully zonked
655 checkValidTheta ctxt theta
656 = do { env <- tcInitOpenTidyEnv (tyCoVarsOfTypes theta)
657 ; addErrCtxtM (checkThetaCtxt ctxt theta) $
658 check_valid_theta env ctxt theta }
659
660 -------------------------
661 check_valid_theta :: TidyEnv -> UserTypeCtxt -> [PredType] -> TcM ()
662 check_valid_theta _ _ []
663 = return ()
664 check_valid_theta env ctxt theta
665 = do { dflags <- getDynFlags
666 ; warnTcM (wopt Opt_WarnDuplicateConstraints dflags &&
667 notNull dups) (dupPredWarn env dups)
668 ; traceTc "check_valid_theta" (ppr theta)
669 ; mapM_ (check_pred_ty env dflags ctxt) theta }
670 where
671 (_,dups) = removeDups cmpType theta
672
673 -------------------------
674 check_pred_ty :: TidyEnv -> DynFlags -> UserTypeCtxt -> PredType -> TcM ()
675 -- Check the validity of a predicate in a signature
676 -- Do not look through any type synonyms; any constraint kinded
677 -- type synonyms have been checked at their definition site
678 -- C.f. Trac #9838
679
680 check_pred_ty env dflags ctxt pred
681 = do { check_type env SigmaCtxt MustBeMonoType pred
682 ; check_pred_help False env dflags ctxt pred }
683
684 check_pred_help :: Bool -- True <=> under a type synonym
685 -> TidyEnv
686 -> DynFlags -> UserTypeCtxt
687 -> PredType -> TcM ()
688 check_pred_help under_syn env dflags ctxt pred
689 | Just pred' <- coreView pred -- Switch on under_syn when going under a
690 -- synonym (Trac #9838, yuk)
691 = check_pred_help True env dflags ctxt pred'
692 | otherwise
693 = case splitTyConApp_maybe pred of
694 Just (tc, tys)
695 | isTupleTyCon tc
696 -> check_tuple_pred under_syn env dflags ctxt pred tys
697 -- NB: this equality check must come first, because (~) is a class,
698 -- too.
699 | tc `hasKey` heqTyConKey ||
700 tc `hasKey` eqTyConKey ||
701 tc `hasKey` eqPrimTyConKey
702 -> check_eq_pred env dflags pred tc tys
703 | Just cls <- tyConClass_maybe tc
704 -> check_class_pred env dflags ctxt pred cls tys -- Includes Coercible
705 _ -> check_irred_pred under_syn env dflags ctxt pred
706
707 check_eq_pred :: TidyEnv -> DynFlags -> PredType -> TyCon -> [TcType] -> TcM ()
708 check_eq_pred env dflags pred tc tys
709 = -- Equational constraints are valid in all contexts if type
710 -- families are permitted
711 do { checkTc (length tys == tyConArity tc) (tyConArityErr tc tys)
712 ; checkTcM (xopt LangExt.TypeFamilies dflags
713 || xopt LangExt.GADTs dflags)
714 (eqPredTyErr env pred) }
715
716 check_tuple_pred :: Bool -> TidyEnv -> DynFlags -> UserTypeCtxt -> PredType -> [PredType] -> TcM ()
717 check_tuple_pred under_syn env dflags ctxt pred ts
718 = do { -- See Note [ConstraintKinds in predicates]
719 checkTcM (under_syn || xopt LangExt.ConstraintKinds dflags)
720 (predTupleErr env pred)
721 ; mapM_ (check_pred_help under_syn env dflags ctxt) ts }
722 -- This case will not normally be executed because without
723 -- -XConstraintKinds tuple types are only kind-checked as *
724
725 check_irred_pred :: Bool -> TidyEnv -> DynFlags -> UserTypeCtxt -> PredType -> TcM ()
726 check_irred_pred under_syn env dflags ctxt pred
727 -- The predicate looks like (X t1 t2) or (x t1 t2) :: Constraint
728 -- where X is a type function
729 = do { -- If it looks like (x t1 t2), require ConstraintKinds
730 -- see Note [ConstraintKinds in predicates]
731 -- But (X t1 t2) is always ok because we just require ConstraintKinds
732 -- at the definition site (Trac #9838)
733 failIfTcM (not under_syn && not (xopt LangExt.ConstraintKinds dflags)
734 && hasTyVarHead pred)
735 (predIrredErr env pred)
736
737 -- Make sure it is OK to have an irred pred in this context
738 -- See Note [Irreducible predicates in superclasses]
739 ; failIfTcM (is_superclass ctxt
740 && not (xopt LangExt.UndecidableInstances dflags)
741 && has_tyfun_head pred)
742 (predSuperClassErr env pred) }
743 where
744 is_superclass ctxt = case ctxt of { ClassSCCtxt _ -> True; _ -> False }
745 has_tyfun_head ty
746 = case tcSplitTyConApp_maybe ty of
747 Just (tc, _) -> isTypeFamilyTyCon tc
748 Nothing -> False
749
750 {- Note [ConstraintKinds in predicates]
751 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
752 Don't check for -XConstraintKinds under a type synonym, because that
753 was done at the type synonym definition site; see Trac #9838
754 e.g. module A where
755 type C a = (Eq a, Ix a) -- Needs -XConstraintKinds
756 module B where
757 import A
758 f :: C a => a -> a -- Does *not* need -XConstraintKinds
759
760 Note [Irreducible predicates in superclasses]
761 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
762 Allowing type-family calls in class superclasses is somewhat dangerous
763 because we can write:
764
765 type family Fooish x :: * -> Constraint
766 type instance Fooish () = Foo
767 class Fooish () a => Foo a where
768
769 This will cause the constraint simplifier to loop because every time we canonicalise a
770 (Foo a) class constraint we add a (Fooish () a) constraint which will be immediately
771 solved to add+canonicalise another (Foo a) constraint. -}
772
773 -------------------------
774 check_class_pred :: TidyEnv -> DynFlags -> UserTypeCtxt -> PredType -> Class -> [TcType] -> TcM ()
775 check_class_pred env dflags ctxt pred cls tys
776 | isIPClass cls
777 = do { check_arity
778 ; checkTcM (okIPCtxt ctxt) (badIPPred env pred) }
779
780 | otherwise
781 = do { check_arity
782 ; checkTcM arg_tys_ok (env, predTyVarErr (tidyType env pred)) }
783 where
784 check_arity = checkTc (classArity cls == length tys)
785 (tyConArityErr (classTyCon cls) tys)
786 flexible_contexts = xopt LangExt.FlexibleContexts dflags
787 undecidable_ok = xopt LangExt.UndecidableInstances dflags
788
789 arg_tys_ok = case ctxt of
790 SpecInstCtxt -> True -- {-# SPECIALISE instance Eq (T Int) #-} is fine
791 InstDeclCtxt -> checkValidClsArgs (flexible_contexts || undecidable_ok) cls tys
792 -- Further checks on head and theta
793 -- in checkInstTermination
794 _ -> checkValidClsArgs flexible_contexts cls tys
795
796 -------------------------
797 okIPCtxt :: UserTypeCtxt -> Bool
798 -- See Note [Implicit parameters in instance decls]
799 okIPCtxt (FunSigCtxt {}) = True
800 okIPCtxt (InfSigCtxt {}) = True
801 okIPCtxt ExprSigCtxt = True
802 okIPCtxt TypeAppCtxt = True
803 okIPCtxt PatSigCtxt = True
804 okIPCtxt ResSigCtxt = True
805 okIPCtxt GenSigCtxt = True
806 okIPCtxt (ConArgCtxt {}) = True
807 okIPCtxt (ForSigCtxt {}) = True -- ??
808 okIPCtxt ThBrackCtxt = True
809 okIPCtxt GhciCtxt = True
810 okIPCtxt SigmaCtxt = True
811 okIPCtxt (DataTyCtxt {}) = True
812 okIPCtxt (PatSynCtxt {}) = True
813
814 okIPCtxt (ClassSCCtxt {}) = False
815 okIPCtxt (InstDeclCtxt {}) = False
816 okIPCtxt (SpecInstCtxt {}) = False
817 okIPCtxt (TySynCtxt {}) = False
818 okIPCtxt (RuleSigCtxt {}) = False
819 okIPCtxt DefaultDeclCtxt = False
820
821 badIPPred :: TidyEnv -> PredType -> (TidyEnv, SDoc)
822 badIPPred env pred
823 = ( env
824 , ptext (sLit "Illegal implicit parameter") <+> quotes (ppr_tidy env pred) )
825
826 {-
827 Note [Kind polymorphic type classes]
828 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
829 MultiParam check:
830
831 class C f where... -- C :: forall k. k -> Constraint
832 instance C Maybe where...
833
834 The dictionary gets type [C * Maybe] even if it's not a MultiParam
835 type class.
836
837 Flexibility check:
838
839 class C f where... -- C :: forall k. k -> Constraint
840 data D a = D a
841 instance C D where
842
843 The dictionary gets type [C * (D *)]. IA0_TODO it should be
844 generalized actually.
845 -}
846
847 checkThetaCtxt :: UserTypeCtxt -> ThetaType -> TidyEnv -> TcM (TidyEnv, SDoc)
848 checkThetaCtxt ctxt theta env
849 = return ( env
850 , vcat [ ptext (sLit "In the context:") <+> pprTheta (tidyTypes env theta)
851 , ptext (sLit "While checking") <+> pprUserTypeCtxt ctxt ] )
852
853 eqPredTyErr, predTupleErr, predIrredErr, predSuperClassErr :: TidyEnv -> PredType -> (TidyEnv, SDoc)
854 eqPredTyErr env pred
855 = ( env
856 , ptext (sLit "Illegal equational constraint") <+> ppr_tidy env pred $$
857 parens (ptext (sLit "Use GADTs or TypeFamilies to permit this")) )
858 predTupleErr env pred
859 = ( env
860 , hang (ptext (sLit "Illegal tuple constraint:") <+> ppr_tidy env pred)
861 2 (parens constraintKindsMsg) )
862 predIrredErr env pred
863 = ( env
864 , hang (ptext (sLit "Illegal constraint:") <+> ppr_tidy env pred)
865 2 (parens constraintKindsMsg) )
866 predSuperClassErr env pred
867 = ( env
868 , hang (ptext (sLit "Illegal constraint") <+> quotes (ppr_tidy env pred)
869 <+> ptext (sLit "in a superclass context"))
870 2 (parens undecidableMsg) )
871
872 predTyVarErr :: PredType -> SDoc -- type is already tidied!
873 predTyVarErr pred
874 = vcat [ hang (ptext (sLit "Non type-variable argument"))
875 2 (ptext (sLit "in the constraint:") <+> ppr pred)
876 , parens (ptext (sLit "Use FlexibleContexts to permit this")) ]
877
878 constraintSynErr :: TidyEnv -> Type -> (TidyEnv, SDoc)
879 constraintSynErr env kind
880 = ( env
881 , hang (ptext (sLit "Illegal constraint synonym of kind:") <+> quotes (ppr_tidy env kind))
882 2 (parens constraintKindsMsg) )
883
884 dupPredWarn :: TidyEnv -> [[PredType]] -> (TidyEnv, SDoc)
885 dupPredWarn env dups
886 = ( env
887 , text "Duplicate constraint" <> plural primaryDups <> text ":"
888 <+> pprWithCommas (ppr_tidy env) primaryDups )
889 where
890 primaryDups = map head dups
891
892 tyConArityErr :: TyCon -> [TcType] -> SDoc
893 -- For type-constructor arity errors, be careful to report
894 -- the number of /visible/ arguments required and supplied,
895 -- ignoring the /invisible/ arguments, which the user does not see.
896 -- (e.g. Trac #10516)
897 tyConArityErr tc tks
898 = arityErr (tyConFlavour tc) (tyConName tc)
899 tc_type_arity tc_type_args
900 where
901 vis_tks = filterOutInvisibleTypes tc tks
902
903 -- tc_type_arity = number of *type* args expected
904 -- tc_type_args = number of *type* args encountered
905 tc_type_arity = count isVisibleBinder $ fst $ splitPiTys (tyConKind tc)
906 tc_type_args = length vis_tks
907
908 arityErr :: Outputable a => String -> a -> Int -> Int -> SDoc
909 arityErr what name n m
910 = hsep [ ptext (sLit "The") <+> text what, quotes (ppr name), ptext (sLit "should have"),
911 n_arguments <> comma, text "but has been given",
912 if m==0 then text "none" else int m]
913 where
914 n_arguments | n == 0 = ptext (sLit "no arguments")
915 | n == 1 = ptext (sLit "1 argument")
916 | True = hsep [int n, ptext (sLit "arguments")]
917
918 {-
919 ************************************************************************
920 * *
921 \subsection{Checking for a decent instance head type}
922 * *
923 ************************************************************************
924
925 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
926 it must normally look like: @instance Foo (Tycon a b c ...) ...@
927
928 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
929 flag is on, or (2)~the instance is imported (they must have been
930 compiled elsewhere). In these cases, we let them go through anyway.
931
932 We can also have instances for functions: @instance Foo (a -> b) ...@.
933 -}
934
935 checkValidInstHead :: UserTypeCtxt -> Class -> [Type] -> TcM ()
936 checkValidInstHead ctxt clas cls_args
937 = do { dflags <- getDynFlags
938
939 ; mod <- getModule
940 ; checkTc (getUnique clas `notElem` abstractClassKeys ||
941 nameModule (getName clas) == mod)
942 (instTypeErr clas cls_args abstract_class_msg)
943
944 -- Check language restrictions;
945 -- but not for SPECIALISE isntance pragmas
946 ; let ty_args = filterOutInvisibleTypes (classTyCon clas) cls_args
947 ; unless spec_inst_prag $
948 do { checkTc (xopt LangExt.TypeSynonymInstances dflags ||
949 all tcInstHeadTyNotSynonym ty_args)
950 (instTypeErr clas cls_args head_type_synonym_msg)
951 ; checkTc (xopt LangExt.FlexibleInstances dflags ||
952 all tcInstHeadTyAppAllTyVars ty_args)
953 (instTypeErr clas cls_args head_type_args_tyvars_msg)
954 ; checkTc (xopt LangExt.MultiParamTypeClasses dflags ||
955 length ty_args == 1 || -- Only count type arguments
956 (xopt LangExt.NullaryTypeClasses dflags &&
957 null ty_args))
958 (instTypeErr clas cls_args head_one_type_msg) }
959
960 -- May not contain type family applications
961 ; mapM_ checkTyFamFreeness ty_args
962
963 ; mapM_ checkValidMonoType ty_args
964 -- For now, I only allow tau-types (not polytypes) in
965 -- the head of an instance decl.
966 -- E.g. instance C (forall a. a->a) is rejected
967 -- One could imagine generalising that, but I'm not sure
968 -- what all the consequences might be
969
970 -- We can't have unlifted type arguments.
971 -- check_arg_type is redundant with checkValidMonoType
972 ; env <- tcInitOpenTidyEnv (tyCoVarsOfTypes ty_args)
973 ; mapM_ (check_lifted env) ty_args
974 }
975
976 where
977 spec_inst_prag = case ctxt of { SpecInstCtxt -> True; _ -> False }
978
979 head_type_synonym_msg = parens (
980 text "All instance types must be of the form (T t1 ... tn)" $$
981 text "where T is not a synonym." $$
982 text "Use TypeSynonymInstances if you want to disable this.")
983
984 head_type_args_tyvars_msg = parens (vcat [
985 text "All instance types must be of the form (T a1 ... an)",
986 text "where a1 ... an are *distinct type variables*,",
987 text "and each type variable appears at most once in the instance head.",
988 text "Use FlexibleInstances if you want to disable this."])
989
990 head_one_type_msg = parens (
991 text "Only one type can be given in an instance head." $$
992 text "Use MultiParamTypeClasses if you want to allow more, or zero.")
993
994 abstract_class_msg =
995 text "Manual instances of this class are not permitted."
996
997 abstractClassKeys :: [Unique]
998 abstractClassKeys = [ heqTyConKey
999 , eqTyConKey
1000 , coercibleTyConKey
1001 ] -- See Note [Equality class instances]
1002
1003 instTypeErr :: Class -> [Type] -> SDoc -> SDoc
1004 instTypeErr cls tys msg
1005 = hang (hang (ptext (sLit "Illegal instance declaration for"))
1006 2 (quotes (pprClassPred cls tys)))
1007 2 msg
1008
1009 {- Note [Valid 'deriving' predicate]
1010 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1011 validDerivPred checks for OK 'deriving' context. See Note [Exotic
1012 derived instance contexts] in TcDeriv. However the predicate is
1013 here because it uses sizeTypes, fvTypes.
1014
1015 It checks for three things
1016
1017 * No repeated variables (hasNoDups fvs)
1018
1019 * No type constructors. This is done by comparing
1020 sizeTypes tys == length (fvTypes tys)
1021 sizeTypes counts variables and constructors; fvTypes returns variables.
1022 So if they are the same, there must be no constructors. But there
1023 might be applications thus (f (g x)).
1024
1025 * Also check for a bizarre corner case, when the derived instance decl
1026 would look like
1027 instance C a b => D (T a) where ...
1028 Note that 'b' isn't a parameter of T. This gives rise to all sorts of
1029 problems; in particular, it's hard to compare solutions for equality
1030 when finding the fixpoint, and that means the inferContext loop does
1031 not converge. See Trac #5287.
1032
1033 Note [Equality class instances]
1034 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1035 We can't have users writing instances for the equality classes. But we
1036 still need to be able to write instances for them ourselves. So we allow
1037 instances only in the defining module.
1038
1039 -}
1040
1041 validDerivPred :: TyVarSet -> PredType -> Bool
1042 -- See Note [Valid 'deriving' predicate]
1043 validDerivPred tv_set pred
1044 = case classifyPredType pred of
1045 ClassPred cls _ -> cls `hasKey` typeableClassKey
1046 -- Typeable constraints are bigger than they appear due
1047 -- to kind polymorphism, but that's OK
1048 || check_tys
1049 EqPred {} -> False -- reject equality constraints
1050 _ -> True -- Non-class predicates are ok
1051 where
1052 check_tys = hasNoDups fvs
1053 -- use sizePred to ignore implicit args
1054 && sizePred pred == fromIntegral (length fvs)
1055 && all (`elemVarSet` tv_set) fvs
1056
1057 fvs = fvType pred
1058
1059 {-
1060 ************************************************************************
1061 * *
1062 \subsection{Checking instance for termination}
1063 * *
1064 ************************************************************************
1065 -}
1066
1067 checkValidInstance :: UserTypeCtxt -> LHsSigType Name -> Type
1068 -> TcM ([TyVar], ThetaType, Class, [Type])
1069 checkValidInstance ctxt hs_type ty
1070 | Just (clas,inst_tys) <- getClassPredTys_maybe tau
1071 , inst_tys `lengthIs` classArity clas
1072 = do { setSrcSpan head_loc (checkValidInstHead ctxt clas inst_tys)
1073 ; checkValidTheta ctxt theta
1074
1075 -- The Termination and Coverate Conditions
1076 -- Check that instance inference will terminate (if we care)
1077 -- For Haskell 98 this will already have been done by checkValidTheta,
1078 -- but as we may be using other extensions we need to check.
1079 --
1080 -- Note that the Termination Condition is *more conservative* than
1081 -- the checkAmbiguity test we do on other type signatures
1082 -- e.g. Bar a => Bar Int is ambiguous, but it also fails
1083 -- the termination condition, because 'a' appears more often
1084 -- in the constraint than in the head
1085 ; undecidable_ok <- xoptM LangExt.UndecidableInstances
1086 ; traceTc "cvi" (ppr undecidable_ok $$ ppr ty)
1087 ; if undecidable_ok
1088 then checkAmbiguity ctxt ty
1089 else checkInstTermination inst_tys theta
1090
1091 ; case (checkInstCoverage undecidable_ok clas theta inst_tys) of
1092 IsValid -> return () -- Check succeeded
1093 NotValid msg -> addErrTc (instTypeErr clas inst_tys msg)
1094
1095 ; return (tvs, theta, clas, inst_tys) }
1096
1097 | otherwise
1098 = failWithTc (ptext (sLit "Malformed instance head:") <+> ppr tau)
1099 where
1100 (tvs, theta, tau) = tcSplitSigmaTy ty
1101
1102 -- The location of the "head" of the instance
1103 head_loc = case splitLHsInstDeclTy hs_type of
1104 (_, _, L loc _) -> loc
1105
1106 {-
1107 Note [Paterson conditions]
1108 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1109 Termination test: the so-called "Paterson conditions" (see Section 5 of
1110 "Understanding functional dependencies via Constraint Handling Rules,
1111 JFP Jan 2007).
1112
1113 We check that each assertion in the context satisfies:
1114 (1) no variable has more occurrences in the assertion than in the head, and
1115 (2) the assertion has fewer constructors and variables (taken together
1116 and counting repetitions) than the head.
1117 This is only needed with -fglasgow-exts, as Haskell 98 restrictions
1118 (which have already been checked) guarantee termination.
1119
1120 The underlying idea is that
1121
1122 for any ground substitution, each assertion in the
1123 context has fewer type constructors than the head.
1124 -}
1125
1126 checkInstTermination :: [TcType] -> ThetaType -> TcM ()
1127 -- See Note [Paterson conditions]
1128 checkInstTermination tys theta
1129 = check_preds theta
1130 where
1131 head_fvs = fvTypes tys
1132 head_size = sizeTypes tys
1133
1134 check_preds :: [PredType] -> TcM ()
1135 check_preds preds = mapM_ check preds
1136
1137 check :: PredType -> TcM ()
1138 check pred
1139 = case classifyPredType pred of
1140 EqPred {} -> return () -- See Trac #4200.
1141 IrredPred {} -> check2 pred (sizeType pred)
1142 ClassPred cls tys
1143 | isTerminatingClass cls
1144 -> return ()
1145
1146 | isCTupleClass cls -- Look inside tuple predicates; Trac #8359
1147 -> check_preds tys
1148
1149 | otherwise
1150 -> check2 pred (sizeTypes $ filterOutInvisibleTypes (classTyCon cls) tys)
1151 -- Other ClassPreds
1152
1153 check2 pred pred_size
1154 | not (null bad_tvs) = addErrTc (noMoreMsg bad_tvs what)
1155 | pred_size >= head_size = addErrTc (smallerMsg what)
1156 | otherwise = return ()
1157 where
1158 what = ptext (sLit "constraint") <+> quotes (ppr pred)
1159 bad_tvs = fvType pred \\ head_fvs
1160
1161 smallerMsg :: SDoc -> SDoc
1162 smallerMsg what
1163 = vcat [ hang (ptext (sLit "The") <+> what)
1164 2 (ptext (sLit "is no smaller than the instance head"))
1165 , parens undecidableMsg ]
1166
1167 noMoreMsg :: [TcTyVar] -> SDoc -> SDoc
1168 noMoreMsg tvs what
1169 = vcat [ hang (ptext (sLit "Variable") <> plural tvs <+> quotes (pprWithCommas ppr tvs)
1170 <+> occurs <+> ptext (sLit "more often"))
1171 2 (sep [ ptext (sLit "in the") <+> what
1172 , ptext (sLit "than in the instance head") ])
1173 , parens undecidableMsg ]
1174 where
1175 occurs = if isSingleton tvs then ptext (sLit "occurs")
1176 else ptext (sLit "occur")
1177
1178 undecidableMsg, constraintKindsMsg :: SDoc
1179 undecidableMsg = ptext (sLit "Use UndecidableInstances to permit this")
1180 constraintKindsMsg = ptext (sLit "Use ConstraintKinds to permit this")
1181
1182 {-
1183 Note [Associated type instances]
1184 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1185 We allow this:
1186 class C a where
1187 type T x a
1188 instance C Int where
1189 type T (S y) Int = y
1190 type T Z Int = Char
1191
1192 Note that
1193 a) The variable 'x' is not bound by the class decl
1194 b) 'x' is instantiated to a non-type-variable in the instance
1195 c) There are several type instance decls for T in the instance
1196
1197 All this is fine. Of course, you can't give any *more* instances
1198 for (T ty Int) elsewhere, because it's an *associated* type.
1199
1200 Note [Checking consistent instantiation]
1201 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1202 class C a b where
1203 type T a x b
1204
1205 instance C [p] Int
1206 type T [p] y Int = (p,y,y) -- Induces the family instance TyCon
1207 -- type TR p y = (p,y,y)
1208
1209 So we
1210 * Form the mini-envt from the class type variables a,b
1211 to the instance decl types [p],Int: [a->[p], b->Int]
1212
1213 * Look at the tyvars a,x,b of the type family constructor T
1214 (it shares tyvars with the class C)
1215
1216 * Apply the mini-evnt to them, and check that the result is
1217 consistent with the instance types [p] y Int
1218
1219 We do *not* assume (at this point) the the bound variables of
1220 the associated type instance decl are the same as for the parent
1221 instance decl. So, for example,
1222
1223 instance C [p] Int
1224 type T [q] y Int = ...
1225
1226 would work equally well. Reason: making the *kind* variables line
1227 up is much harder. Example (Trac #7282):
1228 class Foo (xs :: [k]) where
1229 type Bar xs :: *
1230
1231 instance Foo '[] where
1232 type Bar '[] = Int
1233 Here the instance decl really looks like
1234 instance Foo k ('[] k) where
1235 type Bar k ('[] k) = Int
1236 but the k's are not scoped, and hence won't match Uniques.
1237
1238 So instead we just match structure, with tcMatchTyX, and check
1239 that distinct type variables match 1-1 with distinct type variables.
1240
1241 HOWEVER, we *still* make the instance type variables scope over the
1242 type instances, to pick up non-obvious kinds. Eg
1243 class Foo (a :: k) where
1244 type F a
1245 instance Foo (b :: k -> k) where
1246 type F b = Int
1247 Here the instance is kind-indexed and really looks like
1248 type F (k->k) (b::k->k) = Int
1249 But if the 'b' didn't scope, we would make F's instance too
1250 poly-kinded.
1251 -}
1252
1253 -- | Extra information needed when type-checking associated types. The 'Class' is
1254 -- the enclosing class, and the @VarEnv Type@ maps class variables to their
1255 -- instance types.
1256 type ClsInfo = (Class, VarEnv Type)
1257
1258 checkConsistentFamInst
1259 :: Maybe ClsInfo
1260 -> TyCon -- ^ Family tycon
1261 -> [TyVar] -- ^ Type variables of the family instance
1262 -> [Type] -- ^ Type patterns from instance
1263 -> TcM ()
1264 -- See Note [Checking consistent instantiation]
1265
1266 checkConsistentFamInst Nothing _ _ _ = return ()
1267 checkConsistentFamInst (Just (clas, mini_env)) fam_tc at_tvs at_tys
1268 = do { -- Check that the associated type indeed comes from this class
1269 checkTc (Just clas == tyConAssoc_maybe fam_tc)
1270 (badATErr (className clas) (tyConName fam_tc))
1271
1272 -- See Note [Checking consistent instantiation] in TcTyClsDecls
1273 -- Check right to left, so that we spot type variable
1274 -- inconsistencies before (more confusing) kind variables
1275 ; discardResult $ foldrM check_arg emptyTCvSubst $
1276 tyConTyVars fam_tc `zip` at_tys }
1277 where
1278 at_tv_set = mkVarSet at_tvs
1279
1280 check_arg :: (TyVar, Type) -> TCvSubst -> TcM TCvSubst
1281 check_arg (fam_tc_tv, at_ty) subst
1282 | Just inst_ty <- lookupVarEnv mini_env fam_tc_tv
1283 = case tcMatchTyX at_tv_set subst at_ty inst_ty of
1284 Just subst | all_distinct subst -> return subst
1285 _ -> failWithTc $ wrongATArgErr at_ty inst_ty
1286 -- No need to instantiate here, because the axiom
1287 -- uses the same type variables as the assocated class
1288 | otherwise
1289 = return subst -- Allow non-type-variable instantiation
1290 -- See Note [Associated type instances]
1291
1292 all_distinct :: TCvSubst -> Bool
1293 -- True if all the variables mapped the substitution
1294 -- map to *distinct* type *variables*
1295 all_distinct subst = go [] at_tvs
1296 where
1297 go _ [] = True
1298 go acc (tv:tvs) = case lookupTyVar subst tv of
1299 Nothing -> go acc tvs
1300 Just ty | Just tv' <- tcGetTyVar_maybe ty
1301 , tv' `notElem` acc
1302 -> go (tv' : acc) tvs
1303 _other -> False
1304
1305 badATErr :: Name -> Name -> SDoc
1306 badATErr clas op
1307 = hsep [ptext (sLit "Class"), quotes (ppr clas),
1308 ptext (sLit "does not have an associated type"), quotes (ppr op)]
1309
1310 wrongATArgErr :: Type -> Type -> SDoc
1311 wrongATArgErr ty instTy =
1312 sep [ ptext (sLit "Type indexes must match class instance head")
1313 , ptext (sLit "Found") <+> quotes (ppr ty)
1314 <+> ptext (sLit "but expected") <+> quotes (ppr instTy)
1315 ]
1316
1317 {-
1318 ************************************************************************
1319 * *
1320 Checking type instance well-formedness and termination
1321 * *
1322 ************************************************************************
1323 -}
1324
1325 checkValidCoAxiom :: CoAxiom Branched -> TcM ()
1326 checkValidCoAxiom ax@(CoAxiom { co_ax_tc = fam_tc, co_ax_branches = branches })
1327 = do { mapM_ (checkValidCoAxBranch Nothing fam_tc) branch_list
1328 ; foldlM_ check_branch_compat [] branch_list }
1329 where
1330 branch_list = fromBranches branches
1331 injectivity = familyTyConInjectivityInfo fam_tc
1332
1333 check_branch_compat :: [CoAxBranch] -- previous branches in reverse order
1334 -> CoAxBranch -- current branch
1335 -> TcM [CoAxBranch]-- current branch : previous branches
1336 -- Check for
1337 -- (a) this branch is dominated by previous ones
1338 -- (b) failure of injectivity
1339 check_branch_compat prev_branches cur_branch
1340 | cur_branch `isDominatedBy` prev_branches
1341 = do { addWarnAt (coAxBranchSpan cur_branch) $
1342 inaccessibleCoAxBranch ax cur_branch
1343 ; return prev_branches }
1344 | otherwise
1345 = do { check_injectivity prev_branches cur_branch
1346 ; return (cur_branch : prev_branches) }
1347
1348 -- Injectivity check: check whether a new (CoAxBranch) can extend
1349 -- already checked equations without violating injectivity
1350 -- annotation supplied by the user.
1351 -- See Note [Verifying injectivity annotation] in FamInstEnv
1352 check_injectivity prev_branches cur_branch
1353 | Injective inj <- injectivity
1354 = do { let conflicts =
1355 fst $ foldl (gather_conflicts inj prev_branches cur_branch)
1356 ([], 0) prev_branches
1357 ; mapM_ (\(err, span) -> setSrcSpan span $ addErr err)
1358 (makeInjectivityErrors ax cur_branch inj conflicts) }
1359 | otherwise
1360 = return ()
1361
1362 gather_conflicts inj prev_branches cur_branch (acc, n) branch
1363 -- n is 0-based index of branch in prev_branches
1364 = case injectiveBranches inj cur_branch branch of
1365 InjectivityUnified ax1 ax2
1366 | ax1 `isDominatedBy` (replace_br prev_branches n ax2)
1367 -> (acc, n + 1)
1368 | otherwise
1369 -> (branch : acc, n + 1)
1370 InjectivityAccepted -> (acc, n + 1)
1371
1372 -- Replace n-th element in the list. Assumes 0-based indexing.
1373 replace_br :: [CoAxBranch] -> Int -> CoAxBranch -> [CoAxBranch]
1374 replace_br brs n br = take n brs ++ [br] ++ drop (n+1) brs
1375
1376
1377 -- Check that a "type instance" is well-formed (which includes decidability
1378 -- unless -XUndecidableInstances is given).
1379 --
1380 checkValidCoAxBranch :: Maybe ClsInfo
1381 -> TyCon -> CoAxBranch -> TcM ()
1382 checkValidCoAxBranch mb_clsinfo fam_tc
1383 (CoAxBranch { cab_tvs = tvs, cab_cvs = cvs
1384 , cab_lhs = typats
1385 , cab_rhs = rhs, cab_loc = loc })
1386 = checkValidTyFamEqn mb_clsinfo fam_tc tvs cvs typats rhs loc
1387
1388 -- | Do validity checks on a type family equation, including consistency
1389 -- with any enclosing class instance head, termination, and lack of
1390 -- polytypes.
1391 checkValidTyFamEqn :: Maybe ClsInfo
1392 -> TyCon -- ^ of the type family
1393 -> [TyVar] -- ^ bound tyvars in the equation
1394 -> [CoVar] -- ^ bound covars in the equation
1395 -> [Type] -- ^ type patterns
1396 -> Type -- ^ rhs
1397 -> SrcSpan
1398 -> TcM ()
1399 checkValidTyFamEqn mb_clsinfo fam_tc tvs cvs typats rhs loc
1400 = setSrcSpan loc $
1401 do { checkValidFamPats fam_tc tvs cvs typats
1402
1403 -- The argument patterns, and RHS, are all boxed tau types
1404 -- E.g Reject type family F (a :: k1) :: k2
1405 -- type instance F (forall a. a->a) = ...
1406 -- type instance F Int# = ...
1407 -- type instance F Int = forall a. a->a
1408 -- type instance F Int = Int#
1409 -- See Trac #9357
1410 ; env <- tcInitOpenTidyEnv (tyCoVarsOfTypes (rhs : typats))
1411 ; mapM_ checkValidMonoType typats
1412 ; mapM_ (check_lifted env) typats
1413 ; checkValidMonoType rhs
1414 ; check_lifted env rhs
1415
1416 -- We have a decidable instance unless otherwise permitted
1417 ; undecidable_ok <- xoptM LangExt.UndecidableInstances
1418 ; unless undecidable_ok $
1419 mapM_ addErrTc (checkFamInstRhs typats (tcTyFamInsts rhs))
1420
1421 -- Check that type patterns match the class instance head
1422 ; checkConsistentFamInst mb_clsinfo fam_tc tvs typats }
1423
1424 -- Make sure that each type family application is
1425 -- (1) strictly smaller than the lhs,
1426 -- (2) mentions no type variable more often than the lhs, and
1427 -- (3) does not contain any further type family instances.
1428 --
1429 checkFamInstRhs :: [Type] -- lhs
1430 -> [(TyCon, [Type])] -- type family instances
1431 -> [MsgDoc]
1432 checkFamInstRhs lhsTys famInsts
1433 = mapMaybe check famInsts
1434 where
1435 size = sizeTypes lhsTys
1436 fvs = fvTypes lhsTys
1437 check (tc, tys)
1438 | not (all isTyFamFree tys) = Just (nestedMsg what)
1439 | not (null bad_tvs) = Just (noMoreMsg bad_tvs what)
1440 | size <= sizeTypes tys = Just (smallerMsg what)
1441 | otherwise = Nothing
1442 where
1443 what = ptext (sLit "type family application") <+> quotes (pprType (TyConApp tc tys))
1444 bad_tvs = fvTypes tys \\ fvs
1445
1446 checkValidFamPats :: TyCon -> [TyVar] -> [CoVar] -> [Type] -> TcM ()
1447 -- Patterns in a 'type instance' or 'data instance' decl should
1448 -- a) contain no type family applications
1449 -- (vanilla synonyms are fine, though)
1450 -- b) properly bind all their free type variables
1451 -- e.g. we disallow (Trac #7536)
1452 -- type T a = Int
1453 -- type instance F (T a) = a
1454 -- c) Have the right number of patterns
1455 checkValidFamPats fam_tc tvs cvs ty_pats
1456 = do { -- A family instance must have exactly the same number of type
1457 -- parameters as the family declaration. You can't write
1458 -- type family F a :: * -> *
1459 -- type instance F Int y = y
1460 -- because then the type (F Int) would be like (\y.y)
1461 checkTc (length ty_pats == fam_arity) $
1462 wrongNumberOfParmsErr (fam_arity - count isInvisibleBinder fam_bndrs)
1463 -- report only explicit arguments
1464
1465 ; mapM_ checkTyFamFreeness ty_pats
1466 ; let unbound_tcvs = filterOut (`elemVarSet` exactTyCoVarsOfTypes ty_pats) (tvs ++ cvs)
1467 ; checkTc (null unbound_tcvs) (famPatErr fam_tc unbound_tcvs ty_pats) }
1468 where fam_arity = tyConArity fam_tc
1469 fam_bndrs = take fam_arity $ fst $ splitPiTys (tyConKind fam_tc)
1470
1471 wrongNumberOfParmsErr :: Arity -> SDoc
1472 wrongNumberOfParmsErr exp_arity
1473 = ptext (sLit "Number of parameters must match family declaration; expected")
1474 <+> ppr exp_arity
1475
1476 -- Ensure that no type family instances occur in a type.
1477 checkTyFamFreeness :: Type -> TcM ()
1478 checkTyFamFreeness ty
1479 = checkTc (isTyFamFree ty) $
1480 tyFamInstIllegalErr ty
1481
1482 -- Check that a type does not contain any type family applications.
1483 --
1484 isTyFamFree :: Type -> Bool
1485 isTyFamFree = null . tcTyFamInsts
1486
1487 -- Error messages
1488
1489 inaccessibleCoAxBranch :: CoAxiom br -> CoAxBranch -> SDoc
1490 inaccessibleCoAxBranch fi_ax cur_branch
1491 = ptext (sLit "Type family instance equation is overlapped:") $$
1492 nest 2 (pprCoAxBranch fi_ax cur_branch)
1493
1494 tyFamInstIllegalErr :: Type -> SDoc
1495 tyFamInstIllegalErr ty
1496 = hang (ptext (sLit "Illegal type synonym family application in instance") <>
1497 colon) 2 $
1498 ppr ty
1499
1500 nestedMsg :: SDoc -> SDoc
1501 nestedMsg what
1502 = sep [ ptext (sLit "Illegal nested") <+> what
1503 , parens undecidableMsg ]
1504
1505 famPatErr :: TyCon -> [TyVar] -> [Type] -> SDoc
1506 famPatErr fam_tc tvs pats
1507 = hang (ptext (sLit "Family instance purports to bind type variable") <> plural tvs
1508 <+> pprQuotedList tvs)
1509 2 (hang (ptext (sLit "but the real LHS (expanding synonyms) is:"))
1510 2 (pprTypeApp fam_tc (map expandTypeSynonyms pats) <+> ptext (sLit "= ...")))
1511
1512 {-
1513 ************************************************************************
1514 * *
1515 Telescope checking
1516 * *
1517 ************************************************************************
1518
1519 Note [Bad telescopes]
1520 ~~~~~~~~~~~~~~~~~~~~~
1521 Now that we can mix type and kind variables, there are an awful lot of
1522 ways to shoot yourself in the foot. Here are some.
1523
1524 data SameKind :: k -> k -> * -- just to force unification
1525
1526 1. data T1 a k (b :: k) (x :: SameKind a b)
1527
1528 The problem here is that we discover that a and b should have the same
1529 kind. But this kind mentions k, which is bound *after* a.
1530 (Testcase: dependent/should_fail/BadTelescope)
1531
1532 2. data T2 a (c :: Proxy b) (d :: Proxy a) (x :: SameKind b d)
1533
1534 Note that b is not bound. Yet its kind mentions a. Because we have
1535 a nice rule that all implicitly bound variables come before others,
1536 this is bogus. (We could probably figure out to put b between a and c.
1537 But I think this is doing users a disservice, in the long run.)
1538 (Testcase: dependent/should_fail/BadTelescope4)
1539
1540 3. t3 :: forall a. (forall k (b :: k). SameKind a b) -> ()
1541
1542 This is a straightforward skolem escape. Note that a and b need to have
1543 the same kind.
1544 (Testcase: polykinds/T11142)
1545
1546 How do we deal with all of this? For TyCons, we have checkValidTyConTyVars.
1547 That function looks to see if any of the tyConTyVars are repeated, but
1548 it's really a telescope check. It works because all tycons are kind-generalized.
1549 If there is a bad telescope, the kind-generalization will end up generalizing
1550 over a variable bound later in the telescope.
1551
1552 For non-tycons, we do scope checking when we bring tyvars into scope,
1553 in tcImplicitTKBndrs and tcHsTyVarBndrs. Note that we also have to
1554 sort implicit binders into a well-scoped order whenever we have implicit
1555 binders to worry about. This is done in quantifyTyVars and in
1556 tcImplicitTKBndrs.
1557 -}
1558
1559 -- | Check a list of binders to see if they make a valid telescope.
1560 -- The key property we're checking for is scoping. For example:
1561 -- > data SameKind :: k -> k -> *
1562 -- > data X a k (b :: k) (c :: SameKind a b)
1563 -- Kind inference says that a's kind should be k. But that's impossible,
1564 -- because k isn't in scope when a is bound. This check has to come before
1565 -- general validity checking, because once we kind-generalise, this sort
1566 -- of problem is harder to spot (as we'll generalise over the unbound
1567 -- k in a's type.) See also Note [Bad telescopes].
1568 checkValidTelescope :: SDoc -- the original user-written telescope
1569 -> [TyVar] -- explicit vars (not necessarily zonked)
1570 -> SDoc -- note to put at bottom of message
1571 -> TcM () -- returns zonked tyvars
1572 checkValidTelescope hs_tvs orig_tvs extra
1573 = discardResult $ checkZonkValidTelescope hs_tvs orig_tvs extra
1574
1575 -- | Like 'checkZonkValidTelescope', but returns the zonked tyvars
1576 checkZonkValidTelescope :: SDoc
1577 -> [TyVar]
1578 -> SDoc
1579 -> TcM [TyVar]
1580 checkZonkValidTelescope hs_tvs orig_tvs extra
1581 = do { orig_tvs <- mapM zonkTyCoVarKind orig_tvs
1582 ; let (_, sorted_tidied_tvs) = tidyTyCoVarBndrs emptyTidyEnv $
1583 toposortTyVars orig_tvs
1584 ; unless (go [] emptyVarSet orig_tvs) $
1585 addErr $
1586 vcat [ hang (text "These kind and type variables:" <+> hs_tvs $$
1587 text "are out of dependency order. Perhaps try this ordering:")
1588 2 (sep (map pprTvBndr sorted_tidied_tvs))
1589 , extra ]
1590 ; return orig_tvs }
1591
1592 where
1593 go :: [TyVar] -- misplaced variables
1594 -> TyVarSet -> [TyVar] -> Bool
1595 go errs in_scope [] = null (filter (`elemVarSet` in_scope) errs)
1596 -- report an error only when the variable in the kind is brought
1597 -- into scope later in the telescope. Otherwise, we'll just quantify
1598 -- over it in kindGeneralize, as we should.
1599
1600 go errs in_scope (tv:tvs)
1601 = let bad_tvs = tyCoVarsOfType (tyVarKind tv) `minusVarSet` in_scope in
1602 go (varSetElems bad_tvs ++ errs) (in_scope `extendVarSet` tv) tvs
1603
1604 -- | After inferring kinds of type variables, check to make sure that the
1605 -- inferred kinds any of the type variables bound in a smaller scope.
1606 -- This is a skolem escape check. See also Note [Bad telescopes].
1607 checkValidInferredKinds :: [TyVar] -- ^ vars to check (zonked)
1608 -> TyVarSet -- ^ vars out of scope
1609 -> SDoc -- ^ suffix to error message
1610 -> TcM ()
1611 checkValidInferredKinds orig_kvs out_of_scope extra
1612 = do { let bad_pairs = [ (tv, kv)
1613 | kv <- orig_kvs
1614 , Just tv <- map (lookupVarSet out_of_scope)
1615 (tyCoVarsOfTypeList (tyVarKind kv)) ]
1616 report (tidyTyVarOcc env -> tv, tidyTyVarOcc env -> kv)
1617 = addErr $
1618 text "The kind of variable" <+>
1619 quotes (ppr kv) <> text ", namely" <+>
1620 quotes (ppr (tyVarKind kv)) <> comma $$
1621 text "depends on variable" <+>
1622 quotes (ppr tv) <+> text "from an inner scope" $$
1623 text "Perhaps bind" <+> quotes (ppr kv) <+>
1624 text "sometime after binding" <+>
1625 quotes (ppr tv) $$
1626 extra
1627 ; mapM_ report bad_pairs }
1628
1629 where
1630 (env1, _) = tidyTyCoVarBndrs emptyTidyEnv orig_kvs
1631 (env, _) = tidyTyCoVarBndrs env1 (varSetElems out_of_scope)
1632
1633 {-
1634 ************************************************************************
1635 * *
1636 \subsection{Auxiliary functions}
1637 * *
1638 ************************************************************************
1639 -}
1640
1641 -- Free variables of a type, retaining repetitions, and expanding synonyms
1642 fvType :: Type -> [TyCoVar]
1643 fvType ty | Just exp_ty <- coreView ty = fvType exp_ty
1644 fvType (TyVarTy tv) = [tv]
1645 fvType (TyConApp _ tys) = fvTypes tys
1646 fvType (LitTy {}) = []
1647 fvType (AppTy fun arg) = fvType fun ++ fvType arg
1648 fvType (ForAllTy bndr ty)
1649 = fvType (binderType bndr) ++
1650 caseBinder bndr (\tv -> filter (/= tv)) (const id) (fvType ty)
1651 fvType (CastTy ty co) = fvType ty ++ fvCo co
1652 fvType (CoercionTy co) = fvCo co
1653
1654 fvTypes :: [Type] -> [TyVar]
1655 fvTypes tys = concat (map fvType tys)
1656
1657 fvCo :: Coercion -> [TyCoVar]
1658 fvCo (Refl _ ty) = fvType ty
1659 fvCo (TyConAppCo _ _ args) = concatMap fvCo args
1660 fvCo (AppCo co arg) = fvCo co ++ fvCo arg
1661 fvCo (ForAllCo tv h co) = filter (/= tv) (fvCo co) ++ fvCo h
1662 fvCo (CoVarCo v) = [v]
1663 fvCo (AxiomInstCo _ _ args) = concatMap fvCo args
1664 fvCo (UnivCo p _ t1 t2) = fvProv p ++ fvType t1 ++ fvType t2
1665 fvCo (SymCo co) = fvCo co
1666 fvCo (TransCo co1 co2) = fvCo co1 ++ fvCo co2
1667 fvCo (NthCo _ co) = fvCo co
1668 fvCo (LRCo _ co) = fvCo co
1669 fvCo (InstCo co arg) = fvCo co ++ fvCo arg
1670 fvCo (CoherenceCo co1 co2) = fvCo co1 ++ fvCo co2
1671 fvCo (KindCo co) = fvCo co
1672 fvCo (SubCo co) = fvCo co
1673 fvCo (AxiomRuleCo _ cs) = concatMap fvCo cs
1674
1675 fvProv :: UnivCoProvenance -> [TyCoVar]
1676 fvProv UnsafeCoerceProv = []
1677 fvProv (PhantomProv co) = fvCo co
1678 fvProv (ProofIrrelProv co) = fvCo co
1679 fvProv (PluginProv _) = []
1680 fvProv (HoleProv h) = pprPanic "fvProv falls into a hole" (ppr h)
1681
1682 sizeType :: Type -> Int
1683 -- Size of a type: the number of variables and constructors
1684 sizeType ty | Just exp_ty <- coreView ty = sizeType exp_ty
1685 sizeType (TyVarTy {}) = 1
1686 sizeType (TyConApp _ tys) = sizeTypes tys + 1
1687 sizeType (LitTy {}) = 1
1688 sizeType (AppTy fun arg) = sizeType fun + sizeType arg
1689 sizeType (ForAllTy (Anon arg) res)
1690 = sizeType arg + sizeType res + 1
1691 sizeType (ForAllTy (Named {}) ty)
1692 = sizeType ty
1693 sizeType (CastTy ty _) = sizeType ty
1694 sizeType (CoercionTy _) = 1
1695
1696 sizeTypes :: [Type] -> Int
1697 sizeTypes = sum . map sizeType
1698
1699 -- Size of a predicate
1700 --
1701 -- We are considering whether class constraints terminate.
1702 -- Equality constraints and constraints for the implicit
1703 -- parameter class always termiante so it is safe to say "size 0".
1704 -- (Implicit parameter constraints always terminate because
1705 -- there are no instances for them---they are only solved by
1706 -- "local instances" in expressions).
1707 -- See Trac #4200.
1708 sizePred :: PredType -> Int
1709 sizePred ty = goClass ty
1710 where
1711 goClass p = go (classifyPredType p)
1712
1713 go (ClassPred cls tys')
1714 | isTerminatingClass cls = 0
1715 | otherwise = sizeTypes tys'
1716 go (EqPred {}) = 0
1717 go (IrredPred ty) = sizeType ty
1718
1719 -- | When this says "True", ignore this class constraint during
1720 -- a termination check
1721 isTerminatingClass :: Class -> Bool
1722 isTerminatingClass cls
1723 = isIPClass cls
1724 || cls `hasKey` typeableClassKey
1725 || cls `hasKey` coercibleTyConKey
1726 || cls `hasKey` eqTyConKey
1727 || cls `hasKey` heqTyConKey
1728
1729 -- | Tidy before printing a type
1730 ppr_tidy :: TidyEnv -> Type -> SDoc
1731 ppr_tidy env ty = pprType (tidyType env ty)