Opened 4 years ago

Closed 4 years ago

Last modified 4 years ago

#11408 closed bug (fixed)

Delicate solve order

Reported by: simonpj Owned by:
Priority: normal Milestone: 8.0.1
Component: Compiler Version: 7.10.3
Keywords: Cc: dimitris, goldfire
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: indexed-types/should_compile/T11408
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by simonpj)

Should we successfully infer a type for f:

f x = [h x, [x]]

assuming h :: forall b. F b -> b?

Assuming (x::alpha) and we instantiate h at beta, we get the constraints

 (1)  beta ~ [alpha]		from the list [h x, [x]]
 (2)  alpha ~ F beta		from the call of h

Now if we happen to unify the constraint (1) first, beta := [alpha], then we successfully infer

f :: forall a. (a ~ F [a]) => a -> [[a]]

But if we unify the constraint (2) first, alpha := F beta, we get

f :: forall b.  (b ~ [F b]) => F b -> [[F b]]

which looks ambiguous. It isn't ambiguous, in fact, but the solver has to work hard to prove it. It actually succeeds here, but in the more complicated example in indexed-types/should_compile/IndTypesPerfMerge, it didn't. There the function merge has (a slightly more complicated form of) this delicately-balanced situation.

But see Note [Orientation of equalities with fmvs] in TcFlatten for why we don't defer solving (2).

Change History (5)

comment:1 Changed 4 years ago by Simon Peyton Jones <simonpj@…>

In 9308c736/ghc:

Fix a number of subtle solver bugs

As a result of some other unrelated changes I found that
IndTypesPerf was failing, and opened Trac #11408.  There's
a test in indexed-types/should-compile/T11408.

The bug was that a type like
 forall t. (MT (UL t) (UR t) ~ t) => UL t -> UR t -> Int
is in fact unambiguous, but it's a bit subtle to prove
that it is unambiguous.

In investigating, Dimitrios and I found several subtle
bugs in the constraint solver, fixed by this patch

* canRewrite was missing a Derived/Derived case.  This was
  lost by accident in Richard's big kind-equality patch.

* Interact.interactTyVarEq would discard [D] a ~ ty if there
  was a [W] a ~ ty in the inert set.  But that is wrong because
  the former can rewrite things that the latter cannot.
  Fix: a new function eqCanDischarge

* In TcSMonad.addInertEq, the process was outright wrong for
  a Given/Wanted in the (GWModel) case.  We were adding a new
  Derived without kicking out things that it could rewrite.
  Now the code is simpler (no special GWModel case), and works

* The special case in kickOutRewritable for [W] fsk ~ ty,
  turns out not to be needed.  (We emit a [D] fsk ~ ty which
  will do the job.

I improved comments and documentation, esp in TcSMonad.

comment:2 Changed 4 years ago by simonpj

Description: modified (diff)
Resolution: fixed
Status: newclosed
Test Case: indexed-types/should_compile/T11408

comment:3 Changed 4 years ago by simonpj

Status: closedmerge

comment:4 Changed 4 years ago by bgamari

Status: mergeclosed

This was merged to ghc-8.0 as 9f466c8841c7ddda84951c9e3470540d25d0bfdb.

comment:5 Changed 4 years ago by bgamari

Milestone: 8.0.1
Note: See TracTickets for help on using tickets.