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)