counter-example in mind? I note that GADTs are types, so this might not scale to an untyped setting. Anyway, I'm not following research on GADTs closely, but y

counter-example in mind? I note that GADTs are types, so this might not scale to an untyped setting. Anyway, I'm not following research on GADTs closely, but you show me a sound and complete, compositional encoding of (idealised) object-calculi a la Abadi/Cardelli using (idealised) Haskell?