Widening and Narrowing

As stated, I want to be able to put values of different types, but known interfaces into a list. First, I thought I would need something elaborate for that, which turned out to be true, but not as elaborate as I first expected.

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...