In article <41D808C3.7010408@cs.nott.ac.uk>,
Conor McBride
The latter also means that the existential type encoding of 'some good term' doesn't give you a runnable term. There is thus no useful future-proof way of reflecting back from the type level to the term level. Any existential packaging fixes in advance the functionality which the hidden data can be given: you lose the generic functionality which real first-order data possesses, namely case analysis.
If I understand you correctly, without GADTs/datatype families, you cannot create Expression as a type-constructor without Oleg's auxiliary "t" argument that in fact encodes the structure of the expression. Is that right? I certainly can't see any way of getting rid of it: if, as you say, you existentially package it, the compiler can't deduce runnability. -- Ashley Yakeley, Seattle WA