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