的功能未解metavariable已經沒有居住參數

我正在爲foo一個未解metavariable在下面的代碼：的功能未解metavariable已經沒有居住參數

namespace Funs 
    data Funs : Type -> Type where 
    Nil : Funs a 
    (::) : {b : Type} -> (a -> List b) -> Funs (List a) -> Funs (List a) 

    data FunPtr : Funs a -> Type -> Type where 
    here : FunPtr ((::) {b} _ bs) b 
    there : FunPtr bs b -> FunPtr (_ :: bs) b 

total foo : FunPtr [] b -> Void

如何說服伊德里斯說foo沒有有效的模式來匹配呢？

我已經嘗試添加

foo f = ?foo

，然後做一個分裂的情況下在Emacs上f（只是爲了看看會拿出什麼），但只是刪除了線，留下foo作爲一個未解元。

來源

2014-12-06 Cactus

但是不應該是'total foo：FunPtr Nil b - > Void'？ – user3237465 2014-12-06 23:26:53

@ user3237465：否，'[]'是任何稱爲'Nil'的無用構造函數的語法糖， – Cactus 2014-12-07 04:57:52

事實證明，我需要做的是列舉了foo所有可能的模式的說法，然後伊德里斯能夠一一搞清楚，他們是未unifyable與foo的類型：

foo : FunPtr [] b -> Void 
foo here impossible 
foo (there _) impossible

來源

2014-12-07 04:59:23 Cactus

的功能未解metavariable已經沒有居住參數

回答

相關問題