In the example it is called "NonEmpty". There's the "Stream" nominal type, shown below in Haskell-like text syntax: newtype Stream a = () -> (Empty | NonEmp

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.