8a3aaade8577d780c8824990d0cdaa2b5a35a445
[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 Kind
38 import CoAxiom
39 import Class
40 import TyCon
41
42 -- others:
43 import HsSyn -- HsType
44 import TcRnMonad -- TcType, amongst others
45 import TcEnv ( tcInitTidyEnv, tcInitOpenTidyEnv )
46 import FunDeps
47 import FamInstEnv ( isDominatedBy, injectiveBranches,
48 InjectivityCheckResult(..) )
49 import FamInst ( makeInjectivityErrors )
50 import Name
51 import VarEnv
52 import VarSet
53 import Id ( idType, idName )
54 import Var ( TyVarBndr(..), mkTyVar )
55 import ErrUtils
56 import DynFlags
57 import Util
58 import ListSetOps
59 import SrcLoc
60 import Outputable
61 import Module
62 import Bag ( emptyBag )
63 import Unique ( mkAlphaTyVarUnique )
64 import qualified GHC.LanguageExtensions as LangExt
65
66 import Control.Monad
67 import Data.List ( (\\) )
68 import qualified Data.List.NonEmpty as NE
69
70 {-
71 ************************************************************************
72 * *
73 Checking for ambiguity
74 * *
75 ************************************************************************
76
77 Note [The ambiguity check for type signatures]
78 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
79 checkAmbiguity is a check on *user-supplied type signatures*. It is
80 *purely* there to report functions that cannot possibly be called. So for
81 example we want to reject:
82 f :: C a => Int
83 The idea is there can be no legal calls to 'f' because every call will
84 give rise to an ambiguous constraint. We could soundly omit the
85 ambiguity check on type signatures entirely, at the expense of
86 delaying ambiguity errors to call sites. Indeed, the flag
87 -XAllowAmbiguousTypes switches off the ambiguity check.
88
89 What about things like this:
90 class D a b | a -> b where ..
91 h :: D Int b => Int
92 The Int may well fix 'b' at the call site, so that signature should
93 not be rejected. Moreover, using *visible* fundeps is too
94 conservative. Consider
95 class X a b where ...
96 class D a b | a -> b where ...
97 instance D a b => X [a] b where...
98 h :: X a b => a -> a
99 Here h's type looks ambiguous in 'b', but here's a legal call:
100 ...(h [True])...
101 That gives rise to a (X [Bool] beta) constraint, and using the
102 instance means we need (D Bool beta) and that fixes 'beta' via D's
103 fundep!
104
105 Behind all these special cases there is a simple guiding principle.
106 Consider
107
108 f :: <type>
109 f = ...blah...
110
111 g :: <type>
112 g = f
113
114 You would think that the definition of g would surely typecheck!
115 After all f has exactly the same type, and g=f. But in fact f's type
116 is instantiated and the instantiated constraints are solved against
117 the originals, so in the case an ambiguous type it won't work.
118 Consider our earlier example f :: C a => Int. Then in g's definition,
119 we'll instantiate to (C alpha) and try to deduce (C alpha) from (C a),
120 and fail.
121
122 So in fact we use this as our *definition* of ambiguity. We use a
123 very similar test for *inferred* types, to ensure that they are
124 unambiguous. See Note [Impedance matching] in TcBinds.
125
126 This test is very conveniently implemented by calling
127 tcSubType <type> <type>
128 This neatly takes account of the functional dependecy stuff above,
129 and implicit parameter (see Note [Implicit parameters and ambiguity]).
130 And this is what checkAmbiguity does.
131
132 What about this, though?
133 g :: C [a] => Int
134 Is every call to 'g' ambiguous? After all, we might have
135 instance C [a] where ...
136 at the call site. So maybe that type is ok! Indeed even f's
137 quintessentially ambiguous type might, just possibly be callable:
138 with -XFlexibleInstances we could have
139 instance C a where ...
140 and now a call could be legal after all! Well, we'll reject this
141 unless the instance is available *here*.
142
143 Note [When to call checkAmbiguity]
144 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
145 We call checkAmbiguity
146 (a) on user-specified type signatures
147 (b) in checkValidType
148
149 Conncerning (b), you might wonder about nested foralls. What about
150 f :: forall b. (forall a. Eq a => b) -> b
151 The nested forall is ambiguous. Originally we called checkAmbiguity
152 in the forall case of check_type, but that had two bad consequences:
153 * We got two error messages about (Eq b) in a nested forall like this:
154 g :: forall a. Eq a => forall b. Eq b => a -> a
155 * If we try to check for ambiguity of a nested forall like
156 (forall a. Eq a => b), the implication constraint doesn't bind
157 all the skolems, which results in "No skolem info" in error
158 messages (see Trac #10432).
159
160 To avoid this, we call checkAmbiguity once, at the top, in checkValidType.
161 (I'm still a bit worried about unbound skolems when the type mentions
162 in-scope type variables.)
163
164 In fact, because of the co/contra-variance implemented in tcSubType,
165 this *does* catch function f above. too.
166
167 Concerning (a) the ambiguity check is only used for *user* types, not
168 for types coming from inteface files. The latter can legitimately
169 have ambiguous types. Example
170
171 class S a where s :: a -> (Int,Int)
172 instance S Char where s _ = (1,1)
173 f:: S a => [a] -> Int -> (Int,Int)
174 f (_::[a]) x = (a*x,b)
175 where (a,b) = s (undefined::a)
176
177 Here the worker for f gets the type
178 fw :: forall a. S a => Int -> (# Int, Int #)
179
180
181 Note [Implicit parameters and ambiguity]
182 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
183 Only a *class* predicate can give rise to ambiguity
184 An *implicit parameter* cannot. For example:
185 foo :: (?x :: [a]) => Int
186 foo = length ?x
187 is fine. The call site will supply a particular 'x'
188
189 Furthermore, the type variables fixed by an implicit parameter
190 propagate to the others. E.g.
191 foo :: (Show a, ?x::[a]) => Int
192 foo = show (?x++?x)
193 The type of foo looks ambiguous. But it isn't, because at a call site
194 we might have
195 let ?x = 5::Int in foo
196 and all is well. In effect, implicit parameters are, well, parameters,
197 so we can take their type variables into account as part of the
198 "tau-tvs" stuff. This is done in the function 'FunDeps.grow'.
199 -}
200
201 checkAmbiguity :: UserTypeCtxt -> Type -> TcM ()
202 checkAmbiguity ctxt ty
203 | wantAmbiguityCheck ctxt
204 = do { traceTc "Ambiguity check for" (ppr ty)
205 -- Solve the constraints eagerly because an ambiguous type
206 -- can cause a cascade of further errors. Since the free
207 -- tyvars are skolemised, we can safely use tcSimplifyTop
208 ; allow_ambiguous <- xoptM LangExt.AllowAmbiguousTypes
209 ; (_wrap, wanted) <- addErrCtxt (mk_msg allow_ambiguous) $
210 captureConstraints $
211 tcSubType_NC ctxt ty ty
212 ; simplifyAmbiguityCheck ty wanted
213
214 ; traceTc "Done ambiguity check for" (ppr ty) }
215
216 | otherwise
217 = return ()
218 where
219 mk_msg allow_ambiguous
220 = vcat [ text "In the ambiguity check for" <+> what
221 , ppUnless allow_ambiguous ambig_msg ]
222 ambig_msg = text "To defer the ambiguity check to use sites, enable AllowAmbiguousTypes"
223 what | Just n <- isSigMaybe ctxt = quotes (ppr n)
224 | otherwise = pprUserTypeCtxt ctxt
225
226 wantAmbiguityCheck :: UserTypeCtxt -> Bool
227 wantAmbiguityCheck ctxt
228 = case ctxt of -- See Note [When we don't check for ambiguity]
229 GhciCtxt -> False
230 TySynCtxt {} -> False
231 TypeAppCtxt -> False
232 _ -> True
233
234 checkUserTypeError :: Type -> TcM ()
235 -- Check to see if the type signature mentions "TypeError blah"
236 -- anywhere in it, and fail if so.
237 --
238 -- Very unsatisfactorily (Trac #11144) we need to tidy the type
239 -- because it may have come from an /inferred/ signature, not a
240 -- user-supplied one. This is really only a half-baked fix;
241 -- the other errors in checkValidType don't do tidying, and so
242 -- may give bad error messages when given an inferred type.
243 checkUserTypeError = check
244 where
245 check ty
246 | Just msg <- userTypeError_maybe ty = fail_with msg
247 | Just (_,ts) <- splitTyConApp_maybe ty = mapM_ check ts
248 | Just (t1,t2) <- splitAppTy_maybe ty = check t1 >> check t2
249 | Just (_,t1) <- splitForAllTy_maybe ty = check t1
250 | otherwise = return ()
251
252 fail_with msg = do { env0 <- tcInitTidyEnv
253 ; let (env1, tidy_msg) = tidyOpenType env0 msg
254 ; failWithTcM (env1, pprUserTypeErrorTy tidy_msg) }
255
256
257 {- Note [When we don't check for ambiguity]
258 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
259 In a few places we do not want to check a user-specified type for ambiguity
260
261 * GhciCtxt: Allow ambiguous types in GHCi's :kind command
262 E.g. type family T a :: * -- T :: forall k. k -> *
263 Then :k T should work in GHCi, not complain that
264 (T k) is ambiguous!
265
266 * TySynCtxt: type T a b = C a b => blah
267 It may be that when we /use/ T, we'll give an 'a' or 'b' that somehow
268 cure the ambiguity. So we defer the ambiguity check to the use site.
269
270 There is also an implementation reason (Trac #11608). In the RHS of
271 a type synonym we don't (currently) instantiate 'a' and 'b' with
272 TcTyVars before calling checkValidType, so we get asertion failures
273 from doing an ambiguity check on a type with TyVars in it. Fixing this
274 would not be hard, but let's wait till there's a reason.
275
276 * TypeAppCtxt: visible type application
277 f @ty
278 No need to check ty for ambiguity
279
280
281 ************************************************************************
282 * *
283 Checking validity of a user-defined type
284 * *
285 ************************************************************************
286
287 When dealing with a user-written type, we first translate it from an HsType
288 to a Type, performing kind checking, and then check various things that should
289 be true about it. We don't want to perform these checks at the same time
290 as the initial translation because (a) they are unnecessary for interface-file
291 types and (b) when checking a mutually recursive group of type and class decls,
292 we can't "look" at the tycons/classes yet. Also, the checks are rather
293 diverse, and used to really mess up the other code.
294
295 One thing we check for is 'rank'.
296
297 Rank 0: monotypes (no foralls)
298 Rank 1: foralls at the front only, Rank 0 inside
299 Rank 2: foralls at the front, Rank 1 on left of fn arrow,
300
301 basic ::= tyvar | T basic ... basic
302
303 r2 ::= forall tvs. cxt => r2a
304 r2a ::= r1 -> r2a | basic
305 r1 ::= forall tvs. cxt => r0
306 r0 ::= r0 -> r0 | basic
307
308 Another thing is to check that type synonyms are saturated.
309 This might not necessarily show up in kind checking.
310 type A i = i
311 data T k = MkT (k Int)
312 f :: T A -- BAD!
313 -}
314
315 checkValidType :: UserTypeCtxt -> Type -> TcM ()
316 -- Checks that a user-written type is valid for the given context
317 -- Assumes argument is fully zonked
318 -- Not used for instance decls; checkValidInstance instead
319 checkValidType ctxt ty
320 = do { traceTc "checkValidType" (ppr ty <+> text "::" <+> ppr (typeKind ty))
321 ; rankn_flag <- xoptM LangExt.RankNTypes
322 ; impred_flag <- xoptM LangExt.ImpredicativeTypes
323 ; let gen_rank :: Rank -> Rank
324 gen_rank r | rankn_flag = ArbitraryRank
325 | otherwise = r
326
327 rank1 = gen_rank r1
328 rank0 = gen_rank r0
329
330 r0 = rankZeroMonoType
331 r1 = LimitedRank True r0
332
333 rank
334 = case ctxt of
335 DefaultDeclCtxt-> MustBeMonoType
336 ResSigCtxt -> MustBeMonoType
337 PatSigCtxt -> rank0
338 RuleSigCtxt _ -> rank1
339 TySynCtxt _ -> rank0
340
341 ExprSigCtxt -> rank1
342 KindSigCtxt -> rank1
343 TypeAppCtxt | impred_flag -> ArbitraryRank
344 | otherwise -> tyConArgMonoType
345 -- Normally, ImpredicativeTypes is handled in check_arg_type,
346 -- but visible type applications don't go through there.
347 -- So we do this check here.
348
349 FunSigCtxt {} -> rank1
350 InfSigCtxt _ -> ArbitraryRank -- Inferred type
351 ConArgCtxt _ -> rank1 -- We are given the type of the entire
352 -- constructor, hence rank 1
353 PatSynCtxt _ -> rank1
354
355 ForSigCtxt _ -> rank1
356 SpecInstCtxt -> rank1
357 ThBrackCtxt -> rank1
358 GhciCtxt -> ArbitraryRank
359
360 TyVarBndrKindCtxt _ -> rank0
361 DataKindCtxt _ -> rank1
362 TySynKindCtxt _ -> rank1
363 TyFamResKindCtxt _ -> rank1
364
365 _ -> panic "checkValidType"
366 -- Can't happen; not used for *user* sigs
367
368 ; env <- tcInitOpenTidyEnv (tyCoVarsOfTypeList ty)
369
370 -- Check the internal validity of the type itself
371 ; check_type env ctxt rank ty
372
373 ; checkUserTypeError ty
374
375 -- Check for ambiguous types. See Note [When to call checkAmbiguity]
376 -- NB: this will happen even for monotypes, but that should be cheap;
377 -- and there may be nested foralls for the subtype test to examine
378 ; checkAmbiguity ctxt ty
379
380 ; traceTc "checkValidType done" (ppr ty <+> text "::" <+> ppr (typeKind ty)) }
381
382 checkValidMonoType :: Type -> TcM ()
383 -- Assumes argument is fully zonked
384 checkValidMonoType ty
385 = do { env <- tcInitOpenTidyEnv (tyCoVarsOfTypeList ty)
386 ; check_type env SigmaCtxt MustBeMonoType ty }
387
388 checkTySynRhs :: UserTypeCtxt -> TcType -> TcM ()
389 checkTySynRhs ctxt ty
390 | returnsConstraintKind actual_kind
391 = do { ck <- xoptM LangExt.ConstraintKinds
392 ; if ck
393 then when (isConstraintKind actual_kind)
394 (do { dflags <- getDynFlags
395 ; check_pred_ty emptyTidyEnv dflags ctxt ty })
396 else addErrTcM (constraintSynErr emptyTidyEnv actual_kind) }
397
398 | otherwise
399 = return ()
400 where
401 actual_kind = typeKind ty
402
403 -- | The kind expected in a certain context.
404 data ContextKind = TheKind Kind -- ^ a specific kind
405 | AnythingKind -- ^ any kind will do
406 | OpenKind -- ^ something of the form @TYPE _@
407
408 -- Depending on the context, we might accept any kind (for instance, in a TH
409 -- splice), or only certain kinds (like in type signatures).
410 expectedKindInCtxt :: UserTypeCtxt -> ContextKind
411 expectedKindInCtxt (TySynCtxt _) = AnythingKind
412 expectedKindInCtxt ThBrackCtxt = AnythingKind
413 expectedKindInCtxt GhciCtxt = AnythingKind
414 -- The types in a 'default' decl can have varying kinds
415 -- See Note [Extended defaults]" in TcEnv
416 expectedKindInCtxt DefaultDeclCtxt = AnythingKind
417 expectedKindInCtxt TypeAppCtxt = AnythingKind
418 expectedKindInCtxt (ForSigCtxt _) = TheKind liftedTypeKind
419 expectedKindInCtxt (InstDeclCtxt {}) = TheKind constraintKind
420 expectedKindInCtxt SpecInstCtxt = TheKind constraintKind
421 expectedKindInCtxt _ = OpenKind
422
423 {-
424 Note [Higher rank types]
425 ~~~~~~~~~~~~~~~~~~~~~~~~
426 Technically
427 Int -> forall a. a->a
428 is still a rank-1 type, but it's not Haskell 98 (Trac #5957). So the
429 validity checker allow a forall after an arrow only if we allow it
430 before -- that is, with Rank2Types or RankNTypes
431 -}
432
433 data Rank = ArbitraryRank -- Any rank ok
434
435 | LimitedRank -- Note [Higher rank types]
436 Bool -- Forall ok at top
437 Rank -- Use for function arguments
438
439 | MonoType SDoc -- Monotype, with a suggestion of how it could be a polytype
440
441 | MustBeMonoType -- Monotype regardless of flags
442
443
444 rankZeroMonoType, tyConArgMonoType, synArgMonoType, constraintMonoType :: Rank
445 rankZeroMonoType = MonoType (text "Perhaps you intended to use RankNTypes or Rank2Types")
446 tyConArgMonoType = MonoType (text "GHC doesn't yet support impredicative polymorphism")
447 synArgMonoType = MonoType (text "Perhaps you intended to use LiberalTypeSynonyms")
448 constraintMonoType = MonoType (vcat [ text "A constraint must be a monotype"
449 , text "Perhaps you intended to use QuantifiedConstraints" ])
450
451 funArgResRank :: Rank -> (Rank, Rank) -- Function argument and result
452 funArgResRank (LimitedRank _ arg_rank) = (arg_rank, LimitedRank (forAllAllowed arg_rank) arg_rank)
453 funArgResRank other_rank = (other_rank, other_rank)
454
455 forAllAllowed :: Rank -> Bool
456 forAllAllowed ArbitraryRank = True
457 forAllAllowed (LimitedRank forall_ok _) = forall_ok
458 forAllAllowed _ = False
459
460 ----------------------------------------
461 check_type :: TidyEnv -> UserTypeCtxt -> Rank -> Type -> TcM ()
462 -- The args say what the *type context* requires, independent
463 -- of *flag* settings. You test the flag settings at usage sites.
464 --
465 -- Rank is allowed rank for function args
466 -- Rank 0 means no for-alls anywhere
467
468 check_type env ctxt rank ty
469 | not (null tvbs && null theta)
470 = do { traceTc "check_type" (ppr ty $$ ppr (forAllAllowed rank))
471 ; checkTcM (forAllAllowed rank) (forAllTyErr env rank ty)
472 -- Reject e.g. (Maybe (?x::Int => Int)),
473 -- with a decent error message
474
475 ; check_valid_theta env' SigmaCtxt theta
476 -- Allow type T = ?x::Int => Int -> Int
477 -- but not type T = ?x::Int
478
479 ; check_type env' ctxt rank tau -- Allow foralls to right of arrow
480
481 ; checkTcM (not (any (`elemVarSet` tyCoVarsOfType phi_kind) tvs))
482 (forAllEscapeErr env' ty tau_kind)
483 }
484 where
485 (tvbs, phi) = tcSplitForAllTyVarBndrs ty
486 (theta, tau) = tcSplitPhiTy phi
487
488 tvs = binderVars tvbs
489 (env', _) = tidyTyCoVarBndrs env tvs
490
491 tau_kind = typeKind tau
492 phi_kind | null theta = tau_kind
493 | otherwise = liftedTypeKind
494 -- If there are any constraints, the kind is *. (#11405)
495
496 check_type _ _ _ (TyVarTy _) = return ()
497
498 check_type env ctxt rank (FunTy arg_ty res_ty)
499 = do { check_type env ctxt arg_rank arg_ty
500 ; check_type env ctxt res_rank res_ty }
501 where
502 (arg_rank, res_rank) = funArgResRank rank
503
504 check_type env ctxt rank (AppTy ty1 ty2)
505 = do { check_type env ctxt rank ty1
506 ; check_arg_type env ctxt rank ty2 }
507
508 check_type env ctxt rank ty@(TyConApp tc tys)
509 | isTypeSynonymTyCon tc || isTypeFamilyTyCon tc
510 = check_syn_tc_app env ctxt rank ty tc tys
511 | isUnboxedTupleTyCon tc = check_ubx_tuple env ctxt ty tys
512 | otherwise = mapM_ (check_arg_type env ctxt rank) tys
513
514 check_type _ _ _ (LitTy {}) = return ()
515
516 check_type env ctxt rank (CastTy ty _) = check_type env ctxt rank ty
517
518 check_type _ _ _ ty = pprPanic "check_type" (ppr ty)
519
520 ----------------------------------------
521 check_syn_tc_app :: TidyEnv -> UserTypeCtxt -> Rank -> KindOrType
522 -> TyCon -> [KindOrType] -> TcM ()
523 -- Used for type synonyms and type synonym families,
524 -- which must be saturated,
525 -- but not data families, which need not be saturated
526 check_syn_tc_app env ctxt rank ty tc tys
527 | tys `lengthAtLeast` tc_arity -- Saturated
528 -- Check that the synonym has enough args
529 -- This applies equally to open and closed synonyms
530 -- It's OK to have an *over-applied* type synonym
531 -- data Tree a b = ...
532 -- type Foo a = Tree [a]
533 -- f :: Foo a b -> ...
534 = do { -- See Note [Liberal type synonyms]
535 ; liberal <- xoptM LangExt.LiberalTypeSynonyms
536 ; if not liberal || isTypeFamilyTyCon tc then
537 -- For H98 and synonym families, do check the type args
538 mapM_ check_arg tys
539
540 else -- In the liberal case (only for closed syns), expand then check
541 case tcView ty of
542 Just ty' -> check_type env ctxt rank ty'
543 Nothing -> pprPanic "check_tau_type" (ppr ty) }
544
545 | GhciCtxt <- ctxt -- Accept under-saturated type synonyms in
546 -- GHCi :kind commands; see Trac #7586
547 = mapM_ check_arg tys
548
549 | otherwise
550 = failWithTc (tyConArityErr tc tys)
551 where
552 tc_arity = tyConArity tc
553 check_arg | isTypeFamilyTyCon tc = check_arg_type env ctxt rank
554 | otherwise = check_type env ctxt synArgMonoType
555
556 ----------------------------------------
557 check_ubx_tuple :: TidyEnv -> UserTypeCtxt -> KindOrType
558 -> [KindOrType] -> TcM ()
559 check_ubx_tuple env ctxt ty tys
560 = do { ub_tuples_allowed <- xoptM LangExt.UnboxedTuples
561 ; checkTcM ub_tuples_allowed (ubxArgTyErr env ty)
562
563 ; impred <- xoptM LangExt.ImpredicativeTypes
564 ; let rank' = if impred then ArbitraryRank else tyConArgMonoType
565 -- c.f. check_arg_type
566 -- However, args are allowed to be unlifted, or
567 -- more unboxed tuples, so can't use check_arg_ty
568 ; mapM_ (check_type env ctxt rank') tys }
569
570 ----------------------------------------
571 check_arg_type :: TidyEnv -> UserTypeCtxt -> Rank -> KindOrType -> TcM ()
572 -- The sort of type that can instantiate a type variable,
573 -- or be the argument of a type constructor.
574 -- Not an unboxed tuple, but now *can* be a forall (since impredicativity)
575 -- Other unboxed types are very occasionally allowed as type
576 -- arguments depending on the kind of the type constructor
577 --
578 -- For example, we want to reject things like:
579 --
580 -- instance Ord a => Ord (forall s. T s a)
581 -- and
582 -- g :: T s (forall b.b)
583 --
584 -- NB: unboxed tuples can have polymorphic or unboxed args.
585 -- This happens in the workers for functions returning
586 -- product types with polymorphic components.
587 -- But not in user code.
588 -- Anyway, they are dealt with by a special case in check_tau_type
589
590 check_arg_type _ _ _ (CoercionTy {}) = return ()
591
592 check_arg_type env ctxt rank ty
593 = do { impred <- xoptM LangExt.ImpredicativeTypes
594 ; let rank' = case rank of -- Predictive => must be monotype
595 MustBeMonoType -> MustBeMonoType -- Monotype, regardless
596 _other | impred -> ArbitraryRank
597 | otherwise -> tyConArgMonoType
598 -- Make sure that MustBeMonoType is propagated,
599 -- so that we don't suggest -XImpredicativeTypes in
600 -- (Ord (forall a.a)) => a -> a
601 -- and so that if it Must be a monotype, we check that it is!
602
603 ; check_type env ctxt rank' ty }
604
605 ----------------------------------------
606 forAllTyErr :: TidyEnv -> Rank -> Type -> (TidyEnv, SDoc)
607 forAllTyErr env rank ty
608 = ( env
609 , vcat [ hang herald 2 (ppr_tidy env ty)
610 , suggestion ] )
611 where
612 (tvs, _theta, _tau) = tcSplitSigmaTy ty
613 herald | null tvs = text "Illegal qualified type:"
614 | otherwise = text "Illegal polymorphic type:"
615 suggestion = case rank of
616 LimitedRank {} -> text "Perhaps you intended to use RankNTypes or Rank2Types"
617 MonoType d -> d
618 _ -> Outputable.empty -- Polytype is always illegal
619
620 forAllEscapeErr :: TidyEnv -> Type -> Kind -> (TidyEnv, SDoc)
621 forAllEscapeErr env ty tau_kind
622 = ( env
623 , hang (vcat [ text "Quantified type's kind mentions quantified type variable"
624 , text "(skolem escape)" ])
625 2 (vcat [ text " type:" <+> ppr_tidy env ty
626 , text "of kind:" <+> ppr_tidy env tau_kind ]) )
627
628 ubxArgTyErr :: TidyEnv -> Type -> (TidyEnv, SDoc)
629 ubxArgTyErr env ty
630 = ( env, vcat [ sep [ text "Illegal unboxed tuple type as function argument:"
631 , ppr_tidy env ty ]
632 , text "Perhaps you intended to use UnboxedTuples" ] )
633
634 {-
635 Note [Liberal type synonyms]
636 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
637 If -XLiberalTypeSynonyms is on, expand closed type synonyms *before*
638 doing validity checking. This allows us to instantiate a synonym defn
639 with a for-all type, or with a partially-applied type synonym.
640 e.g. type T a b = a
641 type S m = m ()
642 f :: S (T Int)
643 Here, T is partially applied, so it's illegal in H98. But if you
644 expand S first, then T we get just
645 f :: Int
646 which is fine.
647
648 IMPORTANT: suppose T is a type synonym. Then we must do validity
649 checking on an appliation (T ty1 ty2)
650
651 *either* before expansion (i.e. check ty1, ty2)
652 *or* after expansion (i.e. expand T ty1 ty2, and then check)
653 BUT NOT BOTH
654
655 If we do both, we get exponential behaviour!!
656
657 data TIACons1 i r c = c i ::: r c
658 type TIACons2 t x = TIACons1 t (TIACons1 t x)
659 type TIACons3 t x = TIACons2 t (TIACons1 t x)
660 type TIACons4 t x = TIACons2 t (TIACons2 t x)
661 type TIACons7 t x = TIACons4 t (TIACons3 t x)
662
663
664 ************************************************************************
665 * *
666 \subsection{Checking a theta or source type}
667 * *
668 ************************************************************************
669
670 Note [Implicit parameters in instance decls]
671 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
672 Implicit parameters _only_ allowed in type signatures; not in instance
673 decls, superclasses etc. The reason for not allowing implicit params in
674 instances is a bit subtle. If we allowed
675 instance (?x::Int, Eq a) => Foo [a] where ...
676 then when we saw
677 (e :: (?x::Int) => t)
678 it would be unclear how to discharge all the potential uses of the ?x
679 in e. For example, a constraint Foo [Int] might come out of e, and
680 applying the instance decl would show up two uses of ?x. Trac #8912.
681 -}
682
683 checkValidTheta :: UserTypeCtxt -> ThetaType -> TcM ()
684 -- Assumes argument is fully zonked
685 checkValidTheta ctxt theta
686 = addErrCtxtM (checkThetaCtxt ctxt theta) $
687 do { env <- tcInitOpenTidyEnv (tyCoVarsOfTypesList theta)
688 ; check_valid_theta env ctxt theta }
689
690 -------------------------
691 check_valid_theta :: TidyEnv -> UserTypeCtxt -> [PredType] -> TcM ()
692 check_valid_theta _ _ []
693 = return ()
694 check_valid_theta env ctxt theta
695 = do { dflags <- getDynFlags
696 ; warnTcM (Reason Opt_WarnDuplicateConstraints)
697 (wopt Opt_WarnDuplicateConstraints dflags && notNull dups)
698 (dupPredWarn env dups)
699 ; traceTc "check_valid_theta" (ppr theta)
700 ; mapM_ (check_pred_ty env dflags ctxt) theta }
701 where
702 (_,dups) = removeDups nonDetCmpType theta
703 -- It's OK to use nonDetCmpType because dups only appears in the
704 -- warning
705
706 -------------------------
707 {- Note [Validity checking for constraints]
708 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
709 We look through constraint synonyms so that we can see the underlying
710 constraint(s). For example
711 type Foo = ?x::Int
712 instance Foo => C T
713 We should reject the instance because it has an implicit parameter in
714 the context.
715
716 But we record, in 'under_syn', whether we have looked under a synonym
717 to avoid requiring language extensions at the use site. Main example
718 (Trac #9838):
719
720 {-# LANGUAGE ConstraintKinds #-}
721 module A where
722 type EqShow a = (Eq a, Show a)
723
724 module B where
725 import A
726 foo :: EqShow a => a -> String
727
728 We don't want to require ConstraintKinds in module B.
729 -}
730
731 check_pred_ty :: TidyEnv -> DynFlags -> UserTypeCtxt -> PredType -> TcM ()
732 -- Check the validity of a predicate in a signature
733 -- See Note [Validity checking for constraints]
734 check_pred_ty env dflags ctxt pred
735 = do { check_type env SigmaCtxt rank pred
736 ; check_pred_help False env dflags ctxt pred }
737 where
738 rank | xopt LangExt.QuantifiedConstraints dflags
739 = ArbitraryRank
740 | otherwise
741 = constraintMonoType
742
743 check_pred_help :: Bool -- True <=> under a type synonym
744 -> TidyEnv
745 -> DynFlags -> UserTypeCtxt
746 -> PredType -> TcM ()
747 check_pred_help under_syn env dflags ctxt pred
748 | Just pred' <- tcView pred -- Switch on under_syn when going under a
749 -- synonym (Trac #9838, yuk)
750 = check_pred_help True env dflags ctxt pred'
751
752 | otherwise -- A bit like classifyPredType, but not the same
753 -- E.g. we treat (~) like (~#); and we look inside tuples
754 = case classifyPredType pred of
755 ClassPred cls tys
756 | isCTupleClass cls -> check_tuple_pred under_syn env dflags ctxt pred tys
757 | otherwise -> check_class_pred env dflags ctxt pred cls tys
758
759 EqPred NomEq _ _ -> -- a ~# b
760 check_eq_pred env dflags pred
761
762 EqPred ReprEq _ _ -> -- Ugh! When inferring types we may get
763 -- f :: (a ~R# b) => blha
764 -- And we want to treat that like (Coercible a b)
765 -- We should probably check argument shapes, but we
766 -- didn't do so before, so I'm leaving it for now
767 return ()
768
769 ForAllPred _ theta head -> check_quant_pred env dflags ctxt pred theta head
770 IrredPred {} -> check_irred_pred under_syn env dflags ctxt pred
771
772 check_eq_pred :: TidyEnv -> DynFlags -> PredType -> TcM ()
773 check_eq_pred env dflags pred
774 = -- Equational constraints are valid in all contexts if type
775 -- families are permitted
776 checkTcM (xopt LangExt.TypeFamilies dflags
777 || xopt LangExt.GADTs dflags)
778 (eqPredTyErr env pred)
779
780 check_quant_pred :: TidyEnv -> DynFlags -> UserTypeCtxt
781 -> PredType -> ThetaType -> PredType -> TcM ()
782 check_quant_pred env dflags _ctxt pred theta head_pred
783 = addErrCtxt (text "In the quantified constraint" <+> quotes (ppr pred)) $
784 do { -- Check the instance head
785 case classifyPredType head_pred of
786 ClassPred cls tys -> checkValidInstHead SigmaCtxt cls tys
787 -- SigmaCtxt tells checkValidInstHead that
788 -- this is the head of a quantified constraint
789 IrredPred {} | hasTyVarHead head_pred
790 -> return ()
791 _ -> failWithTcM (badQuantHeadErr env pred)
792
793 -- Check for termination
794 ; unless (xopt LangExt.UndecidableInstances dflags) $
795 checkInstTermination theta head_pred
796 }
797
798 check_tuple_pred :: Bool -> TidyEnv -> DynFlags -> UserTypeCtxt -> PredType -> [PredType] -> TcM ()
799 check_tuple_pred under_syn env dflags ctxt pred ts
800 = do { -- See Note [ConstraintKinds in predicates]
801 checkTcM (under_syn || xopt LangExt.ConstraintKinds dflags)
802 (predTupleErr env pred)
803 ; mapM_ (check_pred_help under_syn env dflags ctxt) ts }
804 -- This case will not normally be executed because without
805 -- -XConstraintKinds tuple types are only kind-checked as *
806
807 check_irred_pred :: Bool -> TidyEnv -> DynFlags -> UserTypeCtxt -> PredType -> TcM ()
808 check_irred_pred under_syn env dflags ctxt pred
809 -- The predicate looks like (X t1 t2) or (x t1 t2) :: Constraint
810 -- where X is a type function
811 = do { -- If it looks like (x t1 t2), require ConstraintKinds
812 -- see Note [ConstraintKinds in predicates]
813 -- But (X t1 t2) is always ok because we just require ConstraintKinds
814 -- at the definition site (Trac #9838)
815 failIfTcM (not under_syn && not (xopt LangExt.ConstraintKinds dflags)
816 && hasTyVarHead pred)
817 (predIrredErr env pred)
818
819 -- Make sure it is OK to have an irred pred in this context
820 -- See Note [Irreducible predicates in superclasses]
821 ; failIfTcM (is_superclass ctxt
822 && not (xopt LangExt.UndecidableInstances dflags)
823 && has_tyfun_head pred)
824 (predSuperClassErr env pred) }
825 where
826 is_superclass ctxt = case ctxt of { ClassSCCtxt _ -> True; _ -> False }
827 has_tyfun_head ty
828 = case tcSplitTyConApp_maybe ty of
829 Just (tc, _) -> isTypeFamilyTyCon tc
830 Nothing -> False
831
832 {- Note [ConstraintKinds in predicates]
833 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
834 Don't check for -XConstraintKinds under a type synonym, because that
835 was done at the type synonym definition site; see Trac #9838
836 e.g. module A where
837 type C a = (Eq a, Ix a) -- Needs -XConstraintKinds
838 module B where
839 import A
840 f :: C a => a -> a -- Does *not* need -XConstraintKinds
841
842 Note [Irreducible predicates in superclasses]
843 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
844 Allowing type-family calls in class superclasses is somewhat dangerous
845 because we can write:
846
847 type family Fooish x :: * -> Constraint
848 type instance Fooish () = Foo
849 class Fooish () a => Foo a where
850
851 This will cause the constraint simplifier to loop because every time we canonicalise a
852 (Foo a) class constraint we add a (Fooish () a) constraint which will be immediately
853 solved to add+canonicalise another (Foo a) constraint. -}
854
855 -------------------------
856 check_class_pred :: TidyEnv -> DynFlags -> UserTypeCtxt
857 -> PredType -> Class -> [TcType] -> TcM ()
858 check_class_pred env dflags ctxt pred cls tys
859 | cls `hasKey` heqTyConKey -- (~) and (~~) are classified as classes,
860 || cls `hasKey` eqTyConKey -- but here we want to treat them as equalities
861 = -- pprTrace "check_class" (ppr cls) $
862 check_eq_pred env dflags pred
863
864 | isIPClass cls
865 = do { check_arity
866 ; checkTcM (okIPCtxt ctxt) (badIPPred env pred) }
867
868 | otherwise -- Includes Coercible
869 = do { check_arity
870 ; checkSimplifiableClassConstraint env dflags ctxt cls tys
871 ; checkTcM arg_tys_ok (predTyVarErr env pred) }
872 where
873 check_arity = checkTc (tys `lengthIs` classArity cls)
874 (tyConArityErr (classTyCon cls) tys)
875
876 -- Check the arguments of a class constraint
877 flexible_contexts = xopt LangExt.FlexibleContexts dflags
878 undecidable_ok = xopt LangExt.UndecidableInstances dflags
879 arg_tys_ok = case ctxt of
880 SpecInstCtxt -> True -- {-# SPECIALISE instance Eq (T Int) #-} is fine
881 InstDeclCtxt {} -> checkValidClsArgs (flexible_contexts || undecidable_ok) cls tys
882 -- Further checks on head and theta
883 -- in checkInstTermination
884 _ -> checkValidClsArgs flexible_contexts cls tys
885
886 checkSimplifiableClassConstraint :: TidyEnv -> DynFlags -> UserTypeCtxt
887 -> Class -> [TcType] -> TcM ()
888 -- See Note [Simplifiable given constraints]
889 checkSimplifiableClassConstraint env dflags ctxt cls tys
890 | not (wopt Opt_WarnSimplifiableClassConstraints dflags)
891 = return ()
892 | xopt LangExt.MonoLocalBinds dflags
893 = return ()
894
895 | DataTyCtxt {} <- ctxt -- Don't do this check for the "stupid theta"
896 = return () -- of a data type declaration
897
898 | cls `hasKey` coercibleTyConKey
899 = return () -- Oddly, we treat (Coercible t1 t2) as unconditionally OK
900 -- matchGlobalInst will reply "yes" because we can reduce
901 -- (Coercible a b) to (a ~R# b)
902
903 | otherwise
904 = do { result <- matchGlobalInst dflags False cls tys
905 ; case result of
906 OneInst { cir_what = what }
907 -> addWarnTc (Reason Opt_WarnSimplifiableClassConstraints)
908 (simplifiable_constraint_warn what)
909 _ -> return () }
910 where
911 pred = mkClassPred cls tys
912
913 simplifiable_constraint_warn :: InstanceWhat -> SDoc
914 simplifiable_constraint_warn what
915 = vcat [ hang (text "The constraint" <+> quotes (ppr (tidyType env pred))
916 <+> text "matches")
917 2 (ppr_what what)
918 , hang (text "This makes type inference for inner bindings fragile;")
919 2 (text "either use MonoLocalBinds, or simplify it using the instance") ]
920
921 ppr_what BuiltinInstance = text "a built-in instance"
922 ppr_what LocalInstance = text "a locally-quantified instance"
923 ppr_what (TopLevInstance { iw_dfun_id = dfun })
924 = hang (text "instance" <+> pprSigmaType (idType dfun))
925 2 (text "--" <+> pprDefinedAt (idName dfun))
926
927
928 {- Note [Simplifiable given constraints]
929 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
930 A type signature like
931 f :: Eq [(a,b)] => a -> b
932 is very fragile, for reasons described at length in TcInteract
933 Note [Instance and Given overlap]. As that Note discusses, for the
934 most part the clever stuff in TcInteract means that we don't use a
935 top-level instance if a local Given might fire, so there is no
936 fragility. But if we /infer/ the type of a local let-binding, things
937 can go wrong (Trac #11948 is an example, discussed in the Note).
938
939 So this warning is switched on only if we have NoMonoLocalBinds; in
940 that case the warning discourages users from writing simplifiable
941 class constraints.
942
943 The warning only fires if the constraint in the signature
944 matches the top-level instances in only one way, and with no
945 unifiers -- that is, under the same circumstances that
946 TcInteract.matchInstEnv fires an interaction with the top
947 level instances. For example (Trac #13526), consider
948
949 instance {-# OVERLAPPABLE #-} Eq (T a) where ...
950 instance Eq (T Char) where ..
951 f :: Eq (T a) => ...
952
953 We don't want to complain about this, even though the context
954 (Eq (T a)) matches an instance, because the user may be
955 deliberately deferring the choice so that the Eq (T Char)
956 has a chance to fire when 'f' is called. And the fragility
957 only matters when there's a risk that the instance might
958 fire instead of the local 'given'; and there is no such
959 risk in this case. Just use the same rules as for instance
960 firing!
961 -}
962
963 -------------------------
964 okIPCtxt :: UserTypeCtxt -> Bool
965 -- See Note [Implicit parameters in instance decls]
966 okIPCtxt (FunSigCtxt {}) = True
967 okIPCtxt (InfSigCtxt {}) = True
968 okIPCtxt ExprSigCtxt = True
969 okIPCtxt TypeAppCtxt = True
970 okIPCtxt PatSigCtxt = True
971 okIPCtxt ResSigCtxt = True
972 okIPCtxt GenSigCtxt = True
973 okIPCtxt (ConArgCtxt {}) = True
974 okIPCtxt (ForSigCtxt {}) = True -- ??
975 okIPCtxt ThBrackCtxt = True
976 okIPCtxt GhciCtxt = True
977 okIPCtxt SigmaCtxt = True
978 okIPCtxt (DataTyCtxt {}) = True
979 okIPCtxt (PatSynCtxt {}) = True
980 okIPCtxt (TySynCtxt {}) = True -- e.g. type Blah = ?x::Int
981 -- Trac #11466
982
983 okIPCtxt (KindSigCtxt {}) = False
984 okIPCtxt (ClassSCCtxt {}) = False
985 okIPCtxt (InstDeclCtxt {}) = False
986 okIPCtxt (SpecInstCtxt {}) = False
987 okIPCtxt (RuleSigCtxt {}) = False
988 okIPCtxt DefaultDeclCtxt = False
989 okIPCtxt DerivClauseCtxt = False
990 okIPCtxt (TyVarBndrKindCtxt {}) = False
991 okIPCtxt (DataKindCtxt {}) = False
992 okIPCtxt (TySynKindCtxt {}) = False
993 okIPCtxt (TyFamResKindCtxt {}) = False
994
995 {-
996 Note [Kind polymorphic type classes]
997 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
998 MultiParam check:
999
1000 class C f where... -- C :: forall k. k -> Constraint
1001 instance C Maybe where...
1002
1003 The dictionary gets type [C * Maybe] even if it's not a MultiParam
1004 type class.
1005
1006 Flexibility check:
1007
1008 class C f where... -- C :: forall k. k -> Constraint
1009 data D a = D a
1010 instance C D where
1011
1012 The dictionary gets type [C * (D *)]. IA0_TODO it should be
1013 generalized actually.
1014 -}
1015
1016 checkThetaCtxt :: UserTypeCtxt -> ThetaType -> TidyEnv -> TcM (TidyEnv, SDoc)
1017 checkThetaCtxt ctxt theta env
1018 = return ( env
1019 , vcat [ text "In the context:" <+> pprTheta (tidyTypes env theta)
1020 , text "While checking" <+> pprUserTypeCtxt ctxt ] )
1021
1022 eqPredTyErr, predTupleErr, predIrredErr,
1023 predSuperClassErr, badQuantHeadErr :: TidyEnv -> PredType -> (TidyEnv, SDoc)
1024 badQuantHeadErr env pred
1025 = ( env
1026 , hang (text "Quantified predicate must have a class or type variable head:")
1027 2 (ppr_tidy env pred) )
1028 eqPredTyErr env pred
1029 = ( env
1030 , text "Illegal equational constraint" <+> ppr_tidy env pred $$
1031 parens (text "Use GADTs or TypeFamilies to permit this") )
1032 predTupleErr env pred
1033 = ( env
1034 , hang (text "Illegal tuple constraint:" <+> ppr_tidy env pred)
1035 2 (parens constraintKindsMsg) )
1036 predIrredErr env pred
1037 = ( env
1038 , hang (text "Illegal constraint:" <+> ppr_tidy env pred)
1039 2 (parens constraintKindsMsg) )
1040 predSuperClassErr env pred
1041 = ( env
1042 , hang (text "Illegal constraint" <+> quotes (ppr_tidy env pred)
1043 <+> text "in a superclass context")
1044 2 (parens undecidableMsg) )
1045
1046 predTyVarErr :: TidyEnv -> PredType -> (TidyEnv, SDoc)
1047 predTyVarErr env pred
1048 = (env
1049 , vcat [ hang (text "Non type-variable argument")
1050 2 (text "in the constraint:" <+> ppr_tidy env pred)
1051 , parens (text "Use FlexibleContexts to permit this") ])
1052
1053 badIPPred :: TidyEnv -> PredType -> (TidyEnv, SDoc)
1054 badIPPred env pred
1055 = ( env
1056 , text "Illegal implicit parameter" <+> quotes (ppr_tidy env pred) )
1057
1058 constraintSynErr :: TidyEnv -> Type -> (TidyEnv, SDoc)
1059 constraintSynErr env kind
1060 = ( env
1061 , hang (text "Illegal constraint synonym of kind:" <+> quotes (ppr_tidy env kind))
1062 2 (parens constraintKindsMsg) )
1063
1064 dupPredWarn :: TidyEnv -> [NE.NonEmpty PredType] -> (TidyEnv, SDoc)
1065 dupPredWarn env dups
1066 = ( env
1067 , text "Duplicate constraint" <> plural primaryDups <> text ":"
1068 <+> pprWithCommas (ppr_tidy env) primaryDups )
1069 where
1070 primaryDups = map NE.head dups
1071
1072 tyConArityErr :: TyCon -> [TcType] -> SDoc
1073 -- For type-constructor arity errors, be careful to report
1074 -- the number of /visible/ arguments required and supplied,
1075 -- ignoring the /invisible/ arguments, which the user does not see.
1076 -- (e.g. Trac #10516)
1077 tyConArityErr tc tks
1078 = arityErr (ppr (tyConFlavour tc)) (tyConName tc)
1079 tc_type_arity tc_type_args
1080 where
1081 vis_tks = filterOutInvisibleTypes tc tks
1082
1083 -- tc_type_arity = number of *type* args expected
1084 -- tc_type_args = number of *type* args encountered
1085 tc_type_arity = count isVisibleTyConBinder (tyConBinders tc)
1086 tc_type_args = length vis_tks
1087
1088 arityErr :: Outputable a => SDoc -> a -> Int -> Int -> SDoc
1089 arityErr what name n m
1090 = hsep [ text "The" <+> what, quotes (ppr name), text "should have",
1091 n_arguments <> comma, text "but has been given",
1092 if m==0 then text "none" else int m]
1093 where
1094 n_arguments | n == 0 = text "no arguments"
1095 | n == 1 = text "1 argument"
1096 | True = hsep [int n, text "arguments"]
1097
1098 {-
1099 ************************************************************************
1100 * *
1101 \subsection{Checking for a decent instance head type}
1102 * *
1103 ************************************************************************
1104
1105 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1106 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1107
1108 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1109 flag is on, or (2)~the instance is imported (they must have been
1110 compiled elsewhere). In these cases, we let them go through anyway.
1111
1112 We can also have instances for functions: @instance Foo (a -> b) ...@.
1113 -}
1114
1115 checkValidInstHead :: UserTypeCtxt -> Class -> [Type] -> TcM ()
1116 checkValidInstHead ctxt clas cls_args
1117 = do { dflags <- getDynFlags
1118 ; this_mod <- getModule
1119 ; is_boot <- tcIsHsBootOrSig
1120 ; check_valid_inst_head dflags this_mod is_boot ctxt clas cls_args }
1121
1122 check_valid_inst_head :: DynFlags -> Module -> Bool
1123 -> UserTypeCtxt -> Class -> [Type] -> TcM ()
1124 -- Wow! There are a surprising number of ad-hoc special cases here.
1125 check_valid_inst_head dflags this_mod is_boot ctxt clas cls_args
1126
1127 -- If not in an hs-boot file, abstract classes cannot have instances
1128 | isAbstractClass clas
1129 , not is_boot
1130 = failWithTc abstract_class_msg
1131
1132 -- For Typeable, don't complain about instances for
1133 -- standalone deriving; they are no-ops, and we warn about
1134 -- it in TcDeriv.deriveStandalone
1135 | clas_nm == typeableClassName
1136 , hand_written_bindings
1137 = failWithTc rejected_class_msg
1138
1139 -- Handwritten instances of KnownNat/KnownSymbol class
1140 -- are always forbidden (#12837)
1141 | clas_nm `elem` [ knownNatClassName, knownSymbolClassName ]
1142 , hand_written_bindings
1143 = failWithTc rejected_class_msg
1144
1145 -- For the most part we don't allow instances for Coercible;
1146 -- but we DO want to allow them in quantified constraints:
1147 -- f :: (forall a b. Coercible a b => Coercible (m a) (m b)) => ...m...
1148 | clas_nm == coercibleTyConName
1149 , not quantified_constraint
1150 = failWithTc rejected_class_msg
1151
1152 -- Handwritten instances of other nonminal-equality classes
1153 -- is forbidden, except in the defining module to allow
1154 -- instance a ~~ b => a ~ b
1155 -- which occurs in Data.Type.Equality
1156 | clas_nm `elem` [ heqTyConName, eqTyConName]
1157 , nameModule clas_nm /= this_mod
1158 = failWithTc rejected_class_msg
1159
1160 -- Check for hand-written Generic instances (disallowed in Safe Haskell)
1161 | clas_nm `elem` genericClassNames
1162 , hand_written_bindings
1163 = do { failIfTc (safeLanguageOn dflags) gen_inst_err
1164 ; when (safeInferOn dflags) (recordUnsafeInfer emptyBag) }
1165
1166 | clas_nm == hasFieldClassName
1167 = checkHasFieldInst clas cls_args
1168
1169 | isCTupleClass clas
1170 = failWithTc tuple_class_msg
1171
1172 -- Check language restrictions on the args to the class
1173 | check_h98_arg_shape
1174 , Just msg <- mb_ty_args_msg
1175 = failWithTc (instTypeErr clas cls_args msg)
1176
1177 | otherwise
1178 = mapM_ checkValidTypePat ty_args
1179 where
1180 clas_nm = getName clas
1181 ty_args = filterOutInvisibleTypes (classTyCon clas) cls_args
1182
1183 hand_written_bindings
1184 = case ctxt of
1185 InstDeclCtxt stand_alone -> not stand_alone
1186 SpecInstCtxt -> False
1187 DerivClauseCtxt -> False
1188 _ -> True
1189
1190 check_h98_arg_shape = case ctxt of
1191 SpecInstCtxt -> False
1192 DerivClauseCtxt -> False
1193 SigmaCtxt -> False
1194 _ -> True
1195 -- SigmaCtxt: once we are in quantified-constraint land, we
1196 -- aren't so picky about enforcing H98-language restrictions
1197 -- E.g. we want to allow a head like Coercible (m a) (m b)
1198
1199
1200 -- When we are looking at the head of a quantified constraint,
1201 -- check_quant_pred sets ctxt to SigmaCtxt
1202 quantified_constraint = case ctxt of
1203 SigmaCtxt -> True
1204 _ -> False
1205
1206 head_type_synonym_msg = parens (
1207 text "All instance types must be of the form (T t1 ... tn)" $$
1208 text "where T is not a synonym." $$
1209 text "Use TypeSynonymInstances if you want to disable this.")
1210
1211 head_type_args_tyvars_msg = parens (vcat [
1212 text "All instance types must be of the form (T a1 ... an)",
1213 text "where a1 ... an are *distinct type variables*,",
1214 text "and each type variable appears at most once in the instance head.",
1215 text "Use FlexibleInstances if you want to disable this."])
1216
1217 head_one_type_msg = parens $
1218 text "Only one type can be given in an instance head." $$
1219 text "Use MultiParamTypeClasses if you want to allow more, or zero."
1220
1221 rejected_class_msg = text "Class" <+> quotes (ppr clas_nm)
1222 <+> text "does not support user-specified instances"
1223 tuple_class_msg = text "You can't specify an instance for a tuple constraint"
1224
1225 gen_inst_err = rejected_class_msg $$ nest 2 (text "(in Safe Haskell)")
1226
1227 abstract_class_msg = text "Cannot define instance for abstract class"
1228 <+> quotes (ppr clas_nm)
1229
1230 mb_ty_args_msg
1231 | not (xopt LangExt.TypeSynonymInstances dflags)
1232 , not (all tcInstHeadTyNotSynonym ty_args)
1233 = Just head_type_synonym_msg
1234
1235 | not (xopt LangExt.FlexibleInstances dflags)
1236 , not (all tcInstHeadTyAppAllTyVars ty_args)
1237 = Just head_type_args_tyvars_msg
1238
1239 | length ty_args /= 1
1240 , not (xopt LangExt.MultiParamTypeClasses dflags)
1241 , not (xopt LangExt.NullaryTypeClasses dflags && null ty_args)
1242 = Just head_one_type_msg
1243
1244 | otherwise
1245 = Nothing
1246
1247 tcInstHeadTyNotSynonym :: Type -> Bool
1248 -- Used in Haskell-98 mode, for the argument types of an instance head
1249 -- These must not be type synonyms, but everywhere else type synonyms
1250 -- are transparent, so we need a special function here
1251 tcInstHeadTyNotSynonym ty
1252 = case ty of -- Do not use splitTyConApp,
1253 -- because that expands synonyms!
1254 TyConApp tc _ -> not (isTypeSynonymTyCon tc)
1255 _ -> True
1256
1257 tcInstHeadTyAppAllTyVars :: Type -> Bool
1258 -- Used in Haskell-98 mode, for the argument types of an instance head
1259 -- These must be a constructor applied to type variable arguments
1260 -- or a type-level literal.
1261 -- But we allow kind instantiations.
1262 tcInstHeadTyAppAllTyVars ty
1263 | Just (tc, tys) <- tcSplitTyConApp_maybe (dropCasts ty)
1264 = ok (filterOutInvisibleTypes tc tys) -- avoid kinds
1265 | LitTy _ <- ty = True -- accept type literals (Trac #13833)
1266 | otherwise
1267 = False
1268 where
1269 -- Check that all the types are type variables,
1270 -- and that each is distinct
1271 ok tys = equalLength tvs tys && hasNoDups tvs
1272 where
1273 tvs = mapMaybe tcGetTyVar_maybe tys
1274
1275 dropCasts :: Type -> Type
1276 -- See Note [Casts during validity checking]
1277 -- This function can turn a well-kinded type into an ill-kinded
1278 -- one, so I've kept it local to this module
1279 -- To consider: drop only HoleCo casts
1280 dropCasts (CastTy ty _) = dropCasts ty
1281 dropCasts (AppTy t1 t2) = mkAppTy (dropCasts t1) (dropCasts t2)
1282 dropCasts (FunTy t1 t2) = mkFunTy (dropCasts t1) (dropCasts t2)
1283 dropCasts (TyConApp tc tys) = mkTyConApp tc (map dropCasts tys)
1284 dropCasts (ForAllTy b ty) = ForAllTy (dropCastsB b) (dropCasts ty)
1285 dropCasts ty = ty -- LitTy, TyVarTy, CoercionTy
1286
1287 dropCastsB :: TyVarBinder -> TyVarBinder
1288 dropCastsB b = b -- Don't bother in the kind of a forall
1289
1290 instTypeErr :: Class -> [Type] -> SDoc -> SDoc
1291 instTypeErr cls tys msg
1292 = hang (hang (text "Illegal instance declaration for")
1293 2 (quotes (pprClassPred cls tys)))
1294 2 msg
1295
1296 -- | See Note [Validity checking of HasField instances]
1297 checkHasFieldInst :: Class -> [Type] -> TcM ()
1298 checkHasFieldInst cls tys@[_k_ty, x_ty, r_ty, _a_ty] =
1299 case splitTyConApp_maybe r_ty of
1300 Nothing -> whoops (text "Record data type must be specified")
1301 Just (tc, _)
1302 | isFamilyTyCon tc
1303 -> whoops (text "Record data type may not be a data family")
1304 | otherwise -> case isStrLitTy x_ty of
1305 Just lbl
1306 | isJust (lookupTyConFieldLabel lbl tc)
1307 -> whoops (ppr tc <+> text "already has a field"
1308 <+> quotes (ppr lbl))
1309 | otherwise -> return ()
1310 Nothing
1311 | null (tyConFieldLabels tc) -> return ()
1312 | otherwise -> whoops (ppr tc <+> text "has fields")
1313 where
1314 whoops = addErrTc . instTypeErr cls tys
1315 checkHasFieldInst _ tys = pprPanic "checkHasFieldInst" (ppr tys)
1316
1317 {- Note [Casts during validity checking]
1318 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1319 Consider the (bogus)
1320 instance Eq Char#
1321 We elaborate to 'Eq (Char# |> UnivCo(hole))' where the hole is an
1322 insoluble equality constraint for * ~ #. We'll report the insoluble
1323 constraint separately, but we don't want to *also* complain that Eq is
1324 not applied to a type constructor. So we look gaily look through
1325 CastTys here.
1326
1327 Another example: Eq (Either a). Then we actually get a cast in
1328 the middle:
1329 Eq ((Either |> g) a)
1330
1331
1332 Note [Validity checking of HasField instances]
1333 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1334 The HasField class has magic constraint solving behaviour (see Note
1335 [HasField instances] in TcInteract). However, we permit users to
1336 declare their own instances, provided they do not clash with the
1337 built-in behaviour. In particular, we forbid:
1338
1339 1. `HasField _ r _` where r is a variable
1340
1341 2. `HasField _ (T ...) _` if T is a data family
1342 (because it might have fields introduced later)
1343
1344 3. `HasField x (T ...) _` where x is a variable,
1345 if T has any fields at all
1346
1347 4. `HasField "foo" (T ...) _` if T has a "foo" field
1348
1349 The usual functional dependency checks also apply.
1350
1351
1352 Note [Valid 'deriving' predicate]
1353 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1354 validDerivPred checks for OK 'deriving' context. See Note [Exotic
1355 derived instance contexts] in TcDeriv. However the predicate is
1356 here because it uses sizeTypes, fvTypes.
1357
1358 It checks for three things
1359
1360 * No repeated variables (hasNoDups fvs)
1361
1362 * No type constructors. This is done by comparing
1363 sizeTypes tys == length (fvTypes tys)
1364 sizeTypes counts variables and constructors; fvTypes returns variables.
1365 So if they are the same, there must be no constructors. But there
1366 might be applications thus (f (g x)).
1367
1368 Note that tys only includes the visible arguments of the class type
1369 constructor. Including the non-visible arguments can cause the following,
1370 perfectly valid instance to be rejected:
1371 class Category (cat :: k -> k -> *) where ...
1372 newtype T (c :: * -> * -> *) a b = MkT (c a b)
1373 instance Category c => Category (T c) where ...
1374 since the first argument to Category is a non-visible *, which sizeTypes
1375 would count as a constructor! See Trac #11833.
1376
1377 * Also check for a bizarre corner case, when the derived instance decl
1378 would look like
1379 instance C a b => D (T a) where ...
1380 Note that 'b' isn't a parameter of T. This gives rise to all sorts of
1381 problems; in particular, it's hard to compare solutions for equality
1382 when finding the fixpoint, and that means the inferContext loop does
1383 not converge. See Trac #5287.
1384
1385 Note [Equality class instances]
1386 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1387 We can't have users writing instances for the equality classes. But we
1388 still need to be able to write instances for them ourselves. So we allow
1389 instances only in the defining module.
1390
1391 -}
1392
1393 validDerivPred :: TyVarSet -> PredType -> Bool
1394 -- See Note [Valid 'deriving' predicate]
1395 validDerivPred tv_set pred
1396 = case classifyPredType pred of
1397 ClassPred cls tys -> cls `hasKey` typeableClassKey
1398 -- Typeable constraints are bigger than they appear due
1399 -- to kind polymorphism, but that's OK
1400 || check_tys cls tys
1401 EqPred {} -> False -- reject equality constraints
1402 _ -> True -- Non-class predicates are ok
1403 where
1404 check_tys cls tys
1405 = hasNoDups fvs
1406 -- use sizePred to ignore implicit args
1407 && lengthIs fvs (sizePred pred)
1408 && all (`elemVarSet` tv_set) fvs
1409 where tys' = filterOutInvisibleTypes (classTyCon cls) tys
1410 fvs = fvTypes tys'
1411
1412 {-
1413 ************************************************************************
1414 * *
1415 \subsection{Checking instance for termination}
1416 * *
1417 ************************************************************************
1418 -}
1419
1420 {- Note [Instances and constraint synonyms]
1421 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1422 Currently, we don't allow instances for constraint synonyms at all.
1423 Consider these (Trac #13267):
1424 type C1 a = Show (a -> Bool)
1425 instance C1 Int where -- I1
1426 show _ = "ur"
1427
1428 This elicits "show is not a (visible) method of class C1", which isn't
1429 a great message. But it comes from the renamer, so it's hard to improve.
1430
1431 This needs a bit more care:
1432 type C2 a = (Show a, Show Int)
1433 instance C2 Int -- I2
1434
1435 If we use (splitTyConApp_maybe tau) in checkValidInstance to decompose
1436 the instance head, we'll expand the synonym on fly, and it'll look like
1437 instance (%,%) (Show Int, Show Int)
1438 and we /really/ don't want that. So we carefully do /not/ expand
1439 synonyms, by matching on TyConApp directly.
1440 -}
1441
1442 checkValidInstance :: UserTypeCtxt -> LHsSigType GhcRn -> Type
1443 -> TcM ([TyVar], ThetaType, Class, [Type])
1444 checkValidInstance ctxt hs_type ty
1445 | not is_tc_app
1446 = failWithTc (text "Instance head is not headed by a class")
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