c-:Π-x:(Π-w:o.a w).Π-z:o.Π[i]y:(a·(d+·(*;x z))).a·(d+·(*;y))
Nonetheless, it serves as a useful counterexample to the approach I was trying earlier. Trying to typecheck
Y Y : a· (d+ · (*; Y Y))
where
Y = λ w . c- · (w;w;*)
leads to an infinite loop.
There had better be a workaround along the lines I was thinking last night, or else I'm kinda hosed.
