Option is typechecking when it shouldn't?

Stream: new members

[Moritz R]

Why does the following typecheck? groundI I isn't an Option yet i can compare it with some Is

variable {F}

def groundI : F → List Nat := sorry

theorem why : ∀(I : F) (Is : List Nat) (_ : groundI I = some Is), True := sorry

[Robin Arnez]

docs#optionCoe

[Robin Arnez]

In other words, groundI I gets coerced into some (groundI I)

[Moritz R]

Hm, why does it not show any coercion arrow or anything in the editor (only in the infoview i can see some (groundI I)

[Moritz R]

image.png

[Moritz R]

Do we only have coercion arrows in the infoview?

[Robin Arnez]

Coercions don't have dedicated syntax, instead they expand directly, e.g. like how ((3 : Nat) : Int) elaborates to (Nat.cast 3 : Int). The coercion arrow only comes from the fact that Nat.cast is tagged @[coe]. In this case we have (groundI I : Option (List Nat)) turn into some (groundI I). some is not tagged @[coe] (that would surely be confusing) so it just shows up as normal.

[Moritz R]

I was thinking more about something that would show on the left side that some coercion is applied to groundI I

[Moritz R]

in the infoview shortening some I to ↑I is confusing, i agree

[Aaron Liu]

In the editor? Like the place you input text?

[Moritz R]

yes

[Moritz R]

image.png
Some annotation like these implicitly inferred arguments that we already have

[Moritz R]

so a shadowy arrow in front of groundI I

[Aaron Liu]

afaik autoimplicits is the only thing that shows up in the editor directly like that