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

[GHC]

#8422: type nats solver is too weak!
----------------------------------------------+----------------------------
        Reporter:  carter                     |            Owner:
            Type:  bug                        |           Status:  new
        Priority:  normal                     |        Milestone:  7.10.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:
----------------------------------------------+----------------------------
Changes (by thoughtpolice):

 * cc: diatchki (added)
 * priority:  highest => normal
 * milestone:  7.8.1 => 7.10.1


Comment:

 This shouldn't be highest priority.

 The example is the status report isn't literal. The solver works as
 expected if you give it terms to think about, but perhaps it should be
 reworded. If you have a problem with something this simple, we need an
 example.

 But the core problem with your example is that the solver doesn't
 recognize that `+` is associative, as Richard pointed out in #8423 (but
 you can get around this with a manual proof term defined inductively. at
 least.) For example, I believe `plus_succ` here should typecheck without
 issue.

 In any case, this probably won't be solved in the 7.8 timeframe, but I've
 added Iavor to the ticket in case he wants to correct me or clarify
 something.

 {{{#!haskell
 {-# LANGUAGE DataKinds, TypeOperators #-}
 module Main where
 import GHC.TypeLits
 import Data.Proxy
 import Data.Type.Equality

 witness1 :: Proxy x -> Proxy (x+2)
 witness1 _ = Proxy

 -- This typechecks
 ex1 :: Proxy 5
 ex1 = witness1 (Proxy :: Proxy 3)

 -- This does not
 --ex2 :: Proxy 5
 --ex2 = witness1 (Proxy :: Proxy 4)

 --------------------------------------------------------------------------------

 -- Proof of zero identity
 plus_id :: Proxy n -> (n+0 :~: n)
 plus_id _ = Refl

 -- Proof of associativity
 --
 -- This doesn't typecheck
 --plus_succ :: Proxy n1 -> Proxy n2 -> (n1+(n2+1) :~: (n1+n2)+1)
 --plus_succ _ _ = Refl
 }}}

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