Failed to compile partial definition

Stream: general

[nrs]

failed to compile 'partial' definition 'MechanizingHylomorphisms.ana', could not prove that the type
  {α : Type} → {F : Container} → (fs : F.shape) → (F.positions fs → Empty) → Coalg F α → α → WType F
is nonempty.

I'm getting the above error while attempting to compile the partial function ana below. I've tried explicitly proving that the function must be inhabited by proving Nonempty and Inhabited for the function's type. Any tips?

structure Container where
  shape : Type _
  positions : shape -> Type _
deriving Inhabited

inductive ExtensionOf (F : Container) (α : Type _) : Type _
  | mk : (s : F.shape) -> (F.positions s -> α) -> ExtensionOf F α

instance {F : Container} [Inhabited F.shape] [Inhabited α] : Inhabited (ExtensionOf F α) where
  default := .mk default default

inductive WType (F : Container)
  | sup : ExtensionOf F (WType F) -> WType F

def Coalg (F : Container) (α : Type)  := α -> ExtensionOf F α

instance : Inhabited ({α : Type} -> {F : Container} -> (fs : F.shape) -> (F.positions fs -> Empty) → Coalg F α → α → WType F) where
  default := fun fs f coalg a => .sup $ .mk fs (Empty.elim ∘ f)

theorem nonEmptyAna : Nonempty ({α : Type} -> {F : Container} -> (fs : F.shape) -> (F.positions fs -> Empty) → Coalg F α → α → WType F) := Nonempty.intro (fun fs f coalg a => .sup $ .mk fs (Empty.elim ∘ f))

partial def ana {α : Type} {F : Container} (fs : F.shape) (fempty : F.positions fs -> Empty) (coalg : Coalg F α) (a :  α) : WType F := match coalg a with
  | .mk s f => .sup (.mk s fun e => ana fs fempty coalg (f e))

[Matt Diamond]

try adding instance (F : Container) : Nonempty (WType F) := sorry above the function and fill in the sorry

[Matt Diamond]

or add a [Nonempty (WType F)] assumption to your function if you want to push the problem upward

[nrs]

Matt Diamond said:

or add a [Nonempty (WType F)] assumption to your function if you want to push the problem upward

ah that worked! thank you very much!