#15546: Display coaxiom branch incompatibilities in GHCi -------------------------------------+------------------------------------- Reporter: mniip | Owner: mniip 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): Phab:D5097 Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Compatibility is a user-facing issue. See [https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts... #compatibility-and-apartness-of-type-family-equations the manual]. Here is an example: {{{#!hs type family b1 && b2 where True && b2 = b2 False && b2 = False b1 && True = b1 b2 && False = False b && b = b }}} {{{ λ> :kind! forall b. b && True forall b. b && True :: Bool = b }}} Note that the first two equations unify with the target `b && True`. Normally, this means that any later equations wouldn't apply. But because the first two equations are both compatible with the third, we don't let the fact that they unify hold up reduction via the third equation, as we can see. I thus agree that the ability to print out incompatibilities is sometimes helpful for users, not just implementors. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15546#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler