Opened 13 months ago

Last modified 7 weeks ago

#15546 new feature request

Display coaxiom branch incompatibilities in GHCi

Reported by: mniip Owned by: mniip
Priority: normal Milestone: 8.6.1
Component: GHCi Version: 8.4.3
Keywords: TypeFamilies, GHCi Cc:
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:

Description

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:

> :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 ==

Change History (11)

comment:1 Changed 13 months ago 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.

comment:2 Changed 13 months ago 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?

comment:3 Changed 13 months ago 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?

comment:4 Changed 13 months ago 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:

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
  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.

comment:5 Changed 13 months ago 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

comment:6 Changed 13 months ago by mniip

Differential Rev(s): D5097
Owner: set to mniip

comment:7 Changed 13 months ago by mniip

Differential Rev(s): D5097Phab:D5097

comment:8 Changed 13 months ago by Simon Peyton Jones <simonpj@…>

In 4b79329f/ghc:

Add comments about pretty-printing via IfaceSyn

Provoked by discussion on Phab:D5097 (Trac #15546), I'm adding
a big Note explaing the strategy of pretty-printing via IfaceSyn

comment:9 Changed 13 months ago by goldfire

Compatibility is a user-facing issue. See the manual. Here is an example:

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.

comment:10 Changed 13 months ago 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?

comment:11 Changed 7 weeks ago by Marge Bot <ben+marge-bot@…>

In 2073745c/ghc:

Add a -fprint-axiom-incomps option (#15546)

Supply branch incomps when building an IfaceClosedSynFamilyTyCon

`pprTyThing` now has access to incomps. This also causes them to be
written out to .hi files, but that doesn't pose an issue other than a
more faithful bijection between `tyThingToIfaceDecl` and `tcIfaceDecl`.

The machinery for displaying axiom incomps was already present but not
in use. Since this is now a thing that pops up in ghci's :info the
format was modified to look like a haskell comment.

Documentation and a test for the new feature included.

Test Plan: T15546

Reviewers: simonpj, bgamari, goldfire

Reviewed By: simonpj

Subscribers: rwbarton, carter

GHC Trac Issues: #15546

Differential Revision: https://phabricator.haskell.org/D5097
Note: See TracTickets for help on using tickets.