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