Nat aus Art Familie Aufruf in Integer

Question

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) 

nicht mit

• 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) 

Wie kann ich es beheben?

Answer 1

Es gibt zwei Probleme mit Ihrem Code. Erstens, (sing :: Sing n) hat n nicht im Anwendungsbereich. Sie benötigen explizit forall, um es in den Geltungsbereich zu bringen. Wenn Sie SingI möchten, müssen Sie dies sagen. GHC weiß nicht und überprüft nie, dass N tSingI für alle t ist, was übrigens nicht wahr ist: N Bool hat Art Nat aber es gibt keine SingI (N Bool).

Daher ist die Lösung:

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

Oder mit Typ-Anwendungen:

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