This may come across as pedantic, but your example only defines a variable with the bottom type. You never actually "construct an inhabitant" because the constr

This may come across as pedantic, but your example only defines a variable with the bottom type. You never actually "construct an inhabitant" because the construction itself is nonterminating. This is actually, in my experience, one of the more common uses for the bottom type - it can mark functions that never return (the "exit" function, for example, or something that loops infinitely, or something that raises an exception).