Stuck at universe constraint FromJson

Stream: lean4

[Adam Topaz]

I came across yet another universe unification issue, this time trying to write down some FromJson instance. Here's a MWE:

import Lean

open Lean

structure Foo (α : Type u) (β : Type v) where
  x : α
  y : α × β

instance [FromJson α] [FromJson β] : FromJson (Foo α β) where
  fromJson? j := do
    let x ← j.getObjValAs? α "x"
    let y ← j.getObjValAs? (α × β) "y"
    return { x := x, y := y }

This gives

stuck at solving universe constraint
  max (max ?u.554 ?u.619) ?u.620 =?= max ?u.619 ?u.620
while trying to unify
  (FromJson (α × β)) ((FromJson (α × β)) α β)
with
  (FromJson (α × β)) ((FromJson (α × β)) α β)

Can anyone tell where the max is being introduced? (besides the product... I don't think that's the issue?). Note that the error mentions three universe parameters... Why?!

[Adam Topaz]

Note that the following

structure Foo (α : Type u) (β : Type v) where
  x : α
  y : α × β
deriving FromJson

results in the same error (as expected)

[Adam Topaz]

Note that this works just fine:

structure Foo (α : Type u) (β : Type v) where
  y : α × β
deriving FromJson

[Gabriel Ebner]

do-notation only supports a single universe. This is a known limitation.

[James Gallicchio]

instance [FromJson α] [FromJson β] : FromJson (Foo.{u,v} α β) where
  fromJson? j := do
    let x : α ← j.getObjValAs? α "x"
    let y ← j.getObjValAs? (α × β) "y"
    return { x := x, y := y }

gives a good error message

[Eric Wieser]

Not just do notation but all of the monad notation, right?

[Eric Wieser]

James Gallicchio said:

... gives a good error message

This is a case of autoImplicit making the error more confusing, right?

[James Gallicchio]

I guess in the sense that you aren't specifying what universe the types are coming from. The universe inference works great until it doesn't and then the messages are unreadable.

[James Gallicchio]

Eric Wieser said:

Not just do notation but all of the monad notation, right?

yeah, the monad typeclasses are not univ polymorphic

[Eric Wieser]

FWIW, I'm PR'ing a docs#ULiftable instance for Except right now, which almost makes it possible to write the above

[Eric Wieser]

The next problem is that docs#Lean.instFromJsonProd it's called isn't universe polymorphic has had the wrong universes inferred!

[Eric Wieser]

mathlib4#6350

[Eric Wieser]

@Adam Topaz, here's a working version:

import Lean
import Mathlib.Control.ULiftable

open Lean

set_option autoImplicit false

universe u v v₁ v₂

structure Foo (α : Type u) (β : Type v) where
  x : α
  y : α × β

instance {ε : Type u} : ULiftable (Except.{u,v₁} ε) (Except.{u,v₂} ε) where
  congr e :=
    { toFun := Except.map e
      invFun := Except.map e.symm
      left_inv := fun f => by cases f <;> simp [Except.map]
      right_inv := fun f => by cases f <;> simp [Except.map]  }

-- fails: this expects `α β : Type (max u v)`!
example {α : Type u} {β : Type v} [FromJson α] [FromJson β] : FromJson (α × β) := Lean.instFromJsonProd

instance {α : Type u} {β : Type v} [FromJson α] [FromJson β] : FromJson (α × β) where
  fromJson?
    | Json.arr #[ja, jb] => do
      let ⟨a⟩ : ULift.{v} α := ← ULiftable.up <| fromJson? ja
      let ⟨b⟩ : ULift.{u} β := ← ULiftable.up <| fromJson? jb
      return (a, b)
    | j => throw s!"expected pair, got '{j}'"

instance {α : Type u} {β : Type v} [FromJson α] [FromJson β] : FromJson (Foo.{u,v} α β) where
  fromJson? j := do
    let ⟨x⟩ : ULift.{v} α := ← ULiftable.up (j.getObjValAs? α "x")
    let y ← j.getObjValAs? (α × β) "y"
    return { x := x, y := y }

[Eric Wieser]

lean4#2382 fixes the error in docs#Lean.instFromJsonProd (which was also caused by autoImplicits)

[Mac Malone]

James Gallicchio said:

Eric Wieser said:

Not just do notation but all of the monad notation, right?

yeah, the monad typeclasses are not univ polymorphic

The core monad classes (e.g., Monad, Alternative, MonadReader,MonadState, and MonadExcept) are all universe polymorphic. And do notation support "technically" supports universe polymorphism. The problem is the two key building blocks, Bind and Seq, are not heterogenous and thus do not support chaining monads of different universes (without one lifting to the other).

[James Gallicchio]

yeah i guess i should have said not universe polymorphic enough :joy:

[Eric Wieser]

Adam Topaz said:

This gives

stuck at solving universe constraint
  max (max ?u.554 ?u.619) ?u.620 =?= max ?u.619 ?u.620
while trying to unify
  (FromJson (α × β)) ((FromJson (α × β)) α β)
with
  (FromJson (α × β)) ((FromJson (α × β)) α β)

This message is nonsense, right? The expressions it refers to don't typecheck! Is there an open issue about this?

[Eric Wieser]

Hovering over them in the goal view gives Error: Rpc error: InternalError: function expected

[Mario Carneiro]

I have seen this issue before

[Mario Carneiro]

we shouldn't expect it to completely type check, especially if it's reporting on a type error, but I have it apply functions on total nonsense

[Mario Carneiro]

like using the type of a function instead of a function itself

[Mario Carneiro]

which looks like the issue here

[Mario Carneiro]

can you make a MWE?

[Eric Wieser]

The example at the top of this thread is a Lean-only MWE