Idris中type-safe sprintf函数类型匹配失败问题求助

问题背景 #

我是Idris新手，正在实现一个类型安全的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` ""  -- 第13行

具体错误信息：

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 []))

矛盾点 #

在REPL中验证可知，这两个类型实际为同一类型：

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

源码和测试文件已上传至GitHub，寻求解决办法。

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