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

Nathan Howell nathan.d.howell at gmail.com
Mon Jan 6 17:15:58 UTC 2014


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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20140106/6e51bc0a/attachment.html>


More information about the Haskell-Cafe mailing list