[commit: ghc] master: A tiny, outright bug in tcDataFamInstDecl (e2f7d77)
git at git.haskell.org
git at git.haskell.org
Mon Feb 15 16:20:19 UTC 2016
Repository : ssh://git@git.haskell.org/ghc
On branch : master
Link : http://ghc.haskell.org/trac/ghc/changeset/e2f7d777bb7e4c176e01e1c4f8184f115253dee0/ghc
>---------------------------------------------------------------
commit e2f7d777bb7e4c176e01e1c4f8184f115253dee0
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date: Mon Feb 15 15:51:50 2016 +0000
A tiny, outright bug in tcDataFamInstDecl
This bug was revealed by Trac #11362. It turns out that in my patch
for Trac #11148 (namely 1160dc5), I failed to turn one occurrence of
tvs' into full_tvs. Sigh. This is tricky stuff and it cost me
several hours to page it back in and figure out what was happening.
The result was a CoAxiom whose lhs had rhs had different kinds. Eeek!
Anyway it's fixed.
I also added an ASSERT, in FamInst.newFamInst, that trips on such
bogus CoAxioms.
>---------------------------------------------------------------
e2f7d777bb7e4c176e01e1c4f8184f115253dee0
compiler/typecheck/FamInst.hs | 9 ++++++++-
compiler/typecheck/TcClassDcl.hs | 3 +--
compiler/typecheck/TcInstDcls.hs | 21 +++++++++++----------
testsuite/tests/polykinds/T6137.hs | 21 +++++++++++++++++++--
4 files changed, 39 insertions(+), 15 deletions(-)
diff --git a/compiler/typecheck/FamInst.hs b/compiler/typecheck/FamInst.hs
index e4b2cc3..c38f163 100644
--- a/compiler/typecheck/FamInst.hs
+++ b/compiler/typecheck/FamInst.hs
@@ -62,7 +62,10 @@ newFamInst :: FamFlavor -> CoAxiom Unbranched -> TcRnIf gbl lcl FamInst
-- Freshen the type variables of the FamInst branches
-- Called from the vectoriser monad too, hence the rather general type
newFamInst flavor axiom@(CoAxiom { co_ax_tc = fam_tc })
- = do { (subst, tvs') <- freshenTyVarBndrs tvs
+ = ASSERT2( tyCoVarsOfTypes lhs `subVarSet` tcv_set, text "lhs" <+> pp_ax )
+ ASSERT2( tyCoVarsOfType rhs `subVarSet` tcv_set, text "rhs" <+> pp_ax )
+ ASSERT2( lhs_kind `eqType` rhs_kind, text "kind" <+> pp_ax $$ ppr lhs_kind $$ ppr rhs_kind )
+ do { (subst, tvs') <- freshenTyVarBndrs tvs
; (subst, cvs') <- freshenCoVarBndrsX subst cvs
; return (FamInst { fi_fam = tyConName fam_tc
, fi_flavor = flavor
@@ -73,6 +76,10 @@ newFamInst flavor axiom@(CoAxiom { co_ax_tc = fam_tc })
, fi_rhs = substTy subst rhs
, fi_axiom = axiom }) }
where
+ lhs_kind = typeKind (mkTyConApp fam_tc lhs)
+ rhs_kind = typeKind rhs
+ tcv_set = mkVarSet (tvs ++ cvs)
+ pp_ax = pprCoAxiom axiom
CoAxBranch { cab_tvs = tvs
, cab_cvs = cvs
, cab_lhs = lhs
diff --git a/compiler/typecheck/TcClassDcl.hs b/compiler/typecheck/TcClassDcl.hs
index 40da199..1e84e4c 100644
--- a/compiler/typecheck/TcClassDcl.hs
+++ b/compiler/typecheck/TcClassDcl.hs
@@ -467,8 +467,7 @@ tcATDefault emit_warn loc inst_subst defined_ats (ATI fam_tc defs)
; traceTc "mk_deflt_at_instance" (vcat [ ppr fam_tc, ppr rhs_ty
, pprCoAxiom axiom ])
- ; fam_inst <- ASSERT( tyCoVarsOfType rhs' `subVarSet` tv_set' )
- newFamInst SynFamilyInst axiom
+ ; fam_inst <- newFamInst SynFamilyInst axiom
; return [fam_inst] }
-- No defaults ==> generate a warning
diff --git a/compiler/typecheck/TcInstDcls.hs b/compiler/typecheck/TcInstDcls.hs
index a94c102..fdc9e8d 100644
--- a/compiler/typecheck/TcInstDcls.hs
+++ b/compiler/typecheck/TcInstDcls.hs
@@ -671,7 +671,7 @@ tcDataFamInstDecl mb_clsinfo
-- (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, _) ->
+ ; (rep_tc, axiom) <- fixM $ \ ~(rec_rep_tc, _) ->
do { data_cons <- tcConDecls new_or_data
rec_rep_tc
(full_tvs, orig_res_ty) cons
@@ -684,23 +684,23 @@ tcDataFamInstDecl mb_clsinfo
axiom_name eta_tvs [] fam_tc eta_pats
(mkTyConApp rep_tc (mkTyVarTys eta_tvs))
parent = DataFamInstTyCon axiom fam_tc pats'
- kind = mkPiTypesPreferFunTy tvs' liftedTypeKind
-
+ rep_tc_kind = mkPiTypesPreferFunTy full_tvs liftedTypeKind
-- NB: Use the full_tvs from the pats. See bullet toward
-- the end of Note [Data type families] in TyCon
- rep_tc = mkAlgTyCon rep_tc_name kind full_tvs
- (map (const Nominal) full_tvs)
- (fmap unLoc cType) stupid_theta
- tc_rhs parent
- Recursive gadt_syntax
+ rep_tc = mkAlgTyCon rep_tc_name
+ rep_tc_kind
+ full_tvs
+ (map (const Nominal) full_tvs)
+ (fmap unLoc cType) stupid_theta
+ tc_rhs parent
+ Recursive gadt_syntax
-- 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
-- dependency. (2) They are always valid loop breakers as
-- they involve a coercion.
- ; fam_inst <- newFamInst (DataFamilyInst rep_tc) axiom
- ; return (rep_tc, fam_inst) }
+ ; return (rep_tc, axiom) }
-- Remember to check validity; no recursion to worry about here
; checkValidTyCon rep_tc
@@ -712,6 +712,7 @@ tcDataFamInstDecl mb_clsinfo
, di_preds = preds
, di_ctxt = tcMkDataFamInstCtxt decl }
+ ; fam_inst <- newFamInst (DataFamilyInst rep_tc) axiom
; return (fam_inst, m_deriv_info) } }
where
eta_reduce :: [Type] -> ([Type], [TyVar])
diff --git a/testsuite/tests/polykinds/T6137.hs b/testsuite/tests/polykinds/T6137.hs
index dafe9a2..aac4c1c 100644
--- a/testsuite/tests/polykinds/T6137.hs
+++ b/testsuite/tests/polykinds/T6137.hs
@@ -17,9 +17,26 @@ data Code i o = F (Code (Sum i o) o)
-- An interpretation for `Code` using a data family works:
data family In (f :: Code i o) :: (i -> *) -> (o -> *)
-data instance In (F f) r o where
- MkIn :: In f (Sum1 r (In (F f) r)) o -> In (F f) r o
+data instance In (F f) r x where
+ MkIn :: In f (Sum1 r (In (F f) r)) x -> In (F f) r x
+
+{- data R:InioFrx o i f r x where
+ where MkIn :: forall o i (f :: Code (Sum i o) o) (r :: i -> *) (x :: o).
+ In (Sum i o) o f (Sum1 o i r (In i o ('F i o f) r)) x
+ -> R:InioFrx o i f r x
+
+ So R:InioFrx :: forall o i. Code i o -> (i -> *) -> o -> *
+
+ data family In i o (f :: Code i o) (a :: i -> *) (b :: o)
+
+ axiom D:R:InioFrx0 ::
+ forall o i (f :: Code (Sum i o) o).
+ In i o ('F i o f) = R:InioFrx o i f
+
+
+ D:R:InioFrx0 :: R:InioFrx o i f ~ In i o ('F i o f)
+-}
-- Requires polymorphic recursion
data In' (f :: Code i o) :: (i -> *) -> o -> * where
MkIn' :: In' g (Sum1 r (In' (F g) r)) t -> In' (F g) r t
More information about the ghc-commits
mailing list