尽管已明确注释，但 Haskell 无法推断类型(或类型级别的 Nat)等式？

Question

我试图用 Haskell 实现一个 Braun 树，定义如下:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}

data BraunTree (n :: Nat) a where
    Empty :: BraunTree 0 a
    Fork :: a -> BraunTree n a -> 
            BraunTree m a ->
            Either (n :~: m) (n :~: (m + 1)) ->
            BraunTree (n + m + 1) a

现在，我正在尝试尝试如何“类型安全地”将内容插入到这棵树中。

insert :: a -> BraunTree (n :: Nat) a -> BraunTree (n + 1 :: Nat) a
insert x Empty = Fork x Empty Empty (Left Refl)
insert x (Fork y (t1 :: BraunTree p a) (t2 :: BraunTree q a) (Left (Refl :: p :~: q))) = Fork x (t1' :: BraunTree (p + 1) a) (t2 :: BraunTree q a) (Right (sucCong Refl :: (p + 1) :~: (q + 1)))
    where
        t1' :: BraunTree (p + 1) a
        t1' = insert x t1

与 sucCong作为

sucCong :: ((p :: Nat) :~: (q :: Nat)) -> (p + 1 :: Nat) :~: (q + 1 :: Nat)
sucCong Refl = Refl

现在，虽然 insert 的第一个子句编译正常，第二行抛出一个令人困惑的错误。

/home/agnishom/test/typeExp/braun.hs:31:90: error:
    • Could not deduce: (((n1 + 1) + n1) + 1) ~ (n + 1)
      from the context: n ~ ((n1 + m) + 1)
        bound by a pattern with constructor:
                   Fork :: forall a (n :: Nat) (m :: Nat).
                           a
                           -> BraunTree n a
                           -> BraunTree m a
                           -> Either (n :~: m) (n :~: (m + 1))
                           -> BraunTree ((n + m) + 1) a,
                 in an equation for ‘insert’
        at /home/agnishom/test/typeExp/braun.hs:31:11-85
      or from: m ~ n1
        bound by a pattern with constructor:
                   Refl :: forall k (a :: k). a :~: a,
                 in an equation for ‘insert’
        at /home/agnishom/test/typeExp/braun.hs:31:69-72
      Expected type: BraunTree (n + 1) a
        Actual type: BraunTree (((n1 + 1) + m) + 1) a
      NB: ‘+’ is a type function, and may not be injective
    • In the expression:
        Fork
          x
          (t1' :: BraunTree (p + 1) a)
          (t2 :: BraunTree q a)
          (Right (sucCong Refl :: (p + 1) :~: (q + 1)))
      In an equation for ‘insert’:
          insert
            x
            (Fork y
                  (t1 :: BraunTree p a)
                  (t2 :: BraunTree q a)
                  (Left (Refl :: p :~: q)))
            = Fork
                x
                (t1' :: BraunTree (p + 1) a)
                (t2 :: BraunTree q a)
                (Right (sucCong Refl :: (p + 1) :~: (q + 1)))
            where
                t1' :: BraunTree (p + 1) a
                t1' = insert x (t1 :: BraunTree p a)
    • Relevant bindings include
        t1' :: BraunTree (n1 + 1) a
          (bound at /home/agnishom/test/typeExp/braun.hs:34:9)
        t1 :: BraunTree n1 a
          (bound at /home/agnishom/test/typeExp/braun.hs:31:19)
        insert :: a -> BraunTree n a -> BraunTree (n + 1) a
          (bound at /home/agnishom/test/typeExp/braun.hs:29:1)

我不确定我在这里做错了什么。另外，为什么haskell 认为 t1 :: BraunTree n1 a (在错误消息中)，即使我已经注释了 t1 :: BraunTree p a ?

帮助解释此错误消息将非常有帮助

Answer 1

您可以尝试使用此编译器插件来推断 Nat 的类型相等性s 自动为您:

https://github.com/clash-lang/ghc-typelits-natnormalise