Deduplicate `HaskellMachRegs.h` and `RtsMachRegs.h` headers
[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 checkValidTheta,
11 checkValidInstance, checkValidInstHead, validDerivPred,
12 checkTySynRhs,
13 checkValidCoAxiom, checkValidCoAxBranch,
14 checkValidTyFamEqn, checkConsistentFamInst,
15 badATErr, arityErr,
16 checkTyConTelescope,
17 allDistinctTyVars
18 ) where
19
20 #include "HsVersions.h"
21
22 import GhcPrelude
23
24 import Maybes
25
26 -- friends:
27 import TcUnify ( tcSubType_NC )
28 import TcSimplify ( simplifyAmbiguityCheck )
29 import ClsInst ( matchGlobalInst, ClsInstResult(..), InstanceWhat(..), AssocInstInfo(..) )
30 import TyCoFVs
31 import TyCoRep
32 import TcType hiding ( sizeType, sizeTypes )
33 import TysWiredIn ( heqTyConName, eqTyConName, coercibleTyConName )
34 import PrelNames
35 import Type
36 import Unify ( tcMatchTyX_BM, BindFlag(..) )
37 import Coercion
38 import CoAxiom
39 import Class
40 import TyCon
41
42 -- others:
43 import IfaceType( pprIfaceType, pprIfaceTypeApp )
44 import ToIface ( toIfaceTyCon, toIfaceTcArgs, toIfaceType )
45 import HsSyn -- HsType
46 import TcRnMonad -- TcType, amongst others
47 import TcEnv ( tcInitTidyEnv, tcInitOpenTidyEnv )
48 import FunDeps
49 import FamInstEnv ( isDominatedBy, injectiveBranches,
50 InjectivityCheckResult(..) )
51 import FamInst ( makeInjectivityErrors )
52 import Name
53 import VarEnv
54 import VarSet
55 import Var ( VarBndr(..), mkTyVar )
56 import Id ( idType, idName )
57 import FV
58 import ErrUtils
59 import DynFlags
60 import Util
61 import ListSetOps
62 import SrcLoc
63 import Outputable
64 import Unique ( mkAlphaTyVarUnique )
65 import Bag ( emptyBag )
66 import qualified GHC.LanguageExtensions as LangExt
67
68 import Control.Monad
69 import Data.Foldable
70 import Data.List ( (\\), nub )
71 import qualified Data.List.NonEmpty as NE
72
73 {-
74 ************************************************************************
75 * *
76 Checking for ambiguity
77 * *
78 ************************************************************************
79
80 Note [The ambiguity check for type signatures]
81 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
82 checkAmbiguity is a check on *user-supplied type signatures*. It is
83 *purely* there to report functions that cannot possibly be called. So for
84 example we want to reject:
85 f :: C a => Int
86 The idea is there can be no legal calls to 'f' because every call will
87 give rise to an ambiguous constraint. We could soundly omit the
88 ambiguity check on type signatures entirely, at the expense of
89 delaying ambiguity errors to call sites. Indeed, the flag
90 -XAllowAmbiguousTypes switches off the ambiguity check.
91
92 What about things like this:
93 class D a b | a -> b where ..
94 h :: D Int b => Int
95 The Int may well fix 'b' at the call site, so that signature should
96 not be rejected. Moreover, using *visible* fundeps is too
97 conservative. Consider
98 class X a b where ...
99 class D a b | a -> b where ...
100 instance D a b => X [a] b where...
101 h :: X a b => a -> a
102 Here h's type looks ambiguous in 'b', but here's a legal call:
103 ...(h [True])...
104 That gives rise to a (X [Bool] beta) constraint, and using the
105 instance means we need (D Bool beta) and that fixes 'beta' via D's
106 fundep!
107
108 Behind all these special cases there is a simple guiding principle.
109 Consider
110
111 f :: <type>
112 f = ...blah...
113
114 g :: <type>
115 g = f
116
117 You would think that the definition of g would surely typecheck!
118 After all f has exactly the same type, and g=f. But in fact f's type
119 is instantiated and the instantiated constraints are solved against
120 the originals, so in the case an ambiguous type it won't work.
121 Consider our earlier example f :: C a => Int. Then in g's definition,
122 we'll instantiate to (C alpha) and try to deduce (C alpha) from (C a),
123 and fail.
124
125 So in fact we use this as our *definition* of ambiguity. We use a
126 very similar test for *inferred* types, to ensure that they are
127 unambiguous. See Note [Impedance matching] in TcBinds.
128
129 This test is very conveniently implemented by calling
130 tcSubType <type> <type>
131 This neatly takes account of the functional dependecy stuff above,
132 and implicit parameter (see Note [Implicit parameters and ambiguity]).
133 And this is what checkAmbiguity does.
134
135 What about this, though?
136 g :: C [a] => Int
137 Is every call to 'g' ambiguous? After all, we might have
138 instance C [a] where ...
139 at the call site. So maybe that type is ok! Indeed even f's
140 quintessentially ambiguous type might, just possibly be callable:
141 with -XFlexibleInstances we could have
142 instance C a where ...
143 and now a call could be legal after all! Well, we'll reject this
144 unless the instance is available *here*.
145
146 Note [When to call checkAmbiguity]
147 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
148 We call checkAmbiguity
149 (a) on user-specified type signatures
150 (b) in checkValidType
151
152 Conncerning (b), you might wonder about nested foralls. What about
153 f :: forall b. (forall a. Eq a => b) -> b
154 The nested forall is ambiguous. Originally we called checkAmbiguity
155 in the forall case of check_type, but that had two bad consequences:
156 * We got two error messages about (Eq b) in a nested forall like this:
157 g :: forall a. Eq a => forall b. Eq b => a -> a
158 * If we try to check for ambiguity of a nested forall like
159 (forall a. Eq a => b), the implication constraint doesn't bind
160 all the skolems, which results in "No skolem info" in error
161 messages (see #10432).
162
163 To avoid this, we call checkAmbiguity once, at the top, in checkValidType.
164 (I'm still a bit worried about unbound skolems when the type mentions
165 in-scope type variables.)
166
167 In fact, because of the co/contra-variance implemented in tcSubType,
168 this *does* catch function f above. too.
169
170 Concerning (a) the ambiguity check is only used for *user* types, not
171 for types coming from inteface files. The latter can legitimately
172 have ambiguous types. Example
173
174 class S a where s :: a -> (Int,Int)
175 instance S Char where s _ = (1,1)
176 f:: S a => [a] -> Int -> (Int,Int)
177 f (_::[a]) x = (a*x,b)
178 where (a,b) = s (undefined::a)
179
180 Here the worker for f gets the type
181 fw :: forall a. S a => Int -> (# Int, Int #)
182
183
184 Note [Implicit parameters and ambiguity]
185 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
186 Only a *class* predicate can give rise to ambiguity
187 An *implicit parameter* cannot. For example:
188 foo :: (?x :: [a]) => Int
189 foo = length ?x
190 is fine. The call site will supply a particular 'x'
191
192 Furthermore, the type variables fixed by an implicit parameter
193 propagate to the others. E.g.
194 foo :: (Show a, ?x::[a]) => Int
195 foo = show (?x++?x)
196 The type of foo looks ambiguous. But it isn't, because at a call site
197 we might have
198 let ?x = 5::Int in foo
199 and all is well. In effect, implicit parameters are, well, parameters,
200 so we can take their type variables into account as part of the
201 "tau-tvs" stuff. This is done in the function 'FunDeps.grow'.
202 -}
203
204 checkAmbiguity :: UserTypeCtxt -> Type -> TcM ()
205 checkAmbiguity ctxt ty
206 | wantAmbiguityCheck ctxt
207 = do { traceTc "Ambiguity check for" (ppr ty)
208 -- Solve the constraints eagerly because an ambiguous type
209 -- can cause a cascade of further errors. Since the free
210 -- tyvars are skolemised, we can safely use tcSimplifyTop
211 ; allow_ambiguous <- xoptM LangExt.AllowAmbiguousTypes
212 ; (_wrap, wanted) <- addErrCtxt (mk_msg allow_ambiguous) $
213 captureConstraints $
214 tcSubType_NC ctxt ty ty
215 ; simplifyAmbiguityCheck ty wanted
216
217 ; traceTc "Done ambiguity check for" (ppr ty) }
218
219 | otherwise
220 = return ()
221 where
222 mk_msg allow_ambiguous
223 = vcat [ text "In the ambiguity check for" <+> what
224 , ppUnless allow_ambiguous ambig_msg ]
225 ambig_msg = text "To defer the ambiguity check to use sites, enable AllowAmbiguousTypes"
226 what | Just n <- isSigMaybe ctxt = quotes (ppr n)
227 | otherwise = pprUserTypeCtxt ctxt
228
229 wantAmbiguityCheck :: UserTypeCtxt -> Bool
230 wantAmbiguityCheck ctxt
231 = case ctxt of -- See Note [When we don't check for ambiguity]
232 GhciCtxt {} -> False
233 TySynCtxt {} -> False
234 TypeAppCtxt -> False
235 _ -> True
236
237 checkUserTypeError :: Type -> TcM ()
238 -- Check to see if the type signature mentions "TypeError blah"
239 -- anywhere in it, and fail if so.
240 --
241 -- Very unsatisfactorily (#11144) we need to tidy the type
242 -- because it may have come from an /inferred/ signature, not a
243 -- user-supplied one. This is really only a half-baked fix;
244 -- the other errors in checkValidType don't do tidying, and so
245 -- may give bad error messages when given an inferred type.
246 checkUserTypeError = check
247 where
248 check ty
249 | Just msg <- userTypeError_maybe ty = fail_with msg
250 | Just (_,ts) <- splitTyConApp_maybe ty = mapM_ check ts
251 | Just (t1,t2) <- splitAppTy_maybe ty = check t1 >> check t2
252 | Just (_,t1) <- splitForAllTy_maybe ty = check t1
253 | otherwise = return ()
254
255 fail_with msg = do { env0 <- tcInitTidyEnv
256 ; let (env1, tidy_msg) = tidyOpenType env0 msg
257 ; failWithTcM (env1, pprUserTypeErrorTy tidy_msg) }
258
259
260 {- Note [When we don't check for ambiguity]
261 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
262 In a few places we do not want to check a user-specified type for ambiguity
263
264 * GhciCtxt: Allow ambiguous types in GHCi's :kind command
265 E.g. type family T a :: * -- T :: forall k. k -> *
266 Then :k T should work in GHCi, not complain that
267 (T k) is ambiguous!
268
269 * TySynCtxt: type T a b = C a b => blah
270 It may be that when we /use/ T, we'll give an 'a' or 'b' that somehow
271 cure the ambiguity. So we defer the ambiguity check to the use site.
272
273 There is also an implementation reason (#11608). In the RHS of
274 a type synonym we don't (currently) instantiate 'a' and 'b' with
275 TcTyVars before calling checkValidType, so we get asertion failures
276 from doing an ambiguity check on a type with TyVars in it. Fixing this
277 would not be hard, but let's wait till there's a reason.
278
279 * TypeAppCtxt: visible type application
280 f @ty
281 No need to check ty for ambiguity
282
283
284 ************************************************************************
285 * *
286 Checking validity of a user-defined type
287 * *
288 ************************************************************************
289
290 When dealing with a user-written type, we first translate it from an HsType
291 to a Type, performing kind checking, and then check various things that should
292 be true about it. We don't want to perform these checks at the same time
293 as the initial translation because (a) they are unnecessary for interface-file
294 types and (b) when checking a mutually recursive group of type and class decls,
295 we can't "look" at the tycons/classes yet. Also, the checks are rather
296 diverse, and used to really mess up the other code.
297
298 One thing we check for is 'rank'.
299
300 Rank 0: monotypes (no foralls)
301 Rank 1: foralls at the front only, Rank 0 inside
302 Rank 2: foralls at the front, Rank 1 on left of fn arrow,
303
304 basic ::= tyvar | T basic ... basic
305
306 r2 ::= forall tvs. cxt => r2a
307 r2a ::= r1 -> r2a | basic
308 r1 ::= forall tvs. cxt => r0
309 r0 ::= r0 -> r0 | basic
310
311 Another thing is to check that type synonyms are saturated.
312 This might not necessarily show up in kind checking.
313 type A i = i
314 data T k = MkT (k Int)
315 f :: T A -- BAD!
316 -}
317
318 checkValidType :: UserTypeCtxt -> Type -> TcM ()
319 -- Checks that a user-written type is valid for the given context
320 -- Assumes argument is fully zonked
321 -- Not used for instance decls; checkValidInstance instead
322 checkValidType ctxt ty
323 = do { traceTc "checkValidType" (ppr ty <+> text "::" <+> ppr (tcTypeKind ty))
324 ; rankn_flag <- xoptM LangExt.RankNTypes
325 ; impred_flag <- xoptM LangExt.ImpredicativeTypes
326 ; let gen_rank :: Rank -> Rank
327 gen_rank r | rankn_flag = ArbitraryRank
328 | otherwise = r
329
330 rank1 = gen_rank r1
331 rank0 = gen_rank r0
332
333 r0 = rankZeroMonoType
334 r1 = LimitedRank True r0
335
336 rank
337 = case ctxt of
338 DefaultDeclCtxt-> MustBeMonoType
339 ResSigCtxt -> MustBeMonoType
340 PatSigCtxt -> rank0
341 RuleSigCtxt _ -> rank1
342 TySynCtxt _ -> rank0
343
344 ExprSigCtxt -> rank1
345 KindSigCtxt -> rank1
346 TypeAppCtxt | impred_flag -> ArbitraryRank
347 | otherwise -> tyConArgMonoType
348 -- Normally, ImpredicativeTypes is handled in check_arg_type,
349 -- but visible type applications don't go through there.
350 -- So we do this check here.
351
352 FunSigCtxt {} -> rank1
353 InfSigCtxt _ -> ArbitraryRank -- Inferred type
354 ConArgCtxt _ -> rank1 -- We are given the type of the entire
355 -- constructor, hence rank 1
356 PatSynCtxt _ -> rank1
357
358 ForSigCtxt _ -> rank1
359 SpecInstCtxt -> rank1
360 ThBrackCtxt -> rank1
361 GhciCtxt {} -> ArbitraryRank
362
363 TyVarBndrKindCtxt _ -> rank0
364 DataKindCtxt _ -> rank1
365 TySynKindCtxt _ -> rank1
366 TyFamResKindCtxt _ -> rank1
367
368 _ -> panic "checkValidType"
369 -- Can't happen; not used for *user* sigs
370
371 ; env <- tcInitOpenTidyEnv (tyCoVarsOfTypeList ty)
372 ; expand <- initialExpandMode
373 ; let ve = ValidityEnv{ ve_tidy_env = env, ve_ctxt = ctxt
374 , ve_rank = rank, ve_expand = expand }
375
376 -- Check the internal validity of the type itself
377 -- Fail if bad things happen, else we misleading
378 -- (and more complicated) errors in checkAmbiguity
379 ; checkNoErrs $
380 do { check_type ve ty
381 ; checkUserTypeError ty
382 ; traceTc "done ct" (ppr ty) }
383
384 -- Check for ambiguous types. See Note [When to call checkAmbiguity]
385 -- NB: this will happen even for monotypes, but that should be cheap;
386 -- and there may be nested foralls for the subtype test to examine
387 ; checkAmbiguity ctxt ty
388
389 ; traceTc "checkValidType done" (ppr ty <+> text "::" <+> ppr (tcTypeKind ty)) }
390
391 checkValidMonoType :: Type -> TcM ()
392 -- Assumes argument is fully zonked
393 checkValidMonoType ty
394 = do { env <- tcInitOpenTidyEnv (tyCoVarsOfTypeList ty)
395 ; expand <- initialExpandMode
396 ; let ve = ValidityEnv{ ve_tidy_env = env, ve_ctxt = SigmaCtxt
397 , ve_rank = MustBeMonoType, ve_expand = expand }
398 ; check_type ve ty }
399
400 checkTySynRhs :: UserTypeCtxt -> TcType -> TcM ()
401 checkTySynRhs ctxt ty
402 | tcReturnsConstraintKind actual_kind
403 = do { ck <- xoptM LangExt.ConstraintKinds
404 ; if ck
405 then when (tcIsConstraintKind actual_kind)
406 (do { dflags <- getDynFlags
407 ; expand <- initialExpandMode
408 ; check_pred_ty emptyTidyEnv dflags ctxt expand ty })
409 else addErrTcM (constraintSynErr emptyTidyEnv actual_kind) }
410
411 | otherwise
412 = return ()
413 where
414 actual_kind = tcTypeKind ty
415
416 {-
417 Note [Higher rank types]
418 ~~~~~~~~~~~~~~~~~~~~~~~~
419 Technically
420 Int -> forall a. a->a
421 is still a rank-1 type, but it's not Haskell 98 (#5957). So the
422 validity checker allow a forall after an arrow only if we allow it
423 before -- that is, with Rank2Types or RankNTypes
424 -}
425
426 data Rank = ArbitraryRank -- Any rank ok
427
428 | LimitedRank -- Note [Higher rank types]
429 Bool -- Forall ok at top
430 Rank -- Use for function arguments
431
432 | MonoType SDoc -- Monotype, with a suggestion of how it could be a polytype
433
434 | MustBeMonoType -- Monotype regardless of flags
435
436 instance Outputable Rank where
437 ppr ArbitraryRank = text "ArbitraryRank"
438 ppr (LimitedRank top_forall_ok r)
439 = text "LimitedRank" <+> ppr top_forall_ok
440 <+> parens (ppr r)
441 ppr (MonoType msg) = text "MonoType" <+> parens msg
442 ppr MustBeMonoType = text "MustBeMonoType"
443
444 rankZeroMonoType, tyConArgMonoType, synArgMonoType, constraintMonoType :: Rank
445 rankZeroMonoType = MonoType (text "Perhaps you intended to use RankNTypes")
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 allConstraintsAllowed :: UserTypeCtxt -> Bool
461 -- We don't allow arbitrary constraints in kinds
462 allConstraintsAllowed (TyVarBndrKindCtxt {}) = False
463 allConstraintsAllowed (DataKindCtxt {}) = False
464 allConstraintsAllowed (TySynKindCtxt {}) = False
465 allConstraintsAllowed (TyFamResKindCtxt {}) = False
466 allConstraintsAllowed _ = True
467
468 -- | Returns 'True' if the supplied 'UserTypeCtxt' is unambiguously not the
469 -- context for the type of a term, where visible, dependent quantification is
470 -- currently disallowed.
471 --
472 -- An example of something that is unambiguously the type of a term is the
473 -- @forall a -> a -> a@ in @foo :: forall a -> a -> a@. On the other hand, the
474 -- same type in @type family Foo :: forall a -> a -> a@ is unambiguously the
475 -- kind of a type, not the type of a term, so it is permitted.
476 --
477 -- For more examples, see
478 -- @testsuite/tests/dependent/should_compile/T16326_Compile*.hs@ (for places
479 -- where VDQ is permitted) and
480 -- @testsuite/tests/dependent/should_fail/T16326_Fail*.hs@ (for places where
481 -- VDQ is disallowed).
482 vdqAllowed :: UserTypeCtxt -> Bool
483 -- Currently allowed in the kinds of types...
484 vdqAllowed (KindSigCtxt {}) = True
485 vdqAllowed (TySynCtxt {}) = True
486 vdqAllowed (ThBrackCtxt {}) = True
487 vdqAllowed (GhciCtxt {}) = True
488 vdqAllowed (TyVarBndrKindCtxt {}) = True
489 vdqAllowed (DataKindCtxt {}) = True
490 vdqAllowed (TySynKindCtxt {}) = True
491 vdqAllowed (TyFamResKindCtxt {}) = True
492 -- ...but not in the types of terms.
493 vdqAllowed (ConArgCtxt {}) = False
494 -- We could envision allowing VDQ in data constructor types so long as the
495 -- constructor is only ever used at the type level, but for now, GHC adopts
496 -- the stance that VDQ is never allowed in data constructor types.
497 vdqAllowed (FunSigCtxt {}) = False
498 vdqAllowed (InfSigCtxt {}) = False
499 vdqAllowed (ExprSigCtxt {}) = False
500 vdqAllowed (TypeAppCtxt {}) = False
501 vdqAllowed (PatSynCtxt {}) = False
502 vdqAllowed (PatSigCtxt {}) = False
503 vdqAllowed (RuleSigCtxt {}) = False
504 vdqAllowed (ResSigCtxt {}) = False
505 vdqAllowed (ForSigCtxt {}) = False
506 vdqAllowed (DefaultDeclCtxt {}) = False
507 -- We count class constraints as "types of terms". All of the cases below deal
508 -- with class constraints.
509 vdqAllowed (InstDeclCtxt {}) = False
510 vdqAllowed (SpecInstCtxt {}) = False
511 vdqAllowed (GenSigCtxt {}) = False
512 vdqAllowed (ClassSCCtxt {}) = False
513 vdqAllowed (SigmaCtxt {}) = False
514 vdqAllowed (DataTyCtxt {}) = False
515 vdqAllowed (DerivClauseCtxt {}) = False
516
517 {-
518 Note [Correctness and performance of type synonym validity checking]
519 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
520 Consider the type A arg1 arg2, where A is a type synonym. How should we check
521 this type for validity? We have three distinct choices, corresponding to the
522 three constructors of ExpandMode:
523
524 1. Expand the application of A, and check the resulting type (`Expand`).
525 2. Don't expand the application of A. Only check the arguments (`NoExpand`).
526 3. Check the arguments *and* check the expanded type (`Both`).
527
528 It's tempting to think that we could always just pick choice (3), but this
529 results in serious performance issues when checking a type like in the
530 signature for `f` below:
531
532 type S = ...
533 f :: S (S (S (S (S (S ....(S Int)...))))
534
535 When checking the type of `f`, we'll check the outer `S` application with and
536 without expansion, and in *each* of those checks, we'll check the next `S`
537 application with and without expansion... the result is exponential blowup! So
538 clearly we don't want to use `Both` 100% of the time.
539
540 On the other hand, neither is it correct to use exclusively `Expand` or
541 exclusively `NoExpand` 100% of the time:
542
543 * If one always expands, then one can miss erroneous programs like the one in
544 the `tcfail129` test case:
545
546 type Foo a = String -> Maybe a
547 type Bar m = m Int
548 blah = undefined :: Bar Foo
549
550 If we expand `Bar Foo` immediately, we'll miss the fact that the `Foo` type
551 synonyms is unsaturated.
552 * If one never expands and only checks the arguments, then one can miss
553 erroneous programs like the one in #16059:
554
555 type Foo b = Eq b => b
556 f :: forall b (a :: Foo b). Int
557
558 The kind of `a` contains a constraint, which is illegal, but this will only
559 be caught if `Foo b` is expanded.
560
561 Therefore, it's impossible to have these validity checks be simultaneously
562 correct and performant if one sticks exclusively to a single `ExpandMode`. In
563 that case, the solution is to vary the `ExpandMode`s! In more detail:
564
565 1. When we start validity checking, we start with `Expand` if
566 LiberalTypeSynonyms is enabled (see Note [Liberal type synonyms] for why we
567 do this), and we start with `Both` otherwise. The `initialExpandMode`
568 function is responsible for this.
569 2. When expanding an application of a type synonym (in `check_syn_tc_app`), we
570 determine which things to check based on the current `ExpandMode` argument.
571 Importantly, if the current mode is `Both`, then we check the arguments in
572 `NoExpand` mode and check the expanded type in `Both` mode.
573
574 Switching to `NoExpand` when checking the arguments is vital to avoid
575 exponential blowup. One consequence of this choice is that if you have
576 the following type synonym in one module (with RankNTypes enabled):
577
578 {-# LANGUAGE RankNTypes #-}
579 module A where
580 type A = forall a. a
581
582 And you define the following in a separate module *without* RankNTypes
583 enabled:
584
585 module B where
586
587 import A
588
589 type Const a b = a
590 f :: Const Int A -> Int
591
592 Then `f` will be accepted, even though `A` (which is technically a rank-n
593 type) appears in its type. We view this as an acceptable compromise, since
594 `A` never appears in the type of `f` post-expansion. If `A` _did_ appear in
595 a type post-expansion, such as in the following variant:
596
597 g :: Const A A -> Int
598
599 Then that would be rejected unless RankNTypes were enabled.
600 -}
601
602 -- | When validity-checking an application of a type synonym, should we
603 -- check the arguments, check the expanded type, or both?
604 -- See Note [Correctness and performance of type synonym validity checking]
605 data ExpandMode
606 = Expand -- ^ Only check the expanded type.
607 | NoExpand -- ^ Only check the arguments.
608 | Both -- ^ Check both the arguments and the expanded type.
609
610 instance Outputable ExpandMode where
611 ppr e = text $ case e of
612 Expand -> "Expand"
613 NoExpand -> "NoExpand"
614 Both -> "Both"
615
616 -- | If @LiberalTypeSynonyms@ is enabled, we start in 'Expand' mode for the
617 -- reasons explained in @Note [Liberal type synonyms]@. Otherwise, we start
618 -- in 'Both' mode.
619 initialExpandMode :: TcM ExpandMode
620 initialExpandMode = do
621 liberal_flag <- xoptM LangExt.LiberalTypeSynonyms
622 pure $ if liberal_flag then Expand else Both
623
624 -- | Information about a type being validity-checked.
625 data ValidityEnv = ValidityEnv
626 { ve_tidy_env :: TidyEnv
627 , ve_ctxt :: UserTypeCtxt
628 , ve_rank :: Rank
629 , ve_expand :: ExpandMode }
630
631 instance Outputable ValidityEnv where
632 ppr (ValidityEnv{ ve_tidy_env = env, ve_ctxt = ctxt
633 , ve_rank = rank, ve_expand = expand }) =
634 hang (text "ValidityEnv")
635 2 (vcat [ text "ve_tidy_env" <+> ppr env
636 , text "ve_ctxt" <+> pprUserTypeCtxt ctxt
637 , text "ve_rank" <+> ppr rank
638 , text "ve_expand" <+> ppr expand ])
639
640 ----------------------------------------
641 check_type :: ValidityEnv -> Type -> TcM ()
642 -- The args say what the *type context* requires, independent
643 -- of *flag* settings. You test the flag settings at usage sites.
644 --
645 -- Rank is allowed rank for function args
646 -- Rank 0 means no for-alls anywhere
647
648 check_type _ (TyVarTy _) = return ()
649
650 check_type ve (AppTy ty1 ty2)
651 = do { check_type ve ty1
652 ; check_arg_type False ve ty2 }
653
654 check_type ve ty@(TyConApp tc tys)
655 | isTypeSynonymTyCon tc || isTypeFamilyTyCon tc
656 = check_syn_tc_app ve ty tc tys
657 | isUnboxedTupleTyCon tc = check_ubx_tuple ve ty tys
658 | otherwise = mapM_ (check_arg_type False ve) tys
659
660 check_type _ (LitTy {}) = return ()
661
662 check_type ve (CastTy ty _) = check_type ve ty
663
664 -- Check for rank-n types, such as (forall x. x -> x) or (Show x => x).
665 --
666 -- Critically, this case must come *after* the case for TyConApp.
667 -- See Note [Liberal type synonyms].
668 check_type ve@(ValidityEnv{ ve_tidy_env = env, ve_ctxt = ctxt
669 , ve_rank = rank, ve_expand = expand }) ty
670 | not (null tvbs && null theta)
671 = do { traceTc "check_type" (ppr ty $$ ppr (forAllAllowed rank))
672 ; checkTcM (forAllAllowed rank) (forAllTyErr env rank ty)
673 -- Reject e.g. (Maybe (?x::Int => Int)),
674 -- with a decent error message
675
676 ; checkConstraintsOK ve theta ty
677 -- Reject forall (a :: Eq b => b). blah
678 -- In a kind signature we don't allow constraints
679
680 ; checkTcM (all (isInvisibleArgFlag . binderArgFlag) tvbs
681 || vdqAllowed ctxt)
682 (illegalVDQTyErr env ty)
683 -- Reject visible, dependent quantification in the type of a
684 -- term (e.g., `f :: forall a -> a -> Maybe a`)
685
686 ; check_valid_theta env' SigmaCtxt expand theta
687 -- Allow type T = ?x::Int => Int -> Int
688 -- but not type T = ?x::Int
689
690 ; check_type (ve{ve_tidy_env = env'}) tau
691 -- Allow foralls to right of arrow
692
693 ; checkEscapingKind env' tvbs' theta tau }
694 where
695 (tvbs, phi) = tcSplitForAllVarBndrs ty
696 (theta, tau) = tcSplitPhiTy phi
697 (env', tvbs') = tidyTyCoVarBinders env tvbs
698
699 check_type (ve@ValidityEnv{ve_rank = rank}) (FunTy _ arg_ty res_ty)
700 = do { check_type (ve{ve_rank = arg_rank}) arg_ty
701 ; check_type (ve{ve_rank = res_rank}) res_ty }
702 where
703 (arg_rank, res_rank) = funArgResRank rank
704
705 check_type _ ty = pprPanic "check_type" (ppr ty)
706
707 ----------------------------------------
708 check_syn_tc_app :: ValidityEnv
709 -> KindOrType -> TyCon -> [KindOrType] -> TcM ()
710 -- Used for type synonyms and type synonym families,
711 -- which must be saturated,
712 -- but not data families, which need not be saturated
713 check_syn_tc_app (ve@ValidityEnv{ ve_ctxt = ctxt, ve_expand = expand })
714 ty tc tys
715 | tys `lengthAtLeast` tc_arity -- Saturated
716 -- Check that the synonym has enough args
717 -- This applies equally to open and closed synonyms
718 -- It's OK to have an *over-applied* type synonym
719 -- data Tree a b = ...
720 -- type Foo a = Tree [a]
721 -- f :: Foo a b -> ...
722 = case expand of
723 _ | isTypeFamilyTyCon tc
724 -> check_args_only expand
725 -- See Note [Correctness and performance of type synonym validity
726 -- checking]
727 Expand -> check_expansion_only expand
728 NoExpand -> check_args_only expand
729 Both -> check_args_only NoExpand *> check_expansion_only Both
730
731 | GhciCtxt True <- ctxt -- Accept outermost under-saturated type synonym or
732 -- type family constructors in GHCi :kind commands.
733 -- See Note [Unsaturated type synonyms in GHCi]
734 = check_args_only expand
735
736 | otherwise
737 = failWithTc (tyConArityErr tc tys)
738 where
739 tc_arity = tyConArity tc
740
741 check_arg :: ExpandMode -> KindOrType -> TcM ()
742 check_arg expand =
743 check_arg_type (isTypeSynonymTyCon tc) (ve{ve_expand = expand})
744
745 check_args_only, check_expansion_only :: ExpandMode -> TcM ()
746 check_args_only expand = mapM_ (check_arg expand) tys
747
748 check_expansion_only expand
749 = ASSERT2( isTypeSynonymTyCon tc, ppr tc )
750 case tcView ty of
751 Just ty' -> let err_ctxt = text "In the expansion of type synonym"
752 <+> quotes (ppr tc)
753 in addErrCtxt err_ctxt $
754 check_type (ve{ve_expand = expand}) ty'
755 Nothing -> pprPanic "check_syn_tc_app" (ppr ty)
756
757 {-
758 Note [Unsaturated type synonyms in GHCi]
759 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
760 Generally speaking, GHC disallows unsaturated uses of type synonyms or type
761 families. For instance, if one defines `type Const a b = a`, then GHC will not
762 permit using `Const` unless it is applied to (at least) two arguments. There is
763 an exception to this rule, however: GHCi's :kind command. For instance, it
764 is quite common to look up the kind of a type constructor like so:
765
766 λ> :kind Const
767 Const :: j -> k -> j
768 λ> :kind Const Int
769 Const Int :: k -> Type
770
771 Strictly speaking, the two uses of `Const` above are unsaturated, but this
772 is an extremely benign (and useful) example of unsaturation, so we allow it
773 here as a special case.
774
775 That being said, we do not allow unsaturation carte blanche in GHCi. Otherwise,
776 this GHCi interaction would be possible:
777
778 λ> newtype Fix f = MkFix (f (Fix f))
779 λ> type Id a = a
780 λ> :kind Fix Id
781 Fix Id :: Type
782
783 This is rather dodgy, so we move to disallow this. We only permit unsaturated
784 synonyms in GHCi if they are *top-level*—that is, if the synonym is the
785 outermost type being applied. This allows `Const` and `Const Int` in the
786 first example, but not `Fix Id` in the second example, as `Id` is not the
787 outermost type being applied (`Fix` is).
788
789 We track this outermost property in the GhciCtxt constructor of UserTypeCtxt.
790 A field of True in GhciCtxt indicates that we're in an outermost position. Any
791 time we invoke `check_arg` to check the validity of an argument, we switch the
792 field to False.
793 -}
794
795 ----------------------------------------
796 check_ubx_tuple :: ValidityEnv -> KindOrType -> [KindOrType] -> TcM ()
797 check_ubx_tuple (ve@ValidityEnv{ve_tidy_env = env}) ty tys
798 = do { ub_tuples_allowed <- xoptM LangExt.UnboxedTuples
799 ; checkTcM ub_tuples_allowed (ubxArgTyErr env ty)
800
801 ; impred <- xoptM LangExt.ImpredicativeTypes
802 ; let rank' = if impred then ArbitraryRank else tyConArgMonoType
803 -- c.f. check_arg_type
804 -- However, args are allowed to be unlifted, or
805 -- more unboxed tuples, so can't use check_arg_ty
806 ; mapM_ (check_type (ve{ve_rank = rank'})) tys }
807
808 ----------------------------------------
809 check_arg_type
810 :: Bool -- ^ Is this the argument to a type synonym?
811 -> ValidityEnv -> KindOrType -> TcM ()
812 -- The sort of type that can instantiate a type variable,
813 -- or be the argument of a type constructor.
814 -- Not an unboxed tuple, but now *can* be a forall (since impredicativity)
815 -- Other unboxed types are very occasionally allowed as type
816 -- arguments depending on the kind of the type constructor
817 --
818 -- For example, we want to reject things like:
819 --
820 -- instance Ord a => Ord (forall s. T s a)
821 -- and
822 -- g :: T s (forall b.b)
823 --
824 -- NB: unboxed tuples can have polymorphic or unboxed args.
825 -- This happens in the workers for functions returning
826 -- product types with polymorphic components.
827 -- But not in user code.
828 -- Anyway, they are dealt with by a special case in check_tau_type
829
830 check_arg_type _ _ (CoercionTy {}) = return ()
831
832 check_arg_type type_syn (ve@ValidityEnv{ve_ctxt = ctxt, ve_rank = rank}) ty
833 = do { impred <- xoptM LangExt.ImpredicativeTypes
834 ; let rank' = case rank of -- Predictive => must be monotype
835 -- Rank-n arguments to type synonyms are OK, provided
836 -- that LiberalTypeSynonyms is enabled.
837 _ | type_syn -> synArgMonoType
838 MustBeMonoType -> MustBeMonoType -- Monotype, regardless
839 _other | impred -> ArbitraryRank
840 | otherwise -> tyConArgMonoType
841 -- Make sure that MustBeMonoType is propagated,
842 -- so that we don't suggest -XImpredicativeTypes in
843 -- (Ord (forall a.a)) => a -> a
844 -- and so that if it Must be a monotype, we check that it is!
845 ctxt' :: UserTypeCtxt
846 ctxt'
847 | GhciCtxt _ <- ctxt = GhciCtxt False
848 -- When checking an argument, set the field of GhciCtxt to
849 -- False to indicate that we are no longer in an outermost
850 -- position (and thus unsaturated synonyms are no longer
851 -- allowed).
852 -- See Note [Unsaturated type synonyms in GHCi]
853 | otherwise = ctxt
854
855 ; check_type (ve{ve_ctxt = ctxt', ve_rank = rank'}) ty }
856
857 ----------------------------------------
858 forAllTyErr :: TidyEnv -> Rank -> Type -> (TidyEnv, SDoc)
859 forAllTyErr env rank ty
860 = ( env
861 , vcat [ hang herald 2 (ppr_tidy env ty)
862 , suggestion ] )
863 where
864 (tvs, _theta, _tau) = tcSplitSigmaTy ty
865 herald | null tvs = text "Illegal qualified type:"
866 | otherwise = text "Illegal polymorphic type:"
867 suggestion = case rank of
868 LimitedRank {} -> text "Perhaps you intended to use RankNTypes"
869 MonoType d -> d
870 _ -> Outputable.empty -- Polytype is always illegal
871
872 -- | Reject type variables that would escape their escape through a kind.
873 -- See @Note [Type variables escaping through kinds]@.
874 checkEscapingKind :: TidyEnv -> [TyVarBinder] -> ThetaType -> Type -> TcM ()
875 checkEscapingKind env tvbs theta tau =
876 case occCheckExpand (binderVars tvbs) phi_kind of
877 -- Ensure that none of the tvs occur in the kind of the forall
878 -- /after/ expanding type synonyms.
879 -- See Note [Phantom type variables in kinds] in Type
880 Nothing -> failWithTcM $ forAllEscapeErr env tvbs theta tau tau_kind
881 Just _ -> pure ()
882 where
883 tau_kind = tcTypeKind tau
884 phi_kind | null theta = tau_kind
885 | otherwise = liftedTypeKind
886 -- If there are any constraints, the kind is *. (#11405)
887
888 forAllEscapeErr :: TidyEnv -> [TyVarBinder] -> ThetaType -> Type -> Kind
889 -> (TidyEnv, SDoc)
890 forAllEscapeErr env tvbs theta tau tau_kind
891 = ( env
892 , vcat [ hang (text "Quantified type's kind mentions quantified type variable")
893 2 (text "type:" <+> quotes (ppr (mkSigmaTy tvbs theta tau)))
894 -- NB: Don't tidy this type since the tvbs were already tidied
895 -- previously, and re-tidying them will make the names of type
896 -- variables different from tau_kind.
897 , hang (text "where the body of the forall has this kind:")
898 2 (quotes (ppr_tidy env tau_kind)) ] )
899
900 {-
901 Note [Type variables escaping through kinds]
902 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
903 Consider:
904
905 type family T (r :: RuntimeRep) :: TYPE r
906 foo :: forall r. T r
907
908 Something smells funny about the type of `foo`. If you spell out the kind
909 explicitly, it becomes clearer from where the smell originates:
910
911 foo :: ((forall r. T r) :: TYPE r)
912
913 The type variable `r` appears in the result kind, which escapes the scope of
914 its binding site! This is not desirable, so we establish a validity check
915 (`checkEscapingKind`) to catch any type variables that might escape through
916 kinds in this way.
917 -}
918
919 ubxArgTyErr :: TidyEnv -> Type -> (TidyEnv, SDoc)
920 ubxArgTyErr env ty
921 = ( env, vcat [ sep [ text "Illegal unboxed tuple type as function argument:"
922 , ppr_tidy env ty ]
923 , text "Perhaps you intended to use UnboxedTuples" ] )
924
925 checkConstraintsOK :: ValidityEnv -> ThetaType -> Type -> TcM ()
926 checkConstraintsOK ve theta ty
927 | null theta = return ()
928 | allConstraintsAllowed (ve_ctxt ve) = return ()
929 | otherwise
930 = -- We are in a kind, where we allow only equality predicates
931 -- See Note [Constraints in kinds] in TyCoRep, and #16263
932 checkTcM (all isEqPred theta) $
933 constraintTyErr (ve_tidy_env ve) ty
934
935 constraintTyErr :: TidyEnv -> Type -> (TidyEnv, SDoc)
936 constraintTyErr env ty
937 = (env, text "Illegal constraint in a kind:" <+> ppr_tidy env ty)
938
939 -- | Reject a use of visible, dependent quantification in the type of a term.
940 illegalVDQTyErr :: TidyEnv -> Type -> (TidyEnv, SDoc)
941 illegalVDQTyErr env ty =
942 (env, vcat
943 [ hang (text "Illegal visible, dependent quantification" <+>
944 text "in the type of a term:")
945 2 (ppr_tidy env ty)
946 , text "(GHC does not yet support this)" ] )
947
948 {-
949 Note [Liberal type synonyms]
950 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
951 If -XLiberalTypeSynonyms is on, expand closed type synonyms *before*
952 doing validity checking. This allows us to instantiate a synonym defn
953 with a for-all type, or with a partially-applied type synonym.
954 e.g. type T a b = a
955 type S m = m ()
956 f :: S (T Int)
957 Here, T is partially applied, so it's illegal in H98. But if you
958 expand S first, then T we get just
959 f :: Int
960 which is fine.
961
962 IMPORTANT: suppose T is a type synonym. Then we must do validity
963 checking on an appliation (T ty1 ty2)
964
965 *either* before expansion (i.e. check ty1, ty2)
966 *or* after expansion (i.e. expand T ty1 ty2, and then check)
967 BUT NOT BOTH
968
969 If we do both, we get exponential behaviour!!
970
971 data TIACons1 i r c = c i ::: r c
972 type TIACons2 t x = TIACons1 t (TIACons1 t x)
973 type TIACons3 t x = TIACons2 t (TIACons1 t x)
974 type TIACons4 t x = TIACons2 t (TIACons2 t x)
975 type TIACons7 t x = TIACons4 t (TIACons3 t x)
976
977 The order in which you do validity checking is also somewhat delicate. Consider
978 the `check_type` function, which drives the validity checking for unsaturated
979 uses of type synonyms. There is a special case for rank-n types, such as
980 (forall x. x -> x) or (Show x => x), since those require at least one language
981 extension to use. It used to be the case that this case came before every other
982 case, but this can lead to bugs. Imagine you have this scenario (from #15954):
983
984 type A a = Int
985 type B (a :: Type -> Type) = forall x. x -> x
986 type C = B A
987
988 If the rank-n case came first, then in the process of checking for `forall`s
989 or contexts, we would expand away `B A` to `forall x. x -> x`. This is because
990 the functions that split apart `forall`s/contexts
991 (tcSplitForAllVarBndrs/tcSplitPhiTy) expand type synonyms! If `B A` is expanded
992 away to `forall x. x -> x` before the actually validity checks occur, we will
993 have completely obfuscated the fact that we had an unsaturated application of
994 the `A` type synonym.
995
996 We have since learned from our mistakes and now put this rank-n case /after/
997 the case for TyConApp, which ensures that an unsaturated `A` TyConApp will be
998 caught properly. But be careful! We can't make the rank-n case /last/ either,
999 as the FunTy case must came after the rank-n case. Otherwise, something like
1000 (Eq a => Int) would be treated as a function type (FunTy), which just
1001 wouldn't do.
1002
1003 ************************************************************************
1004 * *
1005 \subsection{Checking a theta or source type}
1006 * *
1007 ************************************************************************
1008
1009 Note [Implicit parameters in instance decls]
1010 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1011 Implicit parameters _only_ allowed in type signatures; not in instance
1012 decls, superclasses etc. The reason for not allowing implicit params in
1013 instances is a bit subtle. If we allowed
1014 instance (?x::Int, Eq a) => Foo [a] where ...
1015 then when we saw
1016 (e :: (?x::Int) => t)
1017 it would be unclear how to discharge all the potential uses of the ?x
1018 in e. For example, a constraint Foo [Int] might come out of e, and
1019 applying the instance decl would show up two uses of ?x. #8912.
1020 -}
1021
1022 checkValidTheta :: UserTypeCtxt -> ThetaType -> TcM ()
1023 -- Assumes argument is fully zonked
1024 checkValidTheta ctxt theta
1025 = addErrCtxtM (checkThetaCtxt ctxt theta) $
1026 do { env <- tcInitOpenTidyEnv (tyCoVarsOfTypesList theta)
1027 ; expand <- initialExpandMode
1028 ; check_valid_theta env ctxt expand theta }
1029
1030 -------------------------
1031 check_valid_theta :: TidyEnv -> UserTypeCtxt -> ExpandMode
1032 -> [PredType] -> TcM ()
1033 check_valid_theta _ _ _ []
1034 = return ()
1035 check_valid_theta env ctxt expand theta
1036 = do { dflags <- getDynFlags
1037 ; warnTcM (Reason Opt_WarnDuplicateConstraints)
1038 (wopt Opt_WarnDuplicateConstraints dflags && notNull dups)
1039 (dupPredWarn env dups)
1040 ; traceTc "check_valid_theta" (ppr theta)
1041 ; mapM_ (check_pred_ty env dflags ctxt expand) theta }
1042 where
1043 (_,dups) = removeDups nonDetCmpType theta
1044 -- It's OK to use nonDetCmpType because dups only appears in the
1045 -- warning
1046
1047 -------------------------
1048 {- Note [Validity checking for constraints]
1049 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1050 We look through constraint synonyms so that we can see the underlying
1051 constraint(s). For example
1052 type Foo = ?x::Int
1053 instance Foo => C T
1054 We should reject the instance because it has an implicit parameter in
1055 the context.
1056
1057 But we record, in 'under_syn', whether we have looked under a synonym
1058 to avoid requiring language extensions at the use site. Main example
1059 (#9838):
1060
1061 {-# LANGUAGE ConstraintKinds #-}
1062 module A where
1063 type EqShow a = (Eq a, Show a)
1064
1065 module B where
1066 import A
1067 foo :: EqShow a => a -> String
1068
1069 We don't want to require ConstraintKinds in module B.
1070 -}
1071
1072 check_pred_ty :: TidyEnv -> DynFlags -> UserTypeCtxt -> ExpandMode
1073 -> PredType -> TcM ()
1074 -- Check the validity of a predicate in a signature
1075 -- See Note [Validity checking for constraints]
1076 check_pred_ty env dflags ctxt expand pred
1077 = do { check_type ve pred
1078 ; check_pred_help False env dflags ctxt pred }
1079 where
1080 rank | xopt LangExt.QuantifiedConstraints dflags
1081 = ArbitraryRank
1082 | otherwise
1083 = constraintMonoType
1084
1085 ve :: ValidityEnv
1086 ve = ValidityEnv{ ve_tidy_env = env
1087 , ve_ctxt = SigmaCtxt
1088 , ve_rank = rank
1089 , ve_expand = expand }
1090
1091 check_pred_help :: Bool -- True <=> under a type synonym
1092 -> TidyEnv
1093 -> DynFlags -> UserTypeCtxt
1094 -> PredType -> TcM ()
1095 check_pred_help under_syn env dflags ctxt pred
1096 | Just pred' <- tcView pred -- Switch on under_syn when going under a
1097 -- synonym (#9838, yuk)
1098 = check_pred_help True env dflags ctxt pred'
1099
1100 | otherwise -- A bit like classifyPredType, but not the same
1101 -- E.g. we treat (~) like (~#); and we look inside tuples
1102 = case classifyPredType pred of
1103 ClassPred cls tys
1104 | isCTupleClass cls -> check_tuple_pred under_syn env dflags ctxt pred tys
1105 | otherwise -> check_class_pred env dflags ctxt pred cls tys
1106
1107 EqPred NomEq _ _ -> -- a ~# b
1108 check_eq_pred env dflags pred
1109
1110 EqPred ReprEq _ _ -> -- Ugh! When inferring types we may get
1111 -- f :: (a ~R# b) => blha
1112 -- And we want to treat that like (Coercible a b)
1113 -- We should probably check argument shapes, but we
1114 -- didn't do so before, so I'm leaving it for now
1115 return ()
1116
1117 ForAllPred _ theta head -> check_quant_pred env dflags ctxt pred theta head
1118 IrredPred {} -> check_irred_pred under_syn env dflags ctxt pred
1119
1120 check_eq_pred :: TidyEnv -> DynFlags -> PredType -> TcM ()
1121 check_eq_pred env dflags pred
1122 = -- Equational constraints are valid in all contexts if type
1123 -- families are permitted
1124 checkTcM (xopt LangExt.TypeFamilies dflags
1125 || xopt LangExt.GADTs dflags)
1126 (eqPredTyErr env pred)
1127
1128 check_quant_pred :: TidyEnv -> DynFlags -> UserTypeCtxt
1129 -> PredType -> ThetaType -> PredType -> TcM ()
1130 check_quant_pred env dflags _ctxt pred theta head_pred
1131 = addErrCtxt (text "In the quantified constraint" <+> quotes (ppr pred)) $
1132 do { -- Check the instance head
1133 case classifyPredType head_pred of
1134 ClassPred cls tys -> checkValidInstHead SigmaCtxt cls tys
1135 -- SigmaCtxt tells checkValidInstHead that
1136 -- this is the head of a quantified constraint
1137 IrredPred {} | hasTyVarHead head_pred
1138 -> return ()
1139 _ -> failWithTcM (badQuantHeadErr env pred)
1140
1141 -- Check for termination
1142 ; unless (xopt LangExt.UndecidableInstances dflags) $
1143 checkInstTermination theta head_pred
1144 }
1145
1146 check_tuple_pred :: Bool -> TidyEnv -> DynFlags -> UserTypeCtxt -> PredType -> [PredType] -> TcM ()
1147 check_tuple_pred under_syn env dflags ctxt pred ts
1148 = do { -- See Note [ConstraintKinds in predicates]
1149 checkTcM (under_syn || xopt LangExt.ConstraintKinds dflags)
1150 (predTupleErr env pred)
1151 ; mapM_ (check_pred_help under_syn env dflags ctxt) ts }
1152 -- This case will not normally be executed because without
1153 -- -XConstraintKinds tuple types are only kind-checked as *
1154
1155 check_irred_pred :: Bool -> TidyEnv -> DynFlags -> UserTypeCtxt -> PredType -> TcM ()
1156 check_irred_pred under_syn env dflags ctxt pred
1157 -- The predicate looks like (X t1 t2) or (x t1 t2) :: Constraint
1158 -- where X is a type function
1159 = do { -- If it looks like (x t1 t2), require ConstraintKinds
1160 -- see Note [ConstraintKinds in predicates]
1161 -- But (X t1 t2) is always ok because we just require ConstraintKinds
1162 -- at the definition site (#9838)
1163 failIfTcM (not under_syn && not (xopt LangExt.ConstraintKinds dflags)
1164 && hasTyVarHead pred)
1165 (predIrredErr env pred)
1166
1167 -- Make sure it is OK to have an irred pred in this context
1168 -- See Note [Irreducible predicates in superclasses]
1169 ; failIfTcM (is_superclass ctxt
1170 && not (xopt LangExt.UndecidableInstances dflags)
1171 && has_tyfun_head pred)
1172 (predSuperClassErr env pred) }
1173 where
1174 is_superclass ctxt = case ctxt of { ClassSCCtxt _ -> True; _ -> False }
1175 has_tyfun_head ty
1176 = case tcSplitTyConApp_maybe ty of
1177 Just (tc, _) -> isTypeFamilyTyCon tc
1178 Nothing -> False
1179
1180 {- Note [ConstraintKinds in predicates]
1181 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1182 Don't check for -XConstraintKinds under a type synonym, because that
1183 was done at the type synonym definition site; see #9838
1184 e.g. module A where
1185 type C a = (Eq a, Ix a) -- Needs -XConstraintKinds
1186 module B where
1187 import A
1188 f :: C a => a -> a -- Does *not* need -XConstraintKinds
1189
1190 Note [Irreducible predicates in superclasses]
1191 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1192 Allowing type-family calls in class superclasses is somewhat dangerous
1193 because we can write:
1194
1195 type family Fooish x :: * -> Constraint
1196 type instance Fooish () = Foo
1197 class Fooish () a => Foo a where
1198
1199 This will cause the constraint simplifier to loop because every time we canonicalise a
1200 (Foo a) class constraint we add a (Fooish () a) constraint which will be immediately
1201 solved to add+canonicalise another (Foo a) constraint. -}
1202
1203 -------------------------
1204 check_class_pred :: TidyEnv -> DynFlags -> UserTypeCtxt
1205 -> PredType -> Class -> [TcType] -> TcM ()
1206 check_class_pred env dflags ctxt pred cls tys
1207 | isEqPredClass cls -- (~) and (~~) are classified as classes,
1208 -- but here we want to treat them as equalities
1209 = -- pprTrace "check_class" (ppr cls) $
1210 check_eq_pred env dflags pred
1211
1212 | isIPClass cls
1213 = do { check_arity
1214 ; checkTcM (okIPCtxt ctxt) (badIPPred env pred) }
1215
1216 | otherwise -- Includes Coercible
1217 = do { check_arity
1218 ; checkSimplifiableClassConstraint env dflags ctxt cls tys
1219 ; checkTcM arg_tys_ok (predTyVarErr env pred) }
1220 where
1221 check_arity = checkTc (tys `lengthIs` classArity cls)
1222 (tyConArityErr (classTyCon cls) tys)
1223
1224 -- Check the arguments of a class constraint
1225 flexible_contexts = xopt LangExt.FlexibleContexts dflags
1226 undecidable_ok = xopt LangExt.UndecidableInstances dflags
1227 arg_tys_ok = case ctxt of
1228 SpecInstCtxt -> True -- {-# SPECIALISE instance Eq (T Int) #-} is fine
1229 InstDeclCtxt {} -> checkValidClsArgs (flexible_contexts || undecidable_ok) cls tys
1230 -- Further checks on head and theta
1231 -- in checkInstTermination
1232 _ -> checkValidClsArgs flexible_contexts cls tys
1233
1234 checkSimplifiableClassConstraint :: TidyEnv -> DynFlags -> UserTypeCtxt
1235 -> Class -> [TcType] -> TcM ()
1236 -- See Note [Simplifiable given constraints]
1237 checkSimplifiableClassConstraint env dflags ctxt cls tys
1238 | not (wopt Opt_WarnSimplifiableClassConstraints dflags)
1239 = return ()
1240 | xopt LangExt.MonoLocalBinds dflags
1241 = return ()
1242
1243 | DataTyCtxt {} <- ctxt -- Don't do this check for the "stupid theta"
1244 = return () -- of a data type declaration
1245
1246 | cls `hasKey` coercibleTyConKey
1247 = return () -- Oddly, we treat (Coercible t1 t2) as unconditionally OK
1248 -- matchGlobalInst will reply "yes" because we can reduce
1249 -- (Coercible a b) to (a ~R# b)
1250
1251 | otherwise
1252 = do { result <- matchGlobalInst dflags False cls tys
1253 ; case result of
1254 OneInst { cir_what = what }
1255 -> addWarnTc (Reason Opt_WarnSimplifiableClassConstraints)
1256 (simplifiable_constraint_warn what)
1257 _ -> return () }
1258 where
1259 pred = mkClassPred cls tys
1260
1261 simplifiable_constraint_warn :: InstanceWhat -> SDoc
1262 simplifiable_constraint_warn what
1263 = vcat [ hang (text "The constraint" <+> quotes (ppr (tidyType env pred))
1264 <+> text "matches")
1265 2 (ppr_what what)
1266 , hang (text "This makes type inference for inner bindings fragile;")
1267 2 (text "either use MonoLocalBinds, or simplify it using the instance") ]
1268
1269 ppr_what BuiltinInstance = text "a built-in instance"
1270 ppr_what LocalInstance = text "a locally-quantified instance"
1271 ppr_what (TopLevInstance { iw_dfun_id = dfun })
1272 = hang (text "instance" <+> pprSigmaType (idType dfun))
1273 2 (text "--" <+> pprDefinedAt (idName dfun))
1274
1275
1276 {- Note [Simplifiable given constraints]
1277 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1278 A type signature like
1279 f :: Eq [(a,b)] => a -> b
1280 is very fragile, for reasons described at length in TcInteract
1281 Note [Instance and Given overlap]. As that Note discusses, for the
1282 most part the clever stuff in TcInteract means that we don't use a
1283 top-level instance if a local Given might fire, so there is no
1284 fragility. But if we /infer/ the type of a local let-binding, things
1285 can go wrong (#11948 is an example, discussed in the Note).
1286
1287 So this warning is switched on only if we have NoMonoLocalBinds; in
1288 that case the warning discourages users from writing simplifiable
1289 class constraints.
1290
1291 The warning only fires if the constraint in the signature
1292 matches the top-level instances in only one way, and with no
1293 unifiers -- that is, under the same circumstances that
1294 TcInteract.matchInstEnv fires an interaction with the top
1295 level instances. For example (#13526), consider
1296
1297 instance {-# OVERLAPPABLE #-} Eq (T a) where ...
1298 instance Eq (T Char) where ..
1299 f :: Eq (T a) => ...
1300
1301 We don't want to complain about this, even though the context
1302 (Eq (T a)) matches an instance, because the user may be
1303 deliberately deferring the choice so that the Eq (T Char)
1304 has a chance to fire when 'f' is called. And the fragility
1305 only matters when there's a risk that the instance might
1306 fire instead of the local 'given'; and there is no such
1307 risk in this case. Just use the same rules as for instance
1308 firing!
1309 -}
1310
1311 -------------------------
1312 okIPCtxt :: UserTypeCtxt -> Bool
1313 -- See Note [Implicit parameters in instance decls]
1314 okIPCtxt (FunSigCtxt {}) = True
1315 okIPCtxt (InfSigCtxt {}) = True
1316 okIPCtxt ExprSigCtxt = True
1317 okIPCtxt TypeAppCtxt = True
1318 okIPCtxt PatSigCtxt = True
1319 okIPCtxt ResSigCtxt = True
1320 okIPCtxt GenSigCtxt = True
1321 okIPCtxt (ConArgCtxt {}) = True
1322 okIPCtxt (ForSigCtxt {}) = True -- ??
1323 okIPCtxt ThBrackCtxt = True
1324 okIPCtxt (GhciCtxt {}) = True
1325 okIPCtxt SigmaCtxt = True
1326 okIPCtxt (DataTyCtxt {}) = True
1327 okIPCtxt (PatSynCtxt {}) = True
1328 okIPCtxt (TySynCtxt {}) = True -- e.g. type Blah = ?x::Int
1329 -- #11466
1330
1331 okIPCtxt (KindSigCtxt {}) = False
1332 okIPCtxt (ClassSCCtxt {}) = False
1333 okIPCtxt (InstDeclCtxt {}) = False
1334 okIPCtxt (SpecInstCtxt {}) = False
1335 okIPCtxt (RuleSigCtxt {}) = False
1336 okIPCtxt DefaultDeclCtxt = False
1337 okIPCtxt DerivClauseCtxt = False
1338 okIPCtxt (TyVarBndrKindCtxt {}) = False
1339 okIPCtxt (DataKindCtxt {}) = False
1340 okIPCtxt (TySynKindCtxt {}) = False
1341 okIPCtxt (TyFamResKindCtxt {}) = False
1342
1343 {-
1344 Note [Kind polymorphic type classes]
1345 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1346 MultiParam check:
1347
1348 class C f where... -- C :: forall k. k -> Constraint
1349 instance C Maybe where...
1350
1351 The dictionary gets type [C * Maybe] even if it's not a MultiParam
1352 type class.
1353
1354 Flexibility check:
1355
1356 class C f where... -- C :: forall k. k -> Constraint
1357 data D a = D a
1358 instance C D where
1359
1360 The dictionary gets type [C * (D *)]. IA0_TODO it should be
1361 generalized actually.
1362 -}
1363
1364 checkThetaCtxt :: UserTypeCtxt -> ThetaType -> TidyEnv -> TcM (TidyEnv, SDoc)
1365 checkThetaCtxt ctxt theta env
1366 = return ( env
1367 , vcat [ text "In the context:" <+> pprTheta (tidyTypes env theta)
1368 , text "While checking" <+> pprUserTypeCtxt ctxt ] )
1369
1370 eqPredTyErr, predTupleErr, predIrredErr,
1371 predSuperClassErr, badQuantHeadErr :: TidyEnv -> PredType -> (TidyEnv, SDoc)
1372 badQuantHeadErr env pred
1373 = ( env
1374 , hang (text "Quantified predicate must have a class or type variable head:")
1375 2 (ppr_tidy env pred) )
1376 eqPredTyErr env pred
1377 = ( env
1378 , text "Illegal equational constraint" <+> ppr_tidy env pred $$
1379 parens (text "Use GADTs or TypeFamilies to permit this") )
1380 predTupleErr env pred
1381 = ( env
1382 , hang (text "Illegal tuple constraint:" <+> ppr_tidy env pred)
1383 2 (parens constraintKindsMsg) )
1384 predIrredErr env pred
1385 = ( env
1386 , hang (text "Illegal constraint:" <+> ppr_tidy env pred)
1387 2 (parens constraintKindsMsg) )
1388 predSuperClassErr env pred
1389 = ( env
1390 , hang (text "Illegal constraint" <+> quotes (ppr_tidy env pred)
1391 <+> text "in a superclass context")
1392 2 (parens undecidableMsg) )
1393
1394 predTyVarErr :: TidyEnv -> PredType -> (TidyEnv, SDoc)
1395 predTyVarErr env pred
1396 = (env
1397 , vcat [ hang (text "Non type-variable argument")
1398 2 (text "in the constraint:" <+> ppr_tidy env pred)
1399 , parens (text "Use FlexibleContexts to permit this") ])
1400
1401 badIPPred :: TidyEnv -> PredType -> (TidyEnv, SDoc)
1402 badIPPred env pred
1403 = ( env
1404 , text "Illegal implicit parameter" <+> quotes (ppr_tidy env pred) )
1405
1406 constraintSynErr :: TidyEnv -> Type -> (TidyEnv, SDoc)
1407 constraintSynErr env kind
1408 = ( env
1409 , hang (text "Illegal constraint synonym of kind:" <+> quotes (ppr_tidy env kind))
1410 2 (parens constraintKindsMsg) )
1411
1412 dupPredWarn :: TidyEnv -> [NE.NonEmpty PredType] -> (TidyEnv, SDoc)
1413 dupPredWarn env dups
1414 = ( env
1415 , text "Duplicate constraint" <> plural primaryDups <> text ":"
1416 <+> pprWithCommas (ppr_tidy env) primaryDups )
1417 where
1418 primaryDups = map NE.head dups
1419
1420 tyConArityErr :: TyCon -> [TcType] -> SDoc
1421 -- For type-constructor arity errors, be careful to report
1422 -- the number of /visible/ arguments required and supplied,
1423 -- ignoring the /invisible/ arguments, which the user does not see.
1424 -- (e.g. #10516)
1425 tyConArityErr tc tks
1426 = arityErr (ppr (tyConFlavour tc)) (tyConName tc)
1427 tc_type_arity tc_type_args
1428 where
1429 vis_tks = filterOutInvisibleTypes tc tks
1430
1431 -- tc_type_arity = number of *type* args expected
1432 -- tc_type_args = number of *type* args encountered
1433 tc_type_arity = count isVisibleTyConBinder (tyConBinders tc)
1434 tc_type_args = length vis_tks
1435
1436 arityErr :: Outputable a => SDoc -> a -> Int -> Int -> SDoc
1437 arityErr what name n m
1438 = hsep [ text "The" <+> what, quotes (ppr name), text "should have",
1439 n_arguments <> comma, text "but has been given",
1440 if m==0 then text "none" else int m]
1441 where
1442 n_arguments | n == 0 = text "no arguments"
1443 | n == 1 = text "1 argument"
1444 | True = hsep [int n, text "arguments"]
1445
1446 {-
1447 ************************************************************************
1448 * *
1449 \subsection{Checking for a decent instance head type}
1450 * *
1451 ************************************************************************
1452
1453 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1454 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1455
1456 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1457 flag is on, or (2)~the instance is imported (they must have been
1458 compiled elsewhere). In these cases, we let them go through anyway.
1459
1460 We can also have instances for functions: @instance Foo (a -> b) ...@.
1461 -}
1462
1463 checkValidInstHead :: UserTypeCtxt -> Class -> [Type] -> TcM ()
1464 checkValidInstHead ctxt clas cls_args
1465 = do { dflags <- getDynFlags
1466 ; is_boot <- tcIsHsBootOrSig
1467 ; is_sig <- tcIsHsig
1468 ; check_valid_inst_head dflags is_boot is_sig ctxt clas cls_args
1469 }
1470
1471 {-
1472
1473 Note [Instances of built-in classes in signature files]
1474 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1475
1476 User defined instances for KnownNat, KnownSymbol and Typeable are
1477 disallowed -- they are generated when needed by GHC itself on-the-fly.
1478
1479 However, if they occur in a Backpack signature file, they have an
1480 entirely different meaning. Suppose in M.hsig we see
1481
1482 signature M where
1483 data T :: Nat
1484 instance KnownNat T
1485
1486 That says that any module satisfying M.hsig must provide a KnownNat
1487 instance for T. We absolultely need that instance when compiling a
1488 module that imports M.hsig: see #15379 and
1489 Note [Fabricating Evidence for Literals in Backpack] in ClsInst.
1490
1491 Hence, checkValidInstHead accepts a user-written instance declaration
1492 in hsig files, where `is_sig` is True.
1493
1494 -}
1495
1496 check_valid_inst_head :: DynFlags -> Bool -> Bool
1497 -> UserTypeCtxt -> Class -> [Type] -> TcM ()
1498 -- Wow! There are a surprising number of ad-hoc special cases here.
1499 check_valid_inst_head dflags is_boot is_sig ctxt clas cls_args
1500
1501 -- If not in an hs-boot file, abstract classes cannot have instances
1502 | isAbstractClass clas
1503 , not is_boot
1504 = failWithTc abstract_class_msg
1505
1506 -- For Typeable, don't complain about instances for
1507 -- standalone deriving; they are no-ops, and we warn about
1508 -- it in TcDeriv.deriveStandalone.
1509 | clas_nm == typeableClassName
1510 , not is_sig
1511 -- Note [Instances of built-in classes in signature files]
1512 , hand_written_bindings
1513 = failWithTc rejected_class_msg
1514
1515 -- Handwritten instances of KnownNat/KnownSymbol class
1516 -- are always forbidden (#12837)
1517 | clas_nm `elem` [ knownNatClassName, knownSymbolClassName ]
1518 , not is_sig
1519 -- Note [Instances of built-in classes in signature files]
1520 , hand_written_bindings
1521 = failWithTc rejected_class_msg
1522
1523 -- For the most part we don't allow
1524 -- instances for (~), (~~), or Coercible;
1525 -- but we DO want to allow them in quantified constraints:
1526 -- f :: (forall a b. Coercible a b => Coercible (m a) (m b)) => ...m...
1527 | clas_nm `elem` [ heqTyConName, eqTyConName, coercibleTyConName ]
1528 , not quantified_constraint
1529 = failWithTc rejected_class_msg
1530
1531 -- Check for hand-written Generic instances (disallowed in Safe Haskell)
1532 | clas_nm `elem` genericClassNames
1533 , hand_written_bindings
1534 = do { failIfTc (safeLanguageOn dflags) gen_inst_err
1535 ; when (safeInferOn dflags) (recordUnsafeInfer emptyBag) }
1536
1537 | clas_nm == hasFieldClassName
1538 = checkHasFieldInst clas cls_args
1539
1540 | isCTupleClass clas
1541 = failWithTc tuple_class_msg
1542
1543 -- Check language restrictions on the args to the class
1544 | check_h98_arg_shape
1545 , Just msg <- mb_ty_args_msg
1546 = failWithTc (instTypeErr clas cls_args msg)
1547
1548 | otherwise
1549 = checkValidTypePats (classTyCon clas) cls_args
1550 where
1551 clas_nm = getName clas
1552 ty_args = filterOutInvisibleTypes (classTyCon clas) cls_args
1553
1554 hand_written_bindings
1555 = case ctxt of
1556 InstDeclCtxt stand_alone -> not stand_alone
1557 SpecInstCtxt -> False
1558 DerivClauseCtxt -> False
1559 _ -> True
1560
1561 check_h98_arg_shape = case ctxt of
1562 SpecInstCtxt -> False
1563 DerivClauseCtxt -> False
1564 SigmaCtxt -> False
1565 _ -> True
1566 -- SigmaCtxt: once we are in quantified-constraint land, we
1567 -- aren't so picky about enforcing H98-language restrictions
1568 -- E.g. we want to allow a head like Coercible (m a) (m b)
1569
1570
1571 -- When we are looking at the head of a quantified constraint,
1572 -- check_quant_pred sets ctxt to SigmaCtxt
1573 quantified_constraint = case ctxt of
1574 SigmaCtxt -> True
1575 _ -> False
1576
1577 head_type_synonym_msg = parens (
1578 text "All instance types must be of the form (T t1 ... tn)" $$
1579 text "where T is not a synonym." $$
1580 text "Use TypeSynonymInstances if you want to disable this.")
1581
1582 head_type_args_tyvars_msg = parens (vcat [
1583 text "All instance types must be of the form (T a1 ... an)",
1584 text "where a1 ... an are *distinct type variables*,",
1585 text "and each type variable appears at most once in the instance head.",
1586 text "Use FlexibleInstances if you want to disable this."])
1587
1588 head_one_type_msg = parens $
1589 text "Only one type can be given in an instance head." $$
1590 text "Use MultiParamTypeClasses if you want to allow more, or zero."
1591
1592 rejected_class_msg = text "Class" <+> quotes (ppr clas_nm)
1593 <+> text "does not support user-specified instances"
1594 tuple_class_msg = text "You can't specify an instance for a tuple constraint"
1595
1596 gen_inst_err = rejected_class_msg $$ nest 2 (text "(in Safe Haskell)")
1597
1598 abstract_class_msg = text "Cannot define instance for abstract class"
1599 <+> quotes (ppr clas_nm)
1600
1601 mb_ty_args_msg
1602 | not (xopt LangExt.TypeSynonymInstances dflags)
1603 , not (all tcInstHeadTyNotSynonym ty_args)
1604 = Just head_type_synonym_msg
1605
1606 | not (xopt LangExt.FlexibleInstances dflags)
1607 , not (all tcInstHeadTyAppAllTyVars ty_args)
1608 = Just head_type_args_tyvars_msg
1609
1610 | length ty_args /= 1
1611 , not (xopt LangExt.MultiParamTypeClasses dflags)
1612 , not (xopt LangExt.NullaryTypeClasses dflags && null ty_args)
1613 = Just head_one_type_msg
1614
1615 | otherwise
1616 = Nothing
1617
1618 tcInstHeadTyNotSynonym :: Type -> Bool
1619 -- Used in Haskell-98 mode, for the argument types of an instance head
1620 -- These must not be type synonyms, but everywhere else type synonyms
1621 -- are transparent, so we need a special function here
1622 tcInstHeadTyNotSynonym ty
1623 = case ty of -- Do not use splitTyConApp,
1624 -- because that expands synonyms!
1625 TyConApp tc _ -> not (isTypeSynonymTyCon tc)
1626 _ -> True
1627
1628 tcInstHeadTyAppAllTyVars :: Type -> Bool
1629 -- Used in Haskell-98 mode, for the argument types of an instance head
1630 -- These must be a constructor applied to type variable arguments
1631 -- or a type-level literal.
1632 -- But we allow kind instantiations.
1633 tcInstHeadTyAppAllTyVars ty
1634 | Just (tc, tys) <- tcSplitTyConApp_maybe (dropCasts ty)
1635 = ok (filterOutInvisibleTypes tc tys) -- avoid kinds
1636 | LitTy _ <- ty = True -- accept type literals (#13833)
1637 | otherwise
1638 = False
1639 where
1640 -- Check that all the types are type variables,
1641 -- and that each is distinct
1642 ok tys = equalLength tvs tys && hasNoDups tvs
1643 where
1644 tvs = mapMaybe tcGetTyVar_maybe tys
1645
1646 dropCasts :: Type -> Type
1647 -- See Note [Casts during validity checking]
1648 -- This function can turn a well-kinded type into an ill-kinded
1649 -- one, so I've kept it local to this module
1650 -- To consider: drop only HoleCo casts
1651 dropCasts (CastTy ty _) = dropCasts ty
1652 dropCasts (AppTy t1 t2) = mkAppTy (dropCasts t1) (dropCasts t2)
1653 dropCasts ty@(FunTy _ t1 t2) = ty { ft_arg = dropCasts t1, ft_res = dropCasts t2 }
1654 dropCasts (TyConApp tc tys) = mkTyConApp tc (map dropCasts tys)
1655 dropCasts (ForAllTy b ty) = ForAllTy (dropCastsB b) (dropCasts ty)
1656 dropCasts ty = ty -- LitTy, TyVarTy, CoercionTy
1657
1658 dropCastsB :: TyVarBinder -> TyVarBinder
1659 dropCastsB b = b -- Don't bother in the kind of a forall
1660
1661 instTypeErr :: Class -> [Type] -> SDoc -> SDoc
1662 instTypeErr cls tys msg
1663 = hang (hang (text "Illegal instance declaration for")
1664 2 (quotes (pprClassPred cls tys)))
1665 2 msg
1666
1667 -- | See Note [Validity checking of HasField instances]
1668 checkHasFieldInst :: Class -> [Type] -> TcM ()
1669 checkHasFieldInst cls tys@[_k_ty, x_ty, r_ty, _a_ty] =
1670 case splitTyConApp_maybe r_ty of
1671 Nothing -> whoops (text "Record data type must be specified")
1672 Just (tc, _)
1673 | isFamilyTyCon tc
1674 -> whoops (text "Record data type may not be a data family")
1675 | otherwise -> case isStrLitTy x_ty of
1676 Just lbl
1677 | isJust (lookupTyConFieldLabel lbl tc)
1678 -> whoops (ppr tc <+> text "already has a field"
1679 <+> quotes (ppr lbl))
1680 | otherwise -> return ()
1681 Nothing
1682 | null (tyConFieldLabels tc) -> return ()
1683 | otherwise -> whoops (ppr tc <+> text "has fields")
1684 where
1685 whoops = addErrTc . instTypeErr cls tys
1686 checkHasFieldInst _ tys = pprPanic "checkHasFieldInst" (ppr tys)
1687
1688 {- Note [Casts during validity checking]
1689 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1690 Consider the (bogus)
1691 instance Eq Char#
1692 We elaborate to 'Eq (Char# |> UnivCo(hole))' where the hole is an
1693 insoluble equality constraint for * ~ #. We'll report the insoluble
1694 constraint separately, but we don't want to *also* complain that Eq is
1695 not applied to a type constructor. So we look gaily look through
1696 CastTys here.
1697
1698 Another example: Eq (Either a). Then we actually get a cast in
1699 the middle:
1700 Eq ((Either |> g) a)
1701
1702
1703 Note [Validity checking of HasField instances]
1704 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1705 The HasField class has magic constraint solving behaviour (see Note
1706 [HasField instances] in TcInteract). However, we permit users to
1707 declare their own instances, provided they do not clash with the
1708 built-in behaviour. In particular, we forbid:
1709
1710 1. `HasField _ r _` where r is a variable
1711
1712 2. `HasField _ (T ...) _` if T is a data family
1713 (because it might have fields introduced later)
1714
1715 3. `HasField x (T ...) _` where x is a variable,
1716 if T has any fields at all
1717
1718 4. `HasField "foo" (T ...) _` if T has a "foo" field
1719
1720 The usual functional dependency checks also apply.
1721
1722
1723 Note [Valid 'deriving' predicate]
1724 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1725 validDerivPred checks for OK 'deriving' context. See Note [Exotic
1726 derived instance contexts] in TcDeriv. However the predicate is
1727 here because it uses sizeTypes, fvTypes.
1728
1729 It checks for three things
1730
1731 * No repeated variables (hasNoDups fvs)
1732
1733 * No type constructors. This is done by comparing
1734 sizeTypes tys == length (fvTypes tys)
1735 sizeTypes counts variables and constructors; fvTypes returns variables.
1736 So if they are the same, there must be no constructors. But there
1737 might be applications thus (f (g x)).
1738
1739 Note that tys only includes the visible arguments of the class type
1740 constructor. Including the non-visible arguments can cause the following,
1741 perfectly valid instance to be rejected:
1742 class Category (cat :: k -> k -> *) where ...
1743 newtype T (c :: * -> * -> *) a b = MkT (c a b)
1744 instance Category c => Category (T c) where ...
1745 since the first argument to Category is a non-visible *, which sizeTypes
1746 would count as a constructor! See #11833.
1747
1748 * Also check for a bizarre corner case, when the derived instance decl
1749 would look like
1750 instance C a b => D (T a) where ...
1751 Note that 'b' isn't a parameter of T. This gives rise to all sorts of
1752 problems; in particular, it's hard to compare solutions for equality
1753 when finding the fixpoint, and that means the inferContext loop does
1754 not converge. See #5287.
1755
1756 Note [Equality class instances]
1757 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1758 We can't have users writing instances for the equality classes. But we
1759 still need to be able to write instances for them ourselves. So we allow
1760 instances only in the defining module.
1761
1762 -}
1763
1764 validDerivPred :: TyVarSet -> PredType -> Bool
1765 -- See Note [Valid 'deriving' predicate]
1766 validDerivPred tv_set pred
1767 = case classifyPredType pred of
1768 ClassPred cls tys -> cls `hasKey` typeableClassKey
1769 -- Typeable constraints are bigger than they appear due
1770 -- to kind polymorphism, but that's OK
1771 || check_tys cls tys
1772 EqPred {} -> False -- reject equality constraints
1773 _ -> True -- Non-class predicates are ok
1774 where
1775 check_tys cls tys
1776 = hasNoDups fvs
1777 -- use sizePred to ignore implicit args
1778 && lengthIs fvs (sizePred pred)
1779 && all (`elemVarSet` tv_set) fvs
1780 where tys' = filterOutInvisibleTypes (classTyCon cls) tys
1781 fvs = fvTypes tys'
1782
1783 {-
1784 ************************************************************************
1785 * *
1786 \subsection{Checking instance for termination}
1787 * *
1788 ************************************************************************
1789 -}
1790
1791 {- Note [Instances and constraint synonyms]
1792 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1793 Currently, we don't allow instances for constraint synonyms at all.
1794 Consider these (#13267):
1795 type C1 a = Show (a -> Bool)
1796 instance C1 Int where -- I1
1797 show _ = "ur"
1798
1799 This elicits "show is not a (visible) method of class C1", which isn't
1800 a great message. But it comes from the renamer, so it's hard to improve.
1801
1802 This needs a bit more care:
1803 type C2 a = (Show a, Show Int)
1804 instance C2 Int -- I2
1805
1806 If we use (splitTyConApp_maybe tau) in checkValidInstance to decompose
1807 the instance head, we'll expand the synonym on fly, and it'll look like
1808 instance (%,%) (Show Int, Show Int)
1809 and we /really/ don't want that. So we carefully do /not/ expand
1810 synonyms, by matching on TyConApp directly.
1811 -}
1812
1813 checkValidInstance :: UserTypeCtxt -> LHsSigType GhcRn -> Type -> TcM ()
1814 checkValidInstance ctxt hs_type ty
1815 | not is_tc_app
1816 = failWithTc (hang (text "Instance head is not headed by a class:")
1817 2 ( ppr tau))
1818
1819 | isNothing mb_cls
1820 = failWithTc (vcat [ text "Illegal instance for a" <+> ppr (tyConFlavour tc)
1821 , text "A class instance must be for a class" ])
1822
1823 | not arity_ok
1824 = failWithTc (text "Arity mis-match in instance head")
1825
1826 | otherwise
1827 = do { setSrcSpan head_loc $
1828 checkValidInstHead ctxt clas inst_tys
1829
1830 ; traceTc "checkValidInstance {" (ppr ty)
1831
1832 ; env0 <- tcInitTidyEnv
1833 ; expand <- initialExpandMode
1834 ; check_valid_theta env0 ctxt expand theta
1835
1836 -- The Termination and Coverate Conditions
1837 -- Check that instance inference will terminate (if we care)
1838 -- For Haskell 98 this will already have been done by checkValidTheta,
1839 -- but as we may be using other extensions we need to check.
1840 --
1841 -- Note that the Termination Condition is *more conservative* than
1842 -- the checkAmbiguity test we do on other type signatures
1843 -- e.g. Bar a => Bar Int is ambiguous, but it also fails
1844 -- the termination condition, because 'a' appears more often
1845 -- in the constraint than in the head
1846 ; undecidable_ok <- xoptM LangExt.UndecidableInstances
1847 ; if undecidable_ok
1848 then checkAmbiguity ctxt ty
1849 else checkInstTermination theta tau
1850
1851 ; traceTc "cvi 2" (ppr ty)
1852
1853 ; case (checkInstCoverage undecidable_ok clas theta inst_tys) of
1854 IsValid -> return () -- Check succeeded
1855 NotValid msg -> addErrTc (instTypeErr clas inst_tys msg)
1856
1857 ; traceTc "End checkValidInstance }" empty
1858
1859 ; return () }
1860 where
1861 (_tvs, theta, tau) = tcSplitSigmaTy ty
1862 is_tc_app = case tau of { TyConApp {} -> True; _ -> False }
1863 TyConApp tc inst_tys = tau -- See Note [Instances and constraint synonyms]
1864 mb_cls = tyConClass_maybe tc
1865 Just clas = mb_cls
1866 arity_ok = inst_tys `lengthIs` classArity clas
1867
1868 -- The location of the "head" of the instance
1869 head_loc = getLoc (getLHsInstDeclHead hs_type)
1870
1871 {-
1872 Note [Paterson conditions]
1873 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1874 Termination test: the so-called "Paterson conditions" (see Section 5 of
1875 "Understanding functional dependencies via Constraint Handling Rules,
1876 JFP Jan 2007).
1877
1878 We check that each assertion in the context satisfies:
1879 (1) no variable has more occurrences in the assertion than in the head, and
1880 (2) the assertion has fewer constructors and variables (taken together
1881 and counting repetitions) than the head.
1882 This is only needed with -fglasgow-exts, as Haskell 98 restrictions
1883 (which have already been checked) guarantee termination.
1884
1885 The underlying idea is that
1886
1887 for any ground substitution, each assertion in the
1888 context has fewer type constructors than the head.
1889 -}
1890
1891 checkInstTermination :: ThetaType -> TcPredType -> TcM ()
1892 -- See Note [Paterson conditions]
1893 checkInstTermination theta head_pred
1894 = check_preds emptyVarSet theta
1895 where
1896 head_fvs = fvType head_pred
1897 head_size = sizeType head_pred
1898
1899 check_preds :: VarSet -> [PredType] -> TcM ()
1900 check_preds foralld_tvs preds = mapM_ (check foralld_tvs) preds
1901
1902 check :: VarSet -> PredType -> TcM ()
1903 check foralld_tvs pred
1904 = case classifyPredType pred of
1905 EqPred {} -> return () -- See #4200.
1906 IrredPred {} -> check2 foralld_tvs pred (sizeType pred)
1907 ClassPred cls tys
1908 | isTerminatingClass cls
1909 -> return ()
1910
1911 | isCTupleClass cls -- Look inside tuple predicates; #8359
1912 -> check_preds foralld_tvs tys
1913
1914 | otherwise -- Other ClassPreds
1915 -> check2 foralld_tvs pred bogus_size
1916 where
1917 bogus_size = 1 + sizeTypes (filterOutInvisibleTypes (classTyCon cls) tys)
1918 -- See Note [Invisible arguments and termination]
1919
1920 ForAllPred tvs _ head_pred'
1921 -> check (foralld_tvs `extendVarSetList` binderVars tvs) head_pred'
1922 -- Termination of the quantified predicate itself is checked
1923 -- when the predicates are individually checked for validity
1924
1925 check2 foralld_tvs pred pred_size
1926 | not (null bad_tvs) = failWithTc (noMoreMsg bad_tvs what (ppr head_pred))
1927 | not (isTyFamFree pred) = failWithTc (nestedMsg what)
1928 | pred_size >= head_size = failWithTc (smallerMsg what (ppr head_pred))
1929 | otherwise = return ()
1930 -- isTyFamFree: see Note [Type families in instance contexts]
1931 where
1932 what = text "constraint" <+> quotes (ppr pred)
1933 bad_tvs = filterOut (`elemVarSet` foralld_tvs) (fvType pred)
1934 \\ head_fvs
1935
1936 smallerMsg :: SDoc -> SDoc -> SDoc
1937 smallerMsg what inst_head
1938 = vcat [ hang (text "The" <+> what)
1939 2 (sep [ text "is no smaller than"
1940 , text "the instance head" <+> quotes inst_head ])
1941 , parens undecidableMsg ]
1942
1943 noMoreMsg :: [TcTyVar] -> SDoc -> SDoc -> SDoc
1944 noMoreMsg tvs what inst_head
1945 = vcat [ hang (text "Variable" <> plural tvs1 <+> quotes (pprWithCommas ppr tvs1)
1946 <+> occurs <+> text "more often")
1947 2 (sep [ text "in the" <+> what
1948 , text "than in the instance head" <+> quotes inst_head ])
1949 , parens undecidableMsg ]
1950 where
1951 tvs1 = nub tvs
1952 occurs = if isSingleton tvs1 then text "occurs"
1953 else text "occur"
1954
1955 undecidableMsg, constraintKindsMsg :: SDoc
1956 undecidableMsg = text "Use UndecidableInstances to permit this"
1957 constraintKindsMsg = text "Use ConstraintKinds to permit this"
1958
1959 {- Note [Type families in instance contexts]
1960 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1961 Are these OK?
1962 type family F a
1963 instance F a => C (Maybe [a]) where ...
1964 intance C (F a) => C [[[a]]] where ...
1965
1966 No: the type family in the instance head might blow up to an
1967 arbitrarily large type, depending on how 'a' is instantiated.
1968 So we require UndecidableInstances if we have a type family
1969 in the instance head. #15172.
1970
1971 Note [Invisible arguments and termination]
1972 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1973 When checking the ​Paterson conditions for termination an instance
1974 declaration, we check for the number of "constructors and variables"
1975 in the instance head and constraints. Question: Do we look at
1976
1977 * All the arguments, visible or invisible?
1978 * Just the visible arguments?
1979
1980 I think both will ensure termination, provided we are consistent.
1981 Currently we are /not/ consistent, which is really a bug. It's
1982 described in #15177, which contains a number of examples.
1983 The suspicious bits are the calls to filterOutInvisibleTypes.
1984 -}
1985
1986
1987 {-
1988 ************************************************************************
1989 * *
1990 Checking type instance well-formedness and termination
1991 * *
1992 ************************************************************************
1993 -}
1994
1995 checkValidCoAxiom :: CoAxiom Branched -> TcM ()
1996 checkValidCoAxiom ax@(CoAxiom { co_ax_tc = fam_tc, co_ax_branches = branches })
1997 = do { mapM_ (checkValidCoAxBranch fam_tc) branch_list
1998 ; foldlM_ check_branch_compat [] branch_list }
1999 where
2000 branch_list = fromBranches branches
2001 injectivity = tyConInjectivityInfo fam_tc
2002
2003 check_branch_compat :: [CoAxBranch] -- previous branches in reverse order
2004 -> CoAxBranch -- current branch
2005 -> TcM [CoAxBranch]-- current branch : previous branches
2006 -- Check for
2007 -- (a) this branch is dominated by previous ones
2008 -- (b) failure of injectivity
2009 check_branch_compat prev_branches cur_branch
2010 | cur_branch `isDominatedBy` prev_branches
2011 = do { addWarnAt NoReason (coAxBranchSpan cur_branch) $
2012 inaccessibleCoAxBranch fam_tc cur_branch
2013 ; return prev_branches }
2014 | otherwise
2015 = do { check_injectivity prev_branches cur_branch
2016 ; return (cur_branch : prev_branches) }
2017
2018 -- Injectivity check: check whether a new (CoAxBranch) can extend
2019 -- already checked equations without violating injectivity
2020 -- annotation supplied by the user.
2021 -- See Note [Verifying injectivity annotation] in FamInstEnv
2022 check_injectivity prev_branches cur_branch
2023 | Injective inj <- injectivity
2024 = do { let conflicts =
2025 fst $ foldl' (gather_conflicts inj prev_branches cur_branch)
2026 ([], 0) prev_branches
2027 ; mapM_ (\(err, span) -> setSrcSpan span $ addErr err)
2028 (makeInjectivityErrors ax cur_branch inj conflicts) }
2029 | otherwise
2030 = return ()
2031
2032 gather_conflicts inj prev_branches cur_branch (acc, n) branch
2033 -- n is 0-based index of branch in prev_branches
2034 = case injectiveBranches inj cur_branch branch of
2035 -- Case 1B2 in Note [Verifying injectivity annotation] in FamInstEnv
2036 InjectivityUnified ax1 ax2
2037 | ax1 `isDominatedBy` (replace_br prev_branches n ax2)
2038 -> (acc, n + 1)
2039 | otherwise
2040 -> (branch : acc, n + 1)
2041 InjectivityAccepted -> (acc, n + 1)
2042
2043 -- Replace n-th element in the list. Assumes 0-based indexing.
2044 replace_br :: [CoAxBranch] -> Int -> CoAxBranch -> [CoAxBranch]
2045 replace_br brs n br = take n brs ++ [br] ++ drop (n+1) brs
2046
2047
2048 -- Check that a "type instance" is well-formed (which includes decidability
2049 -- unless -XUndecidableInstances is given).
2050 --
2051 checkValidCoAxBranch :: TyCon -> CoAxBranch -> TcM ()
2052 checkValidCoAxBranch fam_tc
2053 (CoAxBranch { cab_tvs = tvs, cab_cvs = cvs
2054 , cab_lhs = typats
2055 , cab_rhs = rhs, cab_loc = loc })
2056 = setSrcSpan loc $
2057 checkValidTyFamEqn fam_tc (tvs++cvs) typats rhs
2058
2059 -- | Do validity checks on a type family equation, including consistency
2060 -- with any enclosing class instance head, termination, and lack of
2061 -- polytypes.
2062 checkValidTyFamEqn :: TyCon -- ^ of the type family
2063 -> [Var] -- ^ Bound variables in the equation
2064 -> [Type] -- ^ Type patterns
2065 -> Type -- ^ Rhs
2066 -> TcM ()
2067 checkValidTyFamEqn fam_tc qvs typats rhs
2068 = do { checkValidTypePats fam_tc typats
2069
2070 -- Check for things used on the right but not bound on the left
2071 ; checkFamPatBinders fam_tc qvs typats rhs
2072
2073 -- Check for oversaturated visible kind arguments in a type family
2074 -- equation.
2075 -- See Note [Oversaturated type family equations]
2076 ; when (isTypeFamilyTyCon fam_tc) $
2077 case drop (tyConArity fam_tc) typats of
2078 [] -> pure ()
2079 spec_arg:_ ->
2080 addErr $ text "Illegal oversaturated visible kind argument:"
2081 <+> quotes (char '@' <> pprParendType spec_arg)
2082
2083 -- The argument patterns, and RHS, are all boxed tau types
2084 -- E.g Reject type family F (a :: k1) :: k2
2085 -- type instance F (forall a. a->a) = ...
2086 -- type instance F Int# = ...
2087 -- type instance F Int = forall a. a->a
2088 -- type instance F Int = Int#
2089 -- See #9357
2090 ; checkValidMonoType rhs
2091
2092 -- We have a decidable instance unless otherwise permitted
2093 ; undecidable_ok <- xoptM LangExt.UndecidableInstances
2094 ; traceTc "checkVTFE" (ppr fam_tc $$ ppr rhs $$ ppr (tcTyFamInsts rhs))
2095 ; unless undecidable_ok $
2096 mapM_ addErrTc (checkFamInstRhs fam_tc typats (tcTyFamInsts rhs)) }
2097
2098 -- Make sure that each type family application is
2099 -- (1) strictly smaller than the lhs,
2100 -- (2) mentions no type variable more often than the lhs, and
2101 -- (3) does not contain any further type family instances.
2102 --
2103 checkFamInstRhs :: TyCon -> [Type] -- LHS
2104 -> [(TyCon, [Type])] -- type family calls in RHS
2105 -> [MsgDoc]
2106 checkFamInstRhs lhs_tc lhs_tys famInsts
2107 = mapMaybe check famInsts
2108 where
2109 lhs_size = sizeTyConAppArgs lhs_tc lhs_tys
2110 inst_head = pprType (TyConApp lhs_tc lhs_tys)
2111 lhs_fvs = fvTypes lhs_tys
2112 check (tc, tys)
2113 | not (all isTyFamFree tys) = Just (nestedMsg what)
2114 | not (null bad_tvs) = Just (noMoreMsg bad_tvs what inst_head)
2115 | lhs_size <= fam_app_size = Just (smallerMsg what inst_head)
2116 | otherwise = Nothing
2117 where
2118 what = text "type family application"
2119 <+> quotes (pprType (TyConApp tc tys))
2120 fam_app_size = sizeTyConAppArgs tc tys
2121 bad_tvs = fvTypes tys \\ lhs_fvs
2122 -- The (\\) is list difference; e.g.
2123 -- [a,b,a,a] \\ [a,a] = [b,a]
2124 -- So we are counting repetitions
2125
2126 -----------------
2127 checkFamPatBinders :: TyCon
2128 -> [TcTyVar] -- Bound on LHS of family instance
2129 -> [TcType] -- LHS patterns
2130 -> Type -- RHS
2131 -> TcM ()
2132 -- We do these binder checks now, in tcFamTyPatsAndGen, rather
2133 -- than later, in checkValidFamEqn, for two reasons:
2134 -- - We have the implicitly and explicitly
2135 -- bound type variables conveniently to hand
2136 -- - If implicit variables are out of scope it may
2137 -- cause a crash; notably in tcConDecl in tcDataFamInstDecl
2138 checkFamPatBinders fam_tc qtvs pats rhs
2139 = do { traceTc "checkFamPatBinders" $
2140 vcat [ debugPprType (mkTyConApp fam_tc pats)
2141 , ppr (mkTyConApp fam_tc pats)
2142 , text "qtvs:" <+> ppr qtvs
2143 , text "rhs_tvs:" <+> ppr (fvVarSet rhs_fvs)
2144 , text "pat_tvs:" <+> ppr pat_tvs
2145 , text "inj_pat_tvs:" <+> ppr inj_pat_tvs ]
2146
2147 -- Check for implicitly-bound tyvars, mentioned on the
2148 -- RHS but not bound on the LHS
2149 -- data T = MkT (forall (a::k). blah)
2150 -- data family D Int = MkD (forall (a::k). blah)
2151 -- In both cases, 'k' is not bound on the LHS, but is used on the RHS
2152 -- We catch the former in kcLHsQTyVars, and the latter right here
2153 -- See Note [Check type-family instance binders]
2154 ; check_tvs bad_rhs_tvs (text "mentioned in the RHS")
2155 (text "bound on the LHS of")
2156
2157 -- Check for explicitly forall'd variable that is not bound on LHS
2158 -- data instance forall a. T Int = MkT Int
2159 -- See Note [Unused explicitly bound variables in a family pattern]
2160 -- See Note [Check type-family instance binders]
2161 ; check_tvs bad_qtvs (text "bound by a forall")
2162 (text "used in")
2163 }
2164 where
2165 pat_tvs = tyCoVarsOfTypes pats
2166 inj_pat_tvs = fvVarSet $ injectiveVarsOfTypes pats
2167 -- The type variables that are in injective positions.
2168 -- See Note [Dodgy binding sites in type family instances]
2169 --
2170 -- NB: It's OK to use the nondeterministic `fvVarSet` function here,
2171 -- since the order of `inj_pat_tvs` is never revealed in an error
2172 -- message.
2173 rhs_fvs = tyCoFVsOfType rhs
2174 used_tvs = pat_tvs `unionVarSet` fvVarSet rhs_fvs
2175 bad_qtvs = filterOut (`elemVarSet` used_tvs) qtvs
2176 -- Bound but not used at all
2177 bad_rhs_tvs = filterOut (`elemVarSet` inj_pat_tvs) (fvVarList rhs_fvs)
2178 -- Used on RHS but not bound on LHS
2179 dodgy_tvs = pat_tvs `minusVarSet` inj_pat_tvs
2180
2181 check_tvs tvs what what2
2182 = unless (null tvs) $ addErrAt (getSrcSpan (head tvs)) $
2183 hang (text "Type variable" <> plural tvs <+> pprQuotedList tvs
2184 <+> isOrAre tvs <+> what <> comma)
2185 2 (vcat [ text "but not" <+> what2 <+> text "the family instance"
2186 , mk_extra tvs ])
2187
2188 -- mk_extra: #7536: give a decent error message for
2189 -- type T a = Int
2190 -- type instance F (T a) = a
2191 mk_extra tvs = ppWhen (any (`elemVarSet` dodgy_tvs) tvs) $
2192 hang (text "The real LHS (expanding synonyms) is:")
2193 2 (pprTypeApp fam_tc (map expandTypeSynonyms pats))
2194
2195
2196 -- | Checks that a list of type patterns is valid in a matching (LHS)
2197 -- position of a class instances or type/data family instance.
2198 --
2199 -- Specifically:
2200 -- * All monotypes
2201 -- * No type-family applications
2202 checkValidTypePats :: TyCon -> [Type] -> TcM ()
2203 checkValidTypePats tc pat_ty_args
2204 = do { -- Check that each of pat_ty_args is a monotype.
2205 -- One could imagine generalising to allow
2206 -- instance C (forall a. a->a)
2207 -- but we don't know what all the consequences might be.
2208 traverse_ checkValidMonoType pat_ty_args
2209
2210 -- Ensure that no type family applications occur a type pattern
2211 ; case tcTyConAppTyFamInstsAndVis tc pat_ty_args of
2212 [] -> pure ()
2213 ((tf_is_invis_arg, tf_tc, tf_args):_) -> failWithTc $
2214 ty_fam_inst_illegal_err tf_is_invis_arg
2215 (mkTyConApp tf_tc tf_args) }
2216 where
2217 inst_ty = mkTyConApp tc pat_ty_args
2218
2219 ty_fam_inst_illegal_err :: Bool -> Type -> SDoc
2220 ty_fam_inst_illegal_err invis_arg ty
2221 = pprWithExplicitKindsWhen invis_arg $
2222 hang (text "Illegal type synonym family application"
2223 <+> quotes (ppr ty) <+> text "in instance" <> colon)
2224 2 (ppr inst_ty)
2225
2226 -- Error messages
2227
2228 inaccessibleCoAxBranch :: TyCon -> CoAxBranch -> SDoc
2229 inaccessibleCoAxBranch fam_tc cur_branch
2230 = text "Type family instance equation is overlapped:" $$
2231 nest 2 (pprCoAxBranchUser fam_tc cur_branch)
2232
2233 nestedMsg :: SDoc -> SDoc
2234 nestedMsg what
2235 = sep [ text "Illegal nested" <+> what
2236 , parens undecidableMsg ]
2237
2238 badATErr :: Name -> Name -> SDoc
2239 badATErr clas op
2240 = hsep [text "Class", quotes (ppr clas),
2241 text "does not have an associated type", quotes (ppr op)]
2242
2243
2244 -------------------------
2245 checkConsistentFamInst :: AssocInstInfo
2246 -> TyCon -- ^ Family tycon
2247 -> CoAxBranch
2248 -> TcM ()
2249 -- See Note [Checking consistent instantiation]
2250
2251 checkConsistentFamInst NotAssociated _ _
2252 = return ()
2253
2254 checkConsistentFamInst (InClsInst { ai_class = clas
2255 , ai_tyvars = inst_tvs
2256 , ai_inst_env = mini_env })
2257 fam_tc branch
2258 = do { traceTc "checkConsistentFamInst" (vcat [ ppr inst_tvs
2259 , ppr arg_triples
2260 , ppr mini_env
2261 , ppr ax_tvs
2262 , ppr ax_arg_tys
2263 , ppr arg_triples ])
2264 -- Check that the associated type indeed comes from this class
2265 -- See [Mismatched class methods and associated type families]
2266 -- in TcInstDecls.
2267 ; checkTc (Just (classTyCon clas) == tyConAssoc_maybe fam_tc)
2268 (badATErr (className clas) (tyConName fam_tc))
2269
2270 ; check_match arg_triples
2271 }
2272 where
2273 (ax_tvs, ax_arg_tys, _) = etaExpandCoAxBranch branch
2274
2275 arg_triples :: [(Type,Type, ArgFlag)]
2276 arg_triples = [ (cls_arg_ty, at_arg_ty, vis)
2277 | (fam_tc_tv, vis, at_arg_ty)
2278 <- zip3 (tyConTyVars fam_tc)
2279 (tyConArgFlags fam_tc ax_arg_tys)
2280 ax_arg_tys
2281 , Just cls_arg_ty <- [lookupVarEnv mini_env fam_tc_tv] ]
2282
2283 pp_wrong_at_arg vis
2284 = pprWithExplicitKindsWhen (isInvisibleArgFlag vis) $
2285 vcat [ text "Type indexes must match class instance head"
2286 , text "Expected:" <+> pp_expected_ty
2287 , text " Actual:" <+> pp_actual_ty ]
2288
2289 -- Fiddling around to arrange that wildcards unconditionally print as "_"
2290 -- We only need to print the LHS, not the RHS at all
2291 -- See Note [Printing conflicts with class header]
2292 (tidy_env1, _) = tidyVarBndrs emptyTidyEnv inst_tvs
2293 (tidy_env2, _) = tidyCoAxBndrsForUser tidy_env1 (ax_tvs \\ inst_tvs)
2294
2295 pp_expected_ty = pprIfaceTypeApp topPrec (toIfaceTyCon fam_tc) $
2296 toIfaceTcArgs fam_tc $
2297 [ case lookupVarEnv mini_env at_tv of
2298 Just cls_arg_ty -> tidyType tidy_env2 cls_arg_ty
2299 Nothing -> mk_wildcard at_tv
2300 | at_tv <- tyConTyVars fam_tc ]
2301
2302 pp_actual_ty = pprIfaceTypeApp topPrec (toIfaceTyCon fam_tc) $
2303 toIfaceTcArgs fam_tc $
2304 tidyTypes tidy_env2 ax_arg_tys
2305
2306 mk_wildcard at_tv = mkTyVarTy (mkTyVar tv_name (tyVarKind at_tv))
2307 tv_name = mkInternalName (mkAlphaTyVarUnique 1) (mkTyVarOcc "_") noSrcSpan
2308
2309 -- For check_match, bind_me, see
2310 -- Note [Matching in the consistent-instantation check]
2311 check_match :: [(Type,Type,ArgFlag)] -> TcM ()
2312 check_match triples = go emptyTCvSubst emptyTCvSubst triples
2313
2314 go _ _ [] = return ()
2315 go lr_subst rl_subst ((ty1,ty2,vis):triples)
2316 | Just lr_subst1 <- tcMatchTyX_BM bind_me lr_subst ty1 ty2
2317 , Just rl_subst1 <- tcMatchTyX_BM bind_me rl_subst ty2 ty1
2318 = go lr_subst1 rl_subst1 triples
2319 | otherwise
2320 = addErrTc (pp_wrong_at_arg vis)
2321
2322 -- The /scoped/ type variables from the class-instance header
2323 -- should not be alpha-renamed. Inferred ones can be.
2324 no_bind_set = mkVarSet inst_tvs
2325 bind_me tv | tv `elemVarSet` no_bind_set = Skolem
2326 | otherwise = BindMe
2327
2328
2329 {- Note [Check type-family instance binders]
2330 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2331 In a type family instance, we require (of course), type variables
2332 used on the RHS are matched on the LHS. This is checked by
2333 checkFamPatBinders. Here is an interesting example:
2334
2335 type family T :: k
2336 type instance T = (Nothing :: Maybe a)
2337
2338 Upon a cursory glance, it may appear that the kind variable `a` is unbound
2339 since there are no (visible) LHS patterns in `T`. However, there is an
2340 *invisible* pattern due to the return kind, so inside of GHC, the instance
2341 looks closer to this:
2342
2343 type family T @k :: k
2344 type instance T @(Maybe a) = (Nothing :: Maybe a)
2345
2346 Here, we can see that `a` really is bound by a LHS type pattern, so `a` is in
2347 fact not unbound. Contrast that with this example (#13985)
2348
2349 type instance T = Proxy (Nothing :: Maybe a)
2350
2351 This would looks like this inside of GHC:
2352
2353 type instance T @(*) = Proxy (Nothing :: Maybe a)
2354
2355 So this time, `a` is neither bound by a visible nor invisible type pattern on
2356 the LHS, so `a` would be reported as not in scope.
2357
2358 Finally, here's one more brain-teaser (from #9574). In the example below:
2359
2360 class Funct f where
2361 type Codomain f :: *
2362 instance Funct ('KProxy :: KProxy o) where
2363 type Codomain 'KProxy = NatTr (Proxy :: o -> *)
2364
2365 As it turns out, `o` is in scope in this example. That is because `o` is
2366 bound by the kind signature of the LHS type pattern 'KProxy. To make this more
2367 obvious, one can also write the instance like so:
2368
2369 instance Funct ('KProxy :: KProxy o) where
2370 type Codomain ('KProxy :: KProxy o) = NatTr (Proxy :: o -> *)
2371
2372 Note [Dodgy binding sites in type family instances]
2373 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2374 Consider the following example (from #7536):
2375
2376 type T a = Int
2377 type instance F (T a) = a
2378
2379 This `F` instance is extremely fishy, since the RHS, `a`, purports to be
2380 "bound" by the LHS pattern `T a`. "Bound" has scare quotes around it because
2381 `T a` expands to `Int`, which doesn't mention at all, so it's as if one had
2382 actually written:
2383
2384 type instance F Int = a
2385
2386 That is clearly bogus, so to reject this, we check that every type variable
2387 that is mentioned on the RHS is /actually/ bound on the LHS. In other words,
2388 we need to do something slightly more sophisticated that just compute the free
2389 variables of the LHS patterns.
2390
2391 It's tempting to just expand all type synonyms on the LHS and then compute
2392 their free variables, but even that isn't sophisticated enough. After all,
2393 an impish user could write the following (#17008):
2394
2395 type family ConstType (a :: Type) :: Type where
2396 ConstType _ = Type
2397
2398 type family F (x :: ConstType a) :: Type where
2399 F (x :: ConstType a) = a
2400
2401 Just like in the previous example, the `a` on the RHS isn't actually bound
2402 on the LHS, but this time a type family is responsible for the deception, not
2403 a type synonym.
2404
2405 We avoid both issues by requiring that all RHS type variables are mentioned
2406 in injective positions on the left-hand side (by way of
2407 `injectiveVarsOfTypes`). For instance, the `a` in `T a` is not in an injective
2408 position, as `T` is not an injective type constructor, so we do not count that.
2409 Similarly for the `a` in `ConstType a`.
2410
2411 Note [Matching in the consistent-instantation check]
2412 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2413 Matching the class-instance header to family-instance tyvars is
2414 tricker than it sounds. Consider (#13972)
2415 class C (a :: k) where
2416 type T k :: Type
2417 instance C Left where
2418 type T (a -> Either a b) = Int
2419
2420 Here there are no lexically-scoped variables from (C Left).
2421 Yet the real class-instance header is C @(p -> Either @p @q)) (Left @p @q)
2422 while the type-family instance is T (a -> Either @a @b)
2423 So we allow alpha-renaming of variables that don't come
2424 from the class-instance header.
2425
2426 We track the lexically-scoped type variables from the
2427 class-instance header in ai_tyvars.
2428
2429 Here's another example (#14045a)
2430 class C (a :: k) where
2431 data S (a :: k)
2432 instance C (z :: Bool) where
2433 data S :: Bool -> Type where
2434
2435 Again, there is no lexical connection, but we will get
2436 class-instance header: C @Bool (z::Bool)
2437 family instance S @Bool (a::Bool)
2438
2439 When looking for mis-matches, we check left-to-right,
2440 kinds first. If we look at types first, we'll fail to
2441 suggest -fprint-explicit-kinds for a mis-match with
2442 T @k vs T @Type
2443 somewhere deep inside the type
2444
2445 Note [Checking consistent instantiation]
2446 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2447 See #11450 for background discussion on this check.
2448
2449 class C a b where
2450 type T a x b
2451
2452 With this class decl, if we have an instance decl
2453 instance C ty1 ty2 where ...
2454 then the type instance must look like
2455 type T ty1 v ty2 = ...
2456 with exactly 'ty1' for 'a', 'ty2' for 'b', and some type 'v' for 'x'.
2457 For example:
2458
2459 instance C [p] Int
2460 type T [p] y Int = (p,y,y)
2461
2462 Note that
2463
2464 * We used to allow completely different bound variables in the
2465 associated type instance; e.g.
2466 instance C [p] Int
2467 type T [q] y Int = ...
2468 But from GHC 8.2 onwards, we don't. It's much simpler this way.
2469 See #11450.
2470
2471 * When the class variable isn't used on the RHS of the type instance,
2472 it's tempting to allow wildcards, thus
2473 instance C [p] Int
2474 type T [_] y Int = (y,y)
2475 But it's awkward to do the test, and it doesn't work if the
2476 variable is repeated:
2477 instance C (p,p) Int
2478 type T (_,_) y Int = (y,y)
2479 Even though 'p' is not used on the RHS, we still need to use 'p'
2480 on the LHS to establish the repeated pattern. So to keep it simple
2481 we just require equality.
2482
2483 * For variables in associated type families that are not bound by the class
2484 itself, we do _not_ check if they are over-specific. In other words,
2485 it's perfectly acceptable to have an instance like this:
2486
2487 instance C [p] Int where
2488 type T [p] (Maybe x) Int = x
2489
2490 While the first and third arguments to T are required to be exactly [p] and
2491 Int, respectively, since they are bound by C, the second argument is allowed
2492 to be more specific than just a type variable. Furthermore, it is permissible
2493 to define multiple equations for T that differ only in the non-class-bound
2494 argument:
2495
2496 instance C [p] Int where
2497 type T [p] (Maybe x) Int = x
2498 type T [p] (Either x y) Int = x -> y
2499
2500 We once considered requiring that non-class-bound variables in associated
2501 type family instances be instantiated with distinct type variables. However,
2502 that requirement proved too restrictive in practice, as there were examples
2503 of extremely simple associated type family instances that this check would
2504 reject, and fixing them required tiresome boilerplate in the form of
2505 auxiliary type families. For instance, you would have to define the above
2506 example as:
2507
2508 instance C [p] Int where
2509 type T [p] x Int = CAux x
2510
2511 type family CAux x where
2512 CAux (Maybe x) = x
2513 CAux (Either x y) = x -> y
2514
2515 We decided that this restriction wasn't buying us much, so we opted not
2516 to pursue that design (see also GHC #13398).
2517
2518 Implementation
2519 * Form the mini-envt from the class type variables a,b
2520 to the instance decl types [p],Int: [a->[p], b->Int]
2521
2522 * Look at the tyvars a,x,b of the type family constructor T
2523 (it shares tyvars with the class C)
2524
2525 * Apply the mini-evnt to them, and check that the result is
2526 consistent with the instance types [p] y Int. (where y can be any type, as
2527 it is not scoped over the class type variables.
2528
2529 We make all the instance type variables scope over the
2530 type instances, of course, which picks up non-obvious kinds. Eg
2531 class Foo (a :: k) where
2532 type F a
2533 instance Foo (b :: k -> k) where
2534 type F b = Int
2535 Here the instance is kind-indexed and really looks like
2536 type F (k->k) (b::k->k) = Int
2537 But if the 'b' didn't scope, we would make F's instance too
2538 poly-kinded.
2539
2540 Note [Printing conflicts with class header]
2541 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2542 It's remarkably painful to give a decent error message for conflicts
2543 with the class header. Consider
2544 clase C b where
2545 type F a b c
2546 instance C [b] where
2547 type F x Int _ _ = ...
2548
2549 Here we want to report a conflict between
2550 Expected: F _ [b] _
2551 Actual: F x Int _ _
2552
2553 But if the type instance shadows the class variable like this
2554 (rename/should_fail/T15828):
2555 instance C [b] where
2556 type forall b. F x (Tree b) _ _ = ...
2557
2558 then we must use a fresh variable name
2559 Expected: F _ [b] _
2560 Actual: F x [b1] _ _
2561
2562 Notice that:
2563 - We want to print an underscore in the "Expected" type in
2564 positions where the class header has no influence over the
2565 parameter. Hence the fancy footwork in pp_expected_ty
2566
2567 - Although the binders in the axiom are aready tidy, we must
2568 re-tidy them to get a fresh variable name when we shadow
2569
2570 - The (ax_tvs \\ inst_tvs) is to avoid tidying one of the
2571 class-instance variables a second time, from 'a' to 'a1' say.
2572 Remember, the ax_tvs of the axiom share identity with the
2573 class-instance variables, inst_tvs..
2574
2575 - We use tidyCoAxBndrsForUser to get underscores rather than
2576 _1, _2, etc in the axiom tyvars; see the definition of
2577 tidyCoAxBndrsForUser
2578
2579 This all seems absurdly complicated.
2580
2581 Note [Unused explicitly bound variables in a family pattern]
2582 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2583
2584 Why is 'unusedExplicitForAllErr' not just a warning?
2585
2586 Consider the following examples:
2587
2588 type instance F a = Maybe b
2589 type instance forall b. F a = Bool
2590 type instance forall b. F a = Maybe b
2591
2592 In every case, b is a type variable not determined by the LHS pattern. The
2593 first is caught by the renamer, but we catch the last two here. Perhaps one
2594 could argue that the second should be accepted, albeit with a warning, but
2595 consider the fact that in a type family instance, there is no way to interact
2596 with such a varable. At least with @x :: forall a. Int@ we can use visibile
2597 type application, like @x \@Bool 1@. (Of course it does nothing, but it is
2598 permissible.) In the type family case, the only sensible explanation is that
2599 the user has made a mistake -- thus we throw an error.
2600
2601 Note [Oversaturated type family equations]
2602 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2603 Type family tycons have very rigid arities. We want to reject something like
2604 this:
2605
2606 type family Foo :: Type -> Type where
2607 Foo x = ...
2608
2609 Because Foo has arity zero (i.e., it doesn't bind anything to the left of the
2610 double colon), we want to disallow any equation for Foo that has more than zero
2611 arguments, such as `Foo x = ...`. The algorithm here is pretty simple: if an
2612 equation has more arguments than the arity of the type family, reject.
2613
2614 Things get trickier when visible kind application enters the picture. Consider
2615 the following example:
2616
2617 type family Bar (x :: j) :: forall k. Either j k where
2618 Bar 5 @Symbol = ...
2619
2620 The arity of Bar is two, since it binds two variables, `j` and `x`. But even
2621 though Bar's equation has two arguments, it's still invalid. Imagine the same
2622 equation in Core:
2623
2624 Bar Nat 5 Symbol = ...
2625
2626 Here, it becomes apparent that Bar is actually taking /three/ arguments! So
2627 we can't just rely on a simple counting argument to reject
2628 `Bar 5 @Symbol = ...`, since it only has two user-written arguments.
2629 Moreover, there's one explicit argument (5) and one visible kind argument
2630 (@Symbol), which matches up perfectly with the fact that Bar has one required
2631 binder (x) and one specified binder (j), so that's not a valid way to detect
2632 oversaturation either.
2633
2634 To solve this problem in a robust way, we do the following:
2635
2636 1. When kind-checking, we count the number of user-written *required*
2637 arguments and check if there is an equal number of required tycon binders.
2638 If not, reject. (See `wrongNumberOfParmsErr` in TcTyClsDecls.)
2639
2640 We perform this step during kind-checking, not during validity checking,
2641 since we can give better error messages if we catch it early.
2642 2. When validity checking, take all of the (Core) type patterns from on
2643 equation, drop the first n of them (where n is the arity of the type family
2644 tycon), and check if there are any types leftover. If so, reject.
2645
2646 Why does this work? We know that after dropping the first n type patterns,
2647 none of the leftover types can be required arguments, since step (1) would
2648 have already caught that. Moreover, the only places where visible kind
2649 applications should be allowed are in the first n types, since those are the
2650 only arguments that can correspond to binding forms. Therefore, the
2651 remaining arguments must correspond to oversaturated uses of visible kind
2652 applications, which are precisely what we want to reject.
2653
2654 Note that we only perform this check for type families, and not for data
2655 families. This is because it is perfectly acceptable to oversaturate data
2656 family instance equations: see Note [Arity of data families] in FamInstEnv.
2657
2658 ************************************************************************
2659 * *
2660 Telescope checking
2661 * *
2662 ************************************************************************
2663
2664 Note [Bad TyCon telescopes]
2665 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
2666 Now that we can mix type and kind variables, there are an awful lot of
2667 ways to shoot yourself in the foot. Here are some.
2668
2669 data SameKind :: k -> k -> * -- just to force unification
2670
2671 1. data T1 a k (b :: k) (x :: SameKind a b)
2672
2673 The problem here is that we discover that a and b should have the same
2674 kind. But this kind mentions k, which is bound *after* a.
2675 (Testcase: dependent/should_fail/BadTelescope)
2676
2677 2. data T2 a (c :: Proxy b) (d :: Proxy a) (x :: SameKind b d)
2678
2679 Note that b is not bound. Yet its kind mentions a. Because we have
2680 a nice rule that all implicitly bound variables come before others,
2681 this is bogus.
2682
2683 To catch these errors, we call checkTyConTelescope during kind-checking
2684 datatype declarations. This checks for
2685
2686 * Ill-scoped binders. From (1) and (2) above we can get putative
2687 kinds like
2688 T1 :: forall (a:k) (k:*) (b:k). SameKind a b -> *
2689 where 'k' is mentioned a's kind before k is bound
2690
2691 This is easy to check for: just look for
2692 out-of-scope variables in the kind
2693
2694 * We should arguably also check for ambiguous binders
2695 but we don't. See Note [Ambiguous kind vars].
2696
2697 See also
2698 * Note [Required, Specified, and Inferred for types] in TcTyClsDecls.
2699 * Note [Keeping scoped variables in order: Explicit] discusses how
2700 this check works for `forall x y z.` written in a type.
2701
2702 Note [Ambiguous kind vars]
2703 ~~~~~~~~~~~~~~~~~~~~~~~~~~
2704 We used to be concerned about ambiguous binders. Suppose we have the kind
2705 S1 :: forall k -> * -> *
2706 S2 :: forall k. * -> *
2707 Here S1 is OK, because k is Required, and at a use of S1 we will
2708 see (S1 *) or (S1 (*->*)) or whatever.
2709
2710 But S2 is /not/ OK because 'k' is Specfied (and hence invisible) and
2711 we have no way (ever) to figure out how 'k' should be instantiated.
2712 For example if we see (S2 Int), that tells us nothing about k's
2713 instantiation. (In this case we'll instantiate it to Any, but that
2714 seems wrong.) This is really the same test as we make for ambiguous
2715 type in term type signatures.
2716
2717 Now, it's impossible for a Specified variable not to occur
2718 at all in the kind -- after all, it is Specified so it must have
2719 occurred. (It /used/ to be possible; see tests T13983 and T7873. But
2720 with the advent of the forall-or-nothing rule for kind variables,
2721 those strange cases went away.)
2722
2723 But one might worry about
2724 type v k = *
2725 S3 :: forall k. V k -> *
2726 which appears to mention 'k' but doesn't really. Or
2727 S4 :: forall k. F k -> *
2728 where F is a type function. But we simply don't check for
2729 those cases of ambiguity, yet anyway. The worst that can happen
2730 is ambiguity at the call sites.
2731
2732 Historical note: this test used to be called reportFloatingKvs.
2733 -}
2734
2735 -- | Check a list of binders to see if they make a valid telescope.
2736 -- See Note [Bad TyCon telescopes]
2737 type TelescopeAcc
2738 = ( TyVarSet -- Bound earlier in the telescope
2739 , Bool -- At least one binder occurred (in a kind) before
2740 -- it was bound in the telescope. E.g.
2741 ) -- T :: forall (a::k) k. blah
2742
2743 checkTyConTelescope :: TyCon -> TcM ()
2744 checkTyConTelescope tc
2745 | bad_scope
2746 = -- See "Ill-scoped binders" in Note [Bad TyCon telescopes]
2747 addErr $
2748 vcat [ hang (text "The kind of" <+> quotes (ppr tc) <+> text "is ill-scoped")
2749 2 pp_tc_kind
2750 , extra
2751 , hang (text "Perhaps try this order instead:")
2752 2 (pprTyVars sorted_tvs) ]
2753
2754 | otherwise
2755 = return ()
2756 where
2757 tcbs = tyConBinders tc
2758 tvs = binderVars tcbs
2759 sorted_tvs = scopedSort tvs
2760
2761 (_, bad_scope) = foldl add_one (emptyVarSet, False) tcbs
2762
2763 add_one :: TelescopeAcc -> TyConBinder -> TelescopeAcc
2764 add_one (bound, bad_scope) tcb
2765 = ( bound `extendVarSet` tv
2766 , bad_scope || not (isEmptyVarSet (fkvs `minusVarSet` bound)) )
2767 where
2768 tv = binderVar tcb
2769 fkvs = tyCoVarsOfType (tyVarKind tv)
2770
2771 inferred_tvs = [ binderVar tcb
2772 | tcb <- tcbs, Inferred == tyConBinderArgFlag tcb ]
2773 specified_tvs = [ binderVar tcb
2774 | tcb <- tcbs, Specified == tyConBinderArgFlag tcb ]
2775
2776 pp_inf = parens (text "namely:" <+> pprTyVars inferred_tvs)
2777 pp_spec = parens (text "namely:" <+> pprTyVars specified_tvs)
2778
2779 pp_tc_kind = text "Inferred kind:" <+> ppr tc <+> dcolon <+> ppr_untidy (tyConKind tc)
2780 ppr_untidy ty = pprIfaceType (toIfaceType ty)
2781 -- We need ppr_untidy here because pprType will tidy the type, which
2782 -- will turn the bogus kind we are trying to report
2783 -- T :: forall (a::k) k (b::k) -> blah
2784 -- into a misleadingly sanitised version
2785 -- T :: forall (a::k) k1 (b::k1) -> blah
2786
2787 extra
2788 | null inferred_tvs && null specified_tvs
2789 = empty
2790 | null inferred_tvs
2791 = hang (text "NB: Specified variables")
2792 2 (sep [pp_spec, text "always come first"])
2793 | null specified_tvs
2794 = hang (text "NB: Inferred variables")
2795 2 (sep [pp_inf, text "always come first"])
2796 | otherwise
2797 = hang (text "NB: Inferred variables")
2798 2 (vcat [ sep [ pp_inf, text "always come first"]
2799 , sep [text "then Specified variables", pp_spec]])
2800
2801 {-
2802 ************************************************************************
2803 * *
2804 \subsection{Auxiliary functions}
2805 * *
2806 ************************************************************************
2807 -}
2808
2809 -- Free variables of a type, retaining repetitions, and expanding synonyms
2810 -- This ignores coercions, as coercions aren't user-written
2811 fvType :: Type -> [TyCoVar]
2812 fvType ty | Just exp_ty <- tcView ty = fvType exp_ty
2813 fvType (TyVarTy tv) = [tv]
2814 fvType (TyConApp _ tys) = fvTypes tys
2815 fvType (LitTy {}) = []
2816 fvType (AppTy fun arg) = fvType fun ++ fvType arg
2817 fvType (FunTy _ arg res) = fvType arg ++ fvType res
2818 fvType (ForAllTy (Bndr tv _) ty)
2819 = fvType (tyVarKind tv) ++
2820 filter (/= tv) (fvType ty)
2821 fvType (CastTy ty _) = fvType ty
2822 fvType (CoercionTy {}) = []
2823
2824 fvTypes :: [Type] -> [TyVar]
2825 fvTypes tys = concat (map fvType tys)
2826
2827 sizeType :: Type -> Int
2828 -- Size of a type: the number of variables and constructors
2829 sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty
2830 sizeType (TyVarTy {}) = 1
2831 sizeType (TyConApp tc tys) = 1 + sizeTyConAppArgs tc tys
2832 sizeType (LitTy {}) = 1
2833 sizeType (AppTy fun arg) = sizeType fun + sizeType arg
2834 sizeType (FunTy _ arg res) = sizeType arg + sizeType res + 1
2835 sizeType (ForAllTy _ ty) = sizeType ty
2836 sizeType (CastTy ty _) = sizeType ty
2837 sizeType (CoercionTy _) = 0
2838
2839 sizeTypes :: [Type] -> Int
2840 sizeTypes = foldr ((+) . sizeType) 0
2841
2842 sizeTyConAppArgs :: TyCon -> [Type] -> Int
2843 sizeTyConAppArgs _tc tys = sizeTypes tys -- (filterOutInvisibleTypes tc tys)
2844 -- See Note [Invisible arguments and termination]
2845
2846 -- Size of a predicate
2847 --
2848 -- We are considering whether class constraints terminate.
2849 -- Equality constraints and constraints for the implicit
2850 -- parameter class always terminate so it is safe to say "size 0".
2851 -- See #4200.
2852 sizePred :: PredType -> Int
2853 sizePred ty = goClass ty
2854 where
2855 goClass p = go (classifyPredType p)
2856
2857 go (ClassPred cls tys')
2858 | isTerminatingClass cls = 0
2859 | otherwise = sizeTypes (filterOutInvisibleTypes (classTyCon cls) tys')
2860 -- The filtering looks bogus
2861 -- See Note [Invisible arguments and termination]
2862 go (EqPred {}) = 0
2863 go (IrredPred ty) = sizeType ty
2864 go (ForAllPred _ _ pred) = goClass pred
2865
2866 -- | When this says "True", ignore this class constraint during
2867 -- a termination check
2868 isTerminatingClass :: Class -> Bool
2869 isTerminatingClass cls
2870 = isIPClass cls -- Implicit parameter constraints always terminate because
2871 -- there are no instances for them --- they are only solved
2872 -- by "local instances" in expressions
2873 || isEqPredClass cls
2874 || cls `hasKey` typeableClassKey
2875 || cls `hasKey` coercibleTyConKey
2876
2877 -- | Tidy before printing a type
2878 ppr_tidy :: TidyEnv -> Type -> SDoc
2879 ppr_tidy env ty = pprType (tidyType env ty)
2880
2881 allDistinctTyVars :: TyVarSet -> [KindOrType] -> Bool
2882 -- (allDistinctTyVars tvs tys) returns True if tys are
2883 -- a) all tyvars
2884 -- b) all distinct
2885 -- c) disjoint from tvs
2886 allDistinctTyVars _ [] = True
2887 allDistinctTyVars tkvs (ty : tys)
2888 = case getTyVar_maybe ty of
2889 Nothing -> False
2890 Just tv | tv `elemVarSet` tkvs -> False
2891 | otherwise -> allDistinctTyVars (tkvs `extendVarSet` tv) tys