[Git][ghc/ghc][wip/T17313] Clean up "Eta reduction for data families" Notes
Ryan Scott
gitlab at gitlab.haskell.org
Tue Mar 31 14:37:18 UTC 2020
Ryan Scott pushed to branch wip/T17313 at Glasgow Haskell Compiler / GHC
Commits:
0bae7ba2 by Ryan Scott at 2020-03-31T10:36:54-04:00
Clean up "Eta reduction for data families" Notes
Before, there were two distinct Notes named
"Eta reduction for data families". This renames one of them to
"Implementing eta reduction for data families" to disambiguate the
two and fixes references in other parts of the codebase to ensure
that they are pointing to the right place.
Fixes #17313.
[ci skip]
- - - - -
7 changed files:
- compiler/GHC/Core/Coercion.hs
- compiler/GHC/Core/Coercion/Axiom.hs
- compiler/GHC/Core/FamInstEnv.hs
- compiler/GHC/Core/TyCon.hs
- compiler/typecheck/TcDeriv.hs
- compiler/typecheck/TcInstDcls.hs
- compiler/typecheck/TcSplice.hs
Changes:
=====================================
compiler/GHC/Core/Coercion.hs
=====================================
@@ -245,7 +245,7 @@ ppr_co_ax_branch ppr_rhs fam_tc branch
-- Eta-expand LHS and RHS types, because sometimes data family
-- instances are eta-reduced.
- -- See Note [Eta reduction for data families] in GHC.Core.FamInstEnv.
+ -- See Note [Eta reduction for data families] in GHC.Core.Coercion.Axiom.
(ee_tvs, ee_lhs, ee_rhs) = etaExpandCoAxBranch branch
pp_lhs = pprIfaceTypeApp topPrec (toIfaceTyCon fam_tc)
=====================================
compiler/GHC/Core/Coercion/Axiom.hs
=====================================
@@ -235,7 +235,7 @@ data CoAxBranch
, cab_tvs :: [TyVar] -- Bound type variables; not necessarily fresh
, cab_eta_tvs :: [TyVar] -- Eta-reduced tyvars
-- See Note [CoAxBranch type variables]
- -- cab_tvs and cab_lhs may be eta-reduded; see
+ -- cab_tvs and cab_lhs may be eta-reduced; see
-- Note [Eta reduction for data families]
, cab_cvs :: [CoVar] -- Bound coercion variables
-- Always empty, for now.
@@ -443,9 +443,13 @@ looked like
(See #9692, #14179, and #15845 for examples of what can go wrong if
we don't eta-expand when showing things to the user.)
-(See also Note [Newtype eta] in GHC.Core.TyCon. This is notionally separate
-and deals with the axiom connecting a newtype with its representation
-type; but it too is eta-reduced.)
+See also:
+
+* Note [Newtype eta] in GHC.Core.TyCon. This is notionally separate
+ and deals with the axiom connecting a newtype with its representation
+ type; but it too is eta-reduced.
+* Note [Implementing eta reduction for data families] in TcInstDcls. This
+ describes the implementation details of this eta reduction happen.
-}
instance Eq (CoAxiom br) where
=====================================
compiler/GHC/Core/FamInstEnv.hs
=====================================
@@ -118,6 +118,7 @@ data FamInst -- See Note [FamInsts and CoAxioms]
, fi_tys :: [Type] -- The LHS type patterns
-- May be eta-reduced; see Note [Eta reduction for data families]
+ -- in GHC.Core.Coercion.Axiom
, fi_rhs :: Type -- the RHS, with its freshened vars
}
@@ -132,7 +133,8 @@ Note [Arity of data families]
Data family instances might legitimately be over- or under-saturated.
Under-saturation has two potential causes:
- U1) Eta reduction. See Note [Eta reduction for data families].
+ U1) Eta reduction. See Note [Eta reduction for data families] in
+ GHC.Core.Coercion.Axiom.
U2) When the user has specified a return kind instead of written out patterns.
Example:
@@ -160,8 +162,8 @@ Over-saturation is also possible:
However, we require that any over-saturation is eta-reducible. That is,
we require that any extra patterns be bare unrepeated type variables;
- see Note [Eta reduction for data families]. Accordingly, the FamInst
- is never over-saturated.
+ see Note [Eta reduction for data families] in GHC.Core.Coercion.Axiom.
+ Accordingly, the FamInst is never over-saturated.
Why can we allow such flexibility for data families but not for type families?
Because data families can be decomposed -- that is, they are generative and
@@ -335,7 +337,7 @@ Then we get a data type for each instance, and an axiom:
axiom ax8 a :: T Bool [a] ~ TBoolList a
These two axioms for T, one with one pattern, one with two;
-see Note [Eta reduction for data families]
+see Note [Eta reduction for data families] in GHC.Core.Coercion.Axiom
Note [FamInstEnv determinism]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -479,7 +481,7 @@ irrelevant (clause 1 of compatible) or benign (clause 2 of compatible).
Note [Compatibility of eta-reduced axioms]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In newtype instances of data families we eta-reduce the axioms,
-See Note [Eta reduction for data families] in GHC.Core.FamInstEnv. This means that
+See Note [Eta reduction for data families] in GHC.Core.Coercion.Axiom. This means that
we sometimes need to test compatibility of two axioms that were eta-reduced to
different degrees, e.g.:
@@ -1057,7 +1059,7 @@ We handle data families and type families separately here:
* For data family instances, though, we need to re-split for each
instance, because the breakdown might be different for each
instance. Why? Because of eta reduction; see
- Note [Eta reduction for data families].
+ Note [Eta reduction for data families] in GHC.Core.Coercion.Axiom.
-}
-- checks if one LHS is dominated by a list of other branches
=====================================
compiler/GHC/Core/TyCon.hs
=====================================
@@ -240,7 +240,7 @@ See also Note [Wrappers for data instance tycons] in GHC.Types.Id.Make
DataFamInstTyCon T [Int] ax_ti
* The axiom ax_ti may be eta-reduced; see
- Note [Eta reduction for data families] in GHC.Core.FamInstEnv
+ Note [Eta reduction for data families] in GHC.Core.Coercion.Axiom
* Data family instances may have a different arity than the data family.
See Note [Arity of data families] in GHC.Core.FamInstEnv
@@ -1100,8 +1100,9 @@ data AlgTyConFlav
-- and R:T is the representation TyCon (ie this one)
-- and a,b,c are the tyConTyVars of this TyCon
--
- -- BUT may be eta-reduced; see FamInstEnv
- -- Note [Eta reduction for data families]
+ -- BUT may be eta-reduced; see
+ -- Note [Eta reduction for data families] in
+ -- GHC.Core.Coercion.Axiom
-- Cached fields of the CoAxiom, but adjusted to
-- use the tyConTyVars of this TyCon
=====================================
compiler/typecheck/TcDeriv.hs
=====================================
@@ -1312,7 +1312,7 @@ write it out
return x = MkT [x]
... etc ...
-See Note [Eta reduction for data families] in GHC.Core.FamInstEnv
+See Note [Eta reduction for data families] in GHC.Core.Coercion.Axiom
%************************************************************************
%* *
=====================================
compiler/typecheck/TcInstDcls.hs
=====================================
@@ -667,7 +667,7 @@ tcDataFamInstDecl mb_clsinfo
new_or_data
-- Eta-reduce the axiom if possible
- -- Quite tricky: see Note [Eta-reduction for data families]
+ -- Quite tricky: see Note [Implementing eta reduction for data families]
; let (eta_pats, eta_tcbs) = eta_reduce fam_tc pats
eta_tvs = map binderVar eta_tcbs
post_eta_qtvs = filterOut (`elem` eta_tvs) qtvs
@@ -761,7 +761,7 @@ tcDataFamInstDecl mb_clsinfo
; return (fam_inst, m_deriv_info) }
where
eta_reduce :: TyCon -> [Type] -> ([Type], [TyConBinder])
- -- See Note [Eta reduction for data families] in GHC.Core.FamInstEnv
+ -- See Note [Eta reduction for data families] in GHC.Core.Coercion.Axiom
-- Splits the incoming patterns into two: the [TyVar]
-- are the patterns that can be eta-reduced away.
-- e.g. T [a] Int a d c ==> (T [a] Int a, [d,c])
@@ -887,8 +887,8 @@ we actually have a place to put the regeneralised variables.
Thus: skolemise away. cf. Inst.deeplySkolemise and TcUnify.tcSkolemise
Examples in indexed-types/should_compile/T12369
-Note [Eta-reduction for data families]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Note [Implementing eta reduction for data families]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
data D :: * -> * -> * -> * -> *
@@ -906,7 +906,10 @@ and an axiom to connect them
except that we'll eta-reduce the axiom to
axiom AxDrep forall a b. D [(a,b]] = Drep a b
-There are several fiddly subtleties lurking here
+
+This is described at some length in Note [Eta reduction for data families]
+in GHC.Core.Coercion.Axiom. There are several fiddly subtleties lurking here,
+however, so this Note aims to describe these subtleties:
* The representation tycon Drep is parameterised over the free
variables of the pattern, in no particular order. So there is no
=====================================
compiler/typecheck/TcSplice.hs
=====================================
@@ -2046,7 +2046,7 @@ reifyFamilyInstance is_poly_tvs (FamInst { fi_flavor = flavor
DataFamilyInst rep_tc ->
do { let -- eta-expand lhs types, because sometimes data/newtype
-- instances are eta-reduced; See #9692
- -- See Note [Eta reduction for data families] in GHC.Core.FamInstEnv
+ -- See Note [Eta reduction for data families] in GHC.Core.Coercion.Axiom
(ee_tvs, ee_lhs, _) = etaExpandCoAxBranch branch
fam' = reifyName fam
dataCons = tyConDataCons rep_tc
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/0bae7ba256acaf48aa7c1d586fdad8e9fc43b4cd
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/0bae7ba256acaf48aa7c1d586fdad8e9fc43b4cd
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/20200331/bbc0cf40/attachment-0001.html>
More information about the ghc-commits
mailing list