We currently normalize in writeback after hir typeck with the new solver to avoid dealing with unnormalized projections during lints and in the MIR. This is probably fine, but we shouldn't forget or ignore this.