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