ToJson deriver hygiene

Stream: lean4

[James Gallicchio]

MWE:

import Lean.Data.Json

structure AsFunc (self) where
  oneOf   : Option (Array self)
deriving Lean.FromJson, Lean.ToJson

only works if the parameter is named self. Is this a hygiene issue in the implementation? I tried to figure out where it's coming from in the metacode but couldn't figure it out.

[Mario Carneiro]

Note that names matter for a {To, From}Json implementation

[James Gallicchio]

but type parameter names...?

[Mario Carneiro]

It's in the constructor:

structure AsFunc (sel) where
  oneOf   : Option (Array sel)
-- AsFunc.oneOf.{u_1} {sel : Type u_1} (self : AsFunc sel) : Option (Array sel)

structure AsFunc (self) where
  oneOf   : Option (Array self)
-- AsFunc.oneOf.{u_1} {self : Type u_1} (self : AsFunc self) : Option (Array self)

[Mario Carneiro]

here's a replication without the deriving handler:

structure AsFunc (self) where
  oneOf   : Option (Array self)

open Lean
example {self} [ToJson self] (x : AsFunc self) : Json :=
  Json.mkObj <| List.join [[("oneOf", toJson (x).oneOf)]]
                                          -- ^^^^^^^^^
-- application type mismatch
--   @AsFunc.oneOf x
-- argument
--   x
-- has type
--   AsFunc self : Type ?u.274
-- but is expected to have type
--   Type ?u.307 : Type (?u.307 + 1)

[Mario Carneiro]

minimized:

structure Foo (self) where
  val : self

example {α} (x : Foo α) : α := x.val -- fails
example {α} (x : Foo α) : α := Foo.val x -- works

[Kyle Miller]

I guess according to the app elaborator when you have a projection of a structure, x.val is meant to be equivalent to Foo.val (self := x).

[Mario Carneiro]

Foo.val (self := x) also fails exactly when the parameter is named self, which makes sense - the reference is ambiguous in that case. But it seems that x.val unfolds to effectively Foo.val (self := x), leading to this issue

[James Gallicchio]

ahhh, I see.

[James Gallicchio]

a linter for ambiguous arg names would be pretty nice :joy:

[Mario Carneiro]

I think the name resolution should work from back to front though, generally later arguments shadow earlier ones not the other way around