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