[GHC] #9117: Coercible constraint solver misses one

[GHC]

#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 only reason for giving a role signature that is less permissive than
 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