#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(