Universe inequalities error

[theolaurent]

The following code returns Failed to solve universe inequalities for inductives

type bar 'a =
  | Bar1 : 'a -> bar 'a
  | Bar2 : foo 'a -> bar 'a
and foo 'a =
  | Foo : bar 'a -> foo 'a

I am not sure why. This return the same error:

type bar 'a =
  | Bar : 'a -> bar 'a
and foo 'a =
  | Foo : bar 'a -> foo 'a

while the seemingly equivalent

type bar 'a =
  | Bar : 'a -> bar 'a
type foo 'a =
  | Foo : bar 'a -> foo 'a

doesn't.

[theolaurent]

The error disappears with one Type u#x annotation. My intuition would be that this annotation shouldn't tell anything new.

module Bug1462

type bar (a : Type u#x) =
  | Bar1 : a -> bar a
  | Bar2 : foo a -> bar a
and foo a =
  | Foo : bar a -> foo a