73398a8e76ba60cc5a6efd560b20d81aab1c2990
[ghc.git] / compiler / typecheck / TcSimplify.hs
1 {-# LANGUAGE CPP #-}
2
3 module TcSimplify(
4 simplifyInfer, InferMode(..),
5 growThetaTyVars,
6 simplifyAmbiguityCheck,
7 simplifyDefault,
8 simplifyTop, captureTopConstraints,
9 simplifyInteractive, solveEqualities,
10 simplifyWantedsTcM,
11 tcCheckSatisfiability,
12
13 -- For Rules we need these
14 solveWanteds, solveWantedsAndDrop,
15 approximateWC, runTcSDeriveds
16 ) where
17
18 #include "HsVersions.h"
19
20 import Bag
21 import Class ( Class, classKey, classTyCon )
22 import DynFlags ( WarningFlag ( Opt_WarnMonomorphism )
23 , WarnReason ( Reason )
24 , DynFlags( solverIterations ) )
25 import Inst
26 import ListSetOps
27 import Maybes
28 import Name
29 import Outputable
30 import PrelInfo
31 import PrelNames
32 import TcErrors
33 import TcEvidence
34 import TcInteract
35 import TcCanonical ( makeSuperClasses )
36 import TcMType as TcM
37 import TcRnMonad as TcM
38 import TcSMonad as TcS
39 import TcType
40 import TrieMap () -- DV: for now
41 import Type
42 import TysWiredIn ( liftedRepTy )
43 import Unify ( tcMatchTyKi )
44 import Util
45 import Var
46 import VarSet
47 import UniqSet
48 import BasicTypes ( IntWithInf, intGtLimit )
49 import ErrUtils ( emptyMessages )
50 import qualified GHC.LanguageExtensions as LangExt
51
52 import Control.Monad ( when, unless )
53 import Data.List ( partition )
54
55 {-
56 *********************************************************************************
57 * *
58 * External interface *
59 * *
60 *********************************************************************************
61 -}
62
63 captureTopConstraints :: TcM a -> TcM (a, WantedConstraints)
64 -- (captureTopConstraints m) runs m, and returns the type constraints it
65 -- generates plus the constraints produced by static forms inside.
66 -- If it fails with an exception, it reports any insolubles
67 -- (out of scope variables) before doing so
68 captureTopConstraints thing_inside
69 = do { static_wc_var <- TcM.newTcRef emptyWC ;
70 ; (mb_res, lie) <- TcM.updGblEnv (\env -> env { tcg_static_wc = static_wc_var } ) $
71 TcM.tryCaptureConstraints thing_inside
72 ; stWC <- TcM.readTcRef static_wc_var
73
74 -- See TcRnMonad Note [Constraints and errors]
75 -- If the thing_inside threw an exception, but generated some insoluble
76 -- constraints, report the latter before propagating the exception
77 -- Otherwise they will be lost altogether
78 ; case mb_res of
79 Right res -> return (res, lie `andWC` stWC)
80 Left {} -> do { _ <- reportUnsolved lie; failM } }
81 -- This call to reportUnsolved is the reason
82 -- this function is here instead of TcRnMonad
83
84 simplifyTop :: WantedConstraints -> TcM (Bag EvBind)
85 -- Simplify top-level constraints
86 -- Usually these will be implications,
87 -- but when there is nothing to quantify we don't wrap
88 -- in a degenerate implication, so we do that here instead
89 simplifyTop wanteds
90 = do { traceTc "simplifyTop {" $ text "wanted = " <+> ppr wanteds
91 ; ((final_wc, unsafe_ol), binds1) <- runTcS $
92 do { final_wc <- simpl_top wanteds
93 ; unsafe_ol <- getSafeOverlapFailures
94 ; return (final_wc, unsafe_ol) }
95 ; traceTc "End simplifyTop }" empty
96
97 ; traceTc "reportUnsolved {" empty
98 ; binds2 <- reportUnsolved final_wc
99 ; traceTc "reportUnsolved }" empty
100
101 ; traceTc "reportUnsolved (unsafe overlapping) {" empty
102 ; unless (isEmptyCts unsafe_ol) $ do {
103 -- grab current error messages and clear, warnAllUnsolved will
104 -- update error messages which we'll grab and then restore saved
105 -- messages.
106 ; errs_var <- getErrsVar
107 ; saved_msg <- TcM.readTcRef errs_var
108 ; TcM.writeTcRef errs_var emptyMessages
109
110 ; warnAllUnsolved $ WC { wc_simple = unsafe_ol
111 , wc_insol = emptyCts
112 , wc_impl = emptyBag }
113
114 ; whyUnsafe <- fst <$> TcM.readTcRef errs_var
115 ; TcM.writeTcRef errs_var saved_msg
116 ; recordUnsafeInfer whyUnsafe
117 }
118 ; traceTc "reportUnsolved (unsafe overlapping) }" empty
119
120 ; return (evBindMapBinds binds1 `unionBags` binds2) }
121
122 -- | Type-check a thing that emits only equality constraints, then
123 -- solve those constraints. Fails outright if there is trouble.
124 solveEqualities :: TcM a -> TcM a
125 solveEqualities thing_inside
126 = checkNoErrs $ -- See Note [Fail fast on kind errors]
127 do { (result, wanted) <- captureConstraints thing_inside
128 ; traceTc "solveEqualities {" $ text "wanted = " <+> ppr wanted
129 ; final_wc <- runTcSEqualities $ simpl_top wanted
130 ; traceTc "End solveEqualities }" empty
131
132 ; traceTc "reportAllUnsolved {" empty
133 ; reportAllUnsolved final_wc
134 ; traceTc "reportAllUnsolved }" empty
135 ; return result }
136
137 simpl_top :: WantedConstraints -> TcS WantedConstraints
138 -- See Note [Top-level Defaulting Plan]
139 simpl_top wanteds
140 = do { wc_first_go <- nestTcS (solveWantedsAndDrop wanteds)
141 -- This is where the main work happens
142 ; try_tyvar_defaulting wc_first_go }
143 where
144 try_tyvar_defaulting :: WantedConstraints -> TcS WantedConstraints
145 try_tyvar_defaulting wc
146 | isEmptyWC wc
147 = return wc
148 | otherwise
149 = do { free_tvs <- TcS.zonkTyCoVarsAndFVList (tyCoVarsOfWCList wc)
150 ; let meta_tvs = filter (isTyVar <&&> isMetaTyVar) free_tvs
151 -- zonkTyCoVarsAndFV: the wc_first_go is not yet zonked
152 -- filter isMetaTyVar: we might have runtime-skolems in GHCi,
153 -- and we definitely don't want to try to assign to those!
154 -- The isTyVar is needed to weed out coercion variables
155
156 ; defaulted <- mapM defaultTyVarTcS meta_tvs -- Has unification side effects
157 ; if or defaulted
158 then do { wc_residual <- nestTcS (solveWanteds wc)
159 -- See Note [Must simplify after defaulting]
160 ; try_class_defaulting wc_residual }
161 else try_class_defaulting wc } -- No defaulting took place
162
163 try_class_defaulting :: WantedConstraints -> TcS WantedConstraints
164 try_class_defaulting wc
165 | isEmptyWC wc
166 = return wc
167 | otherwise -- See Note [When to do type-class defaulting]
168 = do { something_happened <- applyDefaultingRules wc
169 -- See Note [Top-level Defaulting Plan]
170 ; if something_happened
171 then do { wc_residual <- nestTcS (solveWantedsAndDrop wc)
172 ; try_class_defaulting wc_residual }
173 -- See Note [Overview of implicit CallStacks] in TcEvidence
174 else try_callstack_defaulting wc }
175
176 try_callstack_defaulting :: WantedConstraints -> TcS WantedConstraints
177 try_callstack_defaulting wc
178 | isEmptyWC wc
179 = return wc
180 | otherwise
181 = defaultCallStacks wc
182
183 -- | Default any remaining @CallStack@ constraints to empty @CallStack@s.
184 defaultCallStacks :: WantedConstraints -> TcS WantedConstraints
185 -- See Note [Overview of implicit CallStacks] in TcEvidence
186 defaultCallStacks wanteds
187 = do simples <- handle_simples (wc_simple wanteds)
188 mb_implics <- mapBagM handle_implic (wc_impl wanteds)
189 return (wanteds { wc_simple = simples
190 , wc_impl = catBagMaybes mb_implics })
191
192 where
193
194 handle_simples simples
195 = catBagMaybes <$> mapBagM defaultCallStack simples
196
197 handle_implic :: Implication -> TcS (Maybe Implication)
198 -- The Maybe is because solving the CallStack constraint
199 -- may well allow us to discard the implication entirely
200 handle_implic implic
201 | isSolvedStatus (ic_status implic)
202 = return (Just implic)
203 | otherwise
204 = do { wanteds <- setEvBindsTcS (ic_binds implic) $
205 -- defaultCallStack sets a binding, so
206 -- we must set the correct binding group
207 defaultCallStacks (ic_wanted implic)
208 ; setImplicationStatus (implic { ic_wanted = wanteds }) }
209
210 defaultCallStack ct
211 | Just _ <- isCallStackPred (ctPred ct)
212 = do { solveCallStack (cc_ev ct) EvCsEmpty
213 ; return Nothing }
214
215 defaultCallStack ct
216 = return (Just ct)
217
218
219 {- Note [Fail fast on kind errors]
220 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
221 solveEqualities is used to solve kind equalities when kind-checking
222 user-written types. If solving fails we should fail outright, rather
223 than just accumulate an error message, for two reasons:
224
225 * A kind-bogus type signature may cause a cascade of knock-on
226 errors if we let it pass
227
228 * More seriously, we don't have a convenient term-level place to add
229 deferred bindings for unsolved kind-equality constraints, so we
230 don't build evidence bindings (by usine reportAllUnsolved). That
231 means that we'll be left with with a type that has coercion holes
232 in it, something like
233 <type> |> co-hole
234 where co-hole is not filled in. Eeek! That un-filled-in
235 hole actually causes GHC to crash with "fvProv falls into a hole"
236 See Trac #11563, #11520, #11516, #11399
237
238 So it's important to use 'checkNoErrs' here!
239
240 Note [When to do type-class defaulting]
241 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
242 In GHC 7.6 and 7.8.2, we did type-class defaulting only if insolubleWC
243 was false, on the grounds that defaulting can't help solve insoluble
244 constraints. But if we *don't* do defaulting we may report a whole
245 lot of errors that would be solved by defaulting; these errors are
246 quite spurious because fixing the single insoluble error means that
247 defaulting happens again, which makes all the other errors go away.
248 This is jolly confusing: Trac #9033.
249
250 So it seems better to always do type-class defaulting.
251
252 However, always doing defaulting does mean that we'll do it in
253 situations like this (Trac #5934):
254 run :: (forall s. GenST s) -> Int
255 run = fromInteger 0
256 We don't unify the return type of fromInteger with the given function
257 type, because the latter involves foralls. So we're left with
258 (Num alpha, alpha ~ (forall s. GenST s) -> Int)
259 Now we do defaulting, get alpha := Integer, and report that we can't
260 match Integer with (forall s. GenST s) -> Int. That's not totally
261 stupid, but perhaps a little strange.
262
263 Another potential alternative would be to suppress *all* non-insoluble
264 errors if there are *any* insoluble errors, anywhere, but that seems
265 too drastic.
266
267 Note [Must simplify after defaulting]
268 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
269 We may have a deeply buried constraint
270 (t:*) ~ (a:Open)
271 which we couldn't solve because of the kind incompatibility, and 'a' is free.
272 Then when we default 'a' we can solve the constraint. And we want to do
273 that before starting in on type classes. We MUST do it before reporting
274 errors, because it isn't an error! Trac #7967 was due to this.
275
276 Note [Top-level Defaulting Plan]
277 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
278 We have considered two design choices for where/when to apply defaulting.
279 (i) Do it in SimplCheck mode only /whenever/ you try to solve some
280 simple constraints, maybe deep inside the context of implications.
281 This used to be the case in GHC 7.4.1.
282 (ii) Do it in a tight loop at simplifyTop, once all other constraints have
283 finished. This is the current story.
284
285 Option (i) had many disadvantages:
286 a) Firstly, it was deep inside the actual solver.
287 b) Secondly, it was dependent on the context (Infer a type signature,
288 or Check a type signature, or Interactive) since we did not want
289 to always start defaulting when inferring (though there is an exception to
290 this, see Note [Default while Inferring]).
291 c) It plainly did not work. Consider typecheck/should_compile/DfltProb2.hs:
292 f :: Int -> Bool
293 f x = const True (\y -> let w :: a -> a
294 w a = const a (y+1)
295 in w y)
296 We will get an implication constraint (for beta the type of y):
297 [untch=beta] forall a. 0 => Num beta
298 which we really cannot default /while solving/ the implication, since beta is
299 untouchable.
300
301 Instead our new defaulting story is to pull defaulting out of the solver loop and
302 go with option (ii), implemented at SimplifyTop. Namely:
303 - First, have a go at solving the residual constraint of the whole
304 program
305 - Try to approximate it with a simple constraint
306 - Figure out derived defaulting equations for that simple constraint
307 - Go round the loop again if you did manage to get some equations
308
309 Now, that has to do with class defaulting. However there exists type variable /kind/
310 defaulting. Again this is done at the top-level and the plan is:
311 - At the top-level, once you had a go at solving the constraint, do
312 figure out /all/ the touchable unification variables of the wanted constraints.
313 - Apply defaulting to their kinds
314
315 More details in Note [DefaultTyVar].
316
317 Note [Safe Haskell Overlapping Instances]
318 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
319 In Safe Haskell, we apply an extra restriction to overlapping instances. The
320 motive is to prevent untrusted code provided by a third-party, changing the
321 behavior of trusted code through type-classes. This is due to the global and
322 implicit nature of type-classes that can hide the source of the dictionary.
323
324 Another way to state this is: if a module M compiles without importing another
325 module N, changing M to import N shouldn't change the behavior of M.
326
327 Overlapping instances with type-classes can violate this principle. However,
328 overlapping instances aren't always unsafe. They are just unsafe when the most
329 selected dictionary comes from untrusted code (code compiled with -XSafe) and
330 overlaps instances provided by other modules.
331
332 In particular, in Safe Haskell at a call site with overlapping instances, we
333 apply the following rule to determine if it is a 'unsafe' overlap:
334
335 1) Most specific instance, I1, defined in an `-XSafe` compiled module.
336 2) I1 is an orphan instance or a MPTC.
337 3) At least one overlapped instance, Ix, is both:
338 A) from a different module than I1
339 B) Ix is not marked `OVERLAPPABLE`
340
341 This is a slightly involved heuristic, but captures the situation of an
342 imported module N changing the behavior of existing code. For example, if
343 condition (2) isn't violated, then the module author M must depend either on a
344 type-class or type defined in N.
345
346 Secondly, when should these heuristics be enforced? We enforced them when the
347 type-class method call site is in a module marked `-XSafe` or `-XTrustworthy`.
348 This allows `-XUnsafe` modules to operate without restriction, and for Safe
349 Haskell inferrence to infer modules with unsafe overlaps as unsafe.
350
351 One alternative design would be to also consider if an instance was imported as
352 a `safe` import or not and only apply the restriction to instances imported
353 safely. However, since instances are global and can be imported through more
354 than one path, this alternative doesn't work.
355
356 Note [Safe Haskell Overlapping Instances Implementation]
357 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
358
359 How is this implemented? It's complicated! So we'll step through it all:
360
361 1) `InstEnv.lookupInstEnv` -- Performs instance resolution, so this is where
362 we check if a particular type-class method call is safe or unsafe. We do this
363 through the return type, `ClsInstLookupResult`, where the last parameter is a
364 list of instances that are unsafe to overlap. When the method call is safe,
365 the list is null.
366
367 2) `TcInteract.matchClassInst` -- This module drives the instance resolution
368 / dictionary generation. The return type is `LookupInstResult`, which either
369 says no instance matched, or one found, and if it was a safe or unsafe
370 overlap.
371
372 3) `TcInteract.doTopReactDict` -- Takes a dictionary / class constraint and
373 tries to resolve it by calling (in part) `matchClassInst`. The resolving
374 mechanism has a work list (of constraints) that it process one at a time. If
375 the constraint can't be resolved, it's added to an inert set. When compiling
376 an `-XSafe` or `-XTrustworthy` module, we follow this approach as we know
377 compilation should fail. These are handled as normal constraint resolution
378 failures from here-on (see step 6).
379
380 Otherwise, we may be inferring safety (or using `-Wunsafe`), and
381 compilation should succeed, but print warnings and/or mark the compiled module
382 as `-XUnsafe`. In this case, we call `insertSafeOverlapFailureTcS` which adds
383 the unsafe (but resolved!) constraint to the `inert_safehask` field of
384 `InertCans`.
385
386 4) `TcSimplify.simplifyTop`:
387 * Call simpl_top, the top-level function for driving the simplifier for
388 constraint resolution.
389
390 * Once finished, call `getSafeOverlapFailures` to retrieve the
391 list of overlapping instances that were successfully resolved,
392 but unsafe. Remember, this is only applicable for generating warnings
393 (`-Wunsafe`) or inferring a module unsafe. `-XSafe` and `-XTrustworthy`
394 cause compilation failure by not resolving the unsafe constraint at all.
395
396 * For unresolved constraints (all types), call `TcErrors.reportUnsolved`,
397 while for resolved but unsafe overlapping dictionary constraints, call
398 `TcErrors.warnAllUnsolved`. Both functions convert constraints into a
399 warning message for the user.
400
401 * In the case of `warnAllUnsolved` for resolved, but unsafe
402 dictionary constraints, we collect the generated warning
403 message (pop it) and call `TcRnMonad.recordUnsafeInfer` to
404 mark the module we are compiling as unsafe, passing the
405 warning message along as the reason.
406
407 5) `TcErrors.*Unsolved` -- Generates error messages for constraints by
408 actually calling `InstEnv.lookupInstEnv` again! Yes, confusing, but all we
409 know is the constraint that is unresolved or unsafe. For dictionary, all we
410 know is that we need a dictionary of type C, but not what instances are
411 available and how they overlap. So we once again call `lookupInstEnv` to
412 figure that out so we can generate a helpful error message.
413
414 6) `TcRnMonad.recordUnsafeInfer` -- Save the unsafe result and reason in an
415 IORef called `tcg_safeInfer`.
416
417 7) `HscMain.tcRnModule'` -- Reads `tcg_safeInfer` after type-checking, calling
418 `HscMain.markUnsafeInfer` (passing the reason along) when safe-inferrence
419 failed.
420
421 Note [No defaulting in the ambiguity check]
422 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
423 When simplifying constraints for the ambiguity check, we use
424 solveWantedsAndDrop, not simpl_top, so that we do no defaulting.
425 Trac #11947 was an example:
426 f :: Num a => Int -> Int
427 This is ambiguous of course, but we don't want to default the
428 (Num alpha) constraint to (Num Int)! Doing so gives a defaulting
429 warning, but no error.
430 -}
431
432 ------------------
433 simplifyAmbiguityCheck :: Type -> WantedConstraints -> TcM ()
434 simplifyAmbiguityCheck ty wanteds
435 = do { traceTc "simplifyAmbiguityCheck {" (text "type = " <+> ppr ty $$ text "wanted = " <+> ppr wanteds)
436 ; (final_wc, _) <- runTcS $ solveWantedsAndDrop wanteds
437 -- NB: no defaulting! See Note [No defaulting in the ambiguity check]
438
439 ; traceTc "End simplifyAmbiguityCheck }" empty
440
441 -- Normally report all errors; but with -XAllowAmbiguousTypes
442 -- report only insoluble ones, since they represent genuinely
443 -- inaccessible code
444 ; allow_ambiguous <- xoptM LangExt.AllowAmbiguousTypes
445 ; traceTc "reportUnsolved(ambig) {" empty
446 ; unless (allow_ambiguous && not (insolubleWC final_wc))
447 (discardResult (reportUnsolved final_wc))
448 ; traceTc "reportUnsolved(ambig) }" empty
449
450 ; return () }
451
452 ------------------
453 simplifyInteractive :: WantedConstraints -> TcM (Bag EvBind)
454 simplifyInteractive wanteds
455 = traceTc "simplifyInteractive" empty >>
456 simplifyTop wanteds
457
458 ------------------
459 simplifyDefault :: ThetaType -- Wanted; has no type variables in it
460 -> TcM () -- Succeeds if the constraint is soluble
461 simplifyDefault theta
462 = do { traceTc "simplifyDefault" empty
463 ; wanteds <- newWanteds DefaultOrigin theta
464 ; unsolved <- runTcSDeriveds (solveWantedsAndDrop (mkSimpleWC wanteds))
465 ; traceTc "reportUnsolved {" empty
466 ; reportAllUnsolved unsolved
467 ; traceTc "reportUnsolved }" empty
468 ; return () }
469
470 ------------------
471 tcCheckSatisfiability :: Bag EvVar -> TcM Bool
472 -- Return True if satisfiable, False if definitely contradictory
473 tcCheckSatisfiability given_ids
474 = do { lcl_env <- TcM.getLclEnv
475 ; let given_loc = mkGivenLoc topTcLevel UnkSkol lcl_env
476 ; (res, _ev_binds) <- runTcS $
477 do { traceTcS "checkSatisfiability {" (ppr given_ids)
478 ; let given_cts = mkGivens given_loc (bagToList given_ids)
479 -- See Note [Superclasses and satisfiability]
480 ; solveSimpleGivens given_cts
481 ; insols <- getInertInsols
482 ; insols <- try_harder insols
483 ; traceTcS "checkSatisfiability }" (ppr insols)
484 ; return (isEmptyBag insols) }
485 ; return res }
486 where
487 try_harder :: Cts -> TcS Cts
488 -- Maybe we have to search up the superclass chain to find
489 -- an unsatisfiable constraint. Example: pmcheck/T3927b.
490 -- At the moment we try just once
491 try_harder insols
492 | not (isEmptyBag insols) -- We've found that it's definitely unsatisfiable
493 = return insols -- Hurrah -- stop now.
494 | otherwise
495 = do { pending_given <- getPendingScDicts
496 ; new_given <- makeSuperClasses pending_given
497 ; solveSimpleGivens new_given
498 ; getInertInsols }
499
500 {- Note [Superclasses and satisfiability]
501 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
502 Expand superclasses before starting, because (Int ~ Bool), has
503 (Int ~~ Bool) as a superclass, which in turn has (Int ~N# Bool)
504 as a superclass, and it's the latter that is insoluble. See
505 Note [The equality types story] in TysPrim.
506
507 If we fail to prove unsatisfiability we (arbitrarily) try just once to
508 find superclasses, using try_harder. Reason: we might have a type
509 signature
510 f :: F op (Implements push) => ..
511 where F is a type function. This happened in Trac #3972.
512
513 We could do more than once but we'd have to have /some/ limit: in the
514 the recursive case, we would go on forever in the common case where
515 the constraints /are/ satisfiable (Trac #10592 comment:12!).
516
517 For stratightforard situations without type functions the try_harder
518 step does nothing.
519
520
521 ***********************************************************************************
522 * *
523 * Inference
524 * *
525 ***********************************************************************************
526
527 Note [Inferring the type of a let-bound variable]
528 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
529 Consider
530 f x = rhs
531
532 To infer f's type we do the following:
533 * Gather the constraints for the RHS with ambient level *one more than*
534 the current one. This is done by the call
535 pushLevelAndCaptureConstraints (tcMonoBinds...)
536 in TcBinds.tcPolyInfer
537
538 * Call simplifyInfer to simplify the constraints and decide what to
539 quantify over. We pass in the level used for the RHS constraints,
540 here called rhs_tclvl.
541
542 This ensures that the implication constraint we generate, if any,
543 has a strictly-increased level compared to the ambient level outside
544 the let binding.
545
546 -}
547
548 -- | How should we choose which constraints to quantify over?
549 data InferMode = ApplyMR -- ^ Apply the monomorphism restriction,
550 -- never quantifying over any constraints
551 | EagerDefaulting -- ^ See Note [TcRnExprMode] in TcRnDriver,
552 -- the :type +d case; this mode refuses
553 -- to quantify over any defaultable constraint
554 | NoRestrictions -- ^ Quantify over any constraint that
555 -- satisfies TcType.pickQuantifiablePreds
556
557 instance Outputable InferMode where
558 ppr ApplyMR = text "ApplyMR"
559 ppr EagerDefaulting = text "EagerDefaulting"
560 ppr NoRestrictions = text "NoRestrictions"
561
562 simplifyInfer :: TcLevel -- Used when generating the constraints
563 -> InferMode
564 -> [TcIdSigInst] -- Any signatures (possibly partial)
565 -> [(Name, TcTauType)] -- Variables to be generalised,
566 -- and their tau-types
567 -> WantedConstraints
568 -> TcM ([TcTyVar], -- Quantify over these type variables
569 [EvVar], -- ... and these constraints (fully zonked)
570 TcEvBinds) -- ... binding these evidence variables
571 simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds
572 | isEmptyWC wanteds
573 = do { gbl_tvs <- tcGetGlobalTyCoVars
574 ; dep_vars <- zonkTcTypesAndSplitDepVars (map snd name_taus)
575 ; qtkvs <- quantifyZonkedTyVars gbl_tvs dep_vars
576 ; traceTc "simplifyInfer: empty WC" (ppr name_taus $$ ppr qtkvs)
577 ; return (qtkvs, [], emptyTcEvBinds) }
578
579 | otherwise
580 = do { traceTc "simplifyInfer {" $ vcat
581 [ text "sigs =" <+> ppr sigs
582 , text "binds =" <+> ppr name_taus
583 , text "rhs_tclvl =" <+> ppr rhs_tclvl
584 , text "infer_mode =" <+> ppr infer_mode
585 , text "(unzonked) wanted =" <+> ppr wanteds
586 ]
587
588 ; let partial_sigs = filter isPartialSig sigs
589 psig_theta = concatMap sig_inst_theta partial_sigs
590
591 -- First do full-blown solving
592 -- NB: we must gather up all the bindings from doing
593 -- this solving; hence (runTcSWithEvBinds ev_binds_var).
594 -- And note that since there are nested implications,
595 -- calling solveWanteds will side-effect their evidence
596 -- bindings, so we can't just revert to the input
597 -- constraint.
598
599 ; tc_lcl_env <- TcM.getLclEnv
600 ; ev_binds_var <- TcM.newTcEvBinds
601 ; psig_theta_vars <- mapM TcM.newEvVar psig_theta
602 ; wanted_transformed_incl_derivs
603 <- setTcLevel rhs_tclvl $
604 runTcSWithEvBinds ev_binds_var $
605 do { let loc = mkGivenLoc rhs_tclvl UnkSkol tc_lcl_env
606 psig_givens = mkGivens loc psig_theta_vars
607 ; _ <- solveSimpleGivens psig_givens
608 -- See Note [Add signature contexts as givens]
609 ; solveWanteds wanteds }
610 ; wanted_transformed_incl_derivs <- TcM.zonkWC wanted_transformed_incl_derivs
611
612 -- Find quant_pred_candidates, the predicates that
613 -- we'll consider quantifying over
614 -- NB1: wanted_transformed does not include anything provable from
615 -- the psig_theta; it's just the extra bit
616 -- NB2: We do not do any defaulting when inferring a type, this can lead
617 -- to less polymorphic types, see Note [Default while Inferring]
618
619 ; let wanted_transformed = dropDerivedWC wanted_transformed_incl_derivs
620 ; quant_pred_candidates -- Fully zonked
621 <- if insolubleWC wanted_transformed_incl_derivs
622 then return [] -- See Note [Quantification with errors]
623 -- NB: must include derived errors in this test,
624 -- hence "incl_derivs"
625
626 else do { let quant_cand = approximateWC False wanted_transformed
627 meta_tvs = filter isMetaTyVar $
628 tyCoVarsOfCtsList quant_cand
629
630 ; gbl_tvs <- tcGetGlobalTyCoVars
631 -- Miminise quant_cand. We are not interested in any evidence
632 -- produced, because we are going to simplify wanted_transformed
633 -- again later. All we want here are the predicates over which to
634 -- quantify.
635 --
636 -- If any meta-tyvar unifications take place (unlikely),
637 -- we'll pick that up later.
638
639 -- See Note [Promote _and_ default when inferring]
640 ; let def_tyvar tv
641 = when (not $ tv `elemVarSet` gbl_tvs) $
642 defaultTyVar tv
643 ; mapM_ def_tyvar meta_tvs
644 ; mapM_ (promoteTyVar rhs_tclvl) meta_tvs
645
646 ; clone_wanteds <- mapM cloneWanted (bagToList quant_cand)
647 ; WC { wc_simple = simples }
648 <- setTcLevel rhs_tclvl $
649 simplifyWantedsTcM clone_wanteds
650 -- Discard evidence; result is zonked
651
652 ; return [ ctEvPred ev | ct <- bagToList simples
653 , let ev = ctEvidence ct ] }
654
655 -- NB: quant_pred_candidates is already fully zonked
656
657 -- Decide what type variables and constraints to quantify
658 -- NB: bound_theta are constraints we want to quantify over,
659 -- /apart from/ the psig_theta, which we always quantify over
660 ; (qtvs, bound_theta) <- decideQuantification infer_mode name_taus psig_theta
661 quant_pred_candidates
662
663 -- Promote any type variables that are free in the inferred type
664 -- of the function:
665 -- f :: forall qtvs. bound_theta => zonked_tau
666 -- These variables now become free in the envt, and hence will show
667 -- up whenever 'f' is called. They may currently at rhs_tclvl, but
668 -- they had better be unifiable at the outer_tclvl!
669 -- Example: envt mentions alpha[1]
670 -- tau_ty = beta[2] -> beta[2]
671 -- constraints = alpha ~ [beta]
672 -- we don't quantify over beta (since it is fixed by envt)
673 -- so we must promote it! The inferred type is just
674 -- f :: beta -> beta
675 ; zonked_taus <- mapM (TcM.zonkTcType . snd) name_taus
676 -- decideQuantification turned some meta tyvars into
677 -- quantified skolems, so we have to zonk again
678
679 ; let phi_tkvs = tyCoVarsOfTypes bound_theta -- Already zonked
680 `unionVarSet` tyCoVarsOfTypes zonked_taus
681 promote_tkvs = closeOverKinds phi_tkvs `delVarSetList` qtvs
682
683 ; MASSERT2( closeOverKinds promote_tkvs `subVarSet` promote_tkvs
684 , ppr phi_tkvs $$
685 ppr (closeOverKinds phi_tkvs) $$
686 ppr promote_tkvs $$
687 ppr (closeOverKinds promote_tkvs) )
688 -- we really don't want a type to be promoted when its kind isn't!
689
690 -- promoteTyVar ignores coercion variables
691 ; outer_tclvl <- TcM.getTcLevel
692 ; mapM_ (promoteTyVar outer_tclvl) (nonDetEltsUniqSet promote_tkvs)
693 -- It's OK to use nonDetEltsUniqSet here because promoteTyVar is
694 -- commutative
695
696 -- Emit an implication constraint for the
697 -- remaining constraints from the RHS
698 -- extra_qtvs: see Note [Quantification and partial signatures]
699 ; bound_theta_vars <- mapM TcM.newEvVar bound_theta
700 ; psig_theta_vars <- mapM zonkId psig_theta_vars
701 ; all_qtvs <- add_psig_tvs qtvs
702 [ tv | sig <- partial_sigs
703 , (_,tv) <- sig_inst_skols sig ]
704
705 ; let full_theta = psig_theta ++ bound_theta
706 full_theta_vars = psig_theta_vars ++ bound_theta_vars
707 skol_info = InferSkol [ (name, mkSigmaTy [] full_theta ty)
708 | (name, ty) <- name_taus ]
709 -- Don't add the quantified variables here, because
710 -- they are also bound in ic_skols and we want them
711 -- to be tidied uniformly
712
713 implic = Implic { ic_tclvl = rhs_tclvl
714 , ic_skols = all_qtvs
715 , ic_no_eqs = False
716 , ic_given = full_theta_vars
717 , ic_wanted = wanted_transformed
718 , ic_status = IC_Unsolved
719 , ic_binds = ev_binds_var
720 , ic_info = skol_info
721 , ic_needed = emptyVarSet
722 , ic_env = tc_lcl_env }
723 ; emitImplication implic
724
725 -- All done!
726 ; traceTc "} simplifyInfer/produced residual implication for quantification" $
727 vcat [ text "quant_pred_candidates =" <+> ppr quant_pred_candidates
728 , text "promote_tvs=" <+> ppr promote_tkvs
729 , text "psig_theta =" <+> ppr psig_theta
730 , text "bound_theta =" <+> ppr bound_theta
731 , text "full_theta =" <+> ppr full_theta
732 , text "qtvs =" <+> ppr qtvs
733 , text "implic =" <+> ppr implic ]
734
735 ; return ( qtvs, full_theta_vars, TcEvBinds ev_binds_var ) }
736 where
737 add_psig_tvs qtvs [] = return qtvs
738 add_psig_tvs qtvs (tv:tvs)
739 = do { tv <- zonkTcTyVarToTyVar tv
740 ; if tv `elem` qtvs
741 then add_psig_tvs qtvs tvs
742 else do { mb_tv <- zonkQuantifiedTyVar False tv
743 ; case mb_tv of
744 Nothing -> add_psig_tvs qtvs tvs
745 Just tv -> add_psig_tvs (tv:qtvs) tvs } }
746
747 {- Note [Add signature contexts as givens]
748 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
749 Consider this (Trac #11016):
750 f2 :: (?x :: Int) => _
751 f2 = ?x
752 or this
753 f3 :: a ~ Bool => (a, _)
754 f3 = (True, False)
755 or theis
756 f4 :: (Ord a, _) => a -> Bool
757 f4 x = x==x
758
759 We'll use plan InferGen because there are holes in the type. But:
760 * For f2 we want to have the (?x :: Int) constraint floating around
761 so that the functional dependencies kick in. Otherwise the
762 occurrence of ?x on the RHS produces constraint (?x :: alpha), and
763 we won't unify alpha:=Int.
764 * For f3 we want the (a ~ Bool) available to solve the wanted (a ~ Bool)
765 in the RHS
766 * For f4 we want to use the (Ord a) in the signature to solve the Eq a
767 constraint.
768
769 Solution: in simplifyInfer, just before simplifying the constraints
770 gathered from the RHS, add Given constraints for the context of any
771 type signatures.
772
773 ************************************************************************
774 * *
775 Quantification
776 * *
777 ************************************************************************
778
779 Note [Deciding quantification]
780 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
781 If the monomorphism restriction does not apply, then we quantify as follows:
782
783 * Take the global tyvars, and "grow" them using the equality constraints
784 E.g. if x:alpha is in the environment, and alpha ~ [beta] (which can
785 happen because alpha is untouchable here) then do not quantify over
786 beta, because alpha fixes beta, and beta is effectively free in
787 the environment too
788 These are the mono_tvs
789
790 * Take the free vars of the tau-type (zonked_tau_tvs) and "grow" them
791 using all the constraints. These are tau_tvs_plus
792
793 * Use quantifyTyVars to quantify over (tau_tvs_plus - mono_tvs), being
794 careful to close over kinds, and to skolemise the quantified tyvars.
795 (This actually unifies each quantifies meta-tyvar with a fresh skolem.)
796 Result is qtvs.
797
798 * Filter the constraints using pickQuantifiablePreds and the qtvs.
799 We have to zonk the constraints first, so they "see" the freshly
800 created skolems.
801
802 If the MR does apply, mono_tvs includes all the constrained tyvars --
803 including all covars -- and the quantified constraints are empty/insoluble.
804
805 -}
806
807 decideQuantification
808 :: InferMode
809 -> [(Name, TcTauType)] -- Variables to be generalised
810 -> [PredType] -- All annotated constraints from signatures
811 -> [PredType] -- Candidate theta
812 -> TcM ( [TcTyVar] -- Quantify over these (skolems)
813 , [PredType] ) -- and this context (fully zonked)
814 -- See Note [Deciding quantification]
815 decideQuantification infer_mode name_taus psig_theta candidates
816 = do { gbl_tvs <- tcGetGlobalTyCoVars
817 ; zonked_taus <- mapM TcM.zonkTcType (psig_theta ++ taus)
818 -- psig_theta: see Note [Quantification and partial signatures]
819 ; ovl_strings <- xoptM LangExt.OverloadedStrings
820 ; let DV {dv_kvs = zkvs, dv_tvs = ztvs} = splitDepVarsOfTypes zonked_taus
821 (gbl_cand, quant_cand) -- gbl_cand = do not quantify me
822 = case infer_mode of -- quant_cand = try to quantify me
823 ApplyMR -> (candidates, [])
824 NoRestrictions -> ([], candidates)
825 EagerDefaulting -> partition is_interactive_ct candidates
826 where
827 is_interactive_ct ct
828 | Just (cls, _) <- getClassPredTys_maybe ct
829 = isInteractiveClass ovl_strings cls
830 | otherwise
831 = False
832
833 eq_constraints = filter isEqPred quant_cand
834 constrained_tvs = tyCoVarsOfTypes gbl_cand
835 mono_tvs = growThetaTyVars eq_constraints $
836 gbl_tvs `unionVarSet` constrained_tvs
837 tau_tvs_plus = growThetaTyVarsDSet quant_cand ztvs
838 dvs_plus = DV { dv_kvs = zkvs, dv_tvs = tau_tvs_plus }
839
840 ; qtvs <- quantifyZonkedTyVars mono_tvs dvs_plus
841 -- We don't grow the kvs, as there's no real need to. Recall
842 -- that quantifyTyVars uses the separation between kvs and tvs
843 -- only for defaulting, and we don't want (ever) to default a tv
844 -- to *. So, don't grow the kvs.
845
846 ; quant_cand <- TcM.zonkTcTypes quant_cand
847 -- quantifyTyVars turned some meta tyvars into
848 -- quantified skolems, so we have to zonk again
849
850 ; let qtv_set = mkVarSet qtvs
851 theta = pickQuantifiablePreds qtv_set quant_cand
852 min_theta = mkMinimalBySCs theta
853 -- See Note [Minimize by Superclasses]
854
855 -- Warn about the monomorphism restriction
856 ; warn_mono <- woptM Opt_WarnMonomorphism
857 ; let mr_bites | ApplyMR <- infer_mode
858 = constrained_tvs `intersectsVarSet` tcDepVarSet dvs_plus
859 | otherwise
860 = False
861 ; warnTc (Reason Opt_WarnMonomorphism) (warn_mono && mr_bites) $
862 hang (text "The Monomorphism Restriction applies to the binding"
863 <> plural bndrs <+> text "for" <+> pp_bndrs)
864 2 (text "Consider giving a type signature for"
865 <+> if isSingleton bndrs then pp_bndrs
866 else text "these binders")
867
868 ; traceTc "decideQuantification"
869 (vcat [ text "infer_mode:" <+> ppr infer_mode
870 , text "gbl_cand:" <+> ppr gbl_cand
871 , text "quant_cand:" <+> ppr quant_cand
872 , text "gbl_tvs:" <+> ppr gbl_tvs
873 , text "mono_tvs:" <+> ppr mono_tvs
874 , text "tau_tvs_plus:" <+> ppr tau_tvs_plus
875 , text "qtvs:" <+> ppr qtvs
876 , text "min_theta:" <+> ppr min_theta ])
877 ; return (qtvs, min_theta) }
878 where
879 pp_bndrs = pprWithCommas (quotes . ppr) bndrs
880 (bndrs, taus) = unzip name_taus
881
882 ------------------
883 growThetaTyVars :: ThetaType -> TyCoVarSet -> TyVarSet
884 -- See Note [Growing the tau-tvs using constraints]
885 -- NB: only returns tyvars, never covars
886 growThetaTyVars theta tvs
887 | null theta = tvs_only
888 | otherwise = filterVarSet isTyVar $
889 transCloVarSet mk_next seed_tvs
890 where
891 tvs_only = filterVarSet isTyVar tvs
892 seed_tvs = tvs `unionVarSet` tyCoVarsOfTypes ips
893 (ips, non_ips) = partition isIPPred theta
894 -- See Note [Inheriting implicit parameters] in TcType
895
896 mk_next :: VarSet -> VarSet -- Maps current set to newly-grown ones
897 mk_next so_far = foldr (grow_one so_far) emptyVarSet non_ips
898 grow_one so_far pred tvs
899 | pred_tvs `intersectsVarSet` so_far = tvs `unionVarSet` pred_tvs
900 | otherwise = tvs
901 where
902 pred_tvs = tyCoVarsOfType pred
903
904 ------------------
905 growThetaTyVarsDSet :: ThetaType -> DTyCoVarSet -> DTyVarSet
906 -- See Note [Growing the tau-tvs using constraints]
907 -- NB: only returns tyvars, never covars
908 -- It takes a deterministic set of TyCoVars and returns a deterministic set
909 -- of TyVars.
910 -- The implementation mirrors growThetaTyVars, the only difference is that
911 -- it avoids unionDVarSet and uses more efficient extendDVarSetList.
912 growThetaTyVarsDSet theta tvs
913 | null theta = tvs_only
914 | otherwise = filterDVarSet isTyVar $
915 transCloDVarSet mk_next seed_tvs
916 where
917 tvs_only = filterDVarSet isTyVar tvs
918 seed_tvs = tvs `extendDVarSetList` tyCoVarsOfTypesList ips
919 (ips, non_ips) = partition isIPPred theta
920 -- See Note [Inheriting implicit parameters] in TcType
921
922 mk_next :: DVarSet -> DVarSet -- Maps current set to newly-grown ones
923 mk_next so_far = foldr (grow_one so_far) emptyDVarSet non_ips
924 grow_one so_far pred tvs
925 | any (`elemDVarSet` so_far) pred_tvs = tvs `extendDVarSetList` pred_tvs
926 | otherwise = tvs
927 where
928 pred_tvs = tyCoVarsOfTypeList pred
929
930 {- Note [Quantification and partial signatures]
931 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
932 When choosing type variables to quantify, the basic plan is to
933 quantify over all type variables that are
934 * free in the tau_tvs, and
935 * not forced to be monomorphic (mono_tvs),
936 for example by being free in the environment.
937
938 However, in the case of a partial type signature, be doing inference
939 *in the presence of a type signature*. For example:
940 f :: _ -> a
941 f x = ...
942 or
943 g :: (Eq _a) => _b -> _b
944 In both cases we use plan InferGen, and hence call simplifyInfer.
945 But those 'a' variables are skolems, and we should be sure to quantify
946 over them, for two reasons
947
948 * In the case of a type error
949 f :: _ -> Maybe a
950 f x = True && x
951 The inferred type of 'f' is f :: Bool -> Bool, but there's a
952 left-over error of form (HoleCan (Maybe a ~ Bool)). The error-reporting
953 machine expects to find a binding site for the skolem 'a', so we
954 add it to the ic_skols of the residual implication.
955
956 Note that we /only/ do this to the residual implication. We don't
957 complicate the quantified type variables of 'f' for downstream code;
958 it's just a device to make the error message generator know what to
959 report.
960
961 * Consider the partial type signature
962 f :: (Eq _) => Int -> Int
963 f x = x
964 In normal cases that makes sense; e.g.
965 g :: Eq _a => _a -> _a
966 g x = x
967 where the signature makes the type less general than it could
968 be. But for 'f' we must therefore quantify over the user-annotated
969 constraints, to get
970 f :: forall a. Eq a => Int -> Int
971 (thereby correctly triggering an ambiguity error later). If we don't
972 we'll end up with a strange open type
973 f :: Eq alpha => Int -> Int
974 which isn't ambiguous but is still very wrong. That's why include
975 psig_theta in the variables to quantify over, passed to
976 decideQuantification.
977
978 Note [Quantifying over equality constraints]
979 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
980 Should we quantify over an equality constraint (s ~ t)? In general, we don't.
981 Doing so may simply postpone a type error from the function definition site to
982 its call site. (At worst, imagine (Int ~ Bool)).
983
984 However, consider this
985 forall a. (F [a] ~ Int) => blah
986 Should we quantify over the (F [a] ~ Int)? Perhaps yes, because at the call
987 site we will know 'a', and perhaps we have instance F [Bool] = Int.
988 So we *do* quantify over a type-family equality where the arguments mention
989 the quantified variables.
990
991 Note [Growing the tau-tvs using constraints]
992 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
993 (growThetaTyVars insts tvs) is the result of extending the set
994 of tyvars, tvs, using all conceivable links from pred
995
996 E.g. tvs = {a}, preds = {H [a] b, K (b,Int) c, Eq e}
997 Then growThetaTyVars preds tvs = {a,b,c}
998
999 Notice that
1000 growThetaTyVars is conservative if v might be fixed by vs
1001 => v `elem` grow(vs,C)
1002
1003 Note [Quantification with errors]
1004 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1005 If we find that the RHS of the definition has some absolutely-insoluble
1006 constraints, we abandon all attempts to find a context to quantify
1007 over, and instead make the function fully-polymorphic in whatever
1008 type we have found. For two reasons
1009 a) Minimise downstream errors
1010 b) Avoid spurious errors from this function
1011
1012 But NB that we must include *derived* errors in the check. Example:
1013 (a::*) ~ Int#
1014 We get an insoluble derived error *~#, and we don't want to discard
1015 it before doing the isInsolubleWC test! (Trac #8262)
1016
1017 Note [Default while Inferring]
1018 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1019 Our current plan is that defaulting only happens at simplifyTop and
1020 not simplifyInfer. This may lead to some insoluble deferred constraints.
1021 Example:
1022
1023 instance D g => C g Int b
1024
1025 constraint inferred = (forall b. 0 => C gamma alpha b) /\ Num alpha
1026 type inferred = gamma -> gamma
1027
1028 Now, if we try to default (alpha := Int) we will be able to refine the implication to
1029 (forall b. 0 => C gamma Int b)
1030 which can then be simplified further to
1031 (forall b. 0 => D gamma)
1032 Finally, we /can/ approximate this implication with (D gamma) and infer the quantified
1033 type: forall g. D g => g -> g
1034
1035 Instead what will currently happen is that we will get a quantified type
1036 (forall g. g -> g) and an implication:
1037 forall g. 0 => (forall b. 0 => C g alpha b) /\ Num alpha
1038
1039 Which, even if the simplifyTop defaults (alpha := Int) we will still be left with an
1040 unsolvable implication:
1041 forall g. 0 => (forall b. 0 => D g)
1042
1043 The concrete example would be:
1044 h :: C g a s => g -> a -> ST s a
1045 f (x::gamma) = (\_ -> x) (runST (h x (undefined::alpha)) + 1)
1046
1047 But it is quite tedious to do defaulting and resolve the implication constraints, and
1048 we have not observed code breaking because of the lack of defaulting in inference, so
1049 we don't do it for now.
1050
1051
1052
1053 Note [Minimize by Superclasses]
1054 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1055 When we quantify over a constraint, in simplifyInfer we need to
1056 quantify over a constraint that is minimal in some sense: For
1057 instance, if the final wanted constraint is (Eq alpha, Ord alpha),
1058 we'd like to quantify over Ord alpha, because we can just get Eq alpha
1059 from superclass selection from Ord alpha. This minimization is what
1060 mkMinimalBySCs does. Then, simplifyInfer uses the minimal constraint
1061 to check the original wanted.
1062
1063
1064 Note [Avoid unnecessary constraint simplification]
1065 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1066 -------- NB NB NB (Jun 12) -------------
1067 This note not longer applies; see the notes with Trac #4361.
1068 But I'm leaving it in here so we remember the issue.)
1069 ----------------------------------------
1070 When inferring the type of a let-binding, with simplifyInfer,
1071 try to avoid unnecessarily simplifying class constraints.
1072 Doing so aids sharing, but it also helps with delicate
1073 situations like
1074
1075 instance C t => C [t] where ..
1076
1077 f :: C [t] => ....
1078 f x = let g y = ...(constraint C [t])...
1079 in ...
1080 When inferring a type for 'g', we don't want to apply the
1081 instance decl, because then we can't satisfy (C t). So we
1082 just notice that g isn't quantified over 't' and partition
1083 the constraints before simplifying.
1084
1085 This only half-works, but then let-generalisation only half-works.
1086
1087 *********************************************************************************
1088 * *
1089 * Main Simplifier *
1090 * *
1091 ***********************************************************************************
1092
1093 -}
1094
1095 simplifyWantedsTcM :: [CtEvidence] -> TcM WantedConstraints
1096 -- Solve the specified Wanted constraints
1097 -- Discard the evidence binds
1098 -- Discards all Derived stuff in result
1099 -- Postcondition: fully zonked and unflattened constraints
1100 simplifyWantedsTcM wanted
1101 = do { traceTc "simplifyWantedsTcM {" (ppr wanted)
1102 ; (result, _) <- runTcS (solveWantedsAndDrop (mkSimpleWC wanted))
1103 ; result <- TcM.zonkWC result
1104 ; traceTc "simplifyWantedsTcM }" (ppr result)
1105 ; return result }
1106
1107 solveWantedsAndDrop :: WantedConstraints -> TcS WantedConstraints
1108 -- Since solveWanteds returns the residual WantedConstraints,
1109 -- it should always be called within a runTcS or something similar,
1110 -- Result is not zonked
1111 solveWantedsAndDrop wanted
1112 = do { wc <- solveWanteds wanted
1113 ; return (dropDerivedWC wc) }
1114
1115 solveWanteds :: WantedConstraints -> TcS WantedConstraints
1116 -- so that the inert set doesn't mindlessly propagate.
1117 -- NB: wc_simples may be wanted /or/ derived now
1118 solveWanteds wc@(WC { wc_simple = simples, wc_insol = insols, wc_impl = implics })
1119 = do { traceTcS "solveWanteds {" (ppr wc)
1120
1121 ; wc1 <- solveSimpleWanteds simples
1122 ; let WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 } = wc1
1123
1124 ; (floated_eqs, implics2) <- solveNestedImplications (implics `unionBags` implics1)
1125 ; (no_new_scs, simples2) <- expandSuperClasses simples1
1126
1127 ; traceTcS "solveWanteds middle" $ vcat [ text "simples1 =" <+> ppr simples1
1128 , text "simples2 =" <+> ppr simples2 ]
1129
1130 ; dflags <- getDynFlags
1131 ; final_wc <- simpl_loop 0 (solverIterations dflags) floated_eqs
1132 no_new_scs
1133 (WC { wc_simple = simples2, wc_impl = implics2
1134 , wc_insol = insols `unionBags` insols1 })
1135
1136 ; bb <- TcS.getTcEvBindsMap
1137 ; traceTcS "solveWanteds }" $
1138 vcat [ text "final wc =" <+> ppr final_wc
1139 , text "current evbinds =" <+> ppr (evBindMapBinds bb) ]
1140
1141 ; return final_wc }
1142
1143 simpl_loop :: Int -> IntWithInf -> Cts -> Bool
1144 -> WantedConstraints
1145 -> TcS WantedConstraints
1146 simpl_loop n limit floated_eqs no_new_deriveds
1147 wc@(WC { wc_simple = simples, wc_insol = insols, wc_impl = implics })
1148 | isEmptyBag floated_eqs && no_new_deriveds
1149 = return wc -- Done!
1150
1151 | n `intGtLimit` limit
1152 = do { -- Add an error (not a warning) if we blow the limit,
1153 -- Typically if we blow the limit we are going to report some other error
1154 -- (an unsolved constraint), and we don't want that error to suppress
1155 -- the iteration limit warning!
1156 addErrTcS (hang (text "solveWanteds: too many iterations"
1157 <+> parens (text "limit =" <+> ppr limit))
1158 2 (vcat [ text "Unsolved:" <+> ppr wc
1159 , ppUnless (isEmptyBag floated_eqs) $
1160 text "Floated equalities:" <+> ppr floated_eqs
1161 , ppUnless no_new_deriveds $
1162 text "New deriveds found"
1163 , text "Set limit with -fconstraint-solver-iterations=n; n=0 for no limit"
1164 ]))
1165 ; return wc }
1166
1167 | otherwise
1168 = do { let n_floated = lengthBag floated_eqs
1169 ; csTraceTcS $
1170 text "simpl_loop iteration=" <> int n
1171 <+> (parens $ hsep [ text "no new deriveds =" <+> ppr no_new_deriveds <> comma
1172 , int n_floated <+> text "floated eqs" <> comma
1173 , int (lengthBag simples) <+> text "simples to solve" ])
1174
1175 -- solveSimples may make progress if either float_eqs hold
1176 ; (unifs1, wc1) <- reportUnifications $
1177 solveSimpleWanteds (floated_eqs `unionBags` simples)
1178 -- Put floated_eqs first so they get solved first
1179 -- NB: the floated_eqs may include /derived/ equalities
1180 -- arising from fundeps inside an implication
1181
1182 ; let WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 } = wc1
1183 ; (no_new_scs, simples2) <- expandSuperClasses simples1
1184
1185 -- We have already tried to solve the nested implications once
1186 -- Try again only if we have unified some meta-variables
1187 -- (which is a bit like adding more givens
1188 -- See Note [Cutting off simpl_loop]
1189 ; (floated_eqs2, implics2) <- if unifs1 == 0 && isEmptyBag implics1
1190 then return (emptyBag, implics)
1191 else solveNestedImplications (implics `unionBags` implics1)
1192
1193 ; simpl_loop (n+1) limit floated_eqs2 no_new_scs
1194 (WC { wc_simple = simples2, wc_impl = implics2
1195 , wc_insol = insols `unionBags` insols1 }) }
1196
1197 expandSuperClasses :: Cts -> TcS (Bool, Cts)
1198 -- If there are any unsolved wanteds, expand one step of
1199 -- superclasses for deriveds
1200 -- Returned Bool is True <=> no new superclass constraints added
1201 -- See Note [The superclass story] in TcCanonical
1202 expandSuperClasses unsolved
1203 | not (anyBag superClassesMightHelp unsolved)
1204 = return (True, unsolved)
1205 | otherwise
1206 = do { traceTcS "expandSuperClasses {" empty
1207 ; let (pending_wanted, unsolved') = mapAccumBagL get [] unsolved
1208 get acc ct | Just ct' <- isPendingScDict ct
1209 = (ct':acc, ct')
1210 | otherwise
1211 = (acc, ct)
1212 ; pending_given <- getPendingScDicts
1213 ; if null pending_given && null pending_wanted
1214 then do { traceTcS "End expandSuperClasses no-op }" empty
1215 ; return (True, unsolved) }
1216 else
1217 do { new_given <- makeSuperClasses pending_given
1218 ; solveSimpleGivens new_given
1219 ; new_wanted <- makeSuperClasses pending_wanted
1220 ; traceTcS "End expandSuperClasses }"
1221 (vcat [ text "Given:" <+> ppr pending_given
1222 , text "Wanted:" <+> ppr new_wanted ])
1223 ; return (False, unsolved' `unionBags` listToBag new_wanted) } }
1224
1225 solveNestedImplications :: Bag Implication
1226 -> TcS (Cts, Bag Implication)
1227 -- Precondition: the TcS inerts may contain unsolved simples which have
1228 -- to be converted to givens before we go inside a nested implication.
1229 solveNestedImplications implics
1230 | isEmptyBag implics
1231 = return (emptyBag, emptyBag)
1232 | otherwise
1233 = do { traceTcS "solveNestedImplications starting {" empty
1234 ; (floated_eqs_s, unsolved_implics) <- mapAndUnzipBagM solveImplication implics
1235 ; let floated_eqs = concatBag floated_eqs_s
1236
1237 -- ... and we are back in the original TcS inerts
1238 -- Notice that the original includes the _insoluble_simples so it was safe to ignore
1239 -- them in the beginning of this function.
1240 ; traceTcS "solveNestedImplications end }" $
1241 vcat [ text "all floated_eqs =" <+> ppr floated_eqs
1242 , text "unsolved_implics =" <+> ppr unsolved_implics ]
1243
1244 ; return (floated_eqs, catBagMaybes unsolved_implics) }
1245
1246 solveImplication :: Implication -- Wanted
1247 -> TcS (Cts, -- All wanted or derived floated equalities: var = type
1248 Maybe Implication) -- Simplified implication (empty or singleton)
1249 -- Precondition: The TcS monad contains an empty worklist and given-only inerts
1250 -- which after trying to solve this implication we must restore to their original value
1251 solveImplication imp@(Implic { ic_tclvl = tclvl
1252 , ic_binds = ev_binds_var
1253 , ic_skols = skols
1254 , ic_given = given_ids
1255 , ic_wanted = wanteds
1256 , ic_info = info
1257 , ic_status = status
1258 , ic_env = env })
1259 | isSolvedStatus status
1260 = return (emptyCts, Just imp) -- Do nothing
1261
1262 | otherwise -- Even for IC_Insoluble it is worth doing more work
1263 -- The insoluble stuff might be in one sub-implication
1264 -- and other unsolved goals in another; and we want to
1265 -- solve the latter as much as possible
1266 = do { inerts <- getTcSInerts
1267 ; traceTcS "solveImplication {" (ppr imp $$ text "Inerts" <+> ppr inerts)
1268
1269 -- Solve the nested constraints
1270 ; (no_given_eqs, given_insols, residual_wanted)
1271 <- nestImplicTcS ev_binds_var tclvl $
1272 do { let loc = mkGivenLoc tclvl info env
1273 givens = mkGivens loc given_ids
1274 ; solveSimpleGivens givens
1275
1276 ; residual_wanted <- solveWanteds wanteds
1277 -- solveWanteds, *not* solveWantedsAndDrop, because
1278 -- we want to retain derived equalities so we can float
1279 -- them out in floatEqualities
1280
1281 ; (no_eqs, given_insols) <- getNoGivenEqs tclvl skols
1282 -- Call getNoGivenEqs /after/ solveWanteds, because
1283 -- solveWanteds can augment the givens, via expandSuperClasses,
1284 -- to reveal given superclass equalities
1285
1286 ; return (no_eqs, given_insols, residual_wanted) }
1287
1288 ; (floated_eqs, residual_wanted)
1289 <- floatEqualities skols no_given_eqs residual_wanted
1290
1291 ; traceTcS "solveImplication 2"
1292 (ppr given_insols $$ ppr residual_wanted)
1293 ; let final_wanted = residual_wanted `addInsols` given_insols
1294
1295 ; res_implic <- setImplicationStatus (imp { ic_no_eqs = no_given_eqs
1296 , ic_wanted = final_wanted })
1297
1298 ; (evbinds, tcvs) <- TcS.getTcEvBindsAndTCVs ev_binds_var
1299 ; traceTcS "solveImplication end }" $ vcat
1300 [ text "no_given_eqs =" <+> ppr no_given_eqs
1301 , text "floated_eqs =" <+> ppr floated_eqs
1302 , text "res_implic =" <+> ppr res_implic
1303 , text "implication evbinds =" <+> ppr (evBindMapBinds evbinds)
1304 , text "implication tvcs =" <+> ppr tcvs ]
1305
1306 ; return (floated_eqs, res_implic) }
1307
1308 ----------------------
1309 setImplicationStatus :: Implication -> TcS (Maybe Implication)
1310 -- Finalise the implication returned from solveImplication:
1311 -- * Set the ic_status field
1312 -- * Trim the ic_wanted field to remove Derived constraints
1313 -- Precondition: the ic_status field is not already IC_Solved
1314 -- Return Nothing if we can discard the implication altogether
1315 setImplicationStatus implic@(Implic { ic_binds = ev_binds_var
1316 , ic_status = status
1317 , ic_info = info
1318 , ic_wanted = wc
1319 , ic_needed = old_discarded_needs
1320 , ic_given = givens })
1321 | ASSERT2( not (isSolvedStatus status ), ppr info )
1322 -- Precondition: we only set the status if it is not already solved
1323 some_insoluble
1324 = return $ Just $
1325 implic { ic_status = IC_Insoluble
1326 , ic_needed = new_discarded_needs
1327 , ic_wanted = pruned_wc }
1328
1329 | some_unsolved
1330 = do { traceTcS "setImplicationStatus" $
1331 vcat [ppr givens $$ ppr simples $$ ppr insols $$ ppr mb_implic_needs]
1332 ; return $ Just $
1333 implic { ic_status = IC_Unsolved
1334 , ic_needed = new_discarded_needs
1335 , ic_wanted = pruned_wc }
1336 }
1337
1338 | otherwise -- Everything is solved; look at the implications
1339 -- See Note [Tracking redundant constraints]
1340 = do { ev_binds <- TcS.getTcEvBindsAndTCVs ev_binds_var
1341 ; let all_needs = neededEvVars ev_binds $
1342 solved_implic_needs `unionVarSet` new_discarded_needs
1343
1344 dead_givens | warnRedundantGivens info
1345 = filterOut (`elemVarSet` all_needs) givens
1346 | otherwise = [] -- None to report
1347
1348 final_needs = all_needs `delVarSetList` givens
1349
1350 discard_entire_implication -- Can we discard the entire implication?
1351 = null dead_givens -- No warning from this implication
1352 && isEmptyBag pruned_implics -- No live children
1353 && isEmptyVarSet final_needs -- No needed vars to pass up to parent
1354
1355 final_status = IC_Solved { ics_need = final_needs
1356 , ics_dead = dead_givens }
1357 final_implic = implic { ic_status = final_status
1358 , ic_needed = emptyVarSet -- Irrelevant for IC_Solved
1359 , ic_wanted = pruned_wc }
1360
1361 -- Check that there are no term-level evidence bindings
1362 -- in the cases where we have no place to put them
1363 ; MASSERT2( termEvidenceAllowed info || isEmptyEvBindMap (fst ev_binds)
1364 , ppr info $$ ppr ev_binds )
1365
1366 ; traceTcS "setImplicationStatus 2" $
1367 vcat [ppr givens $$ ppr ev_binds $$ ppr all_needs]
1368 ; return $ if discard_entire_implication
1369 then Nothing
1370 else Just final_implic }
1371 where
1372 WC { wc_simple = simples, wc_impl = implics, wc_insol = insols } = wc
1373
1374 some_insoluble = insolubleWC wc
1375 some_unsolved = not (isEmptyBag simples && isEmptyBag insols)
1376 || isNothing mb_implic_needs
1377
1378 pruned_simples = dropDerivedSimples simples
1379 pruned_insols = dropDerivedInsols insols
1380 (pruned_implics, discarded_needs) = partitionBagWith discard_me implics
1381 pruned_wc = wc { wc_simple = pruned_simples
1382 , wc_insol = pruned_insols
1383 , wc_impl = pruned_implics }
1384 new_discarded_needs = foldrBag unionVarSet old_discarded_needs discarded_needs
1385
1386 mb_implic_needs :: Maybe VarSet
1387 -- Just vs => all implics are IC_Solved, with 'vs' needed
1388 -- Nothing => at least one implic is not IC_Solved
1389 mb_implic_needs = foldrBag add_implic (Just emptyVarSet) pruned_implics
1390 Just solved_implic_needs = mb_implic_needs
1391
1392 add_implic implic acc
1393 | Just vs_acc <- acc
1394 , IC_Solved { ics_need = vs } <- ic_status implic
1395 = Just (vs `unionVarSet` vs_acc)
1396 | otherwise = Nothing
1397
1398 discard_me :: Implication -> Either Implication VarSet
1399 discard_me ic
1400 | IC_Solved { ics_dead = dead_givens, ics_need = needed } <- ic_status ic
1401 -- Fully solved
1402 , null dead_givens -- No redundant givens to report
1403 , isEmptyBag (wc_impl (ic_wanted ic))
1404 -- And no children that might have things to report
1405 = Right needed
1406 | otherwise
1407 = Left ic
1408
1409 warnRedundantGivens :: SkolemInfo -> Bool
1410 warnRedundantGivens (SigSkol ctxt _)
1411 = case ctxt of
1412 FunSigCtxt _ warn_redundant -> warn_redundant
1413 ExprSigCtxt -> True
1414 _ -> False
1415
1416 -- To think about: do we want to report redundant givens for
1417 -- pattern synonyms, PatSynSigSkol? c.f Trac #9953, comment:21.
1418 warnRedundantGivens (InstSkol {}) = True
1419 warnRedundantGivens _ = False
1420
1421 neededEvVars :: (EvBindMap, TcTyVarSet) -> VarSet -> VarSet
1422 -- Find all the evidence variables that are "needed",
1423 -- and then delete all those bound by the evidence bindings
1424 -- See Note [Tracking redundant constraints]
1425 neededEvVars (ev_binds, tcvs) initial_seeds
1426 = (needed `unionVarSet` tcvs) `minusVarSet` bndrs
1427 where
1428 seeds = foldEvBindMap add_wanted initial_seeds ev_binds
1429 needed = transCloVarSet also_needs seeds
1430 bndrs = foldEvBindMap add_bndr emptyVarSet ev_binds
1431
1432 add_wanted :: EvBind -> VarSet -> VarSet
1433 add_wanted (EvBind { eb_is_given = is_given, eb_rhs = rhs }) needs
1434 | is_given = needs -- Add the rhs vars of the Wanted bindings only
1435 | otherwise = evVarsOfTerm rhs `unionVarSet` needs
1436
1437 also_needs :: VarSet -> VarSet
1438 also_needs needs
1439 = nonDetFoldUniqSet add emptyVarSet needs
1440 -- It's OK to use nonDetFoldUFM here because we immediately forget
1441 -- about the ordering by creating a set
1442 where
1443 add v needs
1444 | Just ev_bind <- lookupEvBind ev_binds v
1445 , EvBind { eb_is_given = is_given, eb_rhs = rhs } <- ev_bind
1446 , is_given
1447 = evVarsOfTerm rhs `unionVarSet` needs
1448 | otherwise
1449 = needs
1450
1451 add_bndr :: EvBind -> VarSet -> VarSet
1452 add_bndr (EvBind { eb_lhs = v }) vs = extendVarSet vs v
1453
1454
1455 {-
1456 Note [Tracking redundant constraints]
1457 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1458 With Opt_WarnRedundantConstraints, GHC can report which
1459 constraints of a type signature (or instance declaration) are
1460 redundant, and can be omitted. Here is an overview of how it
1461 works:
1462
1463 ----- What is a redundant constraint?
1464
1465 * The things that can be redundant are precisely the Given
1466 constraints of an implication.
1467
1468 * A constraint can be redundant in two different ways:
1469 a) It is implied by other givens. E.g.
1470 f :: (Eq a, Ord a) => blah -- Eq a unnecessary
1471 g :: (Eq a, a~b, Eq b) => blah -- Either Eq a or Eq b unnecessary
1472 b) It is not needed by the Wanted constraints covered by the
1473 implication E.g.
1474 f :: Eq a => a -> Bool
1475 f x = True -- Equality not used
1476
1477 * To find (a), when we have two Given constraints,
1478 we must be careful to drop the one that is a naked variable (if poss).
1479 So if we have
1480 f :: (Eq a, Ord a) => blah
1481 then we may find [G] sc_sel (d1::Ord a) :: Eq a
1482 [G] d2 :: Eq a
1483 We want to discard d2 in favour of the superclass selection from
1484 the Ord dictionary. This is done by TcInteract.solveOneFromTheOther
1485 See Note [Replacement vs keeping].
1486
1487 * To find (b) we need to know which evidence bindings are 'wanted';
1488 hence the eb_is_given field on an EvBind.
1489
1490 ----- How tracking works
1491
1492 * When the constraint solver finishes solving all the wanteds in
1493 an implication, it sets its status to IC_Solved
1494
1495 - The ics_dead field, of IC_Solved, records the subset of this
1496 implication's ic_given that are redundant (not needed).
1497
1498 - The ics_need field of IC_Solved then records all the
1499 in-scope (given) evidence variables bound by the context, that
1500 were needed to solve this implication, including all its nested
1501 implications. (We remove the ic_given of this implication from
1502 the set, of course.)
1503
1504 * We compute which evidence variables are needed by an implication
1505 in setImplicationStatus. A variable is needed if
1506 a) it is free in the RHS of a Wanted EvBind,
1507 b) it is free in the RHS of an EvBind whose LHS is needed,
1508 c) it is in the ics_need of a nested implication.
1509
1510 * We need to be careful not to discard an implication
1511 prematurely, even one that is fully solved, because we might
1512 thereby forget which variables it needs, and hence wrongly
1513 report a constraint as redundant. But we can discard it once
1514 its free vars have been incorporated into its parent; or if it
1515 simply has no free vars. This careful discarding is also
1516 handled in setImplicationStatus.
1517
1518 ----- Reporting redundant constraints
1519
1520 * TcErrors does the actual warning, in warnRedundantConstraints.
1521
1522 * We don't report redundant givens for *every* implication; only
1523 for those which reply True to TcSimplify.warnRedundantGivens:
1524
1525 - For example, in a class declaration, the default method *can*
1526 use the class constraint, but it certainly doesn't *have* to,
1527 and we don't want to report an error there.
1528
1529 - More subtly, in a function definition
1530 f :: (Ord a, Ord a, Ix a) => a -> a
1531 f x = rhs
1532 we do an ambiguity check on the type (which would find that one
1533 of the Ord a constraints was redundant), and then we check that
1534 the definition has that type (which might find that both are
1535 redundant). We don't want to report the same error twice, so we
1536 disable it for the ambiguity check. Hence using two different
1537 FunSigCtxts, one with the warn-redundant field set True, and the
1538 other set False in
1539 - TcBinds.tcSpecPrag
1540 - TcBinds.tcTySig
1541
1542 This decision is taken in setImplicationStatus, rather than TcErrors
1543 so that we can discard implication constraints that we don't need.
1544 So ics_dead consists only of the *reportable* redundant givens.
1545
1546 ----- Shortcomings
1547
1548 Consider (see Trac #9939)
1549 f2 :: (Eq a, Ord a) => a -> a -> Bool
1550 -- Ord a redundant, but Eq a is reported
1551 f2 x y = (x == y)
1552
1553 We report (Eq a) as redundant, whereas actually (Ord a) is. But it's
1554 really not easy to detect that!
1555
1556
1557 Note [Cutting off simpl_loop]
1558 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1559 It is very important not to iterate in simpl_loop unless there is a chance
1560 of progress. Trac #8474 is a classic example:
1561
1562 * There's a deeply-nested chain of implication constraints.
1563 ?x:alpha => ?y1:beta1 => ... ?yn:betan => [W] ?x:Int
1564
1565 * From the innermost one we get a [D] alpha ~ Int,
1566 but alpha is untouchable until we get out to the outermost one
1567
1568 * We float [D] alpha~Int out (it is in floated_eqs), but since alpha
1569 is untouchable, the solveInteract in simpl_loop makes no progress
1570
1571 * So there is no point in attempting to re-solve
1572 ?yn:betan => [W] ?x:Int
1573 via solveNestedImplications, because we'll just get the
1574 same [D] again
1575
1576 * If we *do* re-solve, we'll get an ininite loop. It is cut off by
1577 the fixed bound of 10, but solving the next takes 10*10*...*10 (ie
1578 exponentially many) iterations!
1579
1580 Conclusion: we should call solveNestedImplications only if we did
1581 some unification in solveSimpleWanteds; because that's the only way
1582 we'll get more Givens (a unification is like adding a Given) to
1583 allow the implication to make progress.
1584 -}
1585
1586 promoteTyVar :: TcLevel -> TcTyVar -> TcM ()
1587 -- When we float a constraint out of an implication we must restore
1588 -- invariant (MetaTvInv) in Note [TcLevel and untouchable type variables] in TcType
1589 -- See Note [Promoting unification variables]
1590 promoteTyVar tclvl tv
1591 | isFloatedTouchableMetaTyVar tclvl tv
1592 = do { cloned_tv <- TcM.cloneMetaTyVar tv
1593 ; let rhs_tv = setMetaTyVarTcLevel cloned_tv tclvl
1594 ; TcM.writeMetaTyVar tv (mkTyVarTy rhs_tv) }
1595 | otherwise
1596 = return ()
1597
1598 promoteTyVarTcS :: TcLevel -> TcTyVar -> TcS ()
1599 -- When we float a constraint out of an implication we must restore
1600 -- invariant (MetaTvInv) in Note [TcLevel and untouchable type variables] in TcType
1601 -- See Note [Promoting unification variables]
1602 -- We don't just call promoteTyVar because we want to use unifyTyVar,
1603 -- not writeMetaTyVar
1604 promoteTyVarTcS tclvl tv
1605 | isFloatedTouchableMetaTyVar tclvl tv
1606 = do { cloned_tv <- TcS.cloneMetaTyVar tv
1607 ; let rhs_tv = setMetaTyVarTcLevel cloned_tv tclvl
1608 ; unifyTyVar tv (mkTyVarTy rhs_tv) }
1609 | otherwise
1610 = return ()
1611
1612 -- | If the tyvar is a RuntimeRep var, set it to LiftedRep.
1613 defaultTyVar :: TcTyVar -> TcM ()
1614 -- Precondition: MetaTyVars only
1615 -- See Note [DefaultTyVar]
1616 defaultTyVar the_tv
1617 | isRuntimeRepVar the_tv
1618 = do { traceTc "defaultTyVar RuntimeRep" (ppr the_tv)
1619 ; writeMetaTyVar the_tv liftedRepTy }
1620
1621 | otherwise = return () -- The common case
1622
1623 -- | Like 'defaultTyVar', but in the TcS monad.
1624 defaultTyVarTcS :: TcTyVar -> TcS Bool
1625 defaultTyVarTcS the_tv
1626 | isRuntimeRepVar the_tv
1627 = do { traceTcS "defaultTyVarTcS RuntimeRep" (ppr the_tv)
1628 ; unifyTyVar the_tv liftedRepTy
1629 ; return True }
1630 | otherwise
1631 = return False -- the common case
1632
1633 approximateWC :: Bool -> WantedConstraints -> Cts
1634 -- Postcondition: Wanted or Derived Cts
1635 -- See Note [ApproximateWC]
1636 approximateWC float_past_equalities wc
1637 = float_wc emptyVarSet wc
1638 where
1639 float_wc :: TcTyCoVarSet -> WantedConstraints -> Cts
1640 float_wc trapping_tvs (WC { wc_simple = simples, wc_impl = implics })
1641 = filterBag is_floatable simples `unionBags`
1642 do_bag (float_implic trapping_tvs) implics
1643 where
1644 is_floatable ct = tyCoVarsOfCt ct `disjointVarSet` trapping_tvs
1645
1646 float_implic :: TcTyCoVarSet -> Implication -> Cts
1647 float_implic trapping_tvs imp
1648 | float_past_equalities || ic_no_eqs imp
1649 = float_wc new_trapping_tvs (ic_wanted imp)
1650 | otherwise -- Take care with equalities
1651 = emptyCts -- See (1) under Note [ApproximateWC]
1652 where
1653 new_trapping_tvs = trapping_tvs `extendVarSetList` ic_skols imp
1654 do_bag :: (a -> Bag c) -> Bag a -> Bag c
1655 do_bag f = foldrBag (unionBags.f) emptyBag
1656
1657 {- Note [ApproximateWC]
1658 ~~~~~~~~~~~~~~~~~~~~~~~
1659 approximateWC takes a constraint, typically arising from the RHS of a
1660 let-binding whose type we are *inferring*, and extracts from it some
1661 *simple* constraints that we might plausibly abstract over. Of course
1662 the top-level simple constraints are plausible, but we also float constraints
1663 out from inside, if they are not captured by skolems.
1664
1665 The same function is used when doing type-class defaulting (see the call
1666 to applyDefaultingRules) to extract constraints that that might be defaulted.
1667
1668 There is one caveat:
1669
1670 1. When infering most-general types (in simplifyInfer), we do *not*
1671 float anything out if the implication binds equality constraints,
1672 because that defeats the OutsideIn story. Consider
1673 data T a where
1674 TInt :: T Int
1675 MkT :: T a
1676
1677 f TInt = 3::Int
1678
1679 We get the implication (a ~ Int => res ~ Int), where so far we've decided
1680 f :: T a -> res
1681 We don't want to float (res~Int) out because then we'll infer
1682 f :: T a -> Int
1683 which is only on of the possible types. (GHC 7.6 accidentally *did*
1684 float out of such implications, which meant it would happily infer
1685 non-principal types.)
1686
1687 HOWEVER (Trac #12797) in findDefaultableGroups we are not worried about
1688 the most-general type; and we /do/ want to float out of equalities.
1689 Hence the boolean flag to approximateWC.
1690
1691 ------ Historical note -----------
1692 There used to be a second caveat, driven by Trac #8155
1693
1694 2. We do not float out an inner constraint that shares a type variable
1695 (transitively) with one that is trapped by a skolem. Eg
1696 forall a. F a ~ beta, Integral beta
1697 We don't want to float out (Integral beta). Doing so would be bad
1698 when defaulting, because then we'll default beta:=Integer, and that
1699 makes the error message much worse; we'd get
1700 Can't solve F a ~ Integer
1701 rather than
1702 Can't solve Integral (F a)
1703
1704 Moreover, floating out these "contaminated" constraints doesn't help
1705 when generalising either. If we generalise over (Integral b), we still
1706 can't solve the retained implication (forall a. F a ~ b). Indeed,
1707 arguably that too would be a harder error to understand.
1708
1709 But this transitive closure stuff gives rise to a complex rule for
1710 when defaulting actually happens, and one that was never documented.
1711 Moreover (Trac #12923), the more complex rule is sometimes NOT what
1712 you want. So I simply removed the extra code to implement the
1713 contamination stuff. There was zero effect on the testsuite (not even
1714 #8155).
1715 ------ End of historical note -----------
1716
1717
1718 Note [DefaultTyVar]
1719 ~~~~~~~~~~~~~~~~~~~
1720 defaultTyVar is used on any un-instantiated meta type variables to
1721 default any RuntimeRep variables to LiftedRep. This is important
1722 to ensure that instance declarations match. For example consider
1723
1724 instance Show (a->b)
1725 foo x = show (\_ -> True)
1726
1727 Then we'll get a constraint (Show (p ->q)) where p has kind (TYPE r),
1728 and that won't match the typeKind (*) in the instance decl. See tests
1729 tc217 and tc175.
1730
1731 We look only at touchable type variables. No further constraints
1732 are going to affect these type variables, so it's time to do it by
1733 hand. However we aren't ready to default them fully to () or
1734 whatever, because the type-class defaulting rules have yet to run.
1735
1736 An alternate implementation would be to emit a derived constraint setting
1737 the RuntimeRep variable to LiftedRep, but this seems unnecessarily indirect.
1738
1739 Note [Promote _and_ default when inferring]
1740 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1741 When we are inferring a type, we simplify the constraint, and then use
1742 approximateWC to produce a list of candidate constraints. Then we MUST
1743
1744 a) Promote any meta-tyvars that have been floated out by
1745 approximateWC, to restore invariant (MetaTvInv) described in
1746 Note [TcLevel and untouchable type variables] in TcType.
1747
1748 b) Default the kind of any meta-tyvars that are not mentioned in
1749 in the environment.
1750
1751 To see (b), suppose the constraint is (C ((a :: OpenKind) -> Int)), and we
1752 have an instance (C ((x:*) -> Int)). The instance doesn't match -- but it
1753 should! If we don't solve the constraint, we'll stupidly quantify over
1754 (C (a->Int)) and, worse, in doing so zonkQuantifiedTyVar will quantify over
1755 (b:*) instead of (a:OpenKind), which can lead to disaster; see Trac #7332.
1756 Trac #7641 is a simpler example.
1757
1758 Note [Promoting unification variables]
1759 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1760 When we float an equality out of an implication we must "promote" free
1761 unification variables of the equality, in order to maintain Invariant
1762 (MetaTvInv) from Note [TcLevel and untouchable type variables] in TcType. for the
1763 leftover implication.
1764
1765 This is absolutely necessary. Consider the following example. We start
1766 with two implications and a class with a functional dependency.
1767
1768 class C x y | x -> y
1769 instance C [a] [a]
1770
1771 (I1) [untch=beta]forall b. 0 => F Int ~ [beta]
1772 (I2) [untch=beta]forall c. 0 => F Int ~ [[alpha]] /\ C beta [c]
1773
1774 We float (F Int ~ [beta]) out of I1, and we float (F Int ~ [[alpha]]) out of I2.
1775 They may react to yield that (beta := [alpha]) which can then be pushed inwards
1776 the leftover of I2 to get (C [alpha] [a]) which, using the FunDep, will mean that
1777 (alpha := a). In the end we will have the skolem 'b' escaping in the untouchable
1778 beta! Concrete example is in indexed_types/should_fail/ExtraTcsUntch.hs:
1779
1780 class C x y | x -> y where
1781 op :: x -> y -> ()
1782
1783 instance C [a] [a]
1784
1785 type family F a :: *
1786
1787 h :: F Int -> ()
1788 h = undefined
1789
1790 data TEx where
1791 TEx :: a -> TEx
1792
1793 f (x::beta) =
1794 let g1 :: forall b. b -> ()
1795 g1 _ = h [x]
1796 g2 z = case z of TEx y -> (h [[undefined]], op x [y])
1797 in (g1 '3', g2 undefined)
1798
1799
1800
1801 *********************************************************************************
1802 * *
1803 * Floating equalities *
1804 * *
1805 *********************************************************************************
1806
1807 Note [Float Equalities out of Implications]
1808 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1809 For ordinary pattern matches (including existentials) we float
1810 equalities out of implications, for instance:
1811 data T where
1812 MkT :: Eq a => a -> T
1813 f x y = case x of MkT _ -> (y::Int)
1814 We get the implication constraint (x::T) (y::alpha):
1815 forall a. [untouchable=alpha] Eq a => alpha ~ Int
1816 We want to float out the equality into a scope where alpha is no
1817 longer untouchable, to solve the implication!
1818
1819 But we cannot float equalities out of implications whose givens may
1820 yield or contain equalities:
1821
1822 data T a where
1823 T1 :: T Int
1824 T2 :: T Bool
1825 T3 :: T a
1826
1827 h :: T a -> a -> Int
1828
1829 f x y = case x of
1830 T1 -> y::Int
1831 T2 -> y::Bool
1832 T3 -> h x y
1833
1834 We generate constraint, for (x::T alpha) and (y :: beta):
1835 [untouchables = beta] (alpha ~ Int => beta ~ Int) -- From 1st branch
1836 [untouchables = beta] (alpha ~ Bool => beta ~ Bool) -- From 2nd branch
1837 (alpha ~ beta) -- From 3rd branch
1838
1839 If we float the equality (beta ~ Int) outside of the first implication and
1840 the equality (beta ~ Bool) out of the second we get an insoluble constraint.
1841 But if we just leave them inside the implications, we unify alpha := beta and
1842 solve everything.
1843
1844 Principle:
1845 We do not want to float equalities out which may
1846 need the given *evidence* to become soluble.
1847
1848 Consequence: classes with functional dependencies don't matter (since there is
1849 no evidence for a fundep equality), but equality superclasses do matter (since
1850 they carry evidence).
1851 -}
1852
1853 floatEqualities :: [TcTyVar] -> Bool
1854 -> WantedConstraints
1855 -> TcS (Cts, WantedConstraints)
1856 -- Main idea: see Note [Float Equalities out of Implications]
1857 --
1858 -- Precondition: the wc_simple of the incoming WantedConstraints are
1859 -- fully zonked, so that we can see their free variables
1860 --
1861 -- Postcondition: The returned floated constraints (Cts) are only
1862 -- Wanted or Derived
1863 --
1864 -- Also performs some unifications (via promoteTyVar), adding to
1865 -- monadically-carried ty_binds. These will be used when processing
1866 -- floated_eqs later
1867 --
1868 -- Subtleties: Note [Float equalities from under a skolem binding]
1869 -- Note [Skolem escape]
1870 floatEqualities skols no_given_eqs
1871 wanteds@(WC { wc_simple = simples })
1872 | not no_given_eqs -- There are some given equalities, so don't float
1873 = return (emptyBag, wanteds) -- Note [Float Equalities out of Implications]
1874 | otherwise
1875 = do { outer_tclvl <- TcS.getTcLevel
1876 ; mapM_ (promoteTyVarTcS outer_tclvl)
1877 (tyCoVarsOfCtsList float_eqs)
1878 -- See Note [Promoting unification variables]
1879
1880 ; traceTcS "floatEqualities" (vcat [ text "Skols =" <+> ppr skols
1881 , text "Simples =" <+> ppr simples
1882 , text "Floated eqs =" <+> ppr float_eqs])
1883 ; return ( float_eqs
1884 , wanteds { wc_simple = remaining_simples } ) }
1885 where
1886 skol_set = mkVarSet skols
1887 (float_eqs, remaining_simples) = partitionBag (usefulToFloat skol_set) simples
1888
1889 usefulToFloat :: VarSet -> Ct -> Bool
1890 usefulToFloat skol_set ct -- The constraint is un-flattened and de-canonicalised
1891 = is_meta_var_eq pred &&
1892 (tyCoVarsOfType pred `disjointVarSet` skol_set)
1893 where
1894 pred = ctPred ct
1895
1896 -- Float out alpha ~ ty, or ty ~ alpha
1897 -- which might be unified outside
1898 -- See Note [Which equalities to float]
1899 is_meta_var_eq pred
1900 | EqPred NomEq ty1 ty2 <- classifyPredType pred
1901 = case (tcGetTyVar_maybe ty1, tcGetTyVar_maybe ty2) of
1902 (Just tv1, _) -> float_tv_eq tv1 ty2
1903 (_, Just tv2) -> float_tv_eq tv2 ty1
1904 _ -> False
1905 | otherwise
1906 = False
1907
1908 float_tv_eq tv1 ty2 -- See Note [Which equalities to float]
1909 = isMetaTyVar tv1
1910 && (not (isSigTyVar tv1) || isTyVarTy ty2)
1911
1912 {- Note [Float equalities from under a skolem binding]
1913 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1914 Which of the simple equalities can we float out? Obviously, only
1915 ones that don't mention the skolem-bound variables. But that is
1916 over-eager. Consider
1917 [2] forall a. F a beta[1] ~ gamma[2], G beta[1] gamma[2] ~ Int
1918 The second constraint doesn't mention 'a'. But if we float it,
1919 we'll promote gamma[2] to gamma'[1]. Now suppose that we learn that
1920 beta := Bool, and F a Bool = a, and G Bool _ = Int. Then we'll
1921 we left with the constraint
1922 [2] forall a. a ~ gamma'[1]
1923 which is insoluble because gamma became untouchable.
1924
1925 Solution: float only constraints that stand a jolly good chance of
1926 being soluble simply by being floated, namely ones of form
1927 a ~ ty
1928 where 'a' is a currently-untouchable unification variable, but may
1929 become touchable by being floated (perhaps by more than one level).
1930
1931 We had a very complicated rule previously, but this is nice and
1932 simple. (To see the notes, look at this Note in a version of
1933 TcSimplify prior to Oct 2014).
1934
1935 Note [Which equalities to float]
1936 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1937 Which equalities should we float? We want to float ones where there
1938 is a decent chance that floating outwards will allow unification to
1939 happen. In particular:
1940
1941 Float out equalities of form (alpha ~ ty) or (ty ~ alpha), where
1942
1943 * alpha is a meta-tyvar.
1944
1945 * And 'alpha' is not a SigTv with 'ty' being a non-tyvar. In that
1946 case, floating out won't help either, and it may affect grouping
1947 of error messages.
1948
1949 Note [Skolem escape]
1950 ~~~~~~~~~~~~~~~~~~~~
1951 You might worry about skolem escape with all this floating.
1952 For example, consider
1953 [2] forall a. (a ~ F beta[2] delta,
1954 Maybe beta[2] ~ gamma[1])
1955
1956 The (Maybe beta ~ gamma) doesn't mention 'a', so we float it, and
1957 solve with gamma := beta. But what if later delta:=Int, and
1958 F b Int = b.
1959 Then we'd get a ~ beta[2], and solve to get beta:=a, and now the
1960 skolem has escaped!
1961
1962 But it's ok: when we float (Maybe beta[2] ~ gamma[1]), we promote beta[2]
1963 to beta[1], and that means the (a ~ beta[1]) will be stuck, as it should be.
1964
1965
1966 *********************************************************************************
1967 * *
1968 * Defaulting and disambiguation *
1969 * *
1970 *********************************************************************************
1971 -}
1972
1973 applyDefaultingRules :: WantedConstraints -> TcS Bool
1974 -- True <=> I did some defaulting, by unifying a meta-tyvar
1975 -- Input WantedConstraints are not necessarily zonked
1976
1977 applyDefaultingRules wanteds
1978 | isEmptyWC wanteds
1979 = return False
1980 | otherwise
1981 = do { info@(default_tys, _) <- getDefaultInfo
1982 ; wanteds <- TcS.zonkWC wanteds
1983
1984 ; let groups = findDefaultableGroups info wanteds
1985
1986 ; traceTcS "applyDefaultingRules {" $
1987 vcat [ text "wanteds =" <+> ppr wanteds
1988 , text "groups =" <+> ppr groups
1989 , text "info =" <+> ppr info ]
1990
1991 ; something_happeneds <- mapM (disambigGroup default_tys) groups
1992
1993 ; traceTcS "applyDefaultingRules }" (ppr something_happeneds)
1994
1995 ; return (or something_happeneds) }
1996
1997 findDefaultableGroups
1998 :: ( [Type]
1999 , (Bool,Bool) ) -- (Overloaded strings, extended default rules)
2000 -> WantedConstraints -- Unsolved (wanted or derived)
2001 -> [(TyVar, [Ct])]
2002 findDefaultableGroups (default_tys, (ovl_strings, extended_defaults)) wanteds
2003 | null default_tys
2004 = []
2005 | otherwise
2006 = [ (tv, map fstOf3 group)
2007 | group@((_,_,tv):_) <- unary_groups
2008 , defaultable_tyvar tv
2009 , defaultable_classes (map sndOf3 group) ]
2010 where
2011 simples = approximateWC True wanteds
2012 (unaries, non_unaries) = partitionWith find_unary (bagToList simples)
2013 unary_groups = equivClasses cmp_tv unaries
2014
2015 unary_groups :: [[(Ct, Class, TcTyVar)]] -- (C tv) constraints
2016 unaries :: [(Ct, Class, TcTyVar)] -- (C tv) constraints
2017 non_unaries :: [Ct] -- and *other* constraints
2018
2019 -- Finds unary type-class constraints
2020 -- But take account of polykinded classes like Typeable,
2021 -- which may look like (Typeable * (a:*)) (Trac #8931)
2022 find_unary :: Ct -> Either (Ct, Class, TyVar) Ct
2023 find_unary cc
2024 | Just (cls,tys) <- getClassPredTys_maybe (ctPred cc)
2025 , [ty] <- filterOutInvisibleTypes (classTyCon cls) tys
2026 -- Ignore invisible arguments for this purpose
2027 , Just tv <- tcGetTyVar_maybe ty
2028 , isMetaTyVar tv -- We might have runtime-skolems in GHCi, and
2029 -- we definitely don't want to try to assign to those!
2030 = Left (cc, cls, tv)
2031 find_unary cc = Right cc -- Non unary or non dictionary
2032
2033 bad_tvs :: TcTyCoVarSet -- TyVars mentioned by non-unaries
2034 bad_tvs = mapUnionVarSet tyCoVarsOfCt non_unaries
2035
2036 cmp_tv (_,_,tv1) (_,_,tv2) = tv1 `compare` tv2
2037
2038 defaultable_tyvar :: TcTyVar -> Bool
2039 defaultable_tyvar tv
2040 = let b1 = isTyConableTyVar tv -- Note [Avoiding spurious errors]
2041 b2 = not (tv `elemVarSet` bad_tvs)
2042 in b1 && (b2 || extended_defaults) -- Note [Multi-parameter defaults]
2043
2044 defaultable_classes :: [Class] -> Bool
2045 defaultable_classes clss
2046 | extended_defaults = any (isInteractiveClass ovl_strings) clss
2047 | otherwise = all is_std_class clss && (any (isNumClass ovl_strings) clss)
2048
2049 -- is_std_class adds IsString to the standard numeric classes,
2050 -- when -foverloaded-strings is enabled
2051 is_std_class cls = isStandardClass cls ||
2052 (ovl_strings && (cls `hasKey` isStringClassKey))
2053
2054 ------------------------------
2055 disambigGroup :: [Type] -- The default types
2056 -> (TcTyVar, [Ct]) -- All classes of the form (C a)
2057 -- sharing same type variable
2058 -> TcS Bool -- True <=> something happened, reflected in ty_binds
2059
2060 disambigGroup [] _
2061 = return False
2062 disambigGroup (default_ty:default_tys) group@(the_tv, wanteds)
2063 = do { traceTcS "disambigGroup {" (vcat [ ppr default_ty, ppr the_tv, ppr wanteds ])
2064 ; fake_ev_binds_var <- TcS.newTcEvBinds
2065 ; tclvl <- TcS.getTcLevel
2066 ; success <- nestImplicTcS fake_ev_binds_var (pushTcLevel tclvl) try_group
2067
2068 ; if success then
2069 -- Success: record the type variable binding, and return
2070 do { unifyTyVar the_tv default_ty
2071 ; wrapWarnTcS $ warnDefaulting wanteds default_ty
2072 ; traceTcS "disambigGroup succeeded }" (ppr default_ty)
2073 ; return True }
2074 else
2075 -- Failure: try with the next type
2076 do { traceTcS "disambigGroup failed, will try other default types }"
2077 (ppr default_ty)
2078 ; disambigGroup default_tys group } }
2079 where
2080 try_group
2081 | Just subst <- mb_subst
2082 = do { lcl_env <- TcS.getLclEnv
2083 ; let loc = CtLoc { ctl_origin = GivenOrigin UnkSkol
2084 , ctl_env = lcl_env
2085 , ctl_t_or_k = Nothing
2086 , ctl_depth = initialSubGoalDepth }
2087 ; wanted_evs <- mapM (newWantedEvVarNC loc . substTy subst . ctPred)
2088 wanteds
2089 ; fmap isEmptyWC $
2090 solveSimpleWanteds $ listToBag $
2091 map mkNonCanonical wanted_evs }
2092
2093 | otherwise
2094 = return False
2095
2096 the_ty = mkTyVarTy the_tv
2097 mb_subst = tcMatchTyKi the_ty default_ty
2098 -- Make sure the kinds match too; hence this call to tcMatchTyKi
2099 -- E.g. suppose the only constraint was (Typeable k (a::k))
2100 -- With the addition of polykinded defaulting we also want to reject
2101 -- ill-kinded defaulting attempts like (Eq []) or (Foldable Int) here.
2102
2103 -- In interactive mode, or with -XExtendedDefaultRules,
2104 -- we default Show a to Show () to avoid graututious errors on "show []"
2105 isInteractiveClass :: Bool -- -XOverloadedStrings?
2106 -> Class -> Bool
2107 isInteractiveClass ovl_strings cls
2108 = isNumClass ovl_strings cls || (classKey cls `elem` interactiveClassKeys)
2109
2110 -- isNumClass adds IsString to the standard numeric classes,
2111 -- when -foverloaded-strings is enabled
2112 isNumClass :: Bool -- -XOverloadedStrings?
2113 -> Class -> Bool
2114 isNumClass ovl_strings cls
2115 = isNumericClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
2116
2117
2118 {-
2119 Note [Avoiding spurious errors]
2120 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2121 When doing the unification for defaulting, we check for skolem
2122 type variables, and simply don't default them. For example:
2123 f = (*) -- Monomorphic
2124 g :: Num a => a -> a
2125 g x = f x x
2126 Here, we get a complaint when checking the type signature for g,
2127 that g isn't polymorphic enough; but then we get another one when
2128 dealing with the (Num a) context arising from f's definition;
2129 we try to unify a with Int (to default it), but find that it's
2130 already been unified with the rigid variable from g's type sig.
2131
2132 Note [Multi-parameter defaults]
2133 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2134 With -XExtendedDefaultRules, we default only based on single-variable
2135 constraints, but do not exclude from defaulting any type variables which also
2136 appear in multi-variable constraints. This means that the following will
2137 default properly:
2138
2139 default (Integer, Double)
2140
2141 class A b (c :: Symbol) where
2142 a :: b -> Proxy c
2143
2144 instance A Integer c where a _ = Proxy
2145
2146 main = print (a 5 :: Proxy "5")
2147
2148 Note that if we change the above instance ("instance A Integer") to
2149 "instance A Double", we get an error:
2150
2151 No instance for (A Integer "5")
2152
2153 This is because the first defaulted type (Integer) has successfully satisfied
2154 its single-parameter constraints (in this case Num).
2155 -}