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