Some type parameters cannot be inferred

[robrix]

Module+List.swift has a bunch of type parameters that can’t be inferred, because we’re only able to unify as part of the pairwise definitional equality of two terms. Therefore when we apply a function like (a : Type) → (b : Type) → (a → b) → b, we have to specify a and b explicitly since we can’t guess them from their relationships with the later parameters.

One possible solution would be constraint/assumption generation & the unification thereof.