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