#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