<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote">2014-07-04 10:00 GMT+02:00 Niklas Haas <span dir="ltr"><<a href="mailto:haskell@nand.wakku.to" target="_blank">haskell@nand.wakku.to</a>></span>:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div class="">On Fri, 4 Jul 2014 09:24:40 +0200, Gautier DI FOLCO <<a href="mailto:gautier.difolco@gmail.com">gautier.difolco@gmail.com</a>> wrote:<br>
> data Vector :: Nat -> * -> * where<br>
>     Nil ::                     Vector Z a<br>
>     El  :: a -> Vector n a  -> Vector (S n) a<br>
><br>
> lengthV :: NatToInt l => Vector l a -> Int<br>
> lengthV _ = natToInt (Proxy :: Proxy l)<br>
<br>
</div>You can do this without ScopedTypeVariables using a small helper<br>
function:<br>
<div class=""><br>
lengthV :: NatToInt l => Vector l a -> Int<br>
</div>lengthV = natToInt . (const Proxy :: Vector l' a' -> Proxy l')<br>
<br>
Note that this function is again polymorphic, hence no<br>
ScopedTypeVariables required.<br></blockquote></div><br>Interesting, thanks.<br></div></div>