Spurious Cyclic Datatype Dependency Warning

[whonore]

Dafny version

4.6.0

Code to produce this issue

datatype Box<T> = Box(T)
datatype A = A(Box<int>)
datatype B = B(Box<A>)
const b: B := B(Box(A(Box(0))))

Command to run and resulting output

$ dafny verify test.dfy

test.dfy(3,9): Warning: because of cyclic dependencies among constructor argument types, no instances of datatype 'B' can be constructed
  |
3 | datatype B = B(Box<A>)
  |          ^

What happened?

Dafny warns that B has cyclic dependencies and can't be constructed, but there are no actual cycles and it can be constructed.

Possibly related to #4793 and #4819.

What type of operating system are you experiencing the problem on?

Mac

[keyboardDrummer]

Marking this as broken documentation with regards to severity, since the code was not designed to accept this. However, I think it would be a better use of time to enable Dafny to accept this than to update the documentation.