### Re: Associated types, kind constraints & typelits

Erik Hesselink <hesselink <at> gmail.com>

2014-01-06 17:27:17 GMT

Small additions: the 'Nat' in the original argument is the kind
argument to the class. It seems to be a bug that GHC provided this in
the error, and the latest HEAD doesn't seem to do so anymore. Also, in
the latest HEAD, I think you need to use the singletons library, as
all the singletons stuff is gone from base. My working code:
{-# LANGUAGE TypeFamilies
, DataKinds
, FlexibleContexts
, ScopedTypeVariables
#-}
module Main where
import GHC.TypeLits
import Data.Singletons
class C a where
type T a :: Nat
data D = D
instance C D where
type T D = 10
{- This is not allowed, as intended:
data E = E
instance C E where
type T E = Int
-}
-- This works:
tOfD :: D -> Integer
tOfD D = fromSing $ (sing :: Sing (T D))
tOf :: forall a. (KnownNat (T a), C a) => a -> Integer
tOf _ = fromSing $ (sing :: Sing (T a))
main :: IO ()
main = return ()
Erik
On Mon, Jan 6, 2014 at 6:15 PM, Nathan Howell <nathan.d.howell <at> gmail.com> wrote:
> This requires -XScopedTypeVariables and some constraints:
>
> tOf :: forall a . (SingI (T a), C a) => a -> Integer
> tOf _ = fromSing $ (sing :: Sing (T a))
>
>
> On Mon, Jan 6, 2014 at 9:06 AM, Nicolas Trangez <nicolas <at> incubaid.com>
> wrote:
>>
>> All,
>>
>> While toying with typelits I wanted to get the following to work, but
>> failed to. Is it intended not to work at all, should I change something
>> to get it to work, or is this something which needs some GHC support?
>>
>> Note I obviously tried to add the constraint mentioned in the compiler
>> error, but failed to: I seem to add too many type arguments to SingI,
>> which somewhat puzzles me.
>>
>> Thanks,
>>
>> Nicolas
>>
>> {-# LANGUAGE TypeFamilies,
>> DataKinds #-}
>> module Main where
>>
>> import GHC.TypeLits
>>
>> class C a where
>> type T a :: Nat
>>
>> data D = D
>> instance C D where
>> type T D = 10
>>
>> {- This is not allowed, as intended:
>>
>> data E = E
>> instance C E where
>> type T E = Int
>> -}
>>
>> -- This works:
>> tOfD :: D -> Integer
>> tOfD D = fromSing $ (sing :: Sing (T D))
>>
>> {- This doesn't work:
>> - Could not deduce (SingI Nat (T a1)) arising from a use of `sing'
>> - from the context (C a)
>>
>> tOf :: C a => a -> Integer
>> tOf _ = fromSing $ (sing :: Sing (T a))
>> -}
>>
>> main :: IO ()
>> main = return ()
>>
>> _______________________________________________
>> Haskell-Cafe mailing list
>> Haskell-Cafe <at> haskell.org
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe <at> haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>