On Fri, 4 Jul 2014 09:24:40 +0200, Gautier DI FOLCO <gautier.difolco@gmail.com> wrote:
> data Vector :: Nat -> * -> * where
>     Nil ::                     Vector Z a
>     El  :: a -> Vector n a  -> Vector (S n) a
>
> lengthV :: NatToInt l => Vector l a -> Int
> lengthV _ = natToInt (Proxy :: Proxy l)

You can do this without ScopedTypeVariables using a small helper
function:

lengthV :: NatToInt l => Vector l a -> Int

lengthV = natToInt . (const Proxy :: Vector l' a' -> Proxy l')

Note that this function is again polymorphic, hence no
ScopedTypeVariables required.