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