haskell - Singletons TypeRepStar Sing 数据实例

Question

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

单例库为 import Data.Singletons.TypeRepStar 中的 * 类型提供了一个 Sing 实例。

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

编译器坚持认为 Bloop (a::*) 中的 a 和 Typeable a => Bloop 中的 a 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 被假定为具有类型 *，因此原始定义有效。