什么是类型:匹配ms = m == fromSing s？

Question

使用单例库,这个简单的函数编译和工作.但是,ghci和ghc不同意它的类型签名,如果他们的任何一个建议被粘贴到代码中,它将无法编译.

GHC接受什么类型的签名？ghc-7.10.3,单身人士-2.0.1

{-# LANGUAGE DataKinds, PolyKinds, TypeOperators, TypeFamilies, GADTs, UndecidableInstances, FlexibleContexts #-}

import Data.Proxy (KProxy(..))
import Data.Singletons
import Data.Singletons.Prelude

-- ghc rejects this type signature, but if I leave it off, ghci :t shows exactly this.
matches :: (Eq (DemoteRep 'KProxy), SingKind 'KProxy) => DemoteRep 'KProxy -> Sing a -> Bool
matches m s = m == fromSing s

t :: Sing True
t = sing

demo :: Bool
demo = matches True t

上述类型签名的GHC错误:

Couldn't match type ‘DemoteRep 'KProxy’ with ‘DemoteRep 'KProxy’
NB: ‘DemoteRep’ is a type function, and may not be injective
The kind variable ‘k2’ is ambiguous
Use -fprint-explicit-kinds to see the kind arguments
Expected type: DemoteRep 'KProxy -> Sing a -> Bool
  Actual type: DemoteRep 'KProxy -> Sing a -> Bool
In the ambiguity check for the type signature for ‘matches’:
  matches :: forall (k :: BOX)
                    (k1 :: BOX)
                    (k2 :: BOX)
                    (k3 :: BOX)
                    (a :: k3).
             (Eq (DemoteRep 'KProxy), SingKind 'KProxy) =>
             DemoteRep 'KProxy -> Sing a -> Bool
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature for ‘matches’:
  matches :: (Eq (DemoteRep KProxy), SingKind KProxy) =>
             DemoteRep KProxy -> Sing a -> Bool

ghc -Wall建议使用不同类型的签名,但BOX不会接受这些内容:

Top-level binding with no type signature:
         matches :: forall (k :: BOX) (a :: k).
                    (Eq (DemoteRep 'KProxy), SingKind 'KProxy) =>
                    DemoteRep 'KProxy -> Sing a -> Bool

Answer 1

'KProxy在类型级别就像Proxy在价值级别:它有一个幻像.正如我们在值级别上Proxy :: Proxy a使用幻像类型一样a,我们必须打开类型签名并在类型级别'KProxy :: KProxy k使用幻像类型k进行写入.希望这个比喻具有一定的意义.这是它的样子:

{-# LANGUAGE DataKinds, PolyKinds, TypeOperators, TypeFamilies, GADTs, UndecidableInstances, FlexibleContexts, KindSignatures #-}

import Data.Proxy (KProxy(..))
import Data.Singletons
import Data.Singletons.Prelude

matches ::
  ( Eq (DemoteRep ('KProxy :: KProxy k))
  , SingKind ('KProxy :: KProxy k)
  ) => DemoteRep ('KProxy :: KProxy k) -> Sing (a :: k) -> Bool
matches m s = m == fromSing s

这种类型的变量k会发生在这两个DemoteRep ...和Sing ...,这是什么让我们类型检查m == fromSing s.

GHCi虽然很甜,而且通常很聪明,但不知道类型签名需要"另一层次的间接"并且需要一个引入的类变量.

在旁边

我会注意到这里的多数意见-fprint-explicit-kinds是有帮助的:

?> :t matches
matches
  :: (Eq (DemoteRep * ('KProxy *)), SingKind * ('KProxy *)) =>
     DemoteRep * ('KProxy *) -> Sing * a -> Bool

对我来说,这并没有真正指出这里发生的事情.我只能通过查找签名的一切拼凑DemoteRep,'KProxy以及Sing与方便,花花公子:info命令.