[yairchu]

In the example it is called "NonEmpty".

There's the "Stream" nominal type, shown below in Haskell-like text syntax:

  newtype Stream a = () -> (Empty | NonEmpty { head :: a, tail :: Stream a })

To construct a "Stream", we type "stream" in a hole and pick "Stream« ◗ _", which wraps a "deferred computation" ("◗ _") in the nominal "Stream" type constructor.

Now the type of the value inside the hole within is just "Empty | NonEmpty { head :: a, tail :: Stream a }", now type "nonempty" and pick it.