不能匹配两个相同的类型

问：

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

我正在实现一个类型安全的 sprintf 函数，具有以下类型签名：

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

其中，一大堆东西基本上是在字符串中寻找 printf 说明符，并在函数方面生成所需的参数。例如，would give ，并且会简单地给出 。"%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

特别是，伊德里斯找不到 和 之间的匹配项：StringtypeListToFunc 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 上。