Opened 4 years ago

Closed 4 years ago

# Delicate solve order

Reported by: Owned by: simonpj normal 8.0.1 Compiler 7.10.3 dimitris, goldfire Unknown/Multiple Unknown/Multiple None/Unknown indexed-types/should_compile/T11408

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).

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

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
correctly.

* 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.

### comment:2 Changed 4 years ago by simonpj

Description: modified (diff) → fixed new → closed → indexed-types/should_compile/T11408

### comment:3 Changed 4 years ago by simonpj

Status: closed → merge

### comment:4 Changed 4 years ago by bgamari

Status: merge → closed

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.