Thanks! That was exactly the sort of response I was looking for.

This explains why you need to double up for your current definitions. To
choose between two booleans (which will in turn allow you to choose between
'a's), you need a CB (CB a). You can eliminate the asymmetric type, though,
like so:

 cand :: CB a -> CB a -> CB a

 cand p q t f = p (q t f) f

Right. When he was working on it, I thought of that, and seemed to have completely forgotten when I reworked it.
 

You can probably always do this, but it will become more tedious the more
complex your functions get.

> >type CB a = forall a . a -> a -> a

Note: this is universal quantification, not existential.

As I would assume. But I always see the "forall" keyword used when discussing "existential quantification". I don't know if I've ever seen an "exists" keyword. Is there one? How would it be used?