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

340 ------------------

342 simplifyInteractive wanteds

344 simplifyTop wanteds

346 ------------------

349 simplifyDefault theta

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

356 ; reportAllUnsolved unsolved

361 {-

362 *********************************************************************************

363 * *

364 * Inference

365 * *

366 ***********************************************************************************

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

369 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

370 Consider

371 f x = rhs

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

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

375 the current one. This is done by the call

376 pushLevelAndCaptureConstraints (tcMonoBinds...)

377 in TcBinds.tcPolyInfer

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

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

381 here called rhs_tclvl.

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

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

385 the let binding.

386 -}

391 -- see Note [Which type variables to quantify]

393 -- and their tau-types

394 -> WantedConstraints

398 simplifyInfer rhs_tclvl apply_mr sig_qtvs 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 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!

531 {-

532 ************************************************************************

533 * *

534 Quantification

535 * *

536 ************************************************************************

538 Note [Deciding quantification]

539 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

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

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

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

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

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

545 the environment too

546 These are the mono_tvs

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

549 using all the constraints. These are tau_tvs_plus

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

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

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

554 Result is qtvs.

556 * Filter the constraints using pickQuantifyablePreds and the qtvs.

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

558 created skolems.

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

561 and the quantified constraints are empty.

562 -}

564 decideQuantification

571 -- See Note [Deciding quantification]

572 decideQuantification apply_mr sig_qtvs name_taus 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

582 -- Warn about the monomorphism restriction

592 | otherwise

595 tau_tvs_plus = growThetaTyVars constraints zonked_tau_tvs

598 -- quantifyTyVars turned some meta tyvars into

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

608 where

611 quantify_tvs mono_tvs tau_tvs -- See Note [Which type variable to quantify]

616 ------------------

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

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

622 pickQuantifiablePreds qtvs theta

624 -- -XFlexibleContexts: see Trac #10608, #10351

625 -- flex_ctxt <- xoptM Opt_FlexibleContexts

627 where

628 pick_me flex_ctxt pred

630 ClassPred cls tys

635 -- Representational equality is like a class constraint

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

638 IrredPred ty -> tyVarsOfType ty `intersectsVarSet` qtvs

640 pick_cls_pred flex_ctxt tys

641 = tyVarsOfTypes tys `intersectsVarSet` qtvs

643 -- Only quantify over predicates that checkValidType

644 -- will pass! See Trac #10351.

646 -- See Note [Quantifying over equality constraints]

647 quant_fun ty

650 -> tyVarsOfTypes tys `intersectsVarSet` qtvs

653 ------------------

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

656 growThetaTyVars theta tvs

659 where

660 seed_tvs = tvs `unionVarSet` tyVarsOfTypes ips

662 -- See note [Inheriting implicit parameters]

666 grow_one so_far pred tvs

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

669 where

672 {- Note [Which type variables to quantify]

673 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

674 When choosing type variables to quantify, the basic plan is to

675 quantify over all type variables that are

676 * free in the tau_tvs, and

677 * not forced to be monomorphic (mono_tvs),

678 for example by being free in the environment

680 However, for a pattern binding, or with wildards, we might

681 be doing inference *in the presence of a type signature*.

682 Mostly, if there is a signature we use CheckGen, not InferGen,

683 but with pattern bindings or wildcards we might do inference

684 and still have a type signature. For example:

685 f :: _ -> a

686 f x = ...

687 or

688 p :: a -> a

689 (p,q) = e

690 In both cases we use plan InferGen, and hence call simplifyInfer.

691 But those 'a' variables are skolems, and we should be sure to quantify

692 over them, regardless of the monomorphism restriction etc. If we

693 don't, when reporting a type error we panic when we find that a

694 skolem isn't bound by any enclosing implication.

696 That's why we pass sig_qtvs to simplifyInfer, and make sure (in

697 quantify_tvs) that we do quantify over them. Trac #10615 is

698 a case in point.

700 Note [Quantifying over equality constraints]

701 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

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

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

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

706 However, consider this

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

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

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

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

711 the quantified variables.

713 Note [Growing the tau-tvs using constraints]

714 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

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

716 of tyvars tvs using all conceivable links from pred

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

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

721 Notice that

722 growThetaTyVars is conservative if v might be fixed by vs

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

725 Note [Inheriting implicit parameters]

726 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

727 Consider this:

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

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

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

733 There are two types we might infer for f:

735 f :: Int -> Int

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

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

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

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

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

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

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

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

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

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

750 declarations. See the pickQuantifiablePreds.

752 Note [Quantification with errors]

753 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

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

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

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

757 type we have found. For two reasons

758 a) Minimise downstream errors

759 b) Avoid spurious errors from this function

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

762 (a::*) ~ Int#

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

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

766 Note [Default while Inferring]

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

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

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

770 Example:

772 instance D g => C g Int b

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

775 type inferred = gamma -> gamma

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

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

779 which can then be simplified further to

780 (forall b. 0 => D gamma)

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

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

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

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

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

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

789 unsolvable implication:

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

792 The concrete example would be:

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

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

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

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

798 we don't do it for now.

802 Note [Minimize by Superclasses]

803 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

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

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

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

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

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

809 mkMinimalBySCs does. Then, simplifyInfer uses the minimal constraint

810 to check the original wanted.

813 Note [Avoid unecessary constraint simplification]

814 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

815 -------- NB NB NB (Jun 12) -------------

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

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

818 ----------------------------------------

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

820 try to avoid unnecessarily simplifying class constraints.

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

822 situations like

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

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

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

828 in ...

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

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

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

832 the constraints before simplifying.

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

837 *********************************************************************************

838 * *

839 * Main Simplifier *

840 * *

841 ***********************************************************************************

843 Note [Deferring coercion errors to runtime]

844 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

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

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

848 module Main where

850 a :: Int

851 a = 'a'

853 main = print "b"

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

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

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

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

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

861 that, `a` will get transformed into

863 co :: Int ~ Char

864 co = ...

866 a :: Int

867 a = 'a' `cast` co

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

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

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

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

873 `deferErrorsToRuntime` does.

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

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

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

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

879 -}

882 -- Simplify the input constraints

883 -- Discard the evidence binds

884 -- Discards all Derived stuff in result

885 -- Result is /not/ guaranteed zonked

886 solveWantedsTcM wanted

891 -- Since solveWanteds returns the residual WantedConstraints,

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

893 -- Result is not zonked

894 solveWantedsAndDrop wanted

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

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

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

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

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

907 -- of adding Derived insolubles twice; see

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

927 -> WantedConstraints

928 -> TcS WantedConstraints

929 simpl_loop n limit floated_eqs

931 | n `intGtLimit` limit

937 | no_floated_eqs

940 | otherwise

943 -- solveSimples may make progress if either float_eqs hold

946 -- Put floated_eqs first so they get solved first

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

948 -- arising from fundeps inside an implication

952 -- solveImplications may make progress only if unifs2 holds

961 where

962 no_floated_eqs = isEmptyBag floated_eqs

964 solveNestedImplications :: Bag Implication

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

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

968 solveNestedImplications implics

969 | isEmptyBag implics

971 | otherwise

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

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

978 -- them in the beginning of this function.

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

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

998 | IC_Solved {} <- status

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

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

1004 -- solve the latter as much as possible

1008 -- Solve the nested constraints

1015 -- solveWanteds, *not* solveWantedsAndDrop, because

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

1017 -- them out in floatEqualities

1022 <- floatEqualities skols no_given_eqs residual_wanted

1039 ----------------------

1041 -- Finalise the implication returned from solveImplication:

1042 -- * Set the ic_status field

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

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

1050 | some_insoluble

1056 | some_unsolved

1063 -- See Note [Tracking redundant constraints]

1067 dead_givens | warnRedundantGivens info

1071 final_needs = all_needs `delVarSetList` givens

1073 discard_entire_implication -- Can we discard the entire implication?

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

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

1086 -- accumulate their needed evidence variales into the

1087 -- IC_Solved final_status field of the parent implication.

1090 then Nothing

1092 where

1095 some_insoluble = insolubleWC tc_lvl wc

1097 || isNothing mb_implic_needs

1099 pruned_simples = dropDerivedSimples simples

1100 pruned_insols = dropDerivedInsols insols

1101 pruned_implics = filterBag need_to_keep_implic implics

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

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

1107 Just implic_needs = mb_implic_needs

1109 add_implic implic acc

1110 | Just vs_acc <- acc

1115 need_to_keep_implic ic

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

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

1121 | otherwise

1127 FunSigCtxt _ warn_redundant -> warn_redundant

1130 -- To think about: do we want to report redundant givens for

1131 -- pattern synonyms, PatSynCtxt? c.f Trac #9953, comment:21.

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

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

1139 -- A variable is "needed" if

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

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

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

1143 -- (after removing the givens)

1144 neededEvVars ev_binds initial_seeds

1145 = needed `minusVarSet` bndrs

1146 where

1147 seeds = foldEvBindMap add_wanted initial_seeds ev_binds

1148 needed = transCloVarSet also_needs seeds

1149 bndrs = foldEvBindMap add_bndr emptyVarSet ev_binds

1157 also_needs needs

1158 = foldVarSet add emptyVarSet needs

1159 where

1160 add v needs

1161 | Just ev_bind <- lookupEvBind ev_binds v

1163 , is_given

1164 = evVarsOfTerm rhs `unionVarSet` needs

1165 | otherwise

1166 = needs

1172 {-

1173 Note [Tracking redundant constraints]

1174 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

1175 With Opt_WarnRedundantConstraints, GHC can report which

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

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

1178 works:

1180 ----- What is a redudant constraint?

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

1183 constraints of an implication.

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

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

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

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

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

1190 implication E.g.

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

1192 f x = True -- Equality not uesd

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

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

1196 So if we have

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

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

1199 [G] d2 :: Eq a

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

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

1202 See Note [Replacement vs keeping].

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

1205 hence the eb_is_given field on an EvBind.

1207 ----- How tracking works

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

1210 an implication, it sets its status to IC_Solved

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

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

1215 - The ics_need field of IC_Solved then records all the

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

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

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

1219 the set, of course.)

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

1222 in setImplicationStatus. A variable is needed if

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

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

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

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

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

1229 thereby forget which variables it needs, and hence wrongly

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

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

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

1233 handled in setImplicationStatus

1235 ----- Reporting redundant constraints

1237 * TcErrors does the actual warning, in warnRedundantConstraints.

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

1240 for those which reply True to TcSimplify.warnRedundantGivens:

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

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

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

1246 - More subtly, in a function definition

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

1248 f x = rhs

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

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

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

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

1253 disable it for the ambiguity check. Hence using two different

1254 FunSigCtxts, one with the warn-redundant field set True, and the

1255 other set False in

1256 - TcBinds.tcSpecPrag

1257 - TcBinds.tcTySig

1259 This decision is taken in setImplicationStatus, rather than TcErrors

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

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

1263 ----- Shortcomings

1265 Consider (see Trac #9939)

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

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

1268 f2 x y = (x == y)

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

1271 really not easy to detect that!

1274 Note [Cutting off simpl_loop]

1275 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

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

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

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

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

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

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

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

1286 is untouchable, the solveInteract in simpl_loop makes no progress

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

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

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

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

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

1294 exponentially many) iterations!

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

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

1298 result of prepareInertsForImplications is larger. How can we tell

1299 this?

1301 Consider floated_eqs (all wanted or derived):

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

1304 a unification. So we count those unifications.

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

1307 are pushed in as givens by prepareInertsForImplications. See Note

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

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

1310 simpl_loop. So we iterate if there any of these

1311 -}

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

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

1316 -- See Note [Promoting unification variables]

1317 promoteTyVar tclvl tv

1318 | isFloatedTouchableMetaTyVar tclvl tv

1323 | otherwise

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

1328 promoteAndDefaultTyVar tclvl gbl_tvs tv

1331 else defaultTyVar tv

1335 -- Precondition: MetaTyVars only

1336 -- See Note [DefaultTyVar]

1337 defaultTyVar the_tv

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

1345 -- See Note [DefaultTyVar]

1346 -- We keep the same TcLevel on tv'

1351 -- Postcondition: Wanted or Derived Cts

1352 -- See Note [ApproximateWC]

1353 approximateWC wc

1354 = float_wc emptyVarSet wc

1355 where

1358 = filterBag is_floatable simples `unionBags`

1360 where

1361 is_floatable ct = tyVarsOfCt ct `disjointVarSet` new_trapping_tvs

1362 new_trapping_tvs = transCloVarSet grow trapping_tvs

1366 grow_one so_far ct tvs

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

1369 where

1370 ct_tvs = tyVarsOfCt ct

1373 float_implic trapping_tvs imp

1374 | ic_no_eqs imp -- No equalities, so float

1378 where

1379 new_trapping_tvs = trapping_tvs `extendVarSetList` ic_skols imp

1383 {-

1384 Note [ApproximateWC]

1385 ~~~~~~~~~~~~~~~~~~~~

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

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

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

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

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

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

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

1395 There are two caveats:

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

1398 constraints, because that defeats the OutsideIn story. Consider

1399 data T a where

1400 TInt :: T Int

1401 MkT :: T a

1403 f TInt = 3::Int

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

1406 f :: T a -> res

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

1408 f :: T a -> Int

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

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

1411 non-principal types.)

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

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

1415 forall a. F a ~ beta, Integral beta

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

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

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

1419 Can't solve F a ~ Integer

1420 rather than

1421 Can't solve Integral (F a)

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

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

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

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

1428 Note [DefaultTyVar]

1429 ~~~~~~~~~~~~~~~~~~~

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

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

1432 to ensure that instance declarations match. For example consider

1434 instance Show (a->b)

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

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

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

1439 tc217 and tc175.

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

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

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

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

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

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

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

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

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

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

1454 right kind.

1456 Note [Promote _and_ default when inferring]

1457 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

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

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

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

1462 approximateWC, to restore invariant (MetaTvInv) described in

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

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

1466 in the environment.

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

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

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

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

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

1473 Trac #7641 is a simpler example.

1475 Note [Promoting unification variables]

1476 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

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

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

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

1480 leftover implication.

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

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

1485 class C x y | x -> y

1486 instance C [a] [a]

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

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

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

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

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

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

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

1497 class C x y | x -> y where

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

1500 instance C [a] [a]

1502 type family F a :: *

1504 h :: F Int -> ()

1505 h = undefined

1507 data TEx where

1508 TEx :: a -> TEx

1510 f (x::beta) =

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

1512 g1 _ = h [x]

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

1514 in (g1 '3', g2 undefined)

1517 Note [Solving Family Equations]

1518 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

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

1520 [Wanted] F xis ~ beta

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

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

1524 When is it ok to do so?

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

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

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

1529 have to report this as unsolved.

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

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

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

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

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

1538 in TcMType.

1541 *********************************************************************************

1542 * *

1543 * Floating equalities *

1544 * *

1545 *********************************************************************************

1547 Note [Float Equalities out of Implications]

1548 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

1549 For ordinary pattern matches (including existentials) we float

1550 equalities out of implications, for instance:

1551 data T where

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

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

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

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

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

1557 longer untouchable, to solve the implication!

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

1560 yield or contain equalities:

1562 data T a where

1563 T1 :: T Int

1564 T2 :: T Bool

1565 T3 :: T a

1567 h :: T a -> a -> Int

1569 f x y = case x of

1570 T1 -> y::Int

1571 T2 -> y::Bool

1572 T3 -> h x y

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

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

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

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

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

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

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

1582 solve everything.

1584 Principle:

1585 We do not want to float equalities out which may

1586 need the given *evidence* to become soluble.

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

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

1590 they carry evidence).

1591 -}

1594 -> WantedConstraints

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

1597 --

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

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

1600 --

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

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

1603 -- ev vars or deriveds

1604 --

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

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

1607 -- floated_eqs later

1608 --

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

1610 -- Note [Skolem escape]

1614 | otherwise

1617 -- See Note [Promoting unification variables]

1622 where

1623 skol_set = mkVarSet skols

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

1630 where

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

1634 -- which might be unified outside

1635 -- See Note [Which equalities to float]

1636 is_meta_var_eq pred

1642 | otherwise

1645 float_tv_eq tv1 ty2 -- See Note [Which equalities to float]

1646 = isMetaTyVar tv1

1647 && typeKind ty2 `isSubKind` tyVarKind tv1

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

1651 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

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

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

1654 over-eager. Consider

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

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

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

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

1659 we left with the constraint

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

1661 which is insoluble because gamma became untouchable.

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

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

1665 a ~ ty

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

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

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

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

1671 TcSimplify prior to Oct 2014).

1673 Note [Which equalities to float]

1674 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

1675 Which equalities should we float? We want to float ones where there

1676 is a decent chance that floating outwards will allow unification to

1677 happen. In particular:

1679 Float out equalities of form (alpaha ~ ty) or (ty ~ alpha), where

1681 * alpha is a meta-tyvar

1683 * And the equality is kind-compatible

1685 e.g. Consider (alpha:*) ~ (s:*->*)

1686 From this we already get a Derived insoluble equality. If we

1687 floated it, we'll get *another* Derived insoluble equality one

1688 level out, so the same error will be reported twice.

1690 * And 'alpha' is not a SigTv with 'ty' being a non-tyvar. In that

1691 case, floating out won't help either, and it may affect grouping

1692 of error messages.

1694 Note [Skolem escape]

1695 ~~~~~~~~~~~~~~~~~~~~

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

1697 For example, consider

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

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

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

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

1703 F b Int = b.

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

1705 skolem has escaped!

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

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

1711 *********************************************************************************

1712 * *

1713 * Defaulting and disamgiguation *

1714 * *

1715 *********************************************************************************

1716 -}

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

1720 -- Imput WantedConstraints are not necessarily zonked

1722 applyDefaultingRules wanteds

1723 | isEmptyWC wanteds

1725 | otherwise

1742 findDefaultableGroups

1748 | null default_tys

1749 = []

1750 | otherwise

1753 , defaultable_tyvar tv

1755 where

1756 simples = approximateWC wanteds

1758 unary_groups = equivClasses cmp_tv unaries

1764 -- Finds unary type-class constraints

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

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

1767 find_unary cc

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

1778 bad_tvs = mapUnionVarSet tyVarsOfCt non_unaries

1782 defaultable_tyvar tv

1787 defaultable_classes clss

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

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

1793 isInteractiveClass cls

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

1798 -- when -foverloaded-strings is enabled

1801 -- Similarly is_std_class

1803 ------------------------------

1806 -- sharing same type variable

1809 disambigGroup [] _

1816 try_group

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

1824 else

1825 -- Failure: try with the next type

1829 where

1830 try_group

1831 | Just subst <- mb_subst

1837 wanteds

1839 map mkNonCanonical wanted_evs

1841 | otherwise

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

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

1850 {-

1851 Note [Avoiding spurious errors]

1852 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

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

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

1855 f = (*) -- Monomorphic

1856 g :: Num a => a -> a

1857 g x = f x x

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

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

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

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

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

1863 -}