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