Idris实现Profunctor Iso时类型检查报错问题求解

问题原因 #

Iso类型本质是带隐式参数和约束的多态函数：Iso a b s t = {p : Type -> Type -> Type} -> Profunctor p => p a b -> p s t，要求对所有满足Profunctor约束的p都成立。
问题出在toIso的定义逻辑上：当你直接写toIso (MkPair get set) = dimap get set时，Idris不会自动将dimap用到的Profunctor参数p泛化为全称量化的变量，而是会把它识别为一个待求解的元变量（即报错信息中的p1），导致返回的结果没有保留Iso要求的全Profunctor多态性，调用时自然无法匹配到对应约束。

解决方法 #

有两种可行的修复方案：

方案1：显式绑定隐式参数（推荐，无需修改全局配置） #

手动声明隐式参数p和对应的Profunctor约束，明确告诉Idris要保留该参数的多态性：

toIso : PairFun a b s t -> Iso a b s t
toIso (MkPair get set) {p} {auto _ : Profunctor p} = dimap get set

方案2：开启AutoImplicit扩展 #

在代码头部添加全局扩展声明，让Idris自动泛化所有未绑定的隐式参数：

%language AutoImplicit

任意一种方案修改后，测试代码都可以正常通过类型检查。

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