无法匹配两个相同的类型

Question

我真的不知道如何正确解决这个问题，因为我是伊德里斯的新手，所以我会讲述我的故事。

我正在实现类型安全的

sprintf

函数，具有以下类型签名：

sprintf : (s: String) -> typeListToFunc String (corresArgs (toPrintf (unpack s)))

一大堆东西基本上在字符串中查找 printf 说明符并根据函数生成所需的参数。例如，

"%c%f%d"

会给出

Char -> Double -> Int -> String

，而

""

只会给出

String

。

虽然这个实现工作正常，但由于类型检查失败而无法通过测试。快速浏览一下：

import Specdris.Spec
import Sprintf

specSuite : IO ()
specSuite = spec $ do
  describe "Fixed tests" $ do
    it "Should accept no arg when no fmt" $ do
      sprintf "" `shouldBe` ""  -- this is line 13

特别是，Idris 无法找到

String

和

typeListToFunc String (corresArgs (toPrintf (unpack "")))

之间的匹配：

Type checking ./Sprintf.idr
Type checking ./SprintfSpec.idr
SprintfSpec.idr:10:13-24:108:
   |
10 | specSuite = spec $ do
   |             ~~~~~~~~~ ...
When checking right hand side of specSuite with expected type
        IO ()

When checking an application of function Specdris.Data.SpecResult.SpecResultDo.>>=:
        Can't find implementation for Show (typeListToFunc String (corresArgs (toPrintf (unpack ""))))

        Possible cause:
                SprintfSpec.idr:13:18-27:When checking argument expected to function Specdris.Expectations.shouldBe:
                        Type mismatch between
                                String (Type of "")
                        and
                                typeListToFunc String (corresArgs (toPrintf (unpack ""))) (Expected type)

                        Specifically:
                                Type mismatch between
                                        String
                                and
                                        typeListToFunc String (corresArgs (toPrintf []))

如上所述，它们实际上是同一类型：

$ idris Sprintf.idr
*Sprintf> typeListToFunc String (corresArgs (toPrintf (unpack "")))
String : Type

是的，我真的很困惑为什么伊德里斯不能解决这个问题。 FWIW，如果有人想查看详细信息，我已将我的源文件和测试规范放在 GitHub 上。

Answer 1

原来前人已经意识到这个问题了。

此线程中引用巴里纱：

每个数据类型和类型级别函数都必须公开导出，以便测试模块能够看到它们（测试模块到主函数也是如此），因此 %access 公共导出应该是几乎所有情况下的默认值。这让人们（阅读：我在解决 Idris kata 时）感到厌烦，因为例如 Try It Online 不需要它（代码与 Main.main 位于同一模块中）。

添加

%access public export

解决了问题。