Abstract

Weak-head call-by-name reduction is used for both term evaluation and type conversion in our core calculus λI. This brings simplicity of the design but is not expressive enough to convert types up to congruence. We generalize casts with full reduction and study a variant of λI with full-reduction casts. Type checking is still decidable and type soundness holds up to erasure. We show a case study of full casts to encode GADTs without built-in equalities or injectivity rules.