Fix #11723 and #11724.
[ghc.git] / compiler / typecheck / TcValidity.hs
1 {-
2 (c) The University of Glasgow 2006
3 (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 -}
5
6 {-# LANGUAGE CPP, TupleSections, ViewPatterns #-}
7
8 module TcValidity (
9 Rank, UserTypeCtxt(..), checkValidType, checkValidMonoType,
10 ContextKind(..), expectedKindInCtxt,
11 checkValidTheta, checkValidFamPats,
12 checkValidInstance, validDerivPred,
13 checkInstTermination,
14 ClsInfo, checkValidCoAxiom, checkValidCoAxBranch,
15 checkValidTyFamEqn,
16 arityErr, badATErr,
17 checkValidTelescope, checkZonkValidTelescope, checkValidInferredKinds
18 ) where
19
20 #include "HsVersions.h"
21
22 -- friends:
23 import TcUnify ( tcSubType_NC )
24 import TcSimplify ( simplifyAmbiguityCheck )
25 import TyCoRep
26 import TcType hiding ( sizeType, sizeTypes )
27 import TcMType
28 import PrelNames
29 import Type
30 import Coercion
31 import Unify( tcMatchTyX )
32 import Kind
33 import CoAxiom
34 import Class
35 import TyCon
36
37 -- others:
38 import HsSyn -- HsType
39 import TcRnMonad -- TcType, amongst others
40 import TcHsSyn ( checkForRepresentationPolymorphism )
41 import FunDeps
42 import FamInstEnv ( isDominatedBy, injectiveBranches,
43 InjectivityCheckResult(..) )
44 import FamInst ( makeInjectivityErrors )
45 import Name
46 import VarEnv
47 import VarSet
48 import ErrUtils
49 import DynFlags
50 import Util
51 import ListSetOps
52 import SrcLoc
53 import Outputable
54 import BasicTypes
55 import Module
56 import qualified GHC.LanguageExtensions as LangExt
57
58 import Control.Monad
59 import Data.Maybe
60 import Data.List ( (\\) )
61
62 {-
63 ************************************************************************
64 * *
65 Checking for ambiguity
66 * *
67 ************************************************************************
68
69 Note [The ambiguity check for type signatures]
70 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
71 checkAmbiguity is a check on *user-supplied type signatures*. It is
72 *purely* there to report functions that cannot possibly be called. So for
73 example we want to reject:
74 f :: C a => Int
75 The idea is there can be no legal calls to 'f' because every call will
76 give rise to an ambiguous constraint. We could soundly omit the
77 ambiguity check on type signatures entirely, at the expense of
78 delaying ambiguity errors to call sites. Indeed, the flag
79 -XAllowAmbiguousTypes switches off the ambiguity check.
80
81 What about things like this:
82 class D a b | a -> b where ..
83 h :: D Int b => Int
84 The Int may well fix 'b' at the call site, so that signature should
85 not be rejected. Moreover, using *visible* fundeps is too
86 conservative. Consider
87 class X a b where ...
88 class D a b | a -> b where ...
89 instance D a b => X [a] b where...
90 h :: X a b => a -> a
91 Here h's type looks ambiguous in 'b', but here's a legal call:
92 ...(h [True])...
93 That gives rise to a (X [Bool] beta) constraint, and using the
94 instance means we need (D Bool beta) and that fixes 'beta' via D's
95 fundep!
96
97 Behind all these special cases there is a simple guiding principle.
98 Consider
99
100 f :: <type>
101 f = ...blah...
102
103 g :: <type>
104 g = f
105
106 You would think that the definition of g would surely typecheck!
107 After all f has exactly the same type, and g=f. But in fact f's type
108 is instantiated and the instantiated constraints are solved against
109 the originals, so in the case an ambiguous type it won't work.
110 Consider our earlier example f :: C a => Int. Then in g's definition,
111 we'll instantiate to (C alpha) and try to deduce (C alpha) from (C a),
112 and fail.
113
114 So in fact we use this as our *definition* of ambiguity. We use a
115 very similar test for *inferred* types, to ensure that they are
116 unambiguous. See Note [Impedence matching] in TcBinds.
117
118 This test is very conveniently implemented by calling
119 tcSubType <type> <type>
120 This neatly takes account of the functional dependecy stuff above,
121 and implicit parameter (see Note [Implicit parameters and ambiguity]).
122 And this is what checkAmbiguity does.
123
124 What about this, though?
125 g :: C [a] => Int
126 Is every call to 'g' ambiguous? After all, we might have
127 intance C [a] where ...
128 at the call site. So maybe that type is ok! Indeed even f's
129 quintessentially ambiguous type might, just possibly be callable:
130 with -XFlexibleInstances we could have
131 instance C a where ...
132 and now a call could be legal after all! Well, we'll reject this
133 unless the instance is available *here*.
134
135 Note [When to call checkAmbiguity]
136 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
137 We call checkAmbiguity
138 (a) on user-specified type signatures
139 (b) in checkValidType
140
141 Conncerning (b), you might wonder about nested foralls. What about
142 f :: forall b. (forall a. Eq a => b) -> b
143 The nested forall is ambiguous. Originally we called checkAmbiguity
144 in the forall case of check_type, but that had two bad consequences:
145 * We got two error messages about (Eq b) in a nested forall like this:
146 g :: forall a. Eq a => forall b. Eq b => a -> a
147 * If we try to check for ambiguity of an nested forall like
148 (forall a. Eq a => b), the implication constraint doesn't bind
149 all the skolems, which results in "No skolem info" in error
150 messages (see Trac #10432).
151
152 To avoid this, we call checkAmbiguity once, at the top, in checkValidType.
153 (I'm still a bit worried about unbound skolems when the type mentions
154 in-scope type variables.)
155
156 In fact, because of the co/contra-variance implemented in tcSubType,
157 this *does* catch function f above. too.
158
159 Concerning (a) the ambiguity check is only used for *user* types, not
160 for types coming from inteface files. The latter can legitimately
161 have ambiguous types. Example
162
163 class S a where s :: a -> (Int,Int)
164 instance S Char where s _ = (1,1)
165 f:: S a => [a] -> Int -> (Int,Int)
166 f (_::[a]) x = (a*x,b)
167 where (a,b) = s (undefined::a)
168
169 Here the worker for f gets the type
170 fw :: forall a. S a => Int -> (# Int, Int #)
171
172
173 Note [Implicit parameters and ambiguity]
174 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
175 Only a *class* predicate can give rise to ambiguity
176 An *implicit parameter* cannot. For example:
177 foo :: (?x :: [a]) => Int
178 foo = length ?x
179 is fine. The call site will supply a particular 'x'
180
181 Furthermore, the type variables fixed by an implicit parameter
182 propagate to the others. E.g.
183 foo :: (Show a, ?x::[a]) => Int
184 foo = show (?x++?x)
185 The type of foo looks ambiguous. But it isn't, because at a call site
186 we might have
187 let ?x = 5::Int in foo
188 and all is well. In effect, implicit parameters are, well, parameters,
189 so we can take their type variables into account as part of the
190 "tau-tvs" stuff. This is done in the function 'FunDeps.grow'.
191 -}
192
193 checkAmbiguity :: UserTypeCtxt -> Type -> TcM ()
194 checkAmbiguity ctxt ty
195 | wantAmbiguityCheck ctxt
196 = do { traceTc "Ambiguity check for" (ppr ty)
197 -- Solve the constraints eagerly because an ambiguous type
198 -- can cause a cascade of further errors. Since the free
199 -- tyvars are skolemised, we can safely use tcSimplifyTop
200 ; allow_ambiguous <- xoptM LangExt.AllowAmbiguousTypes
201 ; (_wrap, wanted) <- addErrCtxt (mk_msg allow_ambiguous) $
202 captureConstraints $
203 tcSubType_NC ctxt ty (mkCheckExpType ty)
204 ; simplifyAmbiguityCheck ty wanted
205
206 ; traceTc "Done ambiguity check for" (ppr ty) }
207
208 | otherwise
209 = return ()
210 where
211 mk_msg allow_ambiguous
212 = vcat [ text "In the ambiguity check for" <+> what
213 , ppUnless allow_ambiguous ambig_msg ]
214 ambig_msg = text "To defer the ambiguity check to use sites, enable AllowAmbiguousTypes"
215 what | Just n <- isSigMaybe ctxt = quotes (ppr n)
216 | otherwise = pprUserTypeCtxt ctxt
217
218 wantAmbiguityCheck :: UserTypeCtxt -> Bool
219 wantAmbiguityCheck ctxt
220 = case ctxt of -- See Note [When we don't check for ambiguity]
221 GhciCtxt -> False
222 TySynCtxt {} -> False
223 _ -> True
224
225 checkUserTypeError :: Type -> TcM ()
226 -- Check to see if the type signature mentions "TypeError blah"
227 -- anywhere in it, and fail if so.
228 --
229 -- Very unsatisfactorily (Trac #11144) we need to tidy the type
230 -- because it may have come from an /inferred/ signature, not a
231 -- user-supplied one. This is really only a half-baked fix;
232 -- the other errors in checkValidType don't do tidying, and so
233 -- may give bad error messages when given an inferred type.
234 checkUserTypeError = check
235 where
236 check ty
237 | Just msg <- userTypeError_maybe ty = fail_with msg
238 | Just (_,ts) <- splitTyConApp_maybe ty = mapM_ check ts
239 | Just (t1,t2) <- splitAppTy_maybe ty = check t1 >> check t2
240 | Just (_,t1) <- splitForAllTy_maybe ty = check t1
241 | otherwise = return ()
242
243 fail_with msg = do { env0 <- tcInitTidyEnv
244 ; let (env1, tidy_msg) = tidyOpenType env0 msg
245 ; failWithTcM (env1, pprUserTypeErrorTy tidy_msg) }
246
247
248 {- Note [When we don't check for ambiguity]
249 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
250 In a few places we do not want to check a user-specified type for ambiguity
251
252 * GhciCtxt: Allow ambiguous types in GHCi's :kind command
253 E.g. type family T a :: * -- T :: forall k. k -> *
254 Then :k T should work in GHCi, not complain that
255 (T k) is ambiguous!
256
257 * TySynCtxt: type T a b = C a b => blah
258 It may be that when we /use/ T, we'll give an 'a' or 'b' that somehow
259 cure the ambiguity. So we defer the ambiguity check to the use site.
260
261 There is also an implementation reason (Trac #11608). In the RHS of
262 a type synonym we don't (currently) instantiate 'a' and 'b' with
263 TcTyVars before calling checkValidType, so we get asertion failures
264 from doing an ambiguity check on a type with TyVars in it. Fixing this
265 would not be hard, but let's wait till there's a reason.
266
267
268 ************************************************************************
269 * *
270 Checking validity of a user-defined type
271 * *
272 ************************************************************************
273
274 When dealing with a user-written type, we first translate it from an HsType
275 to a Type, performing kind checking, and then check various things that should
276 be true about it. We don't want to perform these checks at the same time
277 as the initial translation because (a) they are unnecessary for interface-file
278 types and (b) when checking a mutually recursive group of type and class decls,
279 we can't "look" at the tycons/classes yet. Also, the checks are rather
280 diverse, and used to really mess up the other code.
281
282 One thing we check for is 'rank'.
283
284 Rank 0: monotypes (no foralls)
285 Rank 1: foralls at the front only, Rank 0 inside
286 Rank 2: foralls at the front, Rank 1 on left of fn arrow,
287
288 basic ::= tyvar | T basic ... basic
289
290 r2 ::= forall tvs. cxt => r2a
291 r2a ::= r1 -> r2a | basic
292 r1 ::= forall tvs. cxt => r0
293 r0 ::= r0 -> r0 | basic
294
295 Another thing is to check that type synonyms are saturated.
296 This might not necessarily show up in kind checking.
297 type A i = i
298 data T k = MkT (k Int)
299 f :: T A -- BAD!
300 -}
301
302 checkValidType :: UserTypeCtxt -> Type -> TcM ()
303 -- Checks that a user-written type is valid for the given context
304 -- Assumes arguemt is fully zonked
305 -- Not used for instance decls; checkValidInstance instead
306 checkValidType ctxt ty
307 = do { traceTc "checkValidType" (ppr ty <+> text "::" <+> ppr (typeKind ty))
308 ; rankn_flag <- xoptM LangExt.RankNTypes
309 ; impred_flag <- xoptM LangExt.ImpredicativeTypes
310 ; let gen_rank :: Rank -> Rank
311 gen_rank r | rankn_flag = ArbitraryRank
312 | otherwise = r
313
314 rank1 = gen_rank r1
315 rank0 = gen_rank r0
316
317 r0 = rankZeroMonoType
318 r1 = LimitedRank True r0
319
320 rank
321 = case ctxt of
322 DefaultDeclCtxt-> MustBeMonoType
323 ResSigCtxt -> MustBeMonoType
324 PatSigCtxt -> rank0
325 RuleSigCtxt _ -> rank1
326 TySynCtxt _ -> rank0
327
328 ExprSigCtxt -> rank1
329 TypeAppCtxt | impred_flag -> ArbitraryRank
330 | otherwise -> tyConArgMonoType
331 -- Normally, ImpredicativeTypes is handled in check_arg_type,
332 -- but visible type applications don't go through there.
333 -- So we do this check here.
334
335 FunSigCtxt {} -> rank1
336 InfSigCtxt _ -> ArbitraryRank -- Inferred type
337 ConArgCtxt _ -> rank1 -- We are given the type of the entire
338 -- constructor, hence rank 1
339
340 ForSigCtxt _ -> rank1
341 SpecInstCtxt -> rank1
342 ThBrackCtxt -> rank1
343 GhciCtxt -> ArbitraryRank
344 _ -> panic "checkValidType"
345 -- Can't happen; not used for *user* sigs
346
347 ; env <- tcInitOpenTidyEnv (tyCoVarsOfType ty)
348
349 -- Check the internal validity of the type itself
350 ; check_type env ctxt rank ty
351
352 -- Check that the thing has kind Type, and is lifted if necessary.
353 -- Do this *after* check_type, because we can't usefully take
354 -- the kind of an ill-formed type such as (a~Int)
355 ; check_kind env ctxt ty
356
357 ; checkUserTypeError ty
358
359 -- Check for ambiguous types. See Note [When to call checkAmbiguity]
360 -- NB: this will happen even for monotypes, but that should be cheap;
361 -- and there may be nested foralls for the subtype test to examine
362 ; checkAmbiguity ctxt ty
363
364 ; traceTc "checkValidType done" (ppr ty <+> text "::" <+> ppr (typeKind ty)) }
365
366 checkValidMonoType :: Type -> TcM ()
367 -- Assumes arguemt is fully zonked
368 checkValidMonoType ty
369 = do { env <- tcInitOpenTidyEnv (tyCoVarsOfType ty)
370 ; check_type env SigmaCtxt MustBeMonoType ty }
371
372 check_kind :: TidyEnv -> UserTypeCtxt -> TcType -> TcM ()
373 -- Check that the type's kind is acceptable for the context
374 check_kind env ctxt ty
375 | TySynCtxt {} <- ctxt
376 , returnsConstraintKind actual_kind
377 = do { ck <- xoptM LangExt.ConstraintKinds
378 ; if ck
379 then when (isConstraintKind actual_kind)
380 (do { dflags <- getDynFlags
381 ; check_pred_ty env dflags ctxt ty })
382 else addErrTcM (constraintSynErr env actual_kind) }
383
384 | otherwise
385 = case expectedKindInCtxt ctxt of
386 TheKind k -> checkTcM (tcEqType actual_kind k) (kindErr env actual_kind)
387 OpenKind -> checkTcM (classifiesTypeWithValues actual_kind) (kindErr env actual_kind)
388 AnythingKind -> return ()
389 where
390 actual_kind = typeKind ty
391
392 -- | The kind expected in a certain context.
393 data ContextKind = TheKind Kind -- ^ a specific kind
394 | AnythingKind -- ^ any kind will do
395 | OpenKind -- ^ something of the form @TYPE _@
396
397 -- Depending on the context, we might accept any kind (for instance, in a TH
398 -- splice), or only certain kinds (like in type signatures).
399 expectedKindInCtxt :: UserTypeCtxt -> ContextKind
400 expectedKindInCtxt (TySynCtxt _) = AnythingKind
401 expectedKindInCtxt ThBrackCtxt = AnythingKind
402 expectedKindInCtxt GhciCtxt = AnythingKind
403 -- The types in a 'default' decl can have varying kinds
404 -- See Note [Extended defaults]" in TcEnv
405 expectedKindInCtxt DefaultDeclCtxt = AnythingKind
406 expectedKindInCtxt TypeAppCtxt = AnythingKind
407 expectedKindInCtxt (ForSigCtxt _) = TheKind liftedTypeKind
408 expectedKindInCtxt InstDeclCtxt = TheKind constraintKind
409 expectedKindInCtxt SpecInstCtxt = TheKind constraintKind
410 expectedKindInCtxt _ = OpenKind
411
412 {-
413 Note [Higher rank types]
414 ~~~~~~~~~~~~~~~~~~~~~~~~
415 Technically
416 Int -> forall a. a->a
417 is still a rank-1 type, but it's not Haskell 98 (Trac #5957). So the
418 validity checker allow a forall after an arrow only if we allow it
419 before -- that is, with Rank2Types or RankNTypes
420 -}
421
422 data Rank = ArbitraryRank -- Any rank ok
423
424 | LimitedRank -- Note [Higher rank types]
425 Bool -- Forall ok at top
426 Rank -- Use for function arguments
427
428 | MonoType SDoc -- Monotype, with a suggestion of how it could be a polytype
429
430 | MustBeMonoType -- Monotype regardless of flags
431
432
433 rankZeroMonoType, tyConArgMonoType, synArgMonoType, constraintMonoType :: Rank
434 rankZeroMonoType = MonoType (text "Perhaps you intended to use RankNTypes or Rank2Types")
435 tyConArgMonoType = MonoType (text "GHC doesn't yet support impredicative polymorphism")
436 synArgMonoType = MonoType (text "Perhaps you intended to use LiberalTypeSynonyms")
437 constraintMonoType = MonoType (text "A constraint must be a monotype")
438
439 funArgResRank :: Rank -> (Rank, Rank) -- Function argument and result
440 funArgResRank (LimitedRank _ arg_rank) = (arg_rank, LimitedRank (forAllAllowed arg_rank) arg_rank)
441 funArgResRank other_rank = (other_rank, other_rank)
442
443 forAllAllowed :: Rank -> Bool
444 forAllAllowed ArbitraryRank = True
445 forAllAllowed (LimitedRank forall_ok _) = forall_ok
446 forAllAllowed _ = False
447
448 -- The zonker issues errors if it zonks a representation-polymorphic binder
449 -- But sometimes it's nice to check a little more eagerly, trying to report
450 -- errors earlier.
451 representationPolymorphismForbidden :: UserTypeCtxt -> Bool
452 representationPolymorphismForbidden = go
453 where
454 go (ConArgCtxt _) = True -- A rep-polymorphic datacon won't be useful
455 go (PatSynCtxt _) = True -- Similar to previous case
456 go _ = False -- Other cases are caught by zonker
457
458 ----------------------------------------
459 -- | Fail with error message if the type is unlifted
460 check_lifted :: Type -> TcM ()
461 check_lifted _ = return ()
462
463 {- ------ Legacy comment ---------
464 The check_unlifted function seems entirely redundant. The
465 kind system should check for uses of unlifted types. So I've
466 removed the check. See Trac #11120 comment:19.
467
468 check_lifted ty
469 = do { env <- tcInitOpenTidyEnv (tyCoVarsOfType ty)
470 ; checkTcM (not (isUnliftedType ty)) (unliftedArgErr env ty) }
471
472 unliftedArgErr :: TidyEnv -> Type -> (TidyEnv, SDoc)
473 unliftedArgErr env ty = (env, sep [text "Illegal unlifted type:", ppr_tidy env ty])
474 ------ End of legacy comment --------- -}
475
476
477 check_type :: TidyEnv -> UserTypeCtxt -> Rank -> Type -> TcM ()
478 -- The args say what the *type context* requires, independent
479 -- of *flag* settings. You test the flag settings at usage sites.
480 --
481 -- Rank is allowed rank for function args
482 -- Rank 0 means no for-alls anywhere
483
484 check_type env ctxt rank ty
485 | not (null tvs && null theta)
486 = do { traceTc "check_type" (ppr ty $$ ppr (forAllAllowed rank))
487 ; checkTcM (forAllAllowed rank) (forAllTyErr env rank ty)
488 -- Reject e.g. (Maybe (?x::Int => Int)),
489 -- with a decent error message
490
491 ; check_valid_theta env' SigmaCtxt theta
492 -- Allow type T = ?x::Int => Int -> Int
493 -- but not type T = ?x::Int
494
495 ; check_type env' ctxt rank tau -- Allow foralls to right of arrow
496 ; checkTcM (not (any (`elemVarSet` tyCoVarsOfType phi_kind) tvs))
497 (forAllEscapeErr env' ty tau_kind)
498 }
499 where
500 (tvs, theta, tau) = tcSplitSigmaTy ty
501 tau_kind = typeKind tau
502 (env', _) = tidyTyCoVarBndrs env tvs
503
504 phi_kind | null theta = tau_kind
505 | otherwise = liftedTypeKind
506 -- If there are any constraints, the kind is *. (#11405)
507
508 check_type _ _ _ (TyVarTy _) = return ()
509
510 check_type env ctxt rank (ForAllTy (Anon arg_ty) res_ty)
511 = do { check_type env ctxt arg_rank arg_ty
512 ; when (representationPolymorphismForbidden ctxt) $
513 checkForRepresentationPolymorphism empty arg_ty
514 ; check_type env ctxt res_rank res_ty }
515 where
516 (arg_rank, res_rank) = funArgResRank rank
517
518 check_type env ctxt rank (AppTy ty1 ty2)
519 = do { check_arg_type env ctxt rank ty1
520 ; check_arg_type env ctxt rank ty2 }
521
522 check_type env ctxt rank ty@(TyConApp tc tys)
523 | isTypeSynonymTyCon tc || isTypeFamilyTyCon tc
524 = check_syn_tc_app env ctxt rank ty tc tys
525 | isUnboxedTupleTyCon tc = check_ubx_tuple env ctxt ty tys
526 | otherwise = mapM_ (check_arg_type env ctxt rank) tys
527
528 check_type _ _ _ (LitTy {}) = return ()
529
530 check_type env ctxt rank (CastTy ty _) = check_type env ctxt rank ty
531
532 check_type _ _ _ ty = pprPanic "check_type" (ppr ty)
533
534 ----------------------------------------
535 check_syn_tc_app :: TidyEnv -> UserTypeCtxt -> Rank -> KindOrType
536 -> TyCon -> [KindOrType] -> TcM ()
537 -- Used for type synonyms and type synonym families,
538 -- which must be saturated,
539 -- but not data families, which need not be saturated
540 check_syn_tc_app env ctxt rank ty tc tys
541 | tc_arity <= length tys -- Saturated
542 -- Check that the synonym has enough args
543 -- This applies equally to open and closed synonyms
544 -- It's OK to have an *over-applied* type synonym
545 -- data Tree a b = ...
546 -- type Foo a = Tree [a]
547 -- f :: Foo a b -> ...
548 = do { -- See Note [Liberal type synonyms]
549 ; liberal <- xoptM LangExt.LiberalTypeSynonyms
550 ; if not liberal || isTypeFamilyTyCon tc then
551 -- For H98 and synonym families, do check the type args
552 mapM_ check_arg tys
553
554 else -- In the liberal case (only for closed syns), expand then check
555 case coreView ty of
556 Just ty' -> check_type env ctxt rank ty'
557 Nothing -> pprPanic "check_tau_type" (ppr ty) }
558
559 | GhciCtxt <- ctxt -- Accept under-saturated type synonyms in
560 -- GHCi :kind commands; see Trac #7586
561 = mapM_ check_arg tys
562
563 | otherwise
564 = failWithTc (tyConArityErr tc tys)
565 where
566 tc_arity = tyConArity tc
567 check_arg | isTypeFamilyTyCon tc = check_arg_type env ctxt rank
568 | otherwise = check_type env ctxt synArgMonoType
569
570 ----------------------------------------
571 check_ubx_tuple :: TidyEnv -> UserTypeCtxt -> KindOrType
572 -> [KindOrType] -> TcM ()
573 check_ubx_tuple env ctxt ty tys
574 = do { ub_tuples_allowed <- xoptM LangExt.UnboxedTuples
575 ; checkTcM ub_tuples_allowed (ubxArgTyErr env ty)
576
577 ; impred <- xoptM LangExt.ImpredicativeTypes
578 ; let rank' = if impred then ArbitraryRank else tyConArgMonoType
579 -- c.f. check_arg_type
580 -- However, args are allowed to be unlifted, or
581 -- more unboxed tuples, so can't use check_arg_ty
582 ; mapM_ (check_type env ctxt rank') tys }
583
584 ----------------------------------------
585 check_arg_type :: TidyEnv -> UserTypeCtxt -> Rank -> KindOrType -> TcM ()
586 -- The sort of type that can instantiate a type variable,
587 -- or be the argument of a type constructor.
588 -- Not an unboxed tuple, but now *can* be a forall (since impredicativity)
589 -- Other unboxed types are very occasionally allowed as type
590 -- arguments depending on the kind of the type constructor
591 --
592 -- For example, we want to reject things like:
593 --
594 -- instance Ord a => Ord (forall s. T s a)
595 -- and
596 -- g :: T s (forall b.b)
597 --
598 -- NB: unboxed tuples can have polymorphic or unboxed args.
599 -- This happens in the workers for functions returning
600 -- product types with polymorphic components.
601 -- But not in user code.
602 -- Anyway, they are dealt with by a special case in check_tau_type
603
604 check_arg_type _ _ _ (CoercionTy {}) = return ()
605
606 check_arg_type env ctxt rank ty
607 = do { impred <- xoptM LangExt.ImpredicativeTypes
608 ; let rank' = case rank of -- Predictive => must be monotype
609 MustBeMonoType -> MustBeMonoType -- Monotype, regardless
610 _other | impred -> ArbitraryRank
611 | otherwise -> tyConArgMonoType
612 -- Make sure that MustBeMonoType is propagated,
613 -- so that we don't suggest -XImpredicativeTypes in
614 -- (Ord (forall a.a)) => a -> a
615 -- and so that if it Must be a monotype, we check that it is!
616
617 ; check_type env ctxt rank' ty
618 ; check_lifted ty }
619 -- NB the isUnliftedType test also checks for
620 -- T State#
621 -- where there is an illegal partial application of State# (which has
622 -- kind * -> #); see Note [The kind invariant] in TyCoRep
623
624 ----------------------------------------
625 forAllTyErr :: TidyEnv -> Rank -> Type -> (TidyEnv, SDoc)
626 forAllTyErr env rank ty
627 = ( env
628 , vcat [ hang herald 2 (ppr_tidy env ty)
629 , suggestion ] )
630 where
631 (tvs, _theta, _tau) = tcSplitSigmaTy ty
632 herald | null tvs = text "Illegal qualified type:"
633 | otherwise = text "Illegal polymorphic type:"
634 suggestion = case rank of
635 LimitedRank {} -> text "Perhaps you intended to use RankNTypes or Rank2Types"
636 MonoType d -> d
637 _ -> Outputable.empty -- Polytype is always illegal
638
639 forAllEscapeErr :: TidyEnv -> Type -> Kind -> (TidyEnv, SDoc)
640 forAllEscapeErr env ty tau_kind
641 = ( env
642 , hang (vcat [ text "Quantified type's kind mentions quantified type variable"
643 , text "(skolem escape)" ])
644 2 (vcat [ text " type:" <+> ppr_tidy env ty
645 , text "of kind:" <+> ppr_tidy env tau_kind ]) )
646
647 ubxArgTyErr :: TidyEnv -> Type -> (TidyEnv, SDoc)
648 ubxArgTyErr env ty = (env, sep [text "Illegal unboxed tuple type as function argument:", ppr_tidy env ty])
649
650 kindErr :: TidyEnv -> Kind -> (TidyEnv, SDoc)
651 kindErr env kind = (env, sep [text "Expecting an ordinary type, but found a type of kind", ppr_tidy env kind])
652
653 {-
654 Note [Liberal type synonyms]
655 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
656 If -XLiberalTypeSynonyms is on, expand closed type synonyms *before*
657 doing validity checking. This allows us to instantiate a synonym defn
658 with a for-all type, or with a partially-applied type synonym.
659 e.g. type T a b = a
660 type S m = m ()
661 f :: S (T Int)
662 Here, T is partially applied, so it's illegal in H98. But if you
663 expand S first, then T we get just
664 f :: Int
665 which is fine.
666
667 IMPORTANT: suppose T is a type synonym. Then we must do validity
668 checking on an appliation (T ty1 ty2)
669
670 *either* before expansion (i.e. check ty1, ty2)
671 *or* after expansion (i.e. expand T ty1 ty2, and then check)
672 BUT NOT BOTH
673
674 If we do both, we get exponential behaviour!!
675
676 data TIACons1 i r c = c i ::: r c
677 type TIACons2 t x = TIACons1 t (TIACons1 t x)
678 type TIACons3 t x = TIACons2 t (TIACons1 t x)
679 type TIACons4 t x = TIACons2 t (TIACons2 t x)
680 type TIACons7 t x = TIACons4 t (TIACons3 t x)
681
682
683 ************************************************************************
684 * *
685 \subsection{Checking a theta or source type}
686 * *
687 ************************************************************************
688
689 Note [Implicit parameters in instance decls]
690 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
691 Implicit parameters _only_ allowed in type signatures; not in instance
692 decls, superclasses etc. The reason for not allowing implicit params in
693 instances is a bit subtle. If we allowed
694 instance (?x::Int, Eq a) => Foo [a] where ...
695 then when we saw
696 (e :: (?x::Int) => t)
697 it would be unclear how to discharge all the potential uses of the ?x
698 in e. For example, a constraint Foo [Int] might come out of e, and
699 applying the instance decl would show up two uses of ?x. Trac #8912.
700 -}
701
702 checkValidTheta :: UserTypeCtxt -> ThetaType -> TcM ()
703 -- Assumes arguemt is fully zonked
704 checkValidTheta ctxt theta
705 = do { env <- tcInitOpenTidyEnv (tyCoVarsOfTypes theta)
706 ; addErrCtxtM (checkThetaCtxt ctxt theta) $
707 check_valid_theta env ctxt theta }
708
709 -------------------------
710 check_valid_theta :: TidyEnv -> UserTypeCtxt -> [PredType] -> TcM ()
711 check_valid_theta _ _ []
712 = return ()
713 check_valid_theta env ctxt theta
714 = do { dflags <- getDynFlags
715 ; warnTcM (Reason Opt_WarnDuplicateConstraints)
716 (wopt Opt_WarnDuplicateConstraints dflags && notNull dups)
717 (dupPredWarn env dups)
718 ; traceTc "check_valid_theta" (ppr theta)
719 ; mapM_ (check_pred_ty env dflags ctxt) theta }
720 where
721 (_,dups) = removeDups cmpType theta
722
723 -------------------------
724 {- Note [Validity checking for constraints]
725 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
726 We look through constraint synonyms so that we can see the underlying
727 constraint(s). For example
728 type Foo = ?x::Int
729 instance Foo => C T
730 We should reject the instance because it has an implicit parameter in
731 the context.
732
733 But we record, in 'under_syn', whether we have looked under a synonym
734 to avoid requiring language extensions at the use site. Main example
735 (Trac #9838):
736
737 {-# LANGUAGE ConstraintKinds #-}
738 module A where
739 type EqShow a = (Eq a, Show a)
740
741 module B where
742 import A
743 foo :: EqShow a => a -> String
744
745 We don't want to require ConstraintKinds in module B.
746 -}
747
748 check_pred_ty :: TidyEnv -> DynFlags -> UserTypeCtxt -> PredType -> TcM ()
749 -- Check the validity of a predicate in a signature
750 -- See Note [Validity checking for constraints]
751 check_pred_ty env dflags ctxt pred
752 = do { check_type env SigmaCtxt constraintMonoType pred
753 ; check_pred_help False env dflags ctxt pred }
754
755 check_pred_help :: Bool -- True <=> under a type synonym
756 -> TidyEnv
757 -> DynFlags -> UserTypeCtxt
758 -> PredType -> TcM ()
759 check_pred_help under_syn env dflags ctxt pred
760 | Just pred' <- coreView pred -- Switch on under_syn when going under a
761 -- synonym (Trac #9838, yuk)
762 = check_pred_help True env dflags ctxt pred'
763 | otherwise
764 = case splitTyConApp_maybe pred of
765 Just (tc, tys)
766 | isTupleTyCon tc
767 -> check_tuple_pred under_syn env dflags ctxt pred tys
768 -- NB: this equality check must come first, because (~) is a class,
769 -- too.
770 | tc `hasKey` heqTyConKey ||
771 tc `hasKey` eqTyConKey ||
772 tc `hasKey` eqPrimTyConKey
773 -> check_eq_pred env dflags pred tc tys
774 | Just cls <- tyConClass_maybe tc
775 -> check_class_pred env dflags ctxt pred cls tys -- Includes Coercible
776 _ -> check_irred_pred under_syn env dflags ctxt pred
777
778 check_eq_pred :: TidyEnv -> DynFlags -> PredType -> TyCon -> [TcType] -> TcM ()
779 check_eq_pred env dflags pred tc tys
780 = -- Equational constraints are valid in all contexts if type
781 -- families are permitted
782 do { checkTc (length tys == tyConArity tc) (tyConArityErr tc tys)
783 ; checkTcM (xopt LangExt.TypeFamilies dflags
784 || xopt LangExt.GADTs dflags)
785 (eqPredTyErr env pred) }
786
787 check_tuple_pred :: Bool -> TidyEnv -> DynFlags -> UserTypeCtxt -> PredType -> [PredType] -> TcM ()
788 check_tuple_pred under_syn env dflags ctxt pred ts
789 = do { -- See Note [ConstraintKinds in predicates]
790 checkTcM (under_syn || xopt LangExt.ConstraintKinds dflags)
791 (predTupleErr env pred)
792 ; mapM_ (check_pred_help under_syn env dflags ctxt) ts }
793 -- This case will not normally be executed because without
794 -- -XConstraintKinds tuple types are only kind-checked as *
795
796 check_irred_pred :: Bool -> TidyEnv -> DynFlags -> UserTypeCtxt -> PredType -> TcM ()
797 check_irred_pred under_syn env dflags ctxt pred
798 -- The predicate looks like (X t1 t2) or (x t1 t2) :: Constraint
799 -- where X is a type function
800 = do { -- If it looks like (x t1 t2), require ConstraintKinds
801 -- see Note [ConstraintKinds in predicates]
802 -- But (X t1 t2) is always ok because we just require ConstraintKinds
803 -- at the definition site (Trac #9838)
804 failIfTcM (not under_syn && not (xopt LangExt.ConstraintKinds dflags)
805 && hasTyVarHead pred)
806 (predIrredErr env pred)
807
808 -- Make sure it is OK to have an irred pred in this context
809 -- See Note [Irreducible predicates in superclasses]
810 ; failIfTcM (is_superclass ctxt
811 && not (xopt LangExt.UndecidableInstances dflags)
812 && has_tyfun_head pred)
813 (predSuperClassErr env pred) }
814 where
815 is_superclass ctxt = case ctxt of { ClassSCCtxt _ -> True; _ -> False }
816 has_tyfun_head ty
817 = case tcSplitTyConApp_maybe ty of
818 Just (tc, _) -> isTypeFamilyTyCon tc
819 Nothing -> False
820
821 {- Note [ConstraintKinds in predicates]
822 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
823 Don't check for -XConstraintKinds under a type synonym, because that
824 was done at the type synonym definition site; see Trac #9838
825 e.g. module A where
826 type C a = (Eq a, Ix a) -- Needs -XConstraintKinds
827 module B where
828 import A
829 f :: C a => a -> a -- Does *not* need -XConstraintKinds
830
831 Note [Irreducible predicates in superclasses]
832 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
833 Allowing type-family calls in class superclasses is somewhat dangerous
834 because we can write:
835
836 type family Fooish x :: * -> Constraint
837 type instance Fooish () = Foo
838 class Fooish () a => Foo a where
839
840 This will cause the constraint simplifier to loop because every time we canonicalise a
841 (Foo a) class constraint we add a (Fooish () a) constraint which will be immediately
842 solved to add+canonicalise another (Foo a) constraint. -}
843
844 -------------------------
845 check_class_pred :: TidyEnv -> DynFlags -> UserTypeCtxt -> PredType -> Class -> [TcType] -> TcM ()
846 check_class_pred env dflags ctxt pred cls tys
847 | isIPClass cls
848 = do { check_arity
849 ; checkTcM (okIPCtxt ctxt) (badIPPred env pred) }
850
851 | otherwise
852 = do { check_arity
853 ; checkTcM arg_tys_ok (env, predTyVarErr (tidyType env pred)) }
854 where
855 check_arity = checkTc (classArity cls == length tys)
856 (tyConArityErr (classTyCon cls) tys)
857 flexible_contexts = xopt LangExt.FlexibleContexts dflags
858 undecidable_ok = xopt LangExt.UndecidableInstances dflags
859
860 arg_tys_ok = case ctxt of
861 SpecInstCtxt -> True -- {-# SPECIALISE instance Eq (T Int) #-} is fine
862 InstDeclCtxt -> checkValidClsArgs (flexible_contexts || undecidable_ok) cls tys
863 -- Further checks on head and theta
864 -- in checkInstTermination
865 _ -> checkValidClsArgs flexible_contexts cls tys
866
867 -------------------------
868 okIPCtxt :: UserTypeCtxt -> Bool
869 -- See Note [Implicit parameters in instance decls]
870 okIPCtxt (FunSigCtxt {}) = True
871 okIPCtxt (InfSigCtxt {}) = True
872 okIPCtxt ExprSigCtxt = True
873 okIPCtxt TypeAppCtxt = True
874 okIPCtxt PatSigCtxt = True
875 okIPCtxt ResSigCtxt = True
876 okIPCtxt GenSigCtxt = True
877 okIPCtxt (ConArgCtxt {}) = True
878 okIPCtxt (ForSigCtxt {}) = True -- ??
879 okIPCtxt ThBrackCtxt = True
880 okIPCtxt GhciCtxt = True
881 okIPCtxt SigmaCtxt = True
882 okIPCtxt (DataTyCtxt {}) = True
883 okIPCtxt (PatSynCtxt {}) = True
884 okIPCtxt (TySynCtxt {}) = True -- e.g. type Blah = ?x::Int
885 -- Trac #11466
886
887 okIPCtxt (ClassSCCtxt {}) = False
888 okIPCtxt (InstDeclCtxt {}) = False
889 okIPCtxt (SpecInstCtxt {}) = False
890 okIPCtxt (RuleSigCtxt {}) = False
891 okIPCtxt DefaultDeclCtxt = False
892
893 badIPPred :: TidyEnv -> PredType -> (TidyEnv, SDoc)
894 badIPPred env pred
895 = ( env
896 , text "Illegal implicit parameter" <+> quotes (ppr_tidy env pred) )
897
898 {-
899 Note [Kind polymorphic type classes]
900 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
901 MultiParam check:
902
903 class C f where... -- C :: forall k. k -> Constraint
904 instance C Maybe where...
905
906 The dictionary gets type [C * Maybe] even if it's not a MultiParam
907 type class.
908
909 Flexibility check:
910
911 class C f where... -- C :: forall k. k -> Constraint
912 data D a = D a
913 instance C D where
914
915 The dictionary gets type [C * (D *)]. IA0_TODO it should be
916 generalized actually.
917 -}
918
919 checkThetaCtxt :: UserTypeCtxt -> ThetaType -> TidyEnv -> TcM (TidyEnv, SDoc)
920 checkThetaCtxt ctxt theta env
921 = return ( env
922 , vcat [ text "In the context:" <+> pprTheta (tidyTypes env theta)
923 , text "While checking" <+> pprUserTypeCtxt ctxt ] )
924
925 eqPredTyErr, predTupleErr, predIrredErr, predSuperClassErr :: TidyEnv -> PredType -> (TidyEnv, SDoc)
926 eqPredTyErr env pred
927 = ( env
928 , text "Illegal equational constraint" <+> ppr_tidy env pred $$
929 parens (text "Use GADTs or TypeFamilies to permit this") )
930 predTupleErr env pred
931 = ( env
932 , hang (text "Illegal tuple constraint:" <+> ppr_tidy env pred)
933 2 (parens constraintKindsMsg) )
934 predIrredErr env pred
935 = ( env
936 , hang (text "Illegal constraint:" <+> ppr_tidy env pred)
937 2 (parens constraintKindsMsg) )
938 predSuperClassErr env pred
939 = ( env
940 , hang (text "Illegal constraint" <+> quotes (ppr_tidy env pred)
941 <+> text "in a superclass context")
942 2 (parens undecidableMsg) )
943
944 predTyVarErr :: PredType -> SDoc -- type is already tidied!
945 predTyVarErr pred
946 = vcat [ hang (text "Non type-variable argument")
947 2 (text "in the constraint:" <+> ppr pred)
948 , parens (text "Use FlexibleContexts to permit this") ]
949
950 constraintSynErr :: TidyEnv -> Type -> (TidyEnv, SDoc)
951 constraintSynErr env kind
952 = ( env
953 , hang (text "Illegal constraint synonym of kind:" <+> quotes (ppr_tidy env kind))
954 2 (parens constraintKindsMsg) )
955
956 dupPredWarn :: TidyEnv -> [[PredType]] -> (TidyEnv, SDoc)
957 dupPredWarn env dups
958 = ( env
959 , text "Duplicate constraint" <> plural primaryDups <> text ":"
960 <+> pprWithCommas (ppr_tidy env) primaryDups )
961 where
962 primaryDups = map head dups
963
964 tyConArityErr :: TyCon -> [TcType] -> SDoc
965 -- For type-constructor arity errors, be careful to report
966 -- the number of /visible/ arguments required and supplied,
967 -- ignoring the /invisible/ arguments, which the user does not see.
968 -- (e.g. Trac #10516)
969 tyConArityErr tc tks
970 = arityErr (tyConFlavour tc) (tyConName tc)
971 tc_type_arity tc_type_args
972 where
973 vis_tks = filterOutInvisibleTypes tc tks
974
975 -- tc_type_arity = number of *type* args expected
976 -- tc_type_args = number of *type* args encountered
977 tc_type_arity = count isVisibleBinder $ tyConBinders tc
978 tc_type_args = length vis_tks
979
980 arityErr :: Outputable a => String -> a -> Int -> Int -> SDoc
981 arityErr what name n m
982 = hsep [ text "The" <+> text what, quotes (ppr name), text "should have",
983 n_arguments <> comma, text "but has been given",
984 if m==0 then text "none" else int m]
985 where
986 n_arguments | n == 0 = text "no arguments"
987 | n == 1 = text "1 argument"
988 | True = hsep [int n, text "arguments"]
989
990 {-
991 ************************************************************************
992 * *
993 \subsection{Checking for a decent instance head type}
994 * *
995 ************************************************************************
996
997 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
998 it must normally look like: @instance Foo (Tycon a b c ...) ...@
999
1000 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1001 flag is on, or (2)~the instance is imported (they must have been
1002 compiled elsewhere). In these cases, we let them go through anyway.
1003
1004 We can also have instances for functions: @instance Foo (a -> b) ...@.
1005 -}
1006
1007 checkValidInstHead :: UserTypeCtxt -> Class -> [Type] -> TcM ()
1008 checkValidInstHead ctxt clas cls_args
1009 = do { dflags <- getDynFlags
1010
1011 ; mod <- getModule
1012 ; checkTc (getUnique clas `notElem` abstractClassKeys ||
1013 nameModule (getName clas) == mod)
1014 (instTypeErr clas cls_args abstract_class_msg)
1015
1016 -- Check language restrictions;
1017 -- but not for SPECIALISE instance pragmas
1018 ; let ty_args = filterOutInvisibleTypes (classTyCon clas) cls_args
1019 ; unless spec_inst_prag $
1020 do { checkTc (xopt LangExt.TypeSynonymInstances dflags ||
1021 all tcInstHeadTyNotSynonym ty_args)
1022 (instTypeErr clas cls_args head_type_synonym_msg)
1023 ; checkTc (xopt LangExt.FlexibleInstances dflags ||
1024 all tcInstHeadTyAppAllTyVars ty_args)
1025 (instTypeErr clas cls_args head_type_args_tyvars_msg)
1026 ; checkTc (xopt LangExt.MultiParamTypeClasses dflags ||
1027 length ty_args == 1 || -- Only count type arguments
1028 (xopt LangExt.NullaryTypeClasses dflags &&
1029 null ty_args))
1030 (instTypeErr clas cls_args head_one_type_msg) }
1031
1032 ; mapM_ checkValidTypePat ty_args }
1033 where
1034 spec_inst_prag = case ctxt of { SpecInstCtxt -> True; _ -> False }
1035
1036 head_type_synonym_msg = parens (
1037 text "All instance types must be of the form (T t1 ... tn)" $$
1038 text "where T is not a synonym." $$
1039 text "Use TypeSynonymInstances if you want to disable this.")
1040
1041 head_type_args_tyvars_msg = parens (vcat [
1042 text "All instance types must be of the form (T a1 ... an)",
1043 text "where a1 ... an are *distinct type variables*,",
1044 text "and each type variable appears at most once in the instance head.",
1045 text "Use FlexibleInstances if you want to disable this."])
1046
1047 head_one_type_msg = parens (
1048 text "Only one type can be given in an instance head." $$
1049 text "Use MultiParamTypeClasses if you want to allow more, or zero.")
1050
1051 abstract_class_msg =
1052 text "Manual instances of this class are not permitted."
1053
1054 tcInstHeadTyNotSynonym :: Type -> Bool
1055 -- Used in Haskell-98 mode, for the argument types of an instance head
1056 -- These must not be type synonyms, but everywhere else type synonyms
1057 -- are transparent, so we need a special function here
1058 tcInstHeadTyNotSynonym ty
1059 = case ty of -- Do not use splitTyConApp,
1060 -- because that expands synonyms!
1061 TyConApp tc _ -> not (isTypeSynonymTyCon tc)
1062 _ -> True
1063
1064 tcInstHeadTyAppAllTyVars :: Type -> Bool
1065 -- Used in Haskell-98 mode, for the argument types of an instance head
1066 -- These must be a constructor applied to type variable arguments.
1067 -- But we allow kind instantiations.
1068 tcInstHeadTyAppAllTyVars ty
1069 | Just (tc, tys) <- tcSplitTyConApp_maybe (dropCasts ty)
1070 = ok (filterOutInvisibleTypes tc tys) -- avoid kinds
1071
1072 | otherwise
1073 = False
1074 where
1075 -- Check that all the types are type variables,
1076 -- and that each is distinct
1077 ok tys = equalLength tvs tys && hasNoDups tvs
1078 where
1079 tvs = mapMaybe tcGetTyVar_maybe tys
1080
1081 dropCasts :: Type -> Type
1082 -- See Note [Casts during validity checking]
1083 -- This function can turn a well-kinded type into an ill-kinded
1084 -- one, so I've kept it local to this module
1085 -- To consider: drop only UnivCo(HoleProv) casts
1086 dropCasts (CastTy ty _) = dropCasts ty
1087 dropCasts (AppTy t1 t2) = mkAppTy (dropCasts t1) (dropCasts t2)
1088 dropCasts (TyConApp tc tys) = mkTyConApp tc (map dropCasts tys)
1089 dropCasts (ForAllTy b ty) = ForAllTy (dropCastsB b) (dropCasts ty)
1090 dropCasts ty = ty -- LitTy, TyVarTy, CoercionTy
1091
1092 dropCastsB :: TyBinder -> TyBinder
1093 dropCastsB (Anon ty) = Anon (dropCasts ty)
1094 dropCastsB b = b -- Don't bother in the kind of a forall
1095
1096 abstractClassKeys :: [Unique]
1097 abstractClassKeys = [ heqTyConKey
1098 , eqTyConKey
1099 , coercibleTyConKey
1100 ] -- See Note [Equality class instances]
1101
1102 instTypeErr :: Class -> [Type] -> SDoc -> SDoc
1103 instTypeErr cls tys msg
1104 = hang (hang (text "Illegal instance declaration for")
1105 2 (quotes (pprClassPred cls tys)))
1106 2 msg
1107
1108 {- Note [Casts during validity checking]
1109 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1110 Consider the (bogus)
1111 instance Eq Char#
1112 We elaborate to 'Eq (Char# |> UnivCo(hole))' where the hole is an
1113 insoluble equality constraint for * ~ #. We'll report the insoluble
1114 constraint separately, but we don't want to *also* complain that Eq is
1115 not applied to a type constructor. So we look gaily look through
1116 CastTys here.
1117
1118 Another example: Eq (Either a). Then we actually get a cast in
1119 the middle:
1120 Eq ((Either |> g) a)
1121
1122
1123 Note [Valid 'deriving' predicate]
1124 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1125 validDerivPred checks for OK 'deriving' context. See Note [Exotic
1126 derived instance contexts] in TcDeriv. However the predicate is
1127 here because it uses sizeTypes, fvTypes.
1128
1129 It checks for three things
1130
1131 * No repeated variables (hasNoDups fvs)
1132
1133 * No type constructors. This is done by comparing
1134 sizeTypes tys == length (fvTypes tys)
1135 sizeTypes counts variables and constructors; fvTypes returns variables.
1136 So if they are the same, there must be no constructors. But there
1137 might be applications thus (f (g x)).
1138
1139 * Also check for a bizarre corner case, when the derived instance decl
1140 would look like
1141 instance C a b => D (T a) where ...
1142 Note that 'b' isn't a parameter of T. This gives rise to all sorts of
1143 problems; in particular, it's hard to compare solutions for equality
1144 when finding the fixpoint, and that means the inferContext loop does
1145 not converge. See Trac #5287.
1146
1147 Note [Equality class instances]
1148 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1149 We can't have users writing instances for the equality classes. But we
1150 still need to be able to write instances for them ourselves. So we allow
1151 instances only in the defining module.
1152
1153 -}
1154
1155 validDerivPred :: TyVarSet -> PredType -> Bool
1156 -- See Note [Valid 'deriving' predicate]
1157 validDerivPred tv_set pred
1158 = case classifyPredType pred of
1159 ClassPred cls _ -> cls `hasKey` typeableClassKey
1160 -- Typeable constraints are bigger than they appear due
1161 -- to kind polymorphism, but that's OK
1162 || check_tys
1163 EqPred {} -> False -- reject equality constraints
1164 _ -> True -- Non-class predicates are ok
1165 where
1166 check_tys = hasNoDups fvs
1167 -- use sizePred to ignore implicit args
1168 && sizePred pred == fromIntegral (length fvs)
1169 && all (`elemVarSet` tv_set) fvs
1170
1171 fvs = fvType pred
1172
1173 {-
1174 ************************************************************************
1175 * *
1176 \subsection{Checking instance for termination}
1177 * *
1178 ************************************************************************
1179 -}
1180
1181 checkValidInstance :: UserTypeCtxt -> LHsSigType Name -> Type
1182 -> TcM ([TyVar], ThetaType, Class, [Type])
1183 checkValidInstance ctxt hs_type ty
1184 | Just (clas,inst_tys) <- getClassPredTys_maybe tau
1185 , inst_tys `lengthIs` classArity clas
1186 = do { setSrcSpan head_loc (checkValidInstHead ctxt clas inst_tys)
1187 ; traceTc "checkValidInstance {" (ppr ty)
1188 ; checkValidTheta ctxt theta
1189
1190 -- The Termination and Coverate Conditions
1191 -- Check that instance inference will terminate (if we care)
1192 -- For Haskell 98 this will already have been done by checkValidTheta,
1193 -- but as we may be using other extensions we need to check.
1194 --
1195 -- Note that the Termination Condition is *more conservative* than
1196 -- the checkAmbiguity test we do on other type signatures
1197 -- e.g. Bar a => Bar Int is ambiguous, but it also fails
1198 -- the termination condition, because 'a' appears more often
1199 -- in the constraint than in the head
1200 ; undecidable_ok <- xoptM LangExt.UndecidableInstances
1201 ; if undecidable_ok
1202 then checkAmbiguity ctxt ty
1203 else checkInstTermination inst_tys theta
1204
1205 ; traceTc "cvi 2" (ppr ty)
1206
1207 ; case (checkInstCoverage undecidable_ok clas theta inst_tys) of
1208 IsValid -> return () -- Check succeeded
1209 NotValid msg -> addErrTc (instTypeErr clas inst_tys msg)
1210
1211 ; traceTc "End checkValidInstance }" empty
1212
1213 ; return (tvs, theta, clas, inst_tys) }
1214
1215 | otherwise
1216 = failWithTc (text "Malformed instance head:" <+> ppr tau)
1217 where
1218 (tvs, theta, tau) = tcSplitSigmaTy ty
1219
1220 -- The location of the "head" of the instance
1221 head_loc = getLoc (getLHsInstDeclHead hs_type)
1222
1223 {-
1224 Note [Paterson conditions]
1225 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1226 Termination test: the so-called "Paterson conditions" (see Section 5 of
1227 "Understanding functional dependencies via Constraint Handling Rules,
1228 JFP Jan 2007).
1229
1230 We check that each assertion in the context satisfies:
1231 (1) no variable has more occurrences in the assertion than in the head, and
1232 (2) the assertion has fewer constructors and variables (taken together
1233 and counting repetitions) than the head.
1234 This is only needed with -fglasgow-exts, as Haskell 98 restrictions
1235 (which have already been checked) guarantee termination.
1236
1237 The underlying idea is that
1238
1239 for any ground substitution, each assertion in the
1240 context has fewer type constructors than the head.
1241 -}
1242
1243 checkInstTermination :: [TcType] -> ThetaType -> TcM ()
1244 -- See Note [Paterson conditions]
1245 checkInstTermination tys theta
1246 = check_preds theta
1247 where
1248 head_fvs = fvTypes tys
1249 head_size = sizeTypes tys
1250
1251 check_preds :: [PredType] -> TcM ()
1252 check_preds preds = mapM_ check preds
1253
1254 check :: PredType -> TcM ()
1255 check pred
1256 = case classifyPredType pred of
1257 EqPred {} -> return () -- See Trac #4200.
1258 IrredPred {} -> check2 pred (sizeType pred)
1259 ClassPred cls tys
1260 | isTerminatingClass cls
1261 -> return ()
1262
1263 | isCTupleClass cls -- Look inside tuple predicates; Trac #8359
1264 -> check_preds tys
1265
1266 | otherwise
1267 -> check2 pred (sizeTypes $ filterOutInvisibleTypes (classTyCon cls) tys)
1268 -- Other ClassPreds
1269
1270 check2 pred pred_size
1271 | not (null bad_tvs) = addErrTc (noMoreMsg bad_tvs what)
1272 | pred_size >= head_size = addErrTc (smallerMsg what)
1273 | otherwise = return ()
1274 where
1275 what = text "constraint" <+> quotes (ppr pred)
1276 bad_tvs = fvType pred \\ head_fvs
1277
1278 smallerMsg :: SDoc -> SDoc
1279 smallerMsg what
1280 = vcat [ hang (text "The" <+> what)
1281 2 (text "is no smaller than the instance head")
1282 , parens undecidableMsg ]
1283
1284 noMoreMsg :: [TcTyVar] -> SDoc -> SDoc
1285 noMoreMsg tvs what
1286 = vcat [ hang (text "Variable" <> plural tvs <+> quotes (pprWithCommas ppr tvs)
1287 <+> occurs <+> text "more often")
1288 2 (sep [ text "in the" <+> what
1289 , text "than in the instance head" ])
1290 , parens undecidableMsg ]
1291 where
1292 occurs = if isSingleton tvs then text "occurs"
1293 else text "occur"
1294
1295 undecidableMsg, constraintKindsMsg :: SDoc
1296 undecidableMsg = text "Use UndecidableInstances to permit this"
1297 constraintKindsMsg = text "Use ConstraintKinds to permit this"
1298
1299 {-
1300 Note [Associated type instances]
1301 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1302 We allow this:
1303 class C a where
1304 type T x a
1305 instance C Int where
1306 type T (S y) Int = y
1307 type T Z Int = Char
1308
1309 Note that
1310 a) The variable 'x' is not bound by the class decl
1311 b) 'x' is instantiated to a non-type-variable in the instance
1312 c) There are several type instance decls for T in the instance
1313
1314 All this is fine. Of course, you can't give any *more* instances
1315 for (T ty Int) elsewhere, because it's an *associated* type.
1316
1317 Note [Checking consistent instantiation]
1318 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1319 class C a b where
1320 type T a x b
1321
1322 instance C [p] Int
1323 type T [p] y Int = (p,y,y) -- Induces the family instance TyCon
1324 -- type TR p y = (p,y,y)
1325
1326 So we
1327 * Form the mini-envt from the class type variables a,b
1328 to the instance decl types [p],Int: [a->[p], b->Int]
1329
1330 * Look at the tyvars a,x,b of the type family constructor T
1331 (it shares tyvars with the class C)
1332
1333 * Apply the mini-evnt to them, and check that the result is
1334 consistent with the instance types [p] y Int
1335
1336 We do *not* assume (at this point) the the bound variables of
1337 the associated type instance decl are the same as for the parent
1338 instance decl. So, for example,
1339
1340 instance C [p] Int
1341 type T [q] y Int = ...
1342
1343 would work equally well. Reason: making the *kind* variables line
1344 up is much harder. Example (Trac #7282):
1345 class Foo (xs :: [k]) where
1346 type Bar xs :: *
1347
1348 instance Foo '[] where
1349 type Bar '[] = Int
1350 Here the instance decl really looks like
1351 instance Foo k ('[] k) where
1352 type Bar k ('[] k) = Int
1353 but the k's are not scoped, and hence won't match Uniques.
1354
1355 So instead we just match structure, with tcMatchTyX, and check
1356 that distinct type variables match 1-1 with distinct type variables.
1357
1358 HOWEVER, we *still* make the instance type variables scope over the
1359 type instances, to pick up non-obvious kinds. Eg
1360 class Foo (a :: k) where
1361 type F a
1362 instance Foo (b :: k -> k) where
1363 type F b = Int
1364 Here the instance is kind-indexed and really looks like
1365 type F (k->k) (b::k->k) = Int
1366 But if the 'b' didn't scope, we would make F's instance too
1367 poly-kinded.
1368 -}
1369
1370 -- | Extra information needed when type-checking associated types. The 'Class' is
1371 -- the enclosing class, and the @VarEnv Type@ maps class variables to their
1372 -- instance types.
1373 type ClsInfo = (Class, VarEnv Type)
1374
1375 checkConsistentFamInst
1376 :: Maybe ClsInfo
1377 -> TyCon -- ^ Family tycon
1378 -> [TyVar] -- ^ Type variables of the family instance
1379 -> [Type] -- ^ Type patterns from instance
1380 -> TcM ()
1381 -- See Note [Checking consistent instantiation]
1382
1383 checkConsistentFamInst Nothing _ _ _ = return ()
1384 checkConsistentFamInst (Just (clas, mini_env)) fam_tc at_tvs at_tys
1385 = do { -- Check that the associated type indeed comes from this class
1386 checkTc (Just clas == tyConAssoc_maybe fam_tc)
1387 (badATErr (className clas) (tyConName fam_tc))
1388
1389 -- See Note [Checking consistent instantiation]
1390 -- Check right to left, so that we spot type variable
1391 -- inconsistencies before (more confusing) kind variables
1392 ; checkTc (check_args emptyTCvSubst (fam_tc_tvs `zip` at_tys))
1393 (wrongATArgErr fam_tc expected_args at_tys) }
1394 where
1395 fam_tc_tvs = tyConTyVars fam_tc
1396 expected_args = zipWith pick fam_tc_tvs at_tys
1397 pick fam_tc_tv at_ty = case lookupVarEnv mini_env fam_tc_tv of
1398 Just inst_ty -> inst_ty
1399 Nothing -> at_ty
1400
1401 check_args :: TCvSubst -> [(TyVar,Type)] -> Bool
1402 check_args subst ((fam_tc_tv, at_ty) : rest)
1403 | Just inst_ty <- lookupVarEnv mini_env fam_tc_tv
1404 = case tcMatchTyX subst at_ty inst_ty of
1405 Just subst -> check_args subst rest
1406 Nothing -> False
1407
1408 | otherwise
1409 = check_args subst rest
1410
1411 check_args subst []
1412 = check_tvs subst [] at_tvs
1413
1414 check_tvs :: TCvSubst -> [TyVar] -> [TyVar] -> Bool
1415 check_tvs _ _ [] = True -- OK!!
1416 check_tvs subst acc (tv:tvs)
1417 | Just ty <- lookupTyVar subst tv
1418 = case tcGetTyVar_maybe ty of
1419 Nothing -> False
1420 Just tv' | tv' `elem` acc -> False
1421 | otherwise -> check_tvs subst (tv' : acc) tvs
1422 | otherwise
1423 = check_tvs subst acc tvs
1424
1425 {-
1426 check_arg :: (TyVar, Type) -> TCvSubst -> TcM TCvSubst
1427 check_arg (fam_tc_tv, at_ty) subst
1428 | Just inst_ty <- lookupVarEnv mini_env fam_tc_tv
1429 = case tcMatchTyX subst at_ty inst_ty of
1430 Just subst -> return subst
1431 Nothing -> failWithTc $ wrongATArgErr at_ty inst_ty
1432 -- No need to instantiate here, because the axiom
1433 -- uses the same type variables as the assocated class
1434 | otherwise
1435 = return subst -- Allow non-type-variable instantiation
1436 -- See Note [Associated type instances]
1437
1438 check_distinct :: TCvSubst -> TcM ()
1439 -- True if all the variables mapped the substitution
1440 -- map to *distinct* type *variables*
1441 check_distinct subst = go [] at_tvs
1442 where
1443 go _ [] = return ()
1444 go acc (tv:tvs) = case lookupTyVar subst tv of
1445 Nothing -> go acc tvs
1446 Just ty | Just tv' <- tcGetTyVar_maybe ty
1447 , tv' `notElem` acc
1448 -> go (tv' : acc) tvs
1449 _other -> addErrTc (dupTyVar tv)
1450 -}
1451
1452 badATErr :: Name -> Name -> SDoc
1453 badATErr clas op
1454 = hsep [text "Class", quotes (ppr clas),
1455 text "does not have an associated type", quotes (ppr op)]
1456
1457 wrongATArgErr :: TyCon -> [Type] -> [Type] -> SDoc
1458 wrongATArgErr fam_tc expected_args actual_args
1459 = vcat [ text "Type indexes must match class instance head"
1460 , text "Expected:" <+> ppr (mkTyConApp fam_tc expected_args)
1461 , text "Actual: " <+> ppr (mkTyConApp fam_tc actual_args) ]
1462
1463 {-
1464 ************************************************************************
1465 * *
1466 Checking type instance well-formedness and termination
1467 * *
1468 ************************************************************************
1469 -}
1470
1471 checkValidCoAxiom :: CoAxiom Branched -> TcM ()
1472 checkValidCoAxiom ax@(CoAxiom { co_ax_tc = fam_tc, co_ax_branches = branches })
1473 = do { mapM_ (checkValidCoAxBranch Nothing fam_tc) branch_list
1474 ; foldlM_ check_branch_compat [] branch_list }
1475 where
1476 branch_list = fromBranches branches
1477 injectivity = familyTyConInjectivityInfo fam_tc
1478
1479 check_branch_compat :: [CoAxBranch] -- previous branches in reverse order
1480 -> CoAxBranch -- current branch
1481 -> TcM [CoAxBranch]-- current branch : previous branches
1482 -- Check for
1483 -- (a) this branch is dominated by previous ones
1484 -- (b) failure of injectivity
1485 check_branch_compat prev_branches cur_branch
1486 | cur_branch `isDominatedBy` prev_branches
1487 = do { addWarnAt NoReason (coAxBranchSpan cur_branch) $
1488 inaccessibleCoAxBranch ax cur_branch
1489 ; return prev_branches }
1490 | otherwise
1491 = do { check_injectivity prev_branches cur_branch
1492 ; return (cur_branch : prev_branches) }
1493
1494 -- Injectivity check: check whether a new (CoAxBranch) can extend
1495 -- already checked equations without violating injectivity
1496 -- annotation supplied by the user.
1497 -- See Note [Verifying injectivity annotation] in FamInstEnv
1498 check_injectivity prev_branches cur_branch
1499 | Injective inj <- injectivity
1500 = do { let conflicts =
1501 fst $ foldl (gather_conflicts inj prev_branches cur_branch)
1502 ([], 0) prev_branches
1503 ; mapM_ (\(err, span) -> setSrcSpan span $ addErr err)
1504 (makeInjectivityErrors ax cur_branch inj conflicts) }
1505 | otherwise
1506 = return ()
1507
1508 gather_conflicts inj prev_branches cur_branch (acc, n) branch
1509 -- n is 0-based index of branch in prev_branches
1510 = case injectiveBranches inj cur_branch branch of
1511 InjectivityUnified ax1 ax2
1512 | ax1 `isDominatedBy` (replace_br prev_branches n ax2)
1513 -> (acc, n + 1)
1514 | otherwise
1515 -> (branch : acc, n + 1)
1516 InjectivityAccepted -> (acc, n + 1)
1517
1518 -- Replace n-th element in the list. Assumes 0-based indexing.
1519 replace_br :: [CoAxBranch] -> Int -> CoAxBranch -> [CoAxBranch]
1520 replace_br brs n br = take n brs ++ [br] ++ drop (n+1) brs
1521
1522
1523 -- Check that a "type instance" is well-formed (which includes decidability
1524 -- unless -XUndecidableInstances is given).
1525 --
1526 checkValidCoAxBranch :: Maybe ClsInfo
1527 -> TyCon -> CoAxBranch -> TcM ()
1528 checkValidCoAxBranch mb_clsinfo fam_tc
1529 (CoAxBranch { cab_tvs = tvs, cab_cvs = cvs
1530 , cab_lhs = typats
1531 , cab_rhs = rhs, cab_loc = loc })
1532 = checkValidTyFamEqn mb_clsinfo fam_tc tvs cvs typats rhs loc
1533
1534 -- | Do validity checks on a type family equation, including consistency
1535 -- with any enclosing class instance head, termination, and lack of
1536 -- polytypes.
1537 checkValidTyFamEqn :: Maybe ClsInfo
1538 -> TyCon -- ^ of the type family
1539 -> [TyVar] -- ^ bound tyvars in the equation
1540 -> [CoVar] -- ^ bound covars in the equation
1541 -> [Type] -- ^ type patterns
1542 -> Type -- ^ rhs
1543 -> SrcSpan
1544 -> TcM ()
1545 checkValidTyFamEqn mb_clsinfo fam_tc tvs cvs typats rhs loc
1546 = setSrcSpan loc $
1547 do { checkValidFamPats mb_clsinfo fam_tc tvs cvs typats
1548
1549 -- The argument patterns, and RHS, are all boxed tau types
1550 -- E.g Reject type family F (a :: k1) :: k2
1551 -- type instance F (forall a. a->a) = ...
1552 -- type instance F Int# = ...
1553 -- type instance F Int = forall a. a->a
1554 -- type instance F Int = Int#
1555 -- See Trac #9357
1556 ; checkValidMonoType rhs
1557 ; check_lifted rhs
1558
1559 -- We have a decidable instance unless otherwise permitted
1560 ; undecidable_ok <- xoptM LangExt.UndecidableInstances
1561 ; unless undecidable_ok $
1562 mapM_ addErrTc (checkFamInstRhs typats (tcTyFamInsts rhs)) }
1563
1564 -- Make sure that each type family application is
1565 -- (1) strictly smaller than the lhs,
1566 -- (2) mentions no type variable more often than the lhs, and
1567 -- (3) does not contain any further type family instances.
1568 --
1569 checkFamInstRhs :: [Type] -- lhs
1570 -> [(TyCon, [Type])] -- type family instances
1571 -> [MsgDoc]
1572 checkFamInstRhs lhsTys famInsts
1573 = mapMaybe check famInsts
1574 where
1575 size = sizeTypes lhsTys
1576 fvs = fvTypes lhsTys
1577 check (tc, tys)
1578 | not (all isTyFamFree tys) = Just (nestedMsg what)
1579 | not (null bad_tvs) = Just (noMoreMsg bad_tvs what)
1580 | size <= sizeTypes tys = Just (smallerMsg what)
1581 | otherwise = Nothing
1582 where
1583 what = text "type family application" <+> quotes (pprType (TyConApp tc tys))
1584 bad_tvs = fvTypes tys \\ fvs
1585
1586 checkValidFamPats :: Maybe ClsInfo -> TyCon -> [TyVar] -> [CoVar] -> [Type] -> TcM ()
1587 -- Patterns in a 'type instance' or 'data instance' decl should
1588 -- a) contain no type family applications
1589 -- (vanilla synonyms are fine, though)
1590 -- b) properly bind all their free type variables
1591 -- e.g. we disallow (Trac #7536)
1592 -- type T a = Int
1593 -- type instance F (T a) = a
1594 -- c) Have the right number of patterns
1595 -- d) For associated types, are consistently instantiated
1596 checkValidFamPats mb_clsinfo fam_tc tvs cvs ty_pats
1597 = do { -- A family instance must have exactly the same number of type
1598 -- parameters as the family declaration. You can't write
1599 -- type family F a :: * -> *
1600 -- type instance F Int y = y
1601 -- because then the type (F Int) would be like (\y.y)
1602 checkTc (length ty_pats == fam_arity) $
1603 wrongNumberOfParmsErr (fam_arity - count isInvisibleBinder fam_bndrs)
1604 -- report only explicit arguments
1605
1606 ; mapM_ checkValidTypePat ty_pats
1607
1608 ; let unbound_tcvs = filterOut (`elemVarSet` exactTyCoVarsOfTypes ty_pats) (tvs ++ cvs)
1609 ; checkTc (null unbound_tcvs) (famPatErr fam_tc unbound_tcvs ty_pats)
1610
1611 -- Check that type patterns match the class instance head
1612 ; checkConsistentFamInst mb_clsinfo fam_tc tvs ty_pats }
1613 where
1614 fam_arity = tyConArity fam_tc
1615 fam_bndrs = tyConBinders fam_tc
1616
1617
1618 checkValidTypePat :: Type -> TcM ()
1619 -- Used for type patterns in class instances,
1620 -- and in type/data family instances
1621 checkValidTypePat pat_ty
1622 = do { -- Check that pat_ty is a monotype
1623 checkValidMonoType pat_ty
1624 -- One could imagine generalising to allow
1625 -- instance C (forall a. a->a)
1626 -- but we don't know what all the consequences might be
1627
1628 -- Ensure that no type family instances occur a type pattern
1629 ; checkTc (isTyFamFree pat_ty) $
1630 tyFamInstIllegalErr pat_ty
1631
1632 ; check_lifted pat_ty }
1633
1634 isTyFamFree :: Type -> Bool
1635 -- ^ Check that a type does not contain any type family applications.
1636 isTyFamFree = null . tcTyFamInsts
1637
1638 -- Error messages
1639
1640 wrongNumberOfParmsErr :: Arity -> SDoc
1641 wrongNumberOfParmsErr exp_arity
1642 = text "Number of parameters must match family declaration; expected"
1643 <+> ppr exp_arity
1644
1645 inaccessibleCoAxBranch :: CoAxiom br -> CoAxBranch -> SDoc
1646 inaccessibleCoAxBranch fi_ax cur_branch
1647 = text "Type family instance equation is overlapped:" $$
1648 nest 2 (pprCoAxBranch fi_ax cur_branch)
1649
1650 tyFamInstIllegalErr :: Type -> SDoc
1651 tyFamInstIllegalErr ty
1652 = hang (text "Illegal type synonym family application in instance" <>
1653 colon) 2 $
1654 ppr ty
1655
1656 nestedMsg :: SDoc -> SDoc
1657 nestedMsg what
1658 = sep [ text "Illegal nested" <+> what
1659 , parens undecidableMsg ]
1660
1661 famPatErr :: TyCon -> [TyVar] -> [Type] -> SDoc
1662 famPatErr fam_tc tvs pats
1663 = hang (text "Family instance purports to bind type variable" <> plural tvs
1664 <+> pprQuotedList tvs)
1665 2 (hang (text "but the real LHS (expanding synonyms) is:")
1666 2 (pprTypeApp fam_tc (map expandTypeSynonyms pats) <+>
1667 text "= ..."))
1668
1669 {-
1670 ************************************************************************
1671 * *
1672 Telescope checking
1673 * *
1674 ************************************************************************
1675
1676 Note [Bad telescopes]
1677 ~~~~~~~~~~~~~~~~~~~~~
1678 Now that we can mix type and kind variables, there are an awful lot of
1679 ways to shoot yourself in the foot. Here are some.
1680
1681 data SameKind :: k -> k -> * -- just to force unification
1682
1683 1. data T1 a k (b :: k) (x :: SameKind a b)
1684
1685 The problem here is that we discover that a and b should have the same
1686 kind. But this kind mentions k, which is bound *after* a.
1687 (Testcase: dependent/should_fail/BadTelescope)
1688
1689 2. data T2 a (c :: Proxy b) (d :: Proxy a) (x :: SameKind b d)
1690
1691 Note that b is not bound. Yet its kind mentions a. Because we have
1692 a nice rule that all implicitly bound variables come before others,
1693 this is bogus. (We could probably figure out to put b between a and c.
1694 But I think this is doing users a disservice, in the long run.)
1695 (Testcase: dependent/should_fail/BadTelescope4)
1696
1697 3. t3 :: forall a. (forall k (b :: k). SameKind a b) -> ()
1698
1699 This is a straightforward skolem escape. Note that a and b need to have
1700 the same kind.
1701 (Testcase: polykinds/T11142)
1702
1703 How do we deal with all of this? For TyCons, we have checkValidTyConTyVars.
1704 That function looks to see if any of the tyConTyVars are repeated, but
1705 it's really a telescope check. It works because all tycons are kind-generalized.
1706 If there is a bad telescope, the kind-generalization will end up generalizing
1707 over a variable bound later in the telescope.
1708
1709 For non-tycons, we do scope checking when we bring tyvars into scope,
1710 in tcImplicitTKBndrs and tcExplicitTKBndrs. Note that we also have to
1711 sort implicit binders into a well-scoped order whenever we have implicit
1712 binders to worry about. This is done in quantifyTyVars and in
1713 tcImplicitTKBndrs.
1714 -}
1715
1716 -- | Check a list of binders to see if they make a valid telescope.
1717 -- The key property we're checking for is scoping. For example:
1718 -- > data SameKind :: k -> k -> *
1719 -- > data X a k (b :: k) (c :: SameKind a b)
1720 -- Kind inference says that a's kind should be k. But that's impossible,
1721 -- because k isn't in scope when a is bound. This check has to come before
1722 -- general validity checking, because once we kind-generalise, this sort
1723 -- of problem is harder to spot (as we'll generalise over the unbound
1724 -- k in a's type.) See also Note [Bad telescopes].
1725 checkValidTelescope :: SDoc -- the original user-written telescope
1726 -> [TyVar] -- explicit vars (not necessarily zonked)
1727 -> SDoc -- note to put at bottom of message
1728 -> TcM ()
1729 checkValidTelescope hs_tvs orig_tvs extra
1730 = discardResult $ checkZonkValidTelescope hs_tvs orig_tvs extra
1731
1732 -- | Like 'checkZonkValidTelescope', but returns the zonked tyvars
1733 checkZonkValidTelescope :: SDoc
1734 -> [TyVar]
1735 -> SDoc
1736 -> TcM [TyVar]
1737 checkZonkValidTelescope hs_tvs orig_tvs extra
1738 = do { orig_tvs <- mapM zonkTyCoVarKind orig_tvs
1739 ; let (_, sorted_tidied_tvs) = tidyTyCoVarBndrs emptyTidyEnv $
1740 toposortTyVars orig_tvs
1741 ; unless (go [] emptyVarSet orig_tvs) $
1742 addErr $
1743 vcat [ hang (text "These kind and type variables:" <+> hs_tvs $$
1744 text "are out of dependency order. Perhaps try this ordering:")
1745 2 (sep (map pprTvBndr sorted_tidied_tvs))
1746 , extra ]
1747 ; return orig_tvs }
1748
1749 where
1750 go :: [TyVar] -- misplaced variables
1751 -> TyVarSet -> [TyVar] -> Bool
1752 go errs in_scope [] = null (filter (`elemVarSet` in_scope) errs)
1753 -- report an error only when the variable in the kind is brought
1754 -- into scope later in the telescope. Otherwise, we'll just quantify
1755 -- over it in kindGeneralize, as we should.
1756
1757 go errs in_scope (tv:tvs)
1758 = let bad_tvs = tyCoVarsOfType (tyVarKind tv) `minusVarSet` in_scope in
1759 go (varSetElems bad_tvs ++ errs) (in_scope `extendVarSet` tv) tvs
1760
1761 -- | After inferring kinds of type variables, check to make sure that the
1762 -- inferred kinds any of the type variables bound in a smaller scope.
1763 -- This is a skolem escape check. See also Note [Bad telescopes].
1764 checkValidInferredKinds :: [TyVar] -- ^ vars to check (zonked)
1765 -> TyVarSet -- ^ vars out of scope
1766 -> SDoc -- ^ suffix to error message
1767 -> TcM ()
1768 checkValidInferredKinds orig_kvs out_of_scope extra
1769 = do { let bad_pairs = [ (tv, kv)
1770 | kv <- orig_kvs
1771 , Just tv <- map (lookupVarSet out_of_scope)
1772 (tyCoVarsOfTypeList (tyVarKind kv)) ]
1773 report (tidyTyVarOcc env -> tv, tidyTyVarOcc env -> kv)
1774 = addErr $
1775 text "The kind of variable" <+>
1776 quotes (ppr kv) <> text ", namely" <+>
1777 quotes (ppr (tyVarKind kv)) <> comma $$
1778 text "depends on variable" <+>
1779 quotes (ppr tv) <+> text "from an inner scope" $$
1780 text "Perhaps bind" <+> quotes (ppr kv) <+>
1781 text "sometime after binding" <+>
1782 quotes (ppr tv) $$
1783 extra
1784 ; mapM_ report bad_pairs }
1785
1786 where
1787 (env1, _) = tidyTyCoVarBndrs emptyTidyEnv orig_kvs
1788 (env, _) = tidyTyCoVarBndrs env1 (varSetElems out_of_scope)
1789
1790 {-
1791 ************************************************************************
1792 * *
1793 \subsection{Auxiliary functions}
1794 * *
1795 ************************************************************************
1796 -}
1797
1798 -- Free variables of a type, retaining repetitions, and expanding synonyms
1799 fvType :: Type -> [TyCoVar]
1800 fvType ty | Just exp_ty <- coreView ty = fvType exp_ty
1801 fvType (TyVarTy tv) = [tv]
1802 fvType (TyConApp _ tys) = fvTypes tys
1803 fvType (LitTy {}) = []
1804 fvType (AppTy fun arg) = fvType fun ++ fvType arg
1805 fvType (ForAllTy bndr ty)
1806 = fvType (binderType bndr) ++
1807 caseBinder bndr (\tv -> filter (/= tv)) (const id) (fvType ty)
1808 fvType (CastTy ty co) = fvType ty ++ fvCo co
1809 fvType (CoercionTy co) = fvCo co
1810
1811 fvTypes :: [Type] -> [TyVar]
1812 fvTypes tys = concat (map fvType tys)
1813
1814 fvCo :: Coercion -> [TyCoVar]
1815 fvCo (Refl _ ty) = fvType ty
1816 fvCo (TyConAppCo _ _ args) = concatMap fvCo args
1817 fvCo (AppCo co arg) = fvCo co ++ fvCo arg
1818 fvCo (ForAllCo tv h co) = filter (/= tv) (fvCo co) ++ fvCo h
1819 fvCo (CoVarCo v) = [v]
1820 fvCo (AxiomInstCo _ _ args) = concatMap fvCo args
1821 fvCo (UnivCo p _ t1 t2) = fvProv p ++ fvType t1 ++ fvType t2
1822 fvCo (SymCo co) = fvCo co
1823 fvCo (TransCo co1 co2) = fvCo co1 ++ fvCo co2
1824 fvCo (NthCo _ co) = fvCo co
1825 fvCo (LRCo _ co) = fvCo co
1826 fvCo (InstCo co arg) = fvCo co ++ fvCo arg
1827 fvCo (CoherenceCo co1 co2) = fvCo co1 ++ fvCo co2
1828 fvCo (KindCo co) = fvCo co
1829 fvCo (SubCo co) = fvCo co
1830 fvCo (AxiomRuleCo _ cs) = concatMap fvCo cs
1831
1832 fvProv :: UnivCoProvenance -> [TyCoVar]
1833 fvProv UnsafeCoerceProv = []
1834 fvProv (PhantomProv co) = fvCo co
1835 fvProv (ProofIrrelProv co) = fvCo co
1836 fvProv (PluginProv _) = []
1837 fvProv (HoleProv h) = pprPanic "fvProv falls into a hole" (ppr h)
1838
1839 sizeType :: Type -> Int
1840 -- Size of a type: the number of variables and constructors
1841 sizeType ty | Just exp_ty <- coreView ty = sizeType exp_ty
1842 sizeType (TyVarTy {}) = 1
1843 sizeType (TyConApp _ tys) = sizeTypes tys + 1
1844 sizeType (LitTy {}) = 1
1845 sizeType (AppTy fun arg) = sizeType fun + sizeType arg
1846 sizeType (ForAllTy (Anon arg) res)
1847 = sizeType arg + sizeType res + 1
1848 sizeType (ForAllTy (Named {}) ty)
1849 = sizeType ty
1850 sizeType (CastTy ty _) = sizeType ty
1851 sizeType (CoercionTy _) = 1
1852
1853 sizeTypes :: [Type] -> Int
1854 sizeTypes = sum . map sizeType
1855
1856 -- Size of a predicate
1857 --
1858 -- We are considering whether class constraints terminate.
1859 -- Equality constraints and constraints for the implicit
1860 -- parameter class always termiante so it is safe to say "size 0".
1861 -- (Implicit parameter constraints always terminate because
1862 -- there are no instances for them---they are only solved by
1863 -- "local instances" in expressions).
1864 -- See Trac #4200.
1865 sizePred :: PredType -> Int
1866 sizePred ty = goClass ty
1867 where
1868 goClass p = go (classifyPredType p)
1869
1870 go (ClassPred cls tys')
1871 | isTerminatingClass cls = 0
1872 | otherwise = sizeTypes tys'
1873 go (EqPred {}) = 0
1874 go (IrredPred ty) = sizeType ty
1875
1876 -- | When this says "True", ignore this class constraint during
1877 -- a termination check
1878 isTerminatingClass :: Class -> Bool
1879 isTerminatingClass cls
1880 = isIPClass cls
1881 || cls `hasKey` typeableClassKey
1882 || cls `hasKey` coercibleTyConKey
1883 || cls `hasKey` eqTyConKey
1884 || cls `hasKey` heqTyConKey
1885
1886 -- | Tidy before printing a type
1887 ppr_tidy :: TidyEnv -> Type -> SDoc
1888 ppr_tidy env ty = pprType (tidyType env ty)