> GHC cheats in this area. The problem is that (a ~# b) is a type, because that > is terribly, terribly convenient. But it really shouldn't be. > > The problem is that coercion variables are different from regular variables. > So, if we say (v :: a ~# b), we must always be careful: is v a coercion > variable or not? If it isn't, then v is useless. You cannot, for instance, > use v in a cast.
I don't really see a problem here. The fact that only a "coercion variable" can be used in a cast should be enforced by the typing rule for cast. That doesn't require having a distinct "syntactic category" of coercion variables, unless I'm missing something. -- mniip _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
