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