Can't provide impl for structure accessor?

Stream: lean4

[James Gallicchio]

Why does this example not work as one would expect?

namespace Hidden

structure Array (α : Type u) (n : Nat) : Type u where
  data : (i : Fin n) → α

@[extern "some_extern"]
def get {α} {n : Nat}
        (A : Array α n) (i : Fin n) : α
  := A.data i

attribute [implementedBy get] Array.data

It claims there is a type mismatch, but I can't for the life of me see why

[Leonardo de Moura]

The check is currently syntactic and universe level parameter names are taken into account. The following works

namespace Hidden

structure Array (α : Type u) (n : Nat) : Type u where
  data : (i : Fin n) → α

@[extern "some_extern"]
def get {α : Type u} /- <<<< Changed here -/ {n : Nat}
        (A : Array α n) (i : Fin n) : α
  := A.data i

attribute [implementedBy get] Array.data

I will improve this, and make sure the universe levels parameter names are not taken into account.

[James Gallicchio]

Ah, weird, okay -- thank you for giving it a look!

[James Gallicchio]

It also seems like the calling convention modifiers prevent it from matching; is there a way to modify the conventions on auto-generated accessors? (if not I can just put another def between them)