Singletons TypeRepStar Sing数据实例

Question

我是Haskell的新手,所以我可能错过了一些明显的东西,但这里的问题似乎是什么？

该单身库提供Sing了一种例如*在import Data.Singletons.TypeRepStar.

的Sing数据系列的定义如下..

data family Sing (a :: k)

并且*实例定义为..

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

我正在尝试使用以下内容重现最小版本...

{-# 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!"

但我收到以下错误......

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

编译器坚持认为ain Bloop (a :: *)和ain Typeable a => Bloop a不一样a.如果用以下内容替换其中一个,它会产生完全相同的错误b:

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'

这可以通过以下方式更加明显-fprint-explicit-kinds:

* 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'

现在我们可以在错误消息中清楚地看到一个人a有类型k而另一个有类型*.从这一点来看,一个解决方案显而易见 - 明确声明第二种a:

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

看来这是因为PolyKinds扩展而发生的.没有它,第二个a被假定为有类型*,因此原始定义有效.