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