diff options
| author | mniip <mniip@mniip.com> | 2019-01-20 20:48:13 -0500 |
|---|---|---|
| committer | Ben Gamari <ben@smart-cactus.org> | 2019-03-08 10:49:27 -0500 |
| commit | 99eac8cc12e7c7db64924c80455e3fdee8dd10b8 (patch) | |
| tree | 5258a9684169579f941cce1abd6d17a2849199a0 /docs | |
| parent | 068b7e983f4a0b35f453aa5e609998efd0c3f334 (diff) | |
| download | haskell-wip/D5097.tar.gz | |
Add a -fprint-axiom-incomps option (#15546)wip/D5097
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
Diffstat (limited to 'docs')
| -rw-r--r-- | docs/users_guide/glasgow_exts.rst | 3 | ||||
| -rw-r--r-- | docs/users_guide/using.rst | 31 |
2 files changed, 34 insertions, 0 deletions
diff --git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst index 67be116ae4..55562f863c 100644 --- a/docs/users_guide/glasgow_exts.rst +++ b/docs/users_guide/glasgow_exts.rst @@ -7921,6 +7921,9 @@ other hand, the two equations are compatible. Thus, GHC can ignore the first equation when looking at the second. So, ``G a`` will simplify to ``a``. +Incompatibilities between closed type family equations can be displayed +in :ghci-cmd:`:info` when :ghc-flag:`-fprint-axiom-incomps` is enabled. + However see :ref:`ghci-decls` for the overlap rules in GHCi. .. _type-family-decidability: diff --git a/docs/users_guide/using.rst b/docs/users_guide/using.rst index d11dedfb9a..b9dc114ae0 100644 --- a/docs/users_guide/using.rst +++ b/docs/users_guide/using.rst @@ -842,6 +842,37 @@ messages and in GHCi: kinds, GHC uses type-level coercions. Users will rarely need to see these, as they are meant to be internal. +.. ghc-flag:: -fprint-axiom-incomps + :shortdesc: Display equation incompatibilities in closed type families + :type: dynamic + :reverse: -fno-print-axiom-incomps + :category: verbosity + + Using :ghc-flag:`-fprint-axiom-incomps` tells GHC to display + incompatibilities between closed type families' equations, whenever they + are printed by :ghci-cmd:`:info` or :ghc-flag:`--show-iface ⟨file⟩`. + + .. code-block:: none + + ghci> :i Data.Type.Equality.== + type family (==) (a :: k) (b :: k) :: Bool + where + (==) (f a) (g b) = (f == g) && (a == b) + (==) a a = 'True + (==) _1 _2 = 'False + ghci> :set -fprint-axiom-incomps + ghci> :i Data.Type.Equality.== + type family (==) (a :: k) (b :: k) :: Bool + where + (==) (f a) (g b) = (f == g) && (a == b) + (==) a a = 'True + -- incompatible indices: 0 + (==) _1 _2 = 'False + -- incompatible indices: 1, 0 + + The comment after each equation refers to the indices (0-indexed) of + preceding equations it is incompatible with. + .. ghc-flag:: -fprint-equality-relations :shortdesc: Distinguish between equality relations when printing :type: dynamic |