How to introduce proven constraints in a nicer fashion?

Learn
#1

Hi Haskelleers! :slight_smile:

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 :smile:.