Dead code removal, export cleanup
[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 #-}
7
8 module TcValidity (
9 Rank, UserTypeCtxt(..), checkValidType, checkValidMonoType,
10 expectedKindInCtxt,
11 checkValidTheta, checkValidFamPats,
12 checkValidInstance, validDerivPred,
13 checkInstTermination,
14 checkValidCoAxiom, checkValidCoAxBranch,
15 checkConsistentFamInst,
16 arityErr, badATErr
17 ) where
18
19 #include "HsVersions.h"
20
21 -- friends:
22 import TcUnify ( tcSubType_NC )
23 import TcSimplify ( simplifyAmbiguityCheck )
24 import TypeRep
25 import TcType
26 import TcMType
27 import TysWiredIn ( coercibleClass, eqTyCon )
28 import PrelNames
29 import Type
30 import Unify( tcMatchTyX )
31 import Kind
32 import CoAxiom
33 import Class
34 import TyCon
35
36 -- others:
37 import HsSyn -- HsType
38 import TcRnMonad -- TcType, amongst others
39 import FunDeps
40 import FamInstEnv ( isDominatedBy, injectiveBranches,
41 InjectivityCheckResult(..) )
42 import FamInst ( makeInjectivityErrors )
43 import Name
44 import VarEnv
45 import VarSet
46 import ErrUtils
47 import DynFlags
48 import Util
49 import ListSetOps
50 import SrcLoc
51 import Outputable
52 import FastString
53
54 import Control.Monad
55 import Data.Maybe
56 import Data.List ( (\\) )
57
58 {-
59 ************************************************************************
60 * *
61 Checking for ambiguity
62 * *
63 ************************************************************************
64
65 Note [The ambiguity check for type signatures]
66 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
67 checkAmbiguity is a check on *user-supplied type signatures*. It is
68 *purely* there to report functions that cannot possibly be called. So for
69 example we want to reject:
70 f :: C a => Int
71 The idea is there can be no legal calls to 'f' because every call will
72 give rise to an ambiguous constraint. We could soundly omit the
73 ambiguity check on type signatures entirely, at the expense of
74 delaying ambiguity errors to call sites. Indeed, the flag
75 -XAllowAmbiguousTypes switches off the ambiguity check.
76
77 What about things like this:
78 class D a b | a -> b where ..
79 h :: D Int b => Int
80 The Int may well fix 'b' at the call site, so that signature should
81 not be rejected. Moreover, using *visible* fundeps is too
82 conservative. Consider
83 class X a b where ...
84 class D a b | a -> b where ...
85 instance D a b => X [a] b where...
86 h :: X a b => a -> a
87 Here h's type looks ambiguous in 'b', but here's a legal call:
88 ...(h [True])...
89 That gives rise to a (X [Bool] beta) constraint, and using the
90 instance means we need (D Bool beta) and that fixes 'beta' via D's
91 fundep!
92
93 Behind all these special cases there is a simple guiding principle.
94 Consider
95
96 f :: <type>
97 f = ...blah...
98
99 g :: <type>
100 g = f
101
102 You would think that the definition of g would surely typecheck!
103 After all f has exactly the same type, and g=f. But in fact f's type
104 is instantiated and the instantiated constraints are solved against
105 the originals, so in the case an ambiguous type it won't work.
106 Consider our earlier example f :: C a => Int. Then in g's definition,
107 we'll instantiate to (C alpha) and try to deduce (C alpha) from (C a),
108 and fail.
109
110 So in fact we use this as our *definition* of ambiguity. We use a
111 very similar test for *inferred* types, to ensure that they are
112 unambiguous. See Note [Impedence matching] in TcBinds.
113
114 This test is very conveniently implemented by calling
115 tcSubType <type> <type>
116 This neatly takes account of the functional dependecy stuff above,
117 and implicit parameter (see Note [Implicit parameters and ambiguity]).
118 And this is what checkAmbiguity does.
119
120 What about this, though?
121 g :: C [a] => Int
122 Is every call to 'g' ambiguous? After all, we might have
123 intance C [a] where ...
124 at the call site. So maybe that type is ok! Indeed even f's
125 quintessentially ambiguous type might, just possibly be callable:
126 with -XFlexibleInstances we could have
127 instance C a where ...
128 and now a call could be legal after all! Well, we'll reject this
129 unless the instance is available *here*.
130
131 Note [When to call checkAmbiguity]
132 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
133 We call checkAmbiguity
134 (a) on user-specified type signatures
135 (b) in checkValidType
136
137 Conncerning (b), you might wonder about nested foralls. What about
138 f :: forall b. (forall a. Eq a => b) -> b
139 The nested forall is ambiguous. Originally we called checkAmbiguity
140 in the forall case of check_type, but that had two bad consequences:
141 * We got two error messages about (Eq b) in a nested forall like this:
142 g :: forall a. Eq a => forall b. Eq b => a -> a
143 * If we try to check for ambiguity of an nested forall like
144 (forall a. Eq a => b), the implication constraint doesn't bind
145 all the skolems, which results in "No skolem info" in error
146 messages (see Trac #10432).
147
148 To avoid this, we call checkAmbiguity once, at the top, in checkValidType.
149 (I'm still a bit worried about unbound skolems when the type mentions
150 in-scope type variables.)
151
152 In fact, because of the co/contra-variance implemented in tcSubType,
153 this *does* catch function f above. too.
154
155 Concerning (a) the ambiguity check is only used for *user* types, not
156 for types coming from inteface files. The latter can legitimately
157 have ambiguous types. Example
158
159 class S a where s :: a -> (Int,Int)
160 instance S Char where s _ = (1,1)
161 f:: S a => [a] -> Int -> (Int,Int)
162 f (_::[a]) x = (a*x,b)
163 where (a,b) = s (undefined::a)
164
165 Here the worker for f gets the type
166 fw :: forall a. S a => Int -> (# Int, Int #)
167
168
169 Note [Implicit parameters and ambiguity]
170 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
171 Only a *class* predicate can give rise to ambiguity
172 An *implicit parameter* cannot. For example:
173 foo :: (?x :: [a]) => Int
174 foo = length ?x
175 is fine. The call site will supply a particular 'x'
176
177 Furthermore, the type variables fixed by an implicit parameter
178 propagate to the others. E.g.
179 foo :: (Show a, ?x::[a]) => Int
180 foo = show (?x++?x)
181 The type of foo looks ambiguous. But it isn't, because at a call site
182 we might have
183 let ?x = 5::Int in foo
184 and all is well. In effect, implicit parameters are, well, parameters,
185 so we can take their type variables into account as part of the
186 "tau-tvs" stuff. This is done in the function 'FunDeps.grow'.
187 -}
188
189 checkAmbiguity :: UserTypeCtxt -> Type -> TcM ()
190 checkAmbiguity ctxt ty
191 | GhciCtxt <- ctxt -- Allow ambiguous types in GHCi's :kind command
192 = return () -- E.g. type family T a :: * -- T :: forall k. k -> *
193 -- Then :k T should work in GHCi, not complain that
194 -- (T k) is ambiguous!
195
196 | InfSigCtxt {} <- ctxt -- See Note [Validity of inferred types] in TcBinds
197 = return ()
198
199 | otherwise
200 = do { traceTc "Ambiguity check for" (ppr ty)
201 ; let free_tkvs = varSetElemsKvsFirst (closeOverKinds (tyVarsOfType ty))
202 ; (subst, _tvs) <- tcInstSkolTyVars free_tkvs
203 ; let ty' = substTy subst ty
204 -- The type might have free TyVars, esp when the ambiguity check
205 -- happens during a call to checkValidType,
206 -- so we skolemise them as TcTyVars.
207 -- Tiresome; but the type inference engine expects TcTyVars
208 -- NB: The free tyvar might be (a::k), so k is also free
209 -- and we must skolemise it as well. Hence closeOverKinds.
210 -- (Trac #9222)
211
212 -- Solve the constraints eagerly because an ambiguous type
213 -- can cause a cascade of further errors. Since the free
214 -- tyvars are skolemised, we can safely use tcSimplifyTop
215 ; (_wrap, wanted) <- addErrCtxtM (mk_msg ty') $
216 captureConstraints $
217 tcSubType_NC ctxt ty' ty'
218 ; simplifyAmbiguityCheck ty wanted
219
220 ; traceTc "Done ambiguity check for" (ppr ty) }
221 where
222 mk_msg ty tidy_env
223 = do { allow_ambiguous <- xoptM Opt_AllowAmbiguousTypes
224 ; (tidy_env', tidy_ty) <- zonkTidyTcType tidy_env ty
225 ; return (tidy_env', mk_msg tidy_ty $$ ppWhen (not allow_ambiguous) ambig_msg) }
226 where
227 mk_msg ty = pprSigCtxt ctxt (ptext (sLit "the ambiguity check for")) (ppr ty)
228 ambig_msg = ptext (sLit "To defer the ambiguity check to use sites, enable AllowAmbiguousTypes")
229
230 {-
231 ************************************************************************
232 * *
233 Checking validity of a user-defined type
234 * *
235 ************************************************************************
236
237 When dealing with a user-written type, we first translate it from an HsType
238 to a Type, performing kind checking, and then check various things that should
239 be true about it. We don't want to perform these checks at the same time
240 as the initial translation because (a) they are unnecessary for interface-file
241 types and (b) when checking a mutually recursive group of type and class decls,
242 we can't "look" at the tycons/classes yet. Also, the checks are rather
243 diverse, and used to really mess up the other code.
244
245 One thing we check for is 'rank'.
246
247 Rank 0: monotypes (no foralls)
248 Rank 1: foralls at the front only, Rank 0 inside
249 Rank 2: foralls at the front, Rank 1 on left of fn arrow,
250
251 basic ::= tyvar | T basic ... basic
252
253 r2 ::= forall tvs. cxt => r2a
254 r2a ::= r1 -> r2a | basic
255 r1 ::= forall tvs. cxt => r0
256 r0 ::= r0 -> r0 | basic
257
258 Another thing is to check that type synonyms are saturated.
259 This might not necessarily show up in kind checking.
260 type A i = i
261 data T k = MkT (k Int)
262 f :: T A -- BAD!
263 -}
264
265 checkValidType :: UserTypeCtxt -> Type -> TcM ()
266 -- Checks that the type is valid for the given context
267 -- Not used for instance decls; checkValidInstance instead
268 checkValidType ctxt ty
269 = do { traceTc "checkValidType" (ppr ty <+> text "::" <+> ppr (typeKind ty))
270 ; rankn_flag <- xoptM Opt_RankNTypes
271 ; let gen_rank :: Rank -> Rank
272 gen_rank r | rankn_flag = ArbitraryRank
273 | otherwise = r
274
275 rank1 = gen_rank r1
276 rank0 = gen_rank r0
277
278 r0 = rankZeroMonoType
279 r1 = LimitedRank True r0
280
281 rank
282 = case ctxt of
283 DefaultDeclCtxt-> MustBeMonoType
284 ResSigCtxt -> MustBeMonoType
285 PatSigCtxt -> rank0
286 RuleSigCtxt _ -> rank1
287 TySynCtxt _ -> rank0
288
289 ExprSigCtxt -> rank1
290 FunSigCtxt {} -> rank1
291 InfSigCtxt _ -> ArbitraryRank -- Inferred type
292 ConArgCtxt _ -> rank1 -- We are given the type of the entire
293 -- constructor, hence rank 1
294
295 ForSigCtxt _ -> rank1
296 SpecInstCtxt -> rank1
297 ThBrackCtxt -> rank1
298 GhciCtxt -> ArbitraryRank
299 _ -> panic "checkValidType"
300 -- Can't happen; not used for *user* sigs
301
302 -- Check the internal validity of the type itself
303 ; check_type ctxt rank ty
304
305 -- Check that the thing has kind Type, and is lifted if necessary.
306 -- Do this *after* check_type, because we can't usefully take
307 -- the kind of an ill-formed type such as (a~Int)
308 ; check_kind ctxt ty
309
310 -- Check for ambiguous types. See Note [When to call checkAmbiguity]
311 -- NB: this will happen even for monotypes, but that should be cheap;
312 -- and there may be nested foralls for the subtype test to examine
313 ; checkAmbiguity ctxt ty
314
315 ; traceTc "checkValidType done" (ppr ty <+> text "::" <+> ppr (typeKind ty)) }
316
317 checkValidMonoType :: Type -> TcM ()
318 checkValidMonoType ty = check_mono_type SigmaCtxt MustBeMonoType ty
319
320
321 check_kind :: UserTypeCtxt -> TcType -> TcM ()
322 -- Check that the type's kind is acceptable for the context
323 check_kind ctxt ty
324 | TySynCtxt {} <- ctxt
325 , returnsConstraintKind actual_kind
326 = do { ck <- xoptM Opt_ConstraintKinds
327 ; if ck
328 then when (isConstraintKind actual_kind)
329 (do { dflags <- getDynFlags
330 ; check_pred_ty dflags ctxt ty })
331 else addErrTc (constraintSynErr actual_kind) }
332
333 | Just k <- expectedKindInCtxt ctxt
334 = checkTc (tcIsSubKind actual_kind k) (kindErr actual_kind)
335
336 | otherwise
337 = return () -- Any kind will do
338 where
339 actual_kind = typeKind ty
340
341 -- Depending on the context, we might accept any kind (for instance, in a TH
342 -- splice), or only certain kinds (like in type signatures).
343 expectedKindInCtxt :: UserTypeCtxt -> Maybe Kind
344 expectedKindInCtxt (TySynCtxt _) = Nothing -- Any kind will do
345 expectedKindInCtxt ThBrackCtxt = Nothing
346 expectedKindInCtxt GhciCtxt = Nothing
347 expectedKindInCtxt (ForSigCtxt _) = Just liftedTypeKind
348 expectedKindInCtxt InstDeclCtxt = Just constraintKind
349 expectedKindInCtxt SpecInstCtxt = Just constraintKind
350 expectedKindInCtxt _ = Just openTypeKind
351
352 {-
353 Note [Higher rank types]
354 ~~~~~~~~~~~~~~~~~~~~~~~~
355 Technically
356 Int -> forall a. a->a
357 is still a rank-1 type, but it's not Haskell 98 (Trac #5957). So the
358 validity checker allow a forall after an arrow only if we allow it
359 before -- that is, with Rank2Types or RankNTypes
360 -}
361
362 data Rank = ArbitraryRank -- Any rank ok
363
364 | LimitedRank -- Note [Higher rank types]
365 Bool -- Forall ok at top
366 Rank -- Use for function arguments
367
368 | MonoType SDoc -- Monotype, with a suggestion of how it could be a polytype
369
370 | MustBeMonoType -- Monotype regardless of flags
371
372 rankZeroMonoType, tyConArgMonoType, synArgMonoType :: Rank
373 rankZeroMonoType = MonoType (ptext (sLit "Perhaps you intended to use RankNTypes or Rank2Types"))
374 tyConArgMonoType = MonoType (ptext (sLit "GHC doesn't yet support impredicative polymorphism"))
375 synArgMonoType = MonoType (ptext (sLit "Perhaps you intended to use LiberalTypeSynonyms"))
376
377 funArgResRank :: Rank -> (Rank, Rank) -- Function argument and result
378 funArgResRank (LimitedRank _ arg_rank) = (arg_rank, LimitedRank (forAllAllowed arg_rank) arg_rank)
379 funArgResRank other_rank = (other_rank, other_rank)
380
381 forAllAllowed :: Rank -> Bool
382 forAllAllowed ArbitraryRank = True
383 forAllAllowed (LimitedRank forall_ok _) = forall_ok
384 forAllAllowed _ = False
385
386 ----------------------------------------
387 check_mono_type :: UserTypeCtxt -> Rank
388 -> KindOrType -> TcM () -- No foralls anywhere
389 -- No unlifted types of any kind
390 check_mono_type ctxt rank ty
391 | isKind ty = return () -- IA0_NOTE: Do we need to check kinds?
392 | otherwise
393 = do { check_type ctxt rank ty
394 ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
395
396 check_type :: UserTypeCtxt -> Rank -> Type -> TcM ()
397 -- The args say what the *type context* requires, independent
398 -- of *flag* settings. You test the flag settings at usage sites.
399 --
400 -- Rank is allowed rank for function args
401 -- Rank 0 means no for-alls anywhere
402
403 check_type ctxt rank ty
404 | not (null tvs && null theta)
405 = do { checkTc (forAllAllowed rank) (forAllTyErr rank ty)
406 -- Reject e.g. (Maybe (?x::Int => Int)),
407 -- with a decent error message
408
409 ; check_valid_theta SigmaCtxt theta
410 -- Allow type T = ?x::Int => Int -> Int
411 -- but not type T = ?x::Int
412
413 ; check_type ctxt rank tau } -- Allow foralls to right of arrow
414 where
415 (tvs, theta, tau) = tcSplitSigmaTy ty
416
417 check_type _ _ (TyVarTy _) = return ()
418
419 check_type ctxt rank (FunTy arg_ty res_ty)
420 = do { check_type ctxt arg_rank arg_ty
421 ; check_type ctxt res_rank res_ty }
422 where
423 (arg_rank, res_rank) = funArgResRank rank
424
425 check_type ctxt rank (AppTy ty1 ty2)
426 = do { check_arg_type ctxt rank ty1
427 ; check_arg_type ctxt rank ty2 }
428
429 check_type ctxt rank ty@(TyConApp tc tys)
430 | isTypeSynonymTyCon tc || isTypeFamilyTyCon tc
431 = check_syn_tc_app ctxt rank ty tc tys
432 | isUnboxedTupleTyCon tc = check_ubx_tuple ctxt ty tys
433 | otherwise = mapM_ (check_arg_type ctxt rank) tys
434
435 check_type _ _ (LitTy {}) = return ()
436
437 check_type _ _ ty = pprPanic "check_type" (ppr ty)
438
439 ----------------------------------------
440 check_syn_tc_app :: UserTypeCtxt -> Rank -> KindOrType
441 -> TyCon -> [KindOrType] -> TcM ()
442 -- Used for type synonyms and type synonym families,
443 -- which must be saturated,
444 -- but not data families, which need not be saturated
445 check_syn_tc_app ctxt rank ty tc tys
446 | tc_arity <= length tys -- Saturated
447 -- Check that the synonym has enough args
448 -- This applies equally to open and closed synonyms
449 -- It's OK to have an *over-applied* type synonym
450 -- data Tree a b = ...
451 -- type Foo a = Tree [a]
452 -- f :: Foo a b -> ...
453 = do { -- See Note [Liberal type synonyms]
454 ; liberal <- xoptM Opt_LiberalTypeSynonyms
455 ; if not liberal || isTypeFamilyTyCon tc then
456 -- For H98 and synonym families, do check the type args
457 mapM_ check_arg tys
458
459 else -- In the liberal case (only for closed syns), expand then check
460 case tcView ty of
461 Just ty' -> check_type ctxt rank ty'
462 Nothing -> pprPanic "check_tau_type" (ppr ty) }
463
464 | GhciCtxt <- ctxt -- Accept under-saturated type synonyms in
465 -- GHCi :kind commands; see Trac #7586
466 = mapM_ check_arg tys
467
468 | otherwise
469 = failWithTc (tyConArityErr tc tys)
470 where
471 tc_arity = tyConArity tc
472 check_arg | isTypeFamilyTyCon tc = check_arg_type ctxt rank
473 | otherwise = check_mono_type ctxt synArgMonoType
474
475 ----------------------------------------
476 check_ubx_tuple :: UserTypeCtxt -> KindOrType
477 -> [KindOrType] -> TcM ()
478 check_ubx_tuple ctxt ty tys
479 = do { ub_tuples_allowed <- xoptM Opt_UnboxedTuples
480 ; checkTc ub_tuples_allowed (ubxArgTyErr ty)
481
482 ; impred <- xoptM Opt_ImpredicativeTypes
483 ; let rank' = if impred then ArbitraryRank else tyConArgMonoType
484 -- c.f. check_arg_type
485 -- However, args are allowed to be unlifted, or
486 -- more unboxed tuples, so can't use check_arg_ty
487 ; mapM_ (check_type ctxt rank') tys }
488
489 ----------------------------------------
490 check_arg_type :: UserTypeCtxt -> Rank -> KindOrType -> TcM ()
491 -- The sort of type that can instantiate a type variable,
492 -- or be the argument of a type constructor.
493 -- Not an unboxed tuple, but now *can* be a forall (since impredicativity)
494 -- Other unboxed types are very occasionally allowed as type
495 -- arguments depending on the kind of the type constructor
496 --
497 -- For example, we want to reject things like:
498 --
499 -- instance Ord a => Ord (forall s. T s a)
500 -- and
501 -- g :: T s (forall b.b)
502 --
503 -- NB: unboxed tuples can have polymorphic or unboxed args.
504 -- This happens in the workers for functions returning
505 -- product types with polymorphic components.
506 -- But not in user code.
507 -- Anyway, they are dealt with by a special case in check_tau_type
508
509 check_arg_type ctxt rank ty
510 | isKind ty = return () -- IA0_NOTE: Do we need to check a kind?
511 | otherwise
512 = do { impred <- xoptM Opt_ImpredicativeTypes
513 ; let rank' = case rank of -- Predictive => must be monotype
514 MustBeMonoType -> MustBeMonoType -- Monotype, regardless
515 _other | impred -> ArbitraryRank
516 | otherwise -> tyConArgMonoType
517 -- Make sure that MustBeMonoType is propagated,
518 -- so that we don't suggest -XImpredicativeTypes in
519 -- (Ord (forall a.a)) => a -> a
520 -- and so that if it Must be a monotype, we check that it is!
521
522 ; check_type ctxt rank' ty
523 ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
524 -- NB the isUnLiftedType test also checks for
525 -- T State#
526 -- where there is an illegal partial application of State# (which has
527 -- kind * -> #); see Note [The kind invariant] in TypeRep
528
529 ----------------------------------------
530 forAllTyErr :: Rank -> Type -> SDoc
531 forAllTyErr rank ty
532 = vcat [ hang (ptext (sLit "Illegal polymorphic or qualified type:")) 2 (ppr ty)
533 , suggestion ]
534 where
535 suggestion = case rank of
536 LimitedRank {} -> ptext (sLit "Perhaps you intended to use RankNTypes or Rank2Types")
537 MonoType d -> d
538 _ -> Outputable.empty -- Polytype is always illegal
539
540 unliftedArgErr, ubxArgTyErr :: Type -> SDoc
541 unliftedArgErr ty = sep [ptext (sLit "Illegal unlifted type:"), ppr ty]
542 ubxArgTyErr ty = sep [ptext (sLit "Illegal unboxed tuple type as function argument:"), ppr ty]
543
544 kindErr :: Kind -> SDoc
545 kindErr kind = sep [ptext (sLit "Expecting an ordinary type, but found a type of kind"), ppr kind]
546
547 {-
548 Note [Liberal type synonyms]
549 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
550 If -XLiberalTypeSynonyms is on, expand closed type synonyms *before*
551 doing validity checking. This allows us to instantiate a synonym defn
552 with a for-all type, or with a partially-applied type synonym.
553 e.g. type T a b = a
554 type S m = m ()
555 f :: S (T Int)
556 Here, T is partially applied, so it's illegal in H98. But if you
557 expand S first, then T we get just
558 f :: Int
559 which is fine.
560
561 IMPORTANT: suppose T is a type synonym. Then we must do validity
562 checking on an appliation (T ty1 ty2)
563
564 *either* before expansion (i.e. check ty1, ty2)
565 *or* after expansion (i.e. expand T ty1 ty2, and then check)
566 BUT NOT BOTH
567
568 If we do both, we get exponential behaviour!!
569
570 data TIACons1 i r c = c i ::: r c
571 type TIACons2 t x = TIACons1 t (TIACons1 t x)
572 type TIACons3 t x = TIACons2 t (TIACons1 t x)
573 type TIACons4 t x = TIACons2 t (TIACons2 t x)
574 type TIACons7 t x = TIACons4 t (TIACons3 t x)
575
576
577 ************************************************************************
578 * *
579 \subsection{Checking a theta or source type}
580 * *
581 ************************************************************************
582
583 Note [Implicit parameters in instance decls]
584 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
585 Implicit parameters _only_ allowed in type signatures; not in instance
586 decls, superclasses etc. The reason for not allowing implicit params in
587 instances is a bit subtle. If we allowed
588 instance (?x::Int, Eq a) => Foo [a] where ...
589 then when we saw
590 (e :: (?x::Int) => t)
591 it would be unclear how to discharge all the potential uses of the ?x
592 in e. For example, a constraint Foo [Int] might come out of e, and
593 applying the instance decl would show up two uses of ?x. Trac #8912.
594 -}
595
596 checkValidTheta :: UserTypeCtxt -> ThetaType -> TcM ()
597 checkValidTheta ctxt theta
598 = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
599
600 -------------------------
601 check_valid_theta :: UserTypeCtxt -> [PredType] -> TcM ()
602 check_valid_theta _ []
603 = return ()
604 check_valid_theta ctxt theta
605 = do { dflags <- getDynFlags
606 ; warnTc (wopt Opt_WarnDuplicateConstraints dflags &&
607 notNull dups) (dupPredWarn dups)
608 ; traceTc "check_valid_theta" (ppr theta)
609 ; mapM_ (check_pred_ty dflags ctxt) theta }
610 where
611 (_,dups) = removeDups cmpPred theta
612
613 -------------------------
614 check_pred_ty :: DynFlags -> UserTypeCtxt -> PredType -> TcM ()
615 -- Check the validity of a predicate in a signature
616 -- Do not look through any type synonyms; any constraint kinded
617 -- type synonyms have been checked at their definition site
618 -- C.f. Trac #9838
619
620 check_pred_ty dflags ctxt pred
621 = do { checkValidMonoType pred
622 ; check_pred_help False dflags ctxt pred }
623
624 check_pred_help :: Bool -- True <=> under a type synonym
625 -> DynFlags -> UserTypeCtxt
626 -> PredType -> TcM ()
627 check_pred_help under_syn dflags ctxt pred
628 | Just pred' <- coreView pred -- Switch on under_syn when going under a
629 -- synonym (Trac #9838, yuk)
630 = check_pred_help True dflags ctxt pred'
631 | otherwise
632 = case splitTyConApp_maybe pred of
633 Just (tc, tys)
634 | isTupleTyCon tc
635 -> check_tuple_pred under_syn dflags ctxt pred tys
636 | Just cls <- tyConClass_maybe tc
637 -> check_class_pred dflags ctxt pred cls tys -- Includes Coercible
638 | tc `hasKey` eqTyConKey
639 -> check_eq_pred dflags pred tys
640 _ -> check_irred_pred under_syn dflags ctxt pred
641
642 check_eq_pred :: DynFlags -> PredType -> [TcType] -> TcM ()
643 check_eq_pred dflags pred tys
644 = -- Equational constraints are valid in all contexts if type
645 -- families are permitted
646 do { checkTc (length tys == 3)
647 (tyConArityErr eqTyCon tys)
648 ; checkTc (xopt Opt_TypeFamilies dflags || xopt Opt_GADTs dflags)
649 (eqPredTyErr pred) }
650
651 check_tuple_pred :: Bool -> DynFlags -> UserTypeCtxt -> PredType -> [PredType] -> TcM ()
652 check_tuple_pred under_syn dflags ctxt pred ts
653 = do { -- See Note [ConstraintKinds in predicates]
654 checkTc (under_syn || xopt Opt_ConstraintKinds dflags)
655 (predTupleErr pred)
656 ; mapM_ (check_pred_help under_syn dflags ctxt) ts }
657 -- This case will not normally be executed because without
658 -- -XConstraintKinds tuple types are only kind-checked as *
659
660 check_irred_pred :: Bool -> DynFlags -> UserTypeCtxt -> PredType -> TcM ()
661 check_irred_pred under_syn dflags ctxt pred
662 -- The predicate looks like (X t1 t2) or (x t1 t2) :: Constraint
663 -- where X is a type function
664 = do { -- If it looks like (x t1 t2), require ConstraintKinds
665 -- see Note [ConstraintKinds in predicates]
666 -- But (X t1 t2) is always ok because we just require ConstraintKinds
667 -- at the definition site (Trac #9838)
668 failIfTc (not under_syn && not (xopt Opt_ConstraintKinds dflags)
669 && hasTyVarHead pred)
670 (predIrredErr pred)
671
672 -- Make sure it is OK to have an irred pred in this context
673 -- See Note [Irreducible predicates in superclasses]
674 ; failIfTc (is_superclass ctxt
675 && not (xopt Opt_UndecidableInstances dflags)
676 && has_tyfun_head pred)
677 (predSuperClassErr pred) }
678 where
679 is_superclass ctxt = case ctxt of { ClassSCCtxt _ -> True; _ -> False }
680 has_tyfun_head ty
681 = case tcSplitTyConApp_maybe ty of
682 Just (tc, _) -> isTypeFamilyTyCon tc
683 Nothing -> False
684
685 {- Note [ConstraintKinds in predicates]
686 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
687 Don't check for -XConstraintKinds under a type synonym, because that
688 was done at the type synonym definition site; see Trac #9838
689 e.g. module A where
690 type C a = (Eq a, Ix a) -- Needs -XConstraintKinds
691 module B where
692 import A
693 f :: C a => a -> a -- Does *not* need -XConstraintKinds
694
695 Note [Irreducible predicates in superclasses]
696 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
697 Allowing type-family calls in class superclasses is somewhat dangerous
698 because we can write:
699
700 type family Fooish x :: * -> Constraint
701 type instance Fooish () = Foo
702 class Fooish () a => Foo a where
703
704 This will cause the constraint simplifier to loop because every time we canonicalise a
705 (Foo a) class constraint we add a (Fooish () a) constraint which will be immediately
706 solved to add+canonicalise another (Foo a) constraint. -}
707
708 -------------------------
709 check_class_pred :: DynFlags -> UserTypeCtxt -> PredType -> Class -> [TcType] -> TcM ()
710 check_class_pred dflags ctxt pred cls tys
711 | isIPClass cls
712 = do { check_arity
713 ; checkTc (okIPCtxt ctxt) (badIPPred pred) }
714
715 | otherwise
716 = do { check_arity
717 ; checkTc arg_tys_ok (predTyVarErr pred) }
718 where
719 check_arity = checkTc (classArity cls == length tys)
720 (tyConArityErr (classTyCon cls) tys)
721 flexible_contexts = xopt Opt_FlexibleContexts dflags
722 undecidable_ok = xopt Opt_UndecidableInstances dflags
723
724 arg_tys_ok = case ctxt of
725 SpecInstCtxt -> True -- {-# SPECIALISE instance Eq (T Int) #-} is fine
726 InstDeclCtxt -> checkValidClsArgs (flexible_contexts || undecidable_ok) tys
727 -- Further checks on head and theta
728 -- in checkInstTermination
729 _ -> checkValidClsArgs flexible_contexts tys
730
731 -------------------------
732 okIPCtxt :: UserTypeCtxt -> Bool
733 -- See Note [Implicit parameters in instance decls]
734 okIPCtxt (FunSigCtxt {}) = True
735 okIPCtxt (InfSigCtxt {}) = True
736 okIPCtxt ExprSigCtxt = True
737 okIPCtxt PatSigCtxt = True
738 okIPCtxt ResSigCtxt = True
739 okIPCtxt GenSigCtxt = True
740 okIPCtxt (ConArgCtxt {}) = True
741 okIPCtxt (ForSigCtxt {}) = True -- ??
742 okIPCtxt ThBrackCtxt = True
743 okIPCtxt GhciCtxt = True
744 okIPCtxt SigmaCtxt = True
745 okIPCtxt (DataTyCtxt {}) = True
746 okIPCtxt (PatSynCtxt {}) = True
747
748 okIPCtxt (ClassSCCtxt {}) = False
749 okIPCtxt (InstDeclCtxt {}) = False
750 okIPCtxt (SpecInstCtxt {}) = False
751 okIPCtxt (TySynCtxt {}) = False
752 okIPCtxt (RuleSigCtxt {}) = False
753 okIPCtxt DefaultDeclCtxt = False
754
755 badIPPred :: PredType -> SDoc
756 badIPPred pred = ptext (sLit "Illegal implicit parameter") <+> quotes (ppr pred)
757
758 {-
759 Note [Kind polymorphic type classes]
760 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
761 MultiParam check:
762
763 class C f where... -- C :: forall k. k -> Constraint
764 instance C Maybe where...
765
766 The dictionary gets type [C * Maybe] even if it's not a MultiParam
767 type class.
768
769 Flexibility check:
770
771 class C f where... -- C :: forall k. k -> Constraint
772 data D a = D a
773 instance C D where
774
775 The dictionary gets type [C * (D *)]. IA0_TODO it should be
776 generalized actually.
777 -}
778
779 checkThetaCtxt :: UserTypeCtxt -> ThetaType -> SDoc
780 checkThetaCtxt ctxt theta
781 = vcat [ptext (sLit "In the context:") <+> pprTheta theta,
782 ptext (sLit "While checking") <+> pprUserTypeCtxt ctxt ]
783
784 eqPredTyErr, predTyVarErr, predTupleErr, predIrredErr, predSuperClassErr :: PredType -> SDoc
785 eqPredTyErr pred = vcat [ ptext (sLit "Illegal equational constraint") <+> pprType pred
786 , parens (ptext (sLit "Use GADTs or TypeFamilies to permit this")) ]
787 predTyVarErr pred = vcat [ hang (ptext (sLit "Non type-variable argument"))
788 2 (ptext (sLit "in the constraint:") <+> pprType pred)
789 , parens (ptext (sLit "Use FlexibleContexts to permit this")) ]
790 predTupleErr pred = hang (ptext (sLit "Illegal tuple constraint:") <+> pprType pred)
791 2 (parens constraintKindsMsg)
792 predIrredErr pred = hang (ptext (sLit "Illegal constraint:") <+> pprType pred)
793 2 (parens constraintKindsMsg)
794 predSuperClassErr pred
795 = hang (ptext (sLit "Illegal constraint") <+> quotes (pprType pred)
796 <+> ptext (sLit "in a superclass context"))
797 2 (parens undecidableMsg)
798
799 constraintSynErr :: Type -> SDoc
800 constraintSynErr kind = hang (ptext (sLit "Illegal constraint synonym of kind:") <+> quotes (ppr kind))
801 2 (parens constraintKindsMsg)
802
803 dupPredWarn :: [[PredType]] -> SDoc
804 dupPredWarn dups = ptext (sLit "Duplicate constraint(s):") <+> pprWithCommas pprType (map head dups)
805
806 tyConArityErr :: TyCon -> [TcType] -> SDoc
807 -- For type-constructor arity errors, be careful to report
808 -- the number of /type/ arguments required and supplied,
809 -- ignoring the /kind/ arguments, which the user does not see.
810 -- (e.g. Trac #10516)
811 tyConArityErr tc tks
812 = arityErr (tyConFlavour tc) (tyConName tc)
813 tc_type_arity tc_type_args
814 where
815 tvs = tyConTyVars tc
816
817 kbs :: [Bool] -- True for a Type arg, false for a Kind arg
818 kbs = map isTypeVar tvs
819
820 -- tc_type_arity = number of *type* args expected
821 -- tc_type_args = number of *type* args encountered
822 tc_type_arity = count id kbs
823 tc_type_args = count (id . fst) (kbs `zip` tks)
824
825 arityErr :: Outputable a => String -> a -> Int -> Int -> SDoc
826 arityErr what name n m
827 = hsep [ ptext (sLit "The") <+> text what, quotes (ppr name), ptext (sLit "should have"),
828 n_arguments <> comma, text "but has been given",
829 if m==0 then text "none" else int m]
830 where
831 n_arguments | n == 0 = ptext (sLit "no arguments")
832 | n == 1 = ptext (sLit "1 argument")
833 | True = hsep [int n, ptext (sLit "arguments")]
834
835 {-
836 ************************************************************************
837 * *
838 \subsection{Checking for a decent instance head type}
839 * *
840 ************************************************************************
841
842 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
843 it must normally look like: @instance Foo (Tycon a b c ...) ...@
844
845 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
846 flag is on, or (2)~the instance is imported (they must have been
847 compiled elsewhere). In these cases, we let them go through anyway.
848
849 We can also have instances for functions: @instance Foo (a -> b) ...@.
850 -}
851
852 checkValidInstHead :: UserTypeCtxt -> Class -> [Type] -> TcM ()
853 checkValidInstHead ctxt clas cls_args
854 = do { dflags <- getDynFlags
855
856 ; checkTc (clas `notElem` abstractClasses)
857 (instTypeErr clas cls_args abstract_class_msg)
858
859 -- Check language restrictions;
860 -- but not for SPECIALISE isntance pragmas
861 ; let ty_args = dropWhile isKind cls_args
862 ; unless spec_inst_prag $
863 do { checkTc (xopt Opt_TypeSynonymInstances dflags ||
864 all tcInstHeadTyNotSynonym ty_args)
865 (instTypeErr clas cls_args head_type_synonym_msg)
866 ; checkTc (xopt Opt_FlexibleInstances dflags ||
867 all tcInstHeadTyAppAllTyVars ty_args)
868 (instTypeErr clas cls_args head_type_args_tyvars_msg)
869 ; checkTc (xopt Opt_MultiParamTypeClasses dflags ||
870 length ty_args == 1 || -- Only count type arguments
871 (xopt Opt_NullaryTypeClasses dflags &&
872 null ty_args))
873 (instTypeErr clas cls_args head_one_type_msg) }
874
875 -- May not contain type family applications
876 ; mapM_ checkTyFamFreeness ty_args
877
878 ; mapM_ checkValidMonoType ty_args
879 -- For now, I only allow tau-types (not polytypes) in
880 -- the head of an instance decl.
881 -- E.g. instance C (forall a. a->a) is rejected
882 -- One could imagine generalising that, but I'm not sure
883 -- what all the consequences might be
884 }
885
886 where
887 spec_inst_prag = case ctxt of { SpecInstCtxt -> True; _ -> False }
888
889 head_type_synonym_msg = parens (
890 text "All instance types must be of the form (T t1 ... tn)" $$
891 text "where T is not a synonym." $$
892 text "Use TypeSynonymInstances if you want to disable this.")
893
894 head_type_args_tyvars_msg = parens (vcat [
895 text "All instance types must be of the form (T a1 ... an)",
896 text "where a1 ... an are *distinct type variables*,",
897 text "and each type variable appears at most once in the instance head.",
898 text "Use FlexibleInstances if you want to disable this."])
899
900 head_one_type_msg = parens (
901 text "Only one type can be given in an instance head." $$
902 text "Use MultiParamTypeClasses if you want to allow more, or zero.")
903
904 abstract_class_msg =
905 text "The class is abstract, manual instances are not permitted."
906
907 abstractClasses :: [ Class ]
908 abstractClasses = [ coercibleClass ] -- See Note [Coercible Instances]
909
910 instTypeErr :: Class -> [Type] -> SDoc -> SDoc
911 instTypeErr cls tys msg
912 = hang (hang (ptext (sLit "Illegal instance declaration for"))
913 2 (quotes (pprClassPred cls tys)))
914 2 msg
915
916 {- Note [Valid 'deriving' predicate]
917 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
918 validDerivPred checks for OK 'deriving' context. See Note [Exotic
919 derived instance contexts] in TcDeriv. However the predicate is
920 here because it uses sizeTypes, fvTypes.
921
922 It checks for three things
923
924 * No repeated variables (hasNoDups fvs)
925
926 * No type constructors. This is done by comparing
927 sizeTypes tys == length (fvTypes tys)
928 sizeTypes counts variables and constructors; fvTypes returns variables.
929 So if they are the same, there must be no constructors. But there
930 might be applications thus (f (g x)).
931
932 * Also check for a bizarre corner case, when the derived instance decl
933 would look like
934 instance C a b => D (T a) where ...
935 Note that 'b' isn't a parameter of T. This gives rise to all sorts of
936 problems; in particular, it's hard to compare solutions for equality
937 when finding the fixpoint, and that means the inferContext loop does
938 not converge. See Trac #5287.
939 -}
940
941 validDerivPred :: TyVarSet -> PredType -> Bool
942 -- See Note [Valid 'deriving' predicate]
943 validDerivPred tv_set pred
944 = case classifyPredType pred of
945 ClassPred _ tys -> check_tys tys
946 EqPred {} -> False -- reject equality constraints
947 _ -> True -- Non-class predicates are ok
948 where
949 check_tys tys = hasNoDups fvs
950 && sizeTypes tys == fromIntegral (length fvs)
951 && all (`elemVarSet` tv_set) fvs
952 where
953 fvs = fvTypes tys
954
955 {-
956 ************************************************************************
957 * *
958 \subsection{Checking instance for termination}
959 * *
960 ************************************************************************
961 -}
962
963 checkValidInstance :: UserTypeCtxt -> LHsType Name -> Type
964 -> TcM ([TyVar], ThetaType, Class, [Type])
965 checkValidInstance ctxt hs_type ty
966 | Just (clas,inst_tys) <- getClassPredTys_maybe tau
967 , inst_tys `lengthIs` classArity clas
968 = do { setSrcSpan head_loc (checkValidInstHead ctxt clas inst_tys)
969 ; checkValidTheta ctxt theta
970
971 -- The Termination and Coverate Conditions
972 -- Check that instance inference will terminate (if we care)
973 -- For Haskell 98 this will already have been done by checkValidTheta,
974 -- but as we may be using other extensions we need to check.
975 --
976 -- Note that the Termination Condition is *more conservative* than
977 -- the checkAmbiguity test we do on other type signatures
978 -- e.g. Bar a => Bar Int is ambiguous, but it also fails
979 -- the termination condition, because 'a' appears more often
980 -- in the constraint than in the head
981 ; undecidable_ok <- xoptM Opt_UndecidableInstances
982 ; if undecidable_ok
983 then checkAmbiguity ctxt ty
984 else checkInstTermination inst_tys theta
985
986 ; case (checkInstCoverage undecidable_ok clas theta inst_tys) of
987 IsValid -> return () -- Check succeeded
988 NotValid msg -> addErrTc (instTypeErr clas inst_tys msg)
989
990 ; return (tvs, theta, clas, inst_tys) }
991
992 | otherwise
993 = failWithTc (ptext (sLit "Malformed instance head:") <+> ppr tau)
994 where
995 (tvs, theta, tau) = tcSplitSigmaTy ty
996
997 -- The location of the "head" of the instance
998 head_loc = case hs_type of
999 L _ (HsForAllTy _ _ _ _ (L loc _)) -> loc
1000 L loc _ -> loc
1001
1002 {-
1003 Note [Paterson conditions]
1004 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1005 Termination test: the so-called "Paterson conditions" (see Section 5 of
1006 "Understanding functional dependencies via Constraint Handling Rules,
1007 JFP Jan 2007).
1008
1009 We check that each assertion in the context satisfies:
1010 (1) no variable has more occurrences in the assertion than in the head, and
1011 (2) the assertion has fewer constructors and variables (taken together
1012 and counting repetitions) than the head.
1013 This is only needed with -fglasgow-exts, as Haskell 98 restrictions
1014 (which have already been checked) guarantee termination.
1015
1016 The underlying idea is that
1017
1018 for any ground substitution, each assertion in the
1019 context has fewer type constructors than the head.
1020 -}
1021
1022 checkInstTermination :: [TcType] -> ThetaType -> TcM ()
1023 -- See Note [Paterson conditions]
1024 checkInstTermination tys theta
1025 = check_preds theta
1026 where
1027 head_fvs = fvTypes tys
1028 head_size = sizeTypes tys
1029
1030 check_preds :: [PredType] -> TcM ()
1031 check_preds preds = mapM_ check preds
1032
1033 check :: PredType -> TcM ()
1034 check pred
1035 = case classifyPredType pred of
1036 EqPred {} -> return () -- See Trac #4200.
1037 IrredPred {} -> check2 pred (sizeType pred)
1038 ClassPred cls tys
1039 | isIPClass cls
1040 -> return () -- You can't get to class predicates from implicit params
1041
1042 | isCTupleClass cls -- Look inside tuple predicates; Trac #8359
1043 -> check_preds tys
1044
1045 | otherwise
1046 -> check2 pred (sizeTypes tys) -- Other ClassPreds
1047
1048 check2 pred pred_size
1049 | not (null bad_tvs) = addErrTc (noMoreMsg bad_tvs what)
1050 | pred_size >= head_size = addErrTc (smallerMsg what)
1051 | otherwise = return ()
1052 where
1053 what = ptext (sLit "constraint") <+> quotes (ppr pred)
1054 bad_tvs = fvType pred \\ head_fvs
1055
1056 smallerMsg :: SDoc -> SDoc
1057 smallerMsg what
1058 = vcat [ hang (ptext (sLit "The") <+> what)
1059 2 (ptext (sLit "is no smaller than the instance head"))
1060 , parens undecidableMsg ]
1061
1062 noMoreMsg :: [TcTyVar] -> SDoc -> SDoc
1063 noMoreMsg tvs what
1064 = vcat [ hang (ptext (sLit "Variable") <> plural tvs <+> quotes (pprWithCommas ppr tvs)
1065 <+> occurs <+> ptext (sLit "more often"))
1066 2 (sep [ ptext (sLit "in the") <+> what
1067 , ptext (sLit "than in the instance head") ])
1068 , parens undecidableMsg ]
1069 where
1070 occurs = if isSingleton tvs then ptext (sLit "occurs")
1071 else ptext (sLit "occur")
1072
1073 undecidableMsg, constraintKindsMsg :: SDoc
1074 undecidableMsg = ptext (sLit "Use UndecidableInstances to permit this")
1075 constraintKindsMsg = ptext (sLit "Use ConstraintKinds to permit this")
1076
1077 {-
1078 Note [Associated type instances]
1079 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1080 We allow this:
1081 class C a where
1082 type T x a
1083 instance C Int where
1084 type T (S y) Int = y
1085 type T Z Int = Char
1086
1087 Note that
1088 a) The variable 'x' is not bound by the class decl
1089 b) 'x' is instantiated to a non-type-variable in the instance
1090 c) There are several type instance decls for T in the instance
1091
1092 All this is fine. Of course, you can't give any *more* instances
1093 for (T ty Int) elsewhere, because it's an *associated* type.
1094
1095 Note [Checking consistent instantiation]
1096 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1097 class C a b where
1098 type T a x b
1099
1100 instance C [p] Int
1101 type T [p] y Int = (p,y,y) -- Induces the family instance TyCon
1102 -- type TR p y = (p,y,y)
1103
1104 So we
1105 * Form the mini-envt from the class type variables a,b
1106 to the instance decl types [p],Int: [a->[p], b->Int]
1107
1108 * Look at the tyvars a,x,b of the type family constructor T
1109 (it shares tyvars with the class C)
1110
1111 * Apply the mini-evnt to them, and check that the result is
1112 consistent with the instance types [p] y Int
1113
1114 We do *not* assume (at this point) the the bound variables of
1115 the associated type instance decl are the same as for the parent
1116 instance decl. So, for example,
1117
1118 instance C [p] Int
1119 type T [q] y Int = ...
1120
1121 would work equally well. Reason: making the *kind* variables line
1122 up is much harder. Example (Trac #7282):
1123 class Foo (xs :: [k]) where
1124 type Bar xs :: *
1125
1126 instance Foo '[] where
1127 type Bar '[] = Int
1128 Here the instance decl really looks like
1129 instance Foo k ('[] k) where
1130 type Bar k ('[] k) = Int
1131 but the k's are not scoped, and hence won't match Uniques.
1132
1133 So instead we just match structure, with tcMatchTyX, and check
1134 that distinct type variables match 1-1 with distinct type variables.
1135
1136 HOWEVER, we *still* make the instance type variables scope over the
1137 type instances, to pick up non-obvious kinds. Eg
1138 class Foo (a :: k) where
1139 type F a
1140 instance Foo (b :: k -> k) where
1141 type F b = Int
1142 Here the instance is kind-indexed and really looks like
1143 type F (k->k) (b::k->k) = Int
1144 But if the 'b' didn't scope, we would make F's instance too
1145 poly-kinded.
1146 -}
1147
1148 checkConsistentFamInst
1149 :: Maybe ( Class
1150 , VarEnv Type ) -- ^ Class of associated type
1151 -- and instantiation of class TyVars
1152 -> TyCon -- ^ Family tycon
1153 -> [TyVar] -- ^ Type variables of the family instance
1154 -> [Type] -- ^ Type patterns from instance
1155 -> TcM ()
1156 -- See Note [Checking consistent instantiation]
1157
1158 checkConsistentFamInst Nothing _ _ _ = return ()
1159 checkConsistentFamInst (Just (clas, mini_env)) fam_tc at_tvs at_tys
1160 = do { -- Check that the associated type indeed comes from this class
1161 checkTc (Just clas == tyConAssoc_maybe fam_tc)
1162 (badATErr (className clas) (tyConName fam_tc))
1163
1164 -- See Note [Checking consistent instantiation] in TcTyClsDecls
1165 -- Check right to left, so that we spot type variable
1166 -- inconsistencies before (more confusing) kind variables
1167 ; discardResult $ foldrM check_arg emptyTvSubst $
1168 tyConTyVars fam_tc `zip` at_tys }
1169 where
1170 at_tv_set = mkVarSet at_tvs
1171
1172 check_arg :: (TyVar, Type) -> TvSubst -> TcM TvSubst
1173 check_arg (fam_tc_tv, at_ty) subst
1174 | Just inst_ty <- lookupVarEnv mini_env fam_tc_tv
1175 = case tcMatchTyX at_tv_set subst at_ty inst_ty of
1176 Just subst | all_distinct subst -> return subst
1177 _ -> failWithTc $ wrongATArgErr at_ty inst_ty
1178 -- No need to instantiate here, because the axiom
1179 -- uses the same type variables as the assocated class
1180 | otherwise
1181 = return subst -- Allow non-type-variable instantiation
1182 -- See Note [Associated type instances]
1183
1184 all_distinct :: TvSubst -> Bool
1185 -- True if all the variables mapped the substitution
1186 -- map to *distinct* type *variables*
1187 all_distinct subst = go [] at_tvs
1188 where
1189 go _ [] = True
1190 go acc (tv:tvs) = case lookupTyVar subst tv of
1191 Nothing -> go acc tvs
1192 Just ty | Just tv' <- tcGetTyVar_maybe ty
1193 , tv' `notElem` acc
1194 -> go (tv' : acc) tvs
1195 _other -> False
1196
1197 badATErr :: Name -> Name -> SDoc
1198 badATErr clas op
1199 = hsep [ptext (sLit "Class"), quotes (ppr clas),
1200 ptext (sLit "does not have an associated type"), quotes (ppr op)]
1201
1202 wrongATArgErr :: Type -> Type -> SDoc
1203 wrongATArgErr ty instTy =
1204 sep [ ptext (sLit "Type indexes must match class instance head")
1205 , ptext (sLit "Found") <+> quotes (ppr ty)
1206 <+> ptext (sLit "but expected") <+> quotes (ppr instTy)
1207 ]
1208
1209 {-
1210 ************************************************************************
1211 * *
1212 Checking type instance well-formedness and termination
1213 * *
1214 ************************************************************************
1215 -}
1216
1217 checkValidCoAxiom :: CoAxiom Branched -> TcM ()
1218 checkValidCoAxiom (CoAxiom { co_ax_tc = fam_tc, co_ax_branches = branches })
1219 = do { _ <- brListMapM (checkValidCoAxBranch Nothing fam_tc) branches
1220 ; brListFoldlM_ check_branch_compat [] branches }
1221 where
1222 injectivity = familyTyConInjectivityInfo fam_tc
1223
1224 check_branch_compat :: [CoAxBranch] -- previous branches in reverse order
1225 -> CoAxBranch -- current branch
1226 -> TcM [CoAxBranch]-- current branch : previous branches
1227 -- Check for
1228 -- (a) this banch is dominated by previous ones
1229 -- (b) failure of injectivity
1230 check_branch_compat prev_branches cur_branch
1231 | cur_branch `isDominatedBy` prev_branches
1232 = do { addWarnAt (coAxBranchSpan cur_branch) $
1233 inaccessibleCoAxBranch fam_tc cur_branch
1234 ; return prev_branches }
1235 | otherwise
1236 = do { check_injectivity prev_branches cur_branch
1237 ; return (cur_branch : prev_branches) }
1238
1239 -- Injectivity check: check whether a new (CoAxBranch) can extend
1240 -- already checked equations without violating injectivity
1241 -- annotation supplied by the user.
1242 -- See Note [Verifying injectivity annotation] in FamInstEnv
1243 check_injectivity prev_branches cur_branch
1244 | Injective inj <- injectivity
1245 = do { let conflicts =
1246 fst $ foldl (gather_conflicts inj prev_branches cur_branch)
1247 ([], 0) prev_branches
1248 ; mapM_ (\(err, span) -> setSrcSpan span $ addErr err)
1249 (makeInjectivityErrors fam_tc cur_branch inj conflicts) }
1250 | otherwise
1251 = return ()
1252
1253 gather_conflicts inj prev_branches cur_branch (acc, n) branch
1254 -- n is 0-based index of branch in prev_branches
1255 = case injectiveBranches inj cur_branch branch of
1256 InjectivityUnified ax1 ax2
1257 | ax1 `isDominatedBy` (replace_br prev_branches n ax2)
1258 -> (acc, n + 1)
1259 | otherwise
1260 -> (branch : acc, n + 1)
1261 InjectivityAccepted -> (acc, n + 1)
1262
1263 -- Replace n-th element in the list. Assumes 0-based indexing.
1264 replace_br :: [CoAxBranch] -> Int -> CoAxBranch -> [CoAxBranch]
1265 replace_br brs n br = take n brs ++ [br] ++ drop (n+1) brs
1266
1267
1268 -- Check that a "type instance" is well-formed (which includes decidability
1269 -- unless -XUndecidableInstances is given).
1270 --
1271 checkValidCoAxBranch :: Maybe ( Class, VarEnv Type )
1272 -> TyCon -> CoAxBranch -> TcM ()
1273 checkValidCoAxBranch mb_clsinfo fam_tc
1274 (CoAxBranch { cab_tvs = tvs, cab_lhs = typats
1275 , cab_rhs = rhs, cab_loc = loc })
1276 = setSrcSpan loc $
1277 do { checkValidFamPats fam_tc tvs typats
1278
1279 -- The argument patterns, and RHS, are all boxed tau types
1280 -- E.g Reject type family F (a :: k1) :: k2
1281 -- type instance F (forall a. a->a) = ...
1282 -- type instance F Int# = ...
1283 -- type instance F Int = forall a. a->a
1284 -- type instance F Int = Int#
1285 -- See Trac #9357
1286 ; mapM_ checkValidMonoType typats
1287 ; checkValidMonoType rhs
1288
1289 -- We have a decidable instance unless otherwise permitted
1290 ; undecidable_ok <- xoptM Opt_UndecidableInstances
1291 ; unless undecidable_ok $
1292 mapM_ addErrTc (checkFamInstRhs typats (tcTyFamInsts rhs))
1293
1294 -- Check that type patterns match the class instance head
1295 ; checkConsistentFamInst mb_clsinfo fam_tc tvs typats }
1296
1297 -- Make sure that each type family application is
1298 -- (1) strictly smaller than the lhs,
1299 -- (2) mentions no type variable more often than the lhs, and
1300 -- (3) does not contain any further type family instances.
1301 --
1302 checkFamInstRhs :: [Type] -- lhs
1303 -> [(TyCon, [Type])] -- type family instances
1304 -> [MsgDoc]
1305 checkFamInstRhs lhsTys famInsts
1306 = mapMaybe check famInsts
1307 where
1308 size = sizeTypes lhsTys
1309 fvs = fvTypes lhsTys
1310 check (tc, tys)
1311 | not (all isTyFamFree tys) = Just (nestedMsg what)
1312 | not (null bad_tvs) = Just (noMoreMsg bad_tvs what)
1313 | size <= sizeTypes tys = Just (smallerMsg what)
1314 | otherwise = Nothing
1315 where
1316 what = ptext (sLit "type family application") <+> quotes (pprType (TyConApp tc tys))
1317 bad_tvs = fvTypes tys \\ fvs
1318
1319 checkValidFamPats :: TyCon -> [TyVar] -> [Type] -> TcM ()
1320 -- Patterns in a 'type instance' or 'data instance' decl should
1321 -- a) contain no type family applications
1322 -- (vanilla synonyms are fine, though)
1323 -- b) properly bind all their free type variables
1324 -- e.g. we disallow (Trac #7536)
1325 -- type T a = Int
1326 -- type instance F (T a) = a
1327 -- c) Have the right number of patterns
1328 checkValidFamPats fam_tc tvs ty_pats
1329 = ASSERT( length ty_pats == tyConArity fam_tc )
1330 -- A family instance must have exactly the same number of type
1331 -- parameters as the family declaration. You can't write
1332 -- type family F a :: * -> *
1333 -- type instance F Int y = y
1334 -- because then the type (F Int) would be like (\y.y)
1335 -- But this is checked at the time the axiom is created
1336 do { mapM_ checkTyFamFreeness ty_pats
1337 ; let unbound_tvs = filterOut (`elemVarSet` exactTyVarsOfTypes ty_pats) tvs
1338 ; checkTc (null unbound_tvs) (famPatErr fam_tc unbound_tvs ty_pats) }
1339
1340 -- Ensure that no type family instances occur in a type.
1341 checkTyFamFreeness :: Type -> TcM ()
1342 checkTyFamFreeness ty
1343 = checkTc (isTyFamFree ty) $
1344 tyFamInstIllegalErr ty
1345
1346 -- Check that a type does not contain any type family applications.
1347 --
1348 isTyFamFree :: Type -> Bool
1349 isTyFamFree = null . tcTyFamInsts
1350
1351 -- Error messages
1352
1353 inaccessibleCoAxBranch :: TyCon -> CoAxBranch -> SDoc
1354 inaccessibleCoAxBranch fam_tc (CoAxBranch { cab_tvs = tvs
1355 , cab_lhs = lhs
1356 , cab_rhs = rhs })
1357 = ptext (sLit "Type family instance equation is overlapped:") $$
1358 hang (pprUserForAll tvs)
1359 2 (hang (pprTypeApp fam_tc lhs) 2 (equals <+> (ppr rhs)))
1360
1361 tyFamInstIllegalErr :: Type -> SDoc
1362 tyFamInstIllegalErr ty
1363 = hang (ptext (sLit "Illegal type synonym family application in instance") <>
1364 colon) 2 $
1365 ppr ty
1366
1367 nestedMsg :: SDoc -> SDoc
1368 nestedMsg what
1369 = sep [ ptext (sLit "Illegal nested") <+> what
1370 , parens undecidableMsg ]
1371
1372 famPatErr :: TyCon -> [TyVar] -> [Type] -> SDoc
1373 famPatErr fam_tc tvs pats
1374 = hang (ptext (sLit "Family instance purports to bind type variable") <> plural tvs
1375 <+> pprQuotedList tvs)
1376 2 (hang (ptext (sLit "but the real LHS (expanding synonyms) is:"))
1377 2 (pprTypeApp fam_tc (map expandTypeSynonyms pats) <+> ptext (sLit "= ...")))
1378
1379 {-
1380 ************************************************************************
1381 * *
1382 \subsection{Auxiliary functions}
1383 * *
1384 ************************************************************************
1385 -}
1386
1387 -- Free variables of a type, retaining repetitions, and expanding synonyms
1388 -- Ignore kinds altogether: rightly or wrongly, we only check for
1389 -- excessive occurrences of *type* variables.
1390 -- e.g. type instance Demote {T k} a = T (Demote {k} (Any {k}))
1391 --
1392 -- c.f. sizeType, which is often called side by side with fvType
1393 fvType, fv_type :: Type -> [TyVar]
1394 fvType ty | isKind ty = []
1395 | otherwise = fv_type ty
1396
1397 fv_type ty | Just exp_ty <- tcView ty = fv_type exp_ty
1398 fv_type (TyVarTy tv) = [tv]
1399 fv_type (TyConApp _ tys) = fvTypes tys
1400 fv_type (LitTy {}) = []
1401 fv_type (FunTy arg res) = fv_type arg ++ fv_type res
1402 fv_type (AppTy fun arg) = fv_type fun ++ fv_type arg
1403 fv_type (ForAllTy tyvar ty) = filter (/= tyvar) (fv_type ty)
1404
1405 fvTypes :: [Type] -> [TyVar]
1406 fvTypes tys = concat (map fvType tys)
1407