Hi Haskelleers!
I am using Repa, and one of the things that I had was the following:
type family ArrayShape ns where
ArrayShape '[] = Z
ArrayShape (_ ': ns) = ArrayShape ns :. Int
withShapeAS :: forall r (ns :: [Nat]). Sing ns -> (Shape (ArrayShape ns) => r) -> r
withShapeAS SNil f = f
withShapeAS (SCons _ xs) f = withShapeAS xs f
I was wondering if there is a nicer way to prove constraints like Shape (ArrayShape ns)
in Haskell already, or if there is some nice syntax to avoid using weird continuations .