Commit 1160dc51 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Fix egregious error in eta-reduction of data families

This terrible and long-standing bug was shown up by Trac #11148.
We are trying to eta-reduce a data family instance, so that we
can then derive Functor or Generic.  But we were assuming, for
absolutely not reason whatsoever, that the type variables were
lined up in a convenient order.  The fact that it ever worked
was a fluke.

This patch fixes it properly.  Main change is in eta_reduce
in TcInstDcls.tcDataFamInstDecl
parent 822141b9
......@@ -663,33 +663,39 @@ tcDataFamInstDecl mb_clsinfo
-- Construct representation tycon
; rep_tc_name <- newFamInstTyConName fam_tc_name pats'
; axiom_name <- newImplicitBinder rep_tc_name mkInstTyCoOcc
; let orig_res_ty = mkTyConApp fam_tc pats'
; let (eta_pats, etad_tvs) = eta_reduce pats'
eta_tvs = filterOut (`elem` etad_tvs) tvs'
full_tvs = eta_tvs ++ etad_tvs
-- Put the eta-removed tyvars at the end
-- Remember, tvs' is in arbitrary order (except kind vars are
-- first, so there is no reason to suppose that the etad_tvs
-- (obtained from the pats) are at the end (Trac #11148)
orig_res_ty = mkTyConApp fam_tc pats'
; (rep_tc, fam_inst) <- fixM $ \ ~(rec_rep_tc, _) ->
do { data_cons <- tcConDecls new_or_data
False -- Not promotable
rec_rep_tc
(tvs', orig_res_ty) cons
(full_tvs, orig_res_ty) cons
; tc_rhs <- case new_or_data of
DataType -> return (mkDataTyConRhs data_cons)
NewType -> ASSERT( not (null data_cons) )
mkNewTyConRhs rep_tc_name rec_rep_tc (head data_cons)
-- freshen tyvars
; let (eta_tvs, eta_pats) = eta_reduce tvs' pats'
axiom = mkSingleCoAxiom Representational
axiom_name eta_tvs fam_tc eta_pats
(mkTyConApp rep_tc (mkTyVarTys eta_tvs))
parent = DataFamInstTyCon axiom fam_tc pats'
roles = map (const Nominal) tvs'
-- NB: Use the tvs' from the pats. See bullet toward
; let axiom = mkSingleCoAxiom Representational
axiom_name eta_tvs fam_tc eta_pats
(mkTyConApp rep_tc (mkTyVarTys eta_tvs))
parent = DataFamInstTyCon axiom fam_tc pats'
-- NB: Use the full_tvs from the pats. See bullet toward
-- the end of Note [Data type families] in TyCon
rep_tc = buildAlgTyCon rep_tc_name tvs' roles
(fmap unLoc cType) stupid_theta
tc_rhs
Recursive
False -- No promotable to the kind level
gadt_syntax parent
rep_tc = buildAlgTyCon rep_tc_name full_tvs
(map (const Nominal) full_tvs)
(fmap unLoc cType) stupid_theta
tc_rhs
Recursive
False -- No promotable to the kind level
gadt_syntax parent
-- We always assume that indexed types are recursive. Why?
-- (1) Due to their open nature, we can never be sure that a
-- further instance might not introduce a new recursive
......@@ -710,51 +716,27 @@ tcDataFamInstDecl mb_clsinfo
; return (fam_inst, m_deriv_info) } }
where
-- See Note [Eta reduction for data family axioms]
-- [a,b,c,d].T [a] c Int c d ==> [a,b,c]. T [a] c Int c
eta_reduce tvs pats = go (reverse tvs) (reverse pats)
go (tv:tvs) (pat:pats)
| Just tv' <- getTyVar_maybe pat
, tv == tv'
eta_reduce :: [Type] -> ([Type], [TyVar])
-- See Note [Eta reduction for data families] in FamInstEnv
-- 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])
--
-- NB: quadratic algorithm, but types are small here
eta_reduce pats
= go (reverse pats) []
go (pat:pats) etad_tvs
| Just tv <- getTyVar_maybe pat
, not (tv `elemVarSet` tyVarsOfTypes pats)
= go tvs pats
go tvs pats = (reverse tvs, reverse pats)
{-
Note [Eta reduction for data family axioms]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider this
data family T a b :: *
newtype instance T Int a = MkT (IO a) deriving( Monad )
We'd like this to work. From the 'newtype instance' you might
think we'd get:
newtype TInt a = MkT (IO a)
axiom ax1 a :: T Int a ~ TInt a -- The type-instance part
axiom ax2 a :: TInt a ~ IO a -- The newtype part
But now what can we do? We have this problem
Given: d :: Monad IO
Wanted: d' :: Monad (T Int) = d |> ????
What coercion can we use for the ???
Solution: eta-reduce both axioms, thus:
axiom ax1 :: T Int ~ TInt
axiom ax2 :: TInt ~ IO
Now
d' = d |> Monad (sym (ax2 ; ax1))
= go pats (tv : etad_tvs)
go pats etad_tvs = (reverse pats, etad_tvs)
This eta reduction happens both for data instances and newtype instances.
See Note [Newtype eta] in TyCon.
************************************************************************
{- *********************************************************************
* *
Type-checking instance declarations, pass 2
* *
************************************************************************
-}
********************************************************************* -}
tcInstDecls2 :: [LTyClDecl Name] -> [InstInfo Name]
-> TcM (LHsBinds Id)
......
......@@ -102,21 +102,59 @@ data FamInst -- See Note [FamInsts and CoAxioms]
-- INVARIANT: fi_tcs = roughMatchTcs fi_tys
-- Used for "proper matching"; ditto
, fi_tvs :: [TyVar] -- Template tyvars for full match
-- Like ClsInsts, these variables are always
-- fresh. See Note [Template tyvars are fresh]
-- in InstEnv
-- INVARIANT: fi_tvs = coAxiomTyVars fi_axiom
, fi_tvs :: [TyVar] -- Template tyvars for full match
-- Like ClsInsts, these variables are always fresh
-- See Note [Template tyvars are fresh] in InstEnv
-- INVARIANT: fi_tvs = coAxiomTyVars fi_axiom
, fi_tys :: [Type] -- and its arg types
, fi_tys :: [Type] -- The LHS type patterns
-- May be eta-reduced; see Note [Eta reduction for data families]
, fi_rhs :: Type -- the RHS, with its freshened vars
, fi_rhs :: Type -- the RHS, with its freshened vars
}
data FamFlavor
= SynFamilyInst -- A synonym family
| DataFamilyInst TyCon -- A data family, with its representation TyCon
{- Note [Eta reduction for data families]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider this
data family T a b :: *
newtype instance T Int a = MkT (IO a) deriving( Monad )
We'd like this to work.
From the 'newtype instance' you might think we'd get:
newtype TInt a = MkT (IO a)
axiom ax1 a :: T Int a ~ TInt a -- The newtype-instance part
axiom ax2 a :: TInt a ~ IO a -- The newtype part
But now what can we do? We have this problem
Given: d :: Monad IO
Wanted: d' :: Monad (T Int) = d |> ????
What coercion can we use for the ???
Solution: eta-reduce both axioms, thus:
axiom ax1 :: T Int ~ TInt
axiom ax2 :: TInt ~ IO
Now
d' = d |> Monad (sym (ax2 ; ax1))
This eta reduction happens for data instances as well as newtype
instances. Here we want to eta-reduce the data family axiom.
All this is done in TcInstDcls.tcDataFamInstDecl.
See also Note [Newtype eta] in TyCon.
Bottom line:
For a FamInst with fi_flavour = DataFamilyInst rep_tc,
- fi_tvs may be shorter than tyConTyVars of rep_tc
- fi_tys may be shorter than tyConArity of the family tycon
i.e. LHS is unsaturated
- fi_rhs will be (rep_tc fi_tvs)
i.e. RHS is un-saturated
-}
-- Obtain the axiom of a family instance
famInstAxiom :: FamInst -> CoAxiom Unbranched
famInstAxiom = fi_axiom
......@@ -170,11 +208,13 @@ instance Outputable FamInst where
-- See pprTyThing.pprFamInst for printing for the user
pprFamInst :: FamInst -> SDoc
pprFamInst famInst
= hang (pprFamInstHdr famInst)
2 (vcat [ ifPprDebug (ptext (sLit "Coercion axiom:") <+> ppr ax)
, ifPprDebug (ptext (sLit "RHS:") <+> ppr (famInstRHS famInst)) ])
= hang (pprFamInstHdr famInst) 2 (ifPprDebug debug_stuff)
where
ax = fi_axiom famInst
debug_stuff = vcat [ ptext (sLit "Coercion axiom:") <+> ppr ax
, ptext (sLit "Tvs:") <+> ppr (fi_tvs famInst)
, ptext (sLit "LHS:") <+> ppr (fi_tys famInst)
, ptext (sLit "RHS:") <+> ppr (fi_rhs famInst) ]
pprFamInstHdr :: FamInst -> SDoc
pprFamInstHdr fi@(FamInst {fi_flavor = flavor})
......
......@@ -2,7 +2,15 @@ TOP=../../..
include $(TOP)/mk/boilerplate.mk
include $(TOP)/mk/test.mk
.PHONY: T1133
.PHONY: T1133 T11148
T11148:
$(RM) T11148.hi T11148.o
'$(TEST_HC)' $(TEST_HC_OPTS) -c -dunique-increment=-1 T11148.hs
# Set the unique-increment to '-1' to trigger the bug
# This has to be done on the command line;
# an OPTIONS_GHC pragma does not do it
T1133:
'$(TEST_HC)' $(TEST_HC_OPTS) -c T1133.hs-boot
'$(TEST_HC)' $(TEST_HC_OPTS) -c T1133a.hs
......
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE FlexibleInstances #-}
module T11148 where
data family G a b c d
data instance G Int b Float d = G deriving Functor
data family H a b c d
data instance H [b] b d c = H deriving Functor
......@@ -56,3 +56,5 @@ test('T4896', normal, compile, [''])
test('T7947', extra_clean(['T7947a.o', 'T7947a.hi', 'T7947b.o', 'T7947b.hi']), multimod_compile, ['T7947', '-v0'])
test('T10561', normal, compile_fail, [''])
test('T10487', extra_clean(['T10487_M.o', 'T10487_M.hi']), multimod_compile, ['T10487', '-v0'])
test('T11148', normal, run_command,
['$MAKE -s --no-print-directory T11148'])
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