a question on elaboration order

Stream: lean4

[Kenny Lau]

I can get rid of the mathlib dependency later, but consider this:

import Mathlib

axiom Foo {ι A σ : Type*} [SetLike σ A] (𝒜 : ι → σ) (f : A) : Prop

variable (R A : Type*) [Field R] [Field A] [Algebra R A] (𝒜 : ℕ → Submodule R A) (f : 𝒜 67)

#check Foo 𝒜 f -- failed to synthesize SetLike (Submodule R A) ↥(𝒜 67)

I would expect that since SetLike takes an outParam, it should have expected f to have type A, instead of just taking the ↥(𝒜 67), right?

[Kenny Lau]

i.e. I expect it to automatically coerce f to A. is this possible?

[Aaron Liu]

so it first fills in the implicit argument, so you have @Foo ℕ ↥(𝒜 67) (Submodule R A) ?_ 𝒜 f

[Aaron Liu]

then it synthesizes the typeclass variable (expected type is SetLike (Submodule R A) ↥(𝒜 67)), finds a SetLike (Submodule R A) A, and when it tries to unify with the expected type it fails

[Aaron Liu]

but if you do

import Mathlib

axiom Foo {ι A σ : Type*} [SetLike σ A] (𝒜 : ι → σ) (f : A) : Prop

variable (R A : Type*) [Field R] [Field A] [Algebra R A] (𝒜 : ℕ → Submodule R A) (f : 𝒜 67)

#check Foo 𝒜 ↑f

then it works fine

[Kenny Lau]

works fine here but didn't work in my case (I still had to specify the type), or maybe it was just slower, which is still suboptimal

[Kenny Lau]

Aaron Liu said:

so it first fills in the implicit argument, so you have @Foo ℕ (𝒜 67) (Submodule R A) ?_ 𝒜 f

then it synthesizes the typeclass variable (expected type is SetLike (Submodule R A) ↥(𝒜 67)), finds a SetLike (Submodule R A) A, and when it tries to unify with the expected type it fails

right, that's how it works now, but I'm asking is this what it should do, and is there an easy way to change it

[Kenny Lau]

i'm saying that it should find SetLike (Submodule R A) A, and then try to elaborate f to have type A; i.e. i'm proposing that they should use a different algorithm when it seems outParams

[Aaron Liu]

well you have to fill in the holes for typeclass synthesis to work

[Aaron Liu]

otherwise you get SetLike ?_ ?_ and that's not solvable

[Aaron Liu]

and then once they're filled in you can't exactly un-fill them

[Kenny Lau]

sure, from 𝒜 you can infer SetLike (Submodule R A) ?_, but it should delay resolving f

[Aaron Liu]

why should it delay f and not some other thing?

[Aaron Liu]

what determines that f requires delaying?

[Aaron Liu]

we could just as well do f first and delay 𝒜

[Kenny Lau]

Aaron Liu said:

why should it delay f and not some other thing?

1. @Foo ?_ ?_ ?_ ?_ ?_ ?_
2. @Foo ℕ ?_ (Submodule R A) ?_ 𝒜 ?_
3. @Foo ℕ A (Submodule R A) instSetLike 𝒜 ?_
4. @Foo ℕ A (Submodule R A) instSetLike 𝒜 (@Subtype.val A (fun x => x ∈ 𝒜 67) f)

I'm saying that it should use the explicit parameters one at a time, and then fill in earlier blanks, and then use the next explicit parameter

[Aaron Liu]

that's an idea

[Aaron Liu]

oh this works too

import Mathlib

axiom Foo {ι A σ : Type*} [SetLike σ A] (𝒜 : ι → σ) (f : A) : Prop

variable (R A : Type*) [Field R] [Field A] [Algebra R A] (𝒜 : ℕ → Submodule R A) (f : 𝒜 67)

#check (Foo 𝒜) f

[Kenny Lau]

w0t

[Aaron Liu]

since it goes in order

[Aaron Liu]

like you wanted

[Kenny Lau]

yeah I understand how it works but I'm just shocked

[Aaron Liu]

probably anything most things that puts 𝒜 and f in separate docs#Lean.Parser.Term.app nodes will work

[Kenny Lau]

minimsed version:

notation:max "ℕ" => Nat
class SetLike (A : Type) (B : outParam Type) : Type where
  protected coe : A → B → Prop
instance SetLike.instCoeSortType {A B : Type} [SetLike A B] : CoeSort A Type where
  coe p := Subtype (SetLike.coe p)
axiom Submodule : Type → Type → Type
@[instance] axiom Submodule.setLike {R A : Type} : SetLike (Submodule R A) A


axiom Foo {ι A σ : Type} [SetLike σ A] (𝒜 : ι → σ) (f : A) : Prop

variable (R A : Type) (𝒜 : ℕ → Submodule R A) (f : 𝒜 67)

#check Foo 𝒜 f -- fails
-- workarounds:
#check Foo 𝒜 ↑f
#check Foo 𝒜 (f : A)
#check (Foo 𝒜) f -- thanks to Aaron

[Aaron Liu]

interestingly, Foo 𝒜 <| f does not work

[Aaron Liu]

so the parentheses are probably doing something maybe?

[Robin Arnez]

<| has a special case when the left-hand side is an application, in which case it won't generate a new app node but just extend the old one