Re-do superclass solving (again); fixes #10423
[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, eqTyConName )
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 suppply 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 <= n_args -- 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 (arityErr flavour (tyConName tc) tc_arity n_args)
466 where
467 flavour | isTypeFamilyTyCon tc = "Type family"
468 | otherwise = "Type synonym"
469 n_args = length tys
470 tc_arity = tyConArity tc
471 check_arg | isTypeFamilyTyCon tc = check_arg_type ctxt rank
472 | otherwise = check_mono_type ctxt synArgMonoType
473
474 ----------------------------------------
475 check_ubx_tuple :: UserTypeCtxt -> KindOrType
476 -> [KindOrType] -> TcM ()
477 check_ubx_tuple ctxt ty tys
478 = do { ub_tuples_allowed <- xoptM Opt_UnboxedTuples
479 ; checkTc ub_tuples_allowed (ubxArgTyErr ty)
480
481 ; impred <- xoptM Opt_ImpredicativeTypes
482 ; let rank' = if impred then ArbitraryRank else tyConArgMonoType
483 -- c.f. check_arg_type
484 -- However, args are allowed to be unlifted, or
485 -- more unboxed tuples, so can't use check_arg_ty
486 ; mapM_ (check_type ctxt rank') tys }
487
488 ----------------------------------------
489 check_arg_type :: UserTypeCtxt -> Rank -> KindOrType -> TcM ()
490 -- The sort of type that can instantiate a type variable,
491 -- or be the argument of a type constructor.
492 -- Not an unboxed tuple, but now *can* be a forall (since impredicativity)
493 -- Other unboxed types are very occasionally allowed as type
494 -- arguments depending on the kind of the type constructor
495 --
496 -- For example, we want to reject things like:
497 --
498 -- instance Ord a => Ord (forall s. T s a)
499 -- and
500 -- g :: T s (forall b.b)
501 --
502 -- NB: unboxed tuples can have polymorphic or unboxed args.
503 -- This happens in the workers for functions returning
504 -- product types with polymorphic components.
505 -- But not in user code.
506 -- Anyway, they are dealt with by a special case in check_tau_type
507
508 check_arg_type ctxt rank ty
509 | isKind ty = return () -- IA0_NOTE: Do we need to check a kind?
510 | otherwise
511 = do { impred <- xoptM Opt_ImpredicativeTypes
512 ; let rank' = case rank of -- Predictive => must be monotype
513 MustBeMonoType -> MustBeMonoType -- Monotype, regardless
514 _other | impred -> ArbitraryRank
515 | otherwise -> tyConArgMonoType
516 -- Make sure that MustBeMonoType is propagated,
517 -- so that we don't suggest -XImpredicativeTypes in
518 -- (Ord (forall a.a)) => a -> a
519 -- and so that if it Must be a monotype, we check that it is!
520
521 ; check_type ctxt rank' ty
522 ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
523 -- NB the isUnLiftedType test also checks for
524 -- T State#
525 -- where there is an illegal partial application of State# (which has
526 -- kind * -> #); see Note [The kind invariant] in TypeRep
527
528 ----------------------------------------
529 forAllTyErr :: Rank -> Type -> SDoc
530 forAllTyErr rank ty
531 = vcat [ hang (ptext (sLit "Illegal polymorphic or qualified type:")) 2 (ppr ty)
532 , suggestion ]
533 where
534 suggestion = case rank of
535 LimitedRank {} -> ptext (sLit "Perhaps you intended to use RankNTypes or Rank2Types")
536 MonoType d -> d
537 _ -> Outputable.empty -- Polytype is always illegal
538
539 unliftedArgErr, ubxArgTyErr :: Type -> SDoc
540 unliftedArgErr ty = sep [ptext (sLit "Illegal unlifted type:"), ppr ty]
541 ubxArgTyErr ty = sep [ptext (sLit "Illegal unboxed tuple type as function argument:"), ppr ty]
542
543 kindErr :: Kind -> SDoc
544 kindErr kind = sep [ptext (sLit "Expecting an ordinary type, but found a type of kind"), ppr kind]
545
546 {-
547 Note [Liberal type synonyms]
548 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
549 If -XLiberalTypeSynonyms is on, expand closed type synonyms *before*
550 doing validity checking. This allows us to instantiate a synonym defn
551 with a for-all type, or with a partially-applied type synonym.
552 e.g. type T a b = a
553 type S m = m ()
554 f :: S (T Int)
555 Here, T is partially applied, so it's illegal in H98. But if you
556 expand S first, then T we get just
557 f :: Int
558 which is fine.
559
560 IMPORTANT: suppose T is a type synonym. Then we must do validity
561 checking on an appliation (T ty1 ty2)
562
563 *either* before expansion (i.e. check ty1, ty2)
564 *or* after expansion (i.e. expand T ty1 ty2, and then check)
565 BUT NOT BOTH
566
567 If we do both, we get exponential behaviour!!
568
569 data TIACons1 i r c = c i ::: r c
570 type TIACons2 t x = TIACons1 t (TIACons1 t x)
571 type TIACons3 t x = TIACons2 t (TIACons1 t x)
572 type TIACons4 t x = TIACons2 t (TIACons2 t x)
573 type TIACons7 t x = TIACons4 t (TIACons3 t x)
574
575
576 ************************************************************************
577 * *
578 \subsection{Checking a theta or source type}
579 * *
580 ************************************************************************
581
582 Note [Implicit parameters in instance decls]
583 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
584 Implicit parameters _only_ allowed in type signatures; not in instance
585 decls, superclasses etc. The reason for not allowing implicit params in
586 instances is a bit subtle. If we allowed
587 instance (?x::Int, Eq a) => Foo [a] where ...
588 then when we saw
589 (e :: (?x::Int) => t)
590 it would be unclear how to discharge all the potential uses of the ?x
591 in e. For example, a constraint Foo [Int] might come out of e, and
592 applying the instance decl would show up two uses of ?x. Trac #8912.
593 -}
594
595 checkValidTheta :: UserTypeCtxt -> ThetaType -> TcM ()
596 checkValidTheta ctxt theta
597 = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
598
599 -------------------------
600 check_valid_theta :: UserTypeCtxt -> [PredType] -> TcM ()
601 check_valid_theta _ []
602 = return ()
603 check_valid_theta ctxt theta
604 = do { dflags <- getDynFlags
605 ; warnTc (wopt Opt_WarnDuplicateConstraints dflags &&
606 notNull dups) (dupPredWarn dups)
607 ; traceTc "check_valid_theta" (ppr theta)
608 ; mapM_ (check_pred_ty dflags ctxt) theta }
609 where
610 (_,dups) = removeDups cmpPred theta
611
612 -------------------------
613 check_pred_ty :: DynFlags -> UserTypeCtxt -> PredType -> TcM ()
614 -- Check the validity of a predicate in a signature
615 -- Do not look through any type synonyms; any constraint kinded
616 -- type synonyms have been checked at their definition site
617 -- C.f. Trac #9838
618
619 check_pred_ty dflags ctxt pred
620 = do { checkValidMonoType pred
621 ; check_pred_help False dflags ctxt pred }
622
623 check_pred_help :: Bool -- True <=> under a type synonym
624 -> DynFlags -> UserTypeCtxt
625 -> PredType -> TcM ()
626 check_pred_help under_syn dflags ctxt pred
627 | Just pred' <- coreView pred -- Switch on under_syn when going under a
628 -- synonym (Trac #9838, yuk)
629 = check_pred_help True dflags ctxt pred'
630 | otherwise
631 = case splitTyConApp_maybe pred of
632 Just (tc, tys)
633 | isTupleTyCon tc
634 -> check_tuple_pred under_syn dflags ctxt pred tys
635 | Just cls <- tyConClass_maybe tc
636 -> check_class_pred dflags ctxt pred cls tys -- Includes Coercible
637 | tc `hasKey` eqTyConKey
638 -> check_eq_pred dflags pred tys
639 _ -> check_irred_pred under_syn dflags ctxt pred
640
641 check_eq_pred :: DynFlags -> PredType -> [TcType] -> TcM ()
642 check_eq_pred dflags pred tys
643 = -- Equational constraints are valid in all contexts if type
644 -- families are permitted
645 do { checkTc (n_tys == 3)
646 (arityErr "Equality constraint" eqTyConName 3 n_tys)
647 ; checkTc (xopt Opt_TypeFamilies dflags || xopt Opt_GADTs dflags)
648 (eqPredTyErr pred) }
649 where
650 n_tys = length tys
651
652 check_tuple_pred :: Bool -> DynFlags -> UserTypeCtxt -> PredType -> [PredType] -> TcM ()
653 check_tuple_pred under_syn dflags ctxt pred ts
654 = do { -- See Note [ConstraintKinds in predicates]
655 checkTc (under_syn || xopt Opt_ConstraintKinds dflags)
656 (predTupleErr pred)
657 ; mapM_ (check_pred_help under_syn dflags ctxt) ts }
658 -- This case will not normally be executed because without
659 -- -XConstraintKinds tuple types are only kind-checked as *
660
661 check_irred_pred :: Bool -> DynFlags -> UserTypeCtxt -> PredType -> TcM ()
662 check_irred_pred under_syn dflags ctxt pred
663 -- The predicate looks like (X t1 t2) or (x t1 t2) :: Constraint
664 -- where X is a type function
665 = do { -- If it looks like (x t1 t2), require ConstraintKinds
666 -- see Note [ConstraintKinds in predicates]
667 -- But (X t1 t2) is always ok because we just require ConstraintKinds
668 -- at the definition site (Trac #9838)
669 failIfTc (not under_syn && not (xopt Opt_ConstraintKinds dflags)
670 && hasTyVarHead pred)
671 (predIrredErr pred)
672
673 -- Make sure it is OK to have an irred pred in this context
674 -- See Note [Irreducible predicates in superclasses]
675 ; failIfTc (is_superclass ctxt
676 && not (xopt Opt_UndecidableInstances dflags)
677 && has_tyfun_head pred)
678 (predSuperClassErr pred) }
679 where
680 is_superclass ctxt = case ctxt of { ClassSCCtxt _ -> True; _ -> False }
681 has_tyfun_head ty
682 = case tcSplitTyConApp_maybe ty of
683 Just (tc, _) -> isTypeFamilyTyCon tc
684 Nothing -> False
685
686 {- Note [ConstraintKinds in predicates]
687 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
688 Don't check for -XConstraintKinds under a type synonym, because that
689 was done at the type synonym definition site; see Trac #9838
690 e.g. module A where
691 type C a = (Eq a, Ix a) -- Needs -XConstraintKinds
692 module B where
693 import A
694 f :: C a => a -> a -- Does *not* need -XConstraintKinds
695
696 Note [Irreducible predicates in superclasses]
697 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
698 Allowing type-family calls in class superclasses is somewhat dangerous
699 because we can write:
700
701 type family Fooish x :: * -> Constraint
702 type instance Fooish () = Foo
703 class Fooish () a => Foo a where
704
705 This will cause the constraint simplifier to loop because every time we canonicalise a
706 (Foo a) class constraint we add a (Fooish () a) constraint which will be immediately
707 solved to add+canonicalise another (Foo a) constraint. -}
708
709 -------------------------
710 check_class_pred :: DynFlags -> UserTypeCtxt -> PredType -> Class -> [TcType] -> TcM ()
711 check_class_pred dflags ctxt pred cls tys
712 | isIPClass cls
713 = do { checkTc (arity == n_tys) arity_err
714 ; checkTc (okIPCtxt ctxt) (badIPPred pred) }
715
716 | otherwise
717 = do { checkTc (arity == n_tys) arity_err
718 ; checkTc arg_tys_ok (predTyVarErr pred) }
719 where
720 class_name = className cls
721 arity = classArity cls
722 n_tys = length tys
723 arity_err = arityErr "Class" class_name arity n_tys
724
725 flexible_contexts = xopt Opt_FlexibleContexts dflags
726 undecidable_ok = xopt Opt_UndecidableInstances dflags
727
728 arg_tys_ok = case ctxt of
729 SpecInstCtxt -> True -- {-# SPECIALISE instance Eq (T Int) #-} is fine
730 InstDeclCtxt -> checkValidClsArgs (flexible_contexts || undecidable_ok) tys
731 -- Further checks on head and theta
732 -- in checkInstTermination
733 _ -> checkValidClsArgs flexible_contexts tys
734
735 -------------------------
736 okIPCtxt :: UserTypeCtxt -> Bool
737 -- See Note [Implicit parameters in instance decls]
738 okIPCtxt (FunSigCtxt {}) = True
739 okIPCtxt (InfSigCtxt {}) = True
740 okIPCtxt ExprSigCtxt = True
741 okIPCtxt PatSigCtxt = True
742 okIPCtxt ResSigCtxt = True
743 okIPCtxt GenSigCtxt = True
744 okIPCtxt (ConArgCtxt {}) = True
745 okIPCtxt (ForSigCtxt {}) = True -- ??
746 okIPCtxt ThBrackCtxt = True
747 okIPCtxt GhciCtxt = True
748 okIPCtxt SigmaCtxt = True
749 okIPCtxt (DataTyCtxt {}) = True
750
751 okIPCtxt (ClassSCCtxt {}) = False
752 okIPCtxt (InstDeclCtxt {}) = False
753 okIPCtxt (SpecInstCtxt {}) = False
754 okIPCtxt (TySynCtxt {}) = False
755 okIPCtxt (RuleSigCtxt {}) = False
756 okIPCtxt DefaultDeclCtxt = False
757
758 badIPPred :: PredType -> SDoc
759 badIPPred pred = ptext (sLit "Illegal implicit parameter") <+> quotes (ppr pred)
760
761 {-
762 Note [Kind polymorphic type classes]
763 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
764 MultiParam check:
765
766 class C f where... -- C :: forall k. k -> Constraint
767 instance C Maybe where...
768
769 The dictionary gets type [C * Maybe] even if it's not a MultiParam
770 type class.
771
772 Flexibility check:
773
774 class C f where... -- C :: forall k. k -> Constraint
775 data D a = D a
776 instance C D where
777
778 The dictionary gets type [C * (D *)]. IA0_TODO it should be
779 generalized actually.
780 -}
781
782 checkThetaCtxt :: UserTypeCtxt -> ThetaType -> SDoc
783 checkThetaCtxt ctxt theta
784 = vcat [ptext (sLit "In the context:") <+> pprTheta theta,
785 ptext (sLit "While checking") <+> pprUserTypeCtxt ctxt ]
786
787 eqPredTyErr, predTyVarErr, predTupleErr, predIrredErr, predSuperClassErr :: PredType -> SDoc
788 eqPredTyErr pred = vcat [ ptext (sLit "Illegal equational constraint") <+> pprType pred
789 , parens (ptext (sLit "Use GADTs or TypeFamilies to permit this")) ]
790 predTyVarErr pred = vcat [ hang (ptext (sLit "Non type-variable argument"))
791 2 (ptext (sLit "in the constraint:") <+> pprType pred)
792 , parens (ptext (sLit "Use FlexibleContexts to permit this")) ]
793 predTupleErr pred = hang (ptext (sLit "Illegal tuple constraint:") <+> pprType pred)
794 2 (parens constraintKindsMsg)
795 predIrredErr pred = hang (ptext (sLit "Illegal constraint:") <+> pprType pred)
796 2 (parens constraintKindsMsg)
797 predSuperClassErr pred
798 = hang (ptext (sLit "Illegal constraint") <+> quotes (pprType pred)
799 <+> ptext (sLit "in a superclass context"))
800 2 (parens undecidableMsg)
801
802 constraintSynErr :: Type -> SDoc
803 constraintSynErr kind = hang (ptext (sLit "Illegal constraint synonym of kind:") <+> quotes (ppr kind))
804 2 (parens constraintKindsMsg)
805
806 dupPredWarn :: [[PredType]] -> SDoc
807 dupPredWarn dups = ptext (sLit "Duplicate constraint(s):") <+> pprWithCommas pprType (map head dups)
808
809 arityErr :: Outputable a => String -> a -> Int -> Int -> SDoc
810 arityErr kind name n m
811 = hsep [ text kind, quotes (ppr name), ptext (sLit "should have"),
812 n_arguments <> comma, text "but has been given",
813 if m==0 then text "none" else int m]
814 where
815 n_arguments | n == 0 = ptext (sLit "no arguments")
816 | n == 1 = ptext (sLit "1 argument")
817 | True = hsep [int n, ptext (sLit "arguments")]
818
819 {-
820 ************************************************************************
821 * *
822 \subsection{Checking for a decent instance head type}
823 * *
824 ************************************************************************
825
826 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
827 it must normally look like: @instance Foo (Tycon a b c ...) ...@
828
829 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
830 flag is on, or (2)~the instance is imported (they must have been
831 compiled elsewhere). In these cases, we let them go through anyway.
832
833 We can also have instances for functions: @instance Foo (a -> b) ...@.
834 -}
835
836 checkValidInstHead :: UserTypeCtxt -> Class -> [Type] -> TcM ()
837 checkValidInstHead ctxt clas cls_args
838 = do { dflags <- getDynFlags
839
840 ; checkTc (clas `notElem` abstractClasses)
841 (instTypeErr clas cls_args abstract_class_msg)
842
843 -- Check language restrictions;
844 -- but not for SPECIALISE isntance pragmas
845 ; let ty_args = dropWhile isKind cls_args
846 ; unless spec_inst_prag $
847 do { checkTc (xopt Opt_TypeSynonymInstances dflags ||
848 all tcInstHeadTyNotSynonym ty_args)
849 (instTypeErr clas cls_args head_type_synonym_msg)
850 ; checkTc (xopt Opt_FlexibleInstances dflags ||
851 all tcInstHeadTyAppAllTyVars ty_args)
852 (instTypeErr clas cls_args head_type_args_tyvars_msg)
853 ; checkTc (xopt Opt_MultiParamTypeClasses dflags ||
854 length ty_args == 1 || -- Only count type arguments
855 (xopt Opt_NullaryTypeClasses dflags &&
856 null ty_args))
857 (instTypeErr clas cls_args head_one_type_msg) }
858
859 -- May not contain type family applications
860 ; mapM_ checkTyFamFreeness ty_args
861
862 ; mapM_ checkValidMonoType ty_args
863 -- For now, I only allow tau-types (not polytypes) in
864 -- the head of an instance decl.
865 -- E.g. instance C (forall a. a->a) is rejected
866 -- One could imagine generalising that, but I'm not sure
867 -- what all the consequences might be
868 }
869
870 where
871 spec_inst_prag = case ctxt of { SpecInstCtxt -> True; _ -> False }
872
873 head_type_synonym_msg = parens (
874 text "All instance types must be of the form (T t1 ... tn)" $$
875 text "where T is not a synonym." $$
876 text "Use TypeSynonymInstances if you want to disable this.")
877
878 head_type_args_tyvars_msg = parens (vcat [
879 text "All instance types must be of the form (T a1 ... an)",
880 text "where a1 ... an are *distinct type variables*,",
881 text "and each type variable appears at most once in the instance head.",
882 text "Use FlexibleInstances if you want to disable this."])
883
884 head_one_type_msg = parens (
885 text "Only one type can be given in an instance head." $$
886 text "Use MultiParamTypeClasses if you want to allow more, or zero.")
887
888 abstract_class_msg =
889 text "The class is abstract, manual instances are not permitted."
890
891 abstractClasses :: [ Class ]
892 abstractClasses = [ coercibleClass ] -- See Note [Coercible Instances]
893
894 instTypeErr :: Class -> [Type] -> SDoc -> SDoc
895 instTypeErr cls tys msg
896 = hang (hang (ptext (sLit "Illegal instance declaration for"))
897 2 (quotes (pprClassPred cls tys)))
898 2 msg
899
900 {-
901 validDeivPred checks for OK 'deriving' context. See Note [Exotic
902 derived instance contexts] in TcDeriv. However the predicate is
903 here because it uses sizeTypes, fvTypes.
904
905 Also check for a bizarre corner case, when the derived instance decl
906 would look like
907 instance C a b => D (T a) where ...
908 Note that 'b' isn't a parameter of T. This gives rise to all sorts of
909 problems; in particular, it's hard to compare solutions for equality
910 when finding the fixpoint, and that means the inferContext loop does
911 not converge. See Trac #5287.
912 -}
913
914 validDerivPred :: TyVarSet -> PredType -> Bool
915 validDerivPred tv_set pred
916 = case classifyPredType pred of
917 ClassPred _ tys -> check_tys tys
918 EqPred {} -> False -- reject equality constraints
919 _ -> True -- Non-class predicates are ok
920 where
921 check_tys tys = hasNoDups fvs
922 && sizeTypes tys == fromIntegral (length fvs)
923 && all (`elemVarSet` tv_set) fvs
924 fvs = fvType pred
925
926 {-
927 ************************************************************************
928 * *
929 \subsection{Checking instance for termination}
930 * *
931 ************************************************************************
932 -}
933
934 checkValidInstance :: UserTypeCtxt -> LHsType Name -> Type
935 -> TcM ([TyVar], ThetaType, Class, [Type])
936 checkValidInstance ctxt hs_type ty
937 | Just (clas,inst_tys) <- getClassPredTys_maybe tau
938 , inst_tys `lengthIs` classArity clas
939 = do { setSrcSpan head_loc (checkValidInstHead ctxt clas inst_tys)
940 ; checkValidTheta ctxt theta
941
942 -- The Termination and Coverate Conditions
943 -- Check that instance inference will terminate (if we care)
944 -- For Haskell 98 this will already have been done by checkValidTheta,
945 -- but as we may be using other extensions we need to check.
946 --
947 -- Note that the Termination Condition is *more conservative* than
948 -- the checkAmbiguity test we do on other type signatures
949 -- e.g. Bar a => Bar Int is ambiguous, but it also fails
950 -- the termination condition, because 'a' appears more often
951 -- in the constraint than in the head
952 ; undecidable_ok <- xoptM Opt_UndecidableInstances
953 ; if undecidable_ok
954 then checkAmbiguity ctxt ty
955 else checkInstTermination inst_tys theta
956
957 ; case (checkInstCoverage undecidable_ok clas theta inst_tys) of
958 IsValid -> return () -- Check succeeded
959 NotValid msg -> addErrTc (instTypeErr clas inst_tys msg)
960
961 ; return (tvs, theta, clas, inst_tys) }
962
963 | otherwise
964 = failWithTc (ptext (sLit "Malformed instance head:") <+> ppr tau)
965 where
966 (tvs, theta, tau) = tcSplitSigmaTy ty
967
968 -- The location of the "head" of the instance
969 head_loc = case hs_type of
970 L _ (HsForAllTy _ _ _ _ (L loc _)) -> loc
971 L loc _ -> loc
972
973 {-
974 Note [Paterson conditions]
975 ~~~~~~~~~~~~~~~~~~~~~~~~~~
976 Termination test: the so-called "Paterson conditions" (see Section 5 of
977 "Understanding functionsl dependencies via Constraint Handling Rules,
978 JFP Jan 2007).
979
980 We check that each assertion in the context satisfies:
981 (1) no variable has more occurrences in the assertion than in the head, and
982 (2) the assertion has fewer constructors and variables (taken together
983 and counting repetitions) than the head.
984 This is only needed with -fglasgow-exts, as Haskell 98 restrictions
985 (which have already been checked) guarantee termination.
986
987 The underlying idea is that
988
989 for any ground substitution, each assertion in the
990 context has fewer type constructors than the head.
991 -}
992
993 leafTyConKeys :: [Unique]
994 leafTyConKeys = [eqTyConKey, coercibleTyConKey, ipClassNameKey]
995
996 checkInstTermination :: [TcType] -> ThetaType -> TcM ()
997 -- See Note [Paterson conditions]
998 checkInstTermination tys theta
999 = check_preds theta
1000 where
1001 fvs = fvTypes tys
1002 size = sizeTypes tys
1003
1004 check_preds :: [PredType] -> TcM ()
1005 check_preds preds = mapM_ check preds
1006
1007 check :: PredType -> TcM ()
1008 check pred
1009 = case tcSplitTyConApp_maybe pred of
1010 Just (tc, tys)
1011 | getUnique tc `elem` leafTyConKeys
1012 -> return () -- You can't get from equalities or implicit
1013 -- params to class predicates, so this is safe
1014
1015 | isTupleTyCon tc
1016 -> check_preds tys
1017 -- Look inside tuple predicates; Trac #8359
1018
1019 _other -- All others: other ClassPreds, IrredPred
1020 | not (null bad_tvs) -> addErrTc (noMoreMsg bad_tvs what)
1021 | sizePred pred >= size -> addErrTc (smallerMsg what)
1022 | otherwise -> return ()
1023 where
1024 what = ptext (sLit "constraint") <+> quotes (ppr pred)
1025 bad_tvs = filterOut isKindVar (fvType pred \\ fvs)
1026 -- Rightly or wrongly, we only check for
1027 -- excessive occurrences of *type* variables.
1028 -- e.g. type instance Demote {T k} a = T (Demote {k} (Any {k}))
1029
1030 smallerMsg :: SDoc -> SDoc
1031 smallerMsg what
1032 = vcat [ hang (ptext (sLit "The") <+> what)
1033 2 (ptext (sLit "is no smaller than the instance head"))
1034 , parens undecidableMsg ]
1035
1036 noMoreMsg :: [TcTyVar] -> SDoc -> SDoc
1037 noMoreMsg tvs what
1038 = vcat [ hang (ptext (sLit "Variable") <> plural tvs <+> quotes (pprWithCommas ppr tvs)
1039 <+> occurs <+> ptext (sLit "more often"))
1040 2 (sep [ ptext (sLit "in the") <+> what
1041 , ptext (sLit "than in the instance head") ])
1042 , parens undecidableMsg ]
1043 where
1044 occurs = if isSingleton tvs then ptext (sLit "occurs")
1045 else ptext (sLit "occur")
1046
1047 undecidableMsg, constraintKindsMsg :: SDoc
1048 undecidableMsg = ptext (sLit "Use UndecidableInstances to permit this")
1049 constraintKindsMsg = ptext (sLit "Use ConstraintKinds to permit this")
1050
1051 {-
1052 Note [Associated type instances]
1053 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1054 We allow this:
1055 class C a where
1056 type T x a
1057 instance C Int where
1058 type T (S y) Int = y
1059 type T Z Int = Char
1060
1061 Note that
1062 a) The variable 'x' is not bound by the class decl
1063 b) 'x' is instantiated to a non-type-variable in the instance
1064 c) There are several type instance decls for T in the instance
1065
1066 All this is fine. Of course, you can't give any *more* instances
1067 for (T ty Int) elsewhere, because it's an *associated* type.
1068
1069 Note [Checking consistent instantiation]
1070 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1071 class C a b where
1072 type T a x b
1073
1074 instance C [p] Int
1075 type T [p] y Int = (p,y,y) -- Induces the family instance TyCon
1076 -- type TR p y = (p,y,y)
1077
1078 So we
1079 * Form the mini-envt from the class type variables a,b
1080 to the instance decl types [p],Int: [a->[p], b->Int]
1081
1082 * Look at the tyvars a,x,b of the type family constructor T
1083 (it shares tyvars with the class C)
1084
1085 * Apply the mini-evnt to them, and check that the result is
1086 consistent with the instance types [p] y Int
1087
1088 We do *not* assume (at this point) the the bound variables of
1089 the assoicated type instance decl are the same as for the parent
1090 instance decl. So, for example,
1091
1092 instance C [p] Int
1093 type T [q] y Int = ...
1094
1095 would work equally well. Reason: making the *kind* variables line
1096 up is much harder. Example (Trac #7282):
1097 class Foo (xs :: [k]) where
1098 type Bar xs :: *
1099
1100 instance Foo '[] where
1101 type Bar '[] = Int
1102 Here the instance decl really looks like
1103 instance Foo k ('[] k) where
1104 type Bar k ('[] k) = Int
1105 but the k's are not scoped, and hence won't match Uniques.
1106
1107 So instead we just match structure, with tcMatchTyX, and check
1108 that distinct type variables match 1-1 with distinct type variables.
1109
1110 HOWEVER, we *still* make the instance type variables scope over the
1111 type instances, to pick up non-obvious kinds. Eg
1112 class Foo (a :: k) where
1113 type F a
1114 instance Foo (b :: k -> k) where
1115 type F b = Int
1116 Here the instance is kind-indexed and really looks like
1117 type F (k->k) (b::k->k) = Int
1118 But if the 'b' didn't scope, we would make F's instance too
1119 poly-kinded.
1120 -}
1121
1122 checkConsistentFamInst
1123 :: Maybe ( Class
1124 , VarEnv Type ) -- ^ Class of associated type
1125 -- and instantiation of class TyVars
1126 -> TyCon -- ^ Family tycon
1127 -> [TyVar] -- ^ Type variables of the family instance
1128 -> [Type] -- ^ Type patterns from instance
1129 -> TcM ()
1130 -- See Note [Checking consistent instantiation]
1131
1132 checkConsistentFamInst Nothing _ _ _ = return ()
1133 checkConsistentFamInst (Just (clas, mini_env)) fam_tc at_tvs at_tys
1134 = do { -- Check that the associated type indeed comes from this class
1135 checkTc (Just clas == tyConAssoc_maybe fam_tc)
1136 (badATErr (className clas) (tyConName fam_tc))
1137
1138 -- See Note [Checking consistent instantiation] in TcTyClsDecls
1139 -- Check right to left, so that we spot type variable
1140 -- inconsistencies before (more confusing) kind variables
1141 ; discardResult $ foldrM check_arg emptyTvSubst $
1142 tyConTyVars fam_tc `zip` at_tys }
1143 where
1144 at_tv_set = mkVarSet at_tvs
1145
1146 check_arg :: (TyVar, Type) -> TvSubst -> TcM TvSubst
1147 check_arg (fam_tc_tv, at_ty) subst
1148 | Just inst_ty <- lookupVarEnv mini_env fam_tc_tv
1149 = case tcMatchTyX at_tv_set subst at_ty inst_ty of
1150 Just subst | all_distinct subst -> return subst
1151 _ -> failWithTc $ wrongATArgErr at_ty inst_ty
1152 -- No need to instantiate here, because the axiom
1153 -- uses the same type variables as the assocated class
1154 | otherwise
1155 = return subst -- Allow non-type-variable instantiation
1156 -- See Note [Associated type instances]
1157
1158 all_distinct :: TvSubst -> Bool
1159 -- True if all the variables mapped the substitution
1160 -- map to *distinct* type *variables*
1161 all_distinct subst = go [] at_tvs
1162 where
1163 go _ [] = True
1164 go acc (tv:tvs) = case lookupTyVar subst tv of
1165 Nothing -> go acc tvs
1166 Just ty | Just tv' <- tcGetTyVar_maybe ty
1167 , tv' `notElem` acc
1168 -> go (tv' : acc) tvs
1169 _other -> False
1170
1171 badATErr :: Name -> Name -> SDoc
1172 badATErr clas op
1173 = hsep [ptext (sLit "Class"), quotes (ppr clas),
1174 ptext (sLit "does not have an associated type"), quotes (ppr op)]
1175
1176 wrongATArgErr :: Type -> Type -> SDoc
1177 wrongATArgErr ty instTy =
1178 sep [ ptext (sLit "Type indexes must match class instance head")
1179 , ptext (sLit "Found") <+> quotes (ppr ty)
1180 <+> ptext (sLit "but expected") <+> quotes (ppr instTy)
1181 ]
1182
1183 {-
1184 ************************************************************************
1185 * *
1186 Checking type instance well-formedness and termination
1187 * *
1188 ************************************************************************
1189 -}
1190
1191 -- Check that a "type instance" is well-formed (which includes decidability
1192 -- unless -XUndecidableInstances is given).
1193 --
1194 checkValidTyFamInst :: Maybe ( Class, VarEnv Type )
1195 -> TyCon -> CoAxBranch -> TcM ()
1196 checkValidTyFamInst mb_clsinfo fam_tc
1197 (CoAxBranch { cab_tvs = tvs, cab_lhs = typats
1198 , cab_rhs = rhs, cab_loc = loc })
1199 = setSrcSpan loc $
1200 do { checkValidFamPats fam_tc tvs typats
1201
1202 -- The argument patterns, and RHS, are all boxed tau types
1203 -- E.g Reject type family F (a :: k1) :: k2
1204 -- type instance F (forall a. a->a) = ...
1205 -- type instance F Int# = ...
1206 -- type instance F Int = forall a. a->a
1207 -- type instance F Int = Int#
1208 -- See Trac #9357
1209 ; mapM_ checkValidMonoType typats
1210 ; checkValidMonoType rhs
1211
1212 -- We have a decidable instance unless otherwise permitted
1213 ; undecidable_ok <- xoptM Opt_UndecidableInstances
1214 ; unless undecidable_ok $
1215 mapM_ addErrTc (checkFamInstRhs typats (tcTyFamInsts rhs))
1216
1217 -- Check that type patterns match the class instance head
1218 ; checkConsistentFamInst mb_clsinfo fam_tc tvs typats }
1219
1220 -- Make sure that each type family application is
1221 -- (1) strictly smaller than the lhs,
1222 -- (2) mentions no type variable more often than the lhs, and
1223 -- (3) does not contain any further type family instances.
1224 --
1225 checkFamInstRhs :: [Type] -- lhs
1226 -> [(TyCon, [Type])] -- type family instances
1227 -> [MsgDoc]
1228 checkFamInstRhs lhsTys famInsts
1229 = mapMaybe check famInsts
1230 where
1231 size = sizeTypes lhsTys
1232 fvs = fvTypes lhsTys
1233 check (tc, tys)
1234 | not (all isTyFamFree tys) = Just (nestedMsg what)
1235 | not (null bad_tvs) = Just (noMoreMsg bad_tvs what)
1236 | size <= sizeTypes tys = Just (smallerMsg what)
1237 | otherwise = Nothing
1238 where
1239 what = ptext (sLit "type family application") <+> quotes (pprType (TyConApp tc tys))
1240 bad_tvs = filterOut isKindVar (fvTypes tys \\ fvs)
1241 -- Rightly or wrongly, we only check for
1242 -- excessive occurrences of *type* variables.
1243 -- e.g. type instance Demote {T k} a = T (Demote {k} (Any {k}))
1244
1245 checkValidFamPats :: TyCon -> [TyVar] -> [Type] -> TcM ()
1246 -- Patterns in a 'type instance' or 'data instance' decl should
1247 -- a) contain no type family applications
1248 -- (vanilla synonyms are fine, though)
1249 -- b) properly bind all their free type variables
1250 -- e.g. we disallow (Trac #7536)
1251 -- type T a = Int
1252 -- type instance F (T a) = a
1253 -- c) Have the right number of patterns
1254 checkValidFamPats fam_tc tvs ty_pats
1255 = ASSERT( length ty_pats == tyConArity fam_tc )
1256 -- A family instance must have exactly the same number of type
1257 -- parameters as the family declaration. You can't write
1258 -- type family F a :: * -> *
1259 -- type instance F Int y = y
1260 -- because then the type (F Int) would be like (\y.y)
1261 -- But this is checked at the time the axiom is created
1262 do { mapM_ checkTyFamFreeness ty_pats
1263 ; let unbound_tvs = filterOut (`elemVarSet` exactTyVarsOfTypes ty_pats) tvs
1264 ; checkTc (null unbound_tvs) (famPatErr fam_tc unbound_tvs ty_pats) }
1265
1266 -- Ensure that no type family instances occur in a type.
1267 checkTyFamFreeness :: Type -> TcM ()
1268 checkTyFamFreeness ty
1269 = checkTc (isTyFamFree ty) $
1270 tyFamInstIllegalErr ty
1271
1272 -- Check that a type does not contain any type family applications.
1273 --
1274 isTyFamFree :: Type -> Bool
1275 isTyFamFree = null . tcTyFamInsts
1276
1277 -- Error messages
1278
1279 tyFamInstIllegalErr :: Type -> SDoc
1280 tyFamInstIllegalErr ty
1281 = hang (ptext (sLit "Illegal type synonym family application in instance") <>
1282 colon) 2 $
1283 ppr ty
1284
1285 nestedMsg :: SDoc -> SDoc
1286 nestedMsg what
1287 = sep [ ptext (sLit "Illegal nested") <+> what
1288 , parens undecidableMsg ]
1289
1290 famPatErr :: TyCon -> [TyVar] -> [Type] -> SDoc
1291 famPatErr fam_tc tvs pats
1292 = hang (ptext (sLit "Family instance purports to bind type variable") <> plural tvs
1293 <+> pprQuotedList tvs)
1294 2 (hang (ptext (sLit "but the real LHS (expanding synonyms) is:"))
1295 2 (pprTypeApp fam_tc (map expandTypeSynonyms pats) <+> ptext (sLit "= ...")))
1296
1297 {-
1298 ************************************************************************
1299 * *
1300 \subsection{Auxiliary functions}
1301 * *
1302 ************************************************************************
1303 -}
1304
1305 -- Free variables of a type, retaining repetitions, and expanding synonyms
1306 fvType :: Type -> [TyVar]
1307 fvType ty | Just exp_ty <- tcView ty = fvType exp_ty
1308 fvType (TyVarTy tv) = [tv]
1309 fvType (TyConApp _ tys) = fvTypes tys
1310 fvType (LitTy {}) = []
1311 fvType (FunTy arg res) = fvType arg ++ fvType res
1312 fvType (AppTy fun arg) = fvType fun ++ fvType arg
1313 fvType (ForAllTy tyvar ty) = filter (/= tyvar) (fvType ty)
1314
1315 fvTypes :: [Type] -> [TyVar]
1316 fvTypes tys = concat (map fvType tys)
1317