Commit 014d6c1f authored by Ryan Scott's avatar Ryan Scott Committed by Ben Gamari

Fix #15852 by eta expanding data family instance RHSes, too

When I defined `etaExpandFamInstLHS`, I blatantly forgot
to eta expand the RHSes of data family instances. (Actually, I
claimed that they didn't //need// to be eta expanded. I'm not sure
what I was thinking.)

This fixes the issue by changing `etaExpandFamInstLHS` to
`etaExpandFamInst` and, well, making it actually eta expand the RHS.

Test Plan: make test TEST=T15852

Reviewers: goldfire, bgamari

Reviewed By: goldfire

Subscribers: rwbarton, carter

GHC Trac Issues: #15852

Differential Revision: https://phabricator.haskell.org/D5328
parent 66f0056a
......@@ -859,6 +859,8 @@ avoidClashesOccEnv env occs = go env emptyUFM occs
tidyOccName :: TidyOccEnv -> OccName -> (TidyOccEnv, OccName)
tidyOccName env occ@(OccName occ_sp fs)
| not (fs `elemUFM` env)
&& (fs /= fsLit "_")
-- See Note [Always number wildcard types when tidying]
= (addToUFM env fs 1, occ) -- Desired OccName is free
| otherwise
= case lookupUFM env base1 of
......@@ -885,6 +887,34 @@ tidyOccName env occ@(OccName occ_sp fs)
-- If they are the same (n==1), the former wins
-- See Note [TidyOccEnv]
{-
Note [Always number wildcard types when tidying]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider the following example (from the DataFamilyInstanceLHS test case):
data family Sing (a :: k)
data instance Sing (_ :: MyKind) where
SingA :: Sing A
SingB :: Sing B
If we're not careful during tidying, then when this program is compiled with
-ddump-types, we'll get the following information:
COERCION AXIOMS
axiom DataFamilyInstanceLHS.D:R:SingMyKind_0 ::
Sing _ = DataFamilyInstanceLHS.R:SingMyKind_ _
Yikes! We shouldn't have a wildcard type appearing on the RHS like that. To
avoid this issue, during tidying, we always opt to add a numeric suffix to
types that are simply `_`. That way, you instead end up with:
COERCION AXIOMS
axiom DataFamilyInstanceLHS.D:R:SingMyKind_0 ::
Sing _1 = DataFamilyInstanceLHS.R:SingMyKind_ _1
Which is at least legal syntax.
-}
{-
************************************************************************
* *
......
......@@ -4,6 +4,7 @@ import {-# SOURCE #-} TyCoRep
import {-# SOURCE #-} IfaceType( IfaceType, IfaceTyCon, IfaceForAllBndr
, IfaceCoercion, IfaceTyLit, IfaceAppArgs )
import Var ( TyCoVarBinder )
import VarEnv ( TidyEnv )
import TyCon ( TyCon )
import VarSet( VarSet )
......@@ -14,3 +15,4 @@ toIfaceForAllBndr :: TyCoVarBinder -> IfaceForAllBndr
toIfaceTyCon :: TyCon -> IfaceTyCon
toIfaceTcArgs :: TyCon -> [Type] -> IfaceAppArgs
toIfaceCoercionX :: VarSet -> Coercion -> IfaceCoercion
tidyToIfaceTcArgs :: TidyEnv -> TyCon -> [Type] -> IfaceAppArgs
......@@ -1713,10 +1713,10 @@ reifyFamilyInstance is_poly_tvs inst@(FamInst { fi_flavor = flavor
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
(ee_tvs, ee_lhs, _) = etaExpandFamInst fam_tvs lhs rhs
fam' = reifyName fam
dataCons = tyConDataCons rep_tc
isGadt = isGadtSyntaxTyCon rep_tc
; th_tvs <- reifyTyVarsToMaybe ee_tvs
; cons <- mapM (reifyDataCon isGadt (mkTyVarTys ee_tvs)) dataCons
; let types_only = filterOutInvisibleTypes fam_tc ee_lhs
......
......@@ -109,8 +109,11 @@ module Coercion (
#include "HsVersions.h"
import {-# SOURCE #-} ToIface (toIfaceTyCon, tidyToIfaceTcArgs)
import GhcPrelude
import IfaceType
import TyCoRep
import Type
import TyCon
......@@ -170,13 +173,14 @@ Defined here to avoid module loops. CoAxiom is loaded very early on.
pprCoAxiom :: CoAxiom br -> SDoc
pprCoAxiom ax@(CoAxiom { co_ax_branches = branches })
= hang (text "axiom" <+> ppr ax <+> dcolon)
2 (vcat (map (ppr_co_ax_branch (\_ ty -> equals <+> pprType ty) ax) $
2 (vcat (map (ppr_co_ax_branch (\env _ ty ->
equals <+> pprPrecTypeX env topPrec ty) ax) $
fromBranches branches))
pprCoAxBranch :: CoAxiom br -> CoAxBranch -> SDoc
pprCoAxBranch = ppr_co_ax_branch pprRhs
where
pprRhs fam_tc rhs
pprRhs _ fam_tc rhs
| isDataFamilyTyCon fam_tc
= empty -- Don't bother printing anything for the RHS of a data family
-- instance...
......@@ -190,7 +194,8 @@ pprCoAxBranch = ppr_co_ax_branch pprRhs
pprCoAxBranchHdr :: CoAxiom br -> BranchIndex -> SDoc
pprCoAxBranchHdr ax index = pprCoAxBranch ax (coAxiomNthBranch ax index)
ppr_co_ax_branch :: (TyCon -> Type -> SDoc) -> CoAxiom br -> CoAxBranch -> SDoc
ppr_co_ax_branch :: (TidyEnv -> TyCon -> Type -> SDoc)
-> CoAxiom br -> CoAxBranch -> SDoc
ppr_co_ax_branch ppr_rhs
(CoAxiom { co_ax_tc = fam_tc, co_ax_name = name })
(CoAxBranch { cab_tvs = tvs
......@@ -199,8 +204,8 @@ ppr_co_ax_branch ppr_rhs
, cab_rhs = rhs
, cab_loc = loc })
= foldr1 (flip hangNotEmpty 2)
[ pprUserForAll (mkTyCoVarBinders Inferred (ee_tvs ++ cvs))
, pprTypeApp fam_tc ee_lhs <+> ppr_rhs fam_tc rhs
[ pprUserForAll (mkTyCoVarBinders Inferred (ee_tvs' ++ cvs))
, pp_lhs <+> ppr_rhs env fam_tc ee_rhs
, text "-- Defined" <+> pprLoc loc ]
where
pprLoc loc
......@@ -211,10 +216,14 @@ ppr_co_ax_branch ppr_rhs
= text "in" <+>
quotes (ppr (nameModule name))
-- Eta-expand LHS types, because sometimes data family instances
-- are eta-reduced.
-- Eta-expand LHS and RHS 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
(ee_tvs, ee_lhs, ee_rhs) = etaExpandFamInst tvs lhs rhs
(env, ee_tvs') = tidyVarBndrs emptyTidyEnv ee_tvs
pp_lhs = pprIfaceTypeApp topPrec (toIfaceTyCon fam_tc)
(tidyToIfaceTcArgs env fam_tc ee_lhs)
{-
%************************************************************************
......
......@@ -7,7 +7,7 @@
module FamInstEnv (
FamInst(..), FamFlavor(..), famInstAxiom, famInstTyCon, famInstRHS,
famInstsRepTyCons, famInstRepTyCon_maybe, dataFamInstRepTyCon,
etaExpandFamInstLHS,
etaExpandFamInst,
pprFamInst, pprFamInsts,
mkImportedFamInst,
......
......@@ -61,7 +61,7 @@ module TyCoRep (
pickLR,
-- * Pretty-printing
pprType, pprParendType, pprPrecType,
pprType, pprParendType, pprPrecType, pprPrecTypeX,
pprTypeApp, pprTCvBndr, pprTCvBndrs,
pprSigmaType,
pprTheta, pprParendTheta, pprForAll, pprUserForAll,
......@@ -3122,11 +3122,14 @@ pprType = pprPrecType topPrec
pprParendType = pprPrecType appPrec
pprPrecType :: PprPrec -> Type -> SDoc
pprPrecType prec ty
pprPrecType = pprPrecTypeX emptyTidyEnv
pprPrecTypeX :: TidyEnv -> PprPrec -> Type -> SDoc
pprPrecTypeX env prec ty
= getPprStyle $ \sty ->
if debugStyle sty -- Use pprDebugType when in
then debug_ppr_ty prec ty -- when in debug-style
else pprPrecIfaceType prec (tidyToIfaceTypeSty ty sty)
else pprPrecIfaceType prec (tidyToIfaceTypeStyX env ty sty)
pprTyLit :: TyLit -> SDoc
pprTyLit = pprIfaceTyLit . toIfaceTyLit
......@@ -3135,22 +3138,25 @@ pprKind, pprParendKind :: Kind -> SDoc
pprKind = pprType
pprParendKind = pprParendType
tidyToIfaceTypeSty :: Type -> PprStyle -> IfaceType
tidyToIfaceTypeSty ty sty
| userStyle sty = tidyToIfaceType ty
tidyToIfaceTypeStyX :: TidyEnv -> Type -> PprStyle -> IfaceType
tidyToIfaceTypeStyX env ty sty
| userStyle sty = tidyToIfaceTypeX env ty
| otherwise = toIfaceTypeX (tyCoVarsOfType ty) ty
-- in latter case, don't tidy, as we'll be printing uniques.
tidyToIfaceType :: Type -> IfaceType
tidyToIfaceType = tidyToIfaceTypeX emptyTidyEnv
tidyToIfaceTypeX :: TidyEnv -> Type -> IfaceType
-- It's vital to tidy before converting to an IfaceType
-- or nested binders will become indistinguishable!
--
-- Also for the free type variables, tell toIfaceTypeX to
-- leave them as IfaceFreeTyVar. This is super-important
-- for debug printing.
tidyToIfaceType ty = toIfaceTypeX (mkVarSet free_tcvs) (tidyType env ty)
tidyToIfaceTypeX env ty = toIfaceTypeX (mkVarSet free_tcvs) (tidyType env' ty)
where
env = tidyFreeTyCoVars emptyTidyEnv free_tcvs
env' = tidyFreeTyCoVars env free_tcvs
free_tcvs = tyCoVarsOfTypeWellScoped ty
------------
......
......@@ -69,7 +69,7 @@ module Type (
modifyJoinResTy, setJoinResTy,
etaExpandFamInstLHS,
etaExpandFamInst,
-- Analyzing types
TyCoMapper(..), mapType, mapCoercion,
......@@ -3054,29 +3054,26 @@ setJoinResTy ar 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)@.
-- * Return the eta-expanded type variables, left-hand types, and right-hand
-- type (if dealing with a data family instance). This function obtains the
-- eta-reduced variables from the instance's representation 'TyCon' (which
-- heads the right-hand type).
--
-- * Just return the type variables and left-hand types (if dealing with a
-- type family instance).
-- * Just return the type variables, left-hand types, and right-hand type
-- (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).
-- For an explanation of why data family instances need to be eta expanded, see
-- @Note [Eta reduction for data families]@ in "FamInstEnv".
-- 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
etaExpandFamInst
:: [TyVar] -- ^ The type variables
-> [Type] -- ^ The left-hand side types
-> Type -- ^ The right-hand side type
-> ([TyVar], [Type])
etaExpandFamInstLHS tvs lhs rhs
-> ([TyVar], [Type], Type)
etaExpandFamInst tvs lhs rhs
| Just (tycon, tc_args) <- splitTyConApp_maybe rhs
, isFamInstTyCon tycon
= let tc_tvs = tyConTyVars tycon
......@@ -3084,9 +3081,10 @@ etaExpandFamInstLHS tvs lhs rhs
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)
eta_expanded_rhs = mkAppTys rhs etad_tys
in (eta_expanded_tvs, eta_expanded_lhs, eta_expanded_rhs)
| otherwise
= (tvs, lhs)
= (tvs, lhs, rhs)
{-
%************************************************************************
......
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
module T15852 where
import Data.Kind
import Data.Proxy
data family DF a (b :: k)
data instance DF (Proxy c) :: Proxy j -> Type
TYPE CONSTRUCTORS
type role DF nominal nominal nominal
DF :: forall k. * -> k -> *
COERCION AXIOMS
axiom T15852.D:R:DFProxyProxy0 ::
forall k1 k2 (c :: k1) (j :: k2) (a :: Proxy j).
DF (Proxy c) a = T15852.R:DFProxyProxy k1 k2 c j a
-- Defined at T15852.hs:10:15
FAMILY INSTANCES
data instance DF (Proxy c) c j a
Dependent modules: []
Dependent packages: [base-4.12.0.0, ghc-prim-0.5.3,
integer-gmp-1.0.2.0]
......@@ -296,3 +296,4 @@ test('T15352', normal, compile, [''])
test('T15664', normal, compile, [''])
test('T15704', normal, compile, [''])
test('T15711', normal, compile, ['-ddump-types'])
test('T15852', normal, compile, ['-ddump-types'])
......@@ -6,7 +6,7 @@ TYPE CONSTRUCTORS
Sing :: forall k. k -> *
COERCION AXIOMS
axiom DataFamilyInstanceLHS.D:R:SingMyKind_0 ::
Sing _ = DataFamilyInstanceLHS.R:SingMyKind_
Sing _1 = DataFamilyInstanceLHS.R:SingMyKind_ _1
-- Defined at DataFamilyInstanceLHS.hs:8:15
DATA CONSTRUCTORS
A :: MyKind
......
......@@ -4,7 +4,7 @@ TYPE CONSTRUCTORS
Sing :: forall k. k -> *
COERCION AXIOMS
axiom NamedWildcardInDataFamilyInstanceLHS.D:R:SingMyKind_a0 ::
Sing _a = NamedWildcardInDataFamilyInstanceLHS.R:SingMyKind_a
Sing _a = NamedWildcardInDataFamilyInstanceLHS.R:SingMyKind_a _a
-- Defined at NamedWildcardInDataFamilyInstanceLHS.hs:8:15
DATA CONSTRUCTORS
A :: MyKind
......
......@@ -4,13 +4,13 @@ TYPE CONSTRUCTORS
type role F nominal nominal
F :: * -> * -> *
COERCION AXIOMS
axiom TypeFamilyInstanceLHS.D:R:FBool_ ::
F Bool _ = Bool -- Defined at TypeFamilyInstanceLHS.hs:8:15
axiom TypeFamilyInstanceLHS.D:R:FInt_ ::
F Int _ = Int -- Defined at TypeFamilyInstanceLHS.hs:7:15
axiom TypeFamilyInstanceLHS.D:R:FBool_1 ::
F Bool _1 = Bool -- Defined at TypeFamilyInstanceLHS.hs:8:15
axiom TypeFamilyInstanceLHS.D:R:FInt_1 ::
F Int _1 = Int -- Defined at TypeFamilyInstanceLHS.hs:7:15
FAMILY INSTANCES
type instance F Int _
type instance F Bool _
type instance F Int _1
type instance F Bool _1
Dependent modules: []
Dependent packages: [base-4.12.0.0, ghc-prim-0.5.3,
integer-gmp-1.0.2.0]
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