[GHC] #15546: Display coaxiom branch incompatibilities in GHCi

[GHC]

#15546: Display coaxiom branch incompatibilities in GHCi
-------------------------------------+-------------------------------------
        Reporter:  mniip             |                Owner:  (none)
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:  8.6.1
       Component:  GHCi              |              Version:  8.4.3
      Resolution:                    |             Keywords:  TypeFamilies,
                                     |  GHCi
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 mniip):

 The other (actually this) day I discovered that type family compatibility
 checks do not reduce the LHS and expect the equality to trivially hold.
 Example:

 {{{#!hs
 type family If (a :: Bool) (b :: k) (c :: k) :: k where
     If False a b = b
     If True a b = a

 type family Eql (a :: k) (b :: k) :: Bool where
     Eql a a = True
     Eql _ _ = False

 type family Test (a :: Maybe k) (b :: Maybe k) :: Maybe k where
     Test (Just x) (Just y) = If (Eql x y) (Just x) Nothing
     Test a a = a
     Test Nothing _ = Nothing
     Test _ Nothing = Nothing
 }}}
 {{{#!hs
   axiom D:R:Test::
       Test a ('Just x) ('Just y) = If (Eql x y) ('Just x) 'Nothing
       Test k a a = a
       (incompatible indices: [0])
       Test k 'Nothing _ = 'Nothing
       Test k _ 'Nothing = 'Nothing
 }}}

 Clearly `unify(<a, a>, <Just x, Just y>) = theta = [a = Just x, y = x]`.

 `theta(If (Eql x y) (Just x) Nothing) = Just x = theta(a)`.

 If you would like to discuss this restriction I can open another ticket.

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