[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     |           Version:  7.7
  checker)                           |  Operating System:  Unknown/Multiple
       Keywords:                     |   Type of failure:  GHC rejects
   Architecture:  Unknown/Multiple   |  valid program
     Difficulty:  Unknown            |         Test Case:
     Blocked By:                     |          Blocking:
Related Tickets:                     |
-------------------------------------+-------------------------------------
 I just built ghc HEAD today, and the type nat solver can't handle the
 attached program, which *should* be simple to check!  (and while I could
 use unsafeCoerce to "prove" it correct, that defeats the purpose of having
 the type nat solver!)

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