Commit 3d32286d authored by mniip's avatar mniip Committed by Marge Bot

Explicitly number equations when printing axiom incompatibilities

parent bca79345
......@@ -67,7 +67,7 @@ import Binary
import BooleanFormula ( BooleanFormula, pprBooleanFormula, isTrue )
import Var( VarBndr(..), binderVar )
import TyCon ( Role (..), Injectivity(..), tyConBndrVisArgFlag )
import Util( dropList, filterByList, notNull )
import Util( dropList, filterByList, notNull, unzipWith )
import DataCon (SrcStrictness(..), SrcUnpackedness(..))
import Lexeme (isLexSym)
......@@ -561,11 +561,11 @@ 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
{- #0 -} (==) (f a) (g b) = (f == g) && (a == b)
{- #1 -} (==) a a = 'True
-- incompatible with: #0
{- #2 -} (==) _1 _2 = 'False
-- incompatible with: #1, #0
The comment after an equation refers to all previous equations (0-indexed)
that are incompatible with it.
......@@ -576,7 +576,7 @@ that are incompatible with it.
************************************************************************
-}
pprAxBranch :: SDoc -> IfaceAxBranch -> SDoc
pprAxBranch :: SDoc -> BranchIndex -> IfaceAxBranch -> SDoc
-- The TyCon might be local (just an OccName), or this might
-- be a branch for an imported TyCon, so it would be an ExtName
-- So it's easier to take an SDoc here
......@@ -586,25 +586,31 @@ pprAxBranch :: SDoc -> IfaceAxBranch -> SDoc
-- in debug messages
-- in :info F for GHCi, which goes via toConToIfaceDecl on the family tycon
-- For user error messages we use Coercion.pprCoAxiom and friends
pprAxBranch pp_tc (IfaceAxBranch { ifaxbTyVars = tvs
, ifaxbCoVars = _cvs
, ifaxbLHS = pat_tys
, ifaxbRHS = rhs
, ifaxbIncomps = incomps })
pprAxBranch pp_tc idx (IfaceAxBranch { ifaxbTyVars = tvs
, ifaxbCoVars = _cvs
, ifaxbLHS = pat_tys
, ifaxbRHS = rhs
, ifaxbIncomps = incomps })
= WARN( not (null _cvs), pp_tc $$ ppr _cvs )
hang ppr_binders 2 (hang pp_lhs 2 (equals <+> ppr rhs))
$+$
nest 6 maybe_incomps
nest 4 maybe_incomps
where
-- See Note [Printing foralls in type family instances] in IfaceType
ppr_binders = pprUserIfaceForAll $ map (mkIfaceForAllTvBndr Specified) tvs
ppr_binders = maybe_index <+>
pprUserIfaceForAll (map (mkIfaceForAllTvBndr Specified) tvs)
pp_lhs = hang pp_tc 2 (pprParendIfaceAppArgs pat_tys)
-- See Note [Displaying axiom incompatibilities]
maybe_index
= sdocWithDynFlags $ \dflags ->
ppWhen (gopt Opt_PrintAxiomIncomps dflags) $
text "{-" <+> (text "#" <> ppr idx) <+> text "-}"
maybe_incomps
= sdocWithDynFlags $ \dflags ->
ppWhen (gopt Opt_PrintAxiomIncomps dflags && notNull incomps) $
text "--" <+> text "incompatible indices:" <+> interpp'SP incomps
text "--" <+> text "incompatible with:"
<+> pprWithCommas (\incomp -> text "#" <> ppr incomp) incomps
instance Outputable IfaceAnnotation where
ppr (IfaceAnnotation target value) = ppr target <+> colon <+> ppr value
......@@ -887,11 +893,11 @@ pprIfaceDecl ss (IfaceFamily { ifName = tycon
= ppShowIface ss (text "built-in")
pp_branches (IfaceClosedSynFamilyTyCon (Just (ax, brs)))
= vcat (map (pprAxBranch
= vcat (unzipWith (pprAxBranch
(pprPrefixIfDeclBndr
(ss_how_much ss)
(occName tycon))
) brs)
) $ zip [0..] brs)
$$ ppShowIface ss (text "axiom" <+> ppr ax)
pp_branches _ = Outputable.empty
......@@ -927,7 +933,7 @@ pprIfaceDecl ss (IfaceId { ifName = var, ifType = ty,
pprIfaceDecl _ (IfaceAxiom { ifName = name, ifTyCon = tycon
, ifAxBranches = branches })
= hang (text "axiom" <+> ppr name <+> dcolon)
2 (vcat $ map (pprAxBranch (ppr tycon)) branches)
2 (vcat $ unzipWith (pprAxBranch (ppr tycon)) $ zip [0..] branches)
pprCType :: Maybe CType -> SDoc
pprCType Nothing = Outputable.empty
......
......@@ -843,14 +843,14 @@ messages and in GHCi:
ghci> :i Data.Type.Equality.==
type family (==) (a :: k) (b :: k) :: Bool
where
(==) (f a) (g b) = (f == g) && (a == b)
(==) a a = 'True
{- #0 -} (==) (f a) (g b) = (f == g) && (a == b)
{- #1 -} (==) a a = 'True
-- incompatible indices: 0
(==) _1 _2 = 'False
{- #2 -} (==) _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.
The equations are numbered starting from 0, and the comment after each
equation refers to all preceding equations it is incompatible with.
.. ghc-flag:: -fprint-equality-relations
:shortdesc: Distinguish between equality relations when printing
......
......@@ -3,7 +3,7 @@ type family E a b :: * where
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
{- #0 -} E a a = ()
{- #1 -} E a b = Bool
-- incompatible with: #0
-- Defined at <interactive>:2:1
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