[GHC] #15546: Display coaxiom branch incompatibilities in GHCi
#15546: Display coaxiom branch incompatibilities in GHCi -------------------------------------+------------------------------------- Reporter: mniip | Owner: (none) Type: feature | Status: new request | Priority: normal | Milestone: 8.6.1 Component: GHCi | Version: 8.4.3 Keywords: TypeFamilies, | Operating System: Unknown/Multiple GHCi | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Currently the only way to figure out how GHC figured out compatibility of branches in a closed type family is to compile it to `.hi` and then sieve through `--show-iface` output. Something as simple this should suffice: {{{#!hs
:i == type family (==) (a :: k) (b :: k) :: Bool where (==) (f a) (g b) = (f == g) && (a == b) (==) a a = 'True -- incompatible with: 0 (==) _1 _2 = 'False -- incompatible with: 0, 1 -- Defined in ‘Data.Type.Equality’ infix 4 == }}}
-- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15546 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 simonpj): Isn't this incompatibility thing an implementation consideration? If so, we should not burden the user with it. By all means have a flag to augment :i with that info. We have a variety already: the blunderbus `-dppr-debug`, but also the more selective `-fprint-explicit-kinds` etc. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15546#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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): I'd say, even if rarely used, it's still a more important thing to be able to see than even `-fprint-explicit-kinds`, as `:i` will tell you any non- star kinds on its own anyway. But I don't insist. How about `-fprint-axiom-incomps`? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15546#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 simonpj):
How about -fprint-axiom-incomps?
Fine. When you say "more important to see" are you speaking about users or implementors? If the former, can you explain why they need to see this? They are just thinking "pick the first match" aren't they? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15546#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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(
#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 simonpj): I'm sorry I'm lost. What does "that type family compatibility checks do not reduce the LHS and expect the equality to trivially hold" mean? What is "this restriction"? What is illustrated by the example? Is it a bug? Thanks -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15546#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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): D5097 Wiki Page: | -------------------------------------+------------------------------------- Changes (by mniip): * owner: (none) => mniip * differential: => D5097 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15546#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: | -------------------------------------+------------------------------------- Changes (by mniip): * differential: D5097 => Phab:D5097 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15546#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 Simon Peyton Jones
#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
#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 simonpj):
I thus agree that the ability to print out incompatibilities is sometimes helpful for users, not just implementors.
OK, thanks. Now I understand. I agree. mnip: in the code, can you add a Note with an example of what the incompatibility stuff looks like when printed out; and some version of Richard's comments in comment:9 to explain why it might be useful for users to see this information? Also are the equations 0-indexed or 1-indexed? The Note, and the manual entry about the flag, should say. Also can you modify the manual section that Richard points to in comment:9 so that it mentions the existence of the flag to show compatibilities? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15546#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC