Cannot inherit constraint type class

Stream: lean4

[Denis Stoyanov]

hello everyone, I try to learn lean4 and stuck with some problem

class Base (t : Type) where
  T : Type → Type

class Recursive (t : Type) extends Base t, Functor (Base.T t) where
  project : t -> Base.T t t

class Corecursive (t : Type) extends Base t, Functor (Base.T t) where
  embed : Base.T t t -> t

open Corecursive Recursive Functor
unsafe def cata [Recursive t] (alg : Base.T t α → α) : t → α :=
  alg ∘ map (cata alg) ∘ project

unsafe def ana [Corecursive t] (coalg : α → Base.T t α) : α → t :=
  embed ∘ map (ana coalg) ∘ coalg

inductive ListF (α : Type u) (β : Type u) where
  | nilF : ListF α β
  | consF (x : α) (y : β) : ListF α β

namespace ListF

instance : Base (List α) := ⟨ListF α⟩

instance : Functor (Base.T (List α)) where
  map f
    | nilF => nilF
    | consF x y => consF x (f y)

instance : Recursive (List α) where
  project
    | [] => nilF
    | a :: b => consF a b

end ListF

can I use Functor (ListF α) instead of Functor (Base.T (List α))?

[Denis Stoyanov]

when I try this one

instance : Functor (ListF α) where
  map f
    | nilF => nilF
    | consF x y => consF x (f y)

instance : Recursive (List α) where
  project
    | [] => nilF
    | a :: b => consF a b

I got field 'map' is missing

[Alexander Bentkamp]

Instance search doesn't seem to unfold definitions. That's probably a good thing because it might get pretty slow otherwise. So I guess the answer to your question is no. Maybe it makes sense to register both instances?

instance instFunctorListF : Functor (ListF α) where
  map f
    | nilF => nilF
    | consF x y => consF x (f y)

instance : Functor (Base.T (List α)) := instFunctorListF

[Chris B]

What version are you using? On v4.0.0-m4 the example you posted doesn't throw any errors.

[Alexander Bentkamp]

Only second part of Denis's post is supposed to throw the error. I can reproduce it on leanprover/lean4:nightly-2022-04-25.

[Henrik Böving]

Alexander Bentkamp said:

Instance search doesn't seem to unfold definitions. That's probably a good thing because it might get pretty slow otherwise. So I guess the answer to your question is no. Maybe it makes sense to register both instances?

instance instFunctorListF : Functor (ListF α) where
  map f
    | nilF => nilF
    | consF x y => consF x (f y)

instance : Functor (Base.T (List α)) := instFunctorListF

You can make instance search unfold your definitions by declaring them as abbrevs (which is equivalent to tagging them with the reducible attribute)

[Chris B]

Alexander Bentkamp said:

Only second part of Denis's post is supposed to throw the error. I can reproduce it on leanprover/lean4:nightly-2022-04-25.

Yeah, the second part is fine on m4.

[Denis Stoyanov]

look like this is some duplicate of instance, I mean I need use instance : Functor (Base.T (List α)) := instFunctorListF

[Denis Stoyanov]

app:master* λ elan toolchain list
stable
leanprover/lean4:nightly
leanprover/lean4:nightly-2022-04-12 (default)

this is my version of lean

[Denis Stoyanov]

Henrik Böving said:

Alexander Bentkamp said:

Instance search doesn't seem to unfold definitions. That's probably a good thing because it might get pretty slow otherwise. So I guess the answer to your question is no. Maybe it makes sense to register both instances?

instance instFunctorListF : Functor (ListF α) where
  map f
    | nilF => nilF
    | consF x y => consF x (f y)

instance : Functor (Base.T (List α)) := instFunctorListF

You can make instance search unfold your definitions by declaring them as abbrevs (which is equivalent to tagging them with the reducible attribute)

what do u mean?

[Alexander Bentkamp]

You can make instance search unfold your definitions by declaring them as abbrevs (which is equivalent to tagging them with the reducible attribute)

For regular definitions, yes, but it seems you can't do that to Base.T, which is defined via instance : Base (List α) := ⟨ListF α⟩.

[Alexander Bentkamp]

So I think this is what Henrik means:

@[reducible]
def MyNat := Nat

example : Add MyNat := inferInstance