Convert Nat from invoking type family to Integer
import Data.Singletons
import Data.Singletons.TypeLits
type family N t :: Nat where
N Int = 42
N String = 9
foo :: (n ~ N t) => t -> Integer
foo _ = fromSing (sing :: Sing n)
doesn't work with
• Could not deduce: DemoteRep * ~ Integer
from the context: n ~ N t
bound by the type signature for:
foo :: n ~ N t => t -> Integer
at mini.hs:16:1-32
• In the expression: fromSing (sing :: Sing n)
In an equation for ‘foo’: foo _ = fromSing (sing :: Sing n)
How can I fix this?
source to share
There are two problems with the code. First, (sing :: Sing n)
it has no n
scope. To bring it into scope, you need to explicitly forall
.
Second, if you want SingI
, you need to say it. The GHC does not know and never checks what N t
is SingI
for everyone t
, what is actually wrong, by the way: it N Bool
has a form Nat
, but not SingI (N Bool)
.
Hence the solution:
foo :: forall t. SingI (N t) => t -> Integer
foo _ = fromSing (sing :: Sing (N t))
Or with the type of applications:
foo :: forall t. SingI (N t) => t -> Integer
foo _ = fromSing (sing @_ @(N t))
source to share