Can't infer universe level

Stream: general

[Frédéric Dupuis]

I'm stuck on the following error in branch#dupuisf/ring_hom_class_map_comap, which shows up on docs#double_quot.quot_quot_to_quot_sup:

synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  @ring.to_semiring.{u}
    (@has_quotient.quotient.{u u} R (@ideal.{u} R (@ring.to_semiring.{u} R (@comm_ring.to_ring.{u} R _inst_1)))
       (@ideal.has_quotient.{u} R _inst_1)
       I)
    (@comm_ring.to_ring.{u}
       (@has_quotient.quotient.{u u} R (@ideal.{u} R (@ring.to_semiring.{u} R (@comm_ring.to_ring.{u} R _inst_1)))
          (@ideal.has_quotient.{u} R _inst_1)
          I)
       (@ideal.quotient.comm_ring.{u} R _inst_1 I))

inferred

  @ring.to_semiring.{(max u ?l_1)}
    (@has_quotient.quotient.{u u} R (@ideal.{u} R (@ring.to_semiring.{u} R (@comm_ring.to_ring.{u} R _inst_1)))
       (@ideal.has_quotient.{u} R _inst_1)
       I)
    (@comm_ring.to_ring.{(max u ?l_1)}
       (@has_quotient.quotient.{u u} R (@ideal.{u} R (@ring.to_semiring.{u} R (@comm_ring.to_ring.{u} R _inst_1)))
          (@ideal.has_quotient.{u} R _inst_1)
          I)
       (@ideal.quotient.comm_ring.{u} R _inst_1 I))

The synthesized and inferred versions are identical except for a universe level metavariable ?l_1 in the inferred version. Has anyone seen anything like this before? I'm completely baffled by this (and unable to bring it down to an MWE).

[Eric Rodriguez]

does Lean know that max u 0 = u?

[Eric Wieser]

This works:

def quot_quot_to_quot_sup : (R ⧸ I) ⧸ J.map (ideal.quotient.mk I) →+* R ⧸ I ⊔ J :=
by exact ideal.quotient.lift (J.map (ideal.quotient.mk I)) (quot_left_to_quot_sup I J)
  (ker_quot_left_to_quot_sup I J).symm.le

[Adam Topaz]

yeah you might need to add a .{u 0} somewhere....

[Eric Wieser]

Without the by exact, lean doesn't decide on the type of the def before reading its implementation

[Eric Wieser]

The feature that allows def n := 1 is also the feature that makes this type of thing go wrong

[Eric Rodriguez]

this behaviour with def/example vs lemma/theorem always bites everyone... it'd be nice if Lean4 had a setting to control this

[Eric Wieser]

I wonder if we can handle this with an attribute

[Eric Rodriguez]

or at least a version of def that typechecks like lemma

[Eric Rodriguez]

Eric Rodriguez said:

does Lean know that max u 0 = u?

I'm still curious about this, fwiw. I never know what is allowed in universe arithmetic

[Sebastian Ullrich]

Eric Rodriguez said:

this behaviour with def/example vs lemma/theorem always bites everyone... it'd be nice if Lean4 had a setting to control this

Lean 4 defs with given types behave like theorem. The primary remaining difference is that you can still leave out the type with def.

[Frédéric Dupuis]

Eric Wieser said:

Without the by exact, lean doesn't decide on the type of the def before reading its implementation

I see, thanks!

[Eric Wieser]

My naive attempt at implementing a lean4-style def command was

section
setup_tactic_parser

reserve notation `def!`

@[user_command]
meta def angry_def (meta_info : decl_meta_info) (_ : parse $ tk "def!") :
  lean.parser unit := do
{ name ← ident,
  binders ← parse_binders,
  binders ← binders.mmap (λ b : pexpr, do
    expr.local_const u n bi t ← pure b,
    t ← of_tactic (tactic.to_expr t),
    let b2 := expr.local_const u n bi t,
    parser.add_local b2,
    pure b2),
  tk ":",
  type ← parser.pexpr,
  tk ":=",
  body ← parser.pexpr 0,
  x ← binders.mfoldl (λ (x : pexpr × pexpr) b, do
    expr.local_const u n bi t ← pure b,
    pure (expr.pi n bi (pexpr.of_expr t) x.1, expr.lam n bi (pexpr.of_expr t) x.2)) (type, body),
  type ← tactic.to_expr ``(%%(x.1) : Sort*),
  body ← tactic.to_expr ``(%%(x.2) : %%(type)),
  tactic.trace (name, binders, type, body),
  tactic.add_decl (declaration.defn name [] type body default tt) }

end

protected def! foo (x : ℕ) : ℕ := x * x

I can't work how docs#parse_binders is supposed to be used though, and so that doesn't actually work

[Eric Wieser]

It also doesn't handle variables

[Mario Carneiro]

@Sebastian Ullrich said:

Eric Rodriguez said:

this behaviour with def/example vs lemma/theorem always bites everyone... it'd be nice if Lean4 had a setting to control this

Lean 4 defs with given types behave like theorem. The primary remaining difference is that you can still leave out the type with def.

It doesn't work for example though: I want example := 1 to work