Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

Default parameters and default initialization with tactics do not seem to play well together. In particular, the following two test programs do not typecheck:

class Foo where
  x : Nat := by fail

class Bar extends Foo where
  x := 0

instance : Bar where

and

class Foo where
  x : Nat
  hx : x = x

class Bar extends Foo where
  hx' : x = x := by rfl
  hx := hx'

instance : Bar where
  x := 0

On the other hand,

class Foo where
  x : Nat
  hx : x = x

class Bar extends Foo where
  hx' : x = x := rfl
  hx := hx'

instance : Bar where
  x := 0

works as expected, so it's got something to do with tactics.

Context

I'm trying to implement premonoidal categories in mathlib without breaking the old MonoidalCategory API, and this requires a lot of default conditions. Getting everything to work is very challenging!

Versions

Still broken as of 4.16.0-nightly-2025-01-24