CODEWITHSUNDEEP
haskell
Bruno Martinez
Bruno Martinez

Reputation: 2956

Convert Nat from type family call into 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)

fails 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 it?

Upvotes: 3

Views: 403

Answers (1)

András Kovács
András Kovács

Reputation: 30103

There are two issues with your code. First, (sing :: Sing n) does not have n in scope. You need explicit forall to bring it to scope.

Second, if you want SingI, you need to say so. GHC does not know and never checks that N t is SingI for all t, which is not actually true, by the way: N Bool has kind Nat but there is no SingI (N Bool).

Hence, the solution:

foo :: forall t. SingI (N t) => t -> Integer
foo _ = fromSing (sing :: Sing (N t))

Or with type applications:

foo :: forall t. SingI (N t) => t -> Integer
foo _ = fromSing (sing @_ @(N t))

Upvotes: 3

Related Questions