1 {-# LANGUAGE CPP #-}

4 simplifyInfer,

6 simplifyAmbiguityCheck,

7 simplifyDefault,

9 solveWantedsTcM,

11 -- For Rules we need these twoo

12 solveWanteds, runTcS

17 import Bag

22 import Inst

25 import ListSetOps

27 import Name

28 import Outputable

29 import PrelInfo

30 import PrelNames

31 import TcErrors

32 import TcEvidence

33 import TcInteract

37 import TcType

43 import Util

44 import Var

45 import VarSet

48 import FastString

53 {-

54 *********************************************************************************

55 * *

56 * External interface *

57 * *

58 *********************************************************************************

59 -}

62 -- Simplify top-level constraints

63 -- Usually these will be implications,

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

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

66 simplifyTop wanteds

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

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

79 -- messges.

90 ; recordUnsafeInfer whyUnsafe

91 }

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

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

103 simpl_top wanteds

105 -- This is where the main work happens

109 where

111 try_tyvar_defaulting wc

112 | isEmptyWC wc

114 | otherwise

117 -- zonkTyVarsAndFV: the wc_first_go is not yet zonked

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

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

123 -- (defaulting returns fresh vars)

124 then try_class_defaulting wc

126 -- See Note [Must simplify after defaulting]

130 try_class_defaulting wc

131 | isEmptyWC wc

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

141 {-

142 Note [When to do type-class defaulting]

143 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

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

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

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

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

148 quite spurious because fixing the single insoluble error means that

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

150 This is jolly confusing: Trac #9033.

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

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

155 situations like this (Trac #5934):

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

157 run = fromInteger 0

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

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

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

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

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

163 stupid, but perhaps a little strange.

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

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

167 too drastic.

169 Note [Must simplify after defaulting]

170 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

171 We may have a deeply buried constraint

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

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

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

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

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

178 Note [Top-level Defaulting Plan]

179 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

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

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

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

183 This used to be the case in GHC 7.4.1.

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

185 finished. This is the current story.

187 Option (i) had many disadvantages:

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

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

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

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

192 this see Note [Default while Inferring])

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

194 f :: Int -> Bool

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

196 w a = const a (y+1)

197 in w y)

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

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

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

201 untouchable.

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

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

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

206 - Try to approximate it with a simple constraint

207 - Figure out derived defaulting equations for that simple constraint

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

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

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

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

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

214 - Apply defaulting to their kinds

216 More details in Note [DefaultTyVar].

218 Note [Safe Haskell Overlapping Instances]

219 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

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

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

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

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

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

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

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

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

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

231 overlaps instances provided by other modules.

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

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

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

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

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

239 A) from a different module than I1

240 B) Ix is not marked `OVERLAPPABLE`

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

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

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

245 type-class or type defined in N.

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

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

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

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

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

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

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

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

257 Note [Safe Haskell Overlapping Instances Implementation]

258 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

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

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

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

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

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

266 the list is null.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

284 `InertCans`.

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

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

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

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

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

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

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

293 (but unsafe) resolved dictionary constraints.

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

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

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

298 convert constraints into a warning message for the user.

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

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

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

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

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

305 we can generate a helpful error message.

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

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

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

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

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

313 IORef called `tcg_safeInfer`.

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

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

317 failed.

318 -}

320 ------------------

322 simplifyAmbiguityCheck ty wanteds

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

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

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

329 -- 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

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

607 -- flex_ctxt <- xoptM Opt_FlexibleContexts

609 where

610 pick_me flex_ctxt pred

612 ClassPred cls tys

617 -- Representational equality is like a class constraint

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

620 IrredPred ty -> tyVarsOfType ty `intersectsVarSet` qtvs

622 pick_cls_pred flex_ctxt tys

623 = tyVarsOfTypes tys `intersectsVarSet` qtvs

625 -- Only quantify over predicates that checkValidType

626 -- will pass! See Trac #10351.

628 -- See Note [Quantifying over equality constraints]

629 quant_fun ty

632 -> tyVarsOfTypes tys `intersectsVarSet` qtvs

635 ------------------

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

638 growThetaTyVars theta tvs

641 where

642 seed_tvs = tvs `unionVarSet` tyVarsOfTypes ips

644 -- See note [Inheriting implicit parameters]

648 grow_one so_far pred tvs

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

651 where

654 {-

655 Note [Quantifying over equality constraints]

656 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

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

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

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

661 However, consider this

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

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

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

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

666 the quantified variables.

668 Note [Growing the tau-tvs using constraints]

669 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

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

671 of tyvars tvs using all conceivable links from pred

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

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

676 Notice that

677 growThetaTyVars is conservative if v might be fixed by vs

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

680 Note [Inheriting implicit parameters]

681 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

682 Consider this:

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

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

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

688 There are two types we might infer for f:

690 f :: Int -> Int

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

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

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

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

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

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

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

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

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

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

705 declarations. See the pickQuantifiablePreds.

707 Note [Quantification with errors]

708 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

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

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

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

712 type we have found. For two reasons

713 a) Minimise downstream errors

714 b) Avoid spurious errors from this function

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

717 (a::*) ~ Int#

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

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

721 Note [Default while Inferring]

722 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

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

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

725 Example:

727 instance D g => C g Int b

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

730 type inferred = gamma -> gamma

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

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

734 which can then be simplified further to

735 (forall b. 0 => D gamma)

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

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

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

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

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

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

744 unsolvable implication:

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

747 The concrete example would be:

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

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

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

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

753 we don't do it for now.

757 Note [Minimize by Superclasses]

758 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

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

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

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

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

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

764 mkMinimalBySCs does. Then, simplifyInfer uses the minimal constraint

765 to check the original wanted.

768 Note [Avoid unecessary constraint simplification]

769 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

770 -------- NB NB NB (Jun 12) -------------

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

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

773 ----------------------------------------

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

775 try to avoid unnecessarily simplifying class constraints.

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

777 situations like

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

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

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

783 in ...

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

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

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

787 the constraints before simplifying.

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

792 *********************************************************************************

793 * *

794 * Main Simplifier *

795 * *

796 ***********************************************************************************

798 Note [Deferring coercion errors to runtime]

799 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

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

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

803 module Main where

805 a :: Int

806 a = 'a'

808 main = print "b"

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

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

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

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

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

816 that, `a` will get transformed into

818 co :: Int ~ Char

819 co = ...

821 a :: Int

822 a = 'a' `cast` co

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

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

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

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

828 `deferErrorsToRuntime` does.

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

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

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

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

834 -}

837 -- Simplify the input constraints

838 -- Discard the evidence binds

839 -- Discards all Derived stuff in result

840 -- Result is /not/ guaranteed zonked

841 solveWantedsTcM wanted

846 -- Since solveWanteds returns the residual WantedConstraints,

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

848 -- Result is not zonked

849 solveWantedsAndDrop wanted

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

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

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

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

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

862 -- of adding Derived insolubles twice; see

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

882 -> WantedConstraints

883 -> TcS WantedConstraints

884 simpl_loop n limit floated_eqs

886 | n `intGtLimit` limit

892 | no_floated_eqs

895 | otherwise

898 -- solveSimples may make progress if either float_eqs hold

901 -- Put floated_eqs first so they get solved first

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

903 -- arising from fundeps inside an implication

907 -- solveImplications may make progress only if unifs2 holds

916 where

917 no_floated_eqs = isEmptyBag floated_eqs

919 solveNestedImplications :: Bag Implication

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

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

923 solveNestedImplications implics

924 | isEmptyBag implics

926 | otherwise

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

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

933 -- them in the beginning of this function.

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

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

953 | IC_Solved {} <- status

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

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

959 -- solve the latter as much as possible

963 -- Solve the nested constraints

970 -- solveWanteds, *not* solveWantedsAndDrop, because

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

972 -- them out in floatEqualities

977 <- floatEqualities skols no_given_eqs residual_wanted

994 ----------------------

996 -- Finalise the implication returned from solveImplication:

997 -- * Set the ic_status field

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

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

1005 | some_insoluble

1011 | some_unsolved

1018 -- See Note [Tracking redundant constraints]

1022 dead_givens | warnRedundantGivens info

1026 final_needs = all_needs `delVarSetList` givens

1028 discard_entire_implication -- Can we discard the entire implication?

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

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

1041 -- accumulate their needed evidence variales into the

1042 -- IC_Solved final_status field of the parent implication.

1045 then Nothing

1047 where

1050 some_insoluble = insolubleWC tc_lvl wc

1052 || isNothing mb_implic_needs

1054 pruned_simples = dropDerivedSimples simples

1055 pruned_insols = dropDerivedInsols insols

1056 pruned_implics = filterBag need_to_keep_implic implics

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

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

1062 Just implic_needs = mb_implic_needs

1064 add_implic implic acc

1065 | Just vs_acc <- acc

1070 need_to_keep_implic ic

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

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

1076 | otherwise

1082 FunSigCtxt _ warn_redundant -> warn_redundant

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

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

1091 -- A variable is "needed" if

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

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

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

1095 -- (after removing the givens)

1096 neededEvVars ev_binds initial_seeds

1097 = needed `minusVarSet` bndrs

1098 where

1099 seeds = foldEvBindMap add_wanted initial_seeds ev_binds

1100 needed = transCloVarSet also_needs seeds

1101 bndrs = foldEvBindMap add_bndr emptyVarSet ev_binds

1109 also_needs needs

1110 = foldVarSet add emptyVarSet needs

1111 where

1112 add v needs

1113 | Just ev_bind <- lookupEvBind ev_binds v

1115 , is_given

1116 = evVarsOfTerm rhs `unionVarSet` needs

1117 | otherwise

1118 = needs

1124 {-

1125 Note [Tracking redundant constraints]

1126 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

1127 With Opt_WarnRedundantConstraints, GHC can report which

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

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

1130 works:

1132 ----- What is a redudant constraint?

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

1135 constraints of an implication.

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

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

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

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

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

1142 implication E.g.

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

1144 f x = True -- Equality not uesd

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

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

1148 So if we have

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

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

1151 [G] d2 :: Eq a

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

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

1154 See Note [Replacement vs keeping].

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

1157 hence the eb_is_given field on an EvBind.

1159 ----- How tracking works

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

1162 an implication, it sets its status to IC_Solved

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

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

1167 - The ics_need field of IC_Solved then records all the

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

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

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

1171 the set, of course.)

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

1174 in setImplicationStatus. A variable is needed if

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

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

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

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

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

1181 thereby forget which variables it needs, and hence wrongly

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

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

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

1185 handled in setImplicationStatus

1187 ----- Reporting redundant constraints

1189 * TcErrors does the actual warning, in warnRedundantConstraints.

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

1192 for those which reply True to TcSimplify.warnRedundantGivens:

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

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

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

1198 - More subtly, in a function definition

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

1200 f x = rhs

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

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

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

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

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

1206 TcType.FunSigCtxt.

1208 This decision is taken in setImplicationStatus, rather than TcErrors

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

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

1212 ----- Shortcomings

1214 Consider (see Trac #9939)

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

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

1217 f2 x y = (x == y)

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

1220 really not easy to detect that!

1223 Note [Cutting off simpl_loop]

1224 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

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

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

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

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

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

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

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

1235 is untouchable, the solveInteract in simpl_loop makes no progress

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

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

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

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

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

1243 exponentially many) iterations!

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

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

1247 result of prepareInertsForImplications is larger. How can we tell

1248 this?

1250 Consider floated_eqs (all wanted or derived):

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

1253 a unification. So we count those unifications.

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

1256 are pushed in as givens by prepareInertsForImplications. See Note

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

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

1259 simpl_loop. So we iterate if there any of these

1260 -}

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

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

1265 -- See Note [Promoting unification variables]

1266 promoteTyVar tclvl tv

1267 | isFloatedTouchableMetaTyVar tclvl tv

1272 | otherwise

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

1277 promoteAndDefaultTyVar tclvl gbl_tvs tv

1280 else defaultTyVar tv

1284 -- Precondition: MetaTyVars only

1285 -- See Note [DefaultTyVar]

1286 defaultTyVar the_tv

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

1294 -- See Note [DefaultTyVar]

1295 -- We keep the same TcLevel on tv'

1300 -- Postcondition: Wanted or Derived Cts

1301 -- See Note [ApproximateWC]

1302 approximateWC wc

1303 = float_wc emptyVarSet wc

1304 where

1307 = filterBag is_floatable simples `unionBags`

1309 where

1310 is_floatable ct = tyVarsOfCt ct `disjointVarSet` new_trapping_tvs

1311 new_trapping_tvs = transCloVarSet grow trapping_tvs

1315 grow_one so_far ct tvs

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

1318 where

1319 ct_tvs = tyVarsOfCt ct

1322 float_implic trapping_tvs imp

1323 | ic_no_eqs imp -- No equalities, so float

1327 where

1328 new_trapping_tvs = trapping_tvs `extendVarSetList` ic_skols imp

1332 {-

1333 Note [ApproximateWC]

1334 ~~~~~~~~~~~~~~~~~~~~

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

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

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

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

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

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

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

1344 There are two caveats:

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

1347 constraints, because that defeats the OutsideIn story. Consider

1348 data T a where

1349 TInt :: T Int

1350 MkT :: T a

1352 f TInt = 3::Int

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

1355 f :: T a -> res

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

1357 f :: T a -> Int

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

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

1360 non-principal types.)

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

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

1364 forall a. F a ~ beta, Integral beta

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

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

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

1368 Can't solve F a ~ Integer

1369 rather than

1370 Can't solve Integral (F a)

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

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

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

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

1377 Note [DefaultTyVar]

1378 ~~~~~~~~~~~~~~~~~~~

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

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

1381 to ensure that instance declarations match. For example consider

1383 instance Show (a->b)

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

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

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

1388 tc217 and tc175.

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

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

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

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

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

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

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

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

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

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

1403 right kind.

1405 Note [Promote _and_ default when inferring]

1406 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

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

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

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

1411 approximateWC, to restore invariant (MetaTvInv) described in

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

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

1415 in the environment.

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

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

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

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

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

1422 Trac #7641 is a simpler example.

1424 Note [Promoting unification variables]

1425 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

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

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

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

1429 leftover implication.

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

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

1434 class C x y | x -> y

1435 instance C [a] [a]

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

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

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

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

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

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

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

1446 class C x y | x -> y where

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

1449 instance C [a] [a]

1451 type family F a :: *

1453 h :: F Int -> ()

1454 h = undefined

1456 data TEx where

1457 TEx :: a -> TEx

1459 f (x::beta) =

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

1461 g1 _ = h [x]

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

1463 in (g1 '3', g2 undefined)

1466 Note [Solving Family Equations]

1467 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

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

1469 [Wanted] F xis ~ beta

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

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

1473 When is it ok to do so?

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

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

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

1478 have to report this as unsolved.

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

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

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

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

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

1487 in TcMType.

1490 *********************************************************************************

1491 * *

1492 * Floating equalities *

1493 * *

1494 *********************************************************************************

1496 Note [Float Equalities out of Implications]

1497 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

1498 For ordinary pattern matches (including existentials) we float

1499 equalities out of implications, for instance:

1500 data T where

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

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

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

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

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

1506 longer untouchable, to solve the implication!

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

1509 yield or contain equalities:

1511 data T a where

1512 T1 :: T Int

1513 T2 :: T Bool

1514 T3 :: T a

1516 h :: T a -> a -> Int

1518 f x y = case x of

1519 T1 -> y::Int

1520 T2 -> y::Bool

1521 T3 -> h x y

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

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

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

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

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

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

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

1531 solve everything.

1533 Principle:

1534 We do not want to float equalities out which may

1535 need the given *evidence* to become soluble.

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

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

1539 they carry evidence).

1540 -}

1543 -> WantedConstraints

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

1546 --

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

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

1549 --

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

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

1552 -- ev vars or deriveds

1553 --

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

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

1556 -- floated_eqs later

1557 --

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

1559 -- Note [Skolem escape]

1563 | otherwise

1566 -- See Note [Promoting unification variables]

1571 where

1572 skol_set = mkVarSet skols

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

1579 where

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

1583 -- which might be unified outside

1584 -- See Note [Which equalities to float]

1585 is_meta_var_eq pred

1591 | otherwise

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

1595 = isMetaTyVar tv1

1596 && typeKind ty2 `isSubKind` tyVarKind tv1

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

1600 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

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

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

1603 over-eager. Consider

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

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

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

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

1608 we left with the constraint

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

1610 which is insoluble because gamma became untouchable.

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

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

1614 a ~ ty

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

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

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

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

1620 TcSimplify prior to Oct 2014).

1622 Note [Which equalities to float]

1623 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

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

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

1626 happen. In particular:

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

1630 * alpha is a meta-tyvar

1632 * And the equality is kind-compatible

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

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

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

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

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

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

1641 of error messages.

1643 Note [Skolem escape]

1644 ~~~~~~~~~~~~~~~~~~~~

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

1646 For example, consider

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

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

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

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

1652 F b Int = b.

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

1654 skolem has escaped!

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

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

1660 *********************************************************************************

1661 * *

1662 * Defaulting and disamgiguation *

1663 * *

1664 *********************************************************************************

1665 -}

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

1669 -- Imput WantedConstraints are not necessarily zonked

1671 applyDefaultingRules wanteds

1672 | isEmptyWC wanteds

1674 | otherwise

1691 findDefaultableGroups

1697 | null default_tys

1698 = []

1699 | otherwise

1702 , defaultable_tyvar tv

1704 where

1705 simples = approximateWC wanteds

1707 unary_groups = equivClasses cmp_tv unaries

1713 -- Finds unary type-class constraints

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

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

1716 find_unary cc

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

1727 bad_tvs = mapUnionVarSet tyVarsOfCt non_unaries

1731 defaultable_tyvar tv

1736 defaultable_classes clss

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

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

1742 isInteractiveClass cls

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

1747 -- when -foverloaded-strings is enabled

1750 -- Similarly is_std_class

1752 ------------------------------

1755 -- sharing same type variable

1758 disambigGroup [] _

1765 try_group

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

1773 else

1774 -- Failure: try with the next type

1778 where

1779 try_group

1780 | Just subst <- mb_subst

1786 wanteds

1788 map mkNonCanonical wanted_evs

1790 | otherwise

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

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

1799 {-

1800 Note [Avoiding spurious errors]

1801 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

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

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

1804 f = (*) -- Monomorphic

1805 g :: Num a => a -> a

1806 g x = f x x

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

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

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

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

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

1812 -}