I'm struggling to actually describe the bug that this fixes — I ran into it in the wild and divined a reproducer based on the logs (with 14 different verbosity flags...!). I guess literally the problem is this: if we compareAtom a neutral value in a singleton record against a projected metavariable, the field should be compareAs'd, to account for eta again.
The reproducer uses reflection to set up the elaborate ritual. We need:
A comparison of a neutral against a projected metavariable, which does not trigger the meta shortcut;
In an eta record type with one singleton field and one non-eta field.
The comparison against a projected meta lands us in applyE, which eta-expands the meta and compares the corresponding field in the expansion against the original thing. If you set things up just right you get fireworks:
Checking Test138 (/home/amelia/default/Projects/agda/Test138.agda).
/home/amelia/default/Projects/agda/Test138.agda:23,5-27,41
tt != Hom.hom fun tt of type ⊤
Anyway, the fix is just to compareAs the field, so that whatever applicable eta rules can fire again.
I'm struggling to actually describe the bug that this fixes — I ran into it in the wild and divined a reproducer based on the logs (with 14 different verbosity flags...!). I guess literally the problem is this: if we
compareAtoma neutral value in a singleton record against a projected metavariable, the field should becompareAs'd, to account for eta again.The reproducer uses reflection to set up the elaborate ritual. We need:
The comparison against a projected meta lands us in
applyE, which eta-expands the meta and compares the corresponding field in the expansion against the original thing. If you set things up just right you get fireworks:Anyway, the fix is just to
compareAsthe field, so that whatever applicable eta rules can fire again.