具有类型级别 Bool 的 GADT - 使 (&&) 类型运算符暗示对其参数的约束

Question

总之，我试图了解如何在 GADT 的背景下告诉 ghc 这a && b ~ True应该意味着这一点a ~ True。b ~ True

给定一个数据构造函数：

data Foo :: Bool -> * where
    ...
    Bar :: Foo j -> Foo k -> Foo (j && k)
    ...

举个例子Eq (Foo True)：

instance Eq (Foo True) where
   (Bar foo11 foo12) == (Bar foo21 foo22) = foo11 == ff21 && foo12 == foo22
   ....

编译器给出以下错误：

Could not deduce: k1 ~ k
      from the context: 'True ~ (j && k)
        bound by a pattern with constructor:
                   Bar :: forall (j :: Bool) (k :: Bool).
                          Foo j -> Foo k -> Foo (j && k),
                 in an equation for `=='
        at Main.hs:12:4-14
      or from: 'True ~ (j1 && k1)
        bound by a pattern with constructor:
                   Bar :: forall (j :: Bool) (k :: Bool).
                          Foo j -> Foo k -> Foo (j && k),
                 in an equation for `=='
        at Main.hs:12:21-31
      `k1' is a rigid type variable bound by
        a pattern with constructor:
          Bar :: forall (j :: Bool) (k :: Bool).
                 Foo j -> Foo k -> Foo (j && k),
        in an equation for `=='
        at Main.hs:12:21-31
      `k' is a rigid type variable bound by
        a pattern with constructor:
          Bar :: forall (j :: Bool) (k :: Bool).
                 Foo j -> Foo k -> Foo (j && k),
        in an equation for `=='
        at Main.hs:12:4-14
      Expected type: Foo k
        Actual type: Foo k1
    * In the second argument of `(==)', namely `f22'
      In the second argument of `(&&)', namely `f12 == f22'
      In the expression: f11 == f21 && f12 == f22
    * Relevant bindings include
        f22 :: Foo k1 (bound at Main.hs:12:29)
        f12 :: Foo k (bound at Main.hs:12:12)

（以及 j 和 j1 的等效误差）

这显然是在抱怨它不知道这一点f12 :: Foo k并且f22 :: Foo k1具有相同的类型。

最近，我一直在使用 typelit-nat-normalise 来解决类似的问题（添加了 typenat），并且我搜索了一个类似的库，可以解决 bool 的这些问题 - 但无济于事。

我找到了typelevel-rewrite-rules，我认为这可能使我能够为此编写某种重写规则，但我无法计算出告诉编译器的语法：

(a && b ~ True)暗示(a ~ True) AND (b ~ True)。我相信这会解决这个问题。

Answer 1

我相信，在当前的 GHC 中，类型族的这种“反转”是不可能的，至少在没有不安全函数的情况下是不可能的。

即使有不安全的功能，我也不知道添加它是否安全。种类是一种奇怪的野兽，并且通常包含比人们想象的更多的术语。例如type family X :: Bool编译，我们仍然无法证明X ~ 'Truenor X ~ 'False。

下面的代码并没有完全回答这个问题，但我想指出的是，如果我们可以向 so 添加一些约束来Foo携带一些单例，那么我们就可以编写想要的Eq实例。

下面的代码可能可以进一步简化。不过，它就在这里。下面，我定义了“转换”函数fooT1, fooT2来让 GHC 相信Foo k，Foo j我们确实有k ~ j ~ 'True.

{-# LANGUAGE GADTs, ScopedTypeVariables, TypeApplications,
    DataKinds, TypeOperators, KindSignatures,
    FlexibleInstances, AllowAmbiguousTypes #-}
{-# OPTIONS -Wall #-}

import Data.Singletons
import Data.Singletons.Prelude.Bool

data Foo :: Bool -> * where
    Bar :: (SingI j, SingI k) =>
           Foo j -> Foo k -> Foo (j && k)

fooT1 :: forall a b. (SingI a, SingI b, (a && b) ~ 'True) 
      => Foo a -> Foo b -> Foo 'True
fooT1 f _ = case (sing @a, sing @b) of
   (STrue, STrue) -> f

fooT2 :: forall a b. (SingI a, SingI b, (a && b) ~ 'True)
      => Foo a -> Foo b -> Foo 'True
fooT2 _ f = case (sing @a, sing @b) of
   (STrue, STrue) -> f

instance Eq (Foo 'True) where
   (Bar foo11 foo12) == (Bar foo21 foo22) = 
      fooT1 foo11 foo12 == fooT1 foo21 foo22 &&
      fooT2 foo11 foo12 == fooT2 foo21 foo22

请注意，模式匹配(STrue, STrue)是详尽的，GHC 不会发出任何警告。