LiquidHaskell编码Functor恒等定律遇fmap未绑定符号错误

核心报错根源 #

你的Functor定律的逻辑思路是完全正确的，触发报错的原因是LiquidHaskell 0.8.10.2版本对自定义类型类的符号绑定规则没有被满足，具体有两个问题：

• 类型类内部声明的方法（这里是fmap）默认仅作为类定义的局部绑定存在，不会自动暴露为全局可被其他精化规则引用的顶层符号。你在fmap_id的假设精化里直接写fmap，LH无法识别这个符号的来源，才会提示“Unbound symbol”。报错里附带的“perhaps you meant: Category.Functor.LH.C:Functor”就是这个原因——LH在找不到fmap时，扫到了类型类的内部实现标识，才给出了错误的匹配建议。
• 精化谓词中的相等写法不符合LH语法：单等号=在LH中用于变量绑定，双等号==才是语义层面的相等判断。你原来写的{fmap id x = id x}会被LH解析成非法的绑定逻辑，进一步加剧了符号识别的问题。

逐点实现的修正步骤 #

按照顺序调整代码即可通过校验：

1. 保留你原来的Functor类定义与对应的类精化注解，在类定义之后，为fmap添加独立的顶层精化注解，强制LH将fmap绑定为全局可引用的符号：

   {-@ class Functor f where
         fmap :: forall a b. (a -> b) -> f a -> f b
       @-}
   class Functor f where
     fmap :: (a -> b) -> f a -> f b
   
   -- 新增：将fmap绑定为全局可引用符号
   {-@ fmap :: forall f a b. Functor f => (a -> b) -> f a -> f b @-}
   

2. 你定义的带精化的自定义id函数不存在问题，它作为顶层定义已经被正确绑定为可引用符号，不需要修改。
3. 修正fmap_id的假设精化：把原来的单等号换成双等号，明确相等语义：

   {-@ assume
       fmap_id :: forall f a. Functor f => x:f a ->
         { fmap id x == id x } @-}
   fmap_id :: Functor f => f a -> ()
   fmap_id _ = ()
   

关于无点形式的定律表述 #

等逐点实现通过校验后，你要实现基于外延性的无点定律非常简单：LH 0.8.x版本中可以通过显式assume引入函数外延性公理，将逐点相等的结论直接提升为函数层面的相等，把原精化里的逐点等式替换为fmap id == id即可完成无点表述。

注意：在引入函数外延性公理时，需要保证精化的类型层级正确——函数的相等必须作用在相同域/陪域的函数上，避免LH的排序检查报错。

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