Re: type families + GADT = type unsafety?

(Simon, does this mean that non-~ discharging will become subject to GADT-style type annotation rules?)

No, it does not. No type annotations required in non-GADT-related code, even if equalities are involved. Tom -- Tom Schrijvers Department of Computer Science K.U. Leuven Celestijnenlaan 200A B-3001 Heverlee Belgium tel: +32 16 327544 e-mail: tom.schrijvers@cs.kuleuven.be