I can think of a use for a non-equality constraint: an alphabetical ordering on Symbol. This would allow experimental implementations of extensible records (without shadowing) which keep the labels sorted. An order constraint on Nat might be useful, too. Barney.