Refactor validity checking for constraints
[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, TupleSections, ViewPatterns #-}
7
8 module TcValidity (
9 Rank, UserTypeCtxt(..), checkValidType, checkValidMonoType,
10 ContextKind(..), expectedKindInCtxt,
11 checkValidTheta, checkValidFamPats,
12 checkValidInstance, checkValidInstHead, validDerivPred,
13 checkTySynRhs,
14 ClsInstInfo, checkValidCoAxiom, checkValidCoAxBranch,
15 checkValidTyFamEqn,
16 arityErr, badATErr,
17 checkValidTelescope,
18 allDistinctTyVars
19 ) where
20
21 #include "HsVersions.h"
22
23 import GhcPrelude
24
25 import Maybes
26
27 -- friends:
28 import TcUnify ( tcSubType_NC )
29 import TcSimplify ( simplifyAmbiguityCheck )
30 import ClsInst ( matchGlobalInst, ClsInstResult(..), InstanceWhat(..) )
31 import TyCoRep
32 import TcType hiding ( sizeType, sizeTypes )
33 import PrelNames
34 import Type
35 import Coercion
36 import Kind
37 import CoAxiom
38 import Class
39 import TyCon
40
41 -- others:
42 import HsSyn -- HsType
43 import TcRnMonad -- TcType, amongst others
44 import TcEnv ( tcInitTidyEnv, tcInitOpenTidyEnv )
45 import FunDeps
46 import FamInstEnv ( isDominatedBy, injectiveBranches,
47 InjectivityCheckResult(..) )
48 import FamInst ( makeInjectivityErrors )
49 import Name
50 import VarEnv
51 import VarSet
52 import Id ( idType, idName )
53 import Var ( TyVarBndr(..), mkTyVar )
54 import ErrUtils
55 import DynFlags
56 import Util
57 import ListSetOps
58 import SrcLoc
59 import Outputable
60 import Module
61 import Unique ( mkAlphaTyVarUnique )
62 import qualified GHC.LanguageExtensions as LangExt
63
64 import Control.Monad
65 import Data.List ( (\\) )
66 import qualified Data.List.NonEmpty as NE
67
68 {-
69 ************************************************************************
70 * *
71 Checking for ambiguity
72 * *
73 ************************************************************************
74
75 Note [The ambiguity check for type signatures]
76 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
77 checkAmbiguity is a check on *user-supplied type signatures*. It is
78 *purely* there to report functions that cannot possibly be called. So for
79 example we want to reject:
80 f :: C a => Int
81 The idea is there can be no legal calls to 'f' because every call will
82 give rise to an ambiguous constraint. We could soundly omit the
83 ambiguity check on type signatures entirely, at the expense of
84 delaying ambiguity errors to call sites. Indeed, the flag
85 -XAllowAmbiguousTypes switches off the ambiguity check.
86
87 What about things like this:
88 class D a b | a -> b where ..
89 h :: D Int b => Int
90 The Int may well fix 'b' at the call site, so that signature should
91 not be rejected. Moreover, using *visible* fundeps is too
92 conservative. Consider
93 class X a b where ...
94 class D a b | a -> b where ...
95 instance D a b => X [a] b where...
96 h :: X a b => a -> a
97 Here h's type looks ambiguous in 'b', but here's a legal call:
98 ...(h [True])...
99 That gives rise to a (X [Bool] beta) constraint, and using the
100 instance means we need (D Bool beta) and that fixes 'beta' via D's
101 fundep!
102
103 Behind all these special cases there is a simple guiding principle.
104 Consider
105
106 f :: <type>
107 f = ...blah...
108
109 g :: <type>
110 g = f
111
112 You would think that the definition of g would surely typecheck!
113 After all f has exactly the same type, and g=f. But in fact f's type
114 is instantiated and the instantiated constraints are solved against
115 the originals, so in the case an ambiguous type it won't work.
116 Consider our earlier example f :: C a => Int. Then in g's definition,
117 we'll instantiate to (C alpha) and try to deduce (C alpha) from (C a),
118 and fail.
119
120 So in fact we use this as our *definition* of ambiguity. We use a
121 very similar test for *inferred* types, to ensure that they are
122 unambiguous. See Note [Impedance matching] in TcBinds.
123
124 This test is very conveniently implemented by calling
125 tcSubType <type> <type>
126 This neatly takes account of the functional dependecy stuff above,
127 and implicit parameter (see Note [Implicit parameters and ambiguity]).
128 And this is what checkAmbiguity does.
129
130 What about this, though?
131 g :: C [a] => Int
132 Is every call to 'g' ambiguous? After all, we might have
133 instance C [a] where ...
134 at the call site. So maybe that type is ok! Indeed even f's
135 quintessentially ambiguous type might, just possibly be callable:
136 with -XFlexibleInstances we could have
137 instance C a where ...
138 and now a call could be legal after all! Well, we'll reject this
139 unless the instance is available *here*.
140
141 Note [When to call checkAmbiguity]
142 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
143 We call checkAmbiguity
144 (a) on user-specified type signatures
145 (b) in checkValidType
146
147 Conncerning (b), you might wonder about nested foralls. What about
148 f :: forall b. (forall a. Eq a => b) -> b
149 The nested forall is ambiguous. Originally we called checkAmbiguity
150 in the forall case of check_type, but that had two bad consequences:
151 * We got two error messages about (Eq b) in a nested forall like this:
152 g :: forall a. Eq a => forall b. Eq b => a -> a
153 * If we try to check for ambiguity of a nested forall like
154 (forall a. Eq a => b), the implication constraint doesn't bind
155 all the skolems, which results in "No skolem info" in error
156 messages (see Trac #10432).
157
158 To avoid this, we call checkAmbiguity once, at the top, in checkValidType.
159 (I'm still a bit worried about unbound skolems when the type mentions
160 in-scope type variables.)
161
162 In fact, because of the co/contra-variance implemented in tcSubType,
163 this *does* catch function f above. too.
164
165 Concerning (a) the ambiguity check is only used for *user* types, not
166 for types coming from inteface files. The latter can legitimately
167 have ambiguous types. Example
168
169 class S a where s :: a -> (Int,Int)
170 instance S Char where s _ = (1,1)
171 f:: S a => [a] -> Int -> (Int,Int)
172 f (_::[a]) x = (a*x,b)
173 where (a,b) = s (undefined::a)
174
175 Here the worker for f gets the type
176 fw :: forall a. S a => Int -> (# Int, Int #)
177
178
179 Note [Implicit parameters and ambiguity]
180 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
181 Only a *class* predicate can give rise to ambiguity
182 An *implicit parameter* cannot. For example:
183 foo :: (?x :: [a]) => Int
184 foo = length ?x
185 is fine. The call site will supply a particular 'x'
186
187 Furthermore, the type variables fixed by an implicit parameter
188 propagate to the others. E.g.
189 foo :: (Show a, ?x::[a]) => Int
190 foo = show (?x++?x)
191 The type of foo looks ambiguous. But it isn't, because at a call site
192 we might have
193 let ?x = 5::Int in foo
194 and all is well. In effect, implicit parameters are, well, parameters,
195 so we can take their type variables into account as part of the
196 "tau-tvs" stuff. This is done in the function 'FunDeps.grow'.
197 -}
198
199 checkAmbiguity :: UserTypeCtxt -> Type -> TcM ()
200 checkAmbiguity ctxt ty
201 | wantAmbiguityCheck ctxt
202 = do { traceTc "Ambiguity check for" (ppr ty)
203 -- Solve the constraints eagerly because an ambiguous type
204 -- can cause a cascade of further errors. Since the free
205 -- tyvars are skolemised, we can safely use tcSimplifyTop
206 ; allow_ambiguous <- xoptM LangExt.AllowAmbiguousTypes
207 ; (_wrap, wanted) <- addErrCtxt (mk_msg allow_ambiguous) $
208 captureConstraints $
209 tcSubType_NC ctxt ty ty
210 ; simplifyAmbiguityCheck ty wanted
211
212 ; traceTc "Done ambiguity check for" (ppr ty) }
213
214 | otherwise
215 = return ()
216 where
217 mk_msg allow_ambiguous
218 = vcat [ text "In the ambiguity check for" <+> what
219 , ppUnless allow_ambiguous ambig_msg ]
220 ambig_msg = text "To defer the ambiguity check to use sites, enable AllowAmbiguousTypes"
221 what | Just n <- isSigMaybe ctxt = quotes (ppr n)
222 | otherwise = pprUserTypeCtxt ctxt
223
224 wantAmbiguityCheck :: UserTypeCtxt -> Bool
225 wantAmbiguityCheck ctxt
226 = case ctxt of -- See Note [When we don't check for ambiguity]
227 GhciCtxt -> False
228 TySynCtxt {} -> False
229 TypeAppCtxt -> False
230 _ -> True
231
232 checkUserTypeError :: Type -> TcM ()
233 -- Check to see if the type signature mentions "TypeError blah"
234 -- anywhere in it, and fail if so.
235 --
236 -- Very unsatisfactorily (Trac #11144) we need to tidy the type
237 -- because it may have come from an /inferred/ signature, not a
238 -- user-supplied one. This is really only a half-baked fix;
239 -- the other errors in checkValidType don't do tidying, and so
240 -- may give bad error messages when given an inferred type.
241 checkUserTypeError = check
242 where
243 check ty
244 | Just msg <- userTypeError_maybe ty = fail_with msg
245 | Just (_,ts) <- splitTyConApp_maybe ty = mapM_ check ts
246 | Just (t1,t2) <- splitAppTy_maybe ty = check t1 >> check t2
247 | Just (_,t1) <- splitForAllTy_maybe ty = check t1
248 | otherwise = return ()
249
250 fail_with msg = do { env0 <- tcInitTidyEnv
251 ; let (env1, tidy_msg) = tidyOpenType env0 msg
252 ; failWithTcM (env1, pprUserTypeErrorTy tidy_msg) }
253
254
255 {- Note [When we don't check for ambiguity]
256 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
257 In a few places we do not want to check a user-specified type for ambiguity
258
259 * GhciCtxt: Allow ambiguous types in GHCi's :kind command
260 E.g. type family T a :: * -- T :: forall k. k -> *
261 Then :k T should work in GHCi, not complain that
262 (T k) is ambiguous!
263
264 * TySynCtxt: type T a b = C a b => blah
265 It may be that when we /use/ T, we'll give an 'a' or 'b' that somehow
266 cure the ambiguity. So we defer the ambiguity check to the use site.
267
268 There is also an implementation reason (Trac #11608). In the RHS of
269 a type synonym we don't (currently) instantiate 'a' and 'b' with
270 TcTyVars before calling checkValidType, so we get asertion failures
271 from doing an ambiguity check on a type with TyVars in it. Fixing this
272 would not be hard, but let's wait till there's a reason.
273
274 * TypeAppCtxt: visible type application
275 f @ty
276 No need to check ty for ambiguity
277
278
279 ************************************************************************
280 * *
281 Checking validity of a user-defined type
282 * *
283 ************************************************************************
284
285 When dealing with a user-written type, we first translate it from an HsType
286 to a Type, performing kind checking, and then check various things that should
287 be true about it. We don't want to perform these checks at the same time
288 as the initial translation because (a) they are unnecessary for interface-file
289 types and (b) when checking a mutually recursive group of type and class decls,
290 we can't "look" at the tycons/classes yet. Also, the checks are rather
291 diverse, and used to really mess up the other code.
292
293 One thing we check for is 'rank'.
294
295 Rank 0: monotypes (no foralls)
296 Rank 1: foralls at the front only, Rank 0 inside
297 Rank 2: foralls at the front, Rank 1 on left of fn arrow,
298
299 basic ::= tyvar | T basic ... basic
300
301 r2 ::= forall tvs. cxt => r2a
302 r2a ::= r1 -> r2a | basic
303 r1 ::= forall tvs. cxt => r0
304 r0 ::= r0 -> r0 | basic
305
306 Another thing is to check that type synonyms are saturated.
307 This might not necessarily show up in kind checking.
308 type A i = i
309 data T k = MkT (k Int)
310 f :: T A -- BAD!
311 -}
312
313 checkValidType :: UserTypeCtxt -> Type -> TcM ()
314 -- Checks that a user-written type is valid for the given context
315 -- Assumes argument is fully zonked
316 -- Not used for instance decls; checkValidInstance instead
317 checkValidType ctxt ty
318 = do { traceTc "checkValidType" (ppr ty <+> text "::" <+> ppr (typeKind ty))
319 ; rankn_flag <- xoptM LangExt.RankNTypes
320 ; impred_flag <- xoptM LangExt.ImpredicativeTypes
321 ; let gen_rank :: Rank -> Rank
322 gen_rank r | rankn_flag = ArbitraryRank
323 | otherwise = r
324
325 rank1 = gen_rank r1
326 rank0 = gen_rank r0
327
328 r0 = rankZeroMonoType
329 r1 = LimitedRank True r0
330
331 rank
332 = case ctxt of
333 DefaultDeclCtxt-> MustBeMonoType
334 ResSigCtxt -> MustBeMonoType
335 PatSigCtxt -> rank0
336 RuleSigCtxt _ -> rank1
337 TySynCtxt _ -> rank0
338
339 ExprSigCtxt -> rank1
340 KindSigCtxt -> rank1
341 TypeAppCtxt | impred_flag -> ArbitraryRank
342 | otherwise -> tyConArgMonoType
343 -- Normally, ImpredicativeTypes is handled in check_arg_type,
344 -- but visible type applications don't go through there.
345 -- So we do this check here.
346
347 FunSigCtxt {} -> rank1
348 InfSigCtxt _ -> ArbitraryRank -- Inferred type
349 ConArgCtxt _ -> rank1 -- We are given the type of the entire
350 -- constructor, hence rank 1
351 PatSynCtxt _ -> rank1
352
353 ForSigCtxt _ -> rank1
354 SpecInstCtxt -> rank1
355 ThBrackCtxt -> rank1
356 GhciCtxt -> ArbitraryRank
357
358 TyVarBndrKindCtxt _ -> rank0
359 DataKindCtxt _ -> rank1
360 TySynKindCtxt _ -> rank1
361 TyFamResKindCtxt _ -> rank1
362
363 _ -> panic "checkValidType"
364 -- Can't happen; not used for *user* sigs
365
366 ; env <- tcInitOpenTidyEnv (tyCoVarsOfTypeList ty)
367
368 -- Check the internal validity of the type itself
369 ; check_type env ctxt rank ty
370
371 ; checkUserTypeError ty
372
373 -- Check for ambiguous types. See Note [When to call checkAmbiguity]
374 -- NB: this will happen even for monotypes, but that should be cheap;
375 -- and there may be nested foralls for the subtype test to examine
376 ; checkAmbiguity ctxt ty
377
378 ; traceTc "checkValidType done" (ppr ty <+> text "::" <+> ppr (typeKind ty)) }
379
380 checkValidMonoType :: Type -> TcM ()
381 -- Assumes argument is fully zonked
382 checkValidMonoType ty
383 = do { env <- tcInitOpenTidyEnv (tyCoVarsOfTypeList ty)
384 ; check_type env SigmaCtxt MustBeMonoType ty }
385
386 checkTySynRhs :: UserTypeCtxt -> TcType -> TcM ()
387 checkTySynRhs ctxt ty
388 | returnsConstraintKind actual_kind
389 = do { ck <- xoptM LangExt.ConstraintKinds
390 ; if ck
391 then when (isConstraintKind actual_kind)
392 (do { dflags <- getDynFlags
393 ; check_pred_ty emptyTidyEnv dflags ctxt ty })
394 else addErrTcM (constraintSynErr emptyTidyEnv actual_kind) }
395
396 | otherwise
397 = return ()
398 where
399 actual_kind = typeKind ty
400
401 -- | The kind expected in a certain context.
402 data ContextKind = TheKind Kind -- ^ a specific kind
403 | AnythingKind -- ^ any kind will do
404 | OpenKind -- ^ something of the form @TYPE _@
405
406 -- Depending on the context, we might accept any kind (for instance, in a TH
407 -- splice), or only certain kinds (like in type signatures).
408 expectedKindInCtxt :: UserTypeCtxt -> ContextKind
409 expectedKindInCtxt (TySynCtxt _) = AnythingKind
410 expectedKindInCtxt ThBrackCtxt = AnythingKind
411 expectedKindInCtxt GhciCtxt = AnythingKind
412 -- The types in a 'default' decl can have varying kinds
413 -- See Note [Extended defaults]" in TcEnv
414 expectedKindInCtxt DefaultDeclCtxt = AnythingKind
415 expectedKindInCtxt TypeAppCtxt = AnythingKind
416 expectedKindInCtxt (ForSigCtxt _) = TheKind liftedTypeKind
417 expectedKindInCtxt InstDeclCtxt = TheKind constraintKind
418 expectedKindInCtxt SpecInstCtxt = TheKind constraintKind
419 expectedKindInCtxt _ = OpenKind
420
421 {-
422 Note [Higher rank types]
423 ~~~~~~~~~~~~~~~~~~~~~~~~
424 Technically
425 Int -> forall a. a->a
426 is still a rank-1 type, but it's not Haskell 98 (Trac #5957). So the
427 validity checker allow a forall after an arrow only if we allow it
428 before -- that is, with Rank2Types or RankNTypes
429 -}
430
431 data Rank = ArbitraryRank -- Any rank ok
432
433 | LimitedRank -- Note [Higher rank types]
434 Bool -- Forall ok at top
435 Rank -- Use for function arguments
436
437 | MonoType SDoc -- Monotype, with a suggestion of how it could be a polytype
438
439 | MustBeMonoType -- Monotype regardless of flags
440
441
442 rankZeroMonoType, tyConArgMonoType, synArgMonoType, constraintMonoType :: Rank
443 rankZeroMonoType = MonoType (text "Perhaps you intended to use RankNTypes or Rank2Types")
444 tyConArgMonoType = MonoType (text "GHC doesn't yet support impredicative polymorphism")
445 synArgMonoType = MonoType (text "Perhaps you intended to use LiberalTypeSynonyms")
446 constraintMonoType = MonoType (vcat [ text "A constraint must be a monotype"
447 , text "Perhaps you intended to use QuantifiedConstraints" ])
448
449 funArgResRank :: Rank -> (Rank, Rank) -- Function argument and result
450 funArgResRank (LimitedRank _ arg_rank) = (arg_rank, LimitedRank (forAllAllowed arg_rank) arg_rank)
451 funArgResRank other_rank = (other_rank, other_rank)
452
453 forAllAllowed :: Rank -> Bool
454 forAllAllowed ArbitraryRank = True
455 forAllAllowed (LimitedRank forall_ok _) = forall_ok
456 forAllAllowed _ = False
457
458 ----------------------------------------
459 check_type :: TidyEnv -> UserTypeCtxt -> Rank -> Type -> TcM ()
460 -- The args say what the *type context* requires, independent
461 -- of *flag* settings. You test the flag settings at usage sites.
462 --
463 -- Rank is allowed rank for function args
464 -- Rank 0 means no for-alls anywhere
465
466 check_type env ctxt rank ty
467 | not (null tvbs && null theta)
468 = do { traceTc "check_type" (ppr ty $$ ppr (forAllAllowed rank))
469 ; checkTcM (forAllAllowed rank) (forAllTyErr env rank ty)
470 -- Reject e.g. (Maybe (?x::Int => Int)),
471 -- with a decent error message
472
473 ; check_valid_theta env' SigmaCtxt theta
474 -- Allow type T = ?x::Int => Int -> Int
475 -- but not type T = ?x::Int
476
477 ; check_type env' ctxt rank tau -- Allow foralls to right of arrow
478
479 ; checkTcM (not (any (`elemVarSet` tyCoVarsOfType phi_kind) tvs))
480 (forAllEscapeErr env' ty tau_kind)
481 }
482 where
483 (tvbs, phi) = tcSplitForAllTyVarBndrs ty
484 (theta, tau) = tcSplitPhiTy phi
485
486 tvs = binderVars tvbs
487 (env', _) = tidyTyCoVarBndrs env tvs
488
489 tau_kind = typeKind tau
490 phi_kind | null theta = tau_kind
491 | otherwise = liftedTypeKind
492 -- If there are any constraints, the kind is *. (#11405)
493
494 check_type _ _ _ (TyVarTy _) = return ()
495
496 check_type env ctxt rank (FunTy arg_ty res_ty)
497 = do { check_type env ctxt arg_rank arg_ty
498 ; check_type env ctxt res_rank res_ty }
499 where
500 (arg_rank, res_rank) = funArgResRank rank
501
502 check_type env ctxt rank (AppTy ty1 ty2)
503 = do { check_type env ctxt rank ty1
504 ; check_arg_type env ctxt rank ty2 }
505
506 check_type env ctxt rank ty@(TyConApp tc tys)
507 | isTypeSynonymTyCon tc || isTypeFamilyTyCon tc
508 = check_syn_tc_app env ctxt rank ty tc tys
509 | isUnboxedTupleTyCon tc = check_ubx_tuple env ctxt ty tys
510 | otherwise = mapM_ (check_arg_type env ctxt rank) tys
511
512 check_type _ _ _ (LitTy {}) = return ()
513
514 check_type env ctxt rank (CastTy ty _) = check_type env ctxt rank ty
515
516 check_type _ _ _ ty = pprPanic "check_type" (ppr ty)
517
518 ----------------------------------------
519 check_syn_tc_app :: TidyEnv -> UserTypeCtxt -> Rank -> KindOrType
520 -> TyCon -> [KindOrType] -> TcM ()
521 -- Used for type synonyms and type synonym families,
522 -- which must be saturated,
523 -- but not data families, which need not be saturated
524 check_syn_tc_app env ctxt rank ty tc tys
525 | tys `lengthAtLeast` tc_arity -- Saturated
526 -- Check that the synonym has enough args
527 -- This applies equally to open and closed synonyms
528 -- It's OK to have an *over-applied* type synonym
529 -- data Tree a b = ...
530 -- type Foo a = Tree [a]
531 -- f :: Foo a b -> ...
532 = do { -- See Note [Liberal type synonyms]
533 ; liberal <- xoptM LangExt.LiberalTypeSynonyms
534 ; if not liberal || isTypeFamilyTyCon tc then
535 -- For H98 and synonym families, do check the type args
536 mapM_ check_arg tys
537
538 else -- In the liberal case (only for closed syns), expand then check
539 case tcView ty of
540 Just ty' -> check_type env ctxt rank ty'
541 Nothing -> pprPanic "check_tau_type" (ppr ty) }
542
543 | GhciCtxt <- ctxt -- Accept under-saturated type synonyms in
544 -- GHCi :kind commands; see Trac #7586
545 = mapM_ check_arg tys
546
547 | otherwise
548 = failWithTc (tyConArityErr tc tys)
549 where
550 tc_arity = tyConArity tc
551 check_arg | isTypeFamilyTyCon tc = check_arg_type env ctxt rank
552 | otherwise = check_type env ctxt synArgMonoType
553
554 ----------------------------------------
555 check_ubx_tuple :: TidyEnv -> UserTypeCtxt -> KindOrType
556 -> [KindOrType] -> TcM ()
557 check_ubx_tuple env ctxt ty tys
558 = do { ub_tuples_allowed <- xoptM LangExt.UnboxedTuples
559 ; checkTcM ub_tuples_allowed (ubxArgTyErr env ty)
560
561 ; impred <- xoptM LangExt.ImpredicativeTypes
562 ; let rank' = if impred then ArbitraryRank else tyConArgMonoType
563 -- c.f. check_arg_type
564 -- However, args are allowed to be unlifted, or
565 -- more unboxed tuples, so can't use check_arg_ty
566 ; mapM_ (check_type env ctxt rank') tys }
567
568 ----------------------------------------
569 check_arg_type :: TidyEnv -> UserTypeCtxt -> Rank -> KindOrType -> TcM ()
570 -- The sort of type that can instantiate a type variable,
571 -- or be the argument of a type constructor.
572 -- Not an unboxed tuple, but now *can* be a forall (since impredicativity)
573 -- Other unboxed types are very occasionally allowed as type
574 -- arguments depending on the kind of the type constructor
575 --
576 -- For example, we want to reject things like:
577 --
578 -- instance Ord a => Ord (forall s. T s a)
579 -- and
580 -- g :: T s (forall b.b)
581 --
582 -- NB: unboxed tuples can have polymorphic or unboxed args.
583 -- This happens in the workers for functions returning
584 -- product types with polymorphic components.
585 -- But not in user code.
586 -- Anyway, they are dealt with by a special case in check_tau_type
587
588 check_arg_type _ _ _ (CoercionTy {}) = return ()
589
590 check_arg_type env ctxt rank ty
591 = do { impred <- xoptM LangExt.ImpredicativeTypes
592 ; let rank' = case rank of -- Predictive => must be monotype
593 MustBeMonoType -> MustBeMonoType -- Monotype, regardless
594 _other | impred -> ArbitraryRank
595 | otherwise -> tyConArgMonoType
596 -- Make sure that MustBeMonoType is propagated,
597 -- so that we don't suggest -XImpredicativeTypes in
598 -- (Ord (forall a.a)) => a -> a
599 -- and so that if it Must be a monotype, we check that it is!
600
601 ; check_type env ctxt rank' ty }
602
603 ----------------------------------------
604 forAllTyErr :: TidyEnv -> Rank -> Type -> (TidyEnv, SDoc)
605 forAllTyErr env rank ty
606 = ( env
607 , vcat [ hang herald 2 (ppr_tidy env ty)
608 , suggestion ] )
609 where
610 (tvs, _theta, _tau) = tcSplitSigmaTy ty
611 herald | null tvs = text "Illegal qualified type:"
612 | otherwise = text "Illegal polymorphic type:"
613 suggestion = case rank of
614 LimitedRank {} -> text "Perhaps you intended to use RankNTypes or Rank2Types"
615 MonoType d -> d
616 _ -> Outputable.empty -- Polytype is always illegal
617
618 forAllEscapeErr :: TidyEnv -> Type -> Kind -> (TidyEnv, SDoc)
619 forAllEscapeErr env ty tau_kind
620 = ( env
621 , hang (vcat [ text "Quantified type's kind mentions quantified type variable"
622 , text "(skolem escape)" ])
623 2 (vcat [ text " type:" <+> ppr_tidy env ty
624 , text "of kind:" <+> ppr_tidy env tau_kind ]) )
625
626 ubxArgTyErr :: TidyEnv -> Type -> (TidyEnv, SDoc)
627 ubxArgTyErr env ty
628 = ( env, vcat [ sep [ text "Illegal unboxed tuple type as function argument:"
629 , ppr_tidy env ty ]
630 , text "Perhaps you intended to use UnboxedTuples" ] )
631
632 {-
633 Note [Liberal type synonyms]
634 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
635 If -XLiberalTypeSynonyms is on, expand closed type synonyms *before*
636 doing validity checking. This allows us to instantiate a synonym defn
637 with a for-all type, or with a partially-applied type synonym.
638 e.g. type T a b = a
639 type S m = m ()
640 f :: S (T Int)
641 Here, T is partially applied, so it's illegal in H98. But if you
642 expand S first, then T we get just
643 f :: Int
644 which is fine.
645
646 IMPORTANT: suppose T is a type synonym. Then we must do validity
647 checking on an appliation (T ty1 ty2)
648
649 *either* before expansion (i.e. check ty1, ty2)
650 *or* after expansion (i.e. expand T ty1 ty2, and then check)
651 BUT NOT BOTH
652
653 If we do both, we get exponential behaviour!!
654
655 data TIACons1 i r c = c i ::: r c
656 type TIACons2 t x = TIACons1 t (TIACons1 t x)
657 type TIACons3 t x = TIACons2 t (TIACons1 t x)
658 type TIACons4 t x = TIACons2 t (TIACons2 t x)
659 type TIACons7 t x = TIACons4 t (TIACons3 t x)
660
661
662 ************************************************************************
663 * *
664 \subsection{Checking a theta or source type}
665 * *
666 ************************************************************************
667
668 Note [Implicit parameters in instance decls]
669 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
670 Implicit parameters _only_ allowed in type signatures; not in instance
671 decls, superclasses etc. The reason for not allowing implicit params in
672 instances is a bit subtle. If we allowed
673 instance (?x::Int, Eq a) => Foo [a] where ...
674 then when we saw
675 (e :: (?x::Int) => t)
676 it would be unclear how to discharge all the potential uses of the ?x
677 in e. For example, a constraint Foo [Int] might come out of e, and
678 applying the instance decl would show up two uses of ?x. Trac #8912.
679 -}
680
681 checkValidTheta :: UserTypeCtxt -> ThetaType -> TcM ()
682 -- Assumes argument is fully zonked
683 checkValidTheta ctxt theta
684 = addErrCtxtM (checkThetaCtxt ctxt theta) $
685 do { env <- tcInitOpenTidyEnv (tyCoVarsOfTypesList theta)
686 ; check_valid_theta env ctxt theta }
687
688 -------------------------
689 check_valid_theta :: TidyEnv -> UserTypeCtxt -> [PredType] -> TcM ()
690 check_valid_theta _ _ []
691 = return ()
692 check_valid_theta env ctxt theta
693 = do { dflags <- getDynFlags
694 ; warnTcM (Reason Opt_WarnDuplicateConstraints)
695 (wopt Opt_WarnDuplicateConstraints dflags && notNull dups)
696 (dupPredWarn env dups)
697 ; traceTc "check_valid_theta" (ppr theta)
698 ; mapM_ (check_pred_ty env dflags ctxt) theta }
699 where
700 (_,dups) = removeDups nonDetCmpType theta
701 -- It's OK to use nonDetCmpType because dups only appears in the
702 -- warning
703
704 -------------------------
705 {- Note [Validity checking for constraints]
706 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
707 We look through constraint synonyms so that we can see the underlying
708 constraint(s). For example
709 type Foo = ?x::Int
710 instance Foo => C T
711 We should reject the instance because it has an implicit parameter in
712 the context.
713
714 But we record, in 'under_syn', whether we have looked under a synonym
715 to avoid requiring language extensions at the use site. Main example
716 (Trac #9838):
717
718 {-# LANGUAGE ConstraintKinds #-}
719 module A where
720 type EqShow a = (Eq a, Show a)
721
722 module B where
723 import A
724 foo :: EqShow a => a -> String
725
726 We don't want to require ConstraintKinds in module B.
727 -}
728
729 check_pred_ty :: TidyEnv -> DynFlags -> UserTypeCtxt -> PredType -> TcM ()
730 -- Check the validity of a predicate in a signature
731 -- See Note [Validity checking for constraints]
732 check_pred_ty env dflags ctxt pred
733 = do { check_type env SigmaCtxt rank pred
734 ; check_pred_help False env dflags ctxt pred }
735 where
736 rank | xopt LangExt.QuantifiedConstraints dflags
737 = ArbitraryRank
738 | otherwise
739 = constraintMonoType
740
741 check_pred_help :: Bool -- True <=> under a type synonym
742 -> TidyEnv
743 -> DynFlags -> UserTypeCtxt
744 -> PredType -> TcM ()
745 check_pred_help under_syn env dflags ctxt pred
746 | Just pred' <- tcView pred -- Switch on under_syn when going under a
747 -- synonym (Trac #9838, yuk)
748 = check_pred_help True env dflags ctxt pred'
749
750 | otherwise -- A bit like classifyPredType, but not the same
751 -- E.g. we treat (~) like (~#); and we look inside tuples
752 = case classifyPredType pred of
753 ClassPred cls tys
754 | isCTupleClass cls -> check_tuple_pred under_syn env dflags ctxt pred tys
755 | otherwise -> check_class_pred env dflags ctxt pred cls tys
756
757 EqPred NomEq _ _ -> -- a ~# b
758 check_eq_pred env dflags pred
759
760 EqPred ReprEq _ _ -> -- Ugh! When inferring types we may get
761 -- f :: (a ~R# b) => blha
762 -- And we want to treat that like (Coercible a b)
763 -- We should probably check argument shapes, but we
764 -- didn't do so before, so I'm leaving it for now
765 return ()
766
767 ForAllPred _ theta head -> check_quant_pred env dflags pred theta head
768 IrredPred {} -> check_irred_pred under_syn env dflags ctxt pred
769
770 check_eq_pred :: TidyEnv -> DynFlags -> PredType -> TcM ()
771 check_eq_pred env dflags pred
772 = -- Equational constraints are valid in all contexts if type
773 -- families are permitted
774 checkTcM (xopt LangExt.TypeFamilies dflags
775 || xopt LangExt.GADTs dflags)
776 (eqPredTyErr env pred)
777
778 check_quant_pred :: TidyEnv -> DynFlags -> PredType
779 -> ThetaType -> PredType -> TcM ()
780 check_quant_pred env dflags pred theta head_pred
781 = addErrCtxt (text "In the quantified constraint"
782 <+> quotes (ppr pred)) $
783 do { checkTcM head_ok (badQuantHeadErr env pred)
784
785 ; unless (xopt LangExt.UndecidableInstances dflags) $
786 checkInstTermination theta head_pred
787 }
788 where
789 head_ok = case classifyPredType head_pred of
790 ClassPred {} -> True
791 IrredPred {} -> hasTyVarHead head_pred
792 _ -> False
793
794 check_tuple_pred :: Bool -> TidyEnv -> DynFlags -> UserTypeCtxt -> PredType -> [PredType] -> TcM ()
795 check_tuple_pred under_syn env dflags ctxt pred ts
796 = do { -- See Note [ConstraintKinds in predicates]
797 checkTcM (under_syn || xopt LangExt.ConstraintKinds dflags)
798 (predTupleErr env pred)
799 ; mapM_ (check_pred_help under_syn env dflags ctxt) ts }
800 -- This case will not normally be executed because without
801 -- -XConstraintKinds tuple types are only kind-checked as *
802
803 check_irred_pred :: Bool -> TidyEnv -> DynFlags -> UserTypeCtxt -> PredType -> TcM ()
804 check_irred_pred under_syn env dflags ctxt pred
805 -- The predicate looks like (X t1 t2) or (x t1 t2) :: Constraint
806 -- where X is a type function
807 = do { -- If it looks like (x t1 t2), require ConstraintKinds
808 -- see Note [ConstraintKinds in predicates]
809 -- But (X t1 t2) is always ok because we just require ConstraintKinds
810 -- at the definition site (Trac #9838)
811 failIfTcM (not under_syn && not (xopt LangExt.ConstraintKinds dflags)
812 && hasTyVarHead pred)
813 (predIrredErr env pred)
814
815 -- Make sure it is OK to have an irred pred in this context
816 -- See Note [Irreducible predicates in superclasses]
817 ; failIfTcM (is_superclass ctxt
818 && not (xopt LangExt.UndecidableInstances dflags)
819 && has_tyfun_head pred)
820 (predSuperClassErr env pred) }
821 where
822 is_superclass ctxt = case ctxt of { ClassSCCtxt _ -> True; _ -> False }
823 has_tyfun_head ty
824 = case tcSplitTyConApp_maybe ty of
825 Just (tc, _) -> isTypeFamilyTyCon tc
826 Nothing -> False
827
828 {- Note [ConstraintKinds in predicates]
829 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
830 Don't check for -XConstraintKinds under a type synonym, because that
831 was done at the type synonym definition site; see Trac #9838
832 e.g. module A where
833 type C a = (Eq a, Ix a) -- Needs -XConstraintKinds
834 module B where
835 import A
836 f :: C a => a -> a -- Does *not* need -XConstraintKinds
837
838 Note [Irreducible predicates in superclasses]
839 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
840 Allowing type-family calls in class superclasses is somewhat dangerous
841 because we can write:
842
843 type family Fooish x :: * -> Constraint
844 type instance Fooish () = Foo
845 class Fooish () a => Foo a where
846
847 This will cause the constraint simplifier to loop because every time we canonicalise a
848 (Foo a) class constraint we add a (Fooish () a) constraint which will be immediately
849 solved to add+canonicalise another (Foo a) constraint. -}
850
851 -------------------------
852 check_class_pred :: TidyEnv -> DynFlags -> UserTypeCtxt
853 -> PredType -> Class -> [TcType] -> TcM ()
854 check_class_pred env dflags ctxt pred cls tys
855 | cls `hasKey` heqTyConKey -- (~) and (~~) are classified as classes,
856 || cls `hasKey` eqTyConKey -- but here we want to treat them as equalities
857 = pprTrace "check_class" (ppr cls) $
858 check_eq_pred env dflags pred
859
860 | isIPClass cls
861 = do { check_arity
862 ; checkTcM (okIPCtxt ctxt) (badIPPred env pred) }
863
864 | otherwise -- Includes Coercible
865 = do { check_arity
866 ; checkSimplifiableClassConstraint env dflags ctxt cls tys
867 ; checkTcM arg_tys_ok (predTyVarErr env pred) }
868 where
869 check_arity = checkTc (tys `lengthIs` classArity cls)
870 (tyConArityErr (classTyCon cls) tys)
871
872 -- Check the arguments of a class constraint
873 flexible_contexts = xopt LangExt.FlexibleContexts dflags
874 undecidable_ok = xopt LangExt.UndecidableInstances dflags
875 arg_tys_ok = case ctxt of
876 SpecInstCtxt -> True -- {-# SPECIALISE instance Eq (T Int) #-} is fine
877 InstDeclCtxt -> checkValidClsArgs (flexible_contexts || undecidable_ok) cls tys
878 -- Further checks on head and theta
879 -- in checkInstTermination
880 _ -> checkValidClsArgs flexible_contexts cls tys
881
882 checkSimplifiableClassConstraint :: TidyEnv -> DynFlags -> UserTypeCtxt
883 -> Class -> [TcType] -> TcM ()
884 -- See Note [Simplifiable given constraints]
885 checkSimplifiableClassConstraint env dflags ctxt cls tys
886 | not (wopt Opt_WarnSimplifiableClassConstraints dflags)
887 = return ()
888 | xopt LangExt.MonoLocalBinds dflags
889 = return ()
890
891 | DataTyCtxt {} <- ctxt -- Don't do this check for the "stupid theta"
892 = return () -- of a data type declaration
893
894 | cls `hasKey` coercibleTyConKey
895 = return () -- Oddly, we treat (Coercible t1 t2) as unconditionally OK
896 -- matchGlobalInst will reply "yes" because we can reduce
897 -- (Coercible a b) to (a ~R# b)
898
899 | otherwise
900 = do { result <- matchGlobalInst dflags False cls tys
901 ; case result of
902 OneInst { cir_what = what }
903 -> addWarnTc (Reason Opt_WarnSimplifiableClassConstraints)
904 (simplifiable_constraint_warn what)
905 _ -> return () }
906 where
907 pred = mkClassPred cls tys
908
909 simplifiable_constraint_warn :: InstanceWhat -> SDoc
910 simplifiable_constraint_warn what
911 = vcat [ hang (text "The constraint" <+> quotes (ppr (tidyType env pred))
912 <+> text "matches")
913 2 (ppr_what what)
914 , hang (text "This makes type inference for inner bindings fragile;")
915 2 (text "either use MonoLocalBinds, or simplify it using the instance") ]
916
917 ppr_what BuiltinInstance = text "a built-in instance"
918 ppr_what LocalInstance = text "a locally-quantified instance"
919 ppr_what (TopLevInstance { iw_dfun_id = dfun })
920 = hang (text "instance" <+> pprSigmaType (idType dfun))
921 2 (text "--" <+> pprDefinedAt (idName dfun))
922
923
924 {- Note [Simplifiable given constraints]
925 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
926 A type signature like
927 f :: Eq [(a,b)] => a -> b
928 is very fragile, for reasons described at length in TcInteract
929 Note [Instance and Given overlap]. As that Note discusses, for the
930 most part the clever stuff in TcInteract means that we don't use a
931 top-level instance if a local Given might fire, so there is no
932 fragility. But if we /infer/ the type of a local let-binding, things
933 can go wrong (Trac #11948 is an example, discussed in the Note).
934
935 So this warning is switched on only if we have NoMonoLocalBinds; in
936 that case the warning discourages users from writing simplifiable
937 class constraints.
938
939 The warning only fires if the constraint in the signature
940 matches the top-level instances in only one way, and with no
941 unifiers -- that is, under the same circumstances that
942 TcInteract.matchInstEnv fires an interaction with the top
943 level instances. For example (Trac #13526), consider
944
945 instance {-# OVERLAPPABLE #-} Eq (T a) where ...
946 instance Eq (T Char) where ..
947 f :: Eq (T a) => ...
948
949 We don't want to complain about this, even though the context
950 (Eq (T a)) matches an instance, because the user may be
951 deliberately deferring the choice so that the Eq (T Char)
952 has a chance to fire when 'f' is called. And the fragility
953 only matters when there's a risk that the instance might
954 fire instead of the local 'given'; and there is no such
955 risk in this case. Just use the same rules as for instance
956 firing!
957 -}
958
959 -------------------------
960 okIPCtxt :: UserTypeCtxt -> Bool
961 -- See Note [Implicit parameters in instance decls]
962 okIPCtxt (FunSigCtxt {}) = True
963 okIPCtxt (InfSigCtxt {}) = True
964 okIPCtxt ExprSigCtxt = True
965 okIPCtxt TypeAppCtxt = True
966 okIPCtxt PatSigCtxt = True
967 okIPCtxt ResSigCtxt = True
968 okIPCtxt GenSigCtxt = True
969 okIPCtxt (ConArgCtxt {}) = True
970 okIPCtxt (ForSigCtxt {}) = True -- ??
971 okIPCtxt ThBrackCtxt = True
972 okIPCtxt GhciCtxt = True
973 okIPCtxt SigmaCtxt = True
974 okIPCtxt (DataTyCtxt {}) = True
975 okIPCtxt (PatSynCtxt {}) = True
976 okIPCtxt (TySynCtxt {}) = True -- e.g. type Blah = ?x::Int
977 -- Trac #11466
978
979 okIPCtxt (KindSigCtxt {}) = False
980 okIPCtxt (ClassSCCtxt {}) = False
981 okIPCtxt (InstDeclCtxt {}) = False
982 okIPCtxt (SpecInstCtxt {}) = False
983 okIPCtxt (RuleSigCtxt {}) = False
984 okIPCtxt DefaultDeclCtxt = False
985 okIPCtxt DerivClauseCtxt = False
986 okIPCtxt (TyVarBndrKindCtxt {}) = False
987 okIPCtxt (DataKindCtxt {}) = False
988 okIPCtxt (TySynKindCtxt {}) = False
989 okIPCtxt (TyFamResKindCtxt {}) = False
990
991 {-
992 Note [Kind polymorphic type classes]
993 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
994 MultiParam check:
995
996 class C f where... -- C :: forall k. k -> Constraint
997 instance C Maybe where...
998
999 The dictionary gets type [C * Maybe] even if it's not a MultiParam
1000 type class.
1001
1002 Flexibility check:
1003
1004 class C f where... -- C :: forall k. k -> Constraint
1005 data D a = D a
1006 instance C D where
1007
1008 The dictionary gets type [C * (D *)]. IA0_TODO it should be
1009 generalized actually.
1010 -}
1011
1012 checkThetaCtxt :: UserTypeCtxt -> ThetaType -> TidyEnv -> TcM (TidyEnv, SDoc)
1013 checkThetaCtxt ctxt theta env
1014 = return ( env
1015 , vcat [ text "In the context:" <+> pprTheta (tidyTypes env theta)
1016 , text "While checking" <+> pprUserTypeCtxt ctxt ] )
1017
1018 eqPredTyErr, predTupleErr, predIrredErr,
1019 predSuperClassErr, badQuantHeadErr :: TidyEnv -> PredType -> (TidyEnv, SDoc)
1020 badQuantHeadErr env pred
1021 = ( env
1022 , hang (text "Quantified predicate must have a class or type variable head:")
1023 2 (ppr_tidy env pred) )
1024 eqPredTyErr env pred
1025 = ( env
1026 , text "Illegal equational constraint" <+> ppr_tidy env pred $$
1027 parens (text "Use GADTs or TypeFamilies to permit this") )
1028 predTupleErr env pred
1029 = ( env
1030 , hang (text "Illegal tuple constraint:" <+> ppr_tidy env pred)
1031 2 (parens constraintKindsMsg) )
1032 predIrredErr env pred
1033 = ( env
1034 , hang (text "Illegal constraint:" <+> ppr_tidy env pred)
1035 2 (parens constraintKindsMsg) )
1036 predSuperClassErr env pred
1037 = ( env
1038 , hang (text "Illegal constraint" <+> quotes (ppr_tidy env pred)
1039 <+> text "in a superclass context")
1040 2 (parens undecidableMsg) )
1041
1042 predTyVarErr :: TidyEnv -> PredType -> (TidyEnv, SDoc)
1043 predTyVarErr env pred
1044 = (env
1045 , vcat [ hang (text "Non type-variable argument")
1046 2 (text "in the constraint:" <+> ppr_tidy env pred)
1047 , parens (text "Use FlexibleContexts to permit this") ])
1048
1049 badIPPred :: TidyEnv -> PredType -> (TidyEnv, SDoc)
1050 badIPPred env pred
1051 = ( env
1052 , text "Illegal implicit parameter" <+> quotes (ppr_tidy env pred) )
1053
1054 constraintSynErr :: TidyEnv -> Type -> (TidyEnv, SDoc)
1055 constraintSynErr env kind
1056 = ( env
1057 , hang (text "Illegal constraint synonym of kind:" <+> quotes (ppr_tidy env kind))
1058 2 (parens constraintKindsMsg) )
1059
1060 dupPredWarn :: TidyEnv -> [NE.NonEmpty PredType] -> (TidyEnv, SDoc)
1061 dupPredWarn env dups
1062 = ( env
1063 , text "Duplicate constraint" <> plural primaryDups <> text ":"
1064 <+> pprWithCommas (ppr_tidy env) primaryDups )
1065 where
1066 primaryDups = map NE.head dups
1067
1068 tyConArityErr :: TyCon -> [TcType] -> SDoc
1069 -- For type-constructor arity errors, be careful to report
1070 -- the number of /visible/ arguments required and supplied,
1071 -- ignoring the /invisible/ arguments, which the user does not see.
1072 -- (e.g. Trac #10516)
1073 tyConArityErr tc tks
1074 = arityErr (ppr (tyConFlavour tc)) (tyConName tc)
1075 tc_type_arity tc_type_args
1076 where
1077 vis_tks = filterOutInvisibleTypes tc tks
1078
1079 -- tc_type_arity = number of *type* args expected
1080 -- tc_type_args = number of *type* args encountered
1081 tc_type_arity = count isVisibleTyConBinder (tyConBinders tc)
1082 tc_type_args = length vis_tks
1083
1084 arityErr :: Outputable a => SDoc -> a -> Int -> Int -> SDoc
1085 arityErr what name n m
1086 = hsep [ text "The" <+> what, quotes (ppr name), text "should have",
1087 n_arguments <> comma, text "but has been given",
1088 if m==0 then text "none" else int m]
1089 where
1090 n_arguments | n == 0 = text "no arguments"
1091 | n == 1 = text "1 argument"
1092 | True = hsep [int n, text "arguments"]
1093
1094 {-
1095 ************************************************************************
1096 * *
1097 \subsection{Checking for a decent instance head type}
1098 * *
1099 ************************************************************************
1100
1101 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1102 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1103
1104 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1105 flag is on, or (2)~the instance is imported (they must have been
1106 compiled elsewhere). In these cases, we let them go through anyway.
1107
1108 We can also have instances for functions: @instance Foo (a -> b) ...@.
1109 -}
1110
1111 checkValidInstHead :: UserTypeCtxt -> Class -> [Type] -> TcM ()
1112 checkValidInstHead ctxt clas cls_args
1113 = do { dflags <- getDynFlags
1114
1115 ; mod <- getModule
1116 ; checkTc (getUnique clas `notElem` abstractClassKeys ||
1117 nameModule (getName clas) == mod)
1118 (instTypeErr clas cls_args abstract_class_msg)
1119
1120 ; when (clas `hasKey` hasFieldClassNameKey) $
1121 checkHasFieldInst clas cls_args
1122
1123 -- Check language restrictions;
1124 -- but not for SPECIALISE instance pragmas or deriving clauses
1125 ; let ty_args = filterOutInvisibleTypes (classTyCon clas) cls_args
1126 ; unless (spec_inst_prag || deriv_clause) $
1127 do { checkTc (xopt LangExt.TypeSynonymInstances dflags ||
1128 all tcInstHeadTyNotSynonym ty_args)
1129 (instTypeErr clas cls_args head_type_synonym_msg)
1130 ; checkTc (xopt LangExt.FlexibleInstances dflags ||
1131 all tcInstHeadTyAppAllTyVars ty_args)
1132 (instTypeErr clas cls_args head_type_args_tyvars_msg)
1133 ; checkTc (xopt LangExt.MultiParamTypeClasses dflags ||
1134 lengthIs ty_args 1 || -- Only count type arguments
1135 (xopt LangExt.NullaryTypeClasses dflags &&
1136 null ty_args))
1137 (instTypeErr clas cls_args head_one_type_msg) }
1138
1139 ; mapM_ checkValidTypePat ty_args }
1140 where
1141 spec_inst_prag = case ctxt of { SpecInstCtxt -> True; _ -> False }
1142 deriv_clause = case ctxt of { DerivClauseCtxt -> True; _ -> False }
1143
1144 head_type_synonym_msg = parens (
1145 text "All instance types must be of the form (T t1 ... tn)" $$
1146 text "where T is not a synonym." $$
1147 text "Use TypeSynonymInstances if you want to disable this.")
1148
1149 head_type_args_tyvars_msg = parens (vcat [
1150 text "All instance types must be of the form (T a1 ... an)",
1151 text "where a1 ... an are *distinct type variables*,",
1152 text "and each type variable appears at most once in the instance head.",
1153 text "Use FlexibleInstances if you want to disable this."])
1154
1155 head_one_type_msg = parens (
1156 text "Only one type can be given in an instance head." $$
1157 text "Use MultiParamTypeClasses if you want to allow more, or zero.")
1158
1159 abstract_class_msg =
1160 text "Manual instances of this class are not permitted."
1161
1162 tcInstHeadTyNotSynonym :: Type -> Bool
1163 -- Used in Haskell-98 mode, for the argument types of an instance head
1164 -- These must not be type synonyms, but everywhere else type synonyms
1165 -- are transparent, so we need a special function here
1166 tcInstHeadTyNotSynonym ty
1167 = case ty of -- Do not use splitTyConApp,
1168 -- because that expands synonyms!
1169 TyConApp tc _ -> not (isTypeSynonymTyCon tc)
1170 _ -> True
1171
1172 tcInstHeadTyAppAllTyVars :: Type -> Bool
1173 -- Used in Haskell-98 mode, for the argument types of an instance head
1174 -- These must be a constructor applied to type variable arguments
1175 -- or a type-level literal.
1176 -- But we allow kind instantiations.
1177 tcInstHeadTyAppAllTyVars ty
1178 | Just (tc, tys) <- tcSplitTyConApp_maybe (dropCasts ty)
1179 = ok (filterOutInvisibleTypes tc tys) -- avoid kinds
1180 | LitTy _ <- ty = True -- accept type literals (Trac #13833)
1181 | otherwise
1182 = False
1183 where
1184 -- Check that all the types are type variables,
1185 -- and that each is distinct
1186 ok tys = equalLength tvs tys && hasNoDups tvs
1187 where
1188 tvs = mapMaybe tcGetTyVar_maybe tys
1189
1190 dropCasts :: Type -> Type
1191 -- See Note [Casts during validity checking]
1192 -- This function can turn a well-kinded type into an ill-kinded
1193 -- one, so I've kept it local to this module
1194 -- To consider: drop only HoleCo casts
1195 dropCasts (CastTy ty _) = dropCasts ty
1196 dropCasts (AppTy t1 t2) = mkAppTy (dropCasts t1) (dropCasts t2)
1197 dropCasts (FunTy t1 t2) = mkFunTy (dropCasts t1) (dropCasts t2)
1198 dropCasts (TyConApp tc tys) = mkTyConApp tc (map dropCasts tys)
1199 dropCasts (ForAllTy b ty) = ForAllTy (dropCastsB b) (dropCasts ty)
1200 dropCasts ty = ty -- LitTy, TyVarTy, CoercionTy
1201
1202 dropCastsB :: TyVarBinder -> TyVarBinder
1203 dropCastsB b = b -- Don't bother in the kind of a forall
1204
1205 abstractClassKeys :: [Unique]
1206 abstractClassKeys = [ heqTyConKey
1207 , eqTyConKey
1208 , coercibleTyConKey
1209 ] -- See Note [Equality class instances]
1210
1211 instTypeErr :: Class -> [Type] -> SDoc -> SDoc
1212 instTypeErr cls tys msg
1213 = hang (hang (text "Illegal instance declaration for")
1214 2 (quotes (pprClassPred cls tys)))
1215 2 msg
1216
1217 -- | See Note [Validity checking of HasField instances]
1218 checkHasFieldInst :: Class -> [Type] -> TcM ()
1219 checkHasFieldInst cls tys@[_k_ty, x_ty, r_ty, _a_ty] =
1220 case splitTyConApp_maybe r_ty of
1221 Nothing -> whoops (text "Record data type must be specified")
1222 Just (tc, _)
1223 | isFamilyTyCon tc
1224 -> whoops (text "Record data type may not be a data family")
1225 | otherwise -> case isStrLitTy x_ty of
1226 Just lbl
1227 | isJust (lookupTyConFieldLabel lbl tc)
1228 -> whoops (ppr tc <+> text "already has a field"
1229 <+> quotes (ppr lbl))
1230 | otherwise -> return ()
1231 Nothing
1232 | null (tyConFieldLabels tc) -> return ()
1233 | otherwise -> whoops (ppr tc <+> text "has fields")
1234 where
1235 whoops = addErrTc . instTypeErr cls tys
1236 checkHasFieldInst _ tys = pprPanic "checkHasFieldInst" (ppr tys)
1237
1238 {- Note [Casts during validity checking]
1239 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1240 Consider the (bogus)
1241 instance Eq Char#
1242 We elaborate to 'Eq (Char# |> UnivCo(hole))' where the hole is an
1243 insoluble equality constraint for * ~ #. We'll report the insoluble
1244 constraint separately, but we don't want to *also* complain that Eq is
1245 not applied to a type constructor. So we look gaily look through
1246 CastTys here.
1247
1248 Another example: Eq (Either a). Then we actually get a cast in
1249 the middle:
1250 Eq ((Either |> g) a)
1251
1252
1253 Note [Validity checking of HasField instances]
1254 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1255 The HasField class has magic constraint solving behaviour (see Note
1256 [HasField instances] in TcInteract). However, we permit users to
1257 declare their own instances, provided they do not clash with the
1258 built-in behaviour. In particular, we forbid:
1259
1260 1. `HasField _ r _` where r is a variable
1261
1262 2. `HasField _ (T ...) _` if T is a data family
1263 (because it might have fields introduced later)
1264
1265 3. `HasField x (T ...) _` where x is a variable,
1266 if T has any fields at all
1267
1268 4. `HasField "foo" (T ...) _` if T has a "foo" field
1269
1270 The usual functional dependency checks also apply.
1271
1272
1273 Note [Valid 'deriving' predicate]
1274 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1275 validDerivPred checks for OK 'deriving' context. See Note [Exotic
1276 derived instance contexts] in TcDeriv. However the predicate is
1277 here because it uses sizeTypes, fvTypes.
1278
1279 It checks for three things
1280
1281 * No repeated variables (hasNoDups fvs)
1282
1283 * No type constructors. This is done by comparing
1284 sizeTypes tys == length (fvTypes tys)
1285 sizeTypes counts variables and constructors; fvTypes returns variables.
1286 So if they are the same, there must be no constructors. But there
1287 might be applications thus (f (g x)).
1288
1289 Note that tys only includes the visible arguments of the class type
1290 constructor. Including the non-visible arguments can cause the following,
1291 perfectly valid instance to be rejected:
1292 class Category (cat :: k -> k -> *) where ...
1293 newtype T (c :: * -> * -> *) a b = MkT (c a b)
1294 instance Category c => Category (T c) where ...
1295 since the first argument to Category is a non-visible *, which sizeTypes
1296 would count as a constructor! See Trac #11833.
1297
1298 * Also check for a bizarre corner case, when the derived instance decl
1299 would look like
1300 instance C a b => D (T a) where ...
1301 Note that 'b' isn't a parameter of T. This gives rise to all sorts of
1302 problems; in particular, it's hard to compare solutions for equality
1303 when finding the fixpoint, and that means the inferContext loop does
1304 not converge. See Trac #5287.
1305
1306 Note [Equality class instances]
1307 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1308 We can't have users writing instances for the equality classes. But we
1309 still need to be able to write instances for them ourselves. So we allow
1310 instances only in the defining module.
1311
1312 -}
1313
1314 validDerivPred :: TyVarSet -> PredType -> Bool
1315 -- See Note [Valid 'deriving' predicate]
1316 validDerivPred tv_set pred
1317 = case classifyPredType pred of
1318 ClassPred cls tys -> cls `hasKey` typeableClassKey
1319 -- Typeable constraints are bigger than they appear due
1320 -- to kind polymorphism, but that's OK
1321 || check_tys cls tys
1322 EqPred {} -> False -- reject equality constraints
1323 _ -> True -- Non-class predicates are ok
1324 where
1325 check_tys cls tys
1326 = hasNoDups fvs
1327 -- use sizePred to ignore implicit args
1328 && lengthIs fvs (sizePred pred)
1329 && all (`elemVarSet` tv_set) fvs
1330 where tys' = filterOutInvisibleTypes (classTyCon cls) tys
1331 fvs = fvTypes tys'
1332
1333 {-
1334 ************************************************************************
1335 * *
1336 \subsection{Checking instance for termination}
1337 * *
1338 ************************************************************************
1339 -}
1340
1341 {- Note [Instances and constraint synonyms]
1342 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1343 Currently, we don't allow instances for constraint synonyms at all.
1344 Consider these (Trac #13267):
1345 type C1 a = Show (a -> Bool)
1346 instance C1 Int where -- I1
1347 show _ = "ur"
1348
1349 This elicits "show is not a (visible) method of class C1", which isn't
1350 a great message. But it comes from the renamer, so it's hard to improve.
1351
1352 This needs a bit more care:
1353 type C2 a = (Show a, Show Int)
1354 instance C2 Int -- I2
1355
1356 If we use (splitTyConApp_maybe tau) in checkValidInstance to decompose
1357 the instance head, we'll expand the synonym on fly, and it'll look like
1358 instance (%,%) (Show Int, Show Int)
1359 and we /really/ don't want that. So we carefully do /not/ expand
1360 synonyms, by matching on TyConApp directly.
1361 -}
1362
1363 checkValidInstance :: UserTypeCtxt -> LHsSigType GhcRn -> Type
1364 -> TcM ([TyVar], ThetaType, Class, [Type])
1365 checkValidInstance ctxt hs_type ty
1366 | not is_tc_app
1367 = failWithTc (text "Instance head is not headed by a class")
1368
1369 | isNothing mb_cls
1370 = failWithTc (vcat [ text "Illegal instance for a" <+> ppr (tyConFlavour tc)
1371 , text "A class instance must be for a class" ])
1372
1373 | not arity_ok
1374 = failWithTc (text "Arity mis-match in instance head")
1375
1376 | otherwise
1377 = do { setSrcSpan head_loc (checkValidInstHead ctxt clas inst_tys)
1378 ; traceTc "checkValidInstance {" (ppr ty)
1379
1380 ; env0 <- tcInitTidyEnv
1381 ; check_valid_theta env0 ctxt theta
1382
1383 -- The Termination and Coverate Conditions
1384 -- Check that instance inference will terminate (if we care)
1385 -- For Haskell 98 this will already have been done by checkValidTheta,
1386 -- but as we may be using other extensions we need to check.
1387 --
1388 -- Note that the Termination Condition is *more conservative* than
1389 -- the checkAmbiguity test we do on other type signatures
1390 -- e.g. Bar a => Bar Int is ambiguous, but it also fails
1391 -- the termination condition, because 'a' appears more often
1392 -- in the constraint than in the head
1393 ; undecidable_ok <- xoptM LangExt.UndecidableInstances
1394 ; if undecidable_ok
1395 then checkAmbiguity ctxt ty
1396 else checkInstTermination theta tau
1397
1398 ; traceTc "cvi 2" (ppr ty)
1399
1400 ; case (checkInstCoverage undecidable_ok clas theta inst_tys) of
1401 IsValid -> return () -- Check succeeded
1402 NotValid msg -> addErrTc (instTypeErr clas inst_tys msg)
1403
1404 ; traceTc "End checkValidInstance }" empty
1405
1406 ; return (tvs, theta, clas, inst_tys) }
1407 where
1408 (tvs, theta, tau) = tcSplitSigmaTy ty
1409 is_tc_app = case tau of { TyConApp {} -> True; _ -> False }
1410 TyConApp tc inst_tys = tau -- See Note [Instances and constraint synonyms]
1411 mb_cls = tyConClass_maybe tc
1412 Just clas = mb_cls
1413 arity_ok = inst_tys `lengthIs` classArity clas
1414
1415 -- The location of the "head" of the instance
1416 head_loc = getLoc (getLHsInstDeclHead hs_type)
1417
1418 {-
1419 Note [Paterson conditions]
1420 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1421 Termination test: the so-called "Paterson conditions" (see Section 5 of
1422 "Understanding functional dependencies via Constraint Handling Rules,
1423 JFP Jan 2007).
1424
1425 We check that each assertion in the context satisfies:
1426 (1) no variable has more occurrences in the assertion than in the head, and
1427 (2) the assertion has fewer constructors and variables (taken together
1428 and counting repetitions) than the head.
1429 This is only needed with -fglasgow-exts, as Haskell 98 restrictions
1430 (which have already been checked) guarantee termination.
1431
1432 The underlying idea is that
1433
1434 for any ground substitution, each assertion in the
1435 context has fewer type constructors than the head.
1436 -}
1437
1438 checkInstTermination :: ThetaType -> TcPredType -> TcM ()
1439 -- See Note [Paterson conditions]
1440 checkInstTermination theta head_pred
1441 = check_preds emptyVarSet theta
1442 where
1443 head_fvs = fvType head_pred
1444 head_size = sizeType head_pred
1445
1446 check_preds :: VarSet -> [PredType] -> TcM ()
1447 check_preds foralld_tvs preds = mapM_ (check foralld_tvs) preds
1448
1449 check :: VarSet -> PredType -> TcM ()
1450 check foralld_tvs pred
1451 = case classifyPredType pred of
1452 EqPred {} -> return () -- See Trac #4200.
1453 IrredPred {} -> check2 foralld_tvs pred (sizeType pred)
1454 ClassPred cls tys
1455 | isTerminatingClass cls
1456 -> return ()
1457
1458 | isCTupleClass cls -- Look inside tuple predicates; Trac #8359
1459 -> check_preds foralld_tvs tys
1460
1461 | otherwise -- Other ClassPreds
1462 -> check2 foralld_tvs pred bogus_size
1463 where
1464 bogus_size = 1 + sizeTypes (filterOutInvisibleTypes (classTyCon cls) tys)
1465 -- See Note [Invisible arguments and termination]
1466
1467 ForAllPred tvs _ head_pred'
1468 -> check (foralld_tvs `extendVarSetList` binderVars tvs) head_pred'
1469 -- Termination of the quantified predicate itself is checked
1470 -- when the predicates are individually checked for validity
1471
1472 check2 foralld_tvs pred pred_size
1473 | not (null bad_tvs) = failWithTc (noMoreMsg bad_tvs what (ppr head_pred))
1474 | not (isTyFamFree pred) = failWithTc (nestedMsg what)
1475 | pred_size >= head_size = failWithTc (smallerMsg what (ppr head_pred))
1476 | otherwise = return ()
1477 -- isTyFamFree: see Note [Type families in instance contexts]
1478 where
1479 what = text "constraint" <+> quotes (ppr pred)
1480 bad_tvs = filterOut (`elemVarSet` foralld_tvs) (fvType pred)
1481 \\ head_fvs
1482
1483 smallerMsg :: SDoc -> SDoc -> SDoc
1484 smallerMsg what inst_head
1485 = vcat [ hang (text "The" <+> what)
1486 2 (sep [ text "is no smaller than"
1487 , text "the instance head" <+> quotes inst_head ])
1488 , parens undecidableMsg ]
1489
1490 noMoreMsg :: [TcTyVar] -> SDoc -> SDoc -> SDoc
1491 noMoreMsg tvs what inst_head
1492 = vcat [ hang (text "Variable" <> plural tvs <+> quotes (pprWithCommas ppr tvs)
1493 <+> occurs <+> text "more often")
1494 2 (sep [ text "in the" <+> what
1495 , text "than in the instance head" <+> quotes inst_head ])
1496 , parens undecidableMsg ]
1497 where
1498 occurs = if isSingleton tvs then text "occurs"
1499 else text "occur"
1500
1501 undecidableMsg, constraintKindsMsg :: SDoc
1502 undecidableMsg = text "Use UndecidableInstances to permit this"
1503 constraintKindsMsg = text "Use ConstraintKinds to permit this"
1504
1505 {- Note [Type families in instance contexts]
1506 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1507 Are these OK?
1508 type family F a
1509 instance F a => C (Maybe [a]) where ...
1510 intance C (F a) => C [[[a]]] where ...
1511
1512 No: the type family in the instance head might blow up to an
1513 arbitrarily large type, depending on how 'a' is instantiated.
1514 So we require UndecidableInstances if we have a type family
1515 in the instance head. Trac #15172.
1516
1517 Note [Associated type instances]
1518 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1519 We allow this:
1520 class C a where
1521 type T x a
1522 instance C Int where
1523 type T (S y) Int = y
1524 type T Z Int = Char
1525
1526 Note that
1527 a) The variable 'x' is not bound by the class decl
1528 b) 'x' is instantiated to a non-type-variable in the instance
1529 c) There are several type instance decls for T in the instance
1530
1531 All this is fine. Of course, you can't give any *more* instances
1532 for (T ty Int) elsewhere, because it's an *associated* type.
1533
1534 Note [Checking consistent instantiation]
1535 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1536 See Trac #11450 for background discussion on this check.
1537
1538 class C a b where
1539 type T a x b
1540
1541 With this class decl, if we have an instance decl
1542 instance C ty1 ty2 where ...
1543 then the type instance must look like
1544 type T ty1 v ty2 = ...
1545 with exactly 'ty1' for 'a', 'ty2' for 'b', and some type 'v' for 'x'.
1546 For example:
1547
1548 instance C [p] Int
1549 type T [p] y Int = (p,y,y)
1550
1551 Note that
1552
1553 * We used to allow completely different bound variables in the
1554 associated type instance; e.g.
1555 instance C [p] Int
1556 type T [q] y Int = ...
1557 But from GHC 8.2 onwards, we don't. It's much simpler this way.
1558 See Trac #11450.
1559
1560 * When the class variable isn't used on the RHS of the type instance,
1561 it's tempting to allow wildcards, thus
1562 instance C [p] Int
1563 type T [_] y Int = (y,y)
1564 But it's awkward to do the test, and it doesn't work if the
1565 variable is repeated:
1566 instance C (p,p) Int
1567 type T (_,_) y Int = (y,y)
1568 Even though 'p' is not used on the RHS, we still need to use 'p'
1569 on the LHS to establish the repeated pattern. So to keep it simple
1570 we just require equality.
1571
1572 * For variables in associated type families that are not bound by the class
1573 itself, we do _not_ check if they are over-specific. In other words,
1574 it's perfectly acceptable to have an instance like this:
1575
1576 instance C [p] Int where
1577 type T [p] (Maybe x) Int = x
1578
1579 While the first and third arguments to T are required to be exactly [p] and
1580 Int, respectively, since they are bound by C, the second argument is allowed
1581 to be more specific than just a type variable. Furthermore, it is permissible
1582 to define multiple equations for T that differ only in the non-class-bound
1583 argument:
1584
1585 instance C [p] Int where
1586 type T [p] (Maybe x) Int = x
1587 type T [p] (Either x y) Int = x -> y
1588
1589 We once considered requiring that non-class-bound variables in associated
1590 type family instances be instantiated with distinct type variables. However,
1591 that requirement proved too restrictive in practice, as there were examples
1592 of extremely simple associated type family instances that this check would
1593 reject, and fixing them required tiresome boilerplate in the form of
1594 auxiliary type families. For instance, you would have to define the above
1595 example as:
1596
1597 instance C [p] Int where
1598 type T [p] x Int = CAux x
1599
1600 type family CAux x where
1601 CAux (Maybe x) = x
1602 CAux (Either x y) = x -> y
1603
1604 We decided that this restriction wasn't buying us much, so we opted not
1605 to pursue that design (see also GHC Trac #13398).
1606
1607 Implementation
1608 * Form the mini-envt from the class type variables a,b
1609 to the instance decl types [p],Int: [a->[p], b->Int]
1610
1611 * Look at the tyvars a,x,b of the type family constructor T
1612 (it shares tyvars with the class C)
1613
1614 * Apply the mini-evnt to them, and check that the result is
1615 consistent with the instance types [p] y Int. (where y can be any type, as
1616 it is not scoped over the class type variables.
1617
1618 We make all the instance type variables scope over the
1619 type instances, of course, which picks up non-obvious kinds. Eg
1620 class Foo (a :: k) where
1621 type F a
1622 instance Foo (b :: k -> k) where
1623 type F b = Int
1624 Here the instance is kind-indexed and really looks like
1625 type F (k->k) (b::k->k) = Int
1626 But if the 'b' didn't scope, we would make F's instance too
1627 poly-kinded.
1628
1629 Note [Invisible arguments and termination]
1630 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1631 When checking the ​Paterson conditions for termination an instance
1632 declaration, we check for the number of "constructors and variables"
1633 in the instance head and constraints. Question: Do we look at
1634
1635 * All the arguments, visible or invisible?
1636 * Just the visible arguments?
1637
1638 I think both will ensure termination, provided we are consistent.
1639 Currently we are /not/ consistent, which is really a bug. It's
1640 described in Trac #15177, which contains a number of examples.
1641 The suspicious bits are the calls to filterOutInvisibleTypes.
1642 -}
1643
1644 -- | Extra information about the parent instance declaration, needed
1645 -- when type-checking associated types. The 'Class' is the enclosing
1646 -- class, the [TyVar] are the type variable of the instance decl,
1647 -- and and the @VarEnv Type@ maps class variables to their instance
1648 -- types.
1649 type ClsInstInfo = (Class, [TyVar], VarEnv Type)
1650
1651 type AssocInstArgShape = (Maybe Type, Type)
1652 -- AssocInstArgShape is used only for associated family instances
1653 -- (mb_exp, actual)
1654 -- mb_exp = Just ty => this arg corresponds to a class variable
1655 -- = Nothing => it doesn't correspond to a class variable
1656 -- e.g. class C b where
1657 -- type F a b c
1658 -- instance C [x] where
1659 -- type F p [x] q
1660 -- We get [AssocInstArgShape] = [ (Nothing, p)
1661 -- , (Just [x], [x])
1662 -- , (Nothing, q)]
1663
1664 checkConsistentFamInst
1665 :: Maybe ClsInstInfo
1666 -> TyCon -- ^ Family tycon
1667 -> [Type] -- ^ Type patterns from instance
1668 -> SDoc -- ^ pretty-printed user-written instance head
1669 -> TcM ()
1670 -- See Note [Checking consistent instantiation]
1671
1672 checkConsistentFamInst Nothing _ _ _ = return ()
1673 checkConsistentFamInst (Just (clas, inst_tvs, mini_env)) fam_tc at_tys pp_hs_pats
1674 = do { -- Check that the associated type indeed comes from this class
1675 -- See [Mismatched class methods and associated type families]
1676 -- in TcInstDecls.
1677 checkTc (Just clas == tyConAssoc_maybe fam_tc)
1678 (badATErr (className clas) (tyConName fam_tc))
1679
1680 -- Check type args first (more comprehensible)
1681 ; checkTc (all check_arg type_shapes) pp_wrong_at_arg
1682
1683 -- And now kind args
1684 ; checkTcM (all check_arg kind_shapes)
1685 (tidy_env2, pp_wrong_at_arg $$ ppSuggestExplicitKinds)
1686
1687 ; traceTc "cfi" (vcat [ ppr inst_tvs
1688 , ppr arg_shapes
1689 , ppr mini_env ]) }
1690 where
1691 arg_shapes :: [AssocInstArgShape]
1692 arg_shapes = [ (lookupVarEnv mini_env fam_tc_tv, at_ty)
1693 | (fam_tc_tv, at_ty) <- tyConTyVars fam_tc `zip` at_tys ]
1694
1695 (kind_shapes, type_shapes) = partitionInvisibles fam_tc snd arg_shapes
1696
1697 check_arg :: AssocInstArgShape -> Bool
1698 check_arg (Just exp_ty, at_ty) = exp_ty `tcEqType` at_ty
1699 check_arg (Nothing, _ ) = True -- Arg position does not correspond
1700 -- to a class variable
1701
1702 pp_wrong_at_arg
1703 = vcat [ text "Type indexes must match class instance head"
1704 , pp_exp_act ]
1705
1706 pp_exp_act
1707 = vcat [ text "Expected:" <+> ppr (mkTyConApp fam_tc expected_args)
1708 , text " Actual:" <+> pp_hs_pats
1709 , sdocWithDynFlags $ \dflags ->
1710 ppWhen (has_poly_args dflags) $
1711 vcat [ text "where the `<tv>' arguments are type variables,"
1712 , text "distinct from each other and from the instance variables" ] ]
1713
1714 -- We need to tidy, since it's possible that expected_args will contain
1715 -- inferred kind variables with names identical to those in at_tys. If we
1716 -- don't, we'll end up with horrible messages like this one (#13972):
1717 --
1718 -- Expected: T (a -> Either a b)
1719 -- Actual: T (a -> Either a b)
1720 (tidy_env1, _) = tidyOpenTypes emptyTidyEnv at_tys
1721 (tidy_env2, expected_args)
1722 = tidyOpenTypes tidy_env1 [ exp_ty `orElse` mk_tv at_ty
1723 | (exp_ty, at_ty) <- arg_shapes ]
1724 mk_tv at_ty = mkTyVarTy (mkTyVar tv_name (typeKind at_ty))
1725 tv_name = mkInternalName (mkAlphaTyVarUnique 1) (mkTyVarOcc "<tv>") noSrcSpan
1726
1727 has_poly_args dflags = any (isNothing . fst) shapes
1728 where
1729 shapes | gopt Opt_PrintExplicitKinds dflags = arg_shapes
1730 | otherwise = type_shapes
1731
1732 badATErr :: Name -> Name -> SDoc
1733 badATErr clas op
1734 = hsep [text "Class", quotes (ppr clas),
1735 text "does not have an associated type", quotes (ppr op)]
1736
1737
1738 {-
1739 ************************************************************************
1740 * *
1741 Checking type instance well-formedness and termination
1742 * *
1743 ************************************************************************
1744 -}
1745
1746 checkValidCoAxiom :: CoAxiom Branched -> TcM ()
1747 checkValidCoAxiom ax@(CoAxiom { co_ax_tc = fam_tc, co_ax_branches = branches })
1748 = do { mapM_ (checkValidCoAxBranch Nothing fam_tc) branch_list
1749 ; foldlM_ check_branch_compat [] branch_list }
1750 where
1751 branch_list = fromBranches branches
1752 injectivity = tyConInjectivityInfo fam_tc
1753
1754 check_branch_compat :: [CoAxBranch] -- previous branches in reverse order
1755 -> CoAxBranch -- current branch
1756 -> TcM [CoAxBranch]-- current branch : previous branches
1757 -- Check for
1758 -- (a) this branch is dominated by previous ones
1759 -- (b) failure of injectivity
1760 check_branch_compat prev_branches cur_branch
1761 | cur_branch `isDominatedBy` prev_branches
1762 = do { addWarnAt NoReason (coAxBranchSpan cur_branch) $
1763 inaccessibleCoAxBranch ax cur_branch
1764 ; return prev_branches }
1765 | otherwise
1766 = do { check_injectivity prev_branches cur_branch
1767 ; return (cur_branch : prev_branches) }
1768
1769 -- Injectivity check: check whether a new (CoAxBranch) can extend
1770 -- already checked equations without violating injectivity
1771 -- annotation supplied by the user.
1772 -- See Note [Verifying injectivity annotation] in FamInstEnv
1773 check_injectivity prev_branches cur_branch
1774 | Injective inj <- injectivity
1775 = do { let conflicts =
1776 fst $ foldl (gather_conflicts inj prev_branches cur_branch)
1777 ([], 0) prev_branches
1778 ; mapM_ (\(err, span) -> setSrcSpan span $ addErr err)
1779 (makeInjectivityErrors ax cur_branch inj conflicts) }
1780 | otherwise
1781 = return ()
1782
1783 gather_conflicts inj prev_branches cur_branch (acc, n) branch
1784 -- n is 0-based index of branch in prev_branches
1785 = case injectiveBranches inj cur_branch branch of
1786 InjectivityUnified ax1 ax2
1787 | ax1 `isDominatedBy` (replace_br prev_branches n ax2)
1788 -> (acc, n + 1)
1789 | otherwise
1790 -> (branch : acc, n + 1)
1791 InjectivityAccepted -> (acc, n + 1)
1792
1793 -- Replace n-th element in the list. Assumes 0-based indexing.
1794 replace_br :: [CoAxBranch] -> Int -> CoAxBranch -> [CoAxBranch]
1795 replace_br brs n br = take n brs ++ [br] ++ drop (n+1) brs
1796
1797
1798 -- Check that a "type instance" is well-formed (which includes decidability
1799 -- unless -XUndecidableInstances is given).
1800 --
1801 checkValidCoAxBranch :: Maybe ClsInstInfo
1802 -> TyCon -> CoAxBranch -> TcM ()
1803 checkValidCoAxBranch mb_clsinfo fam_tc
1804 (CoAxBranch { cab_tvs = tvs, cab_cvs = cvs
1805 , cab_lhs = typats
1806 , cab_rhs = rhs, cab_loc = loc })
1807 = checkValidTyFamEqn mb_clsinfo fam_tc tvs cvs typats rhs pp_lhs loc
1808 where
1809 pp_lhs = ppr (mkTyConApp fam_tc typats)
1810
1811 -- | Do validity checks on a type family equation, including consistency
1812 -- with any enclosing class instance head, termination, and lack of
1813 -- polytypes.
1814 checkValidTyFamEqn :: Maybe ClsInstInfo
1815 -> TyCon -- ^ of the type family
1816 -> [TyVar] -- ^ bound tyvars in the equation
1817 -> [CoVar] -- ^ bound covars in the equation
1818 -> [Type] -- ^ type patterns
1819 -> Type -- ^ rhs
1820 -> SDoc -- ^ user-written LHS
1821 -> SrcSpan
1822 -> TcM ()
1823 checkValidTyFamEqn mb_clsinfo fam_tc tvs cvs typats rhs pp_lhs loc
1824 = setSrcSpan loc $
1825 do { checkValidFamPats mb_clsinfo fam_tc tvs cvs typats [] pp_lhs
1826
1827 -- The argument patterns, and RHS, are all boxed tau types
1828 -- E.g Reject type family F (a :: k1) :: k2
1829 -- type instance F (forall a. a->a) = ...
1830 -- type instance F Int# = ...
1831 -- type instance F Int = forall a. a->a
1832 -- type instance F Int = Int#
1833 -- See Trac #9357
1834 ; checkValidMonoType rhs
1835
1836 -- We have a decidable instance unless otherwise permitted
1837 ; undecidable_ok <- xoptM LangExt.UndecidableInstances
1838 ; traceTc "checkVTFE" (pp_lhs $$ ppr rhs $$ ppr (tcTyFamInsts rhs))
1839 ; unless undecidable_ok $
1840 mapM_ addErrTc (checkFamInstRhs fam_tc typats (tcTyFamInsts rhs)) }
1841
1842 -- Make sure that each type family application is
1843 -- (1) strictly smaller than the lhs,
1844 -- (2) mentions no type variable more often than the lhs, and
1845 -- (3) does not contain any further type family instances.
1846 --
1847 checkFamInstRhs :: TyCon -> [Type] -- LHS
1848 -> [(TyCon, [Type])] -- type family calls in RHS
1849 -> [MsgDoc]
1850 checkFamInstRhs tc lhsTys famInsts
1851 = mapMaybe check famInsts
1852 where
1853 lhs_size = sizeTyConAppArgs tc lhsTys
1854 fvs = fvTypes lhsTys
1855 check (tc, tys)
1856 | not (all isTyFamFree tys) = Just (nestedMsg what)
1857 | not (null bad_tvs) = Just (noMoreMsg bad_tvs what inst_head)
1858 | lhs_size <= fam_app_size = Just (smallerMsg what inst_head)
1859 | otherwise = Nothing
1860 where
1861 what = text "type family application"
1862 <+> quotes (pprType (TyConApp tc tys))
1863 inst_head = pprType (TyConApp tc lhsTys)
1864 bad_tvs = fvTypes tys \\ fvs
1865 fam_app_size = sizeTyConAppArgs tc tys
1866
1867 checkValidFamPats :: Maybe ClsInstInfo -> TyCon -> [TyVar] -> [CoVar]
1868 -> [Type] -- ^ patterns the user wrote
1869 -> [Type] -- ^ "extra" patterns from a data instance kind sig
1870 -> SDoc -- ^ pretty-printed user-written instance head
1871 -> TcM ()
1872 -- Patterns in a 'type instance' or 'data instance' decl should
1873 -- a) contain no type family applications
1874 -- (vanilla synonyms are fine, though)
1875 -- b) properly bind all their free type variables
1876 -- e.g. we disallow (Trac #7536)
1877 -- type T a = Int
1878 -- type instance F (T a) = a
1879 -- c) For associated types, are consistently instantiated
1880 checkValidFamPats mb_clsinfo fam_tc tvs cvs user_ty_pats extra_ty_pats pp_hs_pats
1881 = do { mapM_ checkValidTypePat user_ty_pats
1882
1883 ; let unbound_tcvs = filterOut (`elemVarSet` exactTyCoVarsOfTypes user_ty_pats)
1884 (tvs ++ cvs)
1885 ; checkTc (null unbound_tcvs) (famPatErr fam_tc unbound_tcvs user_ty_pats)
1886
1887 -- Check that type patterns match the class instance head
1888 ; checkConsistentFamInst mb_clsinfo fam_tc (user_ty_pats `chkAppend` extra_ty_pats) pp_hs_pats }
1889
1890 checkValidTypePat :: Type -> TcM ()
1891 -- Used for type patterns in class instances,
1892 -- and in type/data family instances
1893 checkValidTypePat pat_ty
1894 = do { -- Check that pat_ty is a monotype
1895 checkValidMonoType pat_ty
1896 -- One could imagine generalising to allow
1897 -- instance C (forall a. a->a)
1898 -- but we don't know what all the consequences might be
1899
1900 -- Ensure that no type family instances occur a type pattern
1901 ; checkTc (isTyFamFree pat_ty) $
1902 tyFamInstIllegalErr pat_ty }
1903
1904 -- Error messages
1905
1906 inaccessibleCoAxBranch :: CoAxiom br -> CoAxBranch -> SDoc
1907 inaccessibleCoAxBranch fi_ax cur_branch
1908 = text "Type family instance equation is overlapped:" $$
1909 nest 2 (pprCoAxBranch fi_ax cur_branch)
1910
1911 tyFamInstIllegalErr :: Type -> SDoc
1912 tyFamInstIllegalErr ty
1913 = hang (text "Illegal type synonym family application in instance" <>
1914 colon) 2 $
1915 ppr ty
1916
1917 nestedMsg :: SDoc -> SDoc
1918 nestedMsg what
1919 = sep [ text "Illegal nested" <+> what
1920 , parens undecidableMsg ]
1921
1922 famPatErr :: TyCon -> [TyVar] -> [Type] -> SDoc
1923 famPatErr fam_tc tvs pats
1924 = hang (text "Family instance purports to bind type variable" <> plural tvs
1925 <+> pprQuotedList tvs)
1926 2 (hang (text "but the real LHS (expanding synonyms) is:")
1927 2 (pprTypeApp fam_tc (map expandTypeSynonyms pats) <+>
1928 text "= ..."))
1929
1930 {-
1931 ************************************************************************
1932 * *
1933 Telescope checking
1934 * *
1935 ************************************************************************
1936
1937 Note [Bad telescopes]
1938 ~~~~~~~~~~~~~~~~~~~~~
1939 Now that we can mix type and kind variables, there are an awful lot of
1940 ways to shoot yourself in the foot. Here are some.
1941
1942 data SameKind :: k -> k -> * -- just to force unification
1943
1944 1. data T1 a k (b :: k) (x :: SameKind a b)
1945
1946 The problem here is that we discover that a and b should have the same
1947 kind. But this kind mentions k, which is bound *after* a.
1948 (Testcase: dependent/should_fail/BadTelescope)
1949
1950 2. data T2 a (c :: Proxy b) (d :: Proxy a) (x :: SameKind b d)
1951
1952 Note that b is not bound. Yet its kind mentions a. Because we have
1953 a nice rule that all implicitly bound variables come before others,
1954 this is bogus. (We could probably figure out to put b between a and c.
1955 But I think this is doing users a disservice, in the long run.)
1956 (Testcase: dependent/should_fail/BadTelescope4)
1957
1958 To catch these errors, we call checkValidTelescope during kind-checking
1959 datatype declarations. This must be done *before* kind-generalization,
1960 because kind-generalization might observe, say, T1, see that k is free
1961 in a's kind, and generalize over it, producing nonsense. It also must
1962 be done *after* kind-generalization, in order to catch the T2 case, which
1963 becomes apparent only after generalizing.
1964
1965 Note [Keeping scoped variables in order: Explicit] discusses how this
1966 check works for `forall x y z.` written in a type.
1967
1968 -}
1969
1970 -- | Check a list of binders to see if they make a valid telescope.
1971 -- The key property we're checking for is scoping. For example:
1972 -- > data SameKind :: k -> k -> *
1973 -- > data X a k (b :: k) (c :: SameKind a b)
1974 -- Kind inference says that a's kind should be k. But that's impossible,
1975 -- because k isn't in scope when a is bound. This check has to come before
1976 -- general validity checking, because once we kind-generalise, this sort
1977 -- of problem is harder to spot (as we'll generalise over the unbound
1978 -- k in a's type.) See also Note [Bad telescopes].
1979 checkValidTelescope :: [TyConBinder] -- explicit vars (zonked)
1980 -> SDoc -- original, user-written telescope
1981 -> SDoc -- extra text to print
1982 -> TcM ()
1983 checkValidTelescope tvbs user_tyvars extra
1984 = do { let tvs = binderVars tvbs
1985
1986 (_, sorted_tidied_tvs) = tidyTyCoVarBndrs emptyTidyEnv $
1987 toposortTyVars tvs
1988 ; unless (go [] emptyVarSet (binderVars tvbs)) $
1989 addErr $
1990 vcat [ hang (text "These kind and type variables:" <+> user_tyvars $$
1991 text "are out of dependency order. Perhaps try this ordering:")
1992 2 (pprTyVars sorted_tidied_tvs)
1993 , extra ] }
1994
1995 where
1996 go :: [TyVar] -- misplaced variables
1997 -> TyVarSet -> [TyVar] -> Bool
1998 go errs in_scope [] = null (filter (`elemVarSet` in_scope) errs)
1999 -- report an error only when the variable in the kind is brought
2000 -- into scope later in the telescope. Otherwise, we'll just quantify
2001 -- over it in kindGeneralize, as we should.
2002
2003 go errs in_scope (tv:tvs)
2004 = let bad_tvs = filterOut (`elemVarSet` in_scope) $
2005 tyCoVarsOfTypeList (tyVarKind tv)
2006 in go (bad_tvs ++ errs) (in_scope `extendVarSet` tv) tvs
2007
2008 {-
2009 ************************************************************************
2010 * *
2011 \subsection{Auxiliary functions}
2012 * *
2013 ************************************************************************
2014 -}
2015
2016 -- Free variables of a type, retaining repetitions, and expanding synonyms
2017 fvType :: Type -> [TyCoVar]
2018 fvType ty | Just exp_ty <- tcView ty = fvType exp_ty
2019 fvType (TyVarTy tv) = [tv]
2020 fvType (TyConApp _ tys) = fvTypes tys
2021 fvType (LitTy {}) = []
2022 fvType (AppTy fun arg) = fvType fun ++ fvType arg
2023 fvType (FunTy arg res) = fvType arg ++ fvType res
2024 fvType (ForAllTy (TvBndr tv _) ty)
2025 = fvType (tyVarKind tv) ++
2026 filter (/= tv) (fvType ty)
2027 fvType (CastTy ty co) = fvType ty ++ fvCo co
2028 fvType (CoercionTy co) = fvCo co
2029
2030 fvTypes :: [Type] -> [TyVar]
2031 fvTypes tys = concat (map fvType tys)
2032
2033 fvCo :: Coercion -> [TyCoVar]
2034 fvCo (Refl _ ty) = fvType ty
2035 fvCo (TyConAppCo _ _ args) = concatMap fvCo args
2036 fvCo (AppCo co arg) = fvCo co ++ fvCo arg
2037 fvCo (ForAllCo tv h co) = filter (/= tv) (fvCo co) ++ fvCo h
2038 fvCo (FunCo _ co1 co2) = fvCo co1 ++ fvCo co2
2039 fvCo (CoVarCo v) = [v]
2040 fvCo (AxiomInstCo _ _ args) = concatMap fvCo args
2041 fvCo (UnivCo p _ t1 t2) = fvProv p ++ fvType t1 ++ fvType t2
2042 fvCo (SymCo co) = fvCo co
2043 fvCo (TransCo co1 co2) = fvCo co1 ++ fvCo co2
2044 fvCo (NthCo _ _ co) = fvCo co
2045 fvCo (LRCo _ co) = fvCo co
2046 fvCo (InstCo co arg) = fvCo co ++ fvCo arg
2047 fvCo (CoherenceCo co1 co2) = fvCo co1 ++ fvCo co2
2048 fvCo (KindCo co) = fvCo co
2049 fvCo (SubCo co) = fvCo co
2050 fvCo (AxiomRuleCo _ cs) = concatMap fvCo cs
2051 fvCo (HoleCo h) = pprPanic "fvCo falls into a hole" (ppr h)
2052
2053 fvProv :: UnivCoProvenance -> [TyCoVar]
2054 fvProv UnsafeCoerceProv = []
2055 fvProv (PhantomProv co) = fvCo co
2056 fvProv (ProofIrrelProv co) = fvCo co
2057 fvProv (PluginProv _) = []
2058
2059 sizeType :: Type -> Int
2060 -- Size of a type: the number of variables and constructors
2061 sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty
2062 sizeType (TyVarTy {}) = 1
2063 sizeType (TyConApp tc tys) = 1 + sizeTyConAppArgs tc tys
2064 sizeType (LitTy {}) = 1
2065 sizeType (AppTy fun arg) = sizeType fun + sizeType arg
2066 sizeType (FunTy arg res) = sizeType arg + sizeType res + 1
2067 sizeType (ForAllTy _ ty) = sizeType ty
2068 sizeType (CastTy ty _) = sizeType ty
2069 sizeType (CoercionTy _) = 1
2070
2071 sizeTypes :: [Type] -> Int
2072 sizeTypes = foldr ((+) . sizeType) 0
2073
2074 sizeTyConAppArgs :: TyCon -> [Type] -> Int
2075 sizeTyConAppArgs _tc tys = sizeTypes tys -- (filterOutInvisibleTypes tc tys)
2076 -- See Note [Invisible arguments and termination]
2077
2078 -- Size of a predicate
2079 --
2080 -- We are considering whether class constraints terminate.
2081 -- Equality constraints and constraints for the implicit
2082 -- parameter class always terminate so it is safe to say "size 0".
2083 -- See Trac #4200.
2084 sizePred :: PredType -> Int
2085 sizePred ty = goClass ty
2086 where
2087 goClass p = go (classifyPredType p)
2088
2089 go (ClassPred cls tys')
2090 | isTerminatingClass cls = 0
2091 | otherwise = sizeTypes (filterOutInvisibleTypes (classTyCon cls) tys')
2092 -- The filtering looks bogus
2093 -- See Note [Invisible arguments and termination]
2094 go (EqPred {}) = 0
2095 go (IrredPred ty) = sizeType ty
2096 go (ForAllPred _ _ pred) = goClass pred
2097
2098 -- | When this says "True", ignore this class constraint during
2099 -- a termination check
2100 isTerminatingClass :: Class -> Bool
2101 isTerminatingClass cls
2102 = isIPClass cls -- Implicit parameter constraints always terminate because
2103 -- there are no instances for them --- they are only solved
2104 -- by "local instances" in expressions
2105 || cls `hasKey` typeableClassKey
2106 || cls `hasKey` coercibleTyConKey
2107 || cls `hasKey` eqTyConKey
2108 || cls `hasKey` heqTyConKey
2109
2110 -- | Tidy before printing a type
2111 ppr_tidy :: TidyEnv -> Type -> SDoc
2112 ppr_tidy env ty = pprType (tidyType env ty)
2113
2114 allDistinctTyVars :: TyVarSet -> [KindOrType] -> Bool
2115 -- (allDistinctTyVars tvs tys) returns True if tys are
2116 -- a) all tyvars
2117 -- b) all distinct
2118 -- c) disjoint from tvs
2119 allDistinctTyVars _ [] = True
2120 allDistinctTyVars tkvs (ty : tys)
2121 = case getTyVar_maybe ty of
2122 Nothing -> False
2123 Just tv | tv `elemVarSet` tkvs -> False
2124 | otherwise -> allDistinctTyVars (tkvs `extendVarSet` tv) tys