Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

The following

class foo (F : Type) where
  foo : F

class foobar (F : outParam Type) [foo F] where
  bar : F

gives the error

invalid class, parameter #2 depends on `outParam`, but it is not an `outParam`

It can be fixed writing

class foo (F : Type) where
  foo : F

class foobar (F : outParam Type) [outParam (foo F)] where
  bar : F

but in Lean3 this was not necessary.

I don't know if this is the expected behavior, but it looks worse than in Lean3.