We couldn't do this before because we carry an Atom in the Simp->Imp substitution and we didn't want to add an AtomicImpName case to Atom just for this single use. But with the new IR system that's fine! We add the case and signal that it doesn't have to be handled anywhere else by giving it the Sat r (Is SimpToImpIR) constraint.
One awkward part of the change is that now we have a mix of atom names and imp names in the block that we want to hand to Algebra. I resolved this by rebinding the imp names to atom names before calling into Algebra, but it's a bit ugly.
We couldn't do this before because we carry an
Atomin the Simp->Imp substitution and we didn't want to add anAtomicImpNamecase toAtomjust for this single use. But with the new IR system that's fine! We add the case and signal that it doesn't have to be handled anywhere else by giving it theSat r (Is SimpToImpIR)constraint.One awkward part of the change is that now we have a mix of atom names and imp names in the block that we want to hand to Algebra. I resolved this by rebinding the imp names to atom names before calling into Algebra, but it's a bit ugly.