[Git][ghc/ghc][wip/T24978] 2 commits: Wibbles ...
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Mon Jul 22 12:40:25 UTC 2024
Simon Peyton Jones pushed to branch wip/T24978 at Glasgow Haskell Compiler / GHC
Commits:
8af8bff1 by Simon Peyton Jones at 2024-07-22T08:22:41+01:00
Wibbles ...
...including omitting parens around atomic coercion
- - - - -
8119c093 by Simon Peyton Jones at 2024-07-22T13:40:05+01:00
Wibbles
- - - - -
10 changed files:
- compiler/GHC/Builtin/Types/Literals.hs
- compiler/GHC/Core/Coercion.hs
- compiler/GHC/Core/Coercion/Axiom.hs
- compiler/GHC/Core/FVs.hs
- compiler/GHC/Core/Lint.hs
- compiler/GHC/Core/Rules.hs
- compiler/GHC/Core/TyCo/FVs.hs
- compiler/GHC/Core/Type.hs
- compiler/GHC/Iface/Type.hs
- testsuite/tests/pmcheck/should_compile/T11195.hs
Changes:
=====================================
compiler/GHC/Builtin/Types/Literals.hs
=====================================
@@ -139,6 +139,7 @@ There are a few steps to adding a built-in type family:
tryInteractTopFam :: BuiltInSynFamily -> TyCon -> [Type] -> Type
-> [(CoAxiomRule, TypeEqn)]
+-- The returned CoAxiomRule is always unary
tryInteractTopFam fam fam_tc tys r
= [(BuiltInFamInteract ax_rule, eqn_out)
| ax_rule <- sfInteract fam
=====================================
compiler/GHC/Core/Coercion.hs
=====================================
@@ -2496,7 +2496,7 @@ coercion_lr_kind which orig_co
go_app co args = piResultTys (go co) args
-------------
- go_ax axr@(BuiltInFamRewrite bif) cos = check_bif_res axr (bifrw_proves bif (map coercionKind cos))
+ go_ax axr@(BuiltInFamRewrite bif) cos = check_bif_res axr (bifrw_proves bif (map coercionKind cos))
go_ax axr@(BuiltInFamInteract bif) [co] = check_bif_res axr (bifint_proves bif (coercionKind co))
go_ax axr@(BuiltInFamInteract {}) _ = crash axr
go_ax (UnbranchedAxiom ax) cos = go_branch ax (coAxiomSingleBranch ax) cos
=====================================
compiler/GHC/Core/Coercion/Axiom.hs
=====================================
@@ -567,8 +567,8 @@ instance Binary Role where
* *
************************************************************************
-A CoAxiomRule is a built-in axiom for a built-in type family.
-CoAxiomRules come in two flavours:
+A CoAxiomRule is a built-in axiom, one that we assume to be true:
+CoAxiomRules come in four flavours:
* BuiltInFamRewrite: provides evidence for, say
(ax1) 3+4 ----> 7
@@ -582,24 +582,43 @@ CoAxiomRules come in two flavours:
* BuiltInFamInteract: provides evidence for the consequences of one or two
other coercions. For example
- (ax3) g1: a+b ~ 0 ---> a~0
- (ax4) g2: a+b ~ 0 ---> b~0
- (ax5) g3: a+b1~r1, g4 : a+b2~r ---> b1~b2
- The arguments to the AxiomCo are the full coercions
- (not types, right from the get-go).
+ (ax3) g1: a+b ~ 0 ---> a~0
+ (ax4) g2: a+b ~ 0 ---> b~0
+ (ax5) g3: a+b1 ~ a~b2 ---> b1~b2
+ The argument to the AxiomCo is the full coercion (always just one).
So then:
- AxiomCo ax3 [g1] :: a ~ 0
- AxiomCo ax4 [g2] :: b ~ 0
- AxiomCo ax5 [g3,g4] :: b1 ~ b2
-
+ AxiomCo ax3 [g1] :: a ~ 0
+ AxiomCo ax4 [g2] :: b ~ 0
+ AxiomCo ax5 [g3] :: b1 ~ b2
+
+* BranchedAxiom: used for closed type families
+ type family F a where
+ F Int = Bool
+ F Bool = Char
+ F a = a -> Int
+ We get one (CoAxiom Branched) for the entire family; when used in an
+ AxiomCo we pair it with the BranchIndex to say which branch to pick.
+
+* UnbranchedAxiom: used for several purposes;
+ - Newtypes
+ - Data family instances
+ - Open type family instances
-}
--- | CoAxiomRule is a sum type that joins BuiltInFamRewrite and BuiltInFamInteract
+-- | CoAxiomRule describes a built-in axiom, one that we assume to be true
data CoAxiomRule
- = BuiltInFamRewrite BuiltInFamRewrite
- | BuiltInFamInteract BuiltInFamInteract
- | BranchedAxiom (CoAxiom Branched) BranchIndex
- | UnbranchedAxiom (CoAxiom Unbranched)
+ = BuiltInFamRewrite BuiltInFamRewrite -- Built-in type-family rewrites
+ -- e.g. 3+5 ~ 7
+
+ | BuiltInFamInteract BuiltInFamInteract -- Built-in type-family deductions
+ -- e.g. a+b~0 ==> a~0
+ -- Always unary
+
+ | BranchedAxiom (CoAxiom Branched) BranchIndex -- Closed type family
+
+ | UnbranchedAxiom (CoAxiom Unbranched) -- Open type family instance,
+ -- data family instances
+ -- and newtypes
instance Eq CoAxiomRule where
(BuiltInFamRewrite bif1) == (BuiltInFamRewrite bif2) = bifrw_name bif1 == bifrw_name bif2
@@ -666,10 +685,10 @@ data BuiltInFamInteract -- Argument and result role are always Nominal
= BIF_Interact
{ bifint_name :: FastString
, bifint_proves :: TypeEqn -> Maybe TypeEqn
- -- ^ Returns @Nothing@ when it doesn't like
- -- the supplied arguments. When this happens in a coercion
- -- that means that the coercion is ill-formed, and Core Lint
- -- checks for that.
+ -- ^ Always unary: just one TypeEqn argument
+ -- Returns @Nothing@ when it doesn't like the supplied argument.
+ -- When this happens in a coercion that means that the coercion is
+ -- ill-formed, and Core Lint checks for that.
}
data BuiltInFamRewrite -- Argument roles and result role are always Nominal
@@ -693,7 +712,7 @@ data BuiltInFamRewrite -- Argument roles and result role are always Nominal
-- If Just (inst_tys, res_ty) = bifrw_match ax arg_tys
-- then * length arg_tys = tyConArity fam_tc
-- * length inst_tys = bifrw_arity
- -- * bifrw_proves (map mkNomReflCo inst_tys) = Just (mkNomReflCo res_ty)
+ -- * bifrw_proves (map (return @Pair) inst_tys) = Just (return @Pair res_ty)
-- Provides default implementations that do nothing.
=====================================
compiler/GHC/Core/FVs.hs
=====================================
@@ -39,9 +39,8 @@ module GHC.Core.FVs (
exprFVs,
-- * Orphan names
- orphNamesOfType, orphNamesOfTypes,
- orphNamesOfCo, orphNamesOfAxiomLHS,
- exprsOrphNames,
+ orphNamesOfType, orphNamesOfTypes, orphNamesOfAxiomLHS,
+ orphNamesOfExprs,
-- * Core syntax tree annotation with free variables
FVAnn, -- annotation, abstract
@@ -291,53 +290,35 @@ tickish_fvs :: CoreTickish -> FV
tickish_fvs (Breakpoint _ _ ids _) = FV.mkFVs ids
tickish_fvs _ = emptyFV
-{-
-************************************************************************
-* *
-\section{Free names}
-* *
-************************************************************************
--}
-
--- | Finds the free /external/ names of an expression, notably
--- including the names of type constructors (which of course do not show
--- up in 'exprFreeVars').
-exprOrphNames :: CoreExpr -> NameSet
--- There's no need to delete local binders, because they will all
--- be /internal/ names.
-exprOrphNames e
- = go e
- where
- go (Var v)
- | isExternalName n = unitNameSet n
- | otherwise = emptyNameSet
- where n = idName v
- go (Lit _) = emptyNameSet
- go (Type ty) = orphNamesOfType ty -- Don't need free tyvars
- go (Coercion co) = orphNamesOfCo co
- go (App e1 e2) = go e1 `unionNameSet` go e2
- go (Lam v e) = go e `delFromNameSet` idName v
- go (Tick _ e) = go e
- go (Cast e co) = go e `unionNameSet` orphNamesOfCo co
- go (Let (NonRec _ r) e) = go e `unionNameSet` go r
- go (Let (Rec prs) e) = exprsOrphNames (map snd prs) `unionNameSet` go e
- go (Case e _ ty as) = go e `unionNameSet` orphNamesOfType ty
- `unionNameSet` unionNameSets (map go_alt as)
-
- go_alt (Alt _ _ r) = go r
-
--- | Finds the free /external/ names of several expressions: see 'exprOrphNames' for details
-exprsOrphNames :: [CoreExpr] -> NameSet
-exprsOrphNames es = foldr (unionNameSet . exprOrphNames) emptyNameSet es
-
-
{- **********************************************************************
%* *
- orphNamesXXX
-
+ Orphan names
%* *
%********************************************************************* -}
+{- Note [Finding orphan names]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The functions here (orphNamesOfType, orphNamesOfExpr etc) traverse a template:
+ * the head of an class instance decl
+ * the LHS of a type-family instance
+ * the arguments of a RULE
+to find TyCons or (in the case of a RULE) Ids, that will be matched against when
+matching the template. If none of these orphNames are locally defined, the instance
+or RULE is an orphan: see Note [Orphans] in GHC.Core
+
+Wrinkles:
+ (ON1) We do not need to look inside coercions, because we never match against
+ them. Indeed, it'd be wrong to do so, because it could make an instance
+ into a non-orphan, when it really is an orphan.
+
+ (ON2) These oprhNames functions are also (rather separately) used by GHCi, to
+ implement :info. When you say ":info Foo", we show all the instances that
+ involve `Foo`; that is, all the instances whose oprhNames include `Foo`.
+
+ To support `:info (->)` we need to ensure that (->) is treated as an orphName
+ of FunTy, which is a bit messy since the "real" TyCon is `FUN`
+-}
+
orphNamesOfTyCon :: TyCon -> NameSet
orphNamesOfTyCon tycon = unitNameSet (getName tycon) `unionNameSet` case tyConClass_maybe tycon of
Nothing -> emptyNameSet
@@ -350,6 +331,8 @@ orphNamesOfType (TyVarTy _) = emptyNameSet
orphNamesOfType (LitTy {}) = emptyNameSet
orphNamesOfType (ForAllTy bndr res) = orphNamesOfType (binderType bndr)
`unionNameSet` orphNamesOfType res
+orphNamesOfType (AppTy fun arg) = orphNamesOfType fun `unionNameSet` orphNamesOfType arg
+
orphNamesOfType (TyConApp tycon tys) = func
`unionNameSet` orphNamesOfTyCon tycon
`unionNameSet` orphNamesOfTypes tys
@@ -367,9 +350,9 @@ orphNamesOfType (FunTy af w arg res) = func
fun_tc = tyConName (funTyFlagTyCon af)
-orphNamesOfType (AppTy fun arg) = orphNamesOfType fun `unionNameSet` orphNamesOfType arg
-orphNamesOfType (CastTy ty co) = orphNamesOfType ty `unionNameSet` orphNamesOfCo co
-orphNamesOfType (CoercionTy co) = orphNamesOfCo co
+-- Coercions: see wrinkle (ON1) of Note [Finding orphan names]
+orphNamesOfType (CastTy ty _co) = orphNamesOfType ty
+orphNamesOfType (CoercionTy _co) = emptyNameSet
orphNamesOfThings :: (a -> NameSet) -> [a] -> NameSet
orphNamesOfThings f = foldr (unionNameSet . f) emptyNameSet
@@ -377,57 +360,6 @@ orphNamesOfThings f = foldr (unionNameSet . f) emptyNameSet
orphNamesOfTypes :: [Type] -> NameSet
orphNamesOfTypes = orphNamesOfThings orphNamesOfType
-orphNamesOfMCo :: MCoercion -> NameSet
-orphNamesOfMCo MRefl = emptyNameSet
-orphNamesOfMCo (MCo co) = orphNamesOfCo co
-
-orphNamesOfCo :: Coercion -> NameSet
-orphNamesOfCo (Refl ty) = orphNamesOfType ty
-orphNamesOfCo (GRefl _ ty mco) = orphNamesOfType ty `unionNameSet` orphNamesOfMCo mco
-orphNamesOfCo (TyConAppCo _ tc cos) = unitNameSet (getName tc) `unionNameSet` orphNamesOfCos cos
-orphNamesOfCo (AppCo co1 co2) = orphNamesOfCo co1 `unionNameSet` orphNamesOfCo co2
-orphNamesOfCo (ForAllCo { fco_kind = kind_co, fco_body = co })
- = orphNamesOfCo kind_co
- `unionNameSet` orphNamesOfCo co
-orphNamesOfCo (FunCo { fco_mult = co_mult, fco_arg = co1, fco_res = co2 })
- = orphNamesOfCo co_mult
- `unionNameSet` orphNamesOfCo co1
- `unionNameSet` orphNamesOfCo co2
-orphNamesOfCo (CoVarCo _) = emptyNameSet
-orphNamesOfCo (AxiomCo con cos) = orphNamesOfAxRule con `unionNameSet` orphNamesOfCos cos
-orphNamesOfCo (UnivCo { uco_lty = t1, uco_rty = t2, uco_deps = cos })
- = orphNamesOfType t1 `unionNameSet` orphNamesOfType t2
- `unionNameSet` orphNamesOfCos cos
-orphNamesOfCo (SymCo co) = orphNamesOfCo co
-orphNamesOfCo (TransCo co1 co2) = orphNamesOfCo co1 `unionNameSet` orphNamesOfCo co2
-orphNamesOfCo (SelCo _ co) = orphNamesOfCo co
-orphNamesOfCo (LRCo _ co) = orphNamesOfCo co
-orphNamesOfCo (InstCo co arg) = orphNamesOfCo co `unionNameSet` orphNamesOfCo arg
-orphNamesOfCo (KindCo co) = orphNamesOfCo co
-orphNamesOfCo (SubCo co) = orphNamesOfCo co
-orphNamesOfCo (HoleCo _) = emptyNameSet
-
-orphNamesOfCos :: [Coercion] -> NameSet
-orphNamesOfCos = orphNamesOfThings orphNamesOfCo
-
-orphNamesOfAxRule :: CoAxiomRule -> NameSet
-orphNamesOfAxRule (BuiltInFamRewrite bif) = unitNameSet (tyConName (bifrw_fam_tc bif))
-orphNamesOfAxRule (BuiltInFamInteract {}) = emptyNameSet -- A free-floating axiom
-orphNamesOfAxRule (UnbranchedAxiom ax) = orphNamesOfCoAx ax
-orphNamesOfAxRule (BranchedAxiom ax _) = orphNamesOfCoAx ax
-
-orphNamesOfCoAx :: CoAxiom br -> NameSet
-orphNamesOfCoAx (CoAxiom { co_ax_tc = tc, co_ax_branches = branches })
- = orphNamesOfTyCon tc `unionNameSet` orphNamesOfCoAxBranches branches
-
-orphNamesOfCoAxBranches :: Branches br -> NameSet
-orphNamesOfCoAxBranches
- = foldr (unionNameSet . orphNamesOfCoAxBranch) emptyNameSet . fromBranches
-
-orphNamesOfCoAxBranch :: CoAxBranch -> NameSet
-orphNamesOfCoAxBranch (CoAxBranch { cab_lhs = lhs, cab_rhs = rhs })
- = orphNamesOfTypes lhs `unionNameSet` orphNamesOfType rhs
-
-- | `orphNamesOfAxiomLHS` collects the names of the concrete types and
-- type constructors that make up the LHS of a type family instance,
-- including the family name itself.
@@ -442,12 +374,45 @@ orphNamesOfAxiomLHS axiom
= (orphNamesOfTypes $ concatMap coAxBranchLHS $ fromBranches $ coAxiomBranches axiom)
`extendNameSet` getName (coAxiomTyCon axiom)
--- Detect FUN 'Many as an application of (->), so that :i (->) works as expected
+-- Detect (FUN 'Many) as an application of (->), so that :i (->) works as expected
-- (see #8535) Issue #16475 describes a more robust solution
+-- See wrinkle (ON2) of Note [Finding orphan names]
orph_names_of_fun_ty_con :: Mult -> NameSet
orph_names_of_fun_ty_con ManyTy = unitNameSet unrestrictedFunTyConName
orph_names_of_fun_ty_con _ = emptyNameSet
+-- | Finds the free /external/ names of an expression, notably
+-- including the names of type constructors (which of course do not show
+-- up in 'exprFreeVars').
+orphNamesOfExpr :: CoreExpr -> NameSet
+-- There's no need to delete local binders, because they will all
+-- be /internal/ names.
+orphNamesOfExpr e
+ = go e
+ where
+ go (Var v)
+ | isExternalName n = unitNameSet n
+ | otherwise = emptyNameSet
+ where n = idName v
+ go (Lit _) = emptyNameSet
+ go (Type ty) = orphNamesOfType ty -- Don't need free tyvars
+ go (Coercion _co) = emptyNameSet -- See wrinkle (ON1) of Note [Finding orphan names]
+ go (App e1 e2) = go e1 `unionNameSet` go e2
+ go (Lam v e) = go e `delFromNameSet` idName v
+ go (Tick _ e) = go e
+ go (Cast e _co) = go e -- See wrinkle (ON1) of Note [Finding orphan names]
+ go (Let (NonRec _ r) e) = go e `unionNameSet` go r
+ go (Let (Rec prs) e) = orphNamesOfExprs (map snd prs) `unionNameSet` go e
+ go (Case e _ ty as) = go e `unionNameSet` orphNamesOfType ty
+ `unionNameSet` unionNameSets (map go_alt as)
+
+ go_alt (Alt _ _ r) = go r
+
+-- | Finds the free /external/ names of several expressions: see 'exprOrphNames' for details
+orphNamesOfExprs :: [CoreExpr] -> NameSet
+orphNamesOfExprs es = foldr (unionNameSet . orphNamesOfExpr) emptyNameSet es
+
+
{-
************************************************************************
* *
=====================================
compiler/GHC/Core/Lint.hs
=====================================
@@ -2467,11 +2467,16 @@ lintCoercion co@(FunCo { fco_role = r, fco_afl = afl, fco_afr = afr
, text "res_co:" <+> ppr co2 ])
-- See Note [Bad unsafe coercion]
-lintCoercion co@(UnivCo { uco_role = r
+lintCoercion co@(UnivCo { uco_role = r, uco_prov = prov
, uco_lty = ty1, uco_rty = ty2, uco_deps = deps })
- = do { ty1' <- lintType ty1
+ = do { -- Check the role. PhantomProv must have Phantom role, otherwise any role is fine
+ case prov of
+ PhantomProv -> lintRole co Phantom r
+ _ -> return ()
+
+ -- Check the to and from types
+ ; ty1' <- lintType ty1
; ty2' <- lintType ty2
- ; deps' <- mapM lintCoercion deps
; let k1 = typeKind ty1'
k2 = typeKind ty2'
@@ -2479,6 +2484,9 @@ lintCoercion co@(UnivCo { uco_role = r
&& isTYPEorCONSTRAINT k2)
(checkTypes ty1 ty2)
+ -- Check the coercions on which this UnivCo depends
+ ; deps' <- mapM lintCoercion deps
+
; return (co { uco_lty = ty1', uco_rty = ty2', uco_deps = deps' }) }
where
report s = hang (text $ "Unsafe coercion: " ++ s)
=====================================
compiler/GHC/Core/Rules.hs
=====================================
@@ -48,7 +48,7 @@ import GHC.Core -- All of it
import GHC.Core.Subst
import GHC.Core.SimpleOpt ( exprIsLambda_maybe )
import GHC.Core.FVs ( exprFreeVars, bindFreeVars
- , rulesFreeVarsDSet, exprsOrphNames )
+ , rulesFreeVarsDSet, orphNamesOfExprs )
import GHC.Core.Utils ( exprType, mkTick, mkTicks
, stripTicksTopT, stripTicksTopE
, isJoinBind, mkCastMCo )
@@ -207,7 +207,7 @@ mkRule this_mod is_auto is_local name act fn bndrs args rhs
-- Compute orphanhood. See Note [Orphans] in GHC.Core.InstEnv
-- A rule is an orphan only if none of the variables
-- mentioned on its left-hand side are locally defined
- lhs_names = extendNameSet (exprsOrphNames args) fn
+ lhs_names = extendNameSet (orphNamesOfExprs args) fn
-- Since rules get eventually attached to one of the free names
-- from the definition when compiling the ABI hash, we should make
=====================================
compiler/GHC/Core/TyCo/FVs.hs
=====================================
@@ -1098,6 +1098,21 @@ tyCoVarsOfTypesWellScoped = scopedSort . tyCoVarsOfTypesList
************************************************************************
-}
+{- Note [tyConsOfType]
+~~~~~~~~~~~~~~~~~~~~~~
+It is slightly odd to find the TyCons of a type. Especially since, via a type
+family reduction or axiom, a type that doesn't mention T might start to mention T.
+
+This function is used in only three places:
+* In GHC.Tc.Validity.validDerivPred, when identifying "exotic" predicates.
+* In GHC.Tc.Errors.Ppr.pprTcSolverReportMsg, when trying to print a helpful
+ error about overlapping instances
+* In utisl/dump-decls/Main.hs, an ill-documented module.
+
+None seem critical. Currently tyConsOfType looks inside coercions, but perhaps
+it doesn't even need to do that.
+-}
+
-- | All type constructors occurring in the type; looking through type
-- synonyms, but not newtypes.
-- When it finds a Class, it returns the class TyCon.
=====================================
compiler/GHC/Core/Type.hs
=====================================
@@ -255,7 +255,6 @@ import GHC.Core.TyCo.FVs
import GHC.Types.Var
import GHC.Types.Var.Env
import GHC.Types.Var.Set
-import GHC.Types.Unique.Set
import GHC.Core.TyCon
import GHC.Builtin.Types.Prim
@@ -2300,24 +2299,22 @@ buildSynTyCon name binders res_kind roles rhs
= mkSynonymTyCon name binders res_kind roles rhs
is_tau is_fam_free is_forgetful is_concrete
where
+ qtvs = mkVarSet (map binderVar binders)
is_tau = isTauTy rhs
is_fam_free = isFamFreeTy rhs
- is_concrete = uniqSetAll isConcreteTyCon rhs_tycons
- -- NB: is_concrete is allowed to be conservative, returning False
- -- more often than it could. e.g.
- -- type S a b = b
- -- type family F a
- -- type T a = S (F a) a
- -- We will mark T as not-concrete, even though (since S ignore its first
- -- argument, it could be marked concrete.
-
- is_forgetful = not (all ((`elemVarSet` rhs_tyvars) . binderVar) binders) ||
- uniqSetAny isForgetfulSynTyCon rhs_tycons
- -- NB: is_forgetful is allowed to be conservative, returning True more often
- -- than it should. See comments on GHC.Core.TyCon.isForgetfulSynTyCon
-
- rhs_tycons = tyConsOfType rhs
- rhs_tyvars = tyCoVarsOfType rhs
+ is_concrete = isConcreteTypeWith qtvs rhs
+
+ is_forgetful = not (qtvs `subVarSet` expanded_rhs_tyvars)
+ expanded_rhs_tyvars = tyCoVarsOfType (expandTypeSynonyms rhs)
+ -- See Note [Forgetful type synonyms] in GHC.Core.TyCon
+ -- To find out if this TyCon is forgetful, expand the synonyms in its RHS
+ -- and check that all of the binders are free in the expanded type.
+ -- We really only need to expand the /forgetful/ synonyms on the RHS,
+ -- but we don't currently have a function to do that.
+ -- Failing to expand the RHS led to #25094, e.g.
+ -- type Bucket a b c = Key (a,b,c)
+ -- type Key x = Any
+ -- Here Bucket is definitely forgetful!
{-
************************************************************************
@@ -2851,9 +2848,17 @@ isFixedRuntimeRepKind k
--
-- See Note [Concrete types] in GHC.Tc.Utils.Concrete.
isConcreteType :: Type -> Bool
-isConcreteType = go
+isConcreteType = isConcreteTypeWith emptyVarSet
+
+isConcreteTypeWith :: TyVarSet -> Type -> Bool
+-- See Note [Concrete types] in GHC.Tc.Utils.Concrete.
+-- For this "With" version we pass in a set of TyVars to be considered
+-- concrete. This supports mkSynonymTyCon, which needs to test the RHS
+-- for concreteness, under the assumption that the binders are instantiated
+-- to concrete types
+isConcreteTypeWith conc_tvs = go
where
- go (TyVarTy tv) = isConcreteTyVar tv
+ go (TyVarTy tv) = isConcreteTyVar tv || tv `elemVarSet` conc_tvs
go (AppTy ty1 ty2) = go ty1 && go ty2
go (TyConApp tc tys) = go_tc tc tys
go ForAllTy{} = False
=====================================
compiler/GHC/Iface/Type.hs
=====================================
@@ -2014,7 +2014,8 @@ ppr_co ctxt_prec (IfaceInstCo co ty)
, pprParendIfaceCoercion ty ]
ppr_co ctxt_prec (IfaceAxiomCo ax cos)
- = ppr_special_co ctxt_prec (pprIfAxRule ax) cos
+ | null cos = pprIfAxRule ax -- Don't add parens
+ | otherwise = ppr_special_co ctxt_prec (pprIfAxRule ax) cos
ppr_co ctxt_prec (IfaceSymCo co)
= ppr_special_co ctxt_prec (text "Sym") [co]
ppr_co ctxt_prec (IfaceTransCo co1 co2)
=====================================
testsuite/tests/pmcheck/should_compile/T11195.hs
=====================================
@@ -54,9 +54,10 @@ etaForAllCo_maybe = undefined
matchAxiom = undefined
checkAxInstCo = undefined
-isAxiom_maybe = undefined
+isAxiomCo_maybe co1 = undefined
isCohLeft_maybe = undefined
isCohRight_maybe = undefined
+matchNewtypeBranch = undefined
opt_transList :: InScopeSet -> [NormalCo] -> [NormalCo] -> [NormalCo]
opt_transList is = zipWith (opt_trans is)
@@ -109,61 +110,53 @@ opt_trans_rule is co1 co2
| ForAllCo tv2 vl2 vr1 eta2 r2 <- co2
, Just (tv1,vl1,vr2,eta1,r1) <- etaForAllCo_maybe co1 = undefined
- where
- push_trans tv1 eta1 r1 tv2 eta2 r2 = undefined
-
-- Push transitivity inside axioms
opt_trans_rule is co1 co2
- | Just (sym, con, ind, cos1) <- co1_is_axiom_maybe
+ | Just (sym1, axr1, cos1) <- isAxiomCo_maybe co1
+ , Just (sym2, axr2, cos2) <- isAxiomCo_maybe co2
+ , axr1 == axr2
+ , sym1 == not sym2
+ , Just (tc, role, branch) <- coAxiomRuleBranch_maybe axr1
+ , let qtvs = coAxBranchTyVars branch ++ coAxBranchCoVars branch
+ lhs = mkTyConApp tc (coAxBranchLHS branch)
+ rhs = coAxBranchRHS branch
+ pivot_tvs = exactTyCoVarsOfType (if sym2 then rhs else lhs)
+ , all (`elemVarSet` pivot_tvs) qtvs
+ = if sym2
+ -- TrPushAxSym
+ then liftCoSubstWith role qtvs (opt_transList is cos1 (map mkSymCo cos2)) lhs
+ -- TrPushSymAx
+ else liftCoSubstWith role qtvs (opt_transList is (map mkSymCo cos1) cos2) rhs
+
+ -- See Note [Push transitivity inside axioms] and
+ -- Note [Push transitivity inside newtype axioms only]
+ -- TrPushSymAxR
+ | Just (sym, axr, cos1) <- isAxiomCo_maybe co1
, True <- sym
- , Just cos2 <- matchAxiom sym con ind co2
- , let newAxInst = AxiomInstCo con ind
- (opt_transList is (map mkSymCo cos2) cos1)
- , Nothing <- checkAxInstCo newAxInst
- = undefined
+ , Just cos2 <- matchNewtypeBranch sym axr co2
+ , let newAxInst = AxiomCo axr (opt_transList is (map mkSymCo cos2) cos1)
+ = SymCo newAxInst
-- TrPushAxR
- | Just (sym, con, ind, cos1) <- co1_is_axiom_maybe
+ | Just (sym, axr, cos1) <- isAxiomCo_maybe co1
, False <- sym
- , Just cos2 <- matchAxiom sym con ind co2
- , let newAxInst = AxiomInstCo con ind (opt_transList is cos1 cos2)
- , Nothing <- checkAxInstCo newAxInst
- = undefined
+ , Just cos2 <- matchNewtypeBranch sym axr co2
+ , let newAxInst = AxiomCo axr (opt_transList is cos1 cos2)
+ = newAxInst
-- TrPushSymAxL
- | Just (sym, con, ind, cos2) <- co2_is_axiom_maybe
+ | Just (sym, axr, cos2) <- isAxiomCo_maybe co2
, True <- sym
- , Just cos1 <- matchAxiom (not sym) con ind co1
- , let newAxInst = AxiomInstCo con ind
- (opt_transList is cos2 (map mkSymCo cos1))
- , Nothing <- checkAxInstCo newAxInst
- = undefined
+ , Just cos1 <- matchNewtypeBranch (not sym) axr co1
+ , let newAxInst = AxiomCo axr (opt_transList is cos2 (map mkSymCo cos1))
+ = SymCo newAxInst
-- TrPushAxL
- | Just (sym, con, ind, cos2) <- co2_is_axiom_maybe
+ | Just (sym, axr, cos2) <- isAxiomCo_maybe co2
, False <- sym
- , Just cos1 <- matchAxiom (not sym) con ind co1
- , let newAxInst = AxiomInstCo con ind (opt_transList is cos1 cos2)
- , Nothing <- checkAxInstCo newAxInst
- = undefined
-
- -- TrPushAxSym/TrPushSymAx
- | Just (sym1, con1, ind1, cos1) <- co1_is_axiom_maybe
- , Just (sym2, con2, ind2, cos2) <- co2_is_axiom_maybe
- , con1 == con2
- , ind1 == ind2
- , sym1 == not sym2
- , let branch = coAxiomNthBranch con1 ind1
- qtvs = coAxBranchTyVars branch ++ coAxBranchCoVars branch
- lhs = coAxNthLHS con1 ind1
- rhs = coAxBranchRHS branch
- pivot_tvs = exactTyCoVarsOfType (if sym2 then rhs else lhs)
- , all (`elemVarSet` pivot_tvs) qtvs
- = undefined
- where
- co1_is_axiom_maybe = isAxiom_maybe co1
- co2_is_axiom_maybe = isAxiom_maybe co2
- role = coercionRole co1 -- should be the same as coercionRole co2!
+ , Just cos1 <- matchNewtypeBranch (not sym) axr co1
+ , let newAxInst = AxiomCo axr (opt_transList is cos1 cos2)
+ = newAxInst
opt_trans_rule is co1 co2
| Just (lco, lh) <- isCohRight_maybe co1
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/6ecf186049f4bbdd04f72c21a8960fe903c646ca...8119c093ba8c52c9c22b81ef727022beeff60ecd
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/6ecf186049f4bbdd04f72c21a8960fe903c646ca...8119c093ba8c52c9c22b81ef727022beeff60ecd
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/20240722/02c5e2c8/attachment-0001.html>
More information about the ghc-commits
mailing list