Module types 

The types of values, for the parts of conversion and reduction that look at types — proof irrelevance, η, struct-η, unit-like types, K — and for projections. Values reaching here are well-typed, so this is inference without checking: a head’s type followed along the spine.