[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:5 nomeata]:
 > we don’t run into dead ends if we do on or the other first.

 I don't agree here. Say we have

 {{{
 newtype Phant a = MkPhant Char
 type role Phant representational

 ex1 :: Phant Bool
 ex1 = coerce (MkPhant 'x' :: Phant Int)
 }}}

 This should succeed if we use newtype-unwrapping instances first but
 should fail if we use the congruence case first. And, indeed, it fails! I
 think it should succeed. Regardless of what we decide to do about the
 original feature requested, I think the failure of this example is a
 proper bug.

 I believe that if we try the newtype-unwrapping instances first, the
 algorithm would be sound. Why? Because the congruence case can never be
 more powerful than the newtype-unwrapping case, due to role inference.
 That is, the roles on any type parameters of the newtype can never be more
 permissive than the roles on its representation type.

 So, we actually ''already'' have an ordering dependence on the cases, in
 order to avoid dead ends -- but we didn't realize it! Is there a problem
 with adding one more layer to this? :)  For use cases, see
 [https://github.com/ekmett/roles/blob/master/src/Data/Roles.hs here], some
 experimentation Edward K has done regarding tracking roles in type
 variables. He has to use `eta` in a fair number of constructions. Fixing
 the original ticket would allow these to be proven sound instead of
 relying on `unsafeCoerce`.

 And, in response to Simon, yes that's true that the situation might
 change, but I don't see how that's problematic. These instances are
 intentionally "incoherent", so we are robust in the presence of a change
 in exactly ''how'' the instance is solved for.  The "changed situation"
 shouldn't make a previously-allowable coercion become otherwise.

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