Add valid refinement substitution suggestions for typed holes
[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
731 | otherwise -- A bit like classifyPredType, but not the same
732 -- E.g. we treat (~) like (~#); and we look inside tuples
733 = case splitTyConApp_maybe pred of
734 Just (tc, tys)
735 | isTupleTyCon tc
736 -> check_tuple_pred under_syn env dflags ctxt pred tys
737
738 | tc `hasKey` heqTyConKey ||
739 tc `hasKey` eqTyConKey ||
740 tc `hasKey` eqPrimTyConKey
741 -- NB: this equality check must come first,
742 -- because (~) is a class,too.
743 -> check_eq_pred env dflags pred tc tys
744
745 | Just cls <- tyConClass_maybe tc
746 -- Includes Coercible
747 -> check_class_pred env dflags ctxt pred cls tys
748
749 _ -> check_irred_pred under_syn env dflags ctxt pred
750
751 check_eq_pred :: TidyEnv -> DynFlags -> PredType -> TyCon -> [TcType] -> TcM ()
752 check_eq_pred env dflags pred tc tys
753 = -- Equational constraints are valid in all contexts if type
754 -- families are permitted
755 do { checkTc (tys `lengthIs` tyConArity tc) (tyConArityErr tc tys)
756 ; checkTcM (xopt LangExt.TypeFamilies dflags
757 || xopt LangExt.GADTs dflags)
758 (eqPredTyErr env pred) }
759
760 check_tuple_pred :: Bool -> TidyEnv -> DynFlags -> UserTypeCtxt -> PredType -> [PredType] -> TcM ()
761 check_tuple_pred under_syn env dflags ctxt pred ts
762 = do { -- See Note [ConstraintKinds in predicates]
763 checkTcM (under_syn || xopt LangExt.ConstraintKinds dflags)
764 (predTupleErr env pred)
765 ; mapM_ (check_pred_help under_syn env dflags ctxt) ts }
766 -- This case will not normally be executed because without
767 -- -XConstraintKinds tuple types are only kind-checked as *
768
769 check_irred_pred :: Bool -> TidyEnv -> DynFlags -> UserTypeCtxt -> PredType -> TcM ()
770 check_irred_pred under_syn env dflags ctxt pred
771 -- The predicate looks like (X t1 t2) or (x t1 t2) :: Constraint
772 -- where X is a type function
773 = do { -- If it looks like (x t1 t2), require ConstraintKinds
774 -- see Note [ConstraintKinds in predicates]
775 -- But (X t1 t2) is always ok because we just require ConstraintKinds
776 -- at the definition site (Trac #9838)
777 failIfTcM (not under_syn && not (xopt LangExt.ConstraintKinds dflags)
778 && hasTyVarHead pred)
779 (predIrredErr env pred)
780
781 -- Make sure it is OK to have an irred pred in this context
782 -- See Note [Irreducible predicates in superclasses]
783 ; failIfTcM (is_superclass ctxt
784 && not (xopt LangExt.UndecidableInstances dflags)
785 && has_tyfun_head pred)
786 (predSuperClassErr env pred) }
787 where
788 is_superclass ctxt = case ctxt of { ClassSCCtxt _ -> True; _ -> False }
789 has_tyfun_head ty
790 = case tcSplitTyConApp_maybe ty of
791 Just (tc, _) -> isTypeFamilyTyCon tc
792 Nothing -> False
793
794 {- Note [ConstraintKinds in predicates]
795 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
796 Don't check for -XConstraintKinds under a type synonym, because that
797 was done at the type synonym definition site; see Trac #9838
798 e.g. module A where
799 type C a = (Eq a, Ix a) -- Needs -XConstraintKinds
800 module B where
801 import A
802 f :: C a => a -> a -- Does *not* need -XConstraintKinds
803
804 Note [Irreducible predicates in superclasses]
805 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
806 Allowing type-family calls in class superclasses is somewhat dangerous
807 because we can write:
808
809 type family Fooish x :: * -> Constraint
810 type instance Fooish () = Foo
811 class Fooish () a => Foo a where
812
813 This will cause the constraint simplifier to loop because every time we canonicalise a
814 (Foo a) class constraint we add a (Fooish () a) constraint which will be immediately
815 solved to add+canonicalise another (Foo a) constraint. -}
816
817 -------------------------
818 check_class_pred :: TidyEnv -> DynFlags -> UserTypeCtxt -> PredType -> Class -> [TcType] -> TcM ()
819 check_class_pred env dflags ctxt pred cls tys
820 | isIPClass cls
821 = do { check_arity
822 ; checkTcM (okIPCtxt ctxt) (badIPPred env pred) }
823
824 | otherwise
825 = do { check_arity
826 ; warn_simp <- woptM Opt_WarnSimplifiableClassConstraints
827 ; when warn_simp check_simplifiable_class_constraint
828 ; checkTcM arg_tys_ok (predTyVarErr env pred) }
829 where
830 check_arity = checkTc (tys `lengthIs` classArity cls)
831 (tyConArityErr (classTyCon cls) tys)
832
833 -- Check the arguments of a class constraint
834 flexible_contexts = xopt LangExt.FlexibleContexts dflags
835 undecidable_ok = xopt LangExt.UndecidableInstances dflags
836 arg_tys_ok = case ctxt of
837 SpecInstCtxt -> True -- {-# SPECIALISE instance Eq (T Int) #-} is fine
838 InstDeclCtxt -> checkValidClsArgs (flexible_contexts || undecidable_ok) cls tys
839 -- Further checks on head and theta
840 -- in checkInstTermination
841 _ -> checkValidClsArgs flexible_contexts cls tys
842
843 -- See Note [Simplifiable given constraints]
844 check_simplifiable_class_constraint
845 | xopt LangExt.MonoLocalBinds dflags
846 = return ()
847 | DataTyCtxt {} <- ctxt -- Don't do this check for the "stupid theta"
848 = return () -- of a data type declaration
849 | otherwise
850 = do { envs <- tcGetInstEnvs
851 ; case lookupInstEnv False envs cls tys of
852 ([m], [], _) -> addWarnTc (Reason Opt_WarnSimplifiableClassConstraints)
853 (simplifiable_constraint_warn m)
854 _ -> return () }
855
856 simplifiable_constraint_warn :: InstMatch -> SDoc
857 simplifiable_constraint_warn (match, _)
858 = vcat [ hang (text "The constraint" <+> quotes (ppr (tidyType env pred)))
859 2 (text "matches an instance declaration")
860 , ppr match
861 , hang (text "This makes type inference for inner bindings fragile;")
862 2 (text "either use MonoLocalBinds, or simplify it using the instance") ]
863
864 {- Note [Simplifiable given constraints]
865 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
866 A type signature like
867 f :: Eq [(a,b)] => a -> b
868 is very fragile, for reasons described at length in TcInteract
869 Note [Instance and Given overlap]. As that Note discusses, for the
870 most part the clever stuff in TcInteract means that we don't use a
871 top-level instance if a local Given might fire, so there is no
872 fragility. But if we /infer/ the type of a local let-binding, things
873 can go wrong (Trac #11948 is an example, discussed in the Note).
874
875 So this warning is switched on only if we have NoMonoLocalBinds; in
876 that case the warning discourages users from writing simplifiable
877 class constraints.
878
879 The warning only fires if the constraint in the signature
880 matches the top-level instances in only one way, and with no
881 unifiers -- that is, under the same circumstances that
882 TcInteract.matchInstEnv fires an interaction with the top
883 level instances. For example (Trac #13526), consider
884
885 instance {-# OVERLAPPABLE #-} Eq (T a) where ...
886 instance Eq (T Char) where ..
887 f :: Eq (T a) => ...
888
889 We don't want to complain about this, even though the context
890 (Eq (T a)) matches an instance, because the user may be
891 deliberately deferring the choice so that the Eq (T Char)
892 has a chance to fire when 'f' is called. And the fragility
893 only matters when there's a risk that the instance might
894 fire instead of the local 'given'; and there is no such
895 risk in this case. Just use the same rules as for instance
896 firing!
897 -}
898
899 -------------------------
900 okIPCtxt :: UserTypeCtxt -> Bool
901 -- See Note [Implicit parameters in instance decls]
902 okIPCtxt (FunSigCtxt {}) = True
903 okIPCtxt (InfSigCtxt {}) = True
904 okIPCtxt ExprSigCtxt = True
905 okIPCtxt TypeAppCtxt = True
906 okIPCtxt PatSigCtxt = True
907 okIPCtxt ResSigCtxt = True
908 okIPCtxt GenSigCtxt = True
909 okIPCtxt (ConArgCtxt {}) = True
910 okIPCtxt (ForSigCtxt {}) = True -- ??
911 okIPCtxt ThBrackCtxt = True
912 okIPCtxt GhciCtxt = True
913 okIPCtxt SigmaCtxt = True
914 okIPCtxt (DataTyCtxt {}) = True
915 okIPCtxt (PatSynCtxt {}) = True
916 okIPCtxt (TySynCtxt {}) = True -- e.g. type Blah = ?x::Int
917 -- Trac #11466
918
919 okIPCtxt (ClassSCCtxt {}) = False
920 okIPCtxt (InstDeclCtxt {}) = False
921 okIPCtxt (SpecInstCtxt {}) = False
922 okIPCtxt (RuleSigCtxt {}) = False
923 okIPCtxt DefaultDeclCtxt = False
924
925 {-
926 Note [Kind polymorphic type classes]
927 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
928 MultiParam check:
929
930 class C f where... -- C :: forall k. k -> Constraint
931 instance C Maybe where...
932
933 The dictionary gets type [C * Maybe] even if it's not a MultiParam
934 type class.
935
936 Flexibility check:
937
938 class C f where... -- C :: forall k. k -> Constraint
939 data D a = D a
940 instance C D where
941
942 The dictionary gets type [C * (D *)]. IA0_TODO it should be
943 generalized actually.
944 -}
945
946 checkThetaCtxt :: UserTypeCtxt -> ThetaType -> TidyEnv -> TcM (TidyEnv, SDoc)
947 checkThetaCtxt ctxt theta env
948 = return ( env
949 , vcat [ text "In the context:" <+> pprTheta (tidyTypes env theta)
950 , text "While checking" <+> pprUserTypeCtxt ctxt ] )
951
952 eqPredTyErr, predTupleErr, predIrredErr, predSuperClassErr :: TidyEnv -> PredType -> (TidyEnv, SDoc)
953 eqPredTyErr env pred
954 = ( env
955 , text "Illegal equational constraint" <+> ppr_tidy env pred $$
956 parens (text "Use GADTs or TypeFamilies to permit this") )
957 predTupleErr env pred
958 = ( env
959 , hang (text "Illegal tuple constraint:" <+> ppr_tidy env pred)
960 2 (parens constraintKindsMsg) )
961 predIrredErr env pred
962 = ( env
963 , hang (text "Illegal constraint:" <+> ppr_tidy env pred)
964 2 (parens constraintKindsMsg) )
965 predSuperClassErr env pred
966 = ( env
967 , hang (text "Illegal constraint" <+> quotes (ppr_tidy env pred)
968 <+> text "in a superclass context")
969 2 (parens undecidableMsg) )
970
971 predTyVarErr :: TidyEnv -> PredType -> (TidyEnv, SDoc)
972 predTyVarErr env pred
973 = (env
974 , vcat [ hang (text "Non type-variable argument")
975 2 (text "in the constraint:" <+> ppr_tidy env pred)
976 , parens (text "Use FlexibleContexts to permit this") ])
977
978 badIPPred :: TidyEnv -> PredType -> (TidyEnv, SDoc)
979 badIPPred env pred
980 = ( env
981 , text "Illegal implicit parameter" <+> quotes (ppr_tidy env pred) )
982
983 constraintSynErr :: TidyEnv -> Type -> (TidyEnv, SDoc)
984 constraintSynErr env kind
985 = ( env
986 , hang (text "Illegal constraint synonym of kind:" <+> quotes (ppr_tidy env kind))
987 2 (parens constraintKindsMsg) )
988
989 dupPredWarn :: TidyEnv -> [NE.NonEmpty PredType] -> (TidyEnv, SDoc)
990 dupPredWarn env dups
991 = ( env
992 , text "Duplicate constraint" <> plural primaryDups <> text ":"
993 <+> pprWithCommas (ppr_tidy env) primaryDups )
994 where
995 primaryDups = map NE.head dups
996
997 tyConArityErr :: TyCon -> [TcType] -> SDoc
998 -- For type-constructor arity errors, be careful to report
999 -- the number of /visible/ arguments required and supplied,
1000 -- ignoring the /invisible/ arguments, which the user does not see.
1001 -- (e.g. Trac #10516)
1002 tyConArityErr tc tks
1003 = arityErr (ppr (tyConFlavour tc)) (tyConName tc)
1004 tc_type_arity tc_type_args
1005 where
1006 vis_tks = filterOutInvisibleTypes tc tks
1007
1008 -- tc_type_arity = number of *type* args expected
1009 -- tc_type_args = number of *type* args encountered
1010 tc_type_arity = count isVisibleTyConBinder (tyConBinders tc)
1011 tc_type_args = length vis_tks
1012
1013 arityErr :: Outputable a => SDoc -> a -> Int -> Int -> SDoc
1014 arityErr what name n m
1015 = hsep [ text "The" <+> what, quotes (ppr name), text "should have",
1016 n_arguments <> comma, text "but has been given",
1017 if m==0 then text "none" else int m]
1018 where
1019 n_arguments | n == 0 = text "no arguments"
1020 | n == 1 = text "1 argument"
1021 | True = hsep [int n, text "arguments"]
1022
1023 {-
1024 ************************************************************************
1025 * *
1026 \subsection{Checking for a decent instance head type}
1027 * *
1028 ************************************************************************
1029
1030 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1031 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1032
1033 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1034 flag is on, or (2)~the instance is imported (they must have been
1035 compiled elsewhere). In these cases, we let them go through anyway.
1036
1037 We can also have instances for functions: @instance Foo (a -> b) ...@.
1038 -}
1039
1040 checkValidInstHead :: UserTypeCtxt -> Class -> [Type] -> TcM ()
1041 checkValidInstHead ctxt clas cls_args
1042 = do { dflags <- getDynFlags
1043
1044 ; mod <- getModule
1045 ; checkTc (getUnique clas `notElem` abstractClassKeys ||
1046 nameModule (getName clas) == mod)
1047 (instTypeErr clas cls_args abstract_class_msg)
1048
1049 ; when (clas `hasKey` hasFieldClassNameKey) $
1050 checkHasFieldInst clas cls_args
1051
1052 -- Check language restrictions;
1053 -- but not for SPECIALISE instance pragmas
1054 ; let ty_args = filterOutInvisibleTypes (classTyCon clas) cls_args
1055 ; unless spec_inst_prag $
1056 do { checkTc (xopt LangExt.TypeSynonymInstances dflags ||
1057 all tcInstHeadTyNotSynonym ty_args)
1058 (instTypeErr clas cls_args head_type_synonym_msg)
1059 ; checkTc (xopt LangExt.FlexibleInstances dflags ||
1060 all tcInstHeadTyAppAllTyVars ty_args)
1061 (instTypeErr clas cls_args head_type_args_tyvars_msg)
1062 ; checkTc (xopt LangExt.MultiParamTypeClasses dflags ||
1063 lengthIs ty_args 1 || -- Only count type arguments
1064 (xopt LangExt.NullaryTypeClasses dflags &&
1065 null ty_args))
1066 (instTypeErr clas cls_args head_one_type_msg) }
1067
1068 ; mapM_ checkValidTypePat ty_args }
1069 where
1070 spec_inst_prag = case ctxt of { SpecInstCtxt -> True; _ -> False }
1071
1072 head_type_synonym_msg = parens (
1073 text "All instance types must be of the form (T t1 ... tn)" $$
1074 text "where T is not a synonym." $$
1075 text "Use TypeSynonymInstances if you want to disable this.")
1076
1077 head_type_args_tyvars_msg = parens (vcat [
1078 text "All instance types must be of the form (T a1 ... an)",
1079 text "where a1 ... an are *distinct type variables*,",
1080 text "and each type variable appears at most once in the instance head.",
1081 text "Use FlexibleInstances if you want to disable this."])
1082
1083 head_one_type_msg = parens (
1084 text "Only one type can be given in an instance head." $$
1085 text "Use MultiParamTypeClasses if you want to allow more, or zero.")
1086
1087 abstract_class_msg =
1088 text "Manual instances of this class are not permitted."
1089
1090 tcInstHeadTyNotSynonym :: Type -> Bool
1091 -- Used in Haskell-98 mode, for the argument types of an instance head
1092 -- These must not be type synonyms, but everywhere else type synonyms
1093 -- are transparent, so we need a special function here
1094 tcInstHeadTyNotSynonym ty
1095 = case ty of -- Do not use splitTyConApp,
1096 -- because that expands synonyms!
1097 TyConApp tc _ -> not (isTypeSynonymTyCon tc)
1098 _ -> True
1099
1100 tcInstHeadTyAppAllTyVars :: Type -> Bool
1101 -- Used in Haskell-98 mode, for the argument types of an instance head
1102 -- These must be a constructor applied to type variable arguments.
1103 -- But we allow kind instantiations.
1104 tcInstHeadTyAppAllTyVars ty
1105 | Just (tc, tys) <- tcSplitTyConApp_maybe (dropCasts ty)
1106 = ok (filterOutInvisibleTypes tc tys) -- avoid kinds
1107
1108 | otherwise
1109 = False
1110 where
1111 -- Check that all the types are type variables,
1112 -- and that each is distinct
1113 ok tys = equalLength tvs tys && hasNoDups tvs
1114 where
1115 tvs = mapMaybe tcGetTyVar_maybe tys
1116
1117 dropCasts :: Type -> Type
1118 -- See Note [Casts during validity checking]
1119 -- This function can turn a well-kinded type into an ill-kinded
1120 -- one, so I've kept it local to this module
1121 -- To consider: drop only HoleCo casts
1122 dropCasts (CastTy ty _) = dropCasts ty
1123 dropCasts (AppTy t1 t2) = mkAppTy (dropCasts t1) (dropCasts t2)
1124 dropCasts (FunTy t1 t2) = mkFunTy (dropCasts t1) (dropCasts t2)
1125 dropCasts (TyConApp tc tys) = mkTyConApp tc (map dropCasts tys)
1126 dropCasts (ForAllTy b ty) = ForAllTy (dropCastsB b) (dropCasts ty)
1127 dropCasts ty = ty -- LitTy, TyVarTy, CoercionTy
1128
1129 dropCastsB :: TyVarBinder -> TyVarBinder
1130 dropCastsB b = b -- Don't bother in the kind of a forall
1131
1132 abstractClassKeys :: [Unique]
1133 abstractClassKeys = [ heqTyConKey
1134 , eqTyConKey
1135 , coercibleTyConKey
1136 ] -- See Note [Equality class instances]
1137
1138 instTypeErr :: Class -> [Type] -> SDoc -> SDoc
1139 instTypeErr cls tys msg
1140 = hang (hang (text "Illegal instance declaration for")
1141 2 (quotes (pprClassPred cls tys)))
1142 2 msg
1143
1144 -- | See Note [Validity checking of HasField instances]
1145 checkHasFieldInst :: Class -> [Type] -> TcM ()
1146 checkHasFieldInst cls tys@[_k_ty, x_ty, r_ty, _a_ty] =
1147 case splitTyConApp_maybe r_ty of
1148 Nothing -> whoops (text "Record data type must be specified")
1149 Just (tc, _)
1150 | isFamilyTyCon tc
1151 -> whoops (text "Record data type may not be a data family")
1152 | otherwise -> case isStrLitTy x_ty of
1153 Just lbl
1154 | isJust (lookupTyConFieldLabel lbl tc)
1155 -> whoops (ppr tc <+> text "already has a field"
1156 <+> quotes (ppr lbl))
1157 | otherwise -> return ()
1158 Nothing
1159 | null (tyConFieldLabels tc) -> return ()
1160 | otherwise -> whoops (ppr tc <+> text "has fields")
1161 where
1162 whoops = addErrTc . instTypeErr cls tys
1163 checkHasFieldInst _ tys = pprPanic "checkHasFieldInst" (ppr tys)
1164
1165 {- Note [Casts during validity checking]
1166 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1167 Consider the (bogus)
1168 instance Eq Char#
1169 We elaborate to 'Eq (Char# |> UnivCo(hole))' where the hole is an
1170 insoluble equality constraint for * ~ #. We'll report the insoluble
1171 constraint separately, but we don't want to *also* complain that Eq is
1172 not applied to a type constructor. So we look gaily look through
1173 CastTys here.
1174
1175 Another example: Eq (Either a). Then we actually get a cast in
1176 the middle:
1177 Eq ((Either |> g) a)
1178
1179
1180 Note [Validity checking of HasField instances]
1181 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1182 The HasField class has magic constraint solving behaviour (see Note
1183 [HasField instances] in TcInteract). However, we permit users to
1184 declare their own instances, provided they do not clash with the
1185 built-in behaviour. In particular, we forbid:
1186
1187 1. `HasField _ r _` where r is a variable
1188
1189 2. `HasField _ (T ...) _` if T is a data family
1190 (because it might have fields introduced later)
1191
1192 3. `HasField x (T ...) _` where x is a variable,
1193 if T has any fields at all
1194
1195 4. `HasField "foo" (T ...) _` if T has a "foo" field
1196
1197 The usual functional dependency checks also apply.
1198
1199
1200 Note [Valid 'deriving' predicate]
1201 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1202 validDerivPred checks for OK 'deriving' context. See Note [Exotic
1203 derived instance contexts] in TcDeriv. However the predicate is
1204 here because it uses sizeTypes, fvTypes.
1205
1206 It checks for three things
1207
1208 * No repeated variables (hasNoDups fvs)
1209
1210 * No type constructors. This is done by comparing
1211 sizeTypes tys == length (fvTypes tys)
1212 sizeTypes counts variables and constructors; fvTypes returns variables.
1213 So if they are the same, there must be no constructors. But there
1214 might be applications thus (f (g x)).
1215
1216 Note that tys only includes the visible arguments of the class type
1217 constructor. Including the non-visible arguments can cause the following,
1218 perfectly valid instance to be rejected:
1219 class Category (cat :: k -> k -> *) where ...
1220 newtype T (c :: * -> * -> *) a b = MkT (c a b)
1221 instance Category c => Category (T c) where ...
1222 since the first argument to Category is a non-visible *, which sizeTypes
1223 would count as a constructor! See Trac #11833.
1224
1225 * Also check for a bizarre corner case, when the derived instance decl
1226 would look like
1227 instance C a b => D (T a) where ...
1228 Note that 'b' isn't a parameter of T. This gives rise to all sorts of
1229 problems; in particular, it's hard to compare solutions for equality
1230 when finding the fixpoint, and that means the inferContext loop does
1231 not converge. See Trac #5287.
1232
1233 Note [Equality class instances]
1234 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1235 We can't have users writing instances for the equality classes. But we
1236 still need to be able to write instances for them ourselves. So we allow
1237 instances only in the defining module.
1238
1239 -}
1240
1241 validDerivPred :: TyVarSet -> PredType -> Bool
1242 -- See Note [Valid 'deriving' predicate]
1243 validDerivPred tv_set pred
1244 = case classifyPredType pred of
1245 ClassPred cls tys -> cls `hasKey` typeableClassKey
1246 -- Typeable constraints are bigger than they appear due
1247 -- to kind polymorphism, but that's OK
1248 || check_tys cls tys
1249 EqPred {} -> False -- reject equality constraints
1250 _ -> True -- Non-class predicates are ok
1251 where
1252 check_tys cls tys
1253 = hasNoDups fvs
1254 -- use sizePred to ignore implicit args
1255 && lengthIs fvs (sizePred pred)
1256 && all (`elemVarSet` tv_set) fvs
1257 where tys' = filterOutInvisibleTypes (classTyCon cls) tys
1258 fvs = fvTypes tys'
1259
1260 {-
1261 ************************************************************************
1262 * *
1263 \subsection{Checking instance for termination}
1264 * *
1265 ************************************************************************
1266 -}
1267
1268 {- Note [Instances and constraint synonyms]
1269 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1270 Currently, we don't allow instances for constraint synonyms at all.
1271 Consider these (Trac #13267):
1272 type C1 a = Show (a -> Bool)
1273 instance C1 Int where -- I1
1274 show _ = "ur"
1275
1276 This elicits "show is not a (visible) method of class C1", which isn't
1277 a great message. But it comes from the renamer, so it's hard to improve.
1278
1279 This needs a bit more care:
1280 type C2 a = (Show a, Show Int)
1281 instance C2 Int -- I2
1282
1283 If we use (splitTyConApp_maybe tau) in checkValidInstance to decompose
1284 the instance head, we'll expand the synonym on fly, and it'll look like
1285 instance (%,%) (Show Int, Show Int)
1286 and we /really/ don't want that. So we carefully do /not/ expand
1287 synonyms, by matching on TyConApp directly.
1288 -}
1289
1290 checkValidInstance :: UserTypeCtxt -> LHsSigType GhcRn -> Type
1291 -> TcM ([TyVar], ThetaType, Class, [Type])
1292 checkValidInstance ctxt hs_type ty
1293 | not is_tc_app
1294 = failWithTc (text "Instance head is not headed by a class")
1295
1296 | isNothing mb_cls
1297 = failWithTc (vcat [ text "Illegal instance for a" <+> ppr (tyConFlavour tc)
1298 , text "A class instance must be for a class" ])
1299
1300 | not arity_ok
1301 = failWithTc (text "Arity mis-match in instance head")
1302
1303 | otherwise
1304 = do { setSrcSpan head_loc (checkValidInstHead ctxt clas inst_tys)
1305 ; traceTc "checkValidInstance {" (ppr ty)
1306 ; checkValidTheta ctxt theta
1307
1308 -- The Termination and Coverate Conditions
1309 -- Check that instance inference will terminate (if we care)
1310 -- For Haskell 98 this will already have been done by checkValidTheta,
1311 -- but as we may be using other extensions we need to check.
1312 --
1313 -- Note that the Termination Condition is *more conservative* than
1314 -- the checkAmbiguity test we do on other type signatures
1315 -- e.g. Bar a => Bar Int is ambiguous, but it also fails
1316 -- the termination condition, because 'a' appears more often
1317 -- in the constraint than in the head
1318 ; undecidable_ok <- xoptM LangExt.UndecidableInstances
1319 ; if undecidable_ok
1320 then checkAmbiguity ctxt ty
1321 else checkInstTermination inst_tys theta
1322
1323 ; traceTc "cvi 2" (ppr ty)
1324
1325 ; case (checkInstCoverage undecidable_ok clas theta inst_tys) of
1326 IsValid -> return () -- Check succeeded
1327 NotValid msg -> addErrTc (instTypeErr clas inst_tys msg)
1328
1329 ; traceTc "End checkValidInstance }" empty
1330
1331 ; return (tvs, theta, clas, inst_tys) }
1332 where
1333 (tvs, theta, tau) = tcSplitSigmaTy ty
1334 is_tc_app = case tau of { TyConApp {} -> True; _ -> False }
1335 TyConApp tc inst_tys = tau -- See Note [Instances and constraint synonyms]
1336 mb_cls = tyConClass_maybe tc
1337 Just clas = mb_cls
1338 arity_ok = inst_tys `lengthIs` classArity clas
1339
1340 -- The location of the "head" of the instance
1341 head_loc = getLoc (getLHsInstDeclHead hs_type)
1342
1343 {-
1344 Note [Paterson conditions]
1345 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1346 Termination test: the so-called "Paterson conditions" (see Section 5 of
1347 "Understanding functional dependencies via Constraint Handling Rules,
1348 JFP Jan 2007).
1349
1350 We check that each assertion in the context satisfies:
1351 (1) no variable has more occurrences in the assertion than in the head, and
1352 (2) the assertion has fewer constructors and variables (taken together
1353 and counting repetitions) than the head.
1354 This is only needed with -fglasgow-exts, as Haskell 98 restrictions
1355 (which have already been checked) guarantee termination.
1356
1357 The underlying idea is that
1358
1359 for any ground substitution, each assertion in the
1360 context has fewer type constructors than the head.
1361 -}
1362
1363 checkInstTermination :: [TcType] -> ThetaType -> TcM ()
1364 -- See Note [Paterson conditions]
1365 checkInstTermination tys theta
1366 = check_preds theta
1367 where
1368 head_fvs = fvTypes tys
1369 head_size = sizeTypes tys
1370
1371 check_preds :: [PredType] -> TcM ()
1372 check_preds preds = mapM_ check preds
1373
1374 check :: PredType -> TcM ()
1375 check pred
1376 = case classifyPredType pred of
1377 EqPred {} -> return () -- See Trac #4200.
1378 IrredPred {} -> check2 pred (sizeType pred)
1379 ClassPred cls tys
1380 | isTerminatingClass cls
1381 -> return ()
1382
1383 | isCTupleClass cls -- Look inside tuple predicates; Trac #8359
1384 -> check_preds tys
1385
1386 | otherwise
1387 -> check2 pred (sizeTypes $ filterOutInvisibleTypes (classTyCon cls) tys)
1388 -- Other ClassPreds
1389
1390 check2 pred pred_size
1391 | not (null bad_tvs) = addErrTc (noMoreMsg bad_tvs what)
1392 | pred_size >= head_size = addErrTc (smallerMsg what)
1393 | otherwise = return ()
1394 where
1395 what = text "constraint" <+> quotes (ppr pred)
1396 bad_tvs = fvType pred \\ head_fvs
1397
1398 smallerMsg :: SDoc -> SDoc
1399 smallerMsg what
1400 = vcat [ hang (text "The" <+> what)
1401 2 (text "is no smaller than the instance head")
1402 , parens undecidableMsg ]
1403
1404 noMoreMsg :: [TcTyVar] -> SDoc -> SDoc
1405 noMoreMsg tvs what
1406 = vcat [ hang (text "Variable" <> plural tvs <+> quotes (pprWithCommas ppr tvs)
1407 <+> occurs <+> text "more often")
1408 2 (sep [ text "in the" <+> what
1409 , text "than in the instance head" ])
1410 , parens undecidableMsg ]
1411 where
1412 occurs = if isSingleton tvs then text "occurs"
1413 else text "occur"
1414
1415 undecidableMsg, constraintKindsMsg :: SDoc
1416 undecidableMsg = text "Use UndecidableInstances to permit this"
1417 constraintKindsMsg = text "Use ConstraintKinds to permit this"
1418
1419 {-
1420 Note [Associated type instances]
1421 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1422 We allow this:
1423 class C a where
1424 type T x a
1425 instance C Int where
1426 type T (S y) Int = y
1427 type T Z Int = Char
1428
1429 Note that
1430 a) The variable 'x' is not bound by the class decl
1431 b) 'x' is instantiated to a non-type-variable in the instance
1432 c) There are several type instance decls for T in the instance
1433
1434 All this is fine. Of course, you can't give any *more* instances
1435 for (T ty Int) elsewhere, because it's an *associated* type.
1436
1437 Note [Checking consistent instantiation]
1438 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1439 See Trac #11450 for background discussion on this check.
1440
1441 class C a b where
1442 type T a x b
1443
1444 With this class decl, if we have an instance decl
1445 instance C ty1 ty2 where ...
1446 then the type instance must look like
1447 type T ty1 v ty2 = ...
1448 with exactly 'ty1' for 'a', 'ty2' for 'b', and some type 'v' for 'x'.
1449 For example:
1450
1451 instance C [p] Int
1452 type T [p] y Int = (p,y,y)
1453
1454 Note that
1455
1456 * We used to allow completely different bound variables in the
1457 associated type instance; e.g.
1458 instance C [p] Int
1459 type T [q] y Int = ...
1460 But from GHC 8.2 onwards, we don't. It's much simpler this way.
1461 See Trac #11450.
1462
1463 * When the class variable isn't used on the RHS of the type instance,
1464 it's tempting to allow wildcards, thus
1465 instance C [p] Int
1466 type T [_] y Int = (y,y)
1467 But it's awkward to do the test, and it doesn't work if the
1468 variable is repeated:
1469 instance C (p,p) Int
1470 type T (_,_) y Int = (y,y)
1471 Even though 'p' is not used on the RHS, we still need to use 'p'
1472 on the LHS to establish the repeated pattern. So to keep it simple
1473 we just require equality.
1474
1475 * For variables in associated type families that are not bound by the class
1476 itself, we do _not_ check if they are over-specific. In other words,
1477 it's perfectly acceptable to have an instance like this:
1478
1479 instance C [p] Int where
1480 type T [p] (Maybe x) Int = x
1481
1482 While the first and third arguments to T are required to be exactly [p] and
1483 Int, respectively, since they are bound by C, the second argument is allowed
1484 to be more specific than just a type variable. Furthermore, it is permissible
1485 to define multiple equations for T that differ only in the non-class-bound
1486 argument:
1487
1488 instance C [p] Int where
1489 type T [p] (Maybe x) Int = x
1490 type T [p] (Either x y) Int = x -> y
1491
1492 We once considered requiring that non-class-bound variables in associated
1493 type family instances be instantiated with distinct type variables. However,
1494 that requirement proved too restrictive in practice, as there were examples
1495 of extremely simple associated type family instances that this check would
1496 reject, and fixing them required tiresome boilerplate in the form of
1497 auxiliary type families. For instance, you would have to define the above
1498 example as:
1499
1500 instance C [p] Int where
1501 type T [p] x Int = CAux x
1502
1503 type family CAux x where
1504 CAux (Maybe x) = x
1505 CAux (Either x y) = x -> y
1506
1507 We decided that this restriction wasn't buying us much, so we opted not
1508 to pursue that design (see also GHC Trac #13398).
1509
1510 Implementation
1511 * Form the mini-envt from the class type variables a,b
1512 to the instance decl types [p],Int: [a->[p], b->Int]
1513
1514 * Look at the tyvars a,x,b of the type family constructor T
1515 (it shares tyvars with the class C)
1516
1517 * Apply the mini-evnt to them, and check that the result is
1518 consistent with the instance types [p] y Int. (where y can be any type, as
1519 it is not scoped over the class type variables.
1520
1521 We make all the instance type variables scope over the
1522 type instances, of course, which picks up non-obvious kinds. Eg
1523 class Foo (a :: k) where
1524 type F a
1525 instance Foo (b :: k -> k) where
1526 type F b = Int
1527 Here the instance is kind-indexed and really looks like
1528 type F (k->k) (b::k->k) = Int
1529 But if the 'b' didn't scope, we would make F's instance too
1530 poly-kinded.
1531 -}
1532
1533 -- | Extra information about the parent instance declaration, needed
1534 -- when type-checking associated types. The 'Class' is the enclosing
1535 -- class, the [TyVar] are the type variable of the instance decl,
1536 -- and and the @VarEnv Type@ maps class variables to their instance
1537 -- types.
1538 type ClsInstInfo = (Class, [TyVar], VarEnv Type)
1539
1540 type AssocInstArgShape = (Maybe Type, Type)
1541 -- AssocInstArgShape is used only for associated family instances
1542 -- (mb_exp, actual)
1543 -- mb_exp = Just ty => this arg corresponds to a class variable
1544 -- = Nothing => it doesn't correspond to a class variable
1545 -- e.g. class C b where
1546 -- type F a b c
1547 -- instance C [x] where
1548 -- type F p [x] q
1549 -- We get [AssocInstArgShape] = [ (Nothing, p)
1550 -- , (Just [x], [x])
1551 -- , (Nothing, q)]
1552
1553 checkConsistentFamInst
1554 :: Maybe ClsInstInfo
1555 -> TyCon -- ^ Family tycon
1556 -> [Type] -- ^ Type patterns from instance
1557 -> SDoc -- ^ pretty-printed user-written instance head
1558 -> TcM ()
1559 -- See Note [Checking consistent instantiation]
1560
1561 checkConsistentFamInst Nothing _ _ _ = return ()
1562 checkConsistentFamInst (Just (clas, inst_tvs, mini_env)) fam_tc at_tys pp_hs_pats
1563 = do { -- Check that the associated type indeed comes from this class
1564 checkTc (Just clas == tyConAssoc_maybe fam_tc)
1565 (badATErr (className clas) (tyConName fam_tc))
1566
1567 -- Check type args first (more comprehensible)
1568 ; checkTc (all check_arg type_shapes) pp_wrong_at_arg
1569
1570 -- And now kind args
1571 ; checkTcM (all check_arg kind_shapes)
1572 (tidy_env2, pp_wrong_at_arg $$ ppSuggestExplicitKinds)
1573
1574 ; traceTc "cfi" (vcat [ ppr inst_tvs
1575 , ppr arg_shapes
1576 , ppr mini_env ]) }
1577 where
1578 arg_shapes :: [AssocInstArgShape]
1579 arg_shapes = [ (lookupVarEnv mini_env fam_tc_tv, at_ty)
1580 | (fam_tc_tv, at_ty) <- tyConTyVars fam_tc `zip` at_tys ]
1581
1582 (kind_shapes, type_shapes) = partitionInvisibles fam_tc snd arg_shapes
1583
1584 check_arg :: AssocInstArgShape -> Bool
1585 check_arg (Just exp_ty, at_ty) = exp_ty `tcEqType` at_ty
1586 check_arg (Nothing, _ ) = True -- Arg position does not correspond
1587 -- to a class variable
1588
1589 pp_wrong_at_arg
1590 = vcat [ text "Type indexes must match class instance head"
1591 , pp_exp_act ]
1592
1593 pp_exp_act
1594 = vcat [ text "Expected:" <+> ppr (mkTyConApp fam_tc expected_args)
1595 , text " Actual:" <+> pp_hs_pats
1596 , sdocWithDynFlags $ \dflags ->
1597 ppWhen (has_poly_args dflags) $
1598 vcat [ text "where the `<tv>' arguments are type variables,"
1599 , text "distinct from each other and from the instance variables" ] ]
1600
1601 -- We need to tidy, since it's possible that expected_args will contain
1602 -- inferred kind variables with names identical to those in at_tys. If we
1603 -- don't, we'll end up with horrible messages like this one (#13972):
1604 --
1605 -- Expected: T (a -> Either a b)
1606 -- Actual: T (a -> Either a b)
1607 (tidy_env1, _) = tidyOpenTypes emptyTidyEnv at_tys
1608 (tidy_env2, expected_args)
1609 = tidyOpenTypes tidy_env1 [ exp_ty `orElse` mk_tv at_ty
1610 | (exp_ty, at_ty) <- arg_shapes ]
1611 mk_tv at_ty = mkTyVarTy (mkTyVar tv_name (typeKind at_ty))
1612 tv_name = mkInternalName (mkAlphaTyVarUnique 1) (mkTyVarOcc "<tv>") noSrcSpan
1613
1614 has_poly_args dflags = any (isNothing . fst) shapes
1615 where
1616 shapes | gopt Opt_PrintExplicitKinds dflags = arg_shapes
1617 | otherwise = type_shapes
1618
1619 badATErr :: Name -> Name -> SDoc
1620 badATErr clas op
1621 = hsep [text "Class", quotes (ppr clas),
1622 text "does not have an associated type", quotes (ppr op)]
1623
1624
1625 {-
1626 ************************************************************************
1627 * *
1628 Checking type instance well-formedness and termination
1629 * *
1630 ************************************************************************
1631 -}
1632
1633 checkValidCoAxiom :: CoAxiom Branched -> TcM ()
1634 checkValidCoAxiom ax@(CoAxiom { co_ax_tc = fam_tc, co_ax_branches = branches })
1635 = do { mapM_ (checkValidCoAxBranch Nothing fam_tc) branch_list
1636 ; foldlM_ check_branch_compat [] branch_list }
1637 where
1638 branch_list = fromBranches branches
1639 injectivity = tyConInjectivityInfo fam_tc
1640
1641 check_branch_compat :: [CoAxBranch] -- previous branches in reverse order
1642 -> CoAxBranch -- current branch
1643 -> TcM [CoAxBranch]-- current branch : previous branches
1644 -- Check for
1645 -- (a) this branch is dominated by previous ones
1646 -- (b) failure of injectivity
1647 check_branch_compat prev_branches cur_branch
1648 | cur_branch `isDominatedBy` prev_branches
1649 = do { addWarnAt NoReason (coAxBranchSpan cur_branch) $
1650 inaccessibleCoAxBranch ax cur_branch
1651 ; return prev_branches }
1652 | otherwise
1653 = do { check_injectivity prev_branches cur_branch
1654 ; return (cur_branch : prev_branches) }
1655
1656 -- Injectivity check: check whether a new (CoAxBranch) can extend
1657 -- already checked equations without violating injectivity
1658 -- annotation supplied by the user.
1659 -- See Note [Verifying injectivity annotation] in FamInstEnv
1660 check_injectivity prev_branches cur_branch
1661 | Injective inj <- injectivity
1662 = do { let conflicts =
1663 fst $ foldl (gather_conflicts inj prev_branches cur_branch)
1664 ([], 0) prev_branches
1665 ; mapM_ (\(err, span) -> setSrcSpan span $ addErr err)
1666 (makeInjectivityErrors ax cur_branch inj conflicts) }
1667 | otherwise
1668 = return ()
1669
1670 gather_conflicts inj prev_branches cur_branch (acc, n) branch
1671 -- n is 0-based index of branch in prev_branches
1672 = case injectiveBranches inj cur_branch branch of
1673 InjectivityUnified ax1 ax2
1674 | ax1 `isDominatedBy` (replace_br prev_branches n ax2)
1675 -> (acc, n + 1)
1676 | otherwise
1677 -> (branch : acc, n + 1)
1678 InjectivityAccepted -> (acc, n + 1)
1679
1680 -- Replace n-th element in the list. Assumes 0-based indexing.
1681 replace_br :: [CoAxBranch] -> Int -> CoAxBranch -> [CoAxBranch]
1682 replace_br brs n br = take n brs ++ [br] ++ drop (n+1) brs
1683
1684
1685 -- Check that a "type instance" is well-formed (which includes decidability
1686 -- unless -XUndecidableInstances is given).
1687 --
1688 checkValidCoAxBranch :: Maybe ClsInstInfo
1689 -> TyCon -> CoAxBranch -> TcM ()
1690 checkValidCoAxBranch mb_clsinfo fam_tc
1691 (CoAxBranch { cab_tvs = tvs, cab_cvs = cvs
1692 , cab_lhs = typats
1693 , cab_rhs = rhs, cab_loc = loc })
1694 = checkValidTyFamEqn mb_clsinfo fam_tc tvs cvs typats rhs pp_lhs loc
1695 where
1696 pp_lhs = ppr (mkTyConApp fam_tc typats)
1697
1698 -- | Do validity checks on a type family equation, including consistency
1699 -- with any enclosing class instance head, termination, and lack of
1700 -- polytypes.
1701 checkValidTyFamEqn :: Maybe ClsInstInfo
1702 -> TyCon -- ^ of the type family
1703 -> [TyVar] -- ^ bound tyvars in the equation
1704 -> [CoVar] -- ^ bound covars in the equation
1705 -> [Type] -- ^ type patterns
1706 -> Type -- ^ rhs
1707 -> SDoc -- ^ user-written LHS
1708 -> SrcSpan
1709 -> TcM ()
1710 checkValidTyFamEqn mb_clsinfo fam_tc tvs cvs typats rhs pp_lhs loc
1711 = setSrcSpan loc $
1712 do { checkValidFamPats mb_clsinfo fam_tc tvs cvs typats [] pp_lhs
1713
1714 -- The argument patterns, and RHS, are all boxed tau types
1715 -- E.g Reject type family F (a :: k1) :: k2
1716 -- type instance F (forall a. a->a) = ...
1717 -- type instance F Int# = ...
1718 -- type instance F Int = forall a. a->a
1719 -- type instance F Int = Int#
1720 -- See Trac #9357
1721 ; checkValidMonoType rhs
1722
1723 -- We have a decidable instance unless otherwise permitted
1724 ; undecidable_ok <- xoptM LangExt.UndecidableInstances
1725 ; unless undecidable_ok $
1726 mapM_ addErrTc (checkFamInstRhs typats (tcTyFamInsts rhs)) }
1727
1728 -- Make sure that each type family application is
1729 -- (1) strictly smaller than the lhs,
1730 -- (2) mentions no type variable more often than the lhs, and
1731 -- (3) does not contain any further type family instances.
1732 --
1733 checkFamInstRhs :: [Type] -- lhs
1734 -> [(TyCon, [Type])] -- type family instances
1735 -> [MsgDoc]
1736 checkFamInstRhs lhsTys famInsts
1737 = mapMaybe check famInsts
1738 where
1739 size = sizeTypes lhsTys
1740 fvs = fvTypes lhsTys
1741 check (tc, tys)
1742 | not (all isTyFamFree tys) = Just (nestedMsg what)
1743 | not (null bad_tvs) = Just (noMoreMsg bad_tvs what)
1744 | size <= sizeTypes tys = Just (smallerMsg what)
1745 | otherwise = Nothing
1746 where
1747 what = text "type family application" <+> quotes (pprType (TyConApp tc tys))
1748 bad_tvs = fvTypes tys \\ fvs
1749
1750 checkValidFamPats :: Maybe ClsInstInfo -> TyCon -> [TyVar] -> [CoVar]
1751 -> [Type] -- ^ patterns the user wrote
1752 -> [Type] -- ^ "extra" patterns from a data instance kind sig
1753 -> SDoc -- ^ pretty-printed user-written instance head
1754 -> TcM ()
1755 -- Patterns in a 'type instance' or 'data instance' decl should
1756 -- a) contain no type family applications
1757 -- (vanilla synonyms are fine, though)
1758 -- b) properly bind all their free type variables
1759 -- e.g. we disallow (Trac #7536)
1760 -- type T a = Int
1761 -- type instance F (T a) = a
1762 -- c) For associated types, are consistently instantiated
1763 checkValidFamPats mb_clsinfo fam_tc tvs cvs user_ty_pats extra_ty_pats pp_hs_pats
1764 = do { mapM_ checkValidTypePat user_ty_pats
1765
1766 ; let unbound_tcvs = filterOut (`elemVarSet` exactTyCoVarsOfTypes user_ty_pats)
1767 (tvs ++ cvs)
1768 ; checkTc (null unbound_tcvs) (famPatErr fam_tc unbound_tcvs user_ty_pats)
1769
1770 -- Check that type patterns match the class instance head
1771 ; checkConsistentFamInst mb_clsinfo fam_tc (user_ty_pats `chkAppend` extra_ty_pats) pp_hs_pats }
1772
1773 checkValidTypePat :: Type -> TcM ()
1774 -- Used for type patterns in class instances,
1775 -- and in type/data family instances
1776 checkValidTypePat pat_ty
1777 = do { -- Check that pat_ty is a monotype
1778 checkValidMonoType pat_ty
1779 -- One could imagine generalising to allow
1780 -- instance C (forall a. a->a)
1781 -- but we don't know what all the consequences might be
1782
1783 -- Ensure that no type family instances occur a type pattern
1784 ; checkTc (isTyFamFree pat_ty) $
1785 tyFamInstIllegalErr pat_ty }
1786
1787 -- Error messages
1788
1789 inaccessibleCoAxBranch :: CoAxiom br -> CoAxBranch -> SDoc
1790 inaccessibleCoAxBranch fi_ax cur_branch
1791 = text "Type family instance equation is overlapped:" $$
1792 nest 2 (pprCoAxBranch fi_ax cur_branch)
1793
1794 tyFamInstIllegalErr :: Type -> SDoc
1795 tyFamInstIllegalErr ty
1796 = hang (text "Illegal type synonym family application in instance" <>
1797 colon) 2 $
1798 ppr ty
1799
1800 nestedMsg :: SDoc -> SDoc
1801 nestedMsg what
1802 = sep [ text "Illegal nested" <+> what
1803 , parens undecidableMsg ]
1804
1805 famPatErr :: TyCon -> [TyVar] -> [Type] -> SDoc
1806 famPatErr fam_tc tvs pats
1807 = hang (text "Family instance purports to bind type variable" <> plural tvs
1808 <+> pprQuotedList tvs)
1809 2 (hang (text "but the real LHS (expanding synonyms) is:")
1810 2 (pprTypeApp fam_tc (map expandTypeSynonyms pats) <+>
1811 text "= ..."))
1812
1813 {-
1814 ************************************************************************
1815 * *
1816 Telescope checking
1817 * *
1818 ************************************************************************
1819
1820 Note [Bad telescopes]
1821 ~~~~~~~~~~~~~~~~~~~~~
1822 Now that we can mix type and kind variables, there are an awful lot of
1823 ways to shoot yourself in the foot. Here are some.
1824
1825 data SameKind :: k -> k -> * -- just to force unification
1826
1827 1. data T1 a k (b :: k) (x :: SameKind a b)
1828
1829 The problem here is that we discover that a and b should have the same
1830 kind. But this kind mentions k, which is bound *after* a.
1831 (Testcase: dependent/should_fail/BadTelescope)
1832
1833 2. data T2 a (c :: Proxy b) (d :: Proxy a) (x :: SameKind b d)
1834
1835 Note that b is not bound. Yet its kind mentions a. Because we have
1836 a nice rule that all implicitly bound variables come before others,
1837 this is bogus. (We could probably figure out to put b between a and c.
1838 But I think this is doing users a disservice, in the long run.)
1839 (Testcase: dependent/should_fail/BadTelescope4)
1840
1841 3. t3 :: forall a. (forall k (b :: k). SameKind a b) -> ()
1842
1843 This is a straightforward skolem escape. Note that a and b need to have
1844 the same kind.
1845 (Testcase: polykinds/T11142)
1846
1847 How do we deal with all of this? For TyCons, we have checkValidTyConTyVars.
1848 That function looks to see if any of the tyConTyVars are repeated, but
1849 it's really a telescope check. It works because all tycons are kind-generalized.
1850 If there is a bad telescope, the kind-generalization will end up generalizing
1851 over a variable bound later in the telescope.
1852
1853 For non-tycons, we do scope checking when we bring tyvars into scope,
1854 in tcImplicitTKBndrs and tcExplicitTKBndrs. Note that we also have to
1855 sort implicit binders into a well-scoped order whenever we have implicit
1856 binders to worry about. This is done in quantifyTyVars and in
1857 tcImplicitTKBndrs.
1858 -}
1859
1860 -- | Check a list of binders to see if they make a valid telescope.
1861 -- The key property we're checking for is scoping. For example:
1862 -- > data SameKind :: k -> k -> *
1863 -- > data X a k (b :: k) (c :: SameKind a b)
1864 -- Kind inference says that a's kind should be k. But that's impossible,
1865 -- because k isn't in scope when a is bound. This check has to come before
1866 -- general validity checking, because once we kind-generalise, this sort
1867 -- of problem is harder to spot (as we'll generalise over the unbound
1868 -- k in a's type.) See also Note [Bad telescopes].
1869 checkValidTelescope :: SDoc -- the original user-written telescope
1870 -> [TyVar] -- explicit vars (not necessarily zonked)
1871 -> SDoc -- note to put at bottom of message
1872 -> TcM ()
1873 checkValidTelescope hs_tvs orig_tvs extra
1874 = discardResult $ checkZonkValidTelescope hs_tvs orig_tvs extra
1875
1876 -- | Like 'checkZonkValidTelescope', but returns the zonked tyvars
1877 checkZonkValidTelescope :: SDoc
1878 -> [TyVar]
1879 -> SDoc
1880 -> TcM [TyVar]
1881 checkZonkValidTelescope hs_tvs orig_tvs extra
1882 = do { orig_tvs <- mapM zonkTyCoVarKind orig_tvs
1883 ; let (_, sorted_tidied_tvs) = tidyTyCoVarBndrs emptyTidyEnv $
1884 toposortTyVars orig_tvs
1885 ; unless (go [] emptyVarSet orig_tvs) $
1886 addErr $
1887 vcat [ hang (text "These kind and type variables:" <+> hs_tvs $$
1888 text "are out of dependency order. Perhaps try this ordering:")
1889 2 (sep (map pprTyVar sorted_tidied_tvs))
1890 , extra ]
1891 ; return orig_tvs }
1892
1893 where
1894 go :: [TyVar] -- misplaced variables
1895 -> TyVarSet -> [TyVar] -> Bool
1896 go errs in_scope [] = null (filter (`elemVarSet` in_scope) errs)
1897 -- report an error only when the variable in the kind is brought
1898 -- into scope later in the telescope. Otherwise, we'll just quantify
1899 -- over it in kindGeneralize, as we should.
1900
1901 go errs in_scope (tv:tvs)
1902 = let bad_tvs = filterOut (`elemVarSet` in_scope) $
1903 tyCoVarsOfTypeList (tyVarKind tv)
1904 in go (bad_tvs ++ errs) (in_scope `extendVarSet` tv) tvs
1905
1906 -- | After inferring kinds of type variables, check to make sure that the
1907 -- inferred kinds any of the type variables bound in a smaller scope.
1908 -- This is a skolem escape check. See also Note [Bad telescopes].
1909 checkValidInferredKinds :: [TyVar] -- ^ vars to check (zonked)
1910 -> TyVarSet -- ^ vars out of scope
1911 -> SDoc -- ^ suffix to error message
1912 -> TcM ()
1913 checkValidInferredKinds orig_kvs out_of_scope extra
1914 = do { let bad_pairs = [ (tv, kv)
1915 | kv <- orig_kvs
1916 , Just tv <- map (lookupVarSet out_of_scope)
1917 (tyCoVarsOfTypeList (tyVarKind kv)) ]
1918 report (tidyTyVarOcc env -> tv, tidyTyVarOcc env -> kv)
1919 = addErr $
1920 text "The kind of variable" <+>
1921 quotes (ppr kv) <> text ", namely" <+>
1922 quotes (ppr (tyVarKind kv)) <> comma $$
1923 text "depends on variable" <+>
1924 quotes (ppr tv) <+> text "from an inner scope" $$
1925 text "Perhaps bind" <+> quotes (ppr kv) <+>
1926 text "sometime after binding" <+>
1927 quotes (ppr tv) $$
1928 extra
1929 ; mapM_ report bad_pairs }
1930
1931 where
1932 (env1, _) = tidyTyCoVarBndrs emptyTidyEnv orig_kvs
1933 (env, _) = tidyTyCoVarBndrs env1 (nonDetEltsUniqSet out_of_scope)
1934 -- It's OK to use nonDetEltsUniqSet here because it's only used for
1935 -- generating the error message
1936
1937 {-
1938 ************************************************************************
1939 * *
1940 \subsection{Auxiliary functions}
1941 * *
1942 ************************************************************************
1943 -}
1944
1945 -- Free variables of a type, retaining repetitions, and expanding synonyms
1946 fvType :: Type -> [TyCoVar]
1947 fvType ty | Just exp_ty <- tcView ty = fvType exp_ty
1948 fvType (TyVarTy tv) = [tv]
1949 fvType (TyConApp _ tys) = fvTypes tys
1950 fvType (LitTy {}) = []
1951 fvType (AppTy fun arg) = fvType fun ++ fvType arg
1952 fvType (FunTy arg res) = fvType arg ++ fvType res
1953 fvType (ForAllTy (TvBndr tv _) ty)
1954 = fvType (tyVarKind tv) ++
1955 filter (/= tv) (fvType ty)
1956 fvType (CastTy ty co) = fvType ty ++ fvCo co
1957 fvType (CoercionTy co) = fvCo co
1958
1959 fvTypes :: [Type] -> [TyVar]
1960 fvTypes tys = concat (map fvType tys)
1961
1962 fvCo :: Coercion -> [TyCoVar]
1963 fvCo (Refl _ ty) = fvType ty
1964 fvCo (TyConAppCo _ _ args) = concatMap fvCo args
1965 fvCo (AppCo co arg) = fvCo co ++ fvCo arg
1966 fvCo (ForAllCo tv h co) = filter (/= tv) (fvCo co) ++ fvCo h
1967 fvCo (FunCo _ co1 co2) = fvCo co1 ++ fvCo co2
1968 fvCo (CoVarCo v) = [v]
1969 fvCo (AxiomInstCo _ _ args) = concatMap fvCo args
1970 fvCo (UnivCo p _ t1 t2) = fvProv p ++ fvType t1 ++ fvType t2
1971 fvCo (SymCo co) = fvCo co
1972 fvCo (TransCo co1 co2) = fvCo co1 ++ fvCo co2
1973 fvCo (NthCo _ co) = fvCo co
1974 fvCo (LRCo _ co) = fvCo co
1975 fvCo (InstCo co arg) = fvCo co ++ fvCo arg
1976 fvCo (CoherenceCo co1 co2) = fvCo co1 ++ fvCo co2
1977 fvCo (KindCo co) = fvCo co
1978 fvCo (SubCo co) = fvCo co
1979 fvCo (AxiomRuleCo _ cs) = concatMap fvCo cs
1980 fvCo (HoleCo h) = pprPanic "fvCo falls into a hole" (ppr h)
1981
1982 fvProv :: UnivCoProvenance -> [TyCoVar]
1983 fvProv UnsafeCoerceProv = []
1984 fvProv (PhantomProv co) = fvCo co
1985 fvProv (ProofIrrelProv co) = fvCo co
1986 fvProv (PluginProv _) = []
1987
1988 sizeType :: Type -> Int
1989 -- Size of a type: the number of variables and constructors
1990 sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty
1991 sizeType (TyVarTy {}) = 1
1992 sizeType (TyConApp _ tys) = sizeTypes tys + 1
1993 sizeType (LitTy {}) = 1
1994 sizeType (AppTy fun arg) = sizeType fun + sizeType arg
1995 sizeType (FunTy arg res) = sizeType arg + sizeType res + 1
1996 sizeType (ForAllTy _ ty) = sizeType ty
1997 sizeType (CastTy ty _) = sizeType ty
1998 sizeType (CoercionTy _) = 1
1999
2000 sizeTypes :: [Type] -> Int
2001 sizeTypes = sum . map sizeType
2002
2003 -- Size of a predicate
2004 --
2005 -- We are considering whether class constraints terminate.
2006 -- Equality constraints and constraints for the implicit
2007 -- parameter class always terminate so it is safe to say "size 0".
2008 -- (Implicit parameter constraints always terminate because
2009 -- there are no instances for them---they are only solved by
2010 -- "local instances" in expressions).
2011 -- See Trac #4200.
2012 sizePred :: PredType -> Int
2013 sizePred ty = goClass ty
2014 where
2015 goClass p = go (classifyPredType p)
2016
2017 go (ClassPred cls tys')
2018 | isTerminatingClass cls = 0
2019 | otherwise = sizeTypes (filterOutInvisibleTypes (classTyCon cls) tys')
2020 go (EqPred {}) = 0
2021 go (IrredPred ty) = sizeType ty
2022
2023 -- | When this says "True", ignore this class constraint during
2024 -- a termination check
2025 isTerminatingClass :: Class -> Bool
2026 isTerminatingClass cls
2027 = isIPClass cls
2028 || cls `hasKey` typeableClassKey
2029 || cls `hasKey` coercibleTyConKey
2030 || cls `hasKey` eqTyConKey
2031 || cls `hasKey` heqTyConKey
2032
2033 -- | Tidy before printing a type
2034 ppr_tidy :: TidyEnv -> Type -> SDoc
2035 ppr_tidy env ty = pprType (tidyType env ty)
2036
2037 allDistinctTyVars :: TyVarSet -> [KindOrType] -> Bool
2038 -- (allDistinctTyVars tvs tys) returns True if tys are
2039 -- a) all tyvars
2040 -- b) all distinct
2041 -- c) disjoint from tvs
2042 allDistinctTyVars _ [] = True
2043 allDistinctTyVars tkvs (ty : tys)
2044 = case getTyVar_maybe ty of
2045 Nothing -> False
2046 Just tv | tv `elemVarSet` tkvs -> False
2047 | otherwise -> allDistinctTyVars (tkvs `extendVarSet` tv) tys