why does this recursion fail when defining an instance?

Stream: new members

[Alok Singh]

inductive Tree (a : Type) where
  | nil
  | node (val : a) (left : Tree a) (right : Tree a)
deriving Repr

-- fails with error `failed to synthesize Functor Tree` because of the `Functor.map` calls
instance : Functor Tree where
  map f t := match t with
    | Tree.nil => Tree.nil
    | Tree.node val left right => Tree.node (f val) (Functor.map f left) (Functor.map f right)

def Tree.map (f : a → b) (t : Tree a) : Tree b :=
  match t with
    | Tree.nil => Tree.nil
    | Tree.node val left right => Tree.node (f val) (Tree.map f left) (Tree.map f right)

-- works
instance : Functor Tree where
  map := Tree.map

Why can't I use Functor.map inline recursively? Similar code does work in Haskell.

[Derek Rhodes]

Hi @Alok Singh, @Mark Eastwood ran into this the other day and figured it out over on this thread

Here's a smaller example for those who may not be familiar with Functor:

inductive MyList (α : Type) where
  | Nil
  | Cons : α → MyList α → MyList α
open MyList

class Size (α : Type) where
  size : α → Nat

instance : Size (MyList Nat) where
  size l :=
    match l with
    | Nil => 0
    -- the following calls (Size.size xs), which initiates a search for an
    -- instance for type (MyList Nat), however it's currently being defined and
    -- Lean can't deal with that.
    | Cons x xs => 1 + (Size.size xs)

[Eric Wieser]

If you add let _ := instFunctorTree, then Lean will find the instance, but complain it has no way to prove the recursive call decreases (because it has no arguments to be decreasing)

[Eric Wieser]

This isn't limited to instances, it fails for the same reason as:

structure WrappedFun where f : ℕ → ℕ

def WrappedFun.fib : WrappedFun where
  f
  | 0 => 0
  | 1 => 1
  | (n + 2) => WrappedFun.fib.f (n + 1) + WrappedFun.fib.f n