Commit e2f7d777 authored by Simon Peyton Jones's avatar Simon Peyton Jones

A tiny, outright bug in tcDataFamInstDecl

This bug was revealed by Trac #11362.  It turns out that in my patch
for Trac #11148 (namely 1160dc51), 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.
parent 00571252
......@@ -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
......
......@@ -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
......
......@@ -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])
......
......@@ -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
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