coe sometimes gets stuck on a Clo #11

New issue

Closed

opened 2023-06-05 10:54:20 -04:00 by rhi · 0 comments

rhi commented

2023-06-05 10:54:20 -04:00

Owner

sometimes a term looks like

coe (i ⇒ caseω tag return ★ of { 'just ⇒ A; 'nothing ⇒ True }) payload

where i is unused in the path, so it should just reduce to just

payload ∷ (caseω tag ⋯)

right? well, it doesn't if the case expression actually has a delayed subst somewhere that still mentions i. (this is why the pretty printer includes it, btw.) so just checking for a mention anywhere in ST is not enough.

sometimes a term looks like ``` coe (i ⇒ caseω tag return ★ of { 'just ⇒ A; 'nothing ⇒ True }) payload ``` where `i` is unused in the path, so it should just reduce to just ``` payload ∷ (caseω tag ⋯) ``` right? well, it doesn't if the case expression _actually_ has a delayed subst somewhere that still mentions `i`. (this is why the pretty printer includes it, btw.) so just checking for a mention anywhere in `ST` is not enough.