Treat isConstraintKind more consistently
[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, checkValidInstHead, validDerivPred,
13 checkTySynRhs,
14 ClsInstInfo, checkValidCoAxiom, checkValidCoAxBranch,
15 checkValidTyFamEqn,
16 arityErr, badATErr,
17 checkValidTelescope,
18 allDistinctTyVars
19 ) where
20
21 #include "HsVersions.h"
22
23 import GhcPrelude
24
25 import Maybes
26
27 -- friends:
28 import TcUnify ( tcSubType_NC )
29 import TcSimplify ( simplifyAmbiguityCheck )
30 import ClsInst ( matchGlobalInst, ClsInstResult(..), InstanceWhat(..) )
31 import TyCoRep
32 import TcType hiding ( sizeType, sizeTypes )
33 import TysWiredIn ( heqTyConName, coercibleTyConName )
34 import PrelNames
35 import Type
36 import Coercion
37 import CoAxiom
38 import Class
39 import TyCon
40
41 -- others:
42 import HsSyn -- HsType
43 import TcRnMonad -- TcType, amongst others
44 import TcEnv ( tcInitTidyEnv, tcInitOpenTidyEnv )
45 import FunDeps
46 import FamInstEnv ( isDominatedBy, injectiveBranches,
47 InjectivityCheckResult(..) )
48 import FamInst ( makeInjectivityErrors )
49 import Name
50 import VarEnv
51 import VarSet
52 import Id ( idType, idName )
53 import Var ( TyVarBndr(..), mkTyVar )
54 import ErrUtils
55 import DynFlags
56 import Util
57 import ListSetOps
58 import SrcLoc
59 import Outputable
60 import Module
61 import Bag ( emptyBag )
62 import Unique ( mkAlphaTyVarUnique )
63 import qualified GHC.LanguageExtensions as LangExt
64
65 import Control.Monad
66 import Data.List ( (\\) )
67 import qualified Data.List.NonEmpty as NE
68
69 {-
70 ************************************************************************
71 * *
72 Checking for ambiguity
73 * *
74 ************************************************************************
75
76 Note [The ambiguity check for type signatures]
77 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
78 checkAmbiguity is a check on *user-supplied type signatures*. It is
79 *purely* there to report functions that cannot possibly be called. So for
80 example we want to reject:
81 f :: C a => Int
82 The idea is there can be no legal calls to 'f' because every call will
83 give rise to an ambiguous constraint. We could soundly omit the
84 ambiguity check on type signatures entirely, at the expense of
85 delaying ambiguity errors to call sites. Indeed, the flag
86 -XAllowAmbiguousTypes switches off the ambiguity check.
87
88 What about things like this:
89 class D a b | a -> b where ..
90 h :: D Int b => Int
91 The Int may well fix 'b' at the call site, so that signature should
92 not be rejected. Moreover, using *visible* fundeps is too
93 conservative. Consider
94 class X a b where ...
95 class D a b | a -> b where ...
96 instance D a b => X [a] b where...
97 h :: X a b => a -> a
98 Here h's type looks ambiguous in 'b', but here's a legal call:
99 ...(h [True])...
100 That gives rise to a (X [Bool] beta) constraint, and using the
101 instance means we need (D Bool beta) and that fixes 'beta' via D's
102 fundep!
103
104 Behind all these special cases there is a simple guiding principle.
105 Consider
106
107 f :: <type>
108 f = ...blah...
109
110 g :: <type>
111 g = f
112
113 You would think that the definition of g would surely typecheck!
114 After all f has exactly the same type, and g=f. But in fact f's type
115 is instantiated and the instantiated constraints are solved against
116 the originals, so in the case an ambiguous type it won't work.
117 Consider our earlier example f :: C a => Int. Then in g's definition,
118 we'll instantiate to (C alpha) and try to deduce (C alpha) from (C a),
119 and fail.
120
121 So in fact we use this as our *definition* of ambiguity. We use a
122 very similar test for *inferred* types, to ensure that they are
123 unambiguous. See Note [Impedance matching] in TcBinds.
124
125 This test is very conveniently implemented by calling
126 tcSubType <type> <type>
127 This neatly takes account of the functional dependecy stuff above,
128 and implicit parameter (see Note [Implicit parameters and ambiguity]).
129 And this is what checkAmbiguity does.
130
131 What about this, though?
132 g :: C [a] => Int
133 Is every call to 'g' ambiguous? After all, we might have
134 instance C [a] where ...
135 at the call site. So maybe that type is ok! Indeed even f's
136 quintessentially ambiguous type might, just possibly be callable:
137 with -XFlexibleInstances we could have
138 instance C a where ...
139 and now a call could be legal after all! Well, we'll reject this
140 unless the instance is available *here*.
141
142 Note [When to call checkAmbiguity]
143 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
144 We call checkAmbiguity
145 (a) on user-specified type signatures
146 (b) in checkValidType
147
148 Conncerning (b), you might wonder about nested foralls. What about
149 f :: forall b. (forall a. Eq a => b) -> b
150 The nested forall is ambiguous. Originally we called checkAmbiguity
151 in the forall case of check_type, but that had two bad consequences:
152 * We got two error messages about (Eq b) in a nested forall like this:
153 g :: forall a. Eq a => forall b. Eq b => a -> a
154 * If we try to check for ambiguity of a nested forall like
155 (forall a. Eq a => b), the implication constraint doesn't bind
156 all the skolems, which results in "No skolem info" in error
157 messages (see Trac #10432).
158
159 To avoid this, we call checkAmbiguity once, at the top, in checkValidType.
160 (I'm still a bit worried about unbound skolems when the type mentions
161 in-scope type variables.)
162
163 In fact, because of the co/contra-variance implemented in tcSubType,
164 this *does* catch function f above. too.
165
166 Concerning (a) the ambiguity check is only used for *user* types, not
167 for types coming from inteface files. The latter can legitimately
168 have ambiguous types. Example
169
170 class S a where s :: a -> (Int,Int)
171 instance S Char where s _ = (1,1)
172 f:: S a => [a] -> Int -> (Int,Int)
173 f (_::[a]) x = (a*x,b)
174 where (a,b) = s (undefined::a)
175
176 Here the worker for f gets the type
177 fw :: forall a. S a => Int -> (# Int, Int #)
178
179
180 Note [Implicit parameters and ambiguity]
181 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
182 Only a *class* predicate can give rise to ambiguity
183 An *implicit parameter* cannot. For example:
184 foo :: (?x :: [a]) => Int
185 foo = length ?x
186 is fine. The call site will supply a particular 'x'
187
188 Furthermore, the type variables fixed by an implicit parameter
189 propagate to the others. E.g.
190 foo :: (Show a, ?x::[a]) => Int
191 foo = show (?x++?x)
192 The type of foo looks ambiguous. But it isn't, because at a call site
193 we might have
194 let ?x = 5::Int in foo
195 and all is well. In effect, implicit parameters are, well, parameters,
196 so we can take their type variables into account as part of the
197 "tau-tvs" stuff. This is done in the function 'FunDeps.grow'.
198 -}
199
200 checkAmbiguity :: UserTypeCtxt -> Type -> TcM ()
201 checkAmbiguity ctxt ty
202 | wantAmbiguityCheck ctxt
203 = do { traceTc "Ambiguity check for" (ppr ty)
204 -- Solve the constraints eagerly because an ambiguous type
205 -- can cause a cascade of further errors. Since the free
206 -- tyvars are skolemised, we can safely use tcSimplifyTop
207 ; allow_ambiguous <- xoptM LangExt.AllowAmbiguousTypes
208 ; (_wrap, wanted) <- addErrCtxt (mk_msg allow_ambiguous) $
209 captureConstraints $
210 tcSubType_NC ctxt ty ty
211 ; simplifyAmbiguityCheck ty wanted
212
213 ; traceTc "Done ambiguity check for" (ppr ty) }
214
215 | otherwise
216 = return ()
217 where
218 mk_msg allow_ambiguous
219 = vcat [ text "In the ambiguity check for" <+> what
220 , ppUnless allow_ambiguous ambig_msg ]
221 ambig_msg = text "To defer the ambiguity check to use sites, enable AllowAmbiguousTypes"
222 what | Just n <- isSigMaybe ctxt = quotes (ppr n)
223 | otherwise = pprUserTypeCtxt ctxt
224
225 wantAmbiguityCheck :: UserTypeCtxt -> Bool
226 wantAmbiguityCheck ctxt
227 = case ctxt of -- See Note [When we don't check for ambiguity]
228 GhciCtxt -> False
229 TySynCtxt {} -> False
230 TypeAppCtxt -> False
231 _ -> True
232
233 checkUserTypeError :: Type -> TcM ()
234 -- Check to see if the type signature mentions "TypeError blah"
235 -- anywhere in it, and fail if so.
236 --
237 -- Very unsatisfactorily (Trac #11144) we need to tidy the type
238 -- because it may have come from an /inferred/ signature, not a
239 -- user-supplied one. This is really only a half-baked fix;
240 -- the other errors in checkValidType don't do tidying, and so
241 -- may give bad error messages when given an inferred type.
242 checkUserTypeError = check
243 where
244 check ty
245 | Just msg <- userTypeError_maybe ty = fail_with msg
246 | Just (_,ts) <- splitTyConApp_maybe ty = mapM_ check ts
247 | Just (t1,t2) <- splitAppTy_maybe ty = check t1 >> check t2
248 | Just (_,t1) <- splitForAllTy_maybe ty = check t1
249 | otherwise = return ()
250
251 fail_with msg = do { env0 <- tcInitTidyEnv
252 ; let (env1, tidy_msg) = tidyOpenType env0 msg
253 ; failWithTcM (env1, pprUserTypeErrorTy tidy_msg) }
254
255
256 {- Note [When we don't check for ambiguity]
257 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
258 In a few places we do not want to check a user-specified type for ambiguity
259
260 * GhciCtxt: Allow ambiguous types in GHCi's :kind command
261 E.g. type family T a :: * -- T :: forall k. k -> *
262 Then :k T should work in GHCi, not complain that
263 (T k) is ambiguous!
264
265 * TySynCtxt: type T a b = C a b => blah
266 It may be that when we /use/ T, we'll give an 'a' or 'b' that somehow
267 cure the ambiguity. So we defer the ambiguity check to the use site.
268
269 There is also an implementation reason (Trac #11608). In the RHS of
270 a type synonym we don't (currently) instantiate 'a' and 'b' with
271 TcTyVars before calling checkValidType, so we get asertion failures
272 from doing an ambiguity check on a type with TyVars in it. Fixing this
273 would not be hard, but let's wait till there's a reason.
274
275 * TypeAppCtxt: visible type application
276 f @ty
277 No need to check ty for ambiguity
278
279
280 ************************************************************************
281 * *
282 Checking validity of a user-defined type
283 * *
284 ************************************************************************
285
286 When dealing with a user-written type, we first translate it from an HsType
287 to a Type, performing kind checking, and then check various things that should
288 be true about it. We don't want to perform these checks at the same time
289 as the initial translation because (a) they are unnecessary for interface-file
290 types and (b) when checking a mutually recursive group of type and class decls,
291 we can't "look" at the tycons/classes yet. Also, the checks are rather
292 diverse, and used to really mess up the other code.
293
294 One thing we check for is 'rank'.
295
296 Rank 0: monotypes (no foralls)
297 Rank 1: foralls at the front only, Rank 0 inside
298 Rank 2: foralls at the front, Rank 1 on left of fn arrow,
299
300 basic ::= tyvar | T basic ... basic
301
302 r2 ::= forall tvs. cxt => r2a
303 r2a ::= r1 -> r2a | basic
304 r1 ::= forall tvs. cxt => r0
305 r0 ::= r0 -> r0 | basic
306
307 Another thing is to check that type synonyms are saturated.
308 This might not necessarily show up in kind checking.
309 type A i = i
310 data T k = MkT (k Int)
311 f :: T A -- BAD!
312 -}
313
314 checkValidType :: UserTypeCtxt -> Type -> TcM ()
315 -- Checks that a user-written type is valid for the given context
316 -- Assumes argument is fully zonked
317 -- Not used for instance decls; checkValidInstance instead
318 checkValidType ctxt ty
319 = do { traceTc "checkValidType" (ppr ty <+> text "::" <+> ppr (typeKind ty))
320 ; rankn_flag <- xoptM LangExt.RankNTypes
321 ; impred_flag <- xoptM LangExt.ImpredicativeTypes
322 ; let gen_rank :: Rank -> Rank
323 gen_rank r | rankn_flag = ArbitraryRank
324 | otherwise = r
325
326 rank1 = gen_rank r1
327 rank0 = gen_rank r0
328
329 r0 = rankZeroMonoType
330 r1 = LimitedRank True r0
331
332 rank
333 = case ctxt of
334 DefaultDeclCtxt-> MustBeMonoType
335 ResSigCtxt -> MustBeMonoType
336 PatSigCtxt -> rank0
337 RuleSigCtxt _ -> rank1
338 TySynCtxt _ -> rank0
339
340 ExprSigCtxt -> rank1
341 KindSigCtxt -> rank1
342 TypeAppCtxt | impred_flag -> ArbitraryRank
343 | otherwise -> tyConArgMonoType
344 -- Normally, ImpredicativeTypes is handled in check_arg_type,
345 -- but visible type applications don't go through there.
346 -- So we do this check here.
347
348 FunSigCtxt {} -> rank1
349 InfSigCtxt _ -> ArbitraryRank -- Inferred type
350 ConArgCtxt _ -> rank1 -- We are given the type of the entire
351 -- constructor, hence rank 1
352 PatSynCtxt _ -> rank1
353
354 ForSigCtxt _ -> rank1
355 SpecInstCtxt -> rank1
356 ThBrackCtxt -> rank1
357 GhciCtxt -> ArbitraryRank
358
359 TyVarBndrKindCtxt _ -> rank0
360 DataKindCtxt _ -> rank1
361 TySynKindCtxt _ -> rank1
362 TyFamResKindCtxt _ -> rank1
363
364 _ -> panic "checkValidType"
365 -- Can't happen; not used for *user* sigs
366
367 ; env <- tcInitOpenTidyEnv (tyCoVarsOfTypeList ty)
368
369 -- Check the internal validity of the type itself
370 ; check_type env ctxt rank ty
371
372 ; checkUserTypeError ty
373
374 -- Check for ambiguous types. See Note [When to call checkAmbiguity]
375 -- NB: this will happen even for monotypes, but that should be cheap;
376 -- and there may be nested foralls for the subtype test to examine
377 ; checkAmbiguity ctxt ty
378
379 ; traceTc "checkValidType done" (ppr ty <+> text "::" <+> ppr (typeKind ty)) }
380
381 checkValidMonoType :: Type -> TcM ()
382 -- Assumes argument is fully zonked
383 checkValidMonoType ty
384 = do { env <- tcInitOpenTidyEnv (tyCoVarsOfTypeList ty)
385 ; check_type env SigmaCtxt MustBeMonoType ty }
386
387 checkTySynRhs :: UserTypeCtxt -> TcType -> TcM ()
388 checkTySynRhs ctxt ty
389 | tcReturnsConstraintKind actual_kind
390 = do { ck <- xoptM LangExt.ConstraintKinds
391 ; if ck
392 then when (tcIsConstraintKind actual_kind)
393 (do { dflags <- getDynFlags
394 ; check_pred_ty emptyTidyEnv dflags ctxt ty })
395 else addErrTcM (constraintSynErr emptyTidyEnv actual_kind) }
396
397 | otherwise
398 = return ()
399 where
400 actual_kind = typeKind ty
401
402 -- | The kind expected in a certain context.
403 data ContextKind = TheKind Kind -- ^ a specific kind
404 | AnythingKind -- ^ any kind will do
405 | OpenKind -- ^ something of the form @TYPE _@
406
407 -- Depending on the context, we might accept any kind (for instance, in a TH
408 -- splice), or only certain kinds (like in type signatures).
409 expectedKindInCtxt :: UserTypeCtxt -> ContextKind
410 expectedKindInCtxt (TySynCtxt _) = AnythingKind
411 expectedKindInCtxt ThBrackCtxt = AnythingKind
412 expectedKindInCtxt GhciCtxt = AnythingKind
413 -- The types in a 'default' decl can have varying kinds
414 -- See Note [Extended defaults]" in TcEnv
415 expectedKindInCtxt DefaultDeclCtxt = AnythingKind
416 expectedKindInCtxt TypeAppCtxt = AnythingKind
417 expectedKindInCtxt (ForSigCtxt _) = TheKind liftedTypeKind
418 expectedKindInCtxt (InstDeclCtxt {}) = TheKind constraintKind
419 expectedKindInCtxt SpecInstCtxt = TheKind constraintKind
420 expectedKindInCtxt _ = OpenKind
421
422 {-
423 Note [Higher rank types]
424 ~~~~~~~~~~~~~~~~~~~~~~~~
425 Technically
426 Int -> forall a. a->a
427 is still a rank-1 type, but it's not Haskell 98 (Trac #5957). So the
428 validity checker allow a forall after an arrow only if we allow it
429 before -- that is, with Rank2Types or RankNTypes
430 -}
431
432 data Rank = ArbitraryRank -- Any rank ok
433
434 | LimitedRank -- Note [Higher rank types]
435 Bool -- Forall ok at top
436 Rank -- Use for function arguments
437
438 | MonoType SDoc -- Monotype, with a suggestion of how it could be a polytype
439
440 | MustBeMonoType -- Monotype regardless of flags
441
442
443 rankZeroMonoType, tyConArgMonoType, synArgMonoType, constraintMonoType :: Rank
444 rankZeroMonoType = MonoType (text "Perhaps you intended to use RankNTypes or Rank2Types")
445 tyConArgMonoType = MonoType (text "GHC doesn't yet support impredicative polymorphism")
446 synArgMonoType = MonoType (text "Perhaps you intended to use LiberalTypeSynonyms")
447 constraintMonoType = MonoType (vcat [ text "A constraint must be a monotype"
448 , text "Perhaps you intended to use QuantifiedConstraints" ])
449
450 funArgResRank :: Rank -> (Rank, Rank) -- Function argument and result
451 funArgResRank (LimitedRank _ arg_rank) = (arg_rank, LimitedRank (forAllAllowed arg_rank) arg_rank)
452 funArgResRank other_rank = (other_rank, other_rank)
453
454 forAllAllowed :: Rank -> Bool
455 forAllAllowed ArbitraryRank = True
456 forAllAllowed (LimitedRank forall_ok _) = forall_ok
457 forAllAllowed _ = False
458
459 ----------------------------------------
460 check_type :: TidyEnv -> UserTypeCtxt -> Rank -> Type -> TcM ()
461 -- The args say what the *type context* requires, independent
462 -- of *flag* settings. You test the flag settings at usage sites.
463 --
464 -- Rank is allowed rank for function args
465 -- Rank 0 means no for-alls anywhere
466
467 check_type env ctxt rank ty
468 | not (null tvbs && null theta)
469 = do { traceTc "check_type" (ppr ty $$ ppr (forAllAllowed rank))
470 ; checkTcM (forAllAllowed rank) (forAllTyErr env rank ty)
471 -- Reject e.g. (Maybe (?x::Int => Int)),
472 -- with a decent error message
473
474 ; check_valid_theta env' SigmaCtxt theta
475 -- Allow type T = ?x::Int => Int -> Int
476 -- but not type T = ?x::Int
477
478 ; check_type env' ctxt rank tau -- Allow foralls to right of arrow
479
480 ; checkTcM (not (any (`elemVarSet` tyCoVarsOfType phi_kind) tvs))
481 (forAllEscapeErr env' ty tau_kind)
482 }
483 where
484 (tvbs, phi) = tcSplitForAllTyVarBndrs ty
485 (theta, tau) = tcSplitPhiTy phi
486
487 tvs = binderVars tvbs
488 (env', _) = tidyTyCoVarBndrs env tvs
489
490 tau_kind = typeKind tau
491 phi_kind | null theta = tau_kind
492 | otherwise = liftedTypeKind
493 -- If there are any constraints, the kind is *. (#11405)
494
495 check_type _ _ _ (TyVarTy _) = return ()
496
497 check_type env ctxt rank (FunTy arg_ty res_ty)
498 = do { check_type env ctxt arg_rank arg_ty
499 ; check_type env ctxt res_rank res_ty }
500 where
501 (arg_rank, res_rank) = funArgResRank rank
502
503 check_type env ctxt rank (AppTy ty1 ty2)
504 = do { check_type env ctxt rank ty1
505 ; check_arg_type env ctxt rank ty2 }
506
507 check_type env ctxt rank ty@(TyConApp tc tys)
508 | isTypeSynonymTyCon tc || isTypeFamilyTyCon tc
509 = check_syn_tc_app env ctxt rank ty tc tys
510 | isUnboxedTupleTyCon tc = check_ubx_tuple env ctxt ty tys
511 | otherwise = mapM_ (check_arg_type env ctxt rank) tys
512
513 check_type _ _ _ (LitTy {}) = return ()
514
515 check_type env ctxt rank (CastTy ty _) = check_type env ctxt rank ty
516
517 check_type _ _ _ ty = pprPanic "check_type" (ppr ty)
518
519 ----------------------------------------
520 check_syn_tc_app :: TidyEnv -> UserTypeCtxt -> Rank -> KindOrType
521 -> TyCon -> [KindOrType] -> TcM ()
522 -- Used for type synonyms and type synonym families,
523 -- which must be saturated,
524 -- but not data families, which need not be saturated
525 check_syn_tc_app env ctxt rank ty tc tys
526 | tys `lengthAtLeast` tc_arity -- Saturated
527 -- Check that the synonym has enough args
528 -- This applies equally to open and closed synonyms
529 -- It's OK to have an *over-applied* type synonym
530 -- data Tree a b = ...
531 -- type Foo a = Tree [a]
532 -- f :: Foo a b -> ...
533 = do { -- See Note [Liberal type synonyms]
534 ; liberal <- xoptM LangExt.LiberalTypeSynonyms
535 ; if not liberal || isTypeFamilyTyCon tc then
536 -- For H98 and synonym families, do check the type args
537 mapM_ check_arg tys
538
539 else -- In the liberal case (only for closed syns), expand then check
540 case tcView ty of
541 Just ty' -> check_type env ctxt rank ty'
542 Nothing -> pprPanic "check_tau_type" (ppr ty) }
543
544 | GhciCtxt <- ctxt -- Accept under-saturated type synonyms in
545 -- GHCi :kind commands; see Trac #7586
546 = mapM_ check_arg tys
547
548 | otherwise
549 = failWithTc (tyConArityErr tc tys)
550 where
551 tc_arity = tyConArity tc
552 check_arg | isTypeFamilyTyCon tc = check_arg_type env ctxt rank
553 | otherwise = check_type env ctxt synArgMonoType
554
555 ----------------------------------------
556 check_ubx_tuple :: TidyEnv -> UserTypeCtxt -> KindOrType
557 -> [KindOrType] -> TcM ()
558 check_ubx_tuple env ctxt ty tys
559 = do { ub_tuples_allowed <- xoptM LangExt.UnboxedTuples
560 ; checkTcM ub_tuples_allowed (ubxArgTyErr env ty)
561
562 ; impred <- xoptM LangExt.ImpredicativeTypes
563 ; let rank' = if impred then ArbitraryRank else tyConArgMonoType
564 -- c.f. check_arg_type
565 -- However, args are allowed to be unlifted, or
566 -- more unboxed tuples, so can't use check_arg_ty
567 ; mapM_ (check_type env ctxt rank') tys }
568
569 ----------------------------------------
570 check_arg_type :: TidyEnv -> UserTypeCtxt -> Rank -> KindOrType -> TcM ()
571 -- The sort of type that can instantiate a type variable,
572 -- or be the argument of a type constructor.
573 -- Not an unboxed tuple, but now *can* be a forall (since impredicativity)
574 -- Other unboxed types are very occasionally allowed as type
575 -- arguments depending on the kind of the type constructor
576 --
577 -- For example, we want to reject things like:
578 --
579 -- instance Ord a => Ord (forall s. T s a)
580 -- and
581 -- g :: T s (forall b.b)
582 --
583 -- NB: unboxed tuples can have polymorphic or unboxed args.
584 -- This happens in the workers for functions returning
585 -- product types with polymorphic components.
586 -- But not in user code.
587 -- Anyway, they are dealt with by a special case in check_tau_type
588
589 check_arg_type _ _ _ (CoercionTy {}) = return ()
590
591 check_arg_type env ctxt rank ty
592 = do { impred <- xoptM LangExt.ImpredicativeTypes
593 ; let rank' = case rank of -- Predictive => must be monotype
594 MustBeMonoType -> MustBeMonoType -- Monotype, regardless
595 _other | impred -> ArbitraryRank
596 | otherwise -> tyConArgMonoType
597 -- Make sure that MustBeMonoType is propagated,
598 -- so that we don't suggest -XImpredicativeTypes in
599 -- (Ord (forall a.a)) => a -> a
600 -- and so that if it Must be a monotype, we check that it is!
601
602 ; check_type env ctxt rank' ty }
603
604 ----------------------------------------
605 forAllTyErr :: TidyEnv -> Rank -> Type -> (TidyEnv, SDoc)
606 forAllTyErr env rank ty
607 = ( env
608 , vcat [ hang herald 2 (ppr_tidy env ty)
609 , suggestion ] )
610 where
611 (tvs, _theta, _tau) = tcSplitSigmaTy ty
612 herald | null tvs = text "Illegal qualified type:"
613 | otherwise = text "Illegal polymorphic type:"
614 suggestion = case rank of
615 LimitedRank {} -> text "Perhaps you intended to use RankNTypes or Rank2Types"
616 MonoType d -> d
617 _ -> Outputable.empty -- Polytype is always illegal
618
619 forAllEscapeErr :: TidyEnv -> Type -> Kind -> (TidyEnv, SDoc)
620 forAllEscapeErr env ty tau_kind
621 = ( env
622 , hang (vcat [ text "Quantified type's kind mentions quantified type variable"
623 , text "(skolem escape)" ])
624 2 (vcat [ text " type:" <+> ppr_tidy env ty
625 , text "of kind:" <+> ppr_tidy env tau_kind ]) )
626
627 ubxArgTyErr :: TidyEnv -> Type -> (TidyEnv, SDoc)
628 ubxArgTyErr env ty
629 = ( env, vcat [ sep [ text "Illegal unboxed tuple type as function argument:"
630 , ppr_tidy env ty ]
631 , text "Perhaps you intended to use UnboxedTuples" ] )
632
633 {-
634 Note [Liberal type synonyms]
635 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
636 If -XLiberalTypeSynonyms is on, expand closed type synonyms *before*
637 doing validity checking. This allows us to instantiate a synonym defn
638 with a for-all type, or with a partially-applied type synonym.
639 e.g. type T a b = a
640 type S m = m ()
641 f :: S (T Int)
642 Here, T is partially applied, so it's illegal in H98. But if you
643 expand S first, then T we get just
644 f :: Int
645 which is fine.
646
647 IMPORTANT: suppose T is a type synonym. Then we must do validity
648 checking on an appliation (T ty1 ty2)
649
650 *either* before expansion (i.e. check ty1, ty2)
651 *or* after expansion (i.e. expand T ty1 ty2, and then check)
652 BUT NOT BOTH
653
654 If we do both, we get exponential behaviour!!
655
656 data TIACons1 i r c = c i ::: r c
657 type TIACons2 t x = TIACons1 t (TIACons1 t x)
658 type TIACons3 t x = TIACons2 t (TIACons1 t x)
659 type TIACons4 t x = TIACons2 t (TIACons2 t x)
660 type TIACons7 t x = TIACons4 t (TIACons3 t x)
661
662
663 ************************************************************************
664 * *
665 \subsection{Checking a theta or source type}
666 * *
667 ************************************************************************
668
669 Note [Implicit parameters in instance decls]
670 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
671 Implicit parameters _only_ allowed in type signatures; not in instance
672 decls, superclasses etc. The reason for not allowing implicit params in
673 instances is a bit subtle. If we allowed
674 instance (?x::Int, Eq a) => Foo [a] where ...
675 then when we saw
676 (e :: (?x::Int) => t)
677 it would be unclear how to discharge all the potential uses of the ?x
678 in e. For example, a constraint Foo [Int] might come out of e, and
679 applying the instance decl would show up two uses of ?x. Trac #8912.
680 -}
681
682 checkValidTheta :: UserTypeCtxt -> ThetaType -> TcM ()
683 -- Assumes argument is fully zonked
684 checkValidTheta ctxt theta
685 = addErrCtxtM (checkThetaCtxt ctxt theta) $
686 do { env <- tcInitOpenTidyEnv (tyCoVarsOfTypesList theta)
687 ; check_valid_theta env ctxt theta }
688
689 -------------------------
690 check_valid_theta :: TidyEnv -> UserTypeCtxt -> [PredType] -> TcM ()
691 check_valid_theta _ _ []
692 = return ()
693 check_valid_theta env ctxt theta
694 = do { dflags <- getDynFlags
695 ; warnTcM (Reason Opt_WarnDuplicateConstraints)
696 (wopt Opt_WarnDuplicateConstraints dflags && notNull dups)
697 (dupPredWarn env dups)
698 ; traceTc "check_valid_theta" (ppr theta)
699 ; mapM_ (check_pred_ty env dflags ctxt) theta }
700 where
701 (_,dups) = removeDups nonDetCmpType theta
702 -- It's OK to use nonDetCmpType because dups only appears in the
703 -- warning
704
705 -------------------------
706 {- Note [Validity checking for constraints]
707 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
708 We look through constraint synonyms so that we can see the underlying
709 constraint(s). For example
710 type Foo = ?x::Int
711 instance Foo => C T
712 We should reject the instance because it has an implicit parameter in
713 the context.
714
715 But we record, in 'under_syn', whether we have looked under a synonym
716 to avoid requiring language extensions at the use site. Main example
717 (Trac #9838):
718
719 {-# LANGUAGE ConstraintKinds #-}
720 module A where
721 type EqShow a = (Eq a, Show a)
722
723 module B where
724 import A
725 foo :: EqShow a => a -> String
726
727 We don't want to require ConstraintKinds in module B.
728 -}
729
730 check_pred_ty :: TidyEnv -> DynFlags -> UserTypeCtxt -> PredType -> TcM ()
731 -- Check the validity of a predicate in a signature
732 -- See Note [Validity checking for constraints]
733 check_pred_ty env dflags ctxt pred
734 = do { check_type env SigmaCtxt rank pred
735 ; check_pred_help False env dflags ctxt pred }
736 where
737 rank | xopt LangExt.QuantifiedConstraints dflags
738 = ArbitraryRank
739 | otherwise
740 = constraintMonoType
741
742 check_pred_help :: Bool -- True <=> under a type synonym
743 -> TidyEnv
744 -> DynFlags -> UserTypeCtxt
745 -> PredType -> TcM ()
746 check_pred_help under_syn env dflags ctxt pred
747 | Just pred' <- tcView pred -- Switch on under_syn when going under a
748 -- synonym (Trac #9838, yuk)
749 = check_pred_help True env dflags ctxt pred'
750
751 | otherwise -- A bit like classifyPredType, but not the same
752 -- E.g. we treat (~) like (~#); and we look inside tuples
753 = case classifyPredType pred of
754 ClassPred cls tys
755 | isCTupleClass cls -> check_tuple_pred under_syn env dflags ctxt pred tys
756 | otherwise -> check_class_pred env dflags ctxt pred cls tys
757
758 EqPred NomEq _ _ -> -- a ~# b
759 check_eq_pred env dflags pred
760
761 EqPred ReprEq _ _ -> -- Ugh! When inferring types we may get
762 -- f :: (a ~R# b) => blha
763 -- And we want to treat that like (Coercible a b)
764 -- We should probably check argument shapes, but we
765 -- didn't do so before, so I'm leaving it for now
766 return ()
767
768 ForAllPred _ theta head -> check_quant_pred env dflags ctxt pred theta head
769 IrredPred {} -> check_irred_pred under_syn env dflags ctxt pred
770
771 check_eq_pred :: TidyEnv -> DynFlags -> PredType -> TcM ()
772 check_eq_pred env dflags pred
773 = -- Equational constraints are valid in all contexts if type
774 -- families are permitted
775 checkTcM (xopt LangExt.TypeFamilies dflags
776 || xopt LangExt.GADTs dflags)
777 (eqPredTyErr env pred)
778
779 check_quant_pred :: TidyEnv -> DynFlags -> UserTypeCtxt
780 -> PredType -> ThetaType -> PredType -> TcM ()
781 check_quant_pred env dflags _ctxt pred theta head_pred
782 = addErrCtxt (text "In the quantified constraint" <+> quotes (ppr pred)) $
783 do { -- Check the instance head
784 case classifyPredType head_pred of
785 ClassPred cls tys -> checkValidInstHead SigmaCtxt cls tys
786 -- SigmaCtxt tells checkValidInstHead that
787 -- this is the head of a quantified constraint
788 IrredPred {} | hasTyVarHead head_pred
789 -> return ()
790 _ -> failWithTcM (badQuantHeadErr env pred)
791
792 -- Check for termination
793 ; unless (xopt LangExt.UndecidableInstances dflags) $
794 checkInstTermination theta head_pred
795 }
796
797 check_tuple_pred :: Bool -> TidyEnv -> DynFlags -> UserTypeCtxt -> PredType -> [PredType] -> TcM ()
798 check_tuple_pred under_syn env dflags ctxt pred ts
799 = do { -- See Note [ConstraintKinds in predicates]
800 checkTcM (under_syn || xopt LangExt.ConstraintKinds dflags)
801 (predTupleErr env pred)
802 ; mapM_ (check_pred_help under_syn env dflags ctxt) ts }
803 -- This case will not normally be executed because without
804 -- -XConstraintKinds tuple types are only kind-checked as *
805
806 check_irred_pred :: Bool -> TidyEnv -> DynFlags -> UserTypeCtxt -> PredType -> TcM ()
807 check_irred_pred under_syn env dflags ctxt pred
808 -- The predicate looks like (X t1 t2) or (x t1 t2) :: Constraint
809 -- where X is a type function
810 = do { -- If it looks like (x t1 t2), require ConstraintKinds
811 -- see Note [ConstraintKinds in predicates]
812 -- But (X t1 t2) is always ok because we just require ConstraintKinds
813 -- at the definition site (Trac #9838)
814 failIfTcM (not under_syn && not (xopt LangExt.ConstraintKinds dflags)
815 && hasTyVarHead pred)
816 (predIrredErr env pred)
817
818 -- Make sure it is OK to have an irred pred in this context
819 -- See Note [Irreducible predicates in superclasses]
820 ; failIfTcM (is_superclass ctxt
821 && not (xopt LangExt.UndecidableInstances dflags)
822 && has_tyfun_head pred)
823 (predSuperClassErr env pred) }
824 where
825 is_superclass ctxt = case ctxt of { ClassSCCtxt _ -> True; _ -> False }
826 has_tyfun_head ty
827 = case tcSplitTyConApp_maybe ty of
828 Just (tc, _) -> isTypeFamilyTyCon tc
829 Nothing -> False
830
831 {- Note [ConstraintKinds in predicates]
832 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
833 Don't check for -XConstraintKinds under a type synonym, because that
834 was done at the type synonym definition site; see Trac #9838
835 e.g. module A where
836 type C a = (Eq a, Ix a) -- Needs -XConstraintKinds
837 module B where
838 import A
839 f :: C a => a -> a -- Does *not* need -XConstraintKinds
840
841 Note [Irreducible predicates in superclasses]
842 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
843 Allowing type-family calls in class superclasses is somewhat dangerous
844 because we can write:
845
846 type family Fooish x :: * -> Constraint
847 type instance Fooish () = Foo
848 class Fooish () a => Foo a where
849
850 This will cause the constraint simplifier to loop because every time we canonicalise a
851 (Foo a) class constraint we add a (Fooish () a) constraint which will be immediately
852 solved to add+canonicalise another (Foo a) constraint. -}
853
854 -------------------------
855 check_class_pred :: TidyEnv -> DynFlags -> UserTypeCtxt
856 -> PredType -> Class -> [TcType] -> TcM ()
857 check_class_pred env dflags ctxt pred cls tys
858 | cls `hasKey` heqTyConKey -- (~) and (~~) are classified as classes,
859 || cls `hasKey` eqTyConKey -- but here we want to treat them as equalities
860 = -- pprTrace "check_class" (ppr cls) $
861 check_eq_pred env dflags pred
862
863 | isIPClass cls
864 = do { check_arity
865 ; checkTcM (okIPCtxt ctxt) (badIPPred env pred) }
866
867 | otherwise -- Includes Coercible
868 = do { check_arity
869 ; checkSimplifiableClassConstraint env dflags ctxt cls tys
870 ; checkTcM arg_tys_ok (predTyVarErr env pred) }
871 where
872 check_arity = checkTc (tys `lengthIs` classArity cls)
873 (tyConArityErr (classTyCon cls) tys)
874
875 -- Check the arguments of a class constraint
876 flexible_contexts = xopt LangExt.FlexibleContexts dflags
877 undecidable_ok = xopt LangExt.UndecidableInstances dflags
878 arg_tys_ok = case ctxt of
879 SpecInstCtxt -> True -- {-# SPECIALISE instance Eq (T Int) #-} is fine
880 InstDeclCtxt {} -> checkValidClsArgs (flexible_contexts || undecidable_ok) cls tys
881 -- Further checks on head and theta
882 -- in checkInstTermination
883 _ -> checkValidClsArgs flexible_contexts cls tys
884
885 checkSimplifiableClassConstraint :: TidyEnv -> DynFlags -> UserTypeCtxt
886 -> Class -> [TcType] -> TcM ()
887 -- See Note [Simplifiable given constraints]
888 checkSimplifiableClassConstraint env dflags ctxt cls tys
889 | not (wopt Opt_WarnSimplifiableClassConstraints dflags)
890 = return ()
891 | xopt LangExt.MonoLocalBinds dflags
892 = return ()
893
894 | DataTyCtxt {} <- ctxt -- Don't do this check for the "stupid theta"
895 = return () -- of a data type declaration
896
897 | cls `hasKey` coercibleTyConKey
898 = return () -- Oddly, we treat (Coercible t1 t2) as unconditionally OK
899 -- matchGlobalInst will reply "yes" because we can reduce
900 -- (Coercible a b) to (a ~R# b)
901
902 | otherwise
903 = do { result <- matchGlobalInst dflags False cls tys
904 ; case result of
905 OneInst { cir_what = what }
906 -> addWarnTc (Reason Opt_WarnSimplifiableClassConstraints)
907 (simplifiable_constraint_warn what)
908 _ -> return () }
909 where
910 pred = mkClassPred cls tys
911
912 simplifiable_constraint_warn :: InstanceWhat -> SDoc
913 simplifiable_constraint_warn what
914 = vcat [ hang (text "The constraint" <+> quotes (ppr (tidyType env pred))
915 <+> text "matches")
916 2 (ppr_what what)
917 , hang (text "This makes type inference for inner bindings fragile;")
918 2 (text "either use MonoLocalBinds, or simplify it using the instance") ]
919
920 ppr_what BuiltinInstance = text "a built-in instance"
921 ppr_what LocalInstance = text "a locally-quantified instance"
922 ppr_what (TopLevInstance { iw_dfun_id = dfun })
923 = hang (text "instance" <+> pprSigmaType (idType dfun))
924 2 (text "--" <+> pprDefinedAt (idName dfun))
925
926
927 {- Note [Simplifiable given constraints]
928 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
929 A type signature like
930 f :: Eq [(a,b)] => a -> b
931 is very fragile, for reasons described at length in TcInteract
932 Note [Instance and Given overlap]. As that Note discusses, for the
933 most part the clever stuff in TcInteract means that we don't use a
934 top-level instance if a local Given might fire, so there is no
935 fragility. But if we /infer/ the type of a local let-binding, things
936 can go wrong (Trac #11948 is an example, discussed in the Note).
937
938 So this warning is switched on only if we have NoMonoLocalBinds; in
939 that case the warning discourages users from writing simplifiable
940 class constraints.
941
942 The warning only fires if the constraint in the signature
943 matches the top-level instances in only one way, and with no
944 unifiers -- that is, under the same circumstances that
945 TcInteract.matchInstEnv fires an interaction with the top
946 level instances. For example (Trac #13526), consider
947
948 instance {-# OVERLAPPABLE #-} Eq (T a) where ...
949 instance Eq (T Char) where ..
950 f :: Eq (T a) => ...
951
952 We don't want to complain about this, even though the context
953 (Eq (T a)) matches an instance, because the user may be
954 deliberately deferring the choice so that the Eq (T Char)
955 has a chance to fire when 'f' is called. And the fragility
956 only matters when there's a risk that the instance might
957 fire instead of the local 'given'; and there is no such
958 risk in this case. Just use the same rules as for instance
959 firing!
960 -}
961
962 -------------------------
963 okIPCtxt :: UserTypeCtxt -> Bool
964 -- See Note [Implicit parameters in instance decls]
965 okIPCtxt (FunSigCtxt {}) = True
966 okIPCtxt (InfSigCtxt {}) = True
967 okIPCtxt ExprSigCtxt = True
968 okIPCtxt TypeAppCtxt = True
969 okIPCtxt PatSigCtxt = True
970 okIPCtxt ResSigCtxt = True
971 okIPCtxt GenSigCtxt = True
972 okIPCtxt (ConArgCtxt {}) = True
973 okIPCtxt (ForSigCtxt {}) = True -- ??
974 okIPCtxt ThBrackCtxt = True
975 okIPCtxt GhciCtxt = True
976 okIPCtxt SigmaCtxt = True
977 okIPCtxt (DataTyCtxt {}) = True
978 okIPCtxt (PatSynCtxt {}) = True
979 okIPCtxt (TySynCtxt {}) = True -- e.g. type Blah = ?x::Int
980 -- Trac #11466
981
982 okIPCtxt (KindSigCtxt {}) = False
983 okIPCtxt (ClassSCCtxt {}) = False
984 okIPCtxt (InstDeclCtxt {}) = False
985 okIPCtxt (SpecInstCtxt {}) = False
986 okIPCtxt (RuleSigCtxt {}) = False
987 okIPCtxt DefaultDeclCtxt = False
988 okIPCtxt DerivClauseCtxt = False
989 okIPCtxt (TyVarBndrKindCtxt {}) = False
990 okIPCtxt (DataKindCtxt {}) = False
991 okIPCtxt (TySynKindCtxt {}) = False
992 okIPCtxt (TyFamResKindCtxt {}) = False
993
994 {-
995 Note [Kind polymorphic type classes]
996 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
997 MultiParam check:
998
999 class C f where... -- C :: forall k. k -> Constraint
1000 instance C Maybe where...
1001
1002 The dictionary gets type [C * Maybe] even if it's not a MultiParam
1003 type class.
1004
1005 Flexibility check:
1006
1007 class C f where... -- C :: forall k. k -> Constraint
1008 data D a = D a
1009 instance C D where
1010
1011 The dictionary gets type [C * (D *)]. IA0_TODO it should be
1012 generalized actually.
1013 -}
1014
1015 checkThetaCtxt :: UserTypeCtxt -> ThetaType -> TidyEnv -> TcM (TidyEnv, SDoc)
1016 checkThetaCtxt ctxt theta env
1017 = return ( env
1018 , vcat [ text "In the context:" <+> pprTheta (tidyTypes env theta)
1019 , text "While checking" <+> pprUserTypeCtxt ctxt ] )
1020
1021 eqPredTyErr, predTupleErr, predIrredErr,
1022 predSuperClassErr, badQuantHeadErr :: TidyEnv -> PredType -> (TidyEnv, SDoc)
1023 badQuantHeadErr env pred
1024 = ( env
1025 , hang (text "Quantified predicate must have a class or type variable head:")
1026 2 (ppr_tidy env pred) )
1027 eqPredTyErr env pred
1028 = ( env
1029 , text "Illegal equational constraint" <+> ppr_tidy env pred $$
1030 parens (text "Use GADTs or TypeFamilies to permit this") )
1031 predTupleErr env pred
1032 = ( env
1033 , hang (text "Illegal tuple constraint:" <+> ppr_tidy env pred)
1034 2 (parens constraintKindsMsg) )
1035 predIrredErr env pred
1036 = ( env
1037 , hang (text "Illegal constraint:" <+> ppr_tidy env pred)
1038 2 (parens constraintKindsMsg) )
1039 predSuperClassErr env pred
1040 = ( env
1041 , hang (text "Illegal constraint" <+> quotes (ppr_tidy env pred)
1042 <+> text "in a superclass context")
1043 2 (parens undecidableMsg) )
1044
1045 predTyVarErr :: TidyEnv -> PredType -> (TidyEnv, SDoc)
1046 predTyVarErr env pred
1047 = (env
1048 , vcat [ hang (text "Non type-variable argument")
1049 2 (text "in the constraint:" <+> ppr_tidy env pred)
1050 , parens (text "Use FlexibleContexts to permit this") ])
1051
1052 badIPPred :: TidyEnv -> PredType -> (TidyEnv, SDoc)
1053 badIPPred env pred
1054 = ( env
1055 , text "Illegal implicit parameter" <+> quotes (ppr_tidy env pred) )
1056
1057 constraintSynErr :: TidyEnv -> Type -> (TidyEnv, SDoc)
1058 constraintSynErr env kind
1059 = ( env
1060 , hang (text "Illegal constraint synonym of kind:" <+> quotes (ppr_tidy env kind))
1061 2 (parens constraintKindsMsg) )
1062
1063 dupPredWarn :: TidyEnv -> [NE.NonEmpty PredType] -> (TidyEnv, SDoc)
1064 dupPredWarn env dups
1065 = ( env
1066 , text "Duplicate constraint" <> plural primaryDups <> text ":"
1067 <+> pprWithCommas (ppr_tidy env) primaryDups )
1068 where
1069 primaryDups = map NE.head dups
1070
1071 tyConArityErr :: TyCon -> [TcType] -> SDoc
1072 -- For type-constructor arity errors, be careful to report
1073 -- the number of /visible/ arguments required and supplied,
1074 -- ignoring the /invisible/ arguments, which the user does not see.
1075 -- (e.g. Trac #10516)
1076 tyConArityErr tc tks
1077 = arityErr (ppr (tyConFlavour tc)) (tyConName tc)
1078 tc_type_arity tc_type_args
1079 where
1080 vis_tks = filterOutInvisibleTypes tc tks
1081
1082 -- tc_type_arity = number of *type* args expected
1083 -- tc_type_args = number of *type* args encountered
1084 tc_type_arity = count isVisibleTyConBinder (tyConBinders tc)
1085 tc_type_args = length vis_tks
1086
1087 arityErr :: Outputable a => SDoc -> a -> Int -> Int -> SDoc
1088 arityErr what name n m
1089 = hsep [ text "The" <+> what, quotes (ppr name), text "should have",
1090 n_arguments <> comma, text "but has been given",
1091 if m==0 then text "none" else int m]
1092 where
1093 n_arguments | n == 0 = text "no arguments"
1094 | n == 1 = text "1 argument"
1095 | True = hsep [int n, text "arguments"]
1096
1097 {-
1098 ************************************************************************
1099 * *
1100 \subsection{Checking for a decent instance head type}
1101 * *
1102 ************************************************************************
1103
1104 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1105 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1106
1107 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1108 flag is on, or (2)~the instance is imported (they must have been
1109 compiled elsewhere). In these cases, we let them go through anyway.
1110
1111 We can also have instances for functions: @instance Foo (a -> b) ...@.
1112 -}
1113
1114 checkValidInstHead :: UserTypeCtxt -> Class -> [Type] -> TcM ()
1115 checkValidInstHead ctxt clas cls_args
1116 = do { dflags <- getDynFlags
1117 ; this_mod <- getModule
1118 ; is_boot <- tcIsHsBootOrSig
1119 ; check_valid_inst_head dflags this_mod is_boot ctxt clas cls_args }
1120
1121 check_valid_inst_head :: DynFlags -> Module -> Bool
1122 -> UserTypeCtxt -> Class -> [Type] -> TcM ()
1123 -- Wow! There are a surprising number of ad-hoc special cases here.
1124 check_valid_inst_head dflags this_mod is_boot ctxt clas cls_args
1125
1126 -- If not in an hs-boot file, abstract classes cannot have instances
1127 | isAbstractClass clas
1128 , not is_boot
1129 = failWithTc abstract_class_msg
1130
1131 -- For Typeable, don't complain about instances for
1132 -- standalone deriving; they are no-ops, and we warn about
1133 -- it in TcDeriv.deriveStandalone
1134 | clas_nm == typeableClassName
1135 , hand_written_bindings
1136 = failWithTc rejected_class_msg
1137
1138 -- Handwritten instances of KnownNat/KnownSymbol class
1139 -- are always forbidden (#12837)
1140 | clas_nm `elem` [ knownNatClassName, knownSymbolClassName ]
1141 , hand_written_bindings
1142 = failWithTc rejected_class_msg
1143
1144 -- For the most part we don't allow instances for Coercible;
1145 -- but we DO want to allow them in quantified constraints:
1146 -- f :: (forall a b. Coercible a b => Coercible (m a) (m b)) => ...m...
1147 | clas_nm == coercibleTyConName
1148 , not quantified_constraint
1149 = failWithTc rejected_class_msg
1150
1151 -- Handwritten instances of other nonminal-equality classes
1152 -- is forbidden, except in the defining module to allow
1153 -- instance a ~~ b => a ~ b
1154 -- which occurs in Data.Type.Equality
1155 | clas_nm `elem` [ heqTyConName, eqTyConName]
1156 , nameModule clas_nm /= this_mod
1157 = failWithTc rejected_class_msg
1158
1159 -- Check for hand-written Generic instances (disallowed in Safe Haskell)
1160 | clas_nm `elem` genericClassNames
1161 , hand_written_bindings
1162 = do { failIfTc (safeLanguageOn dflags) gen_inst_err
1163 ; when (safeInferOn dflags) (recordUnsafeInfer emptyBag) }
1164
1165 | clas_nm == hasFieldClassName
1166 = checkHasFieldInst clas cls_args
1167
1168 | isCTupleClass clas
1169 = failWithTc tuple_class_msg
1170
1171 -- Check language restrictions on the args to the class
1172 | check_h98_arg_shape
1173 , Just msg <- mb_ty_args_msg
1174 = failWithTc (instTypeErr clas cls_args msg)
1175
1176 | otherwise
1177 = mapM_ checkValidTypePat ty_args
1178 where
1179 clas_nm = getName clas
1180 ty_args = filterOutInvisibleTypes (classTyCon clas) cls_args
1181
1182 hand_written_bindings
1183 = case ctxt of
1184 InstDeclCtxt stand_alone -> not stand_alone
1185 SpecInstCtxt -> False
1186 DerivClauseCtxt -> False
1187 _ -> True
1188
1189 check_h98_arg_shape = case ctxt of
1190 SpecInstCtxt -> False
1191 DerivClauseCtxt -> False
1192 SigmaCtxt -> False
1193 _ -> True
1194 -- SigmaCtxt: once we are in quantified-constraint land, we
1195 -- aren't so picky about enforcing H98-language restrictions
1196 -- E.g. we want to allow a head like Coercible (m a) (m b)
1197
1198
1199 -- When we are looking at the head of a quantified constraint,
1200 -- check_quant_pred sets ctxt to SigmaCtxt
1201 quantified_constraint = case ctxt of
1202 SigmaCtxt -> True
1203 _ -> False
1204
1205 head_type_synonym_msg = parens (
1206 text "All instance types must be of the form (T t1 ... tn)" $$
1207 text "where T is not a synonym." $$
1208 text "Use TypeSynonymInstances if you want to disable this.")
1209
1210 head_type_args_tyvars_msg = parens (vcat [
1211 text "All instance types must be of the form (T a1 ... an)",
1212 text "where a1 ... an are *distinct type variables*,",
1213 text "and each type variable appears at most once in the instance head.",
1214 text "Use FlexibleInstances if you want to disable this."])
1215
1216 head_one_type_msg = parens $
1217 text "Only one type can be given in an instance head." $$
1218 text "Use MultiParamTypeClasses if you want to allow more, or zero."
1219
1220 rejected_class_msg = text "Class" <+> quotes (ppr clas_nm)
1221 <+> text "does not support user-specified instances"
1222 tuple_class_msg = text "You can't specify an instance for a tuple constraint"
1223
1224 gen_inst_err = rejected_class_msg $$ nest 2 (text "(in Safe Haskell)")
1225
1226 abstract_class_msg = text "Cannot define instance for abstract class"
1227 <+> quotes (ppr clas_nm)
1228
1229 mb_ty_args_msg
1230 | not (xopt LangExt.TypeSynonymInstances dflags)
1231 , not (all tcInstHeadTyNotSynonym ty_args)
1232 = Just head_type_synonym_msg
1233
1234 | not (xopt LangExt.FlexibleInstances dflags)
1235 , not (all tcInstHeadTyAppAllTyVars ty_args)
1236 = Just head_type_args_tyvars_msg
1237
1238 | length ty_args /= 1
1239 , not (xopt LangExt.MultiParamTypeClasses dflags)
1240 , not (xopt LangExt.NullaryTypeClasses dflags && null ty_args)
1241 = Just head_one_type_msg
1242
1243 | otherwise
1244 = Nothing
1245
1246 tcInstHeadTyNotSynonym :: Type -> Bool
1247 -- Used in Haskell-98 mode, for the argument types of an instance head
1248 -- These must not be type synonyms, but everywhere else type synonyms
1249 -- are transparent, so we need a special function here
1250 tcInstHeadTyNotSynonym ty
1251 = case ty of -- Do not use splitTyConApp,
1252 -- because that expands synonyms!
1253 TyConApp tc _ -> not (isTypeSynonymTyCon tc)
1254 _ -> True
1255
1256 tcInstHeadTyAppAllTyVars :: Type -> Bool
1257 -- Used in Haskell-98 mode, for the argument types of an instance head
1258 -- These must be a constructor applied to type variable arguments
1259 -- or a type-level literal.
1260 -- But we allow kind instantiations.
1261 tcInstHeadTyAppAllTyVars ty
1262 | Just (tc, tys) <- tcSplitTyConApp_maybe (dropCasts ty)
1263 = ok (filterOutInvisibleTypes tc tys) -- avoid kinds
1264 | LitTy _ <- ty = True -- accept type literals (Trac #13833)
1265 | otherwise
1266 = False
1267 where
1268 -- Check that all the types are type variables,
1269 -- and that each is distinct
1270 ok tys = equalLength tvs tys && hasNoDups tvs
1271 where
1272 tvs = mapMaybe tcGetTyVar_maybe tys
1273
1274 dropCasts :: Type -> Type
1275 -- See Note [Casts during validity checking]
1276 -- This function can turn a well-kinded type into an ill-kinded
1277 -- one, so I've kept it local to this module
1278 -- To consider: drop only HoleCo casts
1279 dropCasts (CastTy ty _) = dropCasts ty
1280 dropCasts (AppTy t1 t2) = mkAppTy (dropCasts t1) (dropCasts t2)
1281 dropCasts (FunTy t1 t2) = mkFunTy (dropCasts t1) (dropCasts t2)
1282 dropCasts (TyConApp tc tys) = mkTyConApp tc (map dropCasts tys)
1283 dropCasts (ForAllTy b ty) = ForAllTy (dropCastsB b) (dropCasts ty)
1284 dropCasts ty = ty -- LitTy, TyVarTy, CoercionTy
1285
1286 dropCastsB :: TyVarBinder -> TyVarBinder
1287 dropCastsB b = b -- Don't bother in the kind of a forall
1288
1289 instTypeErr :: Class -> [Type] -> SDoc -> SDoc
1290 instTypeErr cls tys msg
1291 = hang (hang (text "Illegal instance declaration for")
1292 2 (quotes (pprClassPred cls tys)))
1293 2 msg
1294
1295 -- | See Note [Validity checking of HasField instances]
1296 checkHasFieldInst :: Class -> [Type] -> TcM ()
1297 checkHasFieldInst cls tys@[_k_ty, x_ty, r_ty, _a_ty] =
1298 case splitTyConApp_maybe r_ty of
1299 Nothing -> whoops (text "Record data type must be specified")
1300 Just (tc, _)
1301 | isFamilyTyCon tc
1302 -> whoops (text "Record data type may not be a data family")
1303 | otherwise -> case isStrLitTy x_ty of
1304 Just lbl
1305 | isJust (lookupTyConFieldLabel lbl tc)
1306 -> whoops (ppr tc <+> text "already has a field"
1307 <+> quotes (ppr lbl))
1308 | otherwise -> return ()
1309 Nothing
1310 | null (tyConFieldLabels tc) -> return ()
1311 | otherwise -> whoops (ppr tc <+> text "has fields")
1312 where
1313 whoops = addErrTc . instTypeErr cls tys
1314 checkHasFieldInst _ tys = pprPanic "checkHasFieldInst" (ppr tys)
1315
1316 {- Note [Casts during validity checking]
1317 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1318 Consider the (bogus)
1319 instance Eq Char#
1320 We elaborate to 'Eq (Char# |> UnivCo(hole))' where the hole is an
1321 insoluble equality constraint for * ~ #. We'll report the insoluble
1322 constraint separately, but we don't want to *also* complain that Eq is
1323 not applied to a type constructor. So we look gaily look through
1324 CastTys here.
1325
1326 Another example: Eq (Either a). Then we actually get a cast in
1327 the middle:
1328 Eq ((Either |> g) a)
1329
1330
1331 Note [Validity checking of HasField instances]
1332 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1333 The HasField class has magic constraint solving behaviour (see Note
1334 [HasField instances] in TcInteract). However, we permit users to
1335 declare their own instances, provided they do not clash with the
1336 built-in behaviour. In particular, we forbid:
1337
1338 1. `HasField _ r _` where r is a variable
1339
1340 2. `HasField _ (T ...) _` if T is a data family
1341 (because it might have fields introduced later)
1342
1343 3. `HasField x (T ...) _` where x is a variable,
1344 if T has any fields at all
1345
1346 4. `HasField "foo" (T ...) _` if T has a "foo" field
1347
1348 The usual functional dependency checks also apply.
1349
1350
1351 Note [Valid 'deriving' predicate]
1352 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1353 validDerivPred checks for OK 'deriving' context. See Note [Exotic
1354 derived instance contexts] in TcDeriv. However the predicate is
1355 here because it uses sizeTypes, fvTypes.
1356
1357 It checks for three things
1358
1359 * No repeated variables (hasNoDups fvs)
1360
1361 * No type constructors. This is done by comparing
1362 sizeTypes tys == length (fvTypes tys)
1363 sizeTypes counts variables and constructors; fvTypes returns variables.
1364 So if they are the same, there must be no constructors. But there
1365 might be applications thus (f (g x)).
1366
1367 Note that tys only includes the visible arguments of the class type
1368 constructor. Including the non-visible arguments can cause the following,
1369 perfectly valid instance to be rejected:
1370 class Category (cat :: k -> k -> *) where ...
1371 newtype T (c :: * -> * -> *) a b = MkT (c a b)
1372 instance Category c => Category (T c) where ...
1373 since the first argument to Category is a non-visible *, which sizeTypes
1374 would count as a constructor! See Trac #11833.
1375
1376 * Also check for a bizarre corner case, when the derived instance decl
1377 would look like
1378 instance C a b => D (T a) where ...
1379 Note that 'b' isn't a parameter of T. This gives rise to all sorts of
1380 problems; in particular, it's hard to compare solutions for equality
1381 when finding the fixpoint, and that means the inferContext loop does
1382 not converge. See Trac #5287.
1383
1384 Note [Equality class instances]
1385 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1386 We can't have users writing instances for the equality classes. But we
1387 still need to be able to write instances for them ourselves. So we allow
1388 instances only in the defining module.
1389
1390 -}
1391
1392 validDerivPred :: TyVarSet -> PredType -> Bool
1393 -- See Note [Valid 'deriving' predicate]
1394 validDerivPred tv_set pred
1395 = case classifyPredType pred of
1396 ClassPred cls tys -> cls `hasKey` typeableClassKey
1397 -- Typeable constraints are bigger than they appear due
1398 -- to kind polymorphism, but that's OK
1399 || check_tys cls tys
1400 EqPred {} -> False -- reject equality constraints
1401 _ -> True -- Non-class predicates are ok
1402 where
1403 check_tys cls tys
1404 = hasNoDups fvs
1405 -- use sizePred to ignore implicit args
1406 && lengthIs fvs (sizePred pred)
1407 && all (`elemVarSet` tv_set) fvs
1408 where tys' = filterOutInvisibleTypes (classTyCon cls) tys
1409 fvs = fvTypes tys'
1410
1411 {-
1412 ************************************************************************
1413 * *
1414 \subsection{Checking instance for termination}
1415 * *
1416 ************************************************************************
1417 -}
1418
1419 {- Note [Instances and constraint synonyms]
1420 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1421 Currently, we don't allow instances for constraint synonyms at all.
1422 Consider these (Trac #13267):
1423 type C1 a = Show (a -> Bool)
1424 instance C1 Int where -- I1
1425 show _ = "ur"
1426
1427 This elicits "show is not a (visible) method of class C1", which isn't
1428 a great message. But it comes from the renamer, so it's hard to improve.
1429
1430 This needs a bit more care:
1431 type C2 a = (Show a, Show Int)
1432 instance C2 Int -- I2
1433
1434 If we use (splitTyConApp_maybe tau) in checkValidInstance to decompose
1435 the instance head, we'll expand the synonym on fly, and it'll look like
1436 instance (%,%) (Show Int, Show Int)
1437 and we /really/ don't want that. So we carefully do /not/ expand
1438 synonyms, by matching on TyConApp directly.
1439 -}
1440
1441 checkValidInstance :: UserTypeCtxt -> LHsSigType GhcRn -> Type
1442 -> TcM ([TyVar], ThetaType, Class, [Type])
1443 checkValidInstance ctxt hs_type ty
1444 | not is_tc_app
1445 = failWithTc (hang (text "Instance head is not headed by a class:")
1446 2 ( ppr tau))
1447
1448 | isNothing mb_cls
1449 = failWithTc (vcat [ text "Illegal instance for a" <+> ppr (tyConFlavour tc)
1450 , text "A class instance must be for a class" ])
1451
1452 | not arity_ok
1453 = failWithTc (text "Arity mis-match in instance head")
1454
1455 | otherwise
1456 = do { setSrcSpan head_loc $
1457 checkValidInstHead ctxt clas inst_tys
1458
1459 ; traceTc "checkValidInstance {" (ppr ty)
1460
1461 ; env0 <- tcInitTidyEnv
1462 ; check_valid_theta env0 ctxt theta
1463
1464 -- The Termination and Coverate Conditions
1465 -- Check that instance inference will terminate (if we care)
1466 -- For Haskell 98 this will already have been done by checkValidTheta,
1467 -- but as we may be using other extensions we need to check.
1468 --
1469 -- Note that the Termination Condition is *more conservative* than
1470 -- the checkAmbiguity test we do on other type signatures
1471 -- e.g. Bar a => Bar Int is ambiguous, but it also fails
1472 -- the termination condition, because 'a' appears more often
1473 -- in the constraint than in the head
1474 ; undecidable_ok <- xoptM LangExt.UndecidableInstances
1475 ; if undecidable_ok
1476 then checkAmbiguity ctxt ty
1477 else checkInstTermination theta tau
1478
1479 ; traceTc "cvi 2" (ppr ty)
1480
1481 ; case (checkInstCoverage undecidable_ok clas theta inst_tys) of
1482 IsValid -> return () -- Check succeeded
1483 NotValid msg -> addErrTc (instTypeErr clas inst_tys msg)
1484
1485 ; traceTc "End checkValidInstance }" empty
1486
1487 ; return (tvs, theta, clas, inst_tys) }
1488 where
1489 (tvs, theta, tau) = tcSplitSigmaTy ty
1490 is_tc_app = case tau of { TyConApp {} -> True; _ -> False }
1491 TyConApp tc inst_tys = tau -- See Note [Instances and constraint synonyms]
1492 mb_cls = tyConClass_maybe tc
1493 Just clas = mb_cls
1494 arity_ok = inst_tys `lengthIs` classArity clas
1495
1496 -- The location of the "head" of the instance
1497 head_loc = getLoc (getLHsInstDeclHead hs_type)
1498
1499 {-
1500 Note [Paterson conditions]
1501 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1502 Termination test: the so-called "Paterson conditions" (see Section 5 of
1503 "Understanding functional dependencies via Constraint Handling Rules,
1504 JFP Jan 2007).
1505
1506 We check that each assertion in the context satisfies:
1507 (1) no variable has more occurrences in the assertion than in the head, and
1508 (2) the assertion has fewer constructors and variables (taken together
1509 and counting repetitions) than the head.
1510 This is only needed with -fglasgow-exts, as Haskell 98 restrictions
1511 (which have already been checked) guarantee termination.
1512
1513 The underlying idea is that
1514
1515 for any ground substitution, each assertion in the
1516 context has fewer type constructors than the head.
1517 -}
1518
1519 checkInstTermination :: ThetaType -> TcPredType -> TcM ()
1520 -- See Note [Paterson conditions]
1521 checkInstTermination theta head_pred
1522 = check_preds emptyVarSet theta
1523 where
1524 head_fvs = fvType head_pred
1525 head_size = sizeType head_pred
1526
1527 check_preds :: VarSet -> [PredType] -> TcM ()
1528 check_preds foralld_tvs preds = mapM_ (check foralld_tvs) preds
1529
1530 check :: VarSet -> PredType -> TcM ()
1531 check foralld_tvs pred
1532 = case classifyPredType pred of
1533 EqPred {} -> return () -- See Trac #4200.
1534 IrredPred {} -> check2 foralld_tvs pred (sizeType pred)
1535 ClassPred cls tys
1536 | isTerminatingClass cls
1537 -> return ()
1538
1539 | isCTupleClass cls -- Look inside tuple predicates; Trac #8359
1540 -> check_preds foralld_tvs tys
1541
1542 | otherwise -- Other ClassPreds
1543 -> check2 foralld_tvs pred bogus_size
1544 where
1545 bogus_size = 1 + sizeTypes (filterOutInvisibleTypes (classTyCon cls) tys)
1546 -- See Note [Invisible arguments and termination]
1547
1548 ForAllPred tvs _ head_pred'
1549 -> check (foralld_tvs `extendVarSetList` binderVars tvs) head_pred'
1550 -- Termination of the quantified predicate itself is checked
1551 -- when the predicates are individually checked for validity
1552
1553 check2 foralld_tvs pred pred_size
1554 | not (null bad_tvs) = failWithTc (noMoreMsg bad_tvs what (ppr head_pred))
1555 | not (isTyFamFree pred) = failWithTc (nestedMsg what)
1556 | pred_size >= head_size = failWithTc (smallerMsg what (ppr head_pred))
1557 | otherwise = return ()
1558 -- isTyFamFree: see Note [Type families in instance contexts]
1559 where
1560 what = text "constraint" <+> quotes (ppr pred)
1561 bad_tvs = filterOut (`elemVarSet` foralld_tvs) (fvType pred)
1562 \\ head_fvs
1563
1564 smallerMsg :: SDoc -> SDoc -> SDoc
1565 smallerMsg what inst_head
1566 = vcat [ hang (text "The" <+> what)
1567 2 (sep [ text "is no smaller than"
1568 , text "the instance head" <+> quotes inst_head ])
1569 , parens undecidableMsg ]
1570
1571 noMoreMsg :: [TcTyVar] -> SDoc -> SDoc -> SDoc
1572 noMoreMsg tvs what inst_head
1573 = vcat [ hang (text "Variable" <> plural tvs <+> quotes (pprWithCommas ppr tvs)
1574 <+> occurs <+> text "more often")
1575 2 (sep [ text "in the" <+> what
1576 , text "than in the instance head" <+> quotes inst_head ])
1577 , parens undecidableMsg ]
1578 where
1579 occurs = if isSingleton tvs then text "occurs"
1580 else text "occur"
1581
1582 undecidableMsg, constraintKindsMsg :: SDoc
1583 undecidableMsg = text "Use UndecidableInstances to permit this"
1584 constraintKindsMsg = text "Use ConstraintKinds to permit this"
1585
1586 {- Note [Type families in instance contexts]
1587 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1588 Are these OK?
1589 type family F a
1590 instance F a => C (Maybe [a]) where ...
1591 intance C (F a) => C [[[a]]] where ...
1592
1593 No: the type family in the instance head might blow up to an
1594 arbitrarily large type, depending on how 'a' is instantiated.
1595 So we require UndecidableInstances if we have a type family
1596 in the instance head. Trac #15172.
1597
1598 Note [Associated type instances]
1599 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1600 We allow this:
1601 class C a where
1602 type T x a
1603 instance C Int where
1604 type T (S y) Int = y
1605 type T Z Int = Char
1606
1607 Note that
1608 a) The variable 'x' is not bound by the class decl
1609 b) 'x' is instantiated to a non-type-variable in the instance
1610 c) There are several type instance decls for T in the instance
1611
1612 All this is fine. Of course, you can't give any *more* instances
1613 for (T ty Int) elsewhere, because it's an *associated* type.
1614
1615 Note [Checking consistent instantiation]
1616 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1617 See Trac #11450 for background discussion on this check.
1618
1619 class C a b where
1620 type T a x b
1621
1622 With this class decl, if we have an instance decl
1623 instance C ty1 ty2 where ...
1624 then the type instance must look like
1625 type T ty1 v ty2 = ...
1626 with exactly 'ty1' for 'a', 'ty2' for 'b', and some type 'v' for 'x'.
1627 For example:
1628
1629 instance C [p] Int
1630 type T [p] y Int = (p,y,y)
1631
1632 Note that
1633
1634 * We used to allow completely different bound variables in the
1635 associated type instance; e.g.
1636 instance C [p] Int
1637 type T [q] y Int = ...
1638 But from GHC 8.2 onwards, we don't. It's much simpler this way.
1639 See Trac #11450.
1640
1641 * When the class variable isn't used on the RHS of the type instance,
1642 it's tempting to allow wildcards, thus
1643 instance C [p] Int
1644 type T [_] y Int = (y,y)
1645 But it's awkward to do the test, and it doesn't work if the
1646 variable is repeated:
1647 instance C (p,p) Int
1648 type T (_,_) y Int = (y,y)
1649 Even though 'p' is not used on the RHS, we still need to use 'p'
1650 on the LHS to establish the repeated pattern. So to keep it simple
1651 we just require equality.
1652
1653 * For variables in associated type families that are not bound by the class
1654 itself, we do _not_ check if they are over-specific. In other words,
1655 it's perfectly acceptable to have an instance like this:
1656
1657 instance C [p] Int where
1658 type T [p] (Maybe x) Int = x
1659
1660 While the first and third arguments to T are required to be exactly [p] and
1661 Int, respectively, since they are bound by C, the second argument is allowed
1662 to be more specific than just a type variable. Furthermore, it is permissible
1663 to define multiple equations for T that differ only in the non-class-bound
1664 argument:
1665
1666 instance C [p] Int where
1667 type T [p] (Maybe x) Int = x
1668 type T [p] (Either x y) Int = x -> y
1669
1670 We once considered requiring that non-class-bound variables in associated
1671 type family instances be instantiated with distinct type variables. However,
1672 that requirement proved too restrictive in practice, as there were examples
1673 of extremely simple associated type family instances that this check would
1674 reject, and fixing them required tiresome boilerplate in the form of
1675 auxiliary type families. For instance, you would have to define the above
1676 example as:
1677
1678 instance C [p] Int where
1679 type T [p] x Int = CAux x
1680
1681 type family CAux x where
1682 CAux (Maybe x) = x
1683 CAux (Either x y) = x -> y
1684
1685 We decided that this restriction wasn't buying us much, so we opted not
1686 to pursue that design (see also GHC Trac #13398).
1687
1688 Implementation
1689 * Form the mini-envt from the class type variables a,b
1690 to the instance decl types [p],Int: [a->[p], b->Int]
1691
1692 * Look at the tyvars a,x,b of the type family constructor T
1693 (it shares tyvars with the class C)
1694
1695 * Apply the mini-evnt to them, and check that the result is
1696 consistent with the instance types [p] y Int. (where y can be any type, as
1697 it is not scoped over the class type variables.
1698
1699 We make all the instance type variables scope over the
1700 type instances, of course, which picks up non-obvious kinds. Eg
1701 class Foo (a :: k) where
1702 type F a
1703 instance Foo (b :: k -> k) where
1704 type F b = Int
1705 Here the instance is kind-indexed and really looks like
1706 type F (k->k) (b::k->k) = Int
1707 But if the 'b' didn't scope, we would make F's instance too
1708 poly-kinded.
1709
1710 Note [Invisible arguments and termination]
1711 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1712 When checking the ​Paterson conditions for termination an instance
1713 declaration, we check for the number of "constructors and variables"
1714 in the instance head and constraints. Question: Do we look at
1715
1716 * All the arguments, visible or invisible?
1717 * Just the visible arguments?
1718
1719 I think both will ensure termination, provided we are consistent.
1720 Currently we are /not/ consistent, which is really a bug. It's
1721 described in Trac #15177, which contains a number of examples.
1722 The suspicious bits are the calls to filterOutInvisibleTypes.
1723 -}
1724
1725 -- | Extra information about the parent instance declaration, needed
1726 -- when type-checking associated types. The 'Class' is the enclosing
1727 -- class, the [TyVar] are the type variable of the instance decl,
1728 -- and and the @VarEnv Type@ maps class variables to their instance
1729 -- types.
1730 type ClsInstInfo = (Class, [TyVar], VarEnv Type)
1731
1732 type AssocInstArgShape = (Maybe Type, Type)
1733 -- AssocInstArgShape is used only for associated family instances
1734 -- (mb_exp, actual)
1735 -- mb_exp = Just ty => this arg corresponds to a class variable
1736 -- = Nothing => it doesn't correspond to a class variable
1737 -- e.g. class C b where
1738 -- type F a b c
1739 -- instance C [x] where
1740 -- type F p [x] q
1741 -- We get [AssocInstArgShape] = [ (Nothing, p)
1742 -- , (Just [x], [x])
1743 -- , (Nothing, q)]
1744
1745 checkConsistentFamInst
1746 :: Maybe ClsInstInfo
1747 -> TyCon -- ^ Family tycon
1748 -> [Type] -- ^ Type patterns from instance
1749 -> SDoc -- ^ pretty-printed user-written instance head
1750 -> TcM ()
1751 -- See Note [Checking consistent instantiation]
1752
1753 checkConsistentFamInst Nothing _ _ _ = return ()
1754 checkConsistentFamInst (Just (clas, inst_tvs, mini_env)) fam_tc at_tys pp_hs_pats
1755 = do { -- Check that the associated type indeed comes from this class
1756 -- See [Mismatched class methods and associated type families]
1757 -- in TcInstDecls.
1758 checkTc (Just clas == tyConAssoc_maybe fam_tc)
1759 (badATErr (className clas) (tyConName fam_tc))
1760
1761 -- Check type args first (more comprehensible)
1762 ; checkTc (all check_arg type_shapes) pp_wrong_at_arg
1763
1764 -- And now kind args
1765 ; checkTcM (all check_arg kind_shapes)
1766 (tidy_env2, pp_wrong_at_arg $$ ppSuggestExplicitKinds)
1767
1768 ; traceTc "cfi" (vcat [ ppr inst_tvs
1769 , ppr arg_shapes
1770 , ppr mini_env ]) }
1771 where
1772 arg_shapes :: [AssocInstArgShape]
1773 arg_shapes = [ (lookupVarEnv mini_env fam_tc_tv, at_ty)
1774 | (fam_tc_tv, at_ty) <- tyConTyVars fam_tc `zip` at_tys ]
1775
1776 (kind_shapes, type_shapes) = partitionInvisibles fam_tc snd arg_shapes
1777
1778 check_arg :: AssocInstArgShape -> Bool
1779 check_arg (Just exp_ty, at_ty) = exp_ty `tcEqType` at_ty
1780 check_arg (Nothing, _ ) = True -- Arg position does not correspond
1781 -- to a class variable
1782
1783 pp_wrong_at_arg
1784 = vcat [ text "Type indexes must match class instance head"
1785 , pp_exp_act ]
1786
1787 pp_exp_act
1788 = vcat [ text "Expected:" <+> ppr (mkTyConApp fam_tc expected_args)
1789 , text " Actual:" <+> pp_hs_pats
1790 , sdocWithDynFlags $ \dflags ->
1791 ppWhen (has_poly_args dflags) $
1792 vcat [ text "where the `<tv>' arguments are type variables,"
1793 , text "distinct from each other and from the instance variables" ] ]
1794
1795 -- We need to tidy, since it's possible that expected_args will contain
1796 -- inferred kind variables with names identical to those in at_tys. If we
1797 -- don't, we'll end up with horrible messages like this one (#13972):
1798 --
1799 -- Expected: T (a -> Either a b)
1800 -- Actual: T (a -> Either a b)
1801 (tidy_env1, _) = tidyOpenTypes emptyTidyEnv at_tys
1802 (tidy_env2, expected_args)
1803 = tidyOpenTypes tidy_env1 [ exp_ty `orElse` mk_tv at_ty
1804 | (exp_ty, at_ty) <- arg_shapes ]
1805 mk_tv at_ty = mkTyVarTy (mkTyVar tv_name (typeKind at_ty))
1806 tv_name = mkInternalName (mkAlphaTyVarUnique 1) (mkTyVarOcc "<tv>") noSrcSpan
1807
1808 has_poly_args dflags = any (isNothing . fst) shapes
1809 where
1810 shapes | gopt Opt_PrintExplicitKinds dflags = arg_shapes
1811 | otherwise = type_shapes
1812
1813 badATErr :: Name -> Name -> SDoc
1814 badATErr clas op
1815 = hsep [text "Class", quotes (ppr clas),
1816 text "does not have an associated type", quotes (ppr op)]
1817
1818
1819 {-
1820 ************************************************************************
1821 * *
1822 Checking type instance well-formedness and termination
1823 * *
1824 ************************************************************************
1825 -}
1826
1827 checkValidCoAxiom :: CoAxiom Branched -> TcM ()
1828 checkValidCoAxiom ax@(CoAxiom { co_ax_tc = fam_tc, co_ax_branches = branches })
1829 = do { mapM_ (checkValidCoAxBranch Nothing fam_tc) branch_list
1830 ; foldlM_ check_branch_compat [] branch_list }
1831 where
1832 branch_list = fromBranches branches
1833 injectivity = tyConInjectivityInfo fam_tc
1834
1835 check_branch_compat :: [CoAxBranch] -- previous branches in reverse order
1836 -> CoAxBranch -- current branch
1837 -> TcM [CoAxBranch]-- current branch : previous branches
1838 -- Check for
1839 -- (a) this branch is dominated by previous ones
1840 -- (b) failure of injectivity
1841 check_branch_compat prev_branches cur_branch
1842 | cur_branch `isDominatedBy` prev_branches
1843 = do { addWarnAt NoReason (coAxBranchSpan cur_branch) $
1844 inaccessibleCoAxBranch ax cur_branch
1845 ; return prev_branches }
1846 | otherwise
1847 = do { check_injectivity prev_branches cur_branch
1848 ; return (cur_branch : prev_branches) }
1849
1850 -- Injectivity check: check whether a new (CoAxBranch) can extend
1851 -- already checked equations without violating injectivity
1852 -- annotation supplied by the user.
1853 -- See Note [Verifying injectivity annotation] in FamInstEnv
1854 check_injectivity prev_branches cur_branch
1855 | Injective inj <- injectivity
1856 = do { let conflicts =
1857 fst $ foldl (gather_conflicts inj prev_branches cur_branch)
1858 ([], 0) prev_branches
1859 ; mapM_ (\(err, span) -> setSrcSpan span $ addErr err)
1860 (makeInjectivityErrors ax cur_branch inj conflicts) }
1861 | otherwise
1862 = return ()
1863
1864 gather_conflicts inj prev_branches cur_branch (acc, n) branch
1865 -- n is 0-based index of branch in prev_branches
1866 = case injectiveBranches inj cur_branch branch of
1867 InjectivityUnified ax1 ax2
1868 | ax1 `isDominatedBy` (replace_br prev_branches n ax2)
1869 -> (acc, n + 1)
1870 | otherwise
1871 -> (branch : acc, n + 1)
1872 InjectivityAccepted -> (acc, n + 1)
1873
1874 -- Replace n-th element in the list. Assumes 0-based indexing.
1875 replace_br :: [CoAxBranch] -> Int -> CoAxBranch -> [CoAxBranch]
1876 replace_br brs n br = take n brs ++ [br] ++ drop (n+1) brs
1877
1878
1879 -- Check that a "type instance" is well-formed (which includes decidability
1880 -- unless -XUndecidableInstances is given).
1881 --
1882 checkValidCoAxBranch :: Maybe ClsInstInfo
1883 -> TyCon -> CoAxBranch -> TcM ()
1884 checkValidCoAxBranch mb_clsinfo fam_tc
1885 (CoAxBranch { cab_tvs = tvs, cab_cvs = cvs
1886 , cab_lhs = typats
1887 , cab_rhs = rhs, cab_loc = loc })
1888 = checkValidTyFamEqn mb_clsinfo fam_tc tvs cvs typats rhs pp_lhs loc
1889 where
1890 pp_lhs = ppr (mkTyConApp fam_tc typats)
1891
1892 -- | Do validity checks on a type family equation, including consistency
1893 -- with any enclosing class instance head, termination, and lack of
1894 -- polytypes.
1895 checkValidTyFamEqn :: Maybe ClsInstInfo
1896 -> TyCon -- ^ of the type family
1897 -> [TyVar] -- ^ bound tyvars in the equation
1898 -> [CoVar] -- ^ bound covars in the equation
1899 -> [Type] -- ^ type patterns
1900 -> Type -- ^ rhs
1901 -> SDoc -- ^ user-written LHS
1902 -> SrcSpan
1903 -> TcM ()
1904 checkValidTyFamEqn mb_clsinfo fam_tc tvs cvs typats rhs pp_lhs loc
1905 = setSrcSpan loc $
1906 do { checkValidFamPats mb_clsinfo fam_tc tvs cvs typats [] pp_lhs
1907
1908 -- The argument patterns, and RHS, are all boxed tau types
1909 -- E.g Reject type family F (a :: k1) :: k2
1910 -- type instance F (forall a. a->a) = ...
1911 -- type instance F Int# = ...
1912 -- type instance F Int = forall a. a->a
1913 -- type instance F Int = Int#
1914 -- See Trac #9357
1915 ; checkValidMonoType rhs
1916
1917 -- We have a decidable instance unless otherwise permitted
1918 ; undecidable_ok <- xoptM LangExt.UndecidableInstances
1919 ; traceTc "checkVTFE" (pp_lhs $$ ppr rhs $$ ppr (tcTyFamInsts rhs))
1920 ; unless undecidable_ok $
1921 mapM_ addErrTc (checkFamInstRhs fam_tc typats (tcTyFamInsts rhs)) }
1922
1923 -- Make sure that each type family application is
1924 -- (1) strictly smaller than the lhs,
1925 -- (2) mentions no type variable more often than the lhs, and
1926 -- (3) does not contain any further type family instances.
1927 --
1928 checkFamInstRhs :: TyCon -> [Type] -- LHS
1929 -> [(TyCon, [Type])] -- type family calls in RHS
1930 -> [MsgDoc]
1931 checkFamInstRhs tc lhsTys famInsts
1932 = mapMaybe check famInsts
1933 where
1934 lhs_size = sizeTyConAppArgs tc lhsTys
1935 fvs = fvTypes lhsTys
1936 check (tc, tys)
1937 | not (all isTyFamFree tys) = Just (nestedMsg what)
1938 | not (null bad_tvs) = Just (noMoreMsg bad_tvs what inst_head)
1939 | lhs_size <= fam_app_size = Just (smallerMsg what inst_head)
1940 | otherwise = Nothing
1941 where
1942 what = text "type family application"
1943 <+> quotes (pprType (TyConApp tc tys))
1944 inst_head = pprType (TyConApp tc lhsTys)
1945 bad_tvs = fvTypes tys \\ fvs
1946 fam_app_size = sizeTyConAppArgs tc tys
1947
1948 checkValidFamPats :: Maybe ClsInstInfo -> TyCon -> [TyVar] -> [CoVar]
1949 -> [Type] -- ^ patterns the user wrote
1950 -> [Type] -- ^ "extra" patterns from a data instance kind sig
1951 -> SDoc -- ^ pretty-printed user-written instance head
1952 -> TcM ()
1953 -- Patterns in a 'type instance' or 'data instance' decl should
1954 -- a) contain no type family applications
1955 -- (vanilla synonyms are fine, though)
1956 -- b) properly bind all their free type variables
1957 -- e.g. we disallow (Trac #7536)
1958 -- type T a = Int
1959 -- type instance F (T a) = a
1960 -- c) For associated types, are consistently instantiated
1961 checkValidFamPats mb_clsinfo fam_tc tvs cvs user_ty_pats extra_ty_pats pp_hs_pats
1962 = do { mapM_ checkValidTypePat user_ty_pats
1963
1964 ; let unbound_tcvs = filterOut (`elemVarSet` exactTyCoVarsOfTypes user_ty_pats)
1965 (tvs ++ cvs)
1966 ; checkTc (null unbound_tcvs) (famPatErr fam_tc unbound_tcvs user_ty_pats)
1967
1968 -- Check that type patterns match the class instance head
1969 ; checkConsistentFamInst mb_clsinfo fam_tc (user_ty_pats `chkAppend` extra_ty_pats) pp_hs_pats }
1970
1971 checkValidTypePat :: Type -> TcM ()
1972 -- Used for type patterns in class instances,
1973 -- and in type/data family instances
1974 checkValidTypePat pat_ty
1975 = do { -- Check that pat_ty is a monotype
1976 checkValidMonoType pat_ty
1977 -- One could imagine generalising to allow
1978 -- instance C (forall a. a->a)
1979 -- but we don't know what all the consequences might be
1980
1981 -- Ensure that no type family instances occur a type pattern
1982 ; checkTc (isTyFamFree pat_ty) $
1983 tyFamInstIllegalErr pat_ty }
1984
1985 -- Error messages
1986
1987 inaccessibleCoAxBranch :: CoAxiom br -> CoAxBranch -> SDoc
1988 inaccessibleCoAxBranch fi_ax cur_branch
1989 = text "Type family instance equation is overlapped:" $$
1990 nest 2 (pprCoAxBranch fi_ax cur_branch)
1991
1992 tyFamInstIllegalErr :: Type -> SDoc
1993 tyFamInstIllegalErr ty
1994 = hang (text "Illegal type synonym family application in instance" <>
1995 colon) 2 $
1996 ppr ty
1997
1998 nestedMsg :: SDoc -> SDoc
1999 nestedMsg what
2000 = sep [ text "Illegal nested" <+> what
2001 , parens undecidableMsg ]
2002
2003 famPatErr :: TyCon -> [TyVar] -> [Type] -> SDoc
2004 famPatErr fam_tc tvs pats
2005 = hang (text "Family instance purports to bind type variable" <> plural tvs
2006 <+> pprQuotedList tvs)
2007 2 (hang (text "but the real LHS (expanding synonyms) is:")
2008 2 (pprTypeApp fam_tc (map expandTypeSynonyms pats) <+>
2009 text "= ..."))
2010
2011 {-
2012 ************************************************************************
2013 * *
2014 Telescope checking
2015 * *
2016 ************************************************************************
2017
2018 Note [Bad telescopes]
2019 ~~~~~~~~~~~~~~~~~~~~~
2020 Now that we can mix type and kind variables, there are an awful lot of
2021 ways to shoot yourself in the foot. Here are some.
2022
2023 data SameKind :: k -> k -> * -- just to force unification
2024
2025 1. data T1 a k (b :: k) (x :: SameKind a b)
2026
2027 The problem here is that we discover that a and b should have the same
2028 kind. But this kind mentions k, which is bound *after* a.
2029 (Testcase: dependent/should_fail/BadTelescope)
2030
2031 2. data T2 a (c :: Proxy b) (d :: Proxy a) (x :: SameKind b d)
2032
2033 Note that b is not bound. Yet its kind mentions a. Because we have
2034 a nice rule that all implicitly bound variables come before others,
2035 this is bogus. (We could probably figure out to put b between a and c.
2036 But I think this is doing users a disservice, in the long run.)
2037 (Testcase: dependent/should_fail/BadTelescope4)
2038
2039 To catch these errors, we call checkValidTelescope during kind-checking
2040 datatype declarations. This must be done *before* kind-generalization,
2041 because kind-generalization might observe, say, T1, see that k is free
2042 in a's kind, and generalize over it, producing nonsense. It also must
2043 be done *after* kind-generalization, in order to catch the T2 case, which
2044 becomes apparent only after generalizing.
2045
2046 Note [Keeping scoped variables in order: Explicit] discusses how this
2047 check works for `forall x y z.` written in a type.
2048
2049 -}
2050
2051 -- | Check a list of binders to see if they make a valid telescope.
2052 -- The key property we're checking for is scoping. For example:
2053 -- > data SameKind :: k -> k -> *
2054 -- > data X a k (b :: k) (c :: SameKind a b)
2055 -- Kind inference says that a's kind should be k. But that's impossible,
2056 -- because k isn't in scope when a is bound. This check has to come before
2057 -- general validity checking, because once we kind-generalise, this sort
2058 -- of problem is harder to spot (as we'll generalise over the unbound
2059 -- k in a's type.) See also Note [Bad telescopes].
2060 checkValidTelescope :: [TyConBinder] -- explicit vars (zonked)
2061 -> SDoc -- original, user-written telescope
2062 -> SDoc -- extra text to print
2063 -> TcM ()
2064 checkValidTelescope tvbs user_tyvars extra
2065 = do { let tvs = binderVars tvbs
2066
2067 (_, sorted_tidied_tvs) = tidyTyCoVarBndrs emptyTidyEnv $
2068 toposortTyVars tvs
2069 ; unless (go [] emptyVarSet (binderVars tvbs)) $
2070 addErr $
2071 vcat [ hang (text "These kind and type variables:" <+> user_tyvars $$
2072 text "are out of dependency order. Perhaps try this ordering:")
2073 2 (pprTyVars sorted_tidied_tvs)
2074 , extra ] }
2075
2076 where
2077 go :: [TyVar] -- misplaced variables
2078 -> TyVarSet -> [TyVar] -> Bool
2079 go errs in_scope [] = null (filter (`elemVarSet` in_scope) errs)
2080 -- report an error only when the variable in the kind is brought
2081 -- into scope later in the telescope. Otherwise, we'll just quantify
2082 -- over it in kindGeneralize, as we should.
2083
2084 go errs in_scope (tv:tvs)
2085 = let bad_tvs = filterOut (`elemVarSet` in_scope) $
2086 tyCoVarsOfTypeList (tyVarKind tv)
2087 in go (bad_tvs ++ errs) (in_scope `extendVarSet` tv) tvs
2088
2089 {-
2090 ************************************************************************
2091 * *
2092 \subsection{Auxiliary functions}
2093 * *
2094 ************************************************************************
2095 -}
2096
2097 -- Free variables of a type, retaining repetitions, and expanding synonyms
2098 fvType :: Type -> [TyCoVar]
2099 fvType ty | Just exp_ty <- tcView ty = fvType exp_ty
2100 fvType (TyVarTy tv) = [tv]
2101 fvType (TyConApp _ tys) = fvTypes tys
2102 fvType (LitTy {}) = []
2103 fvType (AppTy fun arg) = fvType fun ++ fvType arg
2104 fvType (FunTy arg res) = fvType arg ++ fvType res
2105 fvType (ForAllTy (TvBndr tv _) ty)
2106 = fvType (tyVarKind tv) ++
2107 filter (/= tv) (fvType ty)
2108 fvType (CastTy ty co) = fvType ty ++ fvCo co
2109 fvType (CoercionTy co) = fvCo co
2110
2111 fvTypes :: [Type] -> [TyVar]
2112 fvTypes tys = concat (map fvType tys)
2113
2114 fvMCo :: MCoercion -> [TyCoVar]
2115 fvMCo MRefl = []
2116 fvMCo (MCo co) = fvCo co
2117
2118 fvCo :: Coercion -> [TyCoVar]
2119 fvCo (Refl ty) = fvType ty
2120 fvCo (GRefl _ ty mco) = fvType ty ++ fvMCo mco
2121 fvCo (TyConAppCo _ _ args) = concatMap fvCo args
2122 fvCo (AppCo co arg) = fvCo co ++ fvCo arg
2123 fvCo (ForAllCo tv h co) = filter (/= tv) (fvCo co) ++ fvCo h
2124 fvCo (FunCo _ co1 co2) = fvCo co1 ++ fvCo co2
2125 fvCo (CoVarCo v) = [v]
2126 fvCo (AxiomInstCo _ _ args) = concatMap fvCo args
2127 fvCo (UnivCo p _ t1 t2) = fvProv p ++ fvType t1 ++ fvType t2
2128 fvCo (SymCo co) = fvCo co
2129 fvCo (TransCo co1 co2) = fvCo co1 ++ fvCo co2
2130 fvCo (NthCo _ _ co) = fvCo co
2131 fvCo (LRCo _ co) = fvCo co
2132 fvCo (InstCo co arg) = fvCo co ++ fvCo arg
2133 fvCo (KindCo co) = fvCo co
2134 fvCo (SubCo co) = fvCo co
2135 fvCo (AxiomRuleCo _ cs) = concatMap fvCo cs
2136 fvCo (HoleCo h) = pprPanic "fvCo falls into a hole" (ppr h)
2137
2138 fvProv :: UnivCoProvenance -> [TyCoVar]
2139 fvProv UnsafeCoerceProv = []
2140 fvProv (PhantomProv co) = fvCo co
2141 fvProv (ProofIrrelProv co) = fvCo co
2142 fvProv (PluginProv _) = []
2143
2144 sizeType :: Type -> Int
2145 -- Size of a type: the number of variables and constructors
2146 sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty
2147 sizeType (TyVarTy {}) = 1
2148 sizeType (TyConApp tc tys) = 1 + sizeTyConAppArgs tc tys
2149 sizeType (LitTy {}) = 1
2150 sizeType (AppTy fun arg) = sizeType fun + sizeType arg
2151 sizeType (FunTy arg res) = sizeType arg + sizeType res + 1
2152 sizeType (ForAllTy _ ty) = sizeType ty
2153 sizeType (CastTy ty _) = sizeType ty
2154 sizeType (CoercionTy _) = 1
2155
2156 sizeTypes :: [Type] -> Int
2157 sizeTypes = foldr ((+) . sizeType) 0
2158
2159 sizeTyConAppArgs :: TyCon -> [Type] -> Int
2160 sizeTyConAppArgs _tc tys = sizeTypes tys -- (filterOutInvisibleTypes tc tys)
2161 -- See Note [Invisible arguments and termination]
2162
2163 -- Size of a predicate
2164 --
2165 -- We are considering whether class constraints terminate.
2166 -- Equality constraints and constraints for the implicit
2167 -- parameter class always terminate so it is safe to say "size 0".
2168 -- See Trac #4200.
2169 sizePred :: PredType -> Int
2170 sizePred ty = goClass ty
2171 where
2172 goClass p = go (classifyPredType p)
2173
2174 go (ClassPred cls tys')
2175 | isTerminatingClass cls = 0
2176 | otherwise = sizeTypes (filterOutInvisibleTypes (classTyCon cls) tys')
2177 -- The filtering looks bogus
2178 -- See Note [Invisible arguments and termination]
2179 go (EqPred {}) = 0
2180 go (IrredPred ty) = sizeType ty
2181 go (ForAllPred _ _ pred) = goClass pred
2182
2183 -- | When this says "True", ignore this class constraint during
2184 -- a termination check
2185 isTerminatingClass :: Class -> Bool
2186 isTerminatingClass cls
2187 = isIPClass cls -- Implicit parameter constraints always terminate because
2188 -- there are no instances for them --- they are only solved
2189 -- by "local instances" in expressions
2190 || cls `hasKey` typeableClassKey
2191 || cls `hasKey` coercibleTyConKey
2192 || cls `hasKey` eqTyConKey
2193 || cls `hasKey` heqTyConKey
2194
2195 -- | Tidy before printing a type
2196 ppr_tidy :: TidyEnv -> Type -> SDoc
2197 ppr_tidy env ty = pprType (tidyType env ty)
2198
2199 allDistinctTyVars :: TyVarSet -> [KindOrType] -> Bool
2200 -- (allDistinctTyVars tvs tys) returns True if tys are
2201 -- a) all tyvars
2202 -- b) all distinct
2203 -- c) disjoint from tvs
2204 allDistinctTyVars _ [] = True
2205 allDistinctTyVars tkvs (ty : tys)
2206 = case getTyVar_maybe ty of
2207 Nothing -> False
2208 Just tv | tv `elemVarSet` tkvs -> False
2209 | otherwise -> allDistinctTyVars (tkvs `extendVarSet` tv) tys