⊥しか取りえないってのは間違い。
MkT :: forall a. a -> Tはどんな値でも取ってT型を返す関数。
全称量化することで、型パラメータaが取り得る全ての型に共通の性質だけにしか言及できなくなる。
で、結局の所、⊥か、それ以外の何かが入ってる、としか言えなくなる。
(もちろんisBottomみたいな関数は定義できないから、実質何が入ってるかは不明)
forallが積集合云々ってのは、このことを言いたいんじゃないかと思う、多分。

一応、
foo (MkT x) = x :: T -> a
bar (MkT x) = id x :: T -> a
dup (MkT x) = (x, x) :: T -> (a, a)
みたいな関数は定義できる。
まぁT型の定義じゃ意味のある関数は定義できないけれど、値を取り出して関数適用するだけならおｋだから、
型制約付けといたり、関数とセットで入れとくと、OOPっぽいポリモーフィズムできるようになったりする。
ttp://www.kotha.net/ghcguide_ja/latest/data-type-extensions.html#existential-quantification

（件のページのNotesみて初めて知ったけど、WHNFに簡約はできるって発想は無かった…）