Type.Equality与PolyKinds的结合

Question

这个编译代码是this code的一个最小化的例子，从一个语法-2.0的答案到this issue。我还使用了从sameModType中的sameNat派生出来的Data.Type.Equality的定义。

我一直在使用这个解决方案，没有问题，但我想使模数q是类多态的，其具体目标是将Proxy (nat :: Nat)变成nat :: Nat (同时仍然能够使用类*的模块)。

{-# LANGUAGE GADTs, 
             MultiParamTypeClasses, 
             FunctionalDependencies, 
             FlexibleContexts, 
             FlexibleInstances,
             TypeOperators, 
             ScopedTypeVariables,
             DataKinds,
             KindSignatures #-}

import Data.Tagged
import Data.Proxy
import Data.Type.Equality
import Data.Constraint
import Unsafe.Coerce
import GHC.TypeLits

newtype Zq q i = Zq i

data ZqType q
  where
    ZqType :: (Modulus q Int) => Proxy q -> ZqType (Zq q Int)

class (Integral i) => Modulus a i | a -> i where
    value :: Tagged a i

instance (KnownNat q) => Modulus (Proxy (q :: Nat)) Int where 
    value = Tagged $ fromIntegral $ natVal (Proxy :: Proxy q)

sameModType :: (Modulus p i, Modulus q i) 
            => Proxy p -> Proxy q -> Maybe (p :~: q)
sameModType p q | (proxy value p) == (proxy value q) = 
                     Just $ unsafeCoerce Refl
                | otherwise = Nothing

typeEqSym :: ZqType p -> ZqType q -> Maybe (Dict (p ~ q))
typeEqSym (ZqType p) (ZqType q) = do
        Refl <- sameModType p q  -- LINE 39
        return Dict              -- LINE 40

但是，当我将-XPolyKinds扩展添加到上面的代码时，我得到了几个编译错误：

Foo.hs:39:36:
    Could not deduce (k1 ~ k)
    ...
    Expected type: Proxy q0
      Actual type: Proxy q2
    Relevant bindings include
      q :: Proxy q2 (bound at Foo.hs:38:30)
      p :: Proxy q1 (bound at Foo.hs:38:19)
    In the second argument of ‘sameFactoredType’, namely ‘q’
    In a stmt of a 'do' block: Refl <- sameFactoredType p q

Foo.hs:40:16:
    Could not deduce (k ~ k1)
    ...
    Relevant bindings include
      q :: Proxy q2 (bound at Foo.hs:38:30)
      p :: Proxy q1 (bound at Foo.hs:38:19)
    In the first argument of ‘return’, namely ‘Dict’
    In a stmt of a 'do' block: return Dict
    In the expression:
      do { Refl <- sameFactoredType p q;
           return Dict }

Foo.hs:40:16:
    Could not deduce (q1 ~ q2)
    ...
    Relevant bindings include
      q :: Proxy q2 (bound at Foo.hs:38:30)
      p :: Proxy q1 (bound at Foo.hs:38:19)
    In the first argument of ‘return’, namely ‘Dict’
    In a stmt of a 'do' block: return Dict
    In the expression:
      do { Refl <- sameFactoredType p q;
           return Dict }

我对类型相等中的魔力还不太了解，不知道如何解决这个问题。看来，在执行GHC所要求的约束方面，所讨论的大多数类型都是无可救药的，但我以前从未遇到过这样的PolyKinds问题。要用PolyKinds编译代码，需要更改什么？

Answer 1

我不知道这是否是您要寻找的内容，但您可以简单地公开供以后使用的基本参数类型：

data ZqType q k where
  ZqType :: Modulus q Int => Proxy (q :: k) -> ZqType (Zq q Int) ('KProxy :: KProxy k)

typeEqSym :: ZqType p k -> ZqType q k -> Maybe (Dict (p ~ q))
typeEqSym (ZqType p) (ZqType q) = do
        Refl <- sameModType p q  
        return Dict              

instance Modulus Int Int where 
instance Modulus (n :: Nat) Int where 

KProxy应该在Data.Proxy，但它只是data KProxy (x :: *) = KProxy。

人为的例子：

>let x = ZqType (Proxy :: Proxy (10 :: Nat))
>let y = ZqType (Proxy :: Proxy Int)
>typeEqSym x y
<interactive>:25:13:
    Couldn't match kind `*' with `Nat'
    Expected type: ZqType (Zq Int Int) 'KProxy
      Actual type: ZqType (Zq Int Int) 'KProxy
    In the second argument of `typeEqSym', namely `y'
    In the expression: typeEqSym x y

Answer 2

我可以解释这个问题，但由于我不完全确定你想做什么，我不知道你如何才能最好地解决它。

问题在于ZqType的定义

data ZqType q
  where
    ZqType :: (Modulus q Int) => Proxy q -> ZqType (Zq q Int)

ZqType的类型参数称为q，这有点误导。这是一个GADT，类型参数与构造函数中出现的类型参数无关。我宁愿签个善意的字。ZqType的类型是什么？嗯，Zq q Int是一种数据类型，所以它有种类的*。您正在将ZqType应用于Zq q Int，所以ZqType的类型是* -> * (尽管有PolyKind的)。所以我们有

data ZqType :: * -> * where
  ZqType :: (Modulus q Int) => Proxy q -> ZqType (Zq q Int)

接下来，让我们看看ZqType构造函数的类型？如果没有聚类，那就是你写下的：

ZqType :: (Modulus q Int) => Proxy q -> ZqType (Zq q Int)

但是对于PolyKind，q只出现在实物多态位置，因此这变成了：

ZqType :: forall (q :: k). (Modulus q Int) => Proxy q -> ZqType (Zq q Int)

现在让我们看看如何在sameModType中使用这个

typeEqSym :: ZqType a -> ZqType b -> Maybe (Dict (a ~ b))
typeEqSym (ZqType p) (ZqType q) = do
  ...

为了避免混淆，我重命名了类型变量。所以a是一种未知类型的*，b是另一种未知类型的*。你在GADT上的模式匹配。此时，GHC了解到，a实际上是某些未知类型的k1的Zq q1 Int。此外，GHC还了解到，b实际上是某些未知类型k2的Zq q2 Int。特别是，我们在这里不知道k1和k2是一样的，因为这是没有强制执行的。

然后继续调用sameModType，它希望这两个代理都是相同类型的，从而导致第一个同类错误。其余的错误都是同一个问题的结果。