为什么移除Haskell模式同义词的空约束会引发编译错误？

首先明确GHC中模式同义词类型签名的标准格式规则：

pattern 模式名 :: Required约束 => Provided约束 => 类型

• Required约束：使用该模式（不管是构造值还是匹配模式）时，使用者必须提前满足的约束
• Provided约束：当模式匹配成功后，当前分支可以自动获得的额外约束

两种写法的核心差异 #

第一种（可正常编译的版本） #

pattern CEv :: () => (n ~ Zero) => Comp (Vec n) g a

这里的两组约束分工明确：

• Required约束是空的()：匹配该模式不需要提前满足任何约束
• Provided约束是n ~ Zero：只要成功匹配上CEv，就能在当前分支得到n ~ Zero的类型相等证明

对于函数t的参数Comp (Vec m) (Vec n) r，匹配CEv时不需要提前证明m ~ Zero，匹配成功后自然得到m ~ Zero的约束，因此编译完全合法。

第二种（删除空约束后的报错版本） #

pattern CEv :: (n ~ Zero) => Comp (Vec n) g a

当你只写一组约束时，GHC会默认将其识别为Required约束，Provided约束自动留空，等价于：

pattern CEv :: (n ~ Zero) => () => Comp (Vec n) g a

这意味着：你要使用CEv模式（包括做模式匹配），必须**提前证明n ~ Zero**才能使用。但函数t的签名是forall m n r. Comp (Vec m) (Vec n) r -> Bool，这里的m是全称量化的刚性类型变量，没有任何前提保证m ~ Zero，因此编译器找不到对应的类型相等证明，直接抛出匹配错误。

补充说明 #

如果想要省略空的Required约束但保留Provided约束，必须明确写出第一组空约束占位，这是GHC用来区分两种约束作用域的强制语法要求，没有简写方案。

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