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

7 Jan 2014


      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@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@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@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

Erik Hesselink