Can you force
{-# OPTIONS_GHC -Wincomplete-patterns -Werror=incomplete-patterns #-}
?
It would ban solutions like this. In previous catas too.

Yeah, you can use infinite types if you wrap them in a newtype.

Oh damn, PRight is not applied to the continuation but to the initial value. Yep, you're right. So it can't be done.

Thanks!

I get that, but why must it be S a in the first place?

If we have Paren a -> Paren a, apply PRight first, then k, then PLeft, we can feed it Paren Z, we don't need the input to be Paren (S a). This is dependent upon evaluation otder; if you start with PLeft, you do need Paren (S a).

But I have been unable to force that order, so I don't know if that would make it what I would like it to be.

That's what GHC tells me. But it needs not, depending on evaluation order. It could have Paren Z everywhere.

I really hope I can find a way to ban this solution.

But let me tell a story. We got detective and criminal fighting with each other. The bad thing is:

1. Detective can't treat a person who has not committed a crime as a criminal.
2. Detective should brought all criminals to justice.
3. Criminal can always find new ways to circumvent detective.
4. There is no ultimate way to prevent criminal from committing crimes.

Then detective carfully using axioms and modus ponens to find the solution. So... :p

> <

Intended. It was already stated in the section comments.