Commit 2073745c authored by mniip's avatar mniip Committed by Marge Bot

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
parent 6f116005
......@@ -47,6 +47,7 @@ import IfaceType
import BinFingerprint
import CoreSyn( IsOrphan, isOrphan )
import PprCore() -- Printing DFunArgs
import DynFlags( gopt, GeneralFlag (Opt_PrintAxiomIncomps) )
import Demand
import Class
import FieldLabel
......@@ -66,7 +67,7 @@ import Binary
import BooleanFormula ( BooleanFormula, pprBooleanFormula, isTrue )
import Var( VarBndr(..), binderVar )
import TyCon ( Role (..), Injectivity(..), tyConBndrVisArgFlag )
import Util( dropList, filterByList )
import Util( dropList, filterByList, notNull )
import DataCon (SrcStrictness(..), SrcUnpackedness(..))
import Lexeme (isLexSym)
......@@ -545,6 +546,28 @@ to cross the separate compilation boundary.
In general we retain all info that is left by CoreTidy.tidyLetBndr, since
that is what is seen by importing module with --make
Note [Displaying axiom incompatibilities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
With -fprint-axiom-incomps we display which closed type family equations
are incompatible with which. This information is sometimes necessary
because GHC doesn't try equations in order: any equation can be used when
all preceding equations that are incompatible with it do not apply.
For example, the last "a && a = a" equation in Data.Type.Bool.&& is
actually compatible with all previous equations, and can reduce at any
time.
This is displayed as:
Prelude> :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 an equation refers to all previous equations (0-indexed)
that are incompatible with it.
************************************************************************
* *
......@@ -571,13 +594,17 @@ pprAxBranch pp_tc (IfaceAxBranch { ifaxbTyVars = tvs
= WARN( not (null _cvs), pp_tc $$ ppr _cvs )
hang ppr_binders 2 (hang pp_lhs 2 (equals <+> ppr rhs))
$+$
nest 2 maybe_incomps
nest 6 maybe_incomps
where
-- See Note [Printing foralls in type family instances] in IfaceType
ppr_binders = pprUserIfaceForAll $ map (mkIfaceForAllTvBndr Specified) tvs
pp_lhs = hang pp_tc 2 (pprParendIfaceAppArgs pat_tys)
maybe_incomps = ppUnless (null incomps) $ parens $
text "incompatible indices:" <+> ppr incomps
-- See Note [Displaying axiom incompatibilities]
maybe_incomps
= sdocWithDynFlags $ \dflags ->
ppWhen (gopt Opt_PrintAxiomIncomps dflags && notNull incomps) $
text "--" <+> text "incompatible indices:" <+> interpp'SP incomps
instance Outputable IfaceAnnotation where
ppr (IfaceAnnotation target value) = ppr target <+> colon <+> ppr value
......
......@@ -1804,33 +1804,30 @@ coAxiomToIfaceDecl ax@(CoAxiom { co_ax_tc = tycon, co_ax_branches = branches
where
branch_list = fromBranches branches
-- 2nd parameter is the list of branch LHSs, for conversion from incompatible branches
-- to incompatible indices
-- 2nd parameter is the list of branch LHSs, in case of a closed type family,
-- for conversion from incompatible branches to incompatible indices.
-- For an open type family the list should be empty.
-- See Note [Storing compatibility] in CoAxiom
coAxBranchToIfaceBranch :: TyCon -> [[Type]] -> CoAxBranch -> IfaceAxBranch
coAxBranchToIfaceBranch tc lhs_s
branch@(CoAxBranch { cab_incomps = incomps })
= (coAxBranchToIfaceBranch' tc branch) { ifaxbIncomps = iface_incomps }
(CoAxBranch { cab_tvs = tvs, cab_cvs = cvs
, cab_eta_tvs = eta_tvs
, cab_lhs = lhs, cab_roles = roles
, cab_rhs = rhs, cab_incomps = incomps })
= IfaceAxBranch { ifaxbTyVars = toIfaceTvBndrs tvs
, ifaxbCoVars = map toIfaceIdBndr cvs
, ifaxbEtaTyVars = toIfaceTvBndrs eta_tvs
, ifaxbLHS = toIfaceTcArgs tc lhs
, ifaxbRoles = roles
, ifaxbRHS = toIfaceType rhs
, ifaxbIncomps = iface_incomps }
where
iface_incomps = map (expectJust "iface_incomps"
. (flip findIndex lhs_s
. eqTypes)
. flip findIndex lhs_s
. eqTypes
. coAxBranchLHS) incomps
-- use this one for standalone branches without incompatibles
coAxBranchToIfaceBranch' :: TyCon -> CoAxBranch -> IfaceAxBranch
coAxBranchToIfaceBranch' tc (CoAxBranch { cab_tvs = tvs, cab_cvs = cvs
, cab_eta_tvs = eta_tvs
, cab_lhs = lhs
, cab_roles = roles, cab_rhs = rhs })
= IfaceAxBranch { ifaxbTyVars = toIfaceTvBndrs tvs
, ifaxbCoVars = map toIfaceIdBndr cvs
, ifaxbEtaTyVars = toIfaceTvBndrs eta_tvs
, ifaxbLHS = toIfaceTcArgs tc lhs
, ifaxbRoles = roles
, ifaxbRHS = toIfaceType rhs
, ifaxbIncomps = [] }
-----------------
tyConToIfaceDecl :: TidyEnv -> TyCon -> (TidyEnv, IfaceDecl)
-- We *do* tidy TyCons, because they are not (and cannot
......@@ -1911,7 +1908,8 @@ tyConToIfaceDecl env tycon
to_if_fam_flav (ClosedSynFamilyTyCon (Just ax))
= IfaceClosedSynFamilyTyCon (Just (axn, ibr))
where defs = fromBranches $ coAxiomBranches ax
ibr = map (coAxBranchToIfaceBranch' tycon) defs
lhss = map coAxBranchLHS defs
ibr = map (coAxBranchToIfaceBranch tycon lhss) defs
axn = coAxiomName ax
ifaceConDecls (NewTyCon { data_con = con }) = IfNewTyCon (ifaceConDecl con)
......
......@@ -521,6 +521,7 @@ data GeneralFlag
| Opt_PrintExplicitCoercions
| Opt_PrintExplicitRuntimeReps
| Opt_PrintEqualityRelations
| Opt_PrintAxiomIncomps
| Opt_PrintUnicodeSyntax
| Opt_PrintExpandedSynonyms
| Opt_PrintPotentialInstances
......@@ -4235,6 +4236,7 @@ fFlagsDeps = [
flagSpec "print-explicit-coercions" Opt_PrintExplicitCoercions,
flagSpec "print-explicit-runtime-reps" Opt_PrintExplicitRuntimeReps,
flagSpec "print-equality-relations" Opt_PrintEqualityRelations,
flagSpec "print-axiom-incomps" Opt_PrintAxiomIncomps,
flagSpec "print-unicode-syntax" Opt_PrintUnicodeSyntax,
flagSpec "print-expanded-synonyms" Opt_PrintExpandedSynonyms,
flagSpec "print-potential-instances" Opt_PrintPotentialInstances,
......
......@@ -8047,6 +8047,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:
......
......@@ -821,6 +821,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
......
:set -XTypeFamilies
type family E a b where E a a = (); E a b = Bool
:info E
:set -fprint-axiom-incomps
:info E
type family E a b :: *
where
E a a = ()
E a b = Bool
-- Defined at <interactive>:2:1
type family E a b :: *
where
E a a = ()
E a b = Bool
-- incompatible indices: 0
-- Defined at <interactive>:2:1
......@@ -302,3 +302,4 @@ test('T16569', normal, ghci_script, ['T16569.script'])
test('T16767', normal, ghci_script, ['T16767.script'])
test('T16575', normal, ghci_script, ['T16575.script'])
test('T16804', extra_files(['T16804a.hs', 'T16804b.hs']), ghci_script, ['T16804.script'])
test('T15546', normal, ghci_script, ['T15546.script'])
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment