Commit 63a81707 authored by Ryan Scott's avatar Ryan Scott

Fix #15845 by defining etaExpandFamInstLHS and using it

Summary:
Both #9692 and #14179 were caused by GHC being careless
about using eta-reduced data family instance axioms. Each of those
tickets were fixed by manually whipping up some code to eta-expand
the axioms. The same sort of issue has now caused #15845, so I
figured it was high time to factor out the code that each of these
fixes have in common.

This patch introduces the `etaExpandFamInstLHS` function, which takes
a family instance's type variables, LHS types, and RHS type, and
returns type variables and LHS types that have been eta-expanded if
necessary, in the case of a data family instance. (If it's a type
family instance, `etaExpandFamInstLHS` just returns the supplied type
variables and LHS types unchanged).

Along the way, I noticed that many references to
`Note [Eta reduction for data families]` (in `FamInstEnv`) had
slightly bitrotted (they either referred to a somewhat different
name, or claimed that the Note lived in a different module), so
I took the liberty of cleaning those up.

Test Plan: make test TEST="T9692 T15845"

Reviewers: goldfire, bgamari

Reviewed By: goldfire

Subscribers: rwbarton, carter

GHC Trac Issues: #15845

Differential Revision: https://phabricator.haskell.org/D5294
parent 932cd41d
......@@ -1710,23 +1710,16 @@ reifyFamilyInstance is_poly_tvs inst@(FamInst { fi_flavor = flavor
(TH.TySynEqn th_tvs annot_th_lhs th_rhs)) }
DataFamilyInst rep_tc ->
do { let rep_tvs = tyConTyVars rep_tc
fam' = reifyName fam
-- eta-expand lhs types, because sometimes data/newtype
-- instances are eta-reduced; See Trac #9692
-- See Note [Eta reduction for data family axioms]
-- in TcInstDcls
(_rep_tc, rep_tc_args) = splitTyConApp rhs
etad_tyvars = dropList rep_tc_args rep_tvs
etad_tys = mkTyVarTys etad_tyvars
eta_expanded_tvs = mkTyVarTys fam_tvs `chkAppend` etad_tys
eta_expanded_lhs = lhs `chkAppend` etad_tys
do { let -- eta-expand lhs types, because sometimes data/newtype
-- instances are eta-reduced; See Trac #9692
-- See Note [Eta reduction for data families] in FamInstEnv
(ee_tvs, ee_lhs) = etaExpandFamInstLHS fam_tvs lhs rhs
fam' = reifyName fam
dataCons = tyConDataCons rep_tc
isGadt = isGadtSyntaxTyCon rep_tc
; th_tvs <- reifyTyVarsToMaybe fam_tvs
; cons <- mapM (reifyDataCon isGadt eta_expanded_tvs) dataCons
; let types_only = filterOutInvisibleTypes fam_tc eta_expanded_lhs
; th_tvs <- reifyTyVarsToMaybe ee_tvs
; cons <- mapM (reifyDataCon isGadt (mkTyVarTys ee_tvs)) dataCons
; let types_only = filterOutInvisibleTypes fam_tc ee_lhs
; th_tys <- reifyTypes types_only
; annot_th_tys <- zipWith3M annotThType is_poly_tvs types_only th_tys
; return $
......
......@@ -211,20 +211,10 @@ ppr_co_ax_branch ppr_rhs
= text "in" <+>
quotes (ppr (nameModule name))
(ee_tvs, ee_lhs)
| Just (tycon, tc_args) <- splitTyConApp_maybe rhs
, isDataFamilyTyCon fam_tc
= -- Eta-expand LHS types, because sometimes data family instances
-- are eta-reduced.
-- See Note [Eta reduction for data family axioms] in TcInstDecls.
let tc_tvs = tyConTyVars tycon
etad_tvs = dropList tc_args tc_tvs
etad_tys = mkTyVarTys etad_tvs
eta_expanded_tvs = tvs `chkAppend` etad_tvs
eta_expanded_lhs = lhs `chkAppend` etad_tys
in (eta_expanded_tvs, eta_expanded_lhs)
| otherwise
= (tvs, lhs)
-- Eta-expand LHS types, because sometimes data family instances
-- are eta-reduced.
-- See Note [Eta reduction for data families] in FamInstEnv.
(ee_tvs, ee_lhs) = etaExpandFamInstLHS tvs lhs rhs
{-
%************************************************************************
......
......@@ -7,6 +7,7 @@
module FamInstEnv (
FamInst(..), FamFlavor(..), famInstAxiom, famInstTyCon, famInstRHS,
famInstsRepTyCons, famInstRepTyCon_maybe, dataFamInstRepTyCon,
etaExpandFamInstLHS,
pprFamInst, pprFamInsts,
mkImportedFamInst,
......@@ -212,6 +213,11 @@ For a FamInst with fi_flavour = DataFamilyInst rep_tc,
But when fi_flavour = SynFamilyInst,
- fi_tys has the exact arity of the family tycon
There are certain situations (e.g., pretty-printing) where it is necessary to
deal with eta-expanded data family instances. For these situations, the
etaExpandFamInstLHS function exists as a convenient way to perform this eta
expansion. (See #9692, #14179, and #15845 for examples of what can go wrong if
etaExpandFamInstLHS isn't used).
(See also Note [Newtype eta] in TyCon. This is notionally separate
and deals with the axiom connecting a newtype with its representation
......@@ -555,7 +561,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 family axioms] in TcInstDcls. This means that
See Note [Eta reduction for data families] in FamInstEnv. This means that
we sometimes need to test compatibility of two axioms that were eta-reduced to
different degrees, e.g.:
......
......@@ -232,7 +232,7 @@ See also Note [Wrappers for data instance tycons] in MkId.hs
DataFamInstTyCon T [Int] ax_ti
* The axiom ax_ti may be eta-reduced; see
Note [Eta reduction for data family axioms] in FamInstEnv
Note [Eta reduction for data families] in FamInstEnv
* Data family instances may have a different arity than the data family.
See Note [Arity of data families] in FamInstEnv
......@@ -1010,8 +1010,8 @@ 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 TcInstDcls
-- Note [Eta reduction for data family axioms]
-- BUT may be eta-reduced; see FamInstEnv
-- Note [Eta reduction for data families]
-- Cached fields of the CoAxiom, but adjusted to
-- use the tyConTyVars of this TyCon
......
......@@ -69,6 +69,8 @@ module Type (
modifyJoinResTy, setJoinResTy,
etaExpandFamInstLHS,
-- Analyzing types
TyCoMapper(..), mapType, mapCoercion,
......@@ -3049,6 +3051,43 @@ setJoinResTy :: Int -- Number of binders to skip
setJoinResTy ar new_res_ty ty
= modifyJoinResTy ar (const new_res_ty) ty
-- | Given a data or type family instance's type variables, left-hand side
-- types, and right-hand side type, either:
--
-- * Return the eta-expanded type variables and left-hand types (if dealing
-- with a data family instance). This function obtains the eta-reduced
-- variables from the right-hand type, which is expected to be of the form
-- @'mkTyConApp' rep_tc ('mkTyVarTys' tc_tvs)@.
--
-- * Just return the type variables and left-hand types (if dealing with a
-- type family instance).
--
-- For an explanation of why data family instances need to have their
-- left-hand sides eta-expanded, see
-- @Note [Eta reduction for data families]@ in "FamInstEnv". Because the
-- right-hand side is where the eta-reduced variables are obtained from, it
-- is not returned from this function (as there is never a need to modify it).
-- NB: In an ideal world, this would live in FamInstEnv, but this function
-- is used in Coercion (which FamInstEnv imports), so doing so would lead to
-- an import cycle.
etaExpandFamInstLHS
:: [TyVar] -- ^ The type variables
-> [Type] -- ^ The left-hand side types
-> Type -- ^ The right-hand side type
-> ([TyVar], [Type])
etaExpandFamInstLHS tvs lhs rhs
| Just (tycon, tc_args) <- splitTyConApp_maybe rhs
, isFamInstTyCon tycon
= let tc_tvs = tyConTyVars tycon
etad_tvs = dropList tc_args tc_tvs
etad_tys = mkTyVarTys etad_tvs
eta_expanded_tvs = tvs `chkAppend` etad_tvs
eta_expanded_lhs = lhs `chkAppend` etad_tys
in (eta_expanded_tvs, eta_expanded_lhs)
| otherwise
= (tvs, lhs)
{-
%************************************************************************
%* *
......
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
module T15845 where
import Language.Haskell.TH
import System.IO
data family F1 a b
data instance F1 [a] b = MkF1
data family F2 a
data instance F2 a = MkF2
$(do i1 <- reify ''F1
i2 <- reify ''F2
runIO $ mapM_ (hPutStrLn stderr . pprint) [i1, i2]
pure [])
data family T15845.F1 (a_0 :: *) (b_1 :: *) :: *
data instance forall (a_2 :: *) (b_3 :: *). T15845.F1 ([a_2]) b_3
= T15845.MkF1
data family T15845.F2 (a_0 :: *) :: *
data instance forall (a_1 :: *). T15845.F2 a_1 = T15845.MkF2
data family T9692.F (a_0 :: k_1) (b_2 :: k_3) :: *
data instance T9692.F GHC.Types.Int (x_4 :: *) = T9692.FInt x_4
data instance forall (x_4 :: *). T9692.F GHC.Types.Int (x_4 :: *)
= T9692.FInt x_4
......@@ -448,3 +448,4 @@ test('T15783', normal, multimod_compile,
test('T15792', normal, compile, ['-v0 -dsuppress-uniques'])
test('T15815', normal, multimod_compile,
['T15815B', '-v0 ' + config.ghc_th_way_flags])
test('T15845', normal, compile, ['-v0 -dsuppress-uniques'])
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment