[TYPES] Annotating an AST with (existential) types , with ordered contexts - à la Dunfield Krishnaswami

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Hi all,

I am trying to write a compiler with existential types. I understand that the Dunfield-Krishnaswami approach with ordered contexts is the new/cool way to do type inference. 

However, I am stumped as to how to annotate a term with all the solved variables (when using ordered contexts). Is this possible? Is there any guidance/existing literature? 

As an example, I’d like to be able to know/use the type of f in the below:

(λf. (f (λx. x)) (f ())) (λx. x)

Thanks,
Vanessa McHale