如何让GHC认可二进制自然数Succ类型族的内射性？

你的问题非常典型：GHC对类型族内射性的检查是语法导向、保守性的——它不会做语义层面的分析，哪怕我们能证明Succ1的输出永远不会包含One，GHC只会看到Succ1 'One = 'Bit0 'One和Succ1 ('Bit1 x) = 'Bit0 (Succ1 x)这两个等式的RHS都以'Bit0开头，就判定存在潜在重叠，拒绝内射性标注。

下面是几种可行的解决思路，按实用性排序：

1. 手动定义逆类型族 + 类型类证据模拟内射性 #

既然GHC无法自动推导内射性，我们可以手动定义Succ/Succ1的逆操作Pred/Pred1，然后通过类型类证明它们互为逆函数。这样在需要利用内射性的场景（比如Succ a ~ Succ b => a ~ b），就能通过逆函数推导类型等式。

步骤1：定义逆类型族 #

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Nat2 where

data Nat = Zero | Pos Nat1
data Nat1 = One | Bit0 Nat1 | Bit1 Nat1

-- 原Succ/Succ1定义（先去掉内射性标注让GHC通过）
type Succ :: Nat -> Nat
type family Succ n where
  Succ 'Zero = 'Pos 'One
  Succ ('Pos x) = 'Pos (Succ1 x)

type Succ1 :: Nat1 -> Nat1
type family Succ1 n where
  Succ1 'One = 'Bit0 'One
  Succ1 ('Bit0 x) = 'Bit1 x
  Succ1 ('Bit1 x) = 'Bit0 (Succ1 x)

-- 定义逆操作Pred/Pred1
type Pred :: Nat -> Nat
type family Pred n where
  Pred ('Pos 'One) = 'Zero
  Pred ('Pos x) = 'Pos (Pred1 x)

type Pred1 :: Nat1 -> Nat1
type family Pred1 n where
  Pred1 ('Bit0 'One) = 'One
  Pred1 ('Bit1 x) = 'Bit0 x
  Pred1 ('Bit0 x) = 'Bit1 (Pred1 x)

步骤2：用类型类证明逆函数关系 #

我们定义类型类来约束Succ和Pred互为逆函数，以此模拟内射性：

import Data.Type.Equality (Refl(..), (:~:))

-- 顶层Nat的逆函数证据
class SuccPredInverse (n :: Nat) where
  succPred :: Succ (Pred n) :~: n
  predSucc :: Pred (Succ n) :~: n

instance SuccPredInverse 'Zero where
  succPred = Refl
  predSucc = Refl

instance Succ1Pred1Inverse x => SuccPredInverse ('Pos x) where
  succPred = Refl
  predSucc = Refl

-- Nat1层级的逆函数证据
class Succ1Pred1Inverse (n :: Nat1) where
  succ1Pred1 :: Succ1 (Pred1 n) :~: n
  pred1Succ1 :: Pred1 (Succ1 n) :~: n

instance Succ1Pred1Inverse 'One where
  succ1Pred1 = Refl
  pred1Succ1 = Refl

instance Succ1Pred1Inverse x => Succ1Pred1Inverse ('Bit0 x) where
  succ1Pred1 = Refl
  pred1Succ1 = Refl

instance Succ1Pred1Inverse x => Succ1Pred1Inverse ('Bit1 x) where
  succ1Pred1 = Refl
  pred1Succ1 = Refl

步骤3：利用证据推导内射性 #

当你需要证明Succ a ~ Succ b => a ~ b时，可以通过逆函数推导：

succInjective :: forall a b. (SuccPredInverse a, SuccPredInverse b, Succ a ~ Succ b) => a :~: b
succInjective = case predSucc @a of
  Refl -> case predSucc @b of
    Refl -> Refl

这个函数利用Pred (Succ a) ~ a和Pred (Succ b) ~ b，结合Succ a ~ Succ b，就能推导出a ~ b。

2. 编写GHC类型检查器插件 #

如果想让GHC直接认可Succ1的内射性，你可以编写自定义GHC插件，扩展其类型检查逻辑。插件可以遍历Succ1的类型族等式，静态证明：

• 对于任意不同的Nat1输入，Succ1的输出必然不同；
• Succ1的输出永远不会是One，因此Succ1 'One和Succ1 ('Bit1 x)的RHS不会重叠。

不过这种方法门槛较高，需要熟悉GHC的插件API和内部类型检查机制，适合有一定GHC开发经验的场景。

3. 调整二进制编码方式 #

如果愿意修改你的类型级自然数编码，可以换一种让GHC更容易识别内射性的结构。比如用Z（0）、O n（偶数，对应2n）、I n（奇数，对应2n+1）的编码：

data Nat = Z | O Nat | I Nat

type Succ :: Nat -> Nat
type family Succ n where
  Succ Z = I Z
  Succ (O n) = I n
  Succ (I n) = O (Succ n)

这种编码下，Succ的每个等式RHS的构造器都是唯一的（I Z、I n、O _），GHC可以直接接受内射性标注：

type Succ :: Nat -> r
type family Succ n :: r | r -> n where
  Succ Z = I Z
  Succ (O n) = I n
  Succ (I n) = O (Succ n)

不过这需要你重构基于原编码的代码，适合新项目场景。

内容的提问来源于stack exchange，提问作者So8res