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