Неразрешимая метапеременная для функции, у которой нет обитаемых аргументов

Я получаю нерешенную метапеременную для foo в приведенном ниже коде:

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 как нерешенную мета.


idris
person Cactus    schedule 06.12.2014    source источник
comment
Но разве это не должно быть total foo : FunPtr Nil b -> Void?   -  person user3237465    schedule 07.12.2014
comment
@ user3237465: нет, [] — это синтаксический сахар для любого нулевого конструктора с именем Nil   -  person Cactus    schedule 07.12.2014

Ответы (1)


arrow_upward
1
arrow_downward

Оказывается, все, что мне нужно сделать, это перечислить все возможные шаблоны для аргумента foo, а затем Идрис сможет выяснить, один за другим, что они не унифицируемы с типом foo:

foo : FunPtr [] b -> Void
foo here impossible
foo (there _) impossible
person Cactus    schedule 07.12.2014