F :: forall {k} k2. k -> k2 -> *