Forced to disambiguate when using instance method

Stream: lean4

[Bernd Losert]

I have the following code:

class Category (p : Type -> Type -> Type) where
  compose : p b c -> p a b -> p a c
  identity : p a a

export Category (compose identity)

def Function (a : Type) (b : Type) := a -> b

instance : Category Function where
  compose g f x := g (f x)
  identity x := x

def n : Nat := identity 7

When I run lean on this, I get this error:

foo.lean:13:15: error: function expected at
  identity
term has type
  ?m.121 ?m.125 ?m.125

This error was very confusing. Nevertheless, I discovered that changing the last line like this made it work:

def n : Nat := (identity : Function Nat Nat) 7

This seems pretty clumsy to me though. Is there a way to get this working without having to explicitely annotate the type of the identity function?

[Mac]

@Bernd Losert You need to inform Lean that identity is a Function in some manner as the definition of Category does not entail that.

[Bernd Losert]

OK. Coming from Agda, this seemed strange to me. Let me parametrize Category by objects and see if it does better.

[Mac]

@Bernd Losert Also note that by using a def for Function instead of an abbrev, the arrow (e.g., ->) is not a Category, only Function is.

[Bernd Losert]

Oh really? That's interesting.

[Mac]

A def defines a new type that does not share the instances of its definition, whereas an abbrev defines a type that does.

[Bernd Losert]

Good to know. So I tried this, but it still complains:

class Category (Ob : Type u) (Hom : Ob -> Ob -> Type v) where
  compose : {a : Ob} -> {b : Ob} -> {c : Ob} -> Hom b c -> Hom a b -> Hom a c
  identity : {a : Ob} -> Hom a a

export Category (compose identity)

instance : Category Type (. -> .) where
  compose g f x := g (f x)
  identity x := x

def n : Nat := identity 7

[Bernd Losert]

Disambiguating it like this

def n : Nat := (identity : Nat -> Nat) 7

does not help anymore.

[Mac]

The problem is that fun a b => a -> b is not equivalent to the arrow itself.

[Mac]

I am not sure whether it is possible to refer to the arrow directly or at very least I don't know how.

[Bernd Losert]

I see. I guess it's better then to define Category as a struct and be explicit rather than relying on a type classs.

[Reid Barton]

In mathlib it is a class but with only Ob as a parameter, and Hom as a field.

[Bernd Losert]

I tried that too. It does not help though.

[Sebastian Ullrich]

This is a higher-order unification issue, Lean gets stuck at Nat -> Nat =?= ?Hom ?a ?a. identity (Hom := (. -> .)) 7 works.

[Bernd Losert]

Yes. I was trying to make it work without having to disambiguate it.

[Bernd Losert]

It seems it is not possible.