idris - Idris で依存型の printf

Question

Cayenneの例を Idris に翻訳しようとしています- 依存型paperを持つ言語 です。

これが私がこれまでに持っているものです：

PrintfType : (List Char) -> Type
PrintfType Nil                = String
PrintfType ('%' :: 'd' :: cs) = Int -> PrintfType cs
PrintfType ('%' :: 's' :: cs) = String -> PrintfType cs
PrintfType ('%' ::  _  :: cs) = PrintfType cs
PrintfType ( _  :: cs)        = PrintfType cs

printf : (fmt: List Char) -> PrintfType fmt
printf fmt = rec fmt "" where
  rec : (f: List Char) -> String -> PrintfType f
  rec Nil acc = acc
  rec ('%' :: 'd' :: cs) acc = \i => rec cs (acc ++ (show i))
  rec ('%' :: 's' :: cs) acc = \s => rec cs (acc ++ s) 
  rec ('%' ::  _  :: cs) acc = rec cs acc  -- this is line 49
  rec ( c  :: cs)        acc = rec cs (acc ++ (pack [c]))

でのパターン マッチングがすぐに複雑になったため、パターン マッチングを容易にするために、formatList Char引数の代わりにを使用しています。StringString

残念ながら、意味を理解できないエラーメッセージが表示されます。

Type checking ./sprintf.idr
sprintf.idr:49:Can't unify PrintfType (Prelude.List.:: '%' (Prelude.List.:: t cs)) with PrintfType cs

Specifically:
    Can't convert PrintfType (Prelude.List.:: '%' (Prelude.List.:: t cs)) with PrintfType cs

'%' :: ...と の 3 つの要素 ( を含むもの) を持つすべてのパターン マッチ ケースをコメント アウトするPrintfTypeとprintf、コードはコンパイルされます (ただし、明らかに興味深いことは何もしません)。

動作するようにコードを修正するにはどうすればよいprintf "the %s is %d" "answer" 42ですか?