I just need to be able to erase a type. Which is pretty natural, since I can already do the opposite with type matching.
An example, a list of integers and strings:
def islist: ::Text t => list t = cons (5:t) (cons ("Hi!":t) nil)
It's as easy as that. It'll need some work on the prover and the type checker though, since now type variables are used in the terms of definitions, and that's not even close to nice.
022110: Oh cool, another nice date. The compiler I have know inferences a type in a simple bottom-up pass and I don't really feel like exposing the type of the definition into the term. Can I get away with just introducing unknowns?
Great, more work...