1 {-# LANGUAGE CPP #-}

4 simplifyInfer,

6 simplifyAmbiguityCheck,

7 simplifyDefault,

9 solveWantedsTcM,

11 -- For Rules we need these twoo

12 solveWanteds, runTcS

17 import Bag

23 import Inst

26 import ListSetOps

28 import Name

29 import Outputable

30 import PrelInfo

31 import PrelNames

32 import TcErrors

33 import TcEvidence

34 import TcInteract

38 import TcType

44 import Util

45 import Var

46 import VarSet

49 import FastString

54 {-

55 *********************************************************************************

56 * *

57 * External interface *

58 * *

59 *********************************************************************************

60 -}

63 -- Simplify top-level constraints

64 -- Usually these will be implications,

65 -- but when there is nothing to quantify we don't wrap

66 -- in a degenerate implication, so we do that here instead

67 simplifyTop wanteds

78 -- grab current error messages and clear, warnAllUnsolved will

79 -- update error messages which we'll grab and then restore saved

80 -- messges.

91 ; recordUnsafeInfer whyUnsafe

92 }

98 -- ^ See Note [Safe Haskell Overlapping Instances Implementation]

103 -- See Note [Top-level Defaulting Plan]

104 simpl_top wanteds

106 -- This is where the main work happens

110 where

112 try_tyvar_defaulting wc

113 | isEmptyWC wc

115 | otherwise

118 -- zonkTyVarsAndFV: the wc_first_go is not yet zonked

119 -- filter isMetaTyVar: we might have runtime-skolems in GHCi,

120 -- and we definitely don't want to try to assign to those!

124 -- (defaulting returns fresh vars)

125 then try_class_defaulting wc

127 -- See Note [Must simplify after defaulting]

131 try_class_defaulting wc

132 | isEmptyWC wc

136 -- See Note [Top-level Defaulting Plan]

142 {-

143 Note [When to do type-class defaulting]

144 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

145 In GHC 7.6 and 7.8.2, we did type-class defaulting only if insolubleWC

146 was false, on the grounds that defaulting can't help solve insoluble

147 constraints. But if we *don't* do defaulting we may report a whole

148 lot of errors that would be solved by defaulting; these errors are

149 quite spurious because fixing the single insoluble error means that

150 defaulting happens again, which makes all the other errors go away.

151 This is jolly confusing: Trac #9033.

153 So it seems better to always do type-class defaulting.

155 However, always doing defaulting does mean that we'll do it in

156 situations like this (Trac #5934):

157 run :: (forall s. GenST s) -> Int

158 run = fromInteger 0

159 We don't unify the return type of fromInteger with the given function

160 type, because the latter involves foralls. So we're left with

161 (Num alpha, alpha ~ (forall s. GenST s) -> Int)

162 Now we do defaulting, get alpha := Integer, and report that we can't

163 match Integer with (forall s. GenST s) -> Int. That's not totally

164 stupid, but perhaps a little strange.

166 Another potential alternative would be to suppress *all* non-insoluble

167 errors if there are *any* insoluble errors, anywhere, but that seems

168 too drastic.

170 Note [Must simplify after defaulting]

171 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

172 We may have a deeply buried constraint

173 (t:*) ~ (a:Open)

174 which we couldn't solve because of the kind incompatibility, and 'a' is free.

175 Then when we default 'a' we can solve the constraint. And we want to do

176 that before starting in on type classes. We MUST do it before reporting

177 errors, because it isn't an error! Trac #7967 was due to this.

179 Note [Top-level Defaulting Plan]

180 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

181 We have considered two design choices for where/when to apply defaulting.

182 (i) Do it in SimplCheck mode only /whenever/ you try to solve some

183 simple constraints, maybe deep inside the context of implications.

184 This used to be the case in GHC 7.4.1.

185 (ii) Do it in a tight loop at simplifyTop, once all other constraint has

186 finished. This is the current story.

188 Option (i) had many disadvantages:

189 a) First it was deep inside the actual solver,

190 b) Second it was dependent on the context (Infer a type signature,

191 or Check a type signature, or Interactive) since we did not want

192 to always start defaulting when inferring (though there is an exception to

193 this see Note [Default while Inferring])

194 c) It plainly did not work. Consider typecheck/should_compile/DfltProb2.hs:

195 f :: Int -> Bool

196 f x = const True (\y -> let w :: a -> a

197 w a = const a (y+1)

198 in w y)

199 We will get an implication constraint (for beta the type of y):

200 [untch=beta] forall a. 0 => Num beta

201 which we really cannot default /while solving/ the implication, since beta is

202 untouchable.

204 Instead our new defaulting story is to pull defaulting out of the solver loop and

205 go with option (i), implemented at SimplifyTop. Namely:

206 - First have a go at solving the residual constraint of the whole program

207 - Try to approximate it with a simple constraint

208 - Figure out derived defaulting equations for that simple constraint

209 - Go round the loop again if you did manage to get some equations

211 Now, that has to do with class defaulting. However there exists type variable /kind/

212 defaulting. Again this is done at the top-level and the plan is:

213 - At the top-level, once you had a go at solving the constraint, do

214 figure out /all/ the touchable unification variables of the wanted constraints.

215 - Apply defaulting to their kinds

217 More details in Note [DefaultTyVar].

219 Note [Safe Haskell Overlapping Instances]

220 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

221 In Safe Haskell, we apply an extra restriction to overlapping instances. The

222 motive is to prevent untrusted code provided by a third-party, changing the

223 behavior of trusted code through type-classes. This is due to the global and

224 implicit nature of type-classes that can hide the source of the dictionary.

226 Another way to state this is: if a module M compiles without importing another

227 module N, changing M to import N shouldn't change the behavior of M.

229 Overlapping instances with type-classes can violate this principle. However,

230 overlapping instances aren't always unsafe. They are just unsafe when the most

231 selected dictionary comes from untrusted code (code compiled with -XSafe) and

232 overlaps instances provided by other modules.

234 In particular, in Safe Haskell at a call site with overlapping instances, we

235 apply the following rule to determine if it is a 'unsafe' overlap:

237 1) Most specific instance, I1, defined in an `-XSafe` compiled module.

238 2) I1 is an orphan instance or a MPTC.

239 3) At least one overlapped instance, Ix, is both:

240 A) from a different module than I1

241 B) Ix is not marked `OVERLAPPABLE`

243 This is a slightly involved heuristic, but captures the situation of an

244 imported module N changing the behavior of existing code. For example, if

245 condition (2) isn't violated, then the module author M must depend either on a

246 type-class or type defined in N.

248 Secondly, when should these heuristics be enforced? We enforced them when the

249 type-class method call site is in a module marked `-XSafe` or `-XTrustworthy`.

250 This allows `-XUnsafe` modules to operate without restriction, and for Safe

251 Haskell inferrence to infer modules with unsafe overlaps as unsafe.

253 One alternative design would be to also consider if an instance was imported as

254 a `safe` import or not and only apply the restriction to instances imported

255 safely. However, since instances are global and can be imported through more

256 than one path, this alternative doesn't work.

258 Note [Safe Haskell Overlapping Instances Implementation]

259 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

261 How is this implemented? It's compilcated! So we'll step through it all:

263 1) `InstEnv.lookupInstEnv` -- Performs instance resolution, so this is where

264 we check if a particular type-class method call is safe or unsafe. We do this

265 through the return type, `ClsInstLookupResult`, where the last parameter is a

266 list of instances that are unsafe to overlap. When the method call is safe,

267 the list is null.

269 2) `TcInteract.matchClassInst` -- This module drives the instance resolution /

270 dictionary generation. The return type is `LookupInstResult`, which either

271 says no instance matched, or one found and if it was a safe or unsafe overlap.

273 3) `TcInteract.doTopReactDict` -- Takes a dictionary / class constraint and

274 tries to resolve it by calling (in part) `matchClassInst`. The resolving

275 mechanism has a work list (of constraints) that it process one at a time. If

276 the constraint can't be resolved, it's added to an inert set. When compiling

277 an `-XSafe` or `-XTrustworthy` module we follow this approach as we know

278 compilation should fail. These are handled as normal constraint resolution

279 failures from here-on (see step 6).

281 Otherwise, we may be inferring safety (or using `-fwarn-unsafe`) and

282 compilation should succeed, but print warnings and/or mark the compiled module

283 as `-XUnsafe`. In this case, we call `insertSafeOverlapFailureTcS` which adds

284 the unsafe (but resolved!) constraint to the `inert_safehask` field of

285 `InertCans`.

287 4) `TcSimplify.simpl_top` -- Top-level function for driving the simplifier for

288 constraint resolution. Once finished, we call `getSafeOverlapFailures` to

289 retrieve the list of overlapping instances that were successfully resolved,

290 but unsafe. Remember, this is only applicable for generating warnings

291 (`-fwarn-unsafe`) or inferring a module unsafe. `-XSafe` and `-XTrustworthy`

292 cause compilation failure by not resolving the unsafe constraint at all.

293 `simpl_top` returns a list of unresolved constraints (all types), and resolved

294 (but unsafe) resolved dictionary constraints.

296 5) `TcSimplify.simplifyTop` -- Is the caller of `simpl_top`. For unresolved

297 constraints, it calls `TcErrors.reportUnsolved`, while for unsafe overlapping

298 instance constraints, it calls `TcErrors.warnAllUnsolved`. Both functions

299 convert constraints into a warning message for the user.

301 6) `TcErrors.*Unsolved` -- Generates error messages for conastraints by

302 actually calling `InstEnv.lookupInstEnv` again! Yes, confusing, but all we

303 know is the constraint that is unresolved or unsafe. For dictionary, this is

304 know we need a dictionary of type C, but not what instances are available and

305 how they overlap. So we once again call `lookupInstEnv` to figure that out so

306 we can generate a helpful error message.

308 7) `TcSimplify.simplifyTop` -- In the case of `warnAllUnsolved` for resolved,

309 but unsafe dictionary constraints, we collect the generated warning message

310 (pop it) and call `TcRnMonad.recordUnsafeInfer` to mark the module we are

311 compiling as unsafe, passing the warning message along as the reason.

313 8) `TcRnMonad.recordUnsafeInfer` -- Save the unsafe result and reason in an

314 IORef called `tcg_safeInfer`.

316 9) `HscMain.tcRnModule'` -- Reads `tcg_safeInfer` after type-checking, calling

317 `HscMain.markUnsafeInfer` (passing the reason along) when safe-inferrence

318 failed.

319 -}

321 ------------------

323 simplifyAmbiguityCheck ty wanteds

324 = do { traceTc "simplifyAmbiguityCheck {" (text "type = " <+> ppr ty $$ text "wanted = " <+> ppr wanteds)

328 -- Normally report all errors; but with -XAllowAmbiguousTypes

329 -- report only insoluble ones, since they represent genuinely

330 -- inaccessible code

339 ------------------

341 simplifyInteractive wanteds

343 simplifyTop wanteds

345 ------------------

348 simplifyDefault theta

354 -- See Note [Deferring coercion errors to runtime]

355 ; reportAllUnsolved unsolved

360 {-

361 *********************************************************************************

362 * *

363 * Inference

364 * *

365 ***********************************************************************************

367 Note [Inferring the type of a let-bound variable]

368 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

369 Consider

370 f x = rhs

372 To infer f's type we do the following:

373 * Gather the constraints for the RHS with ambient level *one more than*

374 the current one. This is done by the call

375 pushLevelAndCaptureConstraints (tcMonoBinds...)

376 in TcBinds.tcPolyInfer

378 * Call simplifyInfer to simplify the constraints and decide what to

379 quantify over. We pass in the level used for the RHS constraints,

380 here called rhs_tclvl.

382 This ensures that the implication constraint we generate, if any,

383 has a strictly-increased level compared to the ambient level outside

384 the let binding.

385 -}

390 -- and their tau-types

391 -> WantedConstraints

395 -- so the results type is not as general as

396 -- it could be

398 simplifyInfer rhs_tclvl apply_mr name_taus wanteds

399 | isEmptyWC wanteds

405 | otherwise

411 ]

413 -- Historical note: Before step 2 we used to have a

414 -- HORRIBLE HACK described in Note [Avoid unecessary

415 -- constraint simplification] but, as described in Trac

416 -- #4361, we have taken in out now. That's why we start

417 -- with step 2!

419 -- Step 2) First try full-blown solving

421 -- NB: we must gather up all the bindings from doing

422 -- this solving; hence (runTcSWithEvBinds ev_binds_var).

423 -- And note that since there are nested implications,

424 -- calling solveWanteds will side-effect their evidence

425 -- bindings, so we can't just revert to the input

426 -- constraint.

433 -- Step 4) Candidates for quantification are an approximation of wanted_transformed

434 -- NB: Already the fixpoint of any unifications that may have happened

435 -- NB: We do not do any defaulting when inferring a type, this can lead

436 -- to less polymorphic types, see Note [Default while Inferring]

444 -- NB: must include derived errors in this test,

445 -- hence "incl_derivs"

450 -- Miminise quant_cand. We are not interested in any evidence

451 -- produced, because we are going to simplify wanted_transformed

452 -- again later. All we want here is the predicates over which to

453 -- quantify.

454 --

455 -- If any meta-tyvar unifications take place (unlikely), we'll

456 -- pick that up later.

460 runTcSWithEvBinds null_ev_binds_var $

462 -- See Note [Promote _and_ default when inferring]

469 -- NB: quant_pred_candidates is already fully zonked

471 -- Decide what type variables and constraints to quantify

475 <- decideQuantification apply_mr quant_pred_candidates zonked_tau_tvs

477 -- Emit an implication constraint for the

478 -- remaining constraints from the RHS

482 -- Don't add the quantified variables here, because

483 -- they are also bound in ic_skols and we want them

484 -- to be tidied uniformly

495 ; emitImplication implic

497 -- Promote any type variables that are free in the inferred type

498 -- of the function:

499 -- f :: forall qtvs. bound_theta => zonked_tau

500 -- These variables now become free in the envt, and hence will show

501 -- up whenever 'f' is called. They may currently at rhs_tclvl, but

502 -- they had better be unifiable at the outer_tclvl!

503 -- Example: envt mentions alpha[1]

504 -- tau_ty = beta[2] -> beta[2]

505 -- consraints = alpha ~ [beta]

506 -- we don't quantify over beta (since it is fixed by envt)

507 -- so we must promote it! The inferred type is just

508 -- f :: beta -> beta

511 -- decideQuantification turned some meta tyvars into

512 -- quantified skolems, so we have to zonk again

518 -- All done!

532 {-

533 ************************************************************************

534 * *

535 Quantification

536 * *

537 ************************************************************************

539 Note [Deciding quantification]

540 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

541 If the monomorphism restriction does not apply, then we quantify as follows:

542 * Take the global tyvars, and "grow" them using the equality constraints

543 E.g. if x:alpha is in the environment, and alpha ~ [beta] (which can

544 happen because alpha is untouchable here) then do not quantify over

545 beta, because alpha fixes beta, and beta is effectively free in

546 the environment too

547 These are the mono_tvs

549 * Take the free vars of the tau-type (zonked_tau_tvs) and "grow" them

550 using all the constraints. These are tau_tvs_plus

552 * Use quantifyTyVars to quantify over (tau_tvs_plus - mono_tvs), being

553 careful to close over kinds, and to skolemise the quantified tyvars.

554 (This actually unifies each quantifies meta-tyvar with a fresh skolem.)

555 Result is qtvs.

557 * Filter the constraints using pickQuantifyablePreds and the qtvs.

558 We have to zonk the constraints first, so they "see" the freshly

559 created skolems.

561 If the MR does apply, mono_tvs includes all the constrained tyvars,

562 and the quantified constraints are empty.

563 -}

565 decideQuantification

571 -- See Note [Deciding quantification]

572 decideQuantification apply_mr constraints zonked_tau_tvs

573 | apply_mr -- Apply the Monomorphism restriction

576 mono_tvs = gbl_tvs `unionVarSet` constrained_tvs

577 mr_bites = constrained_tvs `intersectsVarSet` zonked_tau_tvs

579 ; traceTc "decideQuantification 1" (vcat [ppr constraints, ppr gbl_tvs, ppr mono_tvs, ppr qtvs])

582 | otherwise

585 tau_tvs_plus = growThetaTyVars constraints zonked_tau_tvs

588 -- quantifyTyVars turned some meta tyvars into

589 -- quantified skolems, so we have to zonk again

598 ------------------

602 -- This function decides whether a particular constraint shoudl be

603 -- quantified over, given the type variables that are being quantified

604 pickQuantifiablePreds qtvs theta

607 where

608 pick_me flex_ctxt pred

610 ClassPred cls tys

615 -- Representational equality is like a class constraint

617 EqPred NomEq ty1 ty2 -> quant_fun ty1 || quant_fun ty2

618 IrredPred ty -> tyVarsOfType ty `intersectsVarSet` qtvs

620 pick_cls_pred flex_ctxt tys

621 = tyVarsOfTypes tys `intersectsVarSet` qtvs

623 -- Only quantify over predicates that checkValidType

624 -- will pass! See Trac #10351.

626 -- See Note [Quantifying over equality constraints]

627 quant_fun ty

630 -> tyVarsOfTypes tys `intersectsVarSet` qtvs

633 ------------------

635 -- See Note [Growing the tau-tvs using constraints]

636 growThetaTyVars theta tvs

639 where

640 seed_tvs = tvs `unionVarSet` tyVarsOfTypes ips

642 -- See note [Inheriting implicit parameters]

646 grow_one so_far pred tvs

647 | pred_tvs `intersectsVarSet` so_far = tvs `unionVarSet` pred_tvs

649 where

652 {-

653 Note [Quantifying over equality constraints]

654 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

655 Should we quantify over an equality constraint (s ~ t)? In general, we don't.

656 Doing so may simply postpone a type error from the function definition site to

657 its call site. (At worst, imagine (Int ~ Bool)).

659 However, consider this

660 forall a. (F [a] ~ Int) => blah

661 Should we quantify over the (F [a] ~ Int). Perhaps yes, because at the call

662 site we will know 'a', and perhaps we have instance F [Bool] = Int.

663 So we *do* quantify over a type-family equality where the arguments mention

664 the quantified variables.

666 Note [Growing the tau-tvs using constraints]

667 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

668 (growThetaTyVars insts tvs) is the result of extending the set

669 of tyvars tvs using all conceivable links from pred

671 E.g. tvs = {a}, preds = {H [a] b, K (b,Int) c, Eq e}

672 Then growThetaTyVars preds tvs = {a,b,c}

674 Notice that

675 growThetaTyVars is conservative if v might be fixed by vs

676 => v `elem` grow(vs,C)

678 Note [Inheriting implicit parameters]

679 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

680 Consider this:

682 f x = (x::Int) + ?y

684 where f is *not* a top-level binding.

685 From the RHS of f we'll get the constraint (?y::Int).

686 There are two types we might infer for f:

688 f :: Int -> Int

690 (so we get ?y from the context of f's definition), or

692 f :: (?y::Int) => Int -> Int

694 At first you might think the first was better, because then

695 ?y behaves like a free variable of the definition, rather than

696 having to be passed at each call site. But of course, the WHOLE

697 IDEA is that ?y should be passed at each call site (that's what

698 dynamic binding means) so we'd better infer the second.

700 BOTTOM LINE: when *inferring types* you must quantify over implicit

701 parameters, *even if* they don't mention the bound type variables.

702 Reason: because implicit parameters, uniquely, have local instance

703 declarations. See the pickQuantifiablePreds.

705 Note [Quantification with errors]

706 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

707 If we find that the RHS of the definition has some absolutely-insoluble

708 constraints, we abandon all attempts to find a context to quantify

709 over, and instead make the function fully-polymorphic in whatever

710 type we have found. For two reasons

711 a) Minimise downstream errors

712 b) Avoid spurious errors from this function

714 But NB that we must include *derived* errors in the check. Example:

715 (a::*) ~ Int#

716 We get an insoluble derived error *~#, and we don't want to discard

717 it before doing the isInsolubleWC test! (Trac #8262)

719 Note [Default while Inferring]

720 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

721 Our current plan is that defaulting only happens at simplifyTop and

722 not simplifyInfer. This may lead to some insoluble deferred constraints

723 Example:

725 instance D g => C g Int b

727 constraint inferred = (forall b. 0 => C gamma alpha b) /\ Num alpha

728 type inferred = gamma -> gamma

730 Now, if we try to default (alpha := Int) we will be able to refine the implication to

731 (forall b. 0 => C gamma Int b)

732 which can then be simplified further to

733 (forall b. 0 => D gamma)

734 Finally we /can/ approximate this implication with (D gamma) and infer the quantified

735 type: forall g. D g => g -> g

737 Instead what will currently happen is that we will get a quantified type

738 (forall g. g -> g) and an implication:

739 forall g. 0 => (forall b. 0 => C g alpha b) /\ Num alpha

741 which, even if the simplifyTop defaults (alpha := Int) we will still be left with an

742 unsolvable implication:

743 forall g. 0 => (forall b. 0 => D g)

745 The concrete example would be:

746 h :: C g a s => g -> a -> ST s a

747 f (x::gamma) = (\_ -> x) (runST (h x (undefined::alpha)) + 1)

749 But it is quite tedious to do defaulting and resolve the implication constraints and

750 we have not observed code breaking because of the lack of defaulting in inference so

751 we don't do it for now.

755 Note [Minimize by Superclasses]

756 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

757 When we quantify over a constraint, in simplifyInfer we need to

758 quantify over a constraint that is minimal in some sense: For

759 instance, if the final wanted constraint is (Eq alpha, Ord alpha),

760 we'd like to quantify over Ord alpha, because we can just get Eq alpha

761 from superclass selection from Ord alpha. This minimization is what

762 mkMinimalBySCs does. Then, simplifyInfer uses the minimal constraint

763 to check the original wanted.

766 Note [Avoid unecessary constraint simplification]

767 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

768 -------- NB NB NB (Jun 12) -------------

769 This note not longer applies; see the notes with Trac #4361.

770 But I'm leaving it in here so we remember the issue.)

771 ----------------------------------------

772 When inferring the type of a let-binding, with simplifyInfer,

773 try to avoid unnecessarily simplifying class constraints.

774 Doing so aids sharing, but it also helps with delicate

775 situations like

777 instance C t => C [t] where ..

779 f :: C [t] => ....

780 f x = let g y = ...(constraint C [t])...

781 in ...

782 When inferring a type for 'g', we don't want to apply the

783 instance decl, because then we can't satisfy (C t). So we

784 just notice that g isn't quantified over 't' and partition

785 the constraints before simplifying.

787 This only half-works, but then let-generalisation only half-works.

790 *********************************************************************************

791 * *

792 * Main Simplifier *

793 * *

794 ***********************************************************************************

796 Note [Deferring coercion errors to runtime]

797 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

798 While developing, sometimes it is desirable to allow compilation to succeed even

799 if there are type errors in the code. Consider the following case:

801 module Main where

803 a :: Int

804 a = 'a'

806 main = print "b"

808 Even though `a` is ill-typed, it is not used in the end, so if all that we're

809 interested in is `main` it is handy to be able to ignore the problems in `a`.

811 Since we treat type equalities as evidence, this is relatively simple. Whenever

812 we run into a type mismatch in TcUnify, we normally just emit an error. But it

813 is always safe to defer the mismatch to the main constraint solver. If we do

814 that, `a` will get transformed into

816 co :: Int ~ Char

817 co = ...

819 a :: Int

820 a = 'a' `cast` co

822 The constraint solver would realize that `co` is an insoluble constraint, and

823 emit an error with `reportUnsolved`. But we can also replace the right-hand side

824 of `co` with `error "Deferred type error: Int ~ Char"`. This allows the program

825 to compile, and it will run fine unless we evaluate `a`. This is what

826 `deferErrorsToRuntime` does.

828 It does this by keeping track of which errors correspond to which coercion

829 in TcErrors (with ErrEnv). TcErrors.reportTidyWanteds does not print the errors

830 and does not fail if -fdefer-type-errors is on, so that we can continue

831 compilation. The errors are turned into warnings in `reportUnsolved`.

832 -}

835 -- Simplify the input constraints

836 -- Discard the evidence binds

837 -- Discards all Derived stuff in result

838 -- Result is /not/ guaranteed zonked

839 solveWantedsTcM wanted

844 -- Since solveWanteds returns the residual WantedConstraints,

845 -- it should always be called within a runTcS or something similar,

846 -- Result is not zonked

847 solveWantedsAndDrop wanted

852 -- so that the inert set doesn't mindlessly propagate.

853 -- NB: wc_simples may be wanted /or/ derived now

857 -- Try the simple bit, including insolubles. Solving insolubles a

858 -- second time round is a bit of a waste; but the code is simple

859 -- and the program is wrong anyway, and we don't run the danger

860 -- of adding Derived insolubles twice; see

861 -- TcSMonad Note [Do not add duplicate derived insolubles]

880 -> WantedConstraints

881 -> TcS WantedConstraints

882 simpl_loop n limit floated_eqs

884 | n `intGtLimit` limit

890 | no_floated_eqs

893 | otherwise

896 -- solveSimples may make progress if either float_eqs hold

899 -- Put floated_eqs first so they get solved first

900 -- NB: the floated_eqs may include /derived/ equalities

901 -- arising from fundeps inside an implication

905 -- solveImplications may make progress only if unifs2 holds

914 where

915 no_floated_eqs = isEmptyBag floated_eqs

917 solveNestedImplications :: Bag Implication

919 -- Precondition: the TcS inerts may contain unsolved simples which have

920 -- to be converted to givens before we go inside a nested implication.

921 solveNestedImplications implics

922 | isEmptyBag implics

924 | otherwise

929 -- ... and we are back in the original TcS inerts

930 -- Notice that the original includes the _insoluble_simples so it was safe to ignore

931 -- them in the beginning of this function.

941 -- Precondition: The TcS monad contains an empty worklist and given-only inerts

942 -- which after trying to solve this implication we must restore to their original value

951 | IC_Solved {} <- status

955 -- The insoluble stuff might be in one sub-implication

956 -- and other unsolved goals in another; and we want to

957 -- solve the latter as much as possible

961 -- Solve the nested constraints

968 -- solveWanteds, *not* solveWantedsAndDrop, because

969 -- we want to retain derived equalities so we can float

970 -- them out in floatEqualities

975 <- floatEqualities skols no_given_eqs residual_wanted

992 ----------------------

994 -- Finalise the implication returned from solveImplication:

995 -- * Set the ic_status field

996 -- * Trim the ic_wanted field to remove Derived constraints

997 -- Return Nothing if we can discard the implication altogether

1002 | some_insoluble

1008 | some_unsolved

1015 -- See Note [Tracking redundant constraints]

1019 dead_givens | warnRedundantGivens info

1023 final_needs = all_needs `delVarSetList` givens

1025 discard_entire_implication -- Can we discard the entire implication?

1036 -- We can only prune the child implications (pruned_implics)

1037 -- in the IC_Solved status case, because only then we can

1038 -- accumulate their needed evidence variales into the

1039 -- IC_Solved final_status field of the parent implication.

1042 then Nothing

1044 where

1047 some_insoluble = insolubleWC wc

1049 || isNothing mb_implic_needs

1051 pruned_simples = dropDerivedSimples simples

1052 pruned_insols = dropDerivedInsols insols

1053 pruned_implics = filterBag need_to_keep_implic implics

1056 -- Just vs => all implics are IC_Solved, with 'vs' needed

1057 -- Nothing => at least one implic is not IC_Solved

1059 Just implic_needs = mb_implic_needs

1061 add_implic implic acc

1062 | Just vs_acc <- acc

1067 need_to_keep_implic ic

1069 -- Fully solved, and no redundant givens to report

1071 -- And no children that might have things to report

1073 | otherwise

1079 FunSigCtxt _ warn_redundant -> warn_redundant

1086 -- Find all the evidence variables that are "needed",

1087 -- and then delete all those bound by the evidence bindings

1088 -- A variable is "needed" if

1089 -- a) it is free in the RHS of a Wanted EvBind (add_wanted)

1090 -- b) it is free in the RHS of an EvBind whose LHS is needed (transClo)

1091 -- c) it is in the ic_need_evs of a nested implication (initial_seeds)

1092 -- (after removing the givens)

1093 neededEvVars ev_binds initial_seeds

1094 = needed `minusVarSet` bndrs

1095 where

1096 seeds = foldEvBindMap add_wanted initial_seeds ev_binds

1097 needed = transCloVarSet also_needs seeds

1098 bndrs = foldEvBindMap add_bndr emptyVarSet ev_binds

1106 also_needs needs

1107 = foldVarSet add emptyVarSet needs

1108 where

1109 add v needs

1110 | Just ev_bind <- lookupEvBind ev_binds v

1112 , is_given

1113 = evVarsOfTerm rhs `unionVarSet` needs

1114 | otherwise

1115 = needs

1121 {-

1122 Note [Tracking redundant constraints]

1123 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

1124 With Opt_WarnRedundantConstraints, GHC can report which

1125 constraints of a type signature (or instance declaration) are

1126 redundant, and can be omitted. Here is an overview of how it

1127 works:

1129 ----- What is a redudant constraint?

1131 * The things that can be redundant are precisely the Given

1132 constraints of an implication.

1134 * A constraint can be redundant in two different ways:

1135 a) It is implied by other givens. E.g.

1136 f :: (Eq a, Ord a) => blah -- Eq a unnecessary

1137 g :: (Eq a, a~b, Eq b) => blah -- Either Eq a or Eq b unnecessary

1138 b) It is not needed by the Wanted constraints covered by the

1139 implication E.g.

1140 f :: Eq a => a -> Bool

1141 f x = True -- Equality not uesd

1143 * To find (a), when we have two Given constraints,

1144 we must be careful to drop the one that is a naked variable (if poss).

1145 So if we have

1146 f :: (Eq a, Ord a) => blah

1147 then we may find [G] sc_sel (d1::Ord a) :: Eq a

1148 [G] d2 :: Eq a

1149 We want to discard d2 in favour of the superclass selection from

1150 the Ord dictionary. This is done by TcInteract.solveOneFromTheOther

1151 See Note [Replacement vs keeping].

1153 * To find (b) we need to know which evidence bindings are 'wanted';

1154 hence the eb_is_given field on an EvBind.

1156 ----- How tracking works

1158 * When the constraint solver finishes solving all the wanteds in

1159 an implication, it sets its status to IC_Solved

1161 - The ics_dead field of IC_Solved records the subset of the ic_given

1162 of this implication that are redundant (not needed).

1164 - The ics_need field of IC_Solved then records all the

1165 in-scope (given) evidence variables, bound by the context, that

1166 were needed to solve this implication, including all its nested

1167 implications. (We remove the ic_given of this implication from

1168 the set, of course.)

1170 * We compute which evidence variables are needed by an implication

1171 in setImplicationStatus. A variable is needed if

1172 a) it is free in the RHS of a Wanted EvBind

1173 b) it is free in the RHS of an EvBind whose LHS is needed

1174 c) it is in the ics_need of a nested implication

1176 * We need to be careful not to discard an implication

1177 prematurely, even one that is fully solved, because we might

1178 thereby forget which variables it needs, and hence wrongly

1179 report a constraint as redundant. But we can discard it once

1180 its free vars have been incorporated into its parent; or if it

1181 simply has no free vars. This careful discarding is also

1182 handled in setImplicationStatus

1184 ----- Reporting redundant constraints

1186 * TcErrors does the actual warning, in warnRedundantConstraints.

1188 * We don't report redundant givens for *every* implication; only

1189 for those which reply True to TcSimplify.warnRedundantGivens:

1191 - For example, in a class declaration, the default method *can*

1192 use the class constraint, but it certainly doesn't *have* to,

1193 and we don't want to report an error there.

1195 - More subtly, in a function definition

1196 f :: (Ord a, Ord a, Ix a) => a -> a

1197 f x = rhs

1198 we do an ambiguity check on the type (which would find that one

1199 of the Ord a constraints was redundant), and then we check that

1200 the definition has that type (which might find that both are

1201 redundant). We don't want to report the same error twice, so

1202 we disable it for the ambiguity check. Hence the flag in

1203 TcType.FunSigCtxt.

1205 This decision is taken in setImplicationStatus, rather than TcErrors

1206 so that we can discard implication constraints that we don't need.

1207 So ics_dead consists only of the *reportable* redundant givens.

1209 ----- Shortcomings

1211 Consider (see Trac #9939)

1212 f2 :: (Eq a, Ord a) => a -> a -> Bool

1213 -- Ord a redundant, but Eq a is reported

1214 f2 x y = (x == y)

1216 We report (Eq a) as redundant, whereas actually (Ord a) is. But it's

1217 really not easy to detect that!

1220 Note [Cutting off simpl_loop]

1221 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

1222 It is very important not to iterate in simpl_loop unless there is a chance

1223 of progress. Trac #8474 is a classic example:

1225 * There's a deeply-nested chain of implication constraints.

1226 ?x:alpha => ?y1:beta1 => ... ?yn:betan => [W] ?x:Int

1228 * From the innermost one we get a [D] alpha ~ Int,

1229 but alpha is untouchable until we get out to the outermost one

1231 * We float [D] alpha~Int out (it is in floated_eqs), but since alpha

1232 is untouchable, the solveInteract in simpl_loop makes no progress

1234 * So there is no point in attempting to re-solve

1235 ?yn:betan => [W] ?x:Int

1236 because we'll just get the same [D] again

1238 * If we *do* re-solve, we'll get an ininite loop. It is cut off by

1239 the fixed bound of 10, but solving the next takes 10*10*...*10 (ie

1240 exponentially many) iterations!

1242 Conclusion: we should iterate simpl_loop iff we will get more 'givens'

1243 in the inert set when solving the nested implications. That is the

1244 result of prepareInertsForImplications is larger. How can we tell

1245 this?

1247 Consider floated_eqs (all wanted or derived):

1249 (a) [W/D] CTyEqCan (a ~ ty). This can give rise to a new given only by causing

1250 a unification. So we count those unifications.

1252 (b) [W] CFunEqCan (F tys ~ xi). Even though these are wanted, they

1253 are pushed in as givens by prepareInertsForImplications. See Note

1254 [Preparing inert set for implications] in TcSMonad. But because

1255 of that very fact, we won't generate another copy if we iterate

1256 simpl_loop. So we iterate if there any of these

1257 -}

1260 -- When we float a constraint out of an implication we must restore

1261 -- invariant (MetaTvInv) in Note [TcLevel and untouchable type variables] in TcType

1262 -- See Note [Promoting unification variables]

1263 promoteTyVar tclvl tv

1264 | isFloatedTouchableMetaTyVar tclvl tv

1269 | otherwise

1273 -- See Note [Promote _and_ default when inferring]

1274 promoteAndDefaultTyVar tclvl gbl_tvs tv

1277 else defaultTyVar tv

1281 -- Precondition: MetaTyVars only

1282 -- See Note [DefaultTyVar]

1283 defaultTyVar the_tv

1290 -- Why not directly derived_pred = mkTcEqPred k default_k?

1291 -- See Note [DefaultTyVar]

1292 -- We keep the same TcLevel on tv'

1297 -- Postcondition: Wanted or Derived Cts

1298 -- See Note [ApproximateWC]

1299 approximateWC wc

1300 = float_wc emptyVarSet wc

1301 where

1304 = filterBag is_floatable simples `unionBags`

1306 where

1307 is_floatable ct = tyVarsOfCt ct `disjointVarSet` new_trapping_tvs

1308 new_trapping_tvs = transCloVarSet grow trapping_tvs

1312 grow_one so_far ct tvs

1313 | ct_tvs `intersectsVarSet` so_far = tvs `unionVarSet` ct_tvs

1315 where

1316 ct_tvs = tyVarsOfCt ct

1319 float_implic trapping_tvs imp

1320 | ic_no_eqs imp -- No equalities, so float

1324 where

1325 new_trapping_tvs = trapping_tvs `extendVarSetList` ic_skols imp

1329 {-

1330 Note [ApproximateWC]

1331 ~~~~~~~~~~~~~~~~~~~~

1332 approximateWC takes a constraint, typically arising from the RHS of a

1333 let-binding whose type we are *inferring*, and extracts from it some

1334 *simple* constraints that we might plausibly abstract over. Of course

1335 the top-level simple constraints are plausible, but we also float constraints

1336 out from inside, if they are not captured by skolems.

1338 The same function is used when doing type-class defaulting (see the call

1339 to applyDefaultingRules) to extract constraints that that might be defaulted.

1341 There are two caveats:

1343 1. We do *not* float anything out if the implication binds equality

1344 constraints, because that defeats the OutsideIn story. Consider

1345 data T a where

1346 TInt :: T Int

1347 MkT :: T a

1349 f TInt = 3::Int

1351 We get the implication (a ~ Int => res ~ Int), where so far we've decided

1352 f :: T a -> res

1353 We don't want to float (res~Int) out because then we'll infer

1354 f :: T a -> Int

1355 which is only on of the possible types. (GHC 7.6 accidentally *did*

1356 float out of such implications, which meant it would happily infer

1357 non-principal types.)

1359 2. We do not float out an inner constraint that shares a type variable

1360 (transitively) with one that is trapped by a skolem. Eg

1361 forall a. F a ~ beta, Integral beta

1362 We don't want to float out (Integral beta). Doing so would be bad

1363 when defaulting, because then we'll default beta:=Integer, and that

1364 makes the error message much worse; we'd get

1365 Can't solve F a ~ Integer

1366 rather than

1367 Can't solve Integral (F a)

1369 Moreover, floating out these "contaminated" constraints doesn't help

1370 when generalising either. If we generalise over (Integral b), we still

1371 can't solve the retained implication (forall a. F a ~ b). Indeed,

1372 arguably that too would be a harder error to understand.

1374 Note [DefaultTyVar]

1375 ~~~~~~~~~~~~~~~~~~~

1376 defaultTyVar is used on any un-instantiated meta type variables to

1377 default the kind of OpenKind and ArgKind etc to *. This is important

1378 to ensure that instance declarations match. For example consider

1380 instance Show (a->b)

1381 foo x = show (\_ -> True)

1383 Then we'll get a constraint (Show (p ->q)) where p has kind ArgKind,

1384 and that won't match the typeKind (*) in the instance decl. See tests

1385 tc217 and tc175.

1387 We look only at touchable type variables. No further constraints

1388 are going to affect these type variables, so it's time to do it by

1389 hand. However we aren't ready to default them fully to () or

1390 whatever, because the type-class defaulting rules have yet to run.

1392 An important point is that if the type variable tv has kind k and the

1393 default is default_k we do not simply generate [D] (k ~ default_k) because:

1395 (1) k may be ArgKind and default_k may be * so we will fail

1397 (2) We need to rewrite all occurrences of the tv to be a type

1398 variable with the right kind and we choose to do this by rewriting

1399 the type variable /itself/ by a new variable which does have the

1400 right kind.

1402 Note [Promote _and_ default when inferring]

1403 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

1404 When we are inferring a type, we simplify the constraint, and then use

1405 approximateWC to produce a list of candidate constraints. Then we MUST

1407 a) Promote any meta-tyvars that have been floated out by

1408 approximateWC, to restore invariant (MetaTvInv) described in

1409 Note [TcLevel and untouchable type variables] in TcType.

1411 b) Default the kind of any meta-tyyvars that are not mentioned in

1412 in the environment.

1414 To see (b), suppose the constraint is (C ((a :: OpenKind) -> Int)), and we

1415 have an instance (C ((x:*) -> Int)). The instance doesn't match -- but it

1416 should! If we don't solve the constraint, we'll stupidly quantify over

1417 (C (a->Int)) and, worse, in doing so zonkQuantifiedTyVar will quantify over

1418 (b:*) instead of (a:OpenKind), which can lead to disaster; see Trac #7332.

1419 Trac #7641 is a simpler example.

1421 Note [Promoting unification variables]

1422 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

1423 When we float an equality out of an implication we must "promote" free

1424 unification variables of the equality, in order to maintain Invariant

1425 (MetaTvInv) from Note [TcLevel and untouchable type variables] in TcType. for the

1426 leftover implication.

1428 This is absolutely necessary. Consider the following example. We start

1429 with two implications and a class with a functional dependency.

1431 class C x y | x -> y

1432 instance C [a] [a]

1434 (I1) [untch=beta]forall b. 0 => F Int ~ [beta]

1435 (I2) [untch=beta]forall c. 0 => F Int ~ [[alpha]] /\ C beta [c]

1437 We float (F Int ~ [beta]) out of I1, and we float (F Int ~ [[alpha]]) out of I2.

1438 They may react to yield that (beta := [alpha]) which can then be pushed inwards

1439 the leftover of I2 to get (C [alpha] [a]) which, using the FunDep, will mean that

1440 (alpha := a). In the end we will have the skolem 'b' escaping in the untouchable

1441 beta! Concrete example is in indexed_types/should_fail/ExtraTcsUntch.hs:

1443 class C x y | x -> y where

1444 op :: x -> y -> ()

1446 instance C [a] [a]

1448 type family F a :: *

1450 h :: F Int -> ()

1451 h = undefined

1453 data TEx where

1454 TEx :: a -> TEx

1456 f (x::beta) =

1457 let g1 :: forall b. b -> ()

1458 g1 _ = h [x]

1459 g2 z = case z of TEx y -> (h [[undefined]], op x [y])

1460 in (g1 '3', g2 undefined)

1463 Note [Solving Family Equations]

1464 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

1465 After we are done with simplification we may be left with constraints of the form:

1466 [Wanted] F xis ~ beta

1467 If 'beta' is a touchable unification variable not already bound in the TyBinds

1468 then we'd like to create a binding for it, effectively "defaulting" it to be 'F xis'.

1470 When is it ok to do so?

1471 1) 'beta' must not already be defaulted to something. Example:

1473 [Wanted] F Int ~ beta <~ Will default [beta := F Int]

1474 [Wanted] F Char ~ beta <~ Already defaulted, can't default again. We

1475 have to report this as unsolved.

1477 2) However, we must still do an occurs check when defaulting (F xis ~ beta), to

1478 set [beta := F xis] only if beta is not among the free variables of xis.

1480 3) Notice that 'beta' can't be bound in ty binds already because we rewrite RHS

1481 of type family equations. See Inert Set invariants in TcInteract.

1483 This solving is now happening during zonking, see Note [Unflattening while zonking]

1484 in TcMType.

1487 *********************************************************************************

1488 * *

1489 * Floating equalities *

1490 * *

1491 *********************************************************************************

1493 Note [Float Equalities out of Implications]

1494 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

1495 For ordinary pattern matches (including existentials) we float

1496 equalities out of implications, for instance:

1497 data T where

1498 MkT :: Eq a => a -> T

1499 f x y = case x of MkT _ -> (y::Int)

1500 We get the implication constraint (x::T) (y::alpha):

1501 forall a. [untouchable=alpha] Eq a => alpha ~ Int

1502 We want to float out the equality into a scope where alpha is no

1503 longer untouchable, to solve the implication!

1505 But we cannot float equalities out of implications whose givens may

1506 yield or contain equalities:

1508 data T a where

1509 T1 :: T Int

1510 T2 :: T Bool

1511 T3 :: T a

1513 h :: T a -> a -> Int

1515 f x y = case x of

1516 T1 -> y::Int

1517 T2 -> y::Bool

1518 T3 -> h x y

1520 We generate constraint, for (x::T alpha) and (y :: beta):

1521 [untouchables = beta] (alpha ~ Int => beta ~ Int) -- From 1st branch

1522 [untouchables = beta] (alpha ~ Bool => beta ~ Bool) -- From 2nd branch

1523 (alpha ~ beta) -- From 3rd branch

1525 If we float the equality (beta ~ Int) outside of the first implication and

1526 the equality (beta ~ Bool) out of the second we get an insoluble constraint.

1527 But if we just leave them inside the implications we unify alpha := beta and

1528 solve everything.

1530 Principle:

1531 We do not want to float equalities out which may

1532 need the given *evidence* to become soluble.

1534 Consequence: classes with functional dependencies don't matter (since there is

1535 no evidence for a fundep equality), but equality superclasses do matter (since

1536 they carry evidence).

1537 -}

1540 -> WantedConstraints

1542 -- Main idea: see Note [Float Equalities out of Implications]

1543 --

1544 -- Precondition: the wc_simple of the incoming WantedConstraints are

1545 -- fully zonked, so that we can see their free variables

1546 --

1547 -- Postcondition: The returned floated constraints (Cts) are only

1548 -- Wanted or Derived and come from the input wanted

1549 -- ev vars or deriveds

1550 --

1551 -- Also performs some unifications (via promoteTyVar), adding to

1552 -- monadically-carried ty_binds. These will be used when processing

1553 -- floated_eqs later

1554 --

1555 -- Subtleties: Note [Float equalities from under a skolem binding]

1556 -- Note [Skolem escape]

1560 | otherwise

1563 -- See Note [Promoting unification variables]

1568 where

1569 skol_set = mkVarSet skols

1574 usefulToFloat is_useful_pred ct -- The constraint is un-flattened and de-canonicalised

1576 where

1579 -- Float out alpha ~ ty, or ty ~ alpha

1580 -- which might be unified outside

1581 -- See Note [Do not float kind-incompatible equalities]

1582 is_meta_var_eq pred

1585 k2 = typeKind ty2

1588 , k2 `isSubKind` k1

1591 , k1 `isSubKind` k2

1594 | otherwise

1597 {- Note [Float equalities from under a skolem binding]

1598 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

1599 Which of the simple equalities can we float out? Obviously, only

1600 ones that don't mention the skolem-bound variables. But that is

1601 over-eager. Consider

1602 [2] forall a. F a beta[1] ~ gamma[2], G beta[1] gamma[2] ~ Int

1603 The second constraint doesn't mention 'a'. But if we float it

1604 we'll promote gamma[2] to gamma'[1]. Now suppose that we learn that

1605 beta := Bool, and F a Bool = a, and G Bool _ = Int. Then we'll

1606 we left with the constraint

1607 [2] forall a. a ~ gamma'[1]

1608 which is insoluble because gamma became untouchable.

1610 Solution: float only constraints that stand a jolly good chance of

1611 being soluble simply by being floated, namely ones of form

1612 a ~ ty

1613 where 'a' is a currently-untouchable unification variable, but may

1614 become touchable by being floated (perhaps by more than one level).

1616 We had a very complicated rule previously, but this is nice and

1617 simple. (To see the notes, look at this Note in a version of

1618 TcSimplify prior to Oct 2014).

1620 Note [Do not float kind-incompatible equalities]

1621 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

1622 If we have (t::* ~ s::*->*), we'll get a Derived insoluble equality.

1623 If we float the equality outwards, we'll get *another* Derived

1624 insoluble equality one level out, so the same error will be reported

1625 twice. So we refrain from floating such equalities.

1627 Note [Skolem escape]

1628 ~~~~~~~~~~~~~~~~~~~~

1629 You might worry about skolem escape with all this floating.

1630 For example, consider

1631 [2] forall a. (a ~ F beta[2] delta,

1632 Maybe beta[2] ~ gamma[1])

1634 The (Maybe beta ~ gamma) doesn't mention 'a', so we float it, and

1635 solve with gamma := beta. But what if later delta:=Int, and

1636 F b Int = b.

1637 Then we'd get a ~ beta[2], and solve to get beta:=a, and now the

1638 skolem has escaped!

1640 But it's ok: when we float (Maybe beta[2] ~ gamma[1]), we promote beta[2]

1641 to beta[1], and that means the (a ~ beta[1]) will be stuck, as it should be.

1644 *********************************************************************************

1645 * *

1646 * Defaulting and disamgiguation *

1647 * *

1648 *********************************************************************************

1649 -}

1652 -- True <=> I did some defaulting, by unifying a meta-tyvar

1653 -- Imput WantedConstraints are not necessarily zonked

1655 applyDefaultingRules wanteds

1656 | isEmptyWC wanteds

1658 | otherwise

1675 findDefaultableGroups

1681 | null default_tys

1682 = []

1683 | otherwise

1686 , defaultable_tyvar tv

1688 where

1689 simples = approximateWC wanteds

1691 unary_groups = equivClasses cmp_tv unaries

1697 -- Finds unary type-class constraints

1698 -- But take account of polykinded classes like Typeable,

1699 -- which may look like (Typeable * (a:*)) (Trac #8931)

1700 find_unary cc

1706 -- we definitely don't want to try to assign to those!

1711 bad_tvs = mapUnionVarSet tyVarsOfCt non_unaries

1715 defaultable_tyvar tv

1720 defaultable_classes clss

1724 -- In interactive mode, or with -XExtendedDefaultRules,

1725 -- we default Show a to Show () to avoid graututious errors on "show []"

1726 isInteractiveClass cls

1730 -- is_num_class adds IsString to the standard numeric classes,

1731 -- when -foverloaded-strings is enabled

1734 -- Similarly is_std_class

1736 ------------------------------

1739 -- sharing same type variable

1742 disambigGroup [] _

1749 try_group

1752 -- Success: record the type variable binding, and return

1757 else

1758 -- Failure: try with the next type

1762 where

1763 try_group

1764 | Just subst <- mb_subst

1766 wanteds

1768 map mkNonCanonical wanted_evs

1770 | otherwise

1775 -- Make sure the kinds match too; hence this call to tcMatchTy

1776 -- E.g. suppose the only constraint was (Typeable k (a::k))

1782 {-

1783 Note [Avoiding spurious errors]

1784 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

1785 When doing the unification for defaulting, we check for skolem

1786 type variables, and simply don't default them. For example:

1787 f = (*) -- Monomorphic

1788 g :: Num a => a -> a

1789 g x = f x x

1790 Here, we get a complaint when checking the type signature for g,

1791 that g isn't polymorphic enough; but then we get another one when

1792 dealing with the (Num a) context arising from f's definition;

1793 we try to unify a with Int (to default it), but find that it's

1794 already been unified with the rigid variable from g's type sig

1795 -}