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 .