diff options
Diffstat (limited to 'compiler/typecheck/TcInstDcls.hs')
| -rw-r--r-- | compiler/typecheck/TcInstDcls.hs | 13 |
1 files changed, 8 insertions, 5 deletions
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 |