type nats solver is too weak!

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

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
module Fancy where

import GHC.TypeLits 

infixr 3 :*
 
data Shape (rank :: Nat) where 
    Nil  :: Shape 0
    (:*) :: {-# UNPACK #-} !(Int :: *) -> !(Shape r) -> Shape (1 + r)

reverseShape :: Shape r -> Shape r 
reverseShape Nil = Nil 
reverseShape shs = go shs Nil 
    where
        go :: Shape a -> Shape b -> Shape (a+b)
        go Nil res = res
        go (ix :* more ) res = go more (ix :* res)