在GHC的DataKinds中，我尝试实现类型级别的二进制nat，它们实现起来很简单，但如果我希望它们在常见情况下有用，那么GHC需要相信Succ类型家族是单射的（因此类型推断至少与一元类型级别的NAT一样有效）。然而，我很难让GHC相信这是事实。考虑以下二进制nats的编码：

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE UndecidableInstances #-}
module Nat2 where

data Nat = Zero | Pos Nat1
data Nat1 = One | Bit0 Nat1 | Bit1 Nat1
  -- by separating Nat and Nat1 we avoid dealing w/ Bit0^n Zero as a spurrious representation of 0

type Succ :: Nat -> r
type family Succ n :: r | r -> n where
  Succ 'Zero = 'Pos 'One
  Succ ('Pos x) = 'Pos (Succ1 x)
  
type Succ1 :: Nat1 -> r
type family Succ1 n :: r | r -> n where
  Succ1 'One = 'Bit0 'One
  Succ1 ('Bit0 x) = 'Bit1 x
  Succ1 ('Bit1 x) = 'Bit0 (Succ1 x)

字符串
GHC不能接受这一点，因为它不能告诉Succ1是单射的：

Nat2.hs:15:3: error: [GHC-05175]
    • Type family equation right-hand sides overlap; this violates
      the family's injectivity annotation:
        Succ Zero = Pos One -- Defined at Nat2.hs:15:3
        Succ (Pos x) = Pos (Succ1 x) -- Defined at Nat2.hs:16:3
    • In the equations for closed type family ‘Succ’
      In the type family declaration for ‘Succ’
   |
15 |   Succ 'Zero = 'Pos 'One
   |   ^^^^^^^^^^^^^^^^^^^^^^

Nat2.hs:20:3: error: [GHC-05175]
    • Type family equation right-hand sides overlap; this violates
      the family's injectivity annotation:
        Succ1 One = Bit0 One -- Defined at Nat2.hs:20:3
        Succ1 (Bit1 x) = Bit0 (Succ1 x) -- Defined at Nat2.hs:22:3
    • In the equations for closed type family ‘Succ1’
      In the type family declaration for ‘Succ1’
   |
20 |   Succ1 'One = 'Bit0 'One
   |   ^^^^^^^^^^^^^^^^^^^^^^^

型

• 我们 * 认为它是单射的，因为通过检查Succ1，One永远不会在它的图像中，所以Bit0 (Succ1 x)的情况永远不会返回Bit0 One，因此Bit1的情况永远不会与One的情况冲突。（“One不在Succ1的图像中“）表明Succ本身也是内射的。然而，GHC并不太聪明，无法找到这个论点。

所以，问题是：在这种情况下（以及类似的情况），有没有办法让GHC相信一个内射类型家族实际上是内射的？（也许是一个类型检查器插件，我可以提供一个函数来反转Suc 1？也许是一个杂注，说“试着从这个家族向后推断，就好像它是内射的;如果你遇到任何歧义，你可以崩溃”？）