[jonsterling]

it's nice for the haskell folks that they'll be getting some sort of dependent types, but suffice it to say that they will be of a very different sort than the Idris ones.

Not to mention, there is hope of giving a semantics to Idris since it is based on a fairly routine variant of type theory, whereas I don't think there is any hope at all of understanding "which" type theory the Haskell folks shall have implemented.