Eric Mertens wrote: > (but I've had my head in Agda lately) Indeed, coming across this problem tempted me to abandon the real world and take refuge in Agda. > http://hpaste.org/44469/software_stack_puzzle Wow, so simple, and no higher-rank types! This is the best solution yet. I am now truly in awe of the power of GADTs. Thanks, Yitz