[GHC] #11070: Type-level arithmetic of sized-types has weaker inference power than in 7.8

[GHC]

#11070: Type-level arithmetic of sized-types has weaker inference power than in 7.8
-------------------------------------+-------------------------------------
        Reporter:  cactus            |                Owner:
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  7.10.2
      Resolution:                    |             Keywords:  TypeFamilies
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 I confirm this behavior.

 I'd love a second opinion, but I think this sort of trickery lies at the
 edge of what the solver can handle. Specifically, here is my analysis:

 1. We're typechecking the body of `bar`, `[((), B)] &* foo`, at type
 `[(((), ()), B X2)]`

 2. The type of `(&*)` tells us that `[((), B)]` has type `[(a, B n)]` for
 some `a` and `n`. Thus, `a` is `()`.

 3. Similarly, we know that `foo` must have type `[(b, B n')]`. Thus, `b`
 is `()` and `n'` is `X1`, where that last fact comes from the signature on
 `foo`.

 4. We must show that `ADD n' n` is `X2` (from `bar`'s signature).
 Rewriting, this is
 {{{
    [W] c1 :: ADD X1 n ~ X2
 }}}
     where `n` is a unification variable.

 5. The type of `(&*)` also gives us
 {{{
    [W] c2 :: n ~ SUB (ADD X1 n) X1
    [W] c3 :: X1 ~ SUB (ADD X1 n) n
 }}}

 Now, here I think I see why GHC 7.8 and GHC 7.10 differ. 7.8 could rewrite
 wanteds with wanteds. That is, it could use `c2` or `c3` to try to solve
 `c1`. But 7.10 doesn't do this, because rewriting wanteds with wanteds
 gives terrible error messages sometimes. (To be fair, I don't actually see
 how this works out, after some effort. But I trust it does.)

 Is this a use case for rewriting wanteds with wanteds? Perhaps. But it
 also seems to require a non-terminating rewrite system, where `n` is
 rewritten with something involving `n`. I'm surprised that happened in
 either GHC version.

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