[ 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
