Coercion is different from Lean 3

Stream: lean4

[Martin Dvořák]

Lean 4 accepts this:

example (x : List Nat) (y : List (id Nat)) :
  List Nat := x ++ ↑y

Lean 4 rejects this:

example (x : List Nat) (y : List (id Nat)) :
  List Nat := x ++ y

It was the other way around in Lean 3.

Two questions:
(1) Why?! In my uneducated opinion, Lean 3 coercion makes more sense.
(2) Can I desugar the ↑ in Lean 4 so that I can see what actually happens there?

[Kyle Miller]

You can use show_term from std4:

example (x : List Nat) (y : List (id Nat)) :
  List Nat := show_term x ++ ↑y

It reveals that it's just x ++ y. It looks like there's a no-op instance defined right after CoeT in core:

instance : CoeT α a α where coe := a

In Lean 3 I don't remember that being allowed -- a coercion meant there had to be a non-trivial coercion.

[Kyle Miller]

I think what's happening here is that the coercion arrow is causing the typeclass inference for HAppend occur without taking into account the type for y, which lets HAppend assume it can use the default homogeneous instance, and then id Nat is defeq to Nat so it's ok.

[Kyle Miller]

This also works, since it also defers taking into account the type of y when resolving HAppend: x ++ by exact y

[Martin Dvořák]

Interesting! This works:

example (x : List Nat) (y : List (id Nat)) :
  List Nat := x.append y

[Kyle Miller]

Right, id is semireducible so the types will pass the defeq check

[Martin Dvořák]

Where can I read about the semireducible stuff?

[Martin Dvořák]

In my situation, the behavior with ++ is a major inconvenience.
It isn't about id specifically; I used id only for the sake of MWE.
The project I am porting contains lots of ++ applied to lists of defeq types.
I'm wondering if I could change the behavior of ++ for my whole project, so that I could consistently use the most readable notation.

[Scott Morrison]

Could you say why you have these defeq wrappers, but still want to ++ them? It sounds at least slightly unusual. (It might be time to come clean?)

[Martin Dvořák]

I think that both wrappers and ++ make the code more readable.

[Scott Morrison]

defeq "abuse" is called that in part because it can make code less readable (because you have to guess, like in this situation, when Lean will or will not see through the wrappers).

[Martin Dvořák]

For example here:
https://github.com/madvorak/grammars/blob/4a158538f7df9ed50144d996b950821b5451165b/src/classes/unrestricted/closure_properties/concatenation.lean#L105

I believe it is better to write nst T N₁ N₂ (where nst stands for "new symbol type") than symbol T (option (N₁ ⊕ N₂) ⊕ (T ⊕ T)) when not using defeq.

[Kyle Miller]

It's fine having nst T N₁ N₂, but is there a reason why you can't be consistent with it?

[Kyle Miller]

You can also make identity functions that explicitly change the type from one thing to another defeq thing. That turns defeq abuse into a more reliable design.

[Martin Dvořák]

Kyle Miller said:

It's fine having nst T N₁ N₂, but is there a reason why you can't be consistent with it?

There are functions that don't have nst T N₁ N₂ as their output type. They might return an element of T or something in the middle and then I wrap the value before appending it to a list of the former type.

[Scott Morrison]

In a slightly similar vein, custom inductives are usually worth the extra boilerplate they cost, to avoid complicated option / ⊕ monsters.

[Martin Dvořák]

Kyle Miller said:

You can also make identity functions that explicitly change the type from one thing to another defeq thing. That turns defeq abuse into a more reliable design.

Good point but I think that defeq abuse makes the code more readable. I got used to taking advantage of defeq to the point Lean 3 allowed it.

[Kyle Miller]

Martin Dvořák said:

There are functions that don't have nst T N₁ N₂ as their output type.

Usually you then write your own wrapper around that function that has the right output type

[Kyle Miller]

(It's called defeq abuse for a reason)

[Martin Dvořák]

Scott Morrison said:

In a slightly similar vein, custom inductives are usually worth the extra boilerplate they cost, to avoid complicated option / ⊕ monsters.

In retrospect, I should have designed more custom types.

[Martin Dvořák]

Kyle Miller said:

(It's called defeq abuse for a reason)

I guess I have been spoiled by Lean 3.
Whenever I wanted defeq types to be treated as the same, Lean 3 treated them as the same types.
In some situations, certain tactics lost their power, but in the statements, defeq was always OK.
Lean 4 is not so tolerant; therefore, I am struggling.

At this point, I should probably stop talking and start working to write better code.
Yet, I am still wondering:
I think (but haven't checked) that defeq can always be mechanically checked.
Why is it the case that Lean can fail at recognizing when you have defeq types?
Isn't there a canonical representation for every type?

[Kyle Miller]

The difference here is due to HAppend being heterogeneous, and typeclass inference is up to instance defeq (reducible and instances), just like Lean 3