The only reason for giving a role signature that is less permissive than
#9117: Coercible constraint solver misses one -------------------------------------+------------------------------------ Reporter: goldfire | Owner: nomeata Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by goldfire): Replying to [comment:10 simonpj]: the actual newtype-unwrapping is, well, to be more restrictive. So I think it'd be rather unusual both to give a role signature, and to expose the data constructor of the newtype. So I'm not too bothered about this particular dead end. Actually, fixing this adds a nice feature to this whole area: the ability to have free conversions within a library but not to export this capability! If we have a newtype with a nominal role annotation, its constructor might be visible only among "friendly" modules, allowing the free conversion. Then, outside of the package, the constructor is inaccessible, so no conversions are possible. This ability was a desideratum at the beginning of the design process that we thought we threw away when we went with the idea of using class instances. But, now we have it back!
But still, yes, putting the rules in the other order would be a good idea. (Make sure you add a `Note`!) I'm a bit bugged that `Coercible (N Age) (N Int)` might take a rather long way round (unwrapping multiple layers of newtype) rather than the short cut (try `(Coercible Age Int)`). But maybe I should not worry about that.
You shouldn't worry about that. :) I conjecture that coercion optimization ''already'' fixes this problem. (See uses of `matchAxiom` in !OptCoercion.)
As to the "knowing more later" stuff, I'm just referring to situations
like `(alpha t1) ~ (alpha t2)` where `alpha` is a unification variable. As constraint solving progresses we may learn what `alpha` is -- but if we have already decomposed the application it may now be too late. It's difficult to use the approach that Richard describes, because it interacts with all the other constraint solving that is going on during type inference. Ah. Good point. I hadn't thought of it that way. You're right -- we need to be careful here. But, if #9123 gets solved in the way that we're thinking of solving it now, we will want the functionality originally requested in this ticket available. So, it may be worth doing some Hard Thinking about this and getting it right. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9117#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler