Commit 827cc509 authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Eta-reduce data/newtype family instance axioms (Trac #4185)

This long-overdue fix arranges to eta-reduce the axiom for a
data/newtype instance in the same way that we have longq
eta-reduced the axiom for a newtype.

See Note [Eta reduction for data family axioms] in TcInstDcls
and Note [Deriving, type families, and partial applications] in TcDeriv.
parent 936001ca
......@@ -11,7 +11,7 @@ The @FamInst@ type: family instance heads
module FamInst (
checkFamInstConsistency, tcExtendLocalFamInstEnv,
tcLookupFamInst, tcLookupDataFamInst,
tcLookupFamInst,
tcGetFamInstEnvs,
newFamInst
) where
......@@ -231,55 +231,8 @@ tcLookupFamInst tycon tys
(match:_)
-> return $ Just match
}
tcLookupDataFamInst :: TyCon -> [Type] -> TcM (TyCon, [Type])
-- Find the instance of a data family
-- Note [Looking up family instances for deriving]
tcLookupDataFamInst tycon tys
| not (isFamilyTyCon tycon)
= return (tycon, tys)
| otherwise
= ASSERT( isAlgTyCon tycon )
do { maybeFamInst <- tcLookupFamInst tycon tys
; case maybeFamInst of
Nothing -> famInstNotFound tycon tys
Just (FamInstMatch { fim_instance = famInst
, fim_index = index
, fim_tys = tys })
-> ASSERT( index == 0 )
let tycon' = dataFamInstRepTyCon famInst
in return (tycon', tys) }
famInstNotFound :: TyCon -> [Type] -> TcM a
famInstNotFound tycon tys
= failWithTc (ptext (sLit "No family instance for")
<+> quotes (pprTypeApp tycon tys))
\end{code}
Note [Looking up family instances for deriving]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
tcLookupFamInstExact is an auxiliary lookup wrapper which requires
that looked-up family instances exist. If called with a vanilla
tycon, the old type application is simply returned.
If we have
data instance F () = ... deriving Eq
data instance F () = ... deriving Eq
then tcLookupFamInstExact will be confused by the two matches;
but that can't happen because tcInstDecls1 doesn't call tcDeriving
if there are any overlaps.
There are two other things that might go wrong with the lookup.
First, we might see a standalone deriving clause
deriving Eq (F ())
when there is no data instance F () in scope.
Note that it's OK to have
data instance F [a] = ...
deriving Eq (F [(a,b)])
where the match is not exact; the same holds for ordinary data types
with standalone deriving declrations.
%************************************************************************
%* *
......
......@@ -591,8 +591,8 @@ deriveStandalone (L loc (DerivDecl deriv_ty))
(Just theta) }
------------------------------------------------------------------
deriveTyData :: [TyVar] -> TyCon -> [Type]
-> LHsType Name -- The deriving predicate
deriveTyData :: [TyVar] -> TyCon -> [Type] -- LHS of data or data instance
-> LHsType Name -- The deriving predicate
-> TcM EarlyDerivSpec
-- The deriving clause of a data or newtype declaration
deriveTyData tvs tc tc_args (L loc deriv_pred)
......@@ -625,7 +625,7 @@ deriveTyData tvs tc tc_args (L loc deriv_pred)
args_to_drop = drop n_args_to_keep tc_args
inst_ty = mkTyConApp tc (take n_args_to_keep tc_args)
inst_ty_kind = typeKind inst_ty
dropped_tvs = mkVarSet (mapCatMaybes getTyVar_maybe args_to_drop)
dropped_tvs = tyVarsOfTypes args_to_drop
univ_tvs = (mkVarSet tvs `extendVarSetList` deriv_tvs)
`minusVarSet` dropped_tvs
......@@ -636,22 +636,19 @@ deriveTyData tvs tc tc_args (L loc deriv_pred)
; checkTc (n_args_to_keep >= 0 && (inst_ty_kind `eqKind` kind))
(derivingKindErr tc cls cls_tys kind)
; checkTc (sizeVarSet dropped_tvs == n_args_to_drop && -- (a)
tyVarsOfTypes (inst_ty:cls_tys) `subVarSet` univ_tvs) -- (b)
; checkTc (all isTyVarTy args_to_drop && -- (a)
sizeVarSet dropped_tvs == n_args_to_drop && -- (b)
tyVarsOfTypes (inst_ty:cls_tys) `subVarSet` univ_tvs) -- (c)
(derivingEtaErr cls cls_tys inst_ty)
-- Check that
-- (a) The args to drop are all type variables; eg reject:
-- data instance T a Int = .... deriving( Monad )
-- (a) The data type can be eta-reduced; eg reject:
-- data instance T a a = ... deriving( Monad )
-- (b) The type class args do not mention any of the dropped type
-- variables
-- newtype T a s = ... deriving( ST s )
-- Type families can't be partially applied
-- e.g. newtype instance T Int a = MkT [a] deriving( Monad )
-- Note [Deriving, type families, and partial applications]
; checkTc (not (isFamilyTyCon tc) || n_args_to_drop == 0)
(typeFamilyPapErr tc cls cls_tys inst_ty)
; mkEqnHelp DerivOrigin (varSetElemsKvsFirst univ_tvs) cls cls_tys inst_ty Nothing } }
where
kindVarsOnly :: [Type] -> [Type]
......@@ -661,33 +658,6 @@ deriveTyData tvs tc tc_args (L loc deriv_pred)
| otherwise = kindVarsOnly ts
\end{code}
Note [Deriving, type families, and partial applications]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When there are no type families, it's quite easy:
newtype S a = MkS [a]
-- :CoS :: S ~ [] -- Eta-reduced
instance Eq [a] => Eq (S a) -- by coercion sym (Eq (:CoS a)) : Eq [a] ~ Eq (S a)
instance Monad [] => Monad S -- by coercion sym (Monad :CoS) : Monad [] ~ Monad S
When type familes are involved it's trickier:
data family T a b
newtype instance T Int a = MkT [a] deriving( Eq, Monad )
-- :RT is the representation type for (T Int a)
-- :CoF:R1T a :: T Int a ~ :RT a -- Not eta reduced
-- :Co:R1T :: :RT ~ [] -- Eta-reduced
instance Eq [a] => Eq (T Int a) -- easy by coercion
instance Monad [] => Monad (T Int) -- only if we can eta reduce???
The "???" bit is that we don't build the :CoF thing in eta-reduced form
Henc the current typeFamilyPapErr, even though the instance makes sense.
After all, we can write it out
instance Monad [] => Monad (T Int) -- only if we can eta reduce???
return x = MkT [x]
... etc ...
\begin{code}
mkEqnHelp :: CtOrigin -> [TyVar] -> Class -> [Type] -> Type
......@@ -704,6 +674,7 @@ mkEqnHelp orig tvs cls cls_tys tc_app mtheta
, className cls == typeableClassName || isAlgTyCon tycon
-- Avoid functions, primitive types, etc, unless it's Typeable
= mk_alg_eqn tycon tc_args
| otherwise
= failWithTc (derivingThingErr False cls cls_tys tc_app
(ptext (sLit "The last argument of the instance must be a data or newtype application")))
......@@ -722,12 +693,8 @@ mkEqnHelp orig tvs cls cls_tys tc_app mtheta
-- We checked for errors before, so we don't need to do that again
= mkPolyKindedTypeableEqn orig tvs cls cls_tys tycon tc_args mtheta
| isDataFamilyTyCon tycon
, length tc_args /= tyConArity tycon
= bale_out (ptext (sLit "Unsaturated data family application"))
| otherwise
= do { (rep_tc, rep_tc_args) <- tcLookupDataFamInst tycon tc_args
= do { (rep_tc, rep_tc_args) <- lookup_data_fam tycon tc_args
-- Be careful to test rep_tc here: in the case of families,
-- we want to check the instance tycon, not the family tycon
......@@ -748,8 +715,85 @@ mkEqnHelp orig tvs cls cls_tys tc_app mtheta
else
mkNewTypeEqn orig dflags tvs cls cls_tys
tycon tc_args rep_tc rep_tc_args mtheta }
lookup_data_fam :: TyCon -> [Type] -> TcM (TyCon, [Type])
-- Find the instance of a data family
-- Note [Looking up family instances for deriving]
lookup_data_fam tycon tys
| not (isFamilyTyCon tycon)
= return (tycon, tys)
| otherwise
= ASSERT( isAlgTyCon tycon )
do { maybeFamInst <- tcLookupFamInst tycon tys
; case maybeFamInst of
Nothing -> bale_out (ptext (sLit "No family instance for")
<+> quotes (pprTypeApp tycon tys))
Just (FamInstMatch { fim_instance = famInst
, fim_index = index
, fim_tys = tys })
-> ASSERT( index == 0 )
let tycon' = dataFamInstRepTyCon famInst
in return (tycon', tys) }
\end{code}
Note [Looking up family instances for deriving]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
tcLookupFamInstExact is an auxiliary lookup wrapper which requires
that looked-up family instances exist. If called with a vanilla
tycon, the old type application is simply returned.
If we have
data instance F () = ... deriving Eq
data instance F () = ... deriving Eq
then tcLookupFamInstExact will be confused by the two matches;
but that can't happen because tcInstDecls1 doesn't call tcDeriving
if there are any overlaps.
There are two other things that might go wrong with the lookup.
First, we might see a standalone deriving clause
deriving Eq (F ())
when there is no data instance F () in scope.
Note that it's OK to have
data instance F [a] = ...
deriving Eq (F [(a,b)])
where the match is not exact; the same holds for ordinary data types
with standalone deriving declarations.
Note [Deriving, type families, and partial applications]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When there are no type families, it's quite easy:
newtype S a = MkS [a]
-- :CoS :: S ~ [] -- Eta-reduced
instance Eq [a] => Eq (S a) -- by coercion sym (Eq (:CoS a)) : Eq [a] ~ Eq (S a)
instance Monad [] => Monad S -- by coercion sym (Monad :CoS) : Monad [] ~ Monad S
When type familes are involved it's trickier:
data family T a b
newtype instance T Int a = MkT [a] deriving( Eq, Monad )
-- :RT is the representation type for (T Int a)
-- :Co:RT :: :RT ~ [] -- Eta-reduced!
-- :CoF:RT a :: T Int a ~ :RT a -- Also eta-reduced!
instance Eq [a] => Eq (T Int a) -- easy by coercion
-- d1 :: Eq [a]
-- d2 :: Eq (T Int a) = d1 |> Eq (sym (:Co:RT a ; :coF:RT a))
instance Monad [] => Monad (T Int) -- only if we can eta reduce???
-- d1 :: Monad []
-- d2 :: Monad (T Int) = d1 |> Monad (sym (:Co:RT ; :coF:RT))
Note the need for the eta-reduced rule axioms. After all, we can
write it out
instance Monad [] => Monad (T Int) -- only if we can eta reduce???
return x = MkT [x]
... etc ...
See Note [Eta reduction for data family axioms] in TcInstDcls.
%************************************************************************
%* *
......@@ -1843,11 +1887,6 @@ derivingEtaErr cls cls_tys inst_ty
nest 2 (ptext (sLit "instance (...) =>")
<+> pprClassPred cls (cls_tys ++ [inst_ty]))]
typeFamilyPapErr :: TyCon -> Class -> [Type] -> Type -> MsgDoc
typeFamilyPapErr tc cls cls_tys inst_ty
= hang (ptext (sLit "Derived instance") <+> quotes (pprClassPred cls (cls_tys ++ [inst_ty])))
2 (ptext (sLit "requires illegal partial application of data type family") <+> ppr tc)
derivingThingErr :: Bool -> Class -> [Type] -> Type -> MsgDoc -> MsgDoc
derivingThingErr newtype_deriving clas tys ty why
= sep [(hang (ptext (sLit "Can't make a derived instance of"))
......
......@@ -50,7 +50,7 @@ import DataCon
import Class
import Var
import VarEnv
import VarSet ( mkVarSet, subVarSet, varSetElems )
import VarSet
import Pair
import CoreUnfold ( mkDFunUnfolding )
import CoreSyn ( Expr(Var, Type), CoreExpr, mkTyApps, mkVarApps )
......@@ -712,8 +712,9 @@ tcDataFamInstDecl mb_clsinfo
NewType -> ASSERT( not (null data_cons) )
mkNewTyConRhs rep_tc_name rec_rep_tc (head data_cons)
-- freshen tyvars
; let axiom = mkSingleCoAxiom axiom_name tvs' fam_tc pats'
(mkTyConApp rep_tc (mkTyVarTys tvs'))
; let (eta_tvs, eta_pats) = eta_reduce tvs' pats'
axiom = mkSingleCoAxiom axiom_name eta_tvs fam_tc eta_pats
(mkTyConApp rep_tc (mkTyVarTys eta_tvs))
parent = FamInstTyCon axiom fam_tc pats'
rep_tc = buildAlgTyCon rep_tc_name tvs' cType stupid_theta tc_rhs
Recursive
......@@ -730,8 +731,44 @@ tcDataFamInstDecl mb_clsinfo
-- Remember to check validity; no recursion to worry about here
; checkValidTyCon rep_tc
; return fam_inst } }
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'
, not (tv `elemVarSet` tyVarsOfTypes pats)
= go tvs pats
go tvs pats = (reverse tvs, reverse pats)
\end{code}
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))
See Note [Newtype eta] in TyCon.
%************************************************************************
%* *
Type-checking instance declarations, pass 2
......
......@@ -133,10 +133,14 @@ data FamInstBranch
-- Like ClsInsts, these variables are always
-- fresh. See Note [Template tyvars are fresh]
-- in InstEnv
, fib_lhs :: [Type] -- type patterns
, fib_lhs :: [Type] -- Type patterns
, fib_rhs :: Type -- RHS of family instance
-- See Note [Why we need fib_rhs]
, fib_tcs :: [Maybe Name] -- used for "rough matching" during typechecking
, fib_tcs :: [Maybe Name] -- Used for "rough matching" during typechecking
-- In 1-1 correspondence with fib_lhs
-- see Note [Rough-match field] in InstEnv
}
......@@ -316,7 +320,7 @@ mkImportedFamInst fam branched roughs axiom
%************************************************************************
Note [FamInstEnv]
~~~~~~~~~~~~~~~~~~~~~
~~~~~~~~~~~~~~~~~
A FamInstEnv maps a family name to the list of known instances for that family.
The same FamInstEnv includes both 'data family' and 'type family' instances.
......@@ -334,6 +338,25 @@ Neverthless it is still useful to have data families in the FamInstEnv:
- In standalone deriving instance Eq (T [Int]) we need to find the
representation type for T [Int]
Note [Varying number of patterns for data family axioms]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
For data families, the number of patterns may vary between instances.
For example
data family T a b
data instance T Int a = T1 a | T2
data instance T Bool [a] = T3 a
Then we get a data type for each instance, and an axiom:
data TInt a = T1 a | T2
data TBoolList a = T3 a
axiom ax7 :: T Int ~ TInt -- Eta-reduced
axiom ax8 a :: T Bool [a] ~ TBoolList a
These two axioms for T, one with one pattern, one with two. The reason
for this eta-reduction is decribed in TcInstDcls
Note [Eta reduction for data family axioms]
\begin{code}
type FamInstEnv = UniqFM FamilyInstEnv -- Maps a family to its instances
-- See Note [FamInstEnv]
......@@ -701,21 +724,8 @@ lookup_fam_inst_env' -- The worker, local to this module
lookup_fam_inst_env' match_fun _one_sided ie fam tys
| isFamilyTyCon fam
, Just (FamIE insts) <- lookupUFM ie fam
= ASSERT2( n_tys >= arity, ppr fam <+> ppr tys )
if arity < n_tys then -- Family type applications must be saturated
-- See Note [Over-saturated matches]
map wrap_extra_tys (find match_fun (take arity tys) insts)
else
find match_fun tys insts -- The common case
= find match_fun tys insts -- The common case
| otherwise = []
where
arity = tyConArity fam
n_tys = length tys
extra_tys = drop arity tys
wrap_extra_tys fim@(FamInstMatch { fim_tys = match_tys })
= fim { fim_tys = match_tys ++ extra_tys }
find :: MatchFun -> [Type] -> [FamInst Branched] -> [FamInstMatch]
find _ _ [] = []
......@@ -737,14 +747,20 @@ find match_fun match_tys (inst@(FamInst { fi_branches = branches, fi_branched =
| instanceCantMatch rough_tcs mb_tcs
= findBranch seen rest (ind+1) -- branch won't unify later; no need to add to 'seen'
| otherwise
= case match_fun seen branch is_branched match_tys of
= case match_fun seen branch is_branched match_tys1 of
(Nothing, KeepSearching) -> findBranch (branch : seen) rest (ind+1)
(Nothing, StopSearching) -> (Nothing, StopSearching)
(Just subst, cont) -> (Just match, cont)
where
match = FamInstMatch { fim_instance = inst
, fim_index = ind
, fim_tys = substTyVars subst tvs }
, fim_tys = substTyVars subst tvs `add_on` match_tys2}
where
-- Deal with over-saturation
-- See Note [Over-saturated matches]
(match_tys1, match_tys2) = splitAtList mb_tcs match_tys
add_on tys1 [] = tys1 -- The wildly common case
add_on tys1 tys2 = tys1 ++ tys2
lookup_fam_inst_env -- The worker, local to this module
:: MatchFun
......@@ -851,7 +867,6 @@ topNormaliseType env ty
normaliseTcApp :: FamInstEnvs -> TyCon -> [Type] -> (Coercion, Type)
normaliseTcApp env tc tys
| isFamilyTyCon tc
, tyConArity tc <= length tys -- Unsaturated data families are possible
, [FamInstMatch { fim_instance = fam_inst
, fim_index = fam_ind
, fim_tys = inst_tys }] <- lookupFamInstEnv env tc ntys
......
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