<div dir="ltr">natVal accepts any type witness now, not just sing. One such type in base is the polykinded Data.Proxy.Proxy, e.g. `natVal (Proxy :: Proxy 0`. For types of kind * you can use almost anything, including an empty list.</div>
<div class="gmail_extra"><br><br><div class="gmail_quote">On Mon, Jan 6, 2014 at 9:27 AM, Erik Hesselink <span dir="ltr"><<a href="mailto:hesselink@gmail.com" target="_blank">hesselink@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Small additions: the 'Nat' in the original argument is the kind<br>
argument to the class. It seems to be a bug that GHC provided this in<br>
the error, and the latest HEAD doesn't seem to do so anymore. Also, in<br>
the latest HEAD, I think you need to use the singletons library, as<br>
all the singletons stuff is gone from base. My working code:<br>
<br>
{-# LANGUAGE TypeFamilies<br>
           , DataKinds<br>
           , FlexibleContexts<br>
           , ScopedTypeVariables<br>
<div class="im">           #-}<br>
module Main where<br>
<br>
import GHC.TypeLits<br>
</div>import Data.Singletons<br>
<div class="im"><br>
class C a where<br>
    type T a :: Nat<br>
<br>
data D = D<br>
instance C D where<br>
    type T D = 10<br>
<br>
{- This is not allowed, as intended:<br>
<br>
data E = E<br>
instance C E where<br>
    type T E = Int<br>
 -}<br>
<br>
-- This works:<br>
tOfD :: D -> Integer<br>
tOfD D = fromSing $ (sing :: Sing (T D))<br>
<br>
</div>tOf :: forall a. (KnownNat (T a), C a) => a -> Integer<br>
<div class="im HOEnZb">tOf _ = fromSing $ (sing :: Sing (T a))<br>
<br>
</div><div class="im HOEnZb">main :: IO ()<br>
main = return ()<br>
<br>
</div><span class="HOEnZb"><font color="#888888">Erik<br>
</font></span><div class="HOEnZb"><div class="h5"><br>
On Mon, Jan 6, 2014 at 6:15 PM, Nathan Howell <<a href="mailto:nathan.d.howell@gmail.com">nathan.d.howell@gmail.com</a>> wrote:<br>
> This requires -XScopedTypeVariables and some constraints:<br>
><br>
> tOf :: forall a . (SingI (T a), C a) => a -> Integer<br>
> tOf _ = fromSing $ (sing :: Sing (T a))<br>
><br>
><br>
> On Mon, Jan 6, 2014 at 9:06 AM, Nicolas Trangez <<a href="mailto:nicolas@incubaid.com">nicolas@incubaid.com</a>><br>
> wrote:<br>
>><br>
>> All,<br>
>><br>
>> While toying with typelits I wanted to get the following to work, but<br>
>> failed to. Is it intended not to work at all, should I change something<br>
>> to get it to work, or is this something which needs some GHC support?<br>
>><br>
>> Note I obviously tried to add the constraint mentioned in the compiler<br>
>> error, but failed to: I seem to add too many type arguments to SingI,<br>
>> which somewhat puzzles me.<br>
>><br>
>> Thanks,<br>
>><br>
>> Nicolas<br>
>><br>
>> {-# LANGUAGE TypeFamilies,<br>
>>              DataKinds #-}<br>
>> module Main where<br>
>><br>
>> import GHC.TypeLits<br>
>><br>
>> class C a where<br>
>>     type T a :: Nat<br>
>><br>
>> data D = D<br>
>> instance C D where<br>
>>     type T D = 10<br>
>><br>
>> {- This is not allowed, as intended:<br>
>><br>
>> data E = E<br>
>> instance C E where<br>
>>     type T E = Int<br>
>>  -}<br>
>><br>
>> -- This works:<br>
>> tOfD :: D -> Integer<br>
>> tOfD D = fromSing $ (sing :: Sing (T D))<br>
>><br>
>> {- This doesn't work:<br>
>>  - Could not deduce (SingI Nat (T a1)) arising from a use of `sing'<br>
>>  -   from the context (C a)<br>
>><br>
>> tOf :: C a => a -> Integer<br>
>> tOf _ = fromSing $ (sing :: Sing (T a))<br>
>>  -}<br>
>><br>
>> main :: IO ()<br>
>> main = return ()<br>
>><br>
>> _______________________________________________<br>
>> Haskell-Cafe mailing list<br>
>> <a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
>> <a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
><br>
><br>
><br>
> _______________________________________________<br>
> Haskell-Cafe mailing list<br>
> <a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
> <a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
><br>
</div></div></blockquote></div><br></div>