idris-lang/Idris-dev — pull request #1265 by ziman (2014-05-29 14:08:36+00:00)
Title: Split dependent pairs

This patch splits the type of dependent pairs into three:
* `Pair : (a : Type) → (P : a → Type) → Type` — non-erased, also known as `(?v ** ?rhs)`.
* `Exists : {a : Type} → (P : a → Type) → Type` — first field erased. Can be viewed as a closure over `P`: `List a ≃ Exists $ Vec_flipped a`. I don't really like the name `Exists` but I don't have anything better and it's called `∃` in Agda, too.
* `Subset : (a : Type) → (P : a → Type) → Type` — second field erased.

There was originally a typeclass `DepPair` that would provide `getWitness` and `getProof` but it didn't work well, since typeclass resolution would choke here and there. Type-directed disambiguation works well in all these cases so it replaces the typeclass.

There's also a test to verify that things actually get erased.