Comment by kubb

> we sometimes blur the distinctions between these distinctions

> venerable program extraction algorithm

> type inference seems a timid virtue

> it is a nuisance that the kind-level ∀ is compulsorily implicit

It sounds fun to do academic research, is that why there's an oversupply of PhD students?