[GHC] #11408: Delicate solve order

[GHC]

#11408: Delicate solve order
-------------------------------------+-------------------------------------
        Reporter:  simonpj           |                Owner:
            Type:  bug               |               Status:  closed
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  7.10.3
      Resolution:  fixed             |             Keywords:
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:                    |
-------------------------------------+-------------------------------------
Changes (by simonpj):

 * status:  new => closed
 * testcase:   => indexed-types/should_compile/T11408
 * resolution:   => fixed


Old description:

> 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 is ambiguous.
>
> Eeek!  This actually shows up in type inference for `indexed-
> types/should_compile/IndTypesPerfMerge`, where 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).

New description:

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

--

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11408#comment:2>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler