9e23eca1eb57409c27308a90c412009021ec5144
[ghc.git] / compiler / typecheck / TcSimplify.hs
1 {-# LANGUAGE CPP #-}
2
3 module TcSimplify(
4 simplifyInfer, InferMode(..),
5 growThetaTyVars,
6 simplifyAmbiguityCheck,
7 simplifyDefault,
8 simplifyTop, simplifyTopImplic,
9 simplifyInteractive,
10 solveEqualities, solveLocalEqualities, solveLocalEqualitiesX,
11 simplifyWantedsTcM,
12 tcCheckSatisfiability,
13 tcNormalise,
14
15 captureTopConstraints,
16
17 simpl_top,
18
19 promoteTyVar,
20 promoteTyVarSet,
21
22 -- For Rules we need these
23 solveWanteds, solveWantedsAndDrop,
24 approximateWC, runTcSDeriveds
25 ) where
26
27 #include "HsVersions.h"
28
29 import GhcPrelude
30
31 import Bag
32 import Class ( Class, classKey, classTyCon )
33 import DynFlags ( WarningFlag ( Opt_WarnMonomorphism )
34 , WarnReason ( Reason )
35 , DynFlags( solverIterations ) )
36 import HsExpr ( UnboundVar(..) )
37 import Id ( idType, mkLocalId )
38 import Inst
39 import ListSetOps
40 import Name
41 import Outputable
42 import PrelInfo
43 import PrelNames
44 import RdrName ( emptyGlobalRdrEnv )
45 import TcErrors
46 import TcEvidence
47 import TcInteract
48 import TcCanonical ( makeSuperClasses, solveCallStack )
49 import TcMType as TcM
50 import TcRnMonad as TcM
51 import TcSMonad as TcS
52 import TcType
53 import TrieMap () -- DV: for now
54 import Type
55 import TysWiredIn ( liftedRepTy )
56 import Unify ( tcMatchTyKi )
57 import Util
58 import Var
59 import VarSet
60 import UniqSet
61 import BasicTypes ( IntWithInf, intGtLimit )
62 import ErrUtils ( emptyMessages )
63 import qualified GHC.LanguageExtensions as LangExt
64
65 import Control.Monad
66 import Data.Foldable ( toList )
67 import Data.List ( partition )
68 import Data.List.NonEmpty ( NonEmpty(..) )
69 import Maybes ( isJust )
70
71 {-
72 *********************************************************************************
73 * *
74 * External interface *
75 * *
76 *********************************************************************************
77 -}
78
79 captureTopConstraints :: TcM a -> TcM (a, WantedConstraints)
80 -- (captureTopConstraints m) runs m, and returns the type constraints it
81 -- generates plus the constraints produced by static forms inside.
82 -- If it fails with an exception, it reports any insolubles
83 -- (out of scope variables) before doing so
84 -- NB: bring any environments into scope before calling this, so that
85 -- the reportUnsolved has access to the most complete GlobalRdrEnv
86 captureTopConstraints thing_inside
87 = do { static_wc_var <- TcM.newTcRef emptyWC ;
88 ; (mb_res, lie) <- TcM.updGblEnv (\env -> env { tcg_static_wc = static_wc_var } ) $
89 TcM.tryCaptureConstraints thing_inside
90 ; stWC <- TcM.readTcRef static_wc_var
91
92 -- See TcRnMonad Note [Constraints and errors]
93 -- If the thing_inside threw an exception, but generated some insoluble
94 -- constraints, report the latter before propagating the exception
95 -- Otherwise they will be lost altogether
96 ; case mb_res of
97 Right res -> return (res, lie `andWC` stWC)
98 Left {} -> do { _ <- reportUnsolved lie; failM } }
99 -- This call to reportUnsolved is the reason
100 -- this function is here instead of TcRnMonad
101
102 simplifyTopImplic :: Bag Implication -> TcM ()
103 simplifyTopImplic implics
104 = do { empty_binds <- simplifyTop (mkImplicWC implics)
105
106 -- Since all the inputs are implications the returned bindings will be empty
107 ; MASSERT2( isEmptyBag empty_binds, ppr empty_binds )
108
109 ; return () }
110
111 simplifyTop :: WantedConstraints -> TcM (Bag EvBind)
112 -- Simplify top-level constraints
113 -- Usually these will be implications,
114 -- but when there is nothing to quantify we don't wrap
115 -- in a degenerate implication, so we do that here instead
116 simplifyTop wanteds
117 = do { traceTc "simplifyTop {" $ text "wanted = " <+> ppr wanteds
118 ; ((final_wc, unsafe_ol), binds1) <- runTcS $
119 do { final_wc <- simpl_top wanteds
120 ; unsafe_ol <- getSafeOverlapFailures
121 ; return (final_wc, unsafe_ol) }
122 ; traceTc "End simplifyTop }" empty
123
124 ; binds2 <- reportUnsolved final_wc
125
126 ; traceTc "reportUnsolved (unsafe overlapping) {" empty
127 ; unless (isEmptyCts unsafe_ol) $ do {
128 -- grab current error messages and clear, warnAllUnsolved will
129 -- update error messages which we'll grab and then restore saved
130 -- messages.
131 ; errs_var <- getErrsVar
132 ; saved_msg <- TcM.readTcRef errs_var
133 ; TcM.writeTcRef errs_var emptyMessages
134
135 ; warnAllUnsolved $ WC { wc_simple = unsafe_ol
136 , wc_impl = emptyBag }
137
138 ; whyUnsafe <- fst <$> TcM.readTcRef errs_var
139 ; TcM.writeTcRef errs_var saved_msg
140 ; recordUnsafeInfer whyUnsafe
141 }
142 ; traceTc "reportUnsolved (unsafe overlapping) }" empty
143
144 ; return (evBindMapBinds binds1 `unionBags` binds2) }
145
146
147 -- | Type-check a thing that emits only equality constraints, solving any
148 -- constraints we can and re-emitting constraints that we can't. The thing_inside
149 -- should generally bump the TcLevel to make sure that this run of the solver
150 -- doesn't affect anything lying around.
151 solveLocalEqualities :: String -> TcM a -> TcM a
152 solveLocalEqualities callsite thing_inside
153 = do { (wanted, res) <- solveLocalEqualitiesX callsite thing_inside
154 ; emitConstraints wanted
155
156 -- See Note [Fail fast if there are insoluble kind equalities]
157 ; if insolubleWC wanted
158 then failM
159 else return res }
160
161 {- Note [Fail fast if there are insoluble kind equalities]
162 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
163 Rather like in simplifyInfer, fail fast if there is an insoluble
164 constraint. Otherwise we'll just succeed in kind-checking a nonsense
165 type, with a cascade of follow-up errors.
166
167 For example polykinds/T12593, T15577, and many others.
168
169 Take care to ensure that you emit the insoluble constraints before
170 failing, because they are what will ulimately lead to the error
171 messsage!
172 -}
173
174 solveLocalEqualitiesX :: String -> TcM a -> TcM (WantedConstraints, a)
175 solveLocalEqualitiesX callsite thing_inside
176 = do { traceTc "solveLocalEqualitiesX {" (vcat [ text "Called from" <+> text callsite ])
177
178 ; (result, wanted) <- captureConstraints thing_inside
179
180 ; traceTc "solveLocalEqualities: running solver" (ppr wanted)
181 ; residual_wanted <- runTcSEqualities (solveWanteds wanted)
182
183 ; traceTc "solveLocalEqualitiesX end }" $
184 text "residual_wanted =" <+> ppr residual_wanted
185
186 ; return (residual_wanted, result) }
187
188 -- | Type-check a thing that emits only equality constraints, then
189 -- solve those constraints. Fails outright if there is trouble.
190 -- Use this if you're not going to get another crack at solving
191 -- (because, e.g., you're checking a datatype declaration)
192 solveEqualities :: TcM a -> TcM a
193 solveEqualities thing_inside
194 = checkNoErrs $ -- See Note [Fail fast on kind errors]
195 do { lvl <- TcM.getTcLevel
196 ; traceTc "solveEqualities {" (text "level =" <+> ppr lvl)
197
198 ; (result, wanted) <- captureConstraints thing_inside
199
200 ; traceTc "solveEqualities: running solver" $ text "wanted = " <+> ppr wanted
201 ; final_wc <- runTcSEqualities $ simpl_top wanted
202 -- NB: Use simpl_top here so that we potentially default RuntimeRep
203 -- vars to LiftedRep. This is needed to avoid #14991.
204
205 ; traceTc "End solveEqualities }" empty
206 ; reportAllUnsolved final_wc
207 ; return result }
208
209 -- | Simplify top-level constraints, but without reporting any unsolved
210 -- constraints nor unsafe overlapping.
211 simpl_top :: WantedConstraints -> TcS WantedConstraints
212 -- See Note [Top-level Defaulting Plan]
213 simpl_top wanteds
214 = do { wc_first_go <- nestTcS (solveWantedsAndDrop wanteds)
215 -- This is where the main work happens
216 ; try_tyvar_defaulting wc_first_go }
217 where
218 try_tyvar_defaulting :: WantedConstraints -> TcS WantedConstraints
219 try_tyvar_defaulting wc
220 | isEmptyWC wc
221 = return wc
222 | otherwise
223 = do { free_tvs <- TcS.zonkTyCoVarsAndFVList (tyCoVarsOfWCList wc)
224 ; let meta_tvs = filter (isTyVar <&&> isMetaTyVar) free_tvs
225 -- zonkTyCoVarsAndFV: the wc_first_go is not yet zonked
226 -- filter isMetaTyVar: we might have runtime-skolems in GHCi,
227 -- and we definitely don't want to try to assign to those!
228 -- The isTyVar is needed to weed out coercion variables
229
230 ; defaulted <- mapM defaultTyVarTcS meta_tvs -- Has unification side effects
231 ; if or defaulted
232 then do { wc_residual <- nestTcS (solveWanteds wc)
233 -- See Note [Must simplify after defaulting]
234 ; try_class_defaulting wc_residual }
235 else try_class_defaulting wc } -- No defaulting took place
236
237 try_class_defaulting :: WantedConstraints -> TcS WantedConstraints
238 try_class_defaulting wc
239 | isEmptyWC wc
240 = return wc
241 | otherwise -- See Note [When to do type-class defaulting]
242 = do { something_happened <- applyDefaultingRules wc
243 -- See Note [Top-level Defaulting Plan]
244 ; if something_happened
245 then do { wc_residual <- nestTcS (solveWantedsAndDrop wc)
246 ; try_class_defaulting wc_residual }
247 -- See Note [Overview of implicit CallStacks] in TcEvidence
248 else try_callstack_defaulting wc }
249
250 try_callstack_defaulting :: WantedConstraints -> TcS WantedConstraints
251 try_callstack_defaulting wc
252 | isEmptyWC wc
253 = return wc
254 | otherwise
255 = defaultCallStacks wc
256
257 -- | Default any remaining @CallStack@ constraints to empty @CallStack@s.
258 defaultCallStacks :: WantedConstraints -> TcS WantedConstraints
259 -- See Note [Overview of implicit CallStacks] in TcEvidence
260 defaultCallStacks wanteds
261 = do simples <- handle_simples (wc_simple wanteds)
262 mb_implics <- mapBagM handle_implic (wc_impl wanteds)
263 return (wanteds { wc_simple = simples
264 , wc_impl = catBagMaybes mb_implics })
265
266 where
267
268 handle_simples simples
269 = catBagMaybes <$> mapBagM defaultCallStack simples
270
271 handle_implic :: Implication -> TcS (Maybe Implication)
272 -- The Maybe is because solving the CallStack constraint
273 -- may well allow us to discard the implication entirely
274 handle_implic implic
275 | isSolvedStatus (ic_status implic)
276 = return (Just implic)
277 | otherwise
278 = do { wanteds <- setEvBindsTcS (ic_binds implic) $
279 -- defaultCallStack sets a binding, so
280 -- we must set the correct binding group
281 defaultCallStacks (ic_wanted implic)
282 ; setImplicationStatus (implic { ic_wanted = wanteds }) }
283
284 defaultCallStack ct
285 | ClassPred cls tys <- classifyPredType (ctPred ct)
286 , Just {} <- isCallStackPred cls tys
287 = do { solveCallStack (ctEvidence ct) EvCsEmpty
288 ; return Nothing }
289
290 defaultCallStack ct
291 = return (Just ct)
292
293
294 {- Note [Fail fast on kind errors]
295 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
296 solveEqualities is used to solve kind equalities when kind-checking
297 user-written types. If solving fails we should fail outright, rather
298 than just accumulate an error message, for two reasons:
299
300 * A kind-bogus type signature may cause a cascade of knock-on
301 errors if we let it pass
302
303 * More seriously, we don't have a convenient term-level place to add
304 deferred bindings for unsolved kind-equality constraints, so we
305 don't build evidence bindings (by usine reportAllUnsolved). That
306 means that we'll be left with with a type that has coercion holes
307 in it, something like
308 <type> |> co-hole
309 where co-hole is not filled in. Eeek! That un-filled-in
310 hole actually causes GHC to crash with "fvProv falls into a hole"
311 See Trac #11563, #11520, #11516, #11399
312
313 So it's important to use 'checkNoErrs' here!
314
315 Note [When to do type-class defaulting]
316 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
317 In GHC 7.6 and 7.8.2, we did type-class defaulting only if insolubleWC
318 was false, on the grounds that defaulting can't help solve insoluble
319 constraints. But if we *don't* do defaulting we may report a whole
320 lot of errors that would be solved by defaulting; these errors are
321 quite spurious because fixing the single insoluble error means that
322 defaulting happens again, which makes all the other errors go away.
323 This is jolly confusing: Trac #9033.
324
325 So it seems better to always do type-class defaulting.
326
327 However, always doing defaulting does mean that we'll do it in
328 situations like this (Trac #5934):
329 run :: (forall s. GenST s) -> Int
330 run = fromInteger 0
331 We don't unify the return type of fromInteger with the given function
332 type, because the latter involves foralls. So we're left with
333 (Num alpha, alpha ~ (forall s. GenST s) -> Int)
334 Now we do defaulting, get alpha := Integer, and report that we can't
335 match Integer with (forall s. GenST s) -> Int. That's not totally
336 stupid, but perhaps a little strange.
337
338 Another potential alternative would be to suppress *all* non-insoluble
339 errors if there are *any* insoluble errors, anywhere, but that seems
340 too drastic.
341
342 Note [Must simplify after defaulting]
343 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
344 We may have a deeply buried constraint
345 (t:*) ~ (a:Open)
346 which we couldn't solve because of the kind incompatibility, and 'a' is free.
347 Then when we default 'a' we can solve the constraint. And we want to do
348 that before starting in on type classes. We MUST do it before reporting
349 errors, because it isn't an error! Trac #7967 was due to this.
350
351 Note [Top-level Defaulting Plan]
352 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
353 We have considered two design choices for where/when to apply defaulting.
354 (i) Do it in SimplCheck mode only /whenever/ you try to solve some
355 simple constraints, maybe deep inside the context of implications.
356 This used to be the case in GHC 7.4.1.
357 (ii) Do it in a tight loop at simplifyTop, once all other constraints have
358 finished. This is the current story.
359
360 Option (i) had many disadvantages:
361 a) Firstly, it was deep inside the actual solver.
362 b) Secondly, it was dependent on the context (Infer a type signature,
363 or Check a type signature, or Interactive) since we did not want
364 to always start defaulting when inferring (though there is an exception to
365 this, see Note [Default while Inferring]).
366 c) It plainly did not work. Consider typecheck/should_compile/DfltProb2.hs:
367 f :: Int -> Bool
368 f x = const True (\y -> let w :: a -> a
369 w a = const a (y+1)
370 in w y)
371 We will get an implication constraint (for beta the type of y):
372 [untch=beta] forall a. 0 => Num beta
373 which we really cannot default /while solving/ the implication, since beta is
374 untouchable.
375
376 Instead our new defaulting story is to pull defaulting out of the solver loop and
377 go with option (ii), implemented at SimplifyTop. Namely:
378 - First, have a go at solving the residual constraint of the whole
379 program
380 - Try to approximate it with a simple constraint
381 - Figure out derived defaulting equations for that simple constraint
382 - Go round the loop again if you did manage to get some equations
383
384 Now, that has to do with class defaulting. However there exists type variable /kind/
385 defaulting. Again this is done at the top-level and the plan is:
386 - At the top-level, once you had a go at solving the constraint, do
387 figure out /all/ the touchable unification variables of the wanted constraints.
388 - Apply defaulting to their kinds
389
390 More details in Note [DefaultTyVar].
391
392 Note [Safe Haskell Overlapping Instances]
393 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
394 In Safe Haskell, we apply an extra restriction to overlapping instances. The
395 motive is to prevent untrusted code provided by a third-party, changing the
396 behavior of trusted code through type-classes. This is due to the global and
397 implicit nature of type-classes that can hide the source of the dictionary.
398
399 Another way to state this is: if a module M compiles without importing another
400 module N, changing M to import N shouldn't change the behavior of M.
401
402 Overlapping instances with type-classes can violate this principle. However,
403 overlapping instances aren't always unsafe. They are just unsafe when the most
404 selected dictionary comes from untrusted code (code compiled with -XSafe) and
405 overlaps instances provided by other modules.
406
407 In particular, in Safe Haskell at a call site with overlapping instances, we
408 apply the following rule to determine if it is a 'unsafe' overlap:
409
410 1) Most specific instance, I1, defined in an `-XSafe` compiled module.
411 2) I1 is an orphan instance or a MPTC.
412 3) At least one overlapped instance, Ix, is both:
413 A) from a different module than I1
414 B) Ix is not marked `OVERLAPPABLE`
415
416 This is a slightly involved heuristic, but captures the situation of an
417 imported module N changing the behavior of existing code. For example, if
418 condition (2) isn't violated, then the module author M must depend either on a
419 type-class or type defined in N.
420
421 Secondly, when should these heuristics be enforced? We enforced them when the
422 type-class method call site is in a module marked `-XSafe` or `-XTrustworthy`.
423 This allows `-XUnsafe` modules to operate without restriction, and for Safe
424 Haskell inferrence to infer modules with unsafe overlaps as unsafe.
425
426 One alternative design would be to also consider if an instance was imported as
427 a `safe` import or not and only apply the restriction to instances imported
428 safely. However, since instances are global and can be imported through more
429 than one path, this alternative doesn't work.
430
431 Note [Safe Haskell Overlapping Instances Implementation]
432 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
433
434 How is this implemented? It's complicated! So we'll step through it all:
435
436 1) `InstEnv.lookupInstEnv` -- Performs instance resolution, so this is where
437 we check if a particular type-class method call is safe or unsafe. We do this
438 through the return type, `ClsInstLookupResult`, where the last parameter is a
439 list of instances that are unsafe to overlap. When the method call is safe,
440 the list is null.
441
442 2) `TcInteract.matchClassInst` -- This module drives the instance resolution
443 / dictionary generation. The return type is `ClsInstResult`, which either
444 says no instance matched, or one found, and if it was a safe or unsafe
445 overlap.
446
447 3) `TcInteract.doTopReactDict` -- Takes a dictionary / class constraint and
448 tries to resolve it by calling (in part) `matchClassInst`. The resolving
449 mechanism has a work list (of constraints) that it process one at a time. If
450 the constraint can't be resolved, it's added to an inert set. When compiling
451 an `-XSafe` or `-XTrustworthy` module, we follow this approach as we know
452 compilation should fail. These are handled as normal constraint resolution
453 failures from here-on (see step 6).
454
455 Otherwise, we may be inferring safety (or using `-Wunsafe`), and
456 compilation should succeed, but print warnings and/or mark the compiled module
457 as `-XUnsafe`. In this case, we call `insertSafeOverlapFailureTcS` which adds
458 the unsafe (but resolved!) constraint to the `inert_safehask` field of
459 `InertCans`.
460
461 4) `TcSimplify.simplifyTop`:
462 * Call simpl_top, the top-level function for driving the simplifier for
463 constraint resolution.
464
465 * Once finished, call `getSafeOverlapFailures` to retrieve the
466 list of overlapping instances that were successfully resolved,
467 but unsafe. Remember, this is only applicable for generating warnings
468 (`-Wunsafe`) or inferring a module unsafe. `-XSafe` and `-XTrustworthy`
469 cause compilation failure by not resolving the unsafe constraint at all.
470
471 * For unresolved constraints (all types), call `TcErrors.reportUnsolved`,
472 while for resolved but unsafe overlapping dictionary constraints, call
473 `TcErrors.warnAllUnsolved`. Both functions convert constraints into a
474 warning message for the user.
475
476 * In the case of `warnAllUnsolved` for resolved, but unsafe
477 dictionary constraints, we collect the generated warning
478 message (pop it) and call `TcRnMonad.recordUnsafeInfer` to
479 mark the module we are compiling as unsafe, passing the
480 warning message along as the reason.
481
482 5) `TcErrors.*Unsolved` -- Generates error messages for constraints by
483 actually calling `InstEnv.lookupInstEnv` again! Yes, confusing, but all we
484 know is the constraint that is unresolved or unsafe. For dictionary, all we
485 know is that we need a dictionary of type C, but not what instances are
486 available and how they overlap. So we once again call `lookupInstEnv` to
487 figure that out so we can generate a helpful error message.
488
489 6) `TcRnMonad.recordUnsafeInfer` -- Save the unsafe result and reason in an
490 IORef called `tcg_safeInfer`.
491
492 7) `HscMain.tcRnModule'` -- Reads `tcg_safeInfer` after type-checking, calling
493 `HscMain.markUnsafeInfer` (passing the reason along) when safe-inferrence
494 failed.
495
496 Note [No defaulting in the ambiguity check]
497 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
498 When simplifying constraints for the ambiguity check, we use
499 solveWantedsAndDrop, not simpl_top, so that we do no defaulting.
500 Trac #11947 was an example:
501 f :: Num a => Int -> Int
502 This is ambiguous of course, but we don't want to default the
503 (Num alpha) constraint to (Num Int)! Doing so gives a defaulting
504 warning, but no error.
505 -}
506
507 ------------------
508 simplifyAmbiguityCheck :: Type -> WantedConstraints -> TcM ()
509 simplifyAmbiguityCheck ty wanteds
510 = do { traceTc "simplifyAmbiguityCheck {" (text "type = " <+> ppr ty $$ text "wanted = " <+> ppr wanteds)
511 ; (final_wc, _) <- runTcS $ solveWantedsAndDrop wanteds
512 -- NB: no defaulting! See Note [No defaulting in the ambiguity check]
513
514 ; traceTc "End simplifyAmbiguityCheck }" empty
515
516 -- Normally report all errors; but with -XAllowAmbiguousTypes
517 -- report only insoluble ones, since they represent genuinely
518 -- inaccessible code
519 ; allow_ambiguous <- xoptM LangExt.AllowAmbiguousTypes
520 ; traceTc "reportUnsolved(ambig) {" empty
521 ; unless (allow_ambiguous && not (insolubleWC final_wc))
522 (discardResult (reportUnsolved final_wc))
523 ; traceTc "reportUnsolved(ambig) }" empty
524
525 ; return () }
526
527 ------------------
528 simplifyInteractive :: WantedConstraints -> TcM (Bag EvBind)
529 simplifyInteractive wanteds
530 = traceTc "simplifyInteractive" empty >>
531 simplifyTop wanteds
532
533 ------------------
534 simplifyDefault :: ThetaType -- Wanted; has no type variables in it
535 -> TcM () -- Succeeds if the constraint is soluble
536 simplifyDefault theta
537 = do { traceTc "simplifyDefault" empty
538 ; wanteds <- newWanteds DefaultOrigin theta
539 ; unsolved <- runTcSDeriveds (solveWantedsAndDrop (mkSimpleWC wanteds))
540 ; reportAllUnsolved unsolved
541 ; return () }
542
543 ------------------
544 tcCheckSatisfiability :: Bag EvVar -> TcM Bool
545 -- Return True if satisfiable, False if definitely contradictory
546 tcCheckSatisfiability given_ids
547 = do { lcl_env <- TcM.getLclEnv
548 ; let given_loc = mkGivenLoc topTcLevel UnkSkol lcl_env
549 ; (res, _ev_binds) <- runTcS $
550 do { traceTcS "checkSatisfiability {" (ppr given_ids)
551 ; let given_cts = mkGivens given_loc (bagToList given_ids)
552 -- See Note [Superclasses and satisfiability]
553 ; solveSimpleGivens given_cts
554 ; insols <- getInertInsols
555 ; insols <- try_harder insols
556 ; traceTcS "checkSatisfiability }" (ppr insols)
557 ; return (isEmptyBag insols) }
558 ; return res }
559 where
560 try_harder :: Cts -> TcS Cts
561 -- Maybe we have to search up the superclass chain to find
562 -- an unsatisfiable constraint. Example: pmcheck/T3927b.
563 -- At the moment we try just once
564 try_harder insols
565 | not (isEmptyBag insols) -- We've found that it's definitely unsatisfiable
566 = return insols -- Hurrah -- stop now.
567 | otherwise
568 = do { pending_given <- getPendingGivenScs
569 ; new_given <- makeSuperClasses pending_given
570 ; solveSimpleGivens new_given
571 ; getInertInsols }
572
573 -- | Normalise a type as much as possible using the given constraints.
574 -- See @Note [tcNormalise]@.
575 tcNormalise :: Bag EvVar -> Type -> TcM Type
576 tcNormalise given_ids ty
577 = do { lcl_env <- TcM.getLclEnv
578 ; let given_loc = mkGivenLoc topTcLevel UnkSkol lcl_env
579 ; wanted_ct <- mk_wanted_ct
580 ; (res, _ev_binds) <- runTcS $
581 do { traceTcS "tcNormalise {" (ppr given_ids)
582 ; let given_cts = mkGivens given_loc (bagToList given_ids)
583 ; solveSimpleGivens given_cts
584 ; wcs <- solveSimpleWanteds (unitBag wanted_ct)
585 -- It's an invariant that this wc_simple will always be
586 -- a singleton Ct, since that's what we fed in as input.
587 ; let ty' = case bagToList (wc_simple wcs) of
588 (ct:_) -> ctEvPred (ctEvidence ct)
589 cts -> pprPanic "tcNormalise" (ppr cts)
590 ; traceTcS "tcNormalise }" (ppr ty')
591 ; pure ty' }
592 ; return res }
593 where
594 mk_wanted_ct :: TcM Ct
595 mk_wanted_ct = do
596 let occ = mkVarOcc "$tcNorm"
597 name <- newSysName occ
598 let ev = mkLocalId name ty
599 hole = ExprHole $ OutOfScope occ emptyGlobalRdrEnv
600 newHoleCt hole ev ty
601
602 {- Note [Superclasses and satisfiability]
603 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
604 Expand superclasses before starting, because (Int ~ Bool), has
605 (Int ~~ Bool) as a superclass, which in turn has (Int ~N# Bool)
606 as a superclass, and it's the latter that is insoluble. See
607 Note [The equality types story] in TysPrim.
608
609 If we fail to prove unsatisfiability we (arbitrarily) try just once to
610 find superclasses, using try_harder. Reason: we might have a type
611 signature
612 f :: F op (Implements push) => ..
613 where F is a type function. This happened in Trac #3972.
614
615 We could do more than once but we'd have to have /some/ limit: in the
616 the recursive case, we would go on forever in the common case where
617 the constraints /are/ satisfiable (Trac #10592 comment:12!).
618
619 For stratightforard situations without type functions the try_harder
620 step does nothing.
621
622 Note [tcNormalise]
623 ~~~~~~~~~~~~~~~~~~
624 tcNormalise is a rather atypical entrypoint to the constraint solver. Whereas
625 most invocations of the constraint solver are intended to simplify a set of
626 constraints or to decide if a particular set of constraints is satisfiable,
627 the purpose of tcNormalise is to take a type, plus some local constraints, and
628 normalise the type as much as possible with respect to those constraints.
629
630 Why is this useful? As one example, when coverage-checking an EmptyCase
631 expression, it's possible that the type of the scrutinee will only reduce
632 if some local equalities are solved for. See "Wrinkle: Local equalities"
633 in Note [Type normalisation for EmptyCase] in Check.
634
635 To accomplish its stated goal, tcNormalise first feeds the local constraints
636 into solveSimpleGivens, then stuffs the argument type in a CHoleCan, and feeds
637 that singleton Ct into solveSimpleWanteds, which reduces the type in the
638 CHoleCan as much as possible with respect to the local given constraints. When
639 solveSimpleWanteds is finished, we dig out the type from the CHoleCan and
640 return that.
641
642 ***********************************************************************************
643 * *
644 * Inference
645 * *
646 ***********************************************************************************
647
648 Note [Inferring the type of a let-bound variable]
649 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
650 Consider
651 f x = rhs
652
653 To infer f's type we do the following:
654 * Gather the constraints for the RHS with ambient level *one more than*
655 the current one. This is done by the call
656 pushLevelAndCaptureConstraints (tcMonoBinds...)
657 in TcBinds.tcPolyInfer
658
659 * Call simplifyInfer to simplify the constraints and decide what to
660 quantify over. We pass in the level used for the RHS constraints,
661 here called rhs_tclvl.
662
663 This ensures that the implication constraint we generate, if any,
664 has a strictly-increased level compared to the ambient level outside
665 the let binding.
666
667 -}
668
669 -- | How should we choose which constraints to quantify over?
670 data InferMode = ApplyMR -- ^ Apply the monomorphism restriction,
671 -- never quantifying over any constraints
672 | EagerDefaulting -- ^ See Note [TcRnExprMode] in TcRnDriver,
673 -- the :type +d case; this mode refuses
674 -- to quantify over any defaultable constraint
675 | NoRestrictions -- ^ Quantify over any constraint that
676 -- satisfies TcType.pickQuantifiablePreds
677
678 instance Outputable InferMode where
679 ppr ApplyMR = text "ApplyMR"
680 ppr EagerDefaulting = text "EagerDefaulting"
681 ppr NoRestrictions = text "NoRestrictions"
682
683 simplifyInfer :: TcLevel -- Used when generating the constraints
684 -> InferMode
685 -> [TcIdSigInst] -- Any signatures (possibly partial)
686 -> [(Name, TcTauType)] -- Variables to be generalised,
687 -- and their tau-types
688 -> WantedConstraints
689 -> TcM ([TcTyVar], -- Quantify over these type variables
690 [EvVar], -- ... and these constraints (fully zonked)
691 TcEvBinds, -- ... binding these evidence variables
692 WantedConstraints, -- Redidual as-yet-unsolved constraints
693 Bool) -- True <=> the residual constraints are insoluble
694
695 simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds
696 | isEmptyWC wanteds
697 = do { -- When quantifying, we want to preserve any order of variables as they
698 -- appear in partial signatures. cf. decideQuantifiedTyVars
699 let psig_tv_tys = [ mkTyVarTy tv | sig <- partial_sigs
700 , (_,tv) <- sig_inst_skols sig ]
701 psig_theta = [ pred | sig <- partial_sigs
702 , pred <- sig_inst_theta sig ]
703
704 ; gbl_tvs <- tcGetGlobalTyCoVars
705 ; dep_vars <- candidateQTyVarsOfTypes (psig_tv_tys ++ psig_theta ++ map snd name_taus)
706 ; qtkvs <- quantifyTyVars gbl_tvs dep_vars
707 ; traceTc "simplifyInfer: empty WC" (ppr name_taus $$ ppr qtkvs)
708 ; return (qtkvs, [], emptyTcEvBinds, emptyWC, False) }
709
710 | otherwise
711 = do { traceTc "simplifyInfer {" $ vcat
712 [ text "sigs =" <+> ppr sigs
713 , text "binds =" <+> ppr name_taus
714 , text "rhs_tclvl =" <+> ppr rhs_tclvl
715 , text "infer_mode =" <+> ppr infer_mode
716 , text "(unzonked) wanted =" <+> ppr wanteds
717 ]
718
719 ; let psig_theta = concatMap sig_inst_theta partial_sigs
720
721 -- First do full-blown solving
722 -- NB: we must gather up all the bindings from doing
723 -- this solving; hence (runTcSWithEvBinds ev_binds_var).
724 -- And note that since there are nested implications,
725 -- calling solveWanteds will side-effect their evidence
726 -- bindings, so we can't just revert to the input
727 -- constraint.
728
729 ; tc_env <- TcM.getEnv
730 ; ev_binds_var <- TcM.newTcEvBinds
731 ; psig_theta_vars <- mapM TcM.newEvVar psig_theta
732 ; wanted_transformed_incl_derivs
733 <- setTcLevel rhs_tclvl $
734 runTcSWithEvBinds ev_binds_var $
735 do { let loc = mkGivenLoc rhs_tclvl UnkSkol $
736 env_lcl tc_env
737 psig_givens = mkGivens loc psig_theta_vars
738 ; _ <- solveSimpleGivens psig_givens
739 -- See Note [Add signature contexts as givens]
740 ; solveWanteds wanteds }
741
742 -- Find quant_pred_candidates, the predicates that
743 -- we'll consider quantifying over
744 -- NB1: wanted_transformed does not include anything provable from
745 -- the psig_theta; it's just the extra bit
746 -- NB2: We do not do any defaulting when inferring a type, this can lead
747 -- to less polymorphic types, see Note [Default while Inferring]
748 ; wanted_transformed_incl_derivs <- TcM.zonkWC wanted_transformed_incl_derivs
749 ; let definite_error = insolubleWC wanted_transformed_incl_derivs
750 -- See Note [Quantification with errors]
751 -- NB: must include derived errors in this test,
752 -- hence "incl_derivs"
753 wanted_transformed = dropDerivedWC wanted_transformed_incl_derivs
754 quant_pred_candidates
755 | definite_error = []
756 | otherwise = ctsPreds (approximateWC False wanted_transformed)
757
758 -- Decide what type variables and constraints to quantify
759 -- NB: quant_pred_candidates is already fully zonked
760 -- NB: bound_theta are constraints we want to quantify over,
761 -- including the psig_theta, which we always quantify over
762 -- NB: bound_theta are fully zonked
763 ; (qtvs, bound_theta, co_vars) <- decideQuantification infer_mode rhs_tclvl
764 name_taus partial_sigs
765 quant_pred_candidates
766 ; bound_theta_vars <- mapM TcM.newEvVar bound_theta
767
768 -- We must produce bindings for the psig_theta_vars, because we may have
769 -- used them in evidence bindings constructed by solveWanteds earlier
770 -- Easiest way to do this is to emit them as new Wanteds (Trac #14643)
771 ; ct_loc <- getCtLocM AnnOrigin Nothing
772 ; let psig_wanted = [ CtWanted { ctev_pred = idType psig_theta_var
773 , ctev_dest = EvVarDest psig_theta_var
774 , ctev_nosh = WDeriv
775 , ctev_loc = ct_loc }
776 | psig_theta_var <- psig_theta_vars ]
777
778 -- Now construct the residual constraint
779 ; residual_wanted <- mkResidualConstraints rhs_tclvl tc_env ev_binds_var
780 name_taus co_vars qtvs bound_theta_vars
781 (wanted_transformed `andWC` mkSimpleWC psig_wanted)
782
783 -- All done!
784 ; traceTc "} simplifyInfer/produced residual implication for quantification" $
785 vcat [ text "quant_pred_candidates =" <+> ppr quant_pred_candidates
786 , text "psig_theta =" <+> ppr psig_theta
787 , text "bound_theta =" <+> ppr bound_theta
788 , text "qtvs =" <+> ppr qtvs
789 , text "definite_error =" <+> ppr definite_error ]
790
791 ; return ( qtvs, bound_theta_vars, TcEvBinds ev_binds_var
792 , residual_wanted, definite_error ) }
793 -- NB: bound_theta_vars must be fully zonked
794 where
795 partial_sigs = filter isPartialSig sigs
796
797 --------------------
798 mkResidualConstraints :: TcLevel -> Env TcGblEnv TcLclEnv -> EvBindsVar
799 -> [(Name, TcTauType)]
800 -> VarSet -> [TcTyVar] -> [EvVar]
801 -> WantedConstraints -> TcM WantedConstraints
802 -- Emit the remaining constraints from the RHS.
803 -- See Note [Emitting the residual implication in simplifyInfer]
804 mkResidualConstraints rhs_tclvl tc_env ev_binds_var
805 name_taus co_vars qtvs full_theta_vars wanteds
806 | isEmptyWC wanteds
807 = return wanteds
808
809 | otherwise
810 = do { wanted_simple <- TcM.zonkSimples (wc_simple wanteds)
811 ; let (outer_simple, inner_simple) = partitionBag is_mono wanted_simple
812 is_mono ct = isWantedCt ct && ctEvId ct `elemVarSet` co_vars
813
814 ; _ <- promoteTyVarSet (tyCoVarsOfCts outer_simple)
815
816 ; let inner_wanted = wanteds { wc_simple = inner_simple }
817 ; return (WC { wc_simple = outer_simple
818 , wc_impl = mk_implic inner_wanted })}
819 where
820 mk_implic inner_wanted
821 | isEmptyWC inner_wanted
822 = emptyBag
823 | otherwise
824 = unitBag (implicationPrototype { ic_tclvl = rhs_tclvl
825 , ic_skols = qtvs
826 , ic_telescope = Nothing
827 , ic_given = full_theta_vars
828 , ic_wanted = inner_wanted
829 , ic_binds = ev_binds_var
830 , ic_no_eqs = False
831 , ic_info = skol_info
832 , ic_env = tc_env })
833
834 full_theta = map idType full_theta_vars
835 skol_info = InferSkol [ (name, mkSigmaTy [] full_theta ty)
836 | (name, ty) <- name_taus ]
837 -- Don't add the quantified variables here, because
838 -- they are also bound in ic_skols and we want them
839 -- to be tidied uniformly
840
841 --------------------
842 ctsPreds :: Cts -> [PredType]
843 ctsPreds cts = [ ctEvPred ev | ct <- bagToList cts
844 , let ev = ctEvidence ct ]
845
846 {- Note [Emitting the residual implication in simplifyInfer]
847 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
848 Consider
849 f = e
850 where f's type is inferred to be something like (a, Proxy k (Int |> co))
851 and we have an as-yet-unsolved, or perhaps insoluble, constraint
852 [W] co :: Type ~ k
853 We can't form types like (forall co. blah), so we can't generalise over
854 the coercion variable, and hence we can't generalise over things free in
855 its kind, in the case 'k'. But we can still generalise over 'a'. So
856 we'll generalise to
857 f :: forall a. (a, Proxy k (Int |> co))
858 Now we do NOT want to form the residual implication constraint
859 forall a. [W] co :: Type ~ k
860 because then co's eventual binding (which will be a value binding if we
861 use -fdefer-type-errors) won't scope over the entire binding for 'f' (whose
862 type mentions 'co'). Instead, just as we don't generalise over 'co', we
863 should not bury its constraint inside the implication. Instead, we must
864 put it outside.
865
866 That is the reason for the partitionBag in emitResidualConstraints,
867 which takes the CoVars free in the inferred type, and pulls their
868 constraints out. (NB: this set of CoVars should be closed-over-kinds.)
869
870 All rather subtle; see Trac #14584.
871
872 Note [Add signature contexts as givens]
873 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
874 Consider this (Trac #11016):
875 f2 :: (?x :: Int) => _
876 f2 = ?x
877 or this
878 f3 :: a ~ Bool => (a, _)
879 f3 = (True, False)
880 or theis
881 f4 :: (Ord a, _) => a -> Bool
882 f4 x = x==x
883
884 We'll use plan InferGen because there are holes in the type. But:
885 * For f2 we want to have the (?x :: Int) constraint floating around
886 so that the functional dependencies kick in. Otherwise the
887 occurrence of ?x on the RHS produces constraint (?x :: alpha), and
888 we won't unify alpha:=Int.
889 * For f3 we want the (a ~ Bool) available to solve the wanted (a ~ Bool)
890 in the RHS
891 * For f4 we want to use the (Ord a) in the signature to solve the Eq a
892 constraint.
893
894 Solution: in simplifyInfer, just before simplifying the constraints
895 gathered from the RHS, add Given constraints for the context of any
896 type signatures.
897
898 ************************************************************************
899 * *
900 Quantification
901 * *
902 ************************************************************************
903
904 Note [Deciding quantification]
905 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
906 If the monomorphism restriction does not apply, then we quantify as follows:
907
908 * Step 1. Take the global tyvars, and "grow" them using the equality
909 constraints
910 E.g. if x:alpha is in the environment, and alpha ~ [beta] (which can
911 happen because alpha is untouchable here) then do not quantify over
912 beta, because alpha fixes beta, and beta is effectively free in
913 the environment too
914
915 We also account for the monomorphism restriction; if it applies,
916 add the free vars of all the constraints.
917
918 Result is mono_tvs; we will not quantify over these.
919
920 * Step 2. Default any non-mono tyvars (i.e ones that are definitely
921 not going to become further constrained), and re-simplify the
922 candidate constraints.
923
924 Motivation for re-simplification (Trac #7857): imagine we have a
925 constraint (C (a->b)), where 'a :: TYPE l1' and 'b :: TYPE l2' are
926 not free in the envt, and instance forall (a::*) (b::*). (C a) => C
927 (a -> b) The instance doesn't match while l1,l2 are polymorphic, but
928 it will match when we default them to LiftedRep.
929
930 This is all very tiresome.
931
932 * Step 3: decide which variables to quantify over, as follows:
933
934 - Take the free vars of the tau-type (zonked_tau_tvs) and "grow"
935 them using all the constraints. These are tau_tvs_plus
936
937 - Use quantifyTyVars to quantify over (tau_tvs_plus - mono_tvs), being
938 careful to close over kinds, and to skolemise the quantified tyvars.
939 (This actually unifies each quantifies meta-tyvar with a fresh skolem.)
940
941 Result is qtvs.
942
943 * Step 4: Filter the constraints using pickQuantifiablePreds and the
944 qtvs. We have to zonk the constraints first, so they "see" the
945 freshly created skolems.
946
947 -}
948
949 decideQuantification
950 :: InferMode
951 -> TcLevel
952 -> [(Name, TcTauType)] -- Variables to be generalised
953 -> [TcIdSigInst] -- Partial type signatures (if any)
954 -> [PredType] -- Candidate theta; already zonked
955 -> TcM ( [TcTyVar] -- Quantify over these (skolems)
956 , [PredType] -- and this context (fully zonked)
957 , VarSet)
958 -- See Note [Deciding quantification]
959 decideQuantification infer_mode rhs_tclvl name_taus psigs candidates
960 = do { -- Step 1: find the mono_tvs
961 ; (mono_tvs, candidates, co_vars) <- decideMonoTyVars infer_mode
962 name_taus psigs candidates
963
964 -- Step 2: default any non-mono tyvars, and re-simplify
965 -- This step may do some unification, but result candidates is zonked
966 ; candidates <- defaultTyVarsAndSimplify rhs_tclvl mono_tvs candidates
967
968 -- Step 3: decide which kind/type variables to quantify over
969 ; qtvs <- decideQuantifiedTyVars mono_tvs name_taus psigs candidates
970
971 -- Step 4: choose which of the remaining candidate
972 -- predicates to actually quantify over
973 -- NB: decideQuantifiedTyVars turned some meta tyvars
974 -- into quantified skolems, so we have to zonk again
975 ; candidates <- TcM.zonkTcTypes candidates
976 ; psig_theta <- TcM.zonkTcTypes (concatMap sig_inst_theta psigs)
977 ; let quantifiable_candidates
978 = pickQuantifiablePreds (mkVarSet qtvs) candidates
979 -- NB: do /not/ run pickQuantifiablePreds over psig_theta,
980 -- because we always want to quantify over psig_theta, and not
981 -- drop any of them; e.g. CallStack constraints. c.f Trac #14658
982
983 theta = mkMinimalBySCs id $ -- See Note [Minimize by Superclasses]
984 (psig_theta ++ quantifiable_candidates)
985
986 ; traceTc "decideQuantification"
987 (vcat [ text "infer_mode:" <+> ppr infer_mode
988 , text "candidates:" <+> ppr candidates
989 , text "psig_theta:" <+> ppr psig_theta
990 , text "mono_tvs:" <+> ppr mono_tvs
991 , text "co_vars:" <+> ppr co_vars
992 , text "qtvs:" <+> ppr qtvs
993 , text "theta:" <+> ppr theta ])
994 ; return (qtvs, theta, co_vars) }
995
996 ------------------
997 decideMonoTyVars :: InferMode
998 -> [(Name,TcType)]
999 -> [TcIdSigInst]
1000 -> [PredType]
1001 -> TcM (TcTyCoVarSet, [PredType], CoVarSet)
1002 -- Decide which tyvars and covars cannot be generalised:
1003 -- (a) Free in the environment
1004 -- (b) Mentioned in a constraint we can't generalise
1005 -- (c) Connected by an equality to (a) or (b)
1006 -- Also return CoVars that appear free in the final quatified types
1007 -- we can't quantify over these, and we must make sure they are in scope
1008 decideMonoTyVars infer_mode name_taus psigs candidates
1009 = do { (no_quant, maybe_quant) <- pick infer_mode candidates
1010
1011 -- If possible, we quantify over partial-sig qtvs, so they are
1012 -- not mono. Need to zonk them because they are meta-tyvar TyVarTvs
1013 ; psig_qtvs <- mapM zonkTcTyVarToTyVar $
1014 concatMap (map snd . sig_inst_skols) psigs
1015
1016 ; psig_theta <- mapM TcM.zonkTcType $
1017 concatMap sig_inst_theta psigs
1018
1019 ; taus <- mapM (TcM.zonkTcType . snd) name_taus
1020
1021 ; mono_tvs0 <- tcGetGlobalTyCoVars
1022 ; let psig_tys = mkTyVarTys psig_qtvs ++ psig_theta
1023
1024 co_vars = coVarsOfTypes (psig_tys ++ taus)
1025 co_var_tvs = closeOverKinds co_vars
1026 -- The co_var_tvs are tvs mentioned in the types of covars or
1027 -- coercion holes. We can't quantify over these covars, so we
1028 -- must include the variable in their types in the mono_tvs.
1029 -- E.g. If we can't quantify over co :: k~Type, then we can't
1030 -- quantify over k either! Hence closeOverKinds
1031
1032 mono_tvs1 = mono_tvs0 `unionVarSet` co_var_tvs
1033
1034 eq_constraints = filter isEqPred candidates
1035 mono_tvs2 = growThetaTyVars eq_constraints mono_tvs1
1036
1037 constrained_tvs = (growThetaTyVars eq_constraints
1038 (tyCoVarsOfTypes no_quant)
1039 `minusVarSet` mono_tvs2)
1040 `delVarSetList` psig_qtvs
1041 -- constrained_tvs: the tyvars that we are not going to
1042 -- quantify solely because of the moonomorphism restriction
1043 --
1044 -- (`minusVarSet` mono_tvs1`): a type variable is only
1045 -- "constrained" (so that the MR bites) if it is not
1046 -- free in the environment (Trac #13785)
1047 --
1048 -- (`delVarSetList` psig_qtvs): if the user has explicitly
1049 -- asked for quantification, then that request "wins"
1050 -- over the MR. Note: do /not/ delete psig_qtvs from
1051 -- mono_tvs1, because mono_tvs1 cannot under any circumstances
1052 -- be quantified (Trac #14479); see
1053 -- Note [Quantification and partial signatures], Wrinkle 3, 4
1054
1055 mono_tvs = mono_tvs2 `unionVarSet` constrained_tvs
1056
1057 -- Warn about the monomorphism restriction
1058 ; warn_mono <- woptM Opt_WarnMonomorphism
1059 ; when (case infer_mode of { ApplyMR -> warn_mono; _ -> False}) $
1060 warnTc (Reason Opt_WarnMonomorphism)
1061 (constrained_tvs `intersectsVarSet` tyCoVarsOfTypes taus)
1062 mr_msg
1063
1064 ; traceTc "decideMonoTyVars" $ vcat
1065 [ text "mono_tvs0 =" <+> ppr mono_tvs0
1066 , text "mono_tvs1 =" <+> ppr mono_tvs1
1067 , text "no_quant =" <+> ppr no_quant
1068 , text "maybe_quant =" <+> ppr maybe_quant
1069 , text "eq_constraints =" <+> ppr eq_constraints
1070 , text "mono_tvs =" <+> ppr mono_tvs
1071 , text "co_vars =" <+> ppr co_vars ]
1072
1073 ; return (mono_tvs, maybe_quant, co_vars) }
1074 where
1075 pick :: InferMode -> [PredType] -> TcM ([PredType], [PredType])
1076 -- Split the candidates into ones we definitely
1077 -- won't quantify, and ones that we might
1078 pick NoRestrictions cand = return ([], cand)
1079 pick ApplyMR cand = return (cand, [])
1080 pick EagerDefaulting cand = do { os <- xoptM LangExt.OverloadedStrings
1081 ; return (partition (is_int_ct os) cand) }
1082
1083 -- For EagerDefaulting, do not quantify over
1084 -- over any interactive class constraint
1085 is_int_ct ovl_strings pred
1086 | Just (cls, _) <- getClassPredTys_maybe pred
1087 = isInteractiveClass ovl_strings cls
1088 | otherwise
1089 = False
1090
1091 pp_bndrs = pprWithCommas (quotes . ppr . fst) name_taus
1092 mr_msg =
1093 hang (sep [ text "The Monomorphism Restriction applies to the binding"
1094 <> plural name_taus
1095 , text "for" <+> pp_bndrs ])
1096 2 (hsep [ text "Consider giving"
1097 , text (if isSingleton name_taus then "it" else "them")
1098 , text "a type signature"])
1099
1100 -------------------
1101 defaultTyVarsAndSimplify :: TcLevel
1102 -> TyCoVarSet
1103 -> [PredType] -- Assumed zonked
1104 -> TcM [PredType] -- Guaranteed zonked
1105 -- Default any tyvar free in the constraints,
1106 -- and re-simplify in case the defaulting allows further simplification
1107 defaultTyVarsAndSimplify rhs_tclvl mono_tvs candidates
1108 = do { -- Promote any tyvars that we cannot generalise
1109 -- See Note [Promote momomorphic tyvars]
1110 ; traceTc "decideMonoTyVars: promotion:" (ppr mono_tvs)
1111 ; (prom, _) <- promoteTyVarSet mono_tvs
1112
1113 -- Default any kind/levity vars
1114 ; DV {dv_kvs = cand_kvs, dv_tvs = cand_tvs}
1115 <- candidateQTyVarsOfTypes candidates
1116 -- any covars should already be handled by
1117 -- the logic in decideMonoTyVars, which looks at
1118 -- the constraints generated
1119
1120 ; poly_kinds <- xoptM LangExt.PolyKinds
1121 ; default_kvs <- mapM (default_one poly_kinds True)
1122 (dVarSetElems cand_kvs)
1123 ; default_tvs <- mapM (default_one poly_kinds False)
1124 (dVarSetElems (cand_tvs `minusDVarSet` cand_kvs))
1125 ; let some_default = or default_kvs || or default_tvs
1126
1127 ; case () of
1128 _ | some_default -> simplify_cand candidates
1129 | prom -> mapM TcM.zonkTcType candidates
1130 | otherwise -> return candidates
1131 }
1132 where
1133 default_one poly_kinds is_kind_var tv
1134 | not (isMetaTyVar tv)
1135 = return False
1136 | tv `elemVarSet` mono_tvs
1137 = return False
1138 | otherwise
1139 = defaultTyVar (not poly_kinds && is_kind_var) tv
1140
1141 simplify_cand candidates
1142 = do { clone_wanteds <- newWanteds DefaultOrigin candidates
1143 ; WC { wc_simple = simples } <- setTcLevel rhs_tclvl $
1144 simplifyWantedsTcM clone_wanteds
1145 -- Discard evidence; simples is fully zonked
1146
1147 ; let new_candidates = ctsPreds simples
1148 ; traceTc "Simplified after defaulting" $
1149 vcat [ text "Before:" <+> ppr candidates
1150 , text "After:" <+> ppr new_candidates ]
1151 ; return new_candidates }
1152
1153 ------------------
1154 decideQuantifiedTyVars
1155 :: TyCoVarSet -- Monomorphic tyvars
1156 -> [(Name,TcType)] -- Annotated theta and (name,tau) pairs
1157 -> [TcIdSigInst] -- Partial signatures
1158 -> [PredType] -- Candidates, zonked
1159 -> TcM [TyVar]
1160 -- Fix what tyvars we are going to quantify over, and quantify them
1161 decideQuantifiedTyVars mono_tvs name_taus psigs candidates
1162 = do { -- Why psig_tys? We try to quantify over everything free in here
1163 -- See Note [Quantification and partial signatures]
1164 -- Wrinkles 2 and 3
1165 ; psig_tv_tys <- mapM TcM.zonkTcTyVar [ tv | sig <- psigs
1166 , (_,tv) <- sig_inst_skols sig ]
1167 ; psig_theta <- mapM TcM.zonkTcType [ pred | sig <- psigs
1168 , pred <- sig_inst_theta sig ]
1169 ; tau_tys <- mapM (TcM.zonkTcType . snd) name_taus
1170 ; mono_tvs <- TcM.zonkTyCoVarsAndFV mono_tvs
1171
1172 ; let -- Try to quantify over variables free in these types
1173 psig_tys = psig_tv_tys ++ psig_theta
1174 seed_tys = psig_tys ++ tau_tys
1175
1176 -- Now "grow" those seeds to find ones reachable via 'candidates'
1177 grown_tcvs = growThetaTyVars candidates (tyCoVarsOfTypes seed_tys)
1178
1179 -- Now we have to classify them into kind variables and type variables
1180 -- (sigh) just for the benefit of -XNoPolyKinds; see quantifyTyVars
1181 --
1182 -- Keep the psig_tys first, so that candidateQTyVarsOfTypes produces
1183 -- them in that order, so that the final qtvs quantifies in the same
1184 -- order as the partial signatures do (Trac #13524)
1185 ; dv@DV {dv_kvs = cand_kvs, dv_tvs = cand_tvs} <- candidateQTyVarsOfTypes $
1186 psig_tys ++ candidates ++ tau_tys
1187 ; let pick = (`dVarSetIntersectVarSet` grown_tcvs)
1188 dvs_plus = dv { dv_kvs = pick cand_kvs, dv_tvs = pick cand_tvs }
1189
1190 ; traceTc "decideQuantifiedTyVars" (vcat
1191 [ text "candidates =" <+> ppr candidates
1192 , text "tau_tys =" <+> ppr tau_tys
1193 , text "seed_tys =" <+> ppr seed_tys
1194 , text "seed_tcvs =" <+> ppr (tyCoVarsOfTypes seed_tys)
1195 , text "grown_tcvs =" <+> ppr grown_tcvs
1196 , text "dvs =" <+> ppr dvs_plus])
1197
1198 ; quantifyTyVars mono_tvs dvs_plus }
1199
1200 ------------------
1201 growThetaTyVars :: ThetaType -> TyCoVarSet -> TyCoVarSet
1202 -- See Note [Growing the tau-tvs using constraints]
1203 growThetaTyVars theta tcvs
1204 | null theta = tcvs
1205 | otherwise = transCloVarSet mk_next seed_tcvs
1206 where
1207 seed_tcvs = tcvs `unionVarSet` tyCoVarsOfTypes ips
1208 (ips, non_ips) = partition isIPPred theta
1209 -- See Note [Inheriting implicit parameters] in TcType
1210
1211 mk_next :: VarSet -> VarSet -- Maps current set to newly-grown ones
1212 mk_next so_far = foldr (grow_one so_far) emptyVarSet non_ips
1213 grow_one so_far pred tcvs
1214 | pred_tcvs `intersectsVarSet` so_far = tcvs `unionVarSet` pred_tcvs
1215 | otherwise = tcvs
1216 where
1217 pred_tcvs = tyCoVarsOfType pred
1218
1219
1220 {- Note [Promote momomorphic tyvars]
1221 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1222 Promote any type variables that are free in the environment. Eg
1223 f :: forall qtvs. bound_theta => zonked_tau
1224 The free vars of f's type become free in the envt, and hence will show
1225 up whenever 'f' is called. They may currently at rhs_tclvl, but they
1226 had better be unifiable at the outer_tclvl! Example: envt mentions
1227 alpha[1]
1228 tau_ty = beta[2] -> beta[2]
1229 constraints = alpha ~ [beta]
1230 we don't quantify over beta (since it is fixed by envt)
1231 so we must promote it! The inferred type is just
1232 f :: beta -> beta
1233
1234 NB: promoteTyVar ignores coercion variables
1235
1236 Note [Quantification and partial signatures]
1237 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1238 When choosing type variables to quantify, the basic plan is to
1239 quantify over all type variables that are
1240 * free in the tau_tvs, and
1241 * not forced to be monomorphic (mono_tvs),
1242 for example by being free in the environment.
1243
1244 However, in the case of a partial type signature, be doing inference
1245 *in the presence of a type signature*. For example:
1246 f :: _ -> a
1247 f x = ...
1248 or
1249 g :: (Eq _a) => _b -> _b
1250 In both cases we use plan InferGen, and hence call simplifyInfer. But
1251 those 'a' variables are skolems (actually TyVarTvs), and we should be
1252 sure to quantify over them. This leads to several wrinkles:
1253
1254 * Wrinkle 1. In the case of a type error
1255 f :: _ -> Maybe a
1256 f x = True && x
1257 The inferred type of 'f' is f :: Bool -> Bool, but there's a
1258 left-over error of form (HoleCan (Maybe a ~ Bool)). The error-reporting
1259 machine expects to find a binding site for the skolem 'a', so we
1260 add it to the quantified tyvars.
1261
1262 * Wrinkle 2. Consider the partial type signature
1263 f :: (Eq _) => Int -> Int
1264 f x = x
1265 In normal cases that makes sense; e.g.
1266 g :: Eq _a => _a -> _a
1267 g x = x
1268 where the signature makes the type less general than it could
1269 be. But for 'f' we must therefore quantify over the user-annotated
1270 constraints, to get
1271 f :: forall a. Eq a => Int -> Int
1272 (thereby correctly triggering an ambiguity error later). If we don't
1273 we'll end up with a strange open type
1274 f :: Eq alpha => Int -> Int
1275 which isn't ambiguous but is still very wrong.
1276
1277 Bottom line: Try to quantify over any variable free in psig_theta,
1278 just like the tau-part of the type.
1279
1280 * Wrinkle 3 (Trac #13482). Also consider
1281 f :: forall a. _ => Int -> Int
1282 f x = if (undefined :: a) == undefined then x else 0
1283 Here we get an (Eq a) constraint, but it's not mentioned in the
1284 psig_theta nor the type of 'f'. But we still want to quantify
1285 over 'a' even if the monomorphism restriction is on.
1286
1287 * Wrinkle 4 (Trac #14479)
1288 foo :: Num a => a -> a
1289 foo xxx = g xxx
1290 where
1291 g :: forall b. Num b => _ -> b
1292 g y = xxx + y
1293
1294 In the signature for 'g', we cannot quantify over 'b' because it turns out to
1295 get unified with 'a', which is free in g's environment. So we carefully
1296 refrain from bogusly quantifying, in TcSimplify.decideMonoTyVars. We
1297 report the error later, in TcBinds.chooseInferredQuantifiers.
1298
1299 Note [Growing the tau-tvs using constraints]
1300 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1301 (growThetaTyVars insts tvs) is the result of extending the set
1302 of tyvars, tvs, using all conceivable links from pred
1303
1304 E.g. tvs = {a}, preds = {H [a] b, K (b,Int) c, Eq e}
1305 Then growThetaTyVars preds tvs = {a,b,c}
1306
1307 Notice that
1308 growThetaTyVars is conservative if v might be fixed by vs
1309 => v `elem` grow(vs,C)
1310
1311 Note [Quantification with errors]
1312 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1313 If we find that the RHS of the definition has some absolutely-insoluble
1314 constraints (including especially "variable not in scope"), we
1315
1316 * Abandon all attempts to find a context to quantify over,
1317 and instead make the function fully-polymorphic in whatever
1318 type we have found
1319
1320 * Return a flag from simplifyInfer, indicating that we found an
1321 insoluble constraint. This flag is used to suppress the ambiguity
1322 check for the inferred type, which may well be bogus, and which
1323 tends to obscure the real error. This fix feels a bit clunky,
1324 but I failed to come up with anything better.
1325
1326 Reasons:
1327 - Avoid downstream errors
1328 - Do not perform an ambiguity test on a bogus type, which might well
1329 fail spuriously, thereby obfuscating the original insoluble error.
1330 Trac #14000 is an example
1331
1332 I tried an alternative approach: simply failM, after emitting the
1333 residual implication constraint; the exception will be caught in
1334 TcBinds.tcPolyBinds, which gives all the binders in the group the type
1335 (forall a. a). But that didn't work with -fdefer-type-errors, because
1336 the recovery from failM emits no code at all, so there is no function
1337 to run! But -fdefer-type-errors aspires to produce a runnable program.
1338
1339 NB that we must include *derived* errors in the check for insolubles.
1340 Example:
1341 (a::*) ~ Int#
1342 We get an insoluble derived error *~#, and we don't want to discard
1343 it before doing the isInsolubleWC test! (Trac #8262)
1344
1345 Note [Default while Inferring]
1346 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1347 Our current plan is that defaulting only happens at simplifyTop and
1348 not simplifyInfer. This may lead to some insoluble deferred constraints.
1349 Example:
1350
1351 instance D g => C g Int b
1352
1353 constraint inferred = (forall b. 0 => C gamma alpha b) /\ Num alpha
1354 type inferred = gamma -> gamma
1355
1356 Now, if we try to default (alpha := Int) we will be able to refine the implication to
1357 (forall b. 0 => C gamma Int b)
1358 which can then be simplified further to
1359 (forall b. 0 => D gamma)
1360 Finally, we /can/ approximate this implication with (D gamma) and infer the quantified
1361 type: forall g. D g => g -> g
1362
1363 Instead what will currently happen is that we will get a quantified type
1364 (forall g. g -> g) and an implication:
1365 forall g. 0 => (forall b. 0 => C g alpha b) /\ Num alpha
1366
1367 Which, even if the simplifyTop defaults (alpha := Int) we will still be left with an
1368 unsolvable implication:
1369 forall g. 0 => (forall b. 0 => D g)
1370
1371 The concrete example would be:
1372 h :: C g a s => g -> a -> ST s a
1373 f (x::gamma) = (\_ -> x) (runST (h x (undefined::alpha)) + 1)
1374
1375 But it is quite tedious to do defaulting and resolve the implication constraints, and
1376 we have not observed code breaking because of the lack of defaulting in inference, so
1377 we don't do it for now.
1378
1379
1380
1381 Note [Minimize by Superclasses]
1382 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1383 When we quantify over a constraint, in simplifyInfer we need to
1384 quantify over a constraint that is minimal in some sense: For
1385 instance, if the final wanted constraint is (Eq alpha, Ord alpha),
1386 we'd like to quantify over Ord alpha, because we can just get Eq alpha
1387 from superclass selection from Ord alpha. This minimization is what
1388 mkMinimalBySCs does. Then, simplifyInfer uses the minimal constraint
1389 to check the original wanted.
1390
1391
1392 Note [Avoid unnecessary constraint simplification]
1393 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1394 -------- NB NB NB (Jun 12) -------------
1395 This note not longer applies; see the notes with Trac #4361.
1396 But I'm leaving it in here so we remember the issue.)
1397 ----------------------------------------
1398 When inferring the type of a let-binding, with simplifyInfer,
1399 try to avoid unnecessarily simplifying class constraints.
1400 Doing so aids sharing, but it also helps with delicate
1401 situations like
1402
1403 instance C t => C [t] where ..
1404
1405 f :: C [t] => ....
1406 f x = let g y = ...(constraint C [t])...
1407 in ...
1408 When inferring a type for 'g', we don't want to apply the
1409 instance decl, because then we can't satisfy (C t). So we
1410 just notice that g isn't quantified over 't' and partition
1411 the constraints before simplifying.
1412
1413 This only half-works, but then let-generalisation only half-works.
1414
1415 *********************************************************************************
1416 * *
1417 * Main Simplifier *
1418 * *
1419 ***********************************************************************************
1420
1421 -}
1422
1423 simplifyWantedsTcM :: [CtEvidence] -> TcM WantedConstraints
1424 -- Solve the specified Wanted constraints
1425 -- Discard the evidence binds
1426 -- Discards all Derived stuff in result
1427 -- Postcondition: fully zonked and unflattened constraints
1428 simplifyWantedsTcM wanted
1429 = do { traceTc "simplifyWantedsTcM {" (ppr wanted)
1430 ; (result, _) <- runTcS (solveWantedsAndDrop (mkSimpleWC wanted))
1431 ; result <- TcM.zonkWC result
1432 ; traceTc "simplifyWantedsTcM }" (ppr result)
1433 ; return result }
1434
1435 solveWantedsAndDrop :: WantedConstraints -> TcS WantedConstraints
1436 -- Since solveWanteds returns the residual WantedConstraints,
1437 -- it should always be called within a runTcS or something similar,
1438 -- Result is not zonked
1439 solveWantedsAndDrop wanted
1440 = do { wc <- solveWanteds wanted
1441 ; return (dropDerivedWC wc) }
1442
1443 solveWanteds :: WantedConstraints -> TcS WantedConstraints
1444 -- so that the inert set doesn't mindlessly propagate.
1445 -- NB: wc_simples may be wanted /or/ derived now
1446 solveWanteds wc@(WC { wc_simple = simples, wc_impl = implics })
1447 = do { cur_lvl <- TcS.getTcLevel
1448 ; traceTcS "solveWanteds {" $
1449 vcat [ text "Level =" <+> ppr cur_lvl
1450 , ppr wc ]
1451
1452 ; wc1 <- solveSimpleWanteds simples
1453 -- Any insoluble constraints are in 'simples' and so get rewritten
1454 -- See Note [Rewrite insolubles] in TcSMonad
1455
1456 ; (floated_eqs, implics2) <- solveNestedImplications $
1457 implics `unionBags` wc_impl wc1
1458
1459 ; dflags <- getDynFlags
1460 ; final_wc <- simpl_loop 0 (solverIterations dflags) floated_eqs
1461 (wc1 { wc_impl = implics2 })
1462
1463 ; ev_binds_var <- getTcEvBindsVar
1464 ; bb <- TcS.getTcEvBindsMap ev_binds_var
1465 ; traceTcS "solveWanteds }" $
1466 vcat [ text "final wc =" <+> ppr final_wc
1467 , text "current evbinds =" <+> ppr (evBindMapBinds bb) ]
1468
1469 ; return final_wc }
1470
1471 simpl_loop :: Int -> IntWithInf -> Cts
1472 -> WantedConstraints -> TcS WantedConstraints
1473 simpl_loop n limit floated_eqs wc@(WC { wc_simple = simples })
1474 | n `intGtLimit` limit
1475 = do { -- Add an error (not a warning) if we blow the limit,
1476 -- Typically if we blow the limit we are going to report some other error
1477 -- (an unsolved constraint), and we don't want that error to suppress
1478 -- the iteration limit warning!
1479 addErrTcS (hang (text "solveWanteds: too many iterations"
1480 <+> parens (text "limit =" <+> ppr limit))
1481 2 (vcat [ text "Unsolved:" <+> ppr wc
1482 , ppUnless (isEmptyBag floated_eqs) $
1483 text "Floated equalities:" <+> ppr floated_eqs
1484 , text "Set limit with -fconstraint-solver-iterations=n; n=0 for no limit"
1485 ]))
1486 ; return wc }
1487
1488 | not (isEmptyBag floated_eqs)
1489 = simplify_again n limit True (wc { wc_simple = floated_eqs `unionBags` simples })
1490 -- Put floated_eqs first so they get solved first
1491 -- NB: the floated_eqs may include /derived/ equalities
1492 -- arising from fundeps inside an implication
1493
1494 | superClassesMightHelp wc
1495 = -- We still have unsolved goals, and apparently no way to solve them,
1496 -- so try expanding superclasses at this level, both Given and Wanted
1497 do { pending_given <- getPendingGivenScs
1498 ; let (pending_wanted, simples1) = getPendingWantedScs simples
1499 ; if null pending_given && null pending_wanted
1500 then return wc -- After all, superclasses did not help
1501 else
1502 do { new_given <- makeSuperClasses pending_given
1503 ; new_wanted <- makeSuperClasses pending_wanted
1504 ; solveSimpleGivens new_given -- Add the new Givens to the inert set
1505 ; simplify_again n limit (null pending_given)
1506 wc { wc_simple = simples1 `unionBags` listToBag new_wanted } } }
1507
1508 | otherwise
1509 = return wc
1510
1511 simplify_again :: Int -> IntWithInf -> Bool
1512 -> WantedConstraints -> TcS WantedConstraints
1513 -- We have definitely decided to have another go at solving
1514 -- the wanted constraints (we have tried at least once already
1515 simplify_again n limit no_new_given_scs
1516 wc@(WC { wc_simple = simples, wc_impl = implics })
1517 = do { csTraceTcS $
1518 text "simpl_loop iteration=" <> int n
1519 <+> (parens $ hsep [ text "no new given superclasses =" <+> ppr no_new_given_scs <> comma
1520 , int (lengthBag simples) <+> text "simples to solve" ])
1521 ; traceTcS "simpl_loop: wc =" (ppr wc)
1522
1523 ; (unifs1, wc1) <- reportUnifications $
1524 solveSimpleWanteds $
1525 simples
1526
1527 -- See Note [Cutting off simpl_loop]
1528 -- We have already tried to solve the nested implications once
1529 -- Try again only if we have unified some meta-variables
1530 -- (which is a bit like adding more givens), or we have some
1531 -- new Given superclasses
1532 ; let new_implics = wc_impl wc1
1533 ; if unifs1 == 0 &&
1534 no_new_given_scs &&
1535 isEmptyBag new_implics
1536
1537 then -- Do not even try to solve the implications
1538 simpl_loop (n+1) limit emptyBag (wc1 { wc_impl = implics })
1539
1540 else -- Try to solve the implications
1541 do { (floated_eqs2, implics2) <- solveNestedImplications $
1542 implics `unionBags` new_implics
1543 ; simpl_loop (n+1) limit floated_eqs2 (wc1 { wc_impl = implics2 })
1544 } }
1545
1546 solveNestedImplications :: Bag Implication
1547 -> TcS (Cts, Bag Implication)
1548 -- Precondition: the TcS inerts may contain unsolved simples which have
1549 -- to be converted to givens before we go inside a nested implication.
1550 solveNestedImplications implics
1551 | isEmptyBag implics
1552 = return (emptyBag, emptyBag)
1553 | otherwise
1554 = do { traceTcS "solveNestedImplications starting {" empty
1555 ; (floated_eqs_s, unsolved_implics) <- mapAndUnzipBagM solveImplication implics
1556 ; let floated_eqs = concatBag floated_eqs_s
1557
1558 -- ... and we are back in the original TcS inerts
1559 -- Notice that the original includes the _insoluble_simples so it was safe to ignore
1560 -- them in the beginning of this function.
1561 ; traceTcS "solveNestedImplications end }" $
1562 vcat [ text "all floated_eqs =" <+> ppr floated_eqs
1563 , text "unsolved_implics =" <+> ppr unsolved_implics ]
1564
1565 ; return (floated_eqs, catBagMaybes unsolved_implics) }
1566
1567 solveImplication :: Implication -- Wanted
1568 -> TcS (Cts, -- All wanted or derived floated equalities: var = type
1569 Maybe Implication) -- Simplified implication (empty or singleton)
1570 -- Precondition: The TcS monad contains an empty worklist and given-only inerts
1571 -- which after trying to solve this implication we must restore to their original value
1572 solveImplication imp@(Implic { ic_tclvl = tclvl
1573 , ic_binds = ev_binds_var
1574 , ic_skols = skols
1575 , ic_given = given_ids
1576 , ic_wanted = wanteds
1577 , ic_info = info
1578 , ic_status = status })
1579 | isSolvedStatus status
1580 = return (emptyCts, Just imp) -- Do nothing
1581
1582 | otherwise -- Even for IC_Insoluble it is worth doing more work
1583 -- The insoluble stuff might be in one sub-implication
1584 -- and other unsolved goals in another; and we want to
1585 -- solve the latter as much as possible
1586 = do { inerts <- getTcSInerts
1587 ; traceTcS "solveImplication {" (ppr imp $$ text "Inerts" <+> ppr inerts)
1588
1589 -- commented out; see `where` clause below
1590 -- ; when debugIsOn check_tc_level
1591
1592 -- Solve the nested constraints
1593 ; (no_given_eqs, given_insols, residual_wanted)
1594 <- nestImplicTcS ev_binds_var tclvl $
1595 do { let loc = mkGivenLoc tclvl info (implicLclEnv imp)
1596 givens = mkGivens loc given_ids
1597 ; solveSimpleGivens givens
1598
1599 ; residual_wanted <- solveWanteds wanteds
1600 -- solveWanteds, *not* solveWantedsAndDrop, because
1601 -- we want to retain derived equalities so we can float
1602 -- them out in floatEqualities
1603
1604 ; (no_eqs, given_insols) <- getNoGivenEqs tclvl skols
1605 -- Call getNoGivenEqs /after/ solveWanteds, because
1606 -- solveWanteds can augment the givens, via expandSuperClasses,
1607 -- to reveal given superclass equalities
1608
1609 ; return (no_eqs, given_insols, residual_wanted) }
1610
1611 ; (floated_eqs, residual_wanted)
1612 <- floatEqualities skols given_ids ev_binds_var
1613 no_given_eqs residual_wanted
1614
1615 ; traceTcS "solveImplication 2"
1616 (ppr given_insols $$ ppr residual_wanted)
1617 ; let final_wanted = residual_wanted `addInsols` given_insols
1618 -- Don't lose track of the insoluble givens,
1619 -- which signal unreachable code; put them in ic_wanted
1620
1621 ; res_implic <- setImplicationStatus (imp { ic_no_eqs = no_given_eqs
1622 , ic_wanted = final_wanted })
1623
1624 ; evbinds <- TcS.getTcEvBindsMap ev_binds_var
1625 ; tcvs <- TcS.getTcEvTyCoVars ev_binds_var
1626 ; traceTcS "solveImplication end }" $ vcat
1627 [ text "no_given_eqs =" <+> ppr no_given_eqs
1628 , text "floated_eqs =" <+> ppr floated_eqs
1629 , text "res_implic =" <+> ppr res_implic
1630 , text "implication evbinds =" <+> ppr (evBindMapBinds evbinds)
1631 , text "implication tvcs =" <+> ppr tcvs ]
1632
1633 ; return (floated_eqs, res_implic) }
1634
1635 where
1636 -- TcLevels must be strictly increasing (see (ImplicInv) in
1637 -- Note [TcLevel and untouchable type variables] in TcType),
1638 -- and in fact I thinkthey should always increase one level at a time.
1639
1640 -- Though sensible, this check causes lots of testsuite failures. It is
1641 -- remaining commented out for now.
1642 {-
1643 check_tc_level = do { cur_lvl <- TcS.getTcLevel
1644 ; MASSERT2( tclvl == pushTcLevel cur_lvl , text "Cur lvl =" <+> ppr cur_lvl $$ text "Imp lvl =" <+> ppr tclvl ) }
1645 -}
1646
1647 ----------------------
1648 setImplicationStatus :: Implication -> TcS (Maybe Implication)
1649 -- Finalise the implication returned from solveImplication:
1650 -- * Set the ic_status field
1651 -- * Trim the ic_wanted field to remove Derived constraints
1652 -- Precondition: the ic_status field is not already IC_Solved
1653 -- Return Nothing if we can discard the implication altogether
1654 setImplicationStatus implic@(Implic { ic_status = status
1655 , ic_info = info
1656 , ic_wanted = wc
1657 , ic_given = givens })
1658 | ASSERT2( not (isSolvedStatus status ), ppr info )
1659 -- Precondition: we only set the status if it is not already solved
1660 not (isSolvedWC pruned_wc)
1661 = do { traceTcS "setImplicationStatus(not-all-solved) {" (ppr implic)
1662
1663 ; implic <- neededEvVars implic
1664
1665 ; let new_status | insolubleWC pruned_wc = IC_Insoluble
1666 | otherwise = IC_Unsolved
1667 new_implic = implic { ic_status = new_status
1668 , ic_wanted = pruned_wc }
1669
1670 ; traceTcS "setImplicationStatus(not-all-solved) }" (ppr new_implic)
1671
1672 ; return $ Just new_implic }
1673
1674 | otherwise -- Everything is solved
1675 -- Set status to IC_Solved,
1676 -- and compute the dead givens and outer needs
1677 -- See Note [Tracking redundant constraints]
1678 = do { traceTcS "setImplicationStatus(all-solved) {" (ppr implic)
1679
1680 ; implic@(Implic { ic_need_inner = need_inner
1681 , ic_need_outer = need_outer }) <- neededEvVars implic
1682
1683 ; bad_telescope <- checkBadTelescope implic
1684
1685 ; let dead_givens | warnRedundantGivens info
1686 = filterOut (`elemVarSet` need_inner) givens
1687 | otherwise = [] -- None to report
1688
1689 discard_entire_implication -- Can we discard the entire implication?
1690 = null dead_givens -- No warning from this implication
1691 && not bad_telescope
1692 && isEmptyWC pruned_wc -- No live children
1693 && isEmptyVarSet need_outer -- No needed vars to pass up to parent
1694
1695 final_status
1696 | bad_telescope = IC_BadTelescope
1697 | otherwise = IC_Solved { ics_dead = dead_givens }
1698 final_implic = implic { ic_status = final_status
1699 , ic_wanted = pruned_wc }
1700
1701 ; traceTcS "setImplicationStatus(all-solved) }" $
1702 vcat [ text "discard:" <+> ppr discard_entire_implication
1703 , text "new_implic:" <+> ppr final_implic ]
1704
1705 ; return $ if discard_entire_implication
1706 then Nothing
1707 else Just final_implic }
1708 where
1709 WC { wc_simple = simples, wc_impl = implics } = wc
1710
1711 pruned_simples = dropDerivedSimples simples
1712 pruned_implics = filterBag keep_me implics
1713 pruned_wc = WC { wc_simple = pruned_simples
1714 , wc_impl = pruned_implics }
1715
1716 keep_me :: Implication -> Bool
1717 keep_me ic
1718 | IC_Solved { ics_dead = dead_givens } <- ic_status ic
1719 -- Fully solved
1720 , null dead_givens -- No redundant givens to report
1721 , isEmptyBag (wc_impl (ic_wanted ic))
1722 -- And no children that might have things to report
1723 = False -- Tnen we don't need to keep it
1724 | otherwise
1725 = True -- Otherwise, keep it
1726
1727 checkBadTelescope :: Implication -> TcS Bool
1728 -- True <=> the skolems form a bad telescope
1729 -- See Note [Keeping scoped variables in order: Explicit] in TcHsType
1730 checkBadTelescope (Implic { ic_telescope = m_telescope
1731 , ic_skols = skols })
1732 | isJust m_telescope
1733 = do{ skols <- mapM TcS.zonkTyCoVarKind skols
1734 ; return (go emptyVarSet (reverse skols))}
1735
1736 | otherwise
1737 = return False
1738
1739 where
1740 go :: TyVarSet -- skolems that appear *later* than the current ones
1741 -> [TcTyVar] -- ordered skolems, in reverse order
1742 -> Bool -- True <=> there is an out-of-order skolem
1743 go _ [] = False
1744 go later_skols (one_skol : earlier_skols)
1745 | tyCoVarsOfType (tyVarKind one_skol) `intersectsVarSet` later_skols
1746 = True
1747 | otherwise
1748 = go (later_skols `extendVarSet` one_skol) earlier_skols
1749
1750 warnRedundantGivens :: SkolemInfo -> Bool
1751 warnRedundantGivens (SigSkol ctxt _ _)
1752 = case ctxt of
1753 FunSigCtxt _ warn_redundant -> warn_redundant
1754 ExprSigCtxt -> True
1755 _ -> False
1756
1757 -- To think about: do we want to report redundant givens for
1758 -- pattern synonyms, PatSynSigSkol? c.f Trac #9953, comment:21.
1759 warnRedundantGivens (InstSkol {}) = True
1760 warnRedundantGivens _ = False
1761
1762 neededEvVars :: Implication -> TcS Implication
1763 -- Find all the evidence variables that are "needed",
1764 -- and delete dead evidence bindings
1765 -- See Note [Tracking redundant constraints]
1766 -- See Note [Delete dead Given evidence bindings]
1767 --
1768 -- - Start from initial_seeds (from nested implications)
1769 --
1770 -- - Add free vars of RHS of all Wanted evidence bindings
1771 -- and coercion variables accumulated in tcvs (all Wanted)
1772 --
1773 -- - Generate 'needed', the needed set of EvVars, by doing transitive
1774 -- closure through Given bindings
1775 -- e.g. Needed {a,b}
1776 -- Given a = sc_sel a2
1777 -- Then a2 is needed too
1778 --
1779 -- - Prune out all Given bindings that are not needed
1780 --
1781 -- - From the 'needed' set, delete ev_bndrs, the binders of the
1782 -- evidence bindings, to give the final needed variables
1783 --
1784 neededEvVars implic@(Implic { ic_given = givens
1785 , ic_binds = ev_binds_var
1786 , ic_wanted = WC { wc_impl = implics }
1787 , ic_need_inner = old_needs })
1788 = do { ev_binds <- TcS.getTcEvBindsMap ev_binds_var
1789 ; tcvs <- TcS.getTcEvTyCoVars ev_binds_var
1790
1791 ; let seeds1 = foldrBag add_implic_seeds old_needs implics
1792 seeds2 = foldEvBindMap add_wanted seeds1 ev_binds
1793 seeds3 = seeds2 `unionVarSet` tcvs
1794 need_inner = findNeededEvVars ev_binds seeds3
1795 live_ev_binds = filterEvBindMap (needed_ev_bind need_inner) ev_binds
1796 need_outer = foldEvBindMap del_ev_bndr need_inner live_ev_binds
1797 `delVarSetList` givens
1798
1799 ; TcS.setTcEvBindsMap ev_binds_var live_ev_binds
1800 -- See Note [Delete dead Given evidence bindings]
1801
1802 ; traceTcS "neededEvVars" $
1803 vcat [ text "old_needs:" <+> ppr old_needs
1804 , text "seeds3:" <+> ppr seeds3
1805 , text "tcvs:" <+> ppr tcvs
1806 , text "ev_binds:" <+> ppr ev_binds
1807 , text "live_ev_binds:" <+> ppr live_ev_binds ]
1808
1809 ; return (implic { ic_need_inner = need_inner
1810 , ic_need_outer = need_outer }) }
1811 where
1812 add_implic_seeds (Implic { ic_need_outer = needs }) acc
1813 = needs `unionVarSet` acc
1814
1815 needed_ev_bind needed (EvBind { eb_lhs = ev_var
1816 , eb_is_given = is_given })
1817 | is_given = ev_var `elemVarSet` needed
1818 | otherwise = True -- Keep all wanted bindings
1819
1820 del_ev_bndr :: EvBind -> VarSet -> VarSet
1821 del_ev_bndr (EvBind { eb_lhs = v }) needs = delVarSet needs v
1822
1823 add_wanted :: EvBind -> VarSet -> VarSet
1824 add_wanted (EvBind { eb_is_given = is_given, eb_rhs = rhs }) needs
1825 | is_given = needs -- Add the rhs vars of the Wanted bindings only
1826 | otherwise = evVarsOfTerm rhs `unionVarSet` needs
1827
1828
1829 {- Note [Delete dead Given evidence bindings]
1830 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1831 As a result of superclass expansion, we speculatively
1832 generate evidence bindings for Givens. E.g.
1833 f :: (a ~ b) => a -> b -> Bool
1834 f x y = ...
1835 We'll have
1836 [G] d1 :: (a~b)
1837 and we'll specuatively generate the evidence binding
1838 [G] d2 :: (a ~# b) = sc_sel d
1839
1840 Now d2 is available for solving. But it may not be needed! Usually
1841 such dead superclass selections will eventually be dropped as dead
1842 code, but:
1843
1844 * It won't always be dropped (Trac #13032). In the case of an
1845 unlifted-equality superclass like d2 above, we generate
1846 case heq_sc d1 of d2 -> ...
1847 and we can't (in general) drop that case exrpession in case
1848 d1 is bottom. So it's technically unsound to have added it
1849 in the first place.
1850
1851 * Simply generating all those extra superclasses can generate lots of
1852 code that has to be zonked, only to be discarded later. Better not
1853 to generate it in the first place.
1854
1855 Moreover, if we simplify this implication more than once
1856 (e.g. because we can't solve it completely on the first iteration
1857 of simpl_looop), we'll generate all the same bindings AGAIN!
1858
1859 Easy solution: take advantage of the work we are doing to track dead
1860 (unused) Givens, and use it to prune the Given bindings too. This is
1861 all done by neededEvVars.
1862
1863 This led to a remarkable 25% overall compiler allocation decrease in
1864 test T12227.
1865
1866 But we don't get to discard all redundant equality superclasses, alas;
1867 see Trac #15205.
1868
1869 Note [Tracking redundant constraints]
1870 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1871 With Opt_WarnRedundantConstraints, GHC can report which
1872 constraints of a type signature (or instance declaration) are
1873 redundant, and can be omitted. Here is an overview of how it
1874 works:
1875
1876 ----- What is a redundant constraint?
1877
1878 * The things that can be redundant are precisely the Given
1879 constraints of an implication.
1880
1881 * A constraint can be redundant in two different ways:
1882 a) It is implied by other givens. E.g.
1883 f :: (Eq a, Ord a) => blah -- Eq a unnecessary
1884 g :: (Eq a, a~b, Eq b) => blah -- Either Eq a or Eq b unnecessary
1885 b) It is not needed by the Wanted constraints covered by the
1886 implication E.g.
1887 f :: Eq a => a -> Bool
1888 f x = True -- Equality not used
1889
1890 * To find (a), when we have two Given constraints,
1891 we must be careful to drop the one that is a naked variable (if poss).
1892 So if we have
1893 f :: (Eq a, Ord a) => blah
1894 then we may find [G] sc_sel (d1::Ord a) :: Eq a
1895 [G] d2 :: Eq a
1896 We want to discard d2 in favour of the superclass selection from
1897 the Ord dictionary. This is done by TcInteract.solveOneFromTheOther
1898 See Note [Replacement vs keeping].
1899
1900 * To find (b) we need to know which evidence bindings are 'wanted';
1901 hence the eb_is_given field on an EvBind.
1902
1903 ----- How tracking works
1904
1905 * The ic_need fields of an Implic records in-scope (given) evidence
1906 variables bound by the context, that were needed to solve this
1907 implication (so far). See the declaration of Implication.
1908
1909 * When the constraint solver finishes solving all the wanteds in
1910 an implication, it sets its status to IC_Solved
1911
1912 - The ics_dead field, of IC_Solved, records the subset of this
1913 implication's ic_given that are redundant (not needed).
1914
1915 * We compute which evidence variables are needed by an implication
1916 in setImplicationStatus. A variable is needed if
1917 a) it is free in the RHS of a Wanted EvBind,
1918 b) it is free in the RHS of an EvBind whose LHS is needed,
1919 c) it is in the ics_need of a nested implication.
1920
1921 * We need to be careful not to discard an implication
1922 prematurely, even one that is fully solved, because we might
1923 thereby forget which variables it needs, and hence wrongly
1924 report a constraint as redundant. But we can discard it once
1925 its free vars have been incorporated into its parent; or if it
1926 simply has no free vars. This careful discarding is also
1927 handled in setImplicationStatus.
1928
1929 ----- Reporting redundant constraints
1930
1931 * TcErrors does the actual warning, in warnRedundantConstraints.
1932
1933 * We don't report redundant givens for *every* implication; only
1934 for those which reply True to TcSimplify.warnRedundantGivens:
1935
1936 - For example, in a class declaration, the default method *can*
1937 use the class constraint, but it certainly doesn't *have* to,
1938 and we don't want to report an error there.
1939
1940 - More subtly, in a function definition
1941 f :: (Ord a, Ord a, Ix a) => a -> a
1942 f x = rhs
1943 we do an ambiguity check on the type (which would find that one
1944 of the Ord a constraints was redundant), and then we check that
1945 the definition has that type (which might find that both are
1946 redundant). We don't want to report the same error twice, so we
1947 disable it for the ambiguity check. Hence using two different
1948 FunSigCtxts, one with the warn-redundant field set True, and the
1949 other set False in
1950 - TcBinds.tcSpecPrag
1951 - TcBinds.tcTySig
1952
1953 This decision is taken in setImplicationStatus, rather than TcErrors
1954 so that we can discard implication constraints that we don't need.
1955 So ics_dead consists only of the *reportable* redundant givens.
1956
1957 ----- Shortcomings
1958
1959 Consider (see Trac #9939)
1960 f2 :: (Eq a, Ord a) => a -> a -> Bool
1961 -- Ord a redundant, but Eq a is reported
1962 f2 x y = (x == y)
1963
1964 We report (Eq a) as redundant, whereas actually (Ord a) is. But it's
1965 really not easy to detect that!
1966
1967
1968 Note [Cutting off simpl_loop]
1969 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1970 It is very important not to iterate in simpl_loop unless there is a chance
1971 of progress. Trac #8474 is a classic example:
1972
1973 * There's a deeply-nested chain of implication constraints.
1974 ?x:alpha => ?y1:beta1 => ... ?yn:betan => [W] ?x:Int
1975
1976 * From the innermost one we get a [D] alpha ~ Int,
1977 but alpha is untouchable until we get out to the outermost one
1978
1979 * We float [D] alpha~Int out (it is in floated_eqs), but since alpha
1980 is untouchable, the solveInteract in simpl_loop makes no progress
1981
1982 * So there is no point in attempting to re-solve
1983 ?yn:betan => [W] ?x:Int
1984 via solveNestedImplications, because we'll just get the
1985 same [D] again
1986
1987 * If we *do* re-solve, we'll get an ininite loop. It is cut off by
1988 the fixed bound of 10, but solving the next takes 10*10*...*10 (ie
1989 exponentially many) iterations!
1990
1991 Conclusion: we should call solveNestedImplications only if we did
1992 some unification in solveSimpleWanteds; because that's the only way
1993 we'll get more Givens (a unification is like adding a Given) to
1994 allow the implication to make progress.
1995 -}
1996
1997 promoteTyVar :: TcTyVar -> TcM (Bool, TcTyVar)
1998 -- When we float a constraint out of an implication we must restore
1999 -- invariant (WantedInv) in Note [TcLevel and untouchable type variables] in TcType
2000 -- Return True <=> we did some promotion
2001 -- Also returns either the original tyvar (no promotion) or the new one
2002 -- See Note [Promoting unification variables]
2003 promoteTyVar tv
2004 = do { tclvl <- TcM.getTcLevel
2005 ; if (isFloatedTouchableMetaTyVar tclvl tv)
2006 then do { cloned_tv <- TcM.cloneMetaTyVar tv
2007 ; let rhs_tv = setMetaTyVarTcLevel cloned_tv tclvl
2008 ; TcM.writeMetaTyVar tv (mkTyVarTy rhs_tv)
2009 ; return (True, rhs_tv) }
2010 else return (False, tv) }
2011
2012 -- Returns whether or not *any* tyvar is defaulted
2013 promoteTyVarSet :: TcTyVarSet -> TcM (Bool, TcTyVarSet)
2014 promoteTyVarSet tvs
2015 = do { (bools, tyvars) <- mapAndUnzipM promoteTyVar (nonDetEltsUniqSet tvs)
2016 -- non-determinism is OK because order of promotion doesn't matter
2017
2018 ; return (or bools, mkVarSet tyvars) }
2019
2020 promoteTyVarTcS :: TcTyVar -> TcS ()
2021 -- When we float a constraint out of an implication we must restore
2022 -- invariant (WantedInv) in Note [TcLevel and untouchable type variables] in TcType
2023 -- See Note [Promoting unification variables]
2024 -- We don't just call promoteTyVar because we want to use unifyTyVar,
2025 -- not writeMetaTyVar
2026 promoteTyVarTcS tv
2027 = do { tclvl <- TcS.getTcLevel
2028 ; when (isFloatedTouchableMetaTyVar tclvl tv) $
2029 do { cloned_tv <- TcS.cloneMetaTyVar tv
2030 ; let rhs_tv = setMetaTyVarTcLevel cloned_tv tclvl
2031 ; unifyTyVar tv (mkTyVarTy rhs_tv) } }
2032
2033 -- | Like 'defaultTyVar', but in the TcS monad.
2034 defaultTyVarTcS :: TcTyVar -> TcS Bool
2035 defaultTyVarTcS the_tv
2036 | isRuntimeRepVar the_tv
2037 , not (isTyVarTyVar the_tv)
2038 -- TyVarTvs should only be unified with a tyvar
2039 -- never with a type; c.f. TcMType.defaultTyVar
2040 -- and Note [Inferring kinds for type declarations] in TcTyClsDecls
2041 = do { traceTcS "defaultTyVarTcS RuntimeRep" (ppr the_tv)
2042 ; unifyTyVar the_tv liftedRepTy
2043 ; return True }
2044 | otherwise
2045 = return False -- the common case
2046
2047 approximateWC :: Bool -> WantedConstraints -> Cts
2048 -- Postcondition: Wanted or Derived Cts
2049 -- See Note [ApproximateWC]
2050 approximateWC float_past_equalities wc
2051 = float_wc emptyVarSet wc
2052 where
2053 float_wc :: TcTyCoVarSet -> WantedConstraints -> Cts
2054 float_wc trapping_tvs (WC { wc_simple = simples, wc_impl = implics })
2055 = filterBag (is_floatable trapping_tvs) simples `unionBags`
2056 do_bag (float_implic trapping_tvs) implics
2057 where
2058
2059 float_implic :: TcTyCoVarSet -> Implication -> Cts
2060 float_implic trapping_tvs imp
2061 | float_past_equalities || ic_no_eqs imp
2062 = float_wc new_trapping_tvs (ic_wanted imp)
2063 | otherwise -- Take care with equalities
2064 = emptyCts -- See (1) under Note [ApproximateWC]
2065 where
2066 new_trapping_tvs = trapping_tvs `extendVarSetList` ic_skols imp
2067
2068 do_bag :: (a -> Bag c) -> Bag a -> Bag c
2069 do_bag f = foldrBag (unionBags.f) emptyBag
2070
2071 is_floatable skol_tvs ct
2072 | isGivenCt ct = False
2073 | isHoleCt ct = False
2074 | insolubleEqCt ct = False
2075 | otherwise = tyCoVarsOfCt ct `disjointVarSet` skol_tvs
2076
2077 {- Note [ApproximateWC]
2078 ~~~~~~~~~~~~~~~~~~~~~~~
2079 approximateWC takes a constraint, typically arising from the RHS of a
2080 let-binding whose type we are *inferring*, and extracts from it some
2081 *simple* constraints that we might plausibly abstract over. Of course
2082 the top-level simple constraints are plausible, but we also float constraints
2083 out from inside, if they are not captured by skolems.
2084
2085 The same function is used when doing type-class defaulting (see the call
2086 to applyDefaultingRules) to extract constraints that that might be defaulted.
2087
2088 There is one caveat:
2089
2090 1. When infering most-general types (in simplifyInfer), we do *not*
2091 float anything out if the implication binds equality constraints,
2092 because that defeats the OutsideIn story. Consider
2093 data T a where
2094 TInt :: T Int
2095 MkT :: T a
2096
2097 f TInt = 3::Int
2098
2099 We get the implication (a ~ Int => res ~ Int), where so far we've decided
2100 f :: T a -> res
2101 We don't want to float (res~Int) out because then we'll infer
2102 f :: T a -> Int
2103 which is only on of the possible types. (GHC 7.6 accidentally *did*
2104 float out of such implications, which meant it would happily infer
2105 non-principal types.)
2106
2107 HOWEVER (Trac #12797) in findDefaultableGroups we are not worried about
2108 the most-general type; and we /do/ want to float out of equalities.
2109 Hence the boolean flag to approximateWC.
2110
2111 ------ Historical note -----------
2112 There used to be a second caveat, driven by Trac #8155
2113
2114 2. We do not float out an inner constraint that shares a type variable
2115 (transitively) with one that is trapped by a skolem. Eg
2116 forall a. F a ~ beta, Integral beta
2117 We don't want to float out (Integral beta). Doing so would be bad
2118 when defaulting, because then we'll default beta:=Integer, and that
2119 makes the error message much worse; we'd get
2120 Can't solve F a ~ Integer
2121 rather than
2122 Can't solve Integral (F a)
2123
2124 Moreover, floating out these "contaminated" constraints doesn't help
2125 when generalising either. If we generalise over (Integral b), we still
2126 can't solve the retained implication (forall a. F a ~ b). Indeed,
2127 arguably that too would be a harder error to understand.
2128
2129 But this transitive closure stuff gives rise to a complex rule for
2130 when defaulting actually happens, and one that was never documented.
2131 Moreover (Trac #12923), the more complex rule is sometimes NOT what
2132 you want. So I simply removed the extra code to implement the
2133 contamination stuff. There was zero effect on the testsuite (not even
2134 #8155).
2135 ------ End of historical note -----------
2136
2137
2138 Note [DefaultTyVar]
2139 ~~~~~~~~~~~~~~~~~~~
2140 defaultTyVar is used on any un-instantiated meta type variables to
2141 default any RuntimeRep variables to LiftedRep. This is important
2142 to ensure that instance declarations match. For example consider
2143
2144 instance Show (a->b)
2145 foo x = show (\_ -> True)
2146
2147 Then we'll get a constraint (Show (p ->q)) where p has kind (TYPE r),
2148 and that won't match the tcTypeKind (*) in the instance decl. See tests
2149 tc217 and tc175.
2150
2151 We look only at touchable type variables. No further constraints
2152 are going to affect these type variables, so it's time to do it by
2153 hand. However we aren't ready to default them fully to () or
2154 whatever, because the type-class defaulting rules have yet to run.
2155
2156 An alternate implementation would be to emit a derived constraint setting
2157 the RuntimeRep variable to LiftedRep, but this seems unnecessarily indirect.
2158
2159 Note [Promote _and_ default when inferring]
2160 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2161 When we are inferring a type, we simplify the constraint, and then use
2162 approximateWC to produce a list of candidate constraints. Then we MUST
2163
2164 a) Promote any meta-tyvars that have been floated out by
2165 approximateWC, to restore invariant (WantedInv) described in
2166 Note [TcLevel and untouchable type variables] in TcType.
2167
2168 b) Default the kind of any meta-tyvars that are not mentioned in
2169 in the environment.
2170
2171 To see (b), suppose the constraint is (C ((a :: OpenKind) -> Int)), and we
2172 have an instance (C ((x:*) -> Int)). The instance doesn't match -- but it
2173 should! If we don't solve the constraint, we'll stupidly quantify over
2174 (C (a->Int)) and, worse, in doing so skolemiseQuantifiedTyVar will quantify over
2175 (b:*) instead of (a:OpenKind), which can lead to disaster; see Trac #7332.
2176 Trac #7641 is a simpler example.
2177
2178 Note [Promoting unification variables]
2179 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2180 When we float an equality out of an implication we must "promote" free
2181 unification variables of the equality, in order to maintain Invariant
2182 (WantedInv) from Note [TcLevel and untouchable type variables] in
2183 TcType. for the leftover implication.
2184
2185 This is absolutely necessary. Consider the following example. We start
2186 with two implications and a class with a functional dependency.
2187
2188 class C x y | x -> y
2189 instance C [a] [a]
2190
2191 (I1) [untch=beta]forall b. 0 => F Int ~ [beta]
2192 (I2) [untch=beta]forall c. 0 => F Int ~ [[alpha]] /\ C beta [c]
2193
2194 We float (F Int ~ [beta]) out of I1, and we float (F Int ~ [[alpha]]) out of I2.
2195 They may react to yield that (beta := [alpha]) which can then be pushed inwards
2196 the leftover of I2 to get (C [alpha] [a]) which, using the FunDep, will mean that
2197 (alpha := a). In the end we will have the skolem 'b' escaping in the untouchable
2198 beta! Concrete example is in indexed_types/should_fail/ExtraTcsUntch.hs:
2199
2200 class C x y | x -> y where
2201 op :: x -> y -> ()
2202
2203 instance C [a] [a]
2204
2205 type family F a :: *
2206
2207 h :: F Int -> ()
2208 h = undefined
2209
2210 data TEx where
2211 TEx :: a -> TEx
2212
2213 f (x::beta) =
2214 let g1 :: forall b. b -> ()
2215 g1 _ = h [x]
2216 g2 z = case z of TEx y -> (h [[undefined]], op x [y])
2217 in (g1 '3', g2 undefined)
2218
2219
2220
2221 *********************************************************************************
2222 * *
2223 * Floating equalities *
2224 * *
2225 *********************************************************************************
2226
2227 Note [Float Equalities out of Implications]
2228 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2229 For ordinary pattern matches (including existentials) we float
2230 equalities out of implications, for instance:
2231 data T where
2232 MkT :: Eq a => a -> T
2233 f x y = case x of MkT _ -> (y::Int)
2234 We get the implication constraint (x::T) (y::alpha):
2235 forall a. [untouchable=alpha] Eq a => alpha ~ Int
2236 We want to float out the equality into a scope where alpha is no
2237 longer untouchable, to solve the implication!
2238
2239 But we cannot float equalities out of implications whose givens may
2240 yield or contain equalities:
2241
2242 data T a where
2243 T1 :: T Int
2244 T2 :: T Bool
2245 T3 :: T a
2246
2247 h :: T a -> a -> Int
2248
2249 f x y = case x of
2250 T1 -> y::Int
2251 T2 -> y::Bool
2252 T3 -> h x y
2253
2254 We generate constraint, for (x::T alpha) and (y :: beta):
2255 [untouchables = beta] (alpha ~ Int => beta ~ Int) -- From 1st branch
2256 [untouchables = beta] (alpha ~ Bool => beta ~ Bool) -- From 2nd branch
2257 (alpha ~ beta) -- From 3rd branch
2258
2259 If we float the equality (beta ~ Int) outside of the first implication and
2260 the equality (beta ~ Bool) out of the second we get an insoluble constraint.
2261 But if we just leave them inside the implications, we unify alpha := beta and
2262 solve everything.
2263
2264 Principle:
2265 We do not want to float equalities out which may
2266 need the given *evidence* to become soluble.
2267
2268 Consequence: classes with functional dependencies don't matter (since there is
2269 no evidence for a fundep equality), but equality superclasses do matter (since
2270 they carry evidence).
2271 -}
2272
2273 floatEqualities :: [TcTyVar] -> [EvId] -> EvBindsVar -> Bool
2274 -> WantedConstraints
2275 -> TcS (Cts, WantedConstraints)
2276 -- Main idea: see Note [Float Equalities out of Implications]
2277 --
2278 -- Precondition: the wc_simple of the incoming WantedConstraints are
2279 -- fully zonked, so that we can see their free variables
2280 --
2281 -- Postcondition: The returned floated constraints (Cts) are only
2282 -- Wanted or Derived
2283 --
2284 -- Also performs some unifications (via promoteTyVar), adding to
2285 -- monadically-carried ty_binds. These will be used when processing
2286 -- floated_eqs later
2287 --
2288 -- Subtleties: Note [Float equalities from under a skolem binding]
2289 -- Note [Skolem escape]
2290 -- Note [What prevents a constraint from floating]
2291 floatEqualities skols given_ids ev_binds_var no_given_eqs
2292 wanteds@(WC { wc_simple = simples })
2293 | not no_given_eqs -- There are some given equalities, so don't float
2294 = return (emptyBag, wanteds) -- Note [Float Equalities out of Implications]
2295
2296 | otherwise
2297 = do { -- First zonk: the inert set (from whence they came) is fully
2298 -- zonked, but unflattening may have filled in unification
2299 -- variables, and we /must/ see them. Otherwise we may float
2300 -- constraints that mention the skolems!
2301 simples <- TcS.zonkSimples simples
2302 ; binds <- TcS.getTcEvBindsMap ev_binds_var
2303
2304 -- Now we can pick the ones to float
2305 -- The constraints are un-flattened and de-canonicalised
2306 ; let (candidate_eqs, no_float_cts) = partitionBag is_float_eq_candidate simples
2307
2308 seed_skols = mkVarSet skols `unionVarSet`
2309 mkVarSet given_ids `unionVarSet`
2310 foldrBag add_non_flt_ct emptyVarSet no_float_cts `unionVarSet`
2311 foldEvBindMap add_one_bind emptyVarSet binds
2312 -- seed_skols: See Note [What prevents a constraint from floating] (1,2,3)
2313 -- Include the EvIds of any non-floating constraints
2314
2315 extended_skols = transCloVarSet (add_captured_ev_ids candidate_eqs) seed_skols
2316 -- extended_skols contains the EvIds of all the trapped constraints
2317 -- See Note [What prevents a constraint from floating] (3)
2318
2319 (flt_eqs, no_flt_eqs) = partitionBag (is_floatable extended_skols)
2320 candidate_eqs
2321
2322 remaining_simples = no_float_cts `andCts` no_flt_eqs
2323
2324 -- Promote any unification variables mentioned in the floated equalities
2325 -- See Note [Promoting unification variables]
2326 ; mapM_ promoteTyVarTcS (tyCoVarsOfCtsList flt_eqs)
2327
2328 ; traceTcS "floatEqualities" (vcat [ text "Skols =" <+> ppr skols
2329 , text "Extended skols =" <+> ppr extended_skols
2330 , text "Simples =" <+> ppr simples
2331 , text "Candidate eqs =" <+> ppr candidate_eqs
2332 , text "Floated eqs =" <+> ppr flt_eqs])
2333 ; return ( flt_eqs, wanteds { wc_simple = remaining_simples } ) }
2334
2335 where
2336 add_one_bind :: EvBind -> VarSet -> VarSet
2337 add_one_bind bind acc = extendVarSet acc (evBindVar bind)
2338
2339 add_non_flt_ct :: Ct -> VarSet -> VarSet
2340 add_non_flt_ct ct acc | isDerivedCt ct = acc
2341 | otherwise = extendVarSet acc (ctEvId ct)
2342
2343 is_floatable :: VarSet -> Ct -> Bool
2344 is_floatable skols ct
2345 | isDerivedCt ct = not (tyCoVarsOfCt ct `intersectsVarSet` skols)
2346 | otherwise = not (ctEvId ct `elemVarSet` skols)
2347
2348 add_captured_ev_ids :: Cts -> VarSet -> VarSet
2349 add_captured_ev_ids cts skols = foldrBag extra_skol emptyVarSet cts
2350 where
2351 extra_skol ct acc
2352 | isDerivedCt ct = acc
2353 | tyCoVarsOfCt ct `intersectsVarSet` skols = extendVarSet acc (ctEvId ct)
2354 | otherwise = acc
2355
2356 -- Identify which equalities are candidates for floating
2357 -- Float out alpha ~ ty, or ty ~ alpha which might be unified outside
2358 -- See Note [Which equalities to float]
2359 is_float_eq_candidate ct
2360 | pred <- ctPred ct
2361 , EqPred NomEq ty1 ty2 <- classifyPredType pred
2362 , tcTypeKind ty1 `tcEqType` tcTypeKind ty2
2363 = case (tcGetTyVar_maybe ty1, tcGetTyVar_maybe ty2) of
2364 (Just tv1, _) -> float_tv_eq_candidate tv1 ty2
2365 (_, Just tv2) -> float_tv_eq_candidate tv2 ty1
2366 _ -> False
2367 | otherwise = False
2368
2369 float_tv_eq_candidate tv1 ty2 -- See Note [Which equalities to float]
2370 = isMetaTyVar tv1
2371 && (not (isTyVarTyVar tv1) || isTyVarTy ty2)
2372
2373
2374 {- Note [Float equalities from under a skolem binding]
2375 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2376 Which of the simple equalities can we float out? Obviously, only
2377 ones that don't mention the skolem-bound variables. But that is
2378 over-eager. Consider
2379 [2] forall a. F a beta[1] ~ gamma[2], G beta[1] gamma[2] ~ Int
2380 The second constraint doesn't mention 'a'. But if we float it,
2381 we'll promote gamma[2] to gamma'[1]. Now suppose that we learn that
2382 beta := Bool, and F a Bool = a, and G Bool _ = Int. Then we'll
2383 we left with the constraint
2384 [2] forall a. a ~ gamma'[1]
2385 which is insoluble because gamma became untouchable.
2386
2387 Solution: float only constraints that stand a jolly good chance of
2388 being soluble simply by being floated, namely ones of form
2389 a ~ ty
2390 where 'a' is a currently-untouchable unification variable, but may
2391 become touchable by being floated (perhaps by more than one level).
2392
2393 We had a very complicated rule previously, but this is nice and
2394 simple. (To see the notes, look at this Note in a version of
2395 TcSimplify prior to Oct 2014).
2396
2397 Note [Which equalities to float]
2398 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2399 Which equalities should we float? We want to float ones where there
2400 is a decent chance that floating outwards will allow unification to
2401 happen. In particular, float out equalities that are:
2402
2403 * Of form (alpha ~# ty) or (ty ~# alpha), where
2404 * alpha is a meta-tyvar.
2405 * And 'alpha' is not a TyVarTv with 'ty' being a non-tyvar. In that
2406 case, floating out won't help either, and it may affect grouping
2407 of error messages.
2408
2409 * Homogeneous (both sides have the same kind). Why only homogeneous?
2410 Because heterogeneous equalities have derived kind equalities.
2411 See Note [Equalities with incompatible kinds] in TcCanonical.
2412 If we float out a hetero equality, then it will spit out the same
2413 derived kind equality again, which might create duplicate error
2414 messages.
2415
2416 Instead, we do float out the kind equality (if it's worth floating
2417 out, as above). If/when we solve it, we'll be able to rewrite the
2418 original hetero equality to be homogeneous, and then perhaps make
2419 progress / float it out. The duplicate error message was spotted in
2420 typecheck/should_fail/T7368.
2421
2422 * Nominal. No point in floating (alpha ~R# ty), because we do not
2423 unify representational equalities even if alpha is touchable.
2424 See Note [Do not unify representational equalities] in TcInteract.
2425
2426 Note [Skolem escape]
2427 ~~~~~~~~~~~~~~~~~~~~
2428 You might worry about skolem escape with all this floating.
2429 For example, consider
2430 [2] forall a. (a ~ F beta[2] delta,
2431 Maybe beta[2] ~ gamma[1])
2432
2433 The (Maybe beta ~ gamma) doesn't mention 'a', so we float it, and
2434 solve with gamma := beta. But what if later delta:=Int, and
2435 F b Int = b.
2436 Then we'd get a ~ beta[2], and solve to get beta:=a, and now the
2437 skolem has escaped!
2438
2439 But it's ok: when we float (Maybe beta[2] ~ gamma[1]), we promote beta[2]
2440 to beta[1], and that means the (a ~ beta[1]) will be stuck, as it should be.
2441
2442 Note [What prevents a constraint from floating]
2443 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2444 What /prevents/ a constraint from floating? If it mentions one of the
2445 "bound variables of the implication". What are they?
2446
2447 The "bound variables of the implication" are
2448
2449 1. The skolem type variables `ic_skols`
2450
2451 2. The "given" evidence variables `ic_given`. Example:
2452 forall a. (co :: t1 ~# t2) => [W] co2 : (a ~# b |> co)
2453 Here 'co' is bound
2454
2455 3. The binders of all evidence bindings in `ic_binds`. Example
2456 forall a. (d :: t1 ~ t2)
2457 EvBinds { (co :: t1 ~# t2) = superclass-sel d }
2458 => [W] co2 : (a ~# b |> co)
2459 Here `co` is gotten by superclass selection from `d`, and the
2460 wanted constraint co2 must not float.
2461
2462 4. And the evidence variable of any equality constraint (incl
2463 Wanted ones) whose type mentions a bound variable. Example:
2464 forall k. [W] co1 :: t1 ~# t2 |> co2
2465 [W] co2 :: k ~# *
2466 Here, since `k` is bound, so is `co2` and hence so is `co1`.
2467
2468 Here (1,2,3) are handled by the "seed_skols" calculation, and
2469 (4) is done by the transCloVarSet call.
2470
2471 The possible dependence on givens, and evidence bindings, is more
2472 subtle than we'd realised at first. See Trac #14584.
2473
2474
2475 *********************************************************************************
2476 * *
2477 * Defaulting and disambiguation *
2478 * *
2479 *********************************************************************************
2480 -}
2481
2482 applyDefaultingRules :: WantedConstraints -> TcS Bool
2483 -- True <=> I did some defaulting, by unifying a meta-tyvar
2484 -- Input WantedConstraints are not necessarily zonked
2485
2486 applyDefaultingRules wanteds
2487 | isEmptyWC wanteds
2488 = return False
2489 | otherwise
2490 = do { info@(default_tys, _) <- getDefaultInfo
2491 ; wanteds <- TcS.zonkWC wanteds
2492
2493 ; let groups = findDefaultableGroups info wanteds
2494
2495 ; traceTcS "applyDefaultingRules {" $
2496 vcat [ text "wanteds =" <+> ppr wanteds
2497 , text "groups =" <+> ppr groups
2498 , text "info =" <+> ppr info ]
2499
2500 ; something_happeneds <- mapM (disambigGroup default_tys) groups
2501
2502 ; traceTcS "applyDefaultingRules }" (ppr something_happeneds)
2503
2504 ; return (or something_happeneds) }
2505
2506 findDefaultableGroups
2507 :: ( [Type]
2508 , (Bool,Bool) ) -- (Overloaded strings, extended default rules)
2509 -> WantedConstraints -- Unsolved (wanted or derived)
2510 -> [(TyVar, [Ct])]
2511 findDefaultableGroups (default_tys, (ovl_strings, extended_defaults)) wanteds
2512 | null default_tys
2513 = []
2514 | otherwise
2515 = [ (tv, map fstOf3 group)
2516 | group'@((_,_,tv) :| _) <- unary_groups
2517 , let group = toList group'
2518 , defaultable_tyvar tv
2519 , defaultable_classes (map sndOf3 group) ]
2520 where
2521 simples = approximateWC True wanteds
2522 (unaries, non_unaries) = partitionWith find_unary (bagToList simples)
2523 unary_groups = equivClasses cmp_tv unaries
2524
2525 unary_groups :: [NonEmpty (Ct, Class, TcTyVar)] -- (C tv) constraints
2526 unaries :: [(Ct, Class, TcTyVar)] -- (C tv) constraints
2527 non_unaries :: [Ct] -- and *other* constraints
2528
2529 -- Finds unary type-class constraints
2530 -- But take account of polykinded classes like Typeable,
2531 -- which may look like (Typeable * (a:*)) (Trac #8931)
2532 find_unary :: Ct -> Either (Ct, Class, TyVar) Ct
2533 find_unary cc
2534 | Just (cls,tys) <- getClassPredTys_maybe (ctPred cc)
2535 , [ty] <- filterOutInvisibleTypes (classTyCon cls) tys
2536 -- Ignore invisible arguments for this purpose
2537 , Just tv <- tcGetTyVar_maybe ty
2538 , isMetaTyVar tv -- We might have runtime-skolems in GHCi, and
2539 -- we definitely don't want to try to assign to those!
2540 = Left (cc, cls, tv)
2541 find_unary cc = Right cc -- Non unary or non dictionary
2542
2543 bad_tvs :: TcTyCoVarSet -- TyVars mentioned by non-unaries
2544 bad_tvs = mapUnionVarSet tyCoVarsOfCt non_unaries
2545
2546 cmp_tv (_,_,tv1) (_,_,tv2) = tv1 `compare` tv2
2547
2548 defaultable_tyvar :: TcTyVar -> Bool
2549 defaultable_tyvar tv
2550 = let b1 = isTyConableTyVar tv -- Note [Avoiding spurious errors]
2551 b2 = not (tv `elemVarSet` bad_tvs)
2552 in b1 && (b2 || extended_defaults) -- Note [Multi-parameter defaults]
2553
2554 defaultable_classes :: [Class] -> Bool
2555 defaultable_classes clss
2556 | extended_defaults = any (isInteractiveClass ovl_strings) clss
2557 | otherwise = all is_std_class clss && (any (isNumClass ovl_strings) clss)
2558
2559 -- is_std_class adds IsString to the standard numeric classes,
2560 -- when -foverloaded-strings is enabled
2561 is_std_class cls = isStandardClass cls ||
2562 (ovl_strings && (cls `hasKey` isStringClassKey))
2563
2564 ------------------------------
2565 disambigGroup :: [Type] -- The default types
2566 -> (TcTyVar, [Ct]) -- All classes of the form (C a)
2567 -- sharing same type variable
2568 -> TcS Bool -- True <=> something happened, reflected in ty_binds
2569
2570 disambigGroup [] _
2571 = return False
2572 disambigGroup (default_ty:default_tys) group@(the_tv, wanteds)
2573 = do { traceTcS "disambigGroup {" (vcat [ ppr default_ty, ppr the_tv, ppr wanteds ])
2574 ; fake_ev_binds_var <- TcS.newTcEvBinds
2575 ; tclvl <- TcS.getTcLevel
2576 ; success <- nestImplicTcS fake_ev_binds_var (pushTcLevel tclvl) try_group
2577
2578 ; if success then
2579 -- Success: record the type variable binding, and return
2580 do { unifyTyVar the_tv default_ty
2581 ; wrapWarnTcS $ warnDefaulting wanteds default_ty
2582 ; traceTcS "disambigGroup succeeded }" (ppr default_ty)
2583 ; return True }
2584 else
2585 -- Failure: try with the next type
2586 do { traceTcS "disambigGroup failed, will try other default types }"
2587 (ppr default_ty)
2588 ; disambigGroup default_tys group } }
2589 where
2590 try_group
2591 | Just subst <- mb_subst
2592 = do { lcl_env <- TcS.getLclEnv
2593 ; tc_lvl <- TcS.getTcLevel
2594 ; let loc = mkGivenLoc tc_lvl UnkSkol lcl_env
2595 ; wanted_evs <- mapM (newWantedEvVarNC loc . substTy subst . ctPred)
2596 wanteds
2597 ; fmap isEmptyWC $
2598 solveSimpleWanteds $ listToBag $
2599 map mkNonCanonical wanted_evs }
2600
2601 | otherwise
2602 = return False
2603
2604 the_ty = mkTyVarTy the_tv
2605 mb_subst = tcMatchTyKi the_ty default_ty
2606 -- Make sure the kinds match too; hence this call to tcMatchTyKi
2607 -- E.g. suppose the only constraint was (Typeable k (a::k))
2608 -- With the addition of polykinded defaulting we also want to reject
2609 -- ill-kinded defaulting attempts like (Eq []) or (Foldable Int) here.
2610
2611 -- In interactive mode, or with -XExtendedDefaultRules,
2612 -- we default Show a to Show () to avoid graututious errors on "show []"
2613 isInteractiveClass :: Bool -- -XOverloadedStrings?
2614 -> Class -> Bool
2615 isInteractiveClass ovl_strings cls
2616 = isNumClass ovl_strings cls || (classKey cls `elem` interactiveClassKeys)
2617
2618 -- isNumClass adds IsString to the standard numeric classes,
2619 -- when -foverloaded-strings is enabled
2620 isNumClass :: Bool -- -XOverloadedStrings?
2621 -> Class -> Bool
2622 isNumClass ovl_strings cls
2623 = isNumericClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
2624
2625
2626 {-
2627 Note [Avoiding spurious errors]
2628 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2629 When doing the unification for defaulting, we check for skolem
2630 type variables, and simply don't default them. For example:
2631 f = (*) -- Monomorphic
2632 g :: Num a => a -> a
2633 g x = f x x
2634 Here, we get a complaint when checking the type signature for g,
2635 that g isn't polymorphic enough; but then we get another one when
2636 dealing with the (Num a) context arising from f's definition;
2637 we try to unify a with Int (to default it), but find that it's
2638 already been unified with the rigid variable from g's type sig.
2639
2640 Note [Multi-parameter defaults]
2641 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2642 With -XExtendedDefaultRules, we default only based on single-variable
2643 constraints, but do not exclude from defaulting any type variables which also
2644 appear in multi-variable constraints. This means that the following will
2645 default properly:
2646
2647 default (Integer, Double)
2648
2649 class A b (c :: Symbol) where
2650 a :: b -> Proxy c
2651
2652 instance A Integer c where a _ = Proxy
2653
2654 main = print (a 5 :: Proxy "5")
2655
2656 Note that if we change the above instance ("instance A Integer") to
2657 "instance A Double", we get an error:
2658
2659 No instance for (A Integer "5")
2660
2661 This is because the first defaulted type (Integer) has successfully satisfied
2662 its single-parameter constraints (in this case Num).
2663 -}