diff options
| -rw-r--r-- | compiler/GHC/Core/Coercion.hs | 2 | ||||
| -rw-r--r-- | compiler/GHC/Core/Coercion/Axiom.hs | 12 | ||||
| -rw-r--r-- | compiler/GHC/Core/FamInstEnv.hs | 14 | ||||
| -rw-r--r-- | compiler/GHC/Core/TyCon.hs | 7 | ||||
| -rw-r--r-- | compiler/typecheck/TcDeriv.hs | 2 | ||||
| -rw-r--r-- | compiler/typecheck/TcInstDcls.hs | 13 | ||||
| -rw-r--r-- | compiler/typecheck/TcSplice.hs | 2 |
7 files changed, 31 insertions, 21 deletions
diff --git a/compiler/GHC/Core/Coercion.hs b/compiler/GHC/Core/Coercion.hs index 06de44f65b..ea9a21d2aa 100644 --- a/compiler/GHC/Core/Coercion.hs +++ b/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) diff --git a/compiler/GHC/Core/Coercion/Axiom.hs b/compiler/GHC/Core/Coercion/Axiom.hs index 9b8fb6e067..5dd99a4ac1 100644 --- a/compiler/GHC/Core/Coercion/Axiom.hs +++ b/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 diff --git a/compiler/GHC/Core/FamInstEnv.hs b/compiler/GHC/Core/FamInstEnv.hs index 8ac78035bd..0b58195be6 100644 --- a/compiler/GHC/Core/FamInstEnv.hs +++ b/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 diff --git a/compiler/GHC/Core/TyCon.hs b/compiler/GHC/Core/TyCon.hs index 11fd1cf5a9..e3044095bc 100644 --- a/compiler/GHC/Core/TyCon.hs +++ b/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 diff --git a/compiler/typecheck/TcDeriv.hs b/compiler/typecheck/TcDeriv.hs index 40efd08652..506ae1a1fc 100644 --- a/compiler/typecheck/TcDeriv.hs +++ b/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 %************************************************************************ %* * diff --git a/compiler/typecheck/TcInstDcls.hs b/compiler/typecheck/TcInstDcls.hs index e189c7d896..40bc3853d5 100644 --- a/compiler/typecheck/TcInstDcls.hs +++ b/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 diff --git a/compiler/typecheck/TcSplice.hs b/compiler/typecheck/TcSplice.hs index d6972f8ec5..40e16d1305 100644 --- a/compiler/typecheck/TcSplice.hs +++ b/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 |