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