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