[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
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 This is by design.  You are expecting `T Int` and `T Bool` to be
 representationally equal because
 if you look at every field of every constructor of `T`, and reduce every
 type-family application
 therein, on the particular argument types `Int` and `Bool`, then the
 answers are reprsentationally
 equal.  Quite true!  But this could be laborious if `T` had many
 constructors
 {{{
 data T a = T1 (X a )
          | T2 [Y a] (Z [a])
          ..etc...
 }}}
 If you add `type instance X Char = Char`, then certainly `T Int` is not
 coercible to `T Char`,
 so that check would have to be done for every individual instantation --
 and recursively so.

 Instead, the type system analyses the data type declaration for `T`
 computes a single summary -- the "role signature" of `T` --that decides,
 one and for all,
 when `(T t1)` is representationally equal to
 `T t2`.

 In this case, because of the possibility of `type instance T Char = Char`,
 the decision is
 that `T t1` is coercible to `T t2` only if `t1` is (nominally) equal to
 `t2`.


 [https://www.microsoft.com/en-us/research/publication/safe-coercions/ The
 paper] explains all this in some details.  I don't see a decently feasibly
 way to fix this, I'm afraid.

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