Singletons TypRepStar Sing Data Instanz

Question

Ich bin neu in Haskell, also vermisse ich wahrscheinlich etwas Offensichtliches, aber was scheint hier das Problem zu sein?

Die Singleton-Bibliothek bietet eine Instanz für die Art * in import Data.Singletons.TypeRepStar.

Die Sing Daten Familie ist wie folgt definiert ..

data family Sing (a :: k) 

und die * Instanz ist wie folgt definiert ..

data instance Sing (a :: *) where 
    STypeRep :: Typeable a => Sing a 

Ich versuche, eine Minimalversion von dieser mit der zu reproduzieren folgende ...

{-# LANGUAGE GADTs 
      , TypeFamilies 
      , PolyKinds 
      #-} 

module Main where 

import Data.Typeable 

data family Bloop (a :: k) 
data instance Bloop (a :: *) where 
    Blop :: Typeable a => Bloop a 

main :: IO() 
main = putStrLn "Hello, Haskell!" 

Aber ich bekomme die f Fehler ach ...

Main.hs:12:3: error: 
    • Data constructor ‘Blop’ returns type ‘Bloop a’ 
     instead of an instance of its parent type ‘Bloop a’ 
    • In the definition of data constructor ‘Blop’ 
     In the data instance declaration for ‘Bloop’ 
    | 
12 | Blop :: Typeable a => Bloop a 
    | ^

Answer 1

Der Compiler besteht darauf, dass die a in Bloop (a :: *) und die a in Typeable a => Bloop a sind nicht die gleichen a. Es erzeugt genau den gleichen Fehler, wenn Sie mit b eine von ihnen ersetzen:

data instance Bloop (b :: *) where 
     Blop :: Typeable a => Bloop a 

* Data constructor `Blop' returns type `Bloop a' 
    instead of an instance of its parent type `Bloop b' 
* In the definition of data constructor `Blop' 
    In the data instance declaration for `Bloop' 

Die mit -fprint-explicit-kinds mehr sichtbar gemacht werden kann:

* Data constructor `Blop' returns type `Bloop k a' 
    instead of an instance of its parent type `Bloop * a' 
* In the definition of data constructor `Blop' 
    In the data instance declaration for `Bloop' 

Jetzt können wir deutlich sehen, rechts in der Fehlermeldung, dass eine a hat Art k und die andere hat Art *. Daraus ist eine Lösung auf der Hand - ausdrücklich die Art der zweiten a erklären:

data instance Bloop (a :: *) where 
     Blop :: Typeable (a :: *) => Bloop (a :: *) -- Works now 

Es scheint, dass dies wegen der PolyKinds Erweiterung geschieht. Ohne es wird angenommen, dass die zweite a die Art * hat und somit die ursprüngliche Definition funktioniert.

Answer 2

Es scheint, als ob die PolyKinds Erweiterung den Fehler verursacht. Die Singleton-Bibliothek teilt die data family Deklaration und die data instance Definitionen in verschiedene Dateien auf. Die Datenfamilie benötigt die PolyKinds-Erweiterung, um zu funktionieren, aber wenn die Instanz fehlschlägt, wenn die Erweiterung aktiviert ist. Anscheinend müssen Sie stattdessen die KindSignatures-Erweiterung verwenden.

Def.hs

{-# LANGUAGE PolyKinds, TypeFamilies #-} 

module Def (Bloop) where 

data family Bloop (a :: k) 

Main.hs

{-# LANGUAGE GADTs 
      , TypeFamilies 
      , KindSignatures 
      #-} 

module Main where 

import Def 
import Data.Typeable 

data instance Bloop (a :: *) where 
    Blop :: Typeable a => Bloop a 

main :: IO() 
main = putStrLn "Hello, Haskell!"