Massive update. Previously type checking was possible only for closed types. This limitation has now been removed.
Type checking is now simply a consequence of regular constraint propagation, previously it was a separate pass. Nevertheless, the system is still statically typed in the expected sense.
Additionally the builtins, the standard library, and even CUE operators were missing types. Now they have precise types so more interesting code can be written (and type checked). A type listing is provided:
github.com/4ad/qcue/blob/mas…). The listing uses explicit (desugared) `forall`, even though all examples use the sugared form. This can be considered both an advantage and a disadvantage. Looking at the types is very informative.
Something has been lost, however. Existential types and dependent types are gone. Existential types are interesting (and in some sense almost inevitable), but they can form a separate proposal. (Additionally the burden on the existing prototype was too high. It was too costly to iterate on the implementation with existential types still present.)
The old playground that still has existential types as well as the old paper can be found at:
v6.cue-semantics.org.
The universal-only paper (v9) is now better organized, shorter, and easier to read. The semantics hasn't changed whatsoever.
There exists an unpublished partial Lean formalization of the current paper.