[Haskell-cafe] Associated types, kind constraints & typelits

[Erik Hesselink]

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
>