RedPRL
Idea: let Quote control unfolding
Maybe we shouldn't automatically unfold anything in evaluation, and instead rely on Quote to specifically request it during checking definitional equivalence. I think I see a way to make that work.
(Just as a remark, this is not as simple as it sounds -- we still need to be able to evaluate to a whnf, in order to implement the typechecker!! Conversion is not the only thing that matters.)
If you allow the type checker to backtrack, that is, to raise NowICareAboutNormalForms, would that still be an issue? On the other hand, we can always try syntactical comparison before doing the full expansion.
What would be cool is if I could first evaluate without unfolding, and then tell the evaluator "OK, I want you to unfold this" etc., and just keep trying until things work. I think it might be plausible.
(Then, the idea is that both the typechecker and the conversion checker/quotation would exploit this.)