Issues with default parameters

Stream: lean4

[Jad Ghalayini]

Hello! I have found what I think is a bug: the following fails to typecheck

class Foo where
  x : Nat := by fail

class Bar extends Foo where
  x := 0

instance : Bar where

with the error

could not synthesize default value for field 'x' of 'Foo' using tactics

Unfortunately, my experiments hint there are some other bugs hiding behind this one, but it's a start.

https://live.lean-lang.org/#codez=MYGwhgzhAEBiD29oHcAWBTATugUNaAHtAFzQByYALiQLzQBGAntAGZgCWIOOokMAQmEzR0BSugB2AExgIkaLLnxFidAAzd2EiJTATg6EtEHCF2PNCA

[Notification Bot]

A message was moved here from #mathlib4 > Premonoidal categories by Eric Wieser.

[Jad Ghalayini]

Also, I've got a related issue, which is that the following doesn't work either

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

I'm not sure if this one is intended behavior, but it also means that my stuff doesn't work!

[Jad Ghalayini]

Note that

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

[Kyle Miller]

Could you please report these issues (https://github.com/leanprover/lean4/issues)? (If you're able to, you may assign them to me too.)

[Jad Ghalayini]

Here's a link to the issue: https://github.com/leanprover/lean4/issues/6769

Thanks!