[GHC] #15683: coerce fails for Coercible type families

[GHC]

#15683: coerce fails for Coercible type families
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.6.1
       Component:  Compiler          |              Version:  8.6.1
      Resolution:                    |             Keywords:  TypeFamilies,
                                     |  Coercible
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by goldfire):

 * keywords:  TypeFamilies => TypeFamilies, Coercible
 * related:  #8177 =>


Comment:

 I'm afraid I disagree with comment:4. That's a related concern, but
 different.

 I think the solution to this problem is to have a ''lattice'' of roles.
 When we say, e.g., `type role T nominal representational phantom`, what we
 mean is:

 * `T a b c` is representationally equal to `T d e f` if `a` is nominally
 equal to `d`, `b` is representationally equal to `e`, and `c` is phantomly
 equal to `f`.

 What you want to say here is

 * `X a` is representationally equal to `X b` if `F a` is
 representationally equal to `F b`.

 We can imagine something like `type role X representational(F)` that means
 the phrase above. This could be checked easily. But it would need to come
 with a theory of GHC core for which we can prove type safety -- not a low
 bar.

 So, it's conceivable that some research could produce what you want, but
 it's out of reach for now.

 Note that this is ''not'' an infelicity of the solver, but an infelicity
 of the theory. (By contrast, #8177 is "just engineering" -- I don't think
 we'd need a new formal proof of safety to do it.)

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