[Git][ghc/ghc][master] Fix bogus test in Lint
Marge Bot (@marge-bot)
gitlab at gitlab.haskell.org
Thu Dec 15 08:56:11 UTC 2022
Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC
Commits:
933d61a4 by Simon Peyton Jones at 2022-12-15T03:55:51-05:00
Fix bogus test in Lint
The Lint check for branch compatiblity within an axiom, in
GHC.Core.Lint.compatible_branches was subtly different to the
check made when contructing an axiom, in
GHC.Core.FamInstEnv.compatibleBranches.
The latter is correct, so I killed the former and am now using the
latter.
On the way I did some improvements to pretty-printing and documentation.
- - - - -
6 changed files:
- compiler/GHC/Core/Coercion.hs
- compiler/GHC/Core/Coercion/Axiom.hs
- compiler/GHC/Core/FamInstEnv.hs
- compiler/GHC/Core/Lint.hs
- + testsuite/tests/indexed-types/should_compile/T22547.hs
- testsuite/tests/indexed-types/should_compile/all.T
Changes:
=====================================
compiler/GHC/Core/Coercion.hs
=====================================
@@ -219,8 +219,8 @@ etaExpandCoAxBranch (CoAxBranch { cab_tvs = tvs
pprCoAxiom :: CoAxiom br -> SDoc
-- Used in debug-printing only
pprCoAxiom ax@(CoAxiom { co_ax_tc = tc, co_ax_branches = branches })
- = hang (text "axiom" <+> ppr ax <+> dcolon)
- 2 (vcat (map (pprCoAxBranchUser tc) (fromBranches branches)))
+ = hang (text "axiom" <+> ppr ax)
+ 2 (braces $ vcat (map (pprCoAxBranchUser tc) (fromBranches branches)))
pprCoAxBranchUser :: TyCon -> CoAxBranch -> SDoc
-- Used when printing injectivity errors (FamInst.reportInjectivityErrors)
@@ -254,8 +254,12 @@ ppr_co_ax_branch ppr_rhs fam_tc branch
[ pprUserForAll (mkForAllTyBinders Inferred bndrs')
-- See Note [Printing foralls in type family instances] in GHC.Iface.Type
, pp_lhs <+> ppr_rhs tidy_env ee_rhs
- , text "-- Defined" <+> pp_loc ]
+ , vcat [ text "-- Defined" <+> pp_loc
+ , ppUnless (null incomps) $ whenPprDebug $
+ text "-- Incomps:" <+> vcat (map (pprCoAxBranch fam_tc) incomps) ]
+ ]
where
+ incomps = coAxBranchIncomps branch
loc = coAxBranchSpan branch
pp_loc | isGoodSrcSpan loc = text "at" <+> ppr (srcSpanStart loc)
| otherwise = text "in" <+> ppr loc
=====================================
compiler/GHC/Core/Coercion/Axiom.hs
=====================================
@@ -39,7 +39,7 @@ import GHC.Prelude
import Language.Haskell.Syntax.Basic (Role(..))
import {-# SOURCE #-} GHC.Core.TyCo.Rep ( Type )
-import {-# SOURCE #-} GHC.Core.TyCo.Ppr ( pprType )
+import {-# SOURCE #-} GHC.Core.TyCo.Ppr ( pprType, pprTyVar )
import {-# SOURCE #-} GHC.Core.TyCon ( TyCon )
import GHC.Utils.Outputable
import GHC.Data.FastString
@@ -278,7 +278,6 @@ coAxiomArity ax index
= length tvs + length cvs
where
CoAxBranch { cab_tvs = tvs, cab_cvs = cvs } = coAxiomNthBranch ax index
-
coAxiomName :: CoAxiom br -> Name
coAxiomName = co_ax_name
@@ -334,7 +333,7 @@ placeHolderIncomps = panic "placeHolderIncomps"
Note [CoAxBranch type variables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In the case of a CoAxBranch of an associated type-family instance,
-we use the *same* type variables (where possible) as the
+we use the *same* type variables in cab_tvs (where possible) as the
enclosing class or instance. Consider
instance C Int [z] where
@@ -344,8 +343,11 @@ In the CoAxBranch in the instance decl (F Int [z]) we use the
same 'z', so that it's easy to check that that type is the same
as that in the instance header.
-So, unlike FamInsts, there is no expectation that the cab_tvs
-are fresh wrt each other, or any other CoAxBranch.
+However, I believe that the cab_tvs of any CoAxBranch are distinct
+from the cab_tvs of other CoAxBranches in the same CoAxiom. This is
+important when checking for compatiblity and apartness; e.g. see
+GHC.Core.FamInstEnv.compatibleBranches. (The story seems a bit wobbly
+here, but it seems to work.)
Note [CoAxBranch roles]
~~~~~~~~~~~~~~~~~~~~~~~
@@ -461,6 +463,12 @@ See also:
* Note [RoughMap and rm_empty] for how this complicates the RoughMap implementation slightly.
-}
+{- *********************************************************************
+* *
+ Instances, especially pretty-printing
+* *
+********************************************************************* -}
+
instance Eq (CoAxiom br) where
a == b = getUnique a == getUnique b
a /= b = getUnique a /= getUnique b
@@ -468,9 +476,6 @@ instance Eq (CoAxiom br) where
instance Uniquable (CoAxiom br) where
getUnique = co_ax_unique
-instance Outputable (CoAxiom br) where
- ppr = ppr . getName
-
instance NamedThing (CoAxiom br) where
getName = co_ax_name
@@ -480,13 +485,22 @@ instance Typeable br => Data.Data (CoAxiom br) where
gunfold _ _ = error "gunfold"
dataTypeOf _ = mkNoRepType "CoAxiom"
+instance Outputable (CoAxiom br) where
+ -- You may want GHC.Core.Coercion.pprCoAxiom instead
+ ppr = ppr . getName
+
instance Outputable CoAxBranch where
- ppr (CoAxBranch { cab_loc = loc
- , cab_lhs = lhs
- , cab_rhs = rhs }) =
- text "CoAxBranch" <+> parens (ppr loc) <> colon
- <+> brackets (pprWithCommas pprType lhs)
- <+> text "=>" <+> pprType rhs
+ -- This instance doesn't know the name of the type family
+ -- If possible, use GHC.Core.Coercion.pprCoAxBranch instead
+ ppr (CoAxBranch { cab_tvs = tvs, cab_cvs = cvs
+ , cab_lhs = lhs_tys, cab_rhs = rhs, cab_incomps = incomps })
+ = text "CoAxBranch" <+> braces payload
+ where
+ payload = hang (text "forall" <+> pprWithCommas pprTyVar (tvs ++ cvs) <> dot)
+ 2 (vcat [ text "<tycon>" <+> sep (map pprType lhs_tys)
+ , nest 2 (text "=" <+> ppr rhs)
+ , ppUnless (null incomps) $
+ text "incomps:" <+> vcat (map ppr incomps) ])
{-
************************************************************************
=====================================
compiler/GHC/Core/FamInstEnv.hs
=====================================
@@ -24,7 +24,7 @@ module GHC.Core.FamInstEnv (
FamInstMatch(..),
lookupFamInstEnv, lookupFamInstEnvConflicts, lookupFamInstEnvByTyCon,
- isDominatedBy, apartnessCheck,
+ isDominatedBy, apartnessCheck, compatibleBranches,
-- Injectivity
InjectivityCheckResult(..),
@@ -534,15 +534,16 @@ fails anyway.
compatibleBranches :: CoAxBranch -> CoAxBranch -> Bool
compatibleBranches (CoAxBranch { cab_lhs = lhs1, cab_rhs = rhs1 })
(CoAxBranch { cab_lhs = lhs2, cab_rhs = rhs2 })
- = let (commonlhs1, commonlhs2) = zipAndUnzip lhs1 lhs2
- -- See Note [Compatibility of eta-reduced axioms]
- in case tcUnifyTysFG alwaysBindFun commonlhs1 commonlhs2 of
- SurelyApart -> True
- Unifiable subst
- | Type.substTyAddInScope subst rhs1 `eqType`
- Type.substTyAddInScope subst rhs2
- -> True
- _ -> False
+ = case tcUnifyTysFG alwaysBindFun commonlhs1 commonlhs2 of
+ -- Here we need the cab_tvs of the two branches to be disinct.
+ -- See Note [CoAxBranch type variables] in GHC.Core.Coercion.Axiom.
+ SurelyApart -> True
+ MaybeApart {} -> False
+ Unifiable subst -> Type.substTyAddInScope subst rhs1 `eqType`
+ Type.substTyAddInScope subst rhs2
+ where
+ (commonlhs1, commonlhs2) = zipAndUnzip lhs1 lhs2
+ -- See Note [Compatibility of eta-reduced axioms]
-- | Result of testing two type family equations for injectiviy.
data InjectivityCheckResult
@@ -597,7 +598,7 @@ computeAxiomIncomps branches
where
go :: [CoAxBranch] -> CoAxBranch -> ([CoAxBranch], CoAxBranch)
go prev_brs cur_br
- = (cur_br : prev_brs, new_br)
+ = (new_br : prev_brs, new_br)
where
new_br = cur_br { cab_incomps = mk_incomps prev_brs cur_br }
=====================================
compiler/GHC/Core/Lint.hs
=====================================
@@ -54,6 +54,7 @@ import GHC.Core.TyCo.FVs
import GHC.Core.TyCo.Ppr
import GHC.Core.TyCon as TyCon
import GHC.Core.Coercion.Axiom
+import GHC.Core.FamInstEnv( compatibleBranches )
import GHC.Core.Unify
import GHC.Core.Coercion.Opt ( checkAxInstCo )
import GHC.Core.Opt.Arity ( typeArity, exprIsDeadEnd )
@@ -2640,8 +2641,10 @@ lint_family_branch fam_tc br@(CoAxBranch { cab_tvs = tvs
; lintL (null cvs)
(text "Coercion variables bound in family axiom")
; forM_ incomps $ \ br' ->
- lintL (not (compatible_branches br br')) $
- text "Incorrect incompatible branch:" <+> ppr br' }
+ lintL (not (compatibleBranches br br')) $
+ hang (text "Incorrect incompatible branches:")
+ 2 (vcat [text "Branch:" <+> ppr br,
+ text "Bogus incomp:" <+> ppr br']) }
lint_axiom_group :: NonEmpty (CoAxiom Branched) -> LintM ()
lint_axiom_group (_ :| []) = return ()
@@ -2663,7 +2666,7 @@ lint_axiom_pair tc (ax1, ax2)
, Just br2@(CoAxBranch { cab_tvs = tvs2
, cab_lhs = lhs2
, cab_rhs = rhs2 }) <- coAxiomSingleBranch_maybe ax2
- = lintL (compatible_branches br1 br2) $
+ = lintL (compatibleBranches br1 br2) $
vcat [ hsep [ text "Axioms", ppr ax1, text "and", ppr ax2
, text "are incompatible" ]
, text "tvs1 =" <+> pprTyVars tvs1
@@ -2677,27 +2680,6 @@ lint_axiom_pair tc (ax1, ax2)
= addErrL (text "Open type family axiom has more than one branch: either" <+>
ppr ax1 <+> text "or" <+> ppr ax2)
-compatible_branches :: CoAxBranch -> CoAxBranch -> Bool
--- True <=> branches are compatible. See Note [Compatibility] in GHC.Core.FamInstEnv.
-compatible_branches (CoAxBranch { cab_tvs = tvs1
- , cab_lhs = lhs1
- , cab_rhs = rhs1 })
- (CoAxBranch { cab_tvs = tvs2
- , cab_lhs = lhs2
- , cab_rhs = rhs2 })
- = -- we need to freshen ax2 w.r.t. ax1
- -- do this by pretending tvs1 are in scope when processing tvs2
- let in_scope = mkInScopeSetList tvs1
- subst0 = mkEmptySubst in_scope
- (subst, _) = substTyVarBndrs subst0 tvs2
- lhs2' = substTys subst lhs2
- rhs2' = substTy subst rhs2
- in
- case tcUnifyTys alwaysBindFun lhs1 lhs2' of
- Just unifying_subst -> substTy unifying_subst rhs1 `eqType`
- substTy unifying_subst rhs2'
- Nothing -> True
-
{-
************************************************************************
* *
@@ -3325,33 +3307,8 @@ dumpLoc (InType ty)
dumpLoc (InCo co)
= (noSrcLoc, text "In the coercion" <+> quotes (ppr co))
dumpLoc (InAxiom ax)
- = (getSrcLoc ax_name, text "In the coercion axiom" <+> ppr ax_name <+> dcolon <+> pp_ax)
- where
- CoAxiom { co_ax_name = ax_name
- , co_ax_tc = tc
- , co_ax_role = ax_role
- , co_ax_branches = branches } = ax
- branch_list = fromBranches branches
-
- pp_ax
- | [branch] <- branch_list
- = pp_branch branch
-
- | otherwise
- = braces $ vcat (map pp_branch branch_list)
-
- pp_branch (CoAxBranch { cab_tvs = tvs
- , cab_cvs = cvs
- , cab_lhs = lhs_tys
- , cab_rhs = rhs_ty })
- = sep [ brackets (pprWithCommas pprTyVar (tvs ++ cvs)) <> dot
- , ppr (mkTyConApp tc lhs_tys)
- , text "~_" <> pp_role ax_role
- , ppr rhs_ty ]
-
- pp_role Nominal = text "N"
- pp_role Representational = text "R"
- pp_role Phantom = text "P"
+ = (getSrcLoc ax, hang (text "In the coercion axiom")
+ 2 (pprCoAxiom ax))
pp_binders :: [Var] -> SDoc
pp_binders bs = sep (punctuate comma (map pp_binder bs))
=====================================
testsuite/tests/indexed-types/should_compile/T22547.hs
=====================================
@@ -0,0 +1,10 @@
+{-# LANGUAGE TypeFamilies #-}
+module M where
+
+import Data.Kind (Type)
+
+data MP1 a = MP1 a
+
+type family Fixup (f :: Type) (g :: Type) :: Type where
+ Fixup f (MP1 f) = Int
+ Fixup f f = f
=====================================
testsuite/tests/indexed-types/should_compile/all.T
=====================================
@@ -305,3 +305,4 @@ test('T14111', normal, compile, ['-O'])
test('T19336', normal, compile, ['-O'])
test('T11715b', normal, ghci_script, ['T11715b.script'])
test('T4254', normal, compile, [''])
+test('T22547', normal, compile, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/933d61a44a9409bf0d4bff0cceca1f02f48da4dd
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/933d61a44a9409bf0d4bff0cceca1f02f48da4dd
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20221215/af817a77/attachment-0001.html>
More information about the ghc-commits
mailing list