在重复的实例声明中安装agda失败

Question

我正试着给agda一个机会，但我无法安装它。我在一个阴谋沙箱里运行GHC 7.8.3。

Failed to install Agda-2.4.0.1
Build log ( /Users/jsnavely/project/agda/.cabal-sandbox/logs/Agda-2.4.0.1.log ):
[1 of 1] Compiling Main             ( /var/folders/dh/ckhr9p0j3kq3bx12176p7rlw0000gn/T/Agda-2.4.0.1-77992/Agda-2.4.0.1/dist/dist-sandbox-eeb4211c/setup/setup.hs, /var/folders/dh/ckhr9p0j3kq3bx12176p7rlw0000gn/T/Agda-2.4.0.1-77992/Agda-2.4.0.1/dist/dist-sandbox-eeb4211c/setup/Main.o )
Linking /var/folders/dh/ckhr9p0j3kq3bx12176p7rlw0000gn/T/Agda-2.4.0.1-77992/Agda-2.4.0.1/dist/dist-sandbox-eeb4211c/setup/setup ...
Configuring Agda-2.4.0.1...
Building Agda-2.4.0.1...
Preprocessing library Agda-2.4.0.1...
[  1 of 272] Compiling Agda.Utils.Maybe.Strict ( src/full/Agda/Utils/Maybe/Strict.hs, dist/dist-sandbox-eeb4211c/build/Agda/Utils/Maybe/Strict.o )
[  2 of 272] Compiling Agda.Utils.SemiRing ( src/full/Agda/Utils/SemiRing.hs, dist/dist-sandbox-eeb4211c/build/Agda/Utils/SemiRing.o )
[  3 of 272] Compiling Agda.TypeChecking.Monad.Debug ( src/full/Agda/TypeChecking/Monad/Debug.hs, dist/dist-sandbox-eeb4211c/build/Agda/TypeChecking/Monad/Debug.o )
[  4 of 272] Compiling Agda.Utils.Cluster ( src/full/Agda/Utils/Cluster.hs, dist/dist-sandbox-eeb4211c/build/Agda/Utils/Cluster.o )

src/full/Agda/Utils/Cluster.hs:50:10:
    Duplicate instance declarations:
      instance Monad m => Functor (EquivT s x y m)
        -- Defined at src/full/Agda/Utils/Cluster.hs:50:10
      instance Functor m => Functor (EquivT s c v m)
        -- Defined in ‘Data.Equivalence.Monad’
cabal: Error: some packages failed to install:
Agda-2.4.0.1 failed during the building phase. The exception was:
ExitFailure 1

我很乐意打开这个包包，但我不确定我会摆弄什么。我们能移除其中一个定义吗？

Answer 1

问题是，equivalence库(刺伤)没有为EquivT定义Functor实例，因此Agda定义了自己的实例。最新版本(0.2.4及更高版本)添加了这个缺失的实例，现在与Agda实例发生了冲突。

您基本上有两个选择:要么降级为equivalence-0.2.3，要么从Agda源文件中删除实例。我检查了，实现匹配。但是，Agda 1具有不同的约束条件(从错误消息中可以看出)：

instance Monad   m => Functor (EquivT s x y m)  -- Agda
instance Functor m => Functor (EquivT s c v m)  -- equivalence

因此，虽然可以安全地删除实例，但是有可能(虽然不太可能)存在一些类型类约束--例如，带有Monad实例但没有Functor实例的类型。

还可以考虑在官方窃听器上报告这个问题。据我所知，它还没有被报道。

Answer 2

这个问题在Agda的git(集线器)版本中得到了解决。修补程序将在2.4.0.2中发布。