Does embedding recursively open definitions?

[verdverm]

What version of CUE are you using (cue version)?

0.4.2

What did you do?

package repro

#Foo: {
  bars: [...#Bar]
}

#Bar: {
  bar: string
}

#Foo

bars: [{
  bar: "bar"
  baz: "baz"
}]

also same when not at top level

package repro

#Foo: {
  bars: [...#Bar]
}

#Bar: {
  bar: string
}

foo: {
  #Foo
  bars: [{
    bar: "bar"
    baz: "baz"
  }]
}

What did you expect to see?

An error like bars.0: field not allowed: baz:

What did you see instead?

$ cue eval repro.cue 
#Foo: {
    bars: []
}
#Bar: {
    bar: string
}
bars: [{
    bar: "bar"
    baz: "baz"
}]

[mpvl]

@verdverm This is a very interesting case.

Definitions are indeed recursively opened according to the spec, although there are cases where it does not erroneously.

But arguably it should not open up these cases where a type is defined by a reference to a defintion.

That said, it does put in question the use of the embedding at top level pattern as seen here. For the non-top-level case one could simply write:

foo:  #Foo
foo: {
  bars: [{
    bar: "bar"
    baz: "baz"
  }]
}

But it is not possible to do this at the top level. So we may need another way to express this somehow, without writing

#Foo&{
  bars: [{
    bar: "bar"
    baz: "baz"
  }]
}

at the top level.

[myitcv]

That said, it does put in question the use of the embedding at top level pattern as seen here

Didn't we envisage using must() in situations where the top level should be constrained by a definition but that definition not be opened?

But arguably it should not open up these cases where a type is defined by a reference to a defintion.

I'm not clear what the "right" answer is here. There is at least some symmetry to embedding recursively opening a definition where referencing a definition recursively closes it. The reason I hesitate on the relaxing of the embedding rule to "not open up these cases where a type is defined by a reference to a definition" is that people might be referencing definitions within a structure to enable/promote reuse, but still be relying on the existing behaviour of things being opened recursively.

So perhaps we need to collect examples that help to inform thinking here?