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