Неожиданный corecursive вызов

Question

Это (обрезанное) определение corecursive функции в Изабель

primcorec tree :: "'form fset ⇒ 'vertex ⇒ 'preform ⇒ (('form fset × 'form), ('rule × 'preform) NatRule) dtree" where
 "tree Γ v p =
    (case undefined of Hyp h c ⇒ undefined | Reg c ⇒
    Node undefined (fimage (tree Γ v) undefined)
    )"

доходность

Unexpected corecursive call in "case undefined of Reg c ⇒ Node undefined (tree Γ v |`| undefined)" at
  "case case undefined of Reg c ⇒ Node undefined (tree Γ v |`| undefined) of Node uu uua ⇒ uua"

но если я упросту это дальше

primcorec tree :: "'form fset ⇒ 'vertex ⇒ 'preform ⇒ (('form fset × 'form), ('rule × 'preform) NatRule) dtree" where
   "tree Γ v p =
      (Node undefined (fimage (tree Γ v) undefined))"

оно работает.

Я также пытался использовать вид деконструктора, т.е.

primcorec tree :: "'form fset ⇒ 'vertex ⇒ 'preform ⇒ (('form fset × 'form), ('rule × 'preform) NatRule) dtree" where
 "cont (tree Γ v p) = (case undefined of Hyp h c ⇒ undefined | Reg c ⇒ (fimage (tree Γ v) undefined))"

И теперь я получаю другое сообщение об ошибке: Invalid map function at "case undefined of Reg c ⇒ tree Γ v |`| undefined",

В чем может быть причина?

С другим case Выражения это работает, и я не нахожу упоминания об ограничении в документации (§ 5.1.1 в документации по типу данных).

Answer 1

Через личное сообщение мне сказали, что решение состоит в том, чтобы добавить (discs_sel) вариант к datatype где Hyp конструктор приходит из.