[GHC] #8422: type nats solver is too weak!

[GHC]

#8422: type nats solver is too weak!
----------------------------------------------+----------------------------
        Reporter:  carter                     |            Owner:
            Type:  bug                        |           Status:  new
        Priority:  highest                    |        Milestone:  7.8.1
       Component:  Compiler (Type checker)    |          Version:  7.7
      Resolution:                             |         Keywords:
Operating System:  Unknown/Multiple           |     Architecture:
 Type of failure:  GHC rejects valid program  |  Unknown/Multiple
       Test Case:                             |       Difficulty:  Unknown
        Blocking:                             |       Blocked By:
                                              |  Related Tickets:
----------------------------------------------+----------------------------

Comment (by carter):

 the error in question  is

 {{{

 Fancy.hs:58:35:
     Could not deduce ((r2 + (1 + b)) ~ (a + b))
     from the context (r ~ (1 + r1))
       bound by a pattern with constructor
                  :* :: forall (r :: Nat). Int -> Shape r -> Shape (1 + r),
                in an equation for ?reverseShape?
       at Fancy.hs:54:19-30
     or from (a ~ (1 + r2))
       bound by a pattern with constructor
                  :* :: forall (r :: Nat). Int -> Shape r -> Shape (1 + r),
                in an equation for ?go?
       at Fancy.hs:58:13-22
     NB: ?+? is a type function, and may not be injective
     Expected type: Shape (a + b)
       Actual type: Shape (r2 + (1 + b))
     Relevant bindings include
       res :: Shape b (bound at Fancy.hs:58:27)
       more :: Shape r2 (bound at Fancy.hs:58:19)
       go :: Shape a -> Shape b -> Shape (a + b) (bound at Fancy.hs:57:9)
     In the expression: go more (ix :* res)
     In an equation for ?go?: go (ix :* more) res = go more (ix :* res)

 }}}

 in one case , the solver should be able to deduce that 0+b = b ===>  b = r
 and in the other case that  a = a_1+1 then (a+b =r ) implies  a_1 + b +1=r

 or something like that

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