| > Nothing deep. Just that "=" means so many things that it seemed better | > to use a different notation. | > | | How about ==? Only one meaning so far, and that both on the term level and | equivalent to the constraint I'm quite happy with "~"! It's sufficiently different from "=" that someone meeting it for the first time is going to thing "hmm, better read the manual"; and they'd be right. Anyway, while on this subject, I am considering making the following change: make all operator symbols into type constructors (currently they are type variables) That would allow you to write data a * b = Prod a b data a + b = Left a | Right b and write natural-looking types like f :: a*b -> a When we have indexed type families working, this will be even more natural. As things stand, only operators starting with a ":" are type constructors, thus data a :*: b = Prod a b etc. By analogy with the term language, operators are currently classified as "type variables", so you could write (oddly) data T (+) x = MkT (+) x [this may not even work today, but it should] to mean the same as data T y x = MkT y x But this is pretty useless! Very occasionally one might want a type variable with kind (*->*->*), but much much more often you want a type *constructor* with that kind. I thought I'd mention this here in case people have ideas. Simon