Hi, Am Montag, den 02.09.2013, 12:07 -0400 schrieb Richard Eisenberg:
Here are some specific thoughts, upon reviewing your (surprisingly short!) patch:
well, note the long list of thing that remain to be done. Also, the code went through several iterations already; I guess that helps as well :-)
- I strongly dislike the name NT (and derivatives), for at least two reasons: 1) Someone new to this work won't know what it means, and 2) it's useful for things unrelated to newtypes (because of phantoms). How about "safeCoerce"? The class could have the name "Coercible". Neither of these names conflict on a default search at Hoogle.
The name is a working title, and your suggestions are good. I might prefer something that also hints as to why things are coercible and hints that it is somehow related to representation.
- Why box ~R#? Couldn't castEqR just take an unboxed R equality?
I guesst castEqR could, but it seems I still need a TyCon that boxes ~R# so that it can be used as the type of a class method. (As mentioned, this TyCon could also be the TyCon of the class itself, I just need to find out how to wire that up.)
- If keeping boxed ~R#, you might want to add an ASSERT in mkEqReprBox ensuring that the coercion passed in has role R. (Use coercionRole.)
Will do.
- It looks like you plan to make the NT class more wired in (line 507 of TcEvidence). Would this get rid of the Class parameter to EvNT and then simplify mkNT?
Correct. The Class parameter is just a work-around for now, and mkNT and mkUnNT can simple be removed.
- getEqRolePredTys never seems to care about its Role return value. I'm happy about this, because the type-checker doesn't really know about roles. (It assumes everything is Nominal, which is how users would expect type-checking to behave, I think.)
That part of the patch is in the “I had to do this to make it work” because in some cases getRolePredTys would have thrown assertions about Representational roles appearing. If you think this is fine, the easiest would be to simply have getPredTys work with the different kinds of equalities. Also, that it currently works with NT should probably not be the final word.
- The changes in Coercion are correct -- the use of Nominal that you removed harkened to the days when all CoVars were Nominal.
Would you prefer to apply these changes to HEAD independently of the coercion feature? It would keep my patch cleaner.
After looking at it all, I wonder if shoehorning this feature into the class / instance mechanism is the right way to go. How much is that buying us? The instance lookup mechanism for NT is totally customized (as it should be, it seems). So, how much harder would it be to make this a free-floating feature, separate from classes? This would mean adding a new thing with kind (* -> * -> Constraint) to replace "NT". (In a perfect world, this could be spelled ≈, but I'm not a huge fan of Unicode syntax in reality.) But, there would be no need to worry about user-defined instances, and all the wired-in class stuff could be gotten rid of. It's not that I think the class/instance approach is that bad, but we've had to wander so far away from using GHC's built-in features around instance lookup that I think we should re-examine.
Thoughts?
This would move it closer to Eq and Eq#, right? I still don’t understand all of the code involved in constraint handling, especially with constraints that are not classes. I believe that it buys us the infrastructure of requesting new constraints, of solving constraints only once, and of getting an error message that looks familiar to the user. OTOH this infrastructure is not fully suited, e.g. for "newtype Void = Void Void" it creates looping EqR values. I’ll read through more of the code and see if we can do without classes alltogether. Thanks for your review, Joachim -- Joachim “nomeata” Breitner mail@joachim-breitner.de • http://www.joachim-breitner.de/ Jabber: nomeata@joachim-breitner.de • GPG-Key: 0x4743206C Debian Developer: nomeata@debian.org