如何解决Idris中“Error: Multiple solutions found”错误？

错误原因分析 #

你的代码里，Set a的两个构造器（Nil和(::)）都声明了Eq a约束，同时contains函数的类型签名也包含Eq a约束。当处理contains x (y :: s)的右侧表达式时，Idris检测到两个可用的Eq a实例：

• 一个来自(::)构造器携带的隐式Eq a参数
• 另一个来自contains函数自身的Eq a约束

由于无法确定使用哪一个实例，因此抛出"Multiple solutions found in search of: Eq a"的歧义错误。

解决方案 #

方案1：将Eq a约束绑定到Set类型本身（推荐）

把Eq a作为Set类型的隐式参数，让整个Set a类型共享同一个Eq a实例，避免重复约束导致的歧义：

mutual
  data Set : (a : Type) -> {auto eq : Eq a} -> Type where
    Nil : Set a
    (::) : (x : a) -> (s : Set a) -> {auto _ : contains x s = False} -> Set a

  contains : (x : a) -> (s : Set a) -> Bool
  contains x [] = False
  contains x (y :: s) = (x == y) || contains x s

说明：

• Set类型现在依赖于隐式的Eq a证据，所有构造器和操作函数都会共享这个实例
• contains函数无需额外声明Eq a约束，因为可以从Set a自动获取对应的隐式证据

方案2：显式指定使用的Eq a实例

如果不想修改Set类型的定义，可以在contains的模式匹配中显式指定使用构造器的Eq a实例：

mutual
  data Set : Type -> Type where
    Nil : Eq a => Set a
    (::) : Eq a => (x : a) -> (s : Set a) -> {auto _ : contains x s = False} -> Set a

  contains : {eq : Eq a} -> a -> Set a -> Bool
  contains x [] = False
  contains x (y :: s) = let %instance = eq in (x == y) || contains x s

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