Evaluation (& substitution?) produces ill-typed normal forms

[robrix]

I haven’t yet seen a case where this is causing us trouble, but while working on #174, I ran into this example of a well-typed expression for which evaluation does not preserve well-typedness:

cons Character ('h' : Character) (cons Character ('i' : Character) (nil Character))