{-# LANGUAGE RankNTypes #-}
type Bottom = forall a. a -- zero inhabitants
f :: Bottom -> a
f x = x
I think you are running into some weird haskellisms with your Bottom-type.
The normal way of defining that in haskell is using the "EmptyDataDecls" pragma, like this:
{-# LANGUAGE EmptyDataDecls #-}
data Empty
g :: Empty -> a
g x = x
(From a theoretic standpoint, I would have thought your Bottom was a essentially a type-level identity function..)
'forall a. a' is just how you define the bottom type in System F, which Haskell is somewhat based on. As a type it describes that a term of that type can just conjure a value of any type out of thin air, which is obviously nonsense. That what makes it the bottom type.
The sub typing behavior associated with that is just the normal subsumption rule of polymorphic functions. The same reason why you can pass a function of type 'forall a. a -> a' to something expecting a function of type 'Int -> Int'. The types don't 'match' directly, but they do under the subsumption rule.
With "forall a. a" I was coming from the persepctive of intuisionistic type theory where the usual parametric polymorphism just get subsumed by Π-types and universal quantification is usually represented with Π-types, so you would have:
forall a.a (Universal Quantification)
<==> Π(a : Type) a (Π-type)
<==> (a : Type) -> a (Agda-notation)
==> a -> a (Π-type as regular function type)