<div dir="ltr"><span style="font-family:arial,helvetica,sans-serif">I've been playing with <span style="font-family:courier new,monospace">TypeLits</span> recently, trying to create a vector with type-fixed size. I've hit a stumbling block trying to compile this (simplified) code:<br>
</span><div><div><span style="font-family:courier new,monospace"><span style="font-family:arial,helvetica,sans-serif"><br></span>{-# LANGUAGE DataKinds #-}<br>{-# LANGUAGE KindSignatures #-}<br><br>import Control.Exception (assert)<br>
import GHC.TypeLits<br><br>data Foo (n :: Nat) a = Foo a<br><br>
size :: SingI n => Foo n a -> Int<br>size = fromInteger . fromSing . sizeSing<br>  where<br>    sizeSing :: Foo n a -> Sing n<br>    sizeSing _ = sing<br></span><span style="font-family:arial,helvetica,sans-serif"><br>
</span></div><div><span style="font-family:arial,helvetica,sans-serif">The error is:</span><br><span style="font-family:courier new,monospace">    Could not deduce (SingI Nat n1) arising from a use of `sing'<br>    from the context (SingI Nat n)<br>
      bound by the type signature for<br>                 size :: SingI Nat n => Foo n a -> Int<br>      at /home/ben/test.hs:10:9-33<br>    Possible fix: add an instance declaration for (SingI Nat n1)<br>    In the expression: sing<br>
    In an equation for `sizeSing': sizeSing _ = sing<br>    In an equation for `size':<br>        size<br>          = fromInteger . fromSing . sizeSing<br>          where<br>              sizeSing :: Foo n a -> Sing n<br>
              sizeSing _ = sing</span><br><br></div><div>Can anybody shed light on this? It seems like the kind of thing that <span style="font-family:courier new,monospace">ScopedTypeVariables</span> should solve, but it doesn't make a difference.<br>
</div></div></div>