[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 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.  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.

 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.

 NB that this "more info later" stuff does not apply to the reordering to
 apply newtype unwrapping before decomposition, because both newtype
 unwrapping and decomposition apply only when the head is a known type
 constructor.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9117#comment:10>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler