[Haskell-cafe] Associated data types

[Jules Bean]

Lennart Augustsson wrote:
> For an associated data type D, we know that the type function D is
> injective, i.e., for different indicies given to D we'll get different
> data types.  This makes much more powerful reasoning possible in the
> type checker.  If associated data types are removed there has to be
> some new mechanism to declare an associated type as injective, or the
> type system will lose power.

Interesting.

Are you able to give an example which exploits this "known distinct 
types" effect?