Haskell中sop-core库NS类型模式匹配冗余分支问题求解

sop-core包中的NS类型存在一个长期被开发者讨论的穷尽匹配问题：构造器S :: NS f xs -> NS f (x ': xs)在xs ~ '[]时，S的参数理论上不存在任何合法值（类型无居民），但Haskell原生的模式匹配检查无法识别这个类型级约束，会强制要求开发者匹配该分支，否则直接抛出非穷尽匹配的编译错误。

典型的冗余匹配场景如下：

type T = NS I '[Int, String]

matchT :: T -> String
matchT = \case
  Z (I n) -> show n
  S (Z (I s)) -> s
  S (S _) -> error "FIXME" -- 该分支运行时永远不会触发

如果移除上述代码中最后一条不可达分支，编译器会直接报Pattern match(es) are non-exhaustive（模式匹配非穷尽）错误，阻断编译。

• 使用Void类型的absurd替代无意义的error兜底
  当匹配到多层S嵌套后的分支时，对应参数的类型是NS f '[]，这个类型没有任何构造器，不存在合法值。可以直接引入Data.Void中的absurd处理该分支，语义明确且不需要写无意义的错误提示字符串：

  import Data.Void (absurd)
  
  matchT :: T -> String
  matchT = \case
    Z (I n) -> show n
    S (Z (I s)) -> s
    S impossible -> absurd impossible
  

• 调用sop-core自带的NS消解组合子
  sop-core本身内置了针对NS类型的穷尽消除函数，不需要手动逐层匹配构造器。针对固定长度的类型级列表，这类组合子会在内部处理好长度证明，业务侧只需要按顺序传入对应位置的处理函数即可，完全不会出现冗余分支的问题。
• 引入类型检查插件强化穷尽判定
  可以安装适配类型级列表、sop类型的GHC类型检查插件，这类插件会在编译期识别类型级列表的长度约束，自动证明多层S嵌套后的分支不可能存在，不再要求开发者手动编写冗余的兜底分支。
• 封装专用匹配视图
  针对项目中常用的固定长度NS类型别名，可以提前封装好专用的视图匹配函数，把不可达分支的处理逻辑封装在底层，业务代码调用时只需要处理实际存在的分支即可，不需要重复写兜底逻辑。

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