| In that context, how well-understood is the combination of impredicative | types via boxy types and a proper existential quantifier at the moment? | It's certainly something that has many uses in an industrial context.
Stephanie Weirich, Dimitrios Vytiniotis, and I are currently re-writing our paper about type inference for impredicative polymorphism. I don't think there's any difficulty with existentials, at least when they are wrapped in a data constructor (which is the way GHC deals with existentials at the moment). We'll have a draft done in a couple of weeks. (Until then the paper on my home page is still approximately right.) http://research.microsoft.com/%7Esimonpj/papers/boxy Can you elaborate on what you had in mind in your last sentence above? Simon _______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell