On Sunday, 11 October 2020 at 12:18:59 UTC, Stefan Koch wrote: > Good Morning, > > today I would like to write about something which came up while > implementing type functions. > > [...] You have a typo here: But Ø cannot be ⊥, because ⊥ can be a valid return type The empty type cannot be a return type