diff options
| -rw-r--r-- | compiler/typecheck/FamInst.hs | 9 | ||||
| -rw-r--r-- | compiler/typecheck/TcClassDcl.hs | 3 | ||||
| -rw-r--r-- | compiler/typecheck/TcInstDcls.hs | 21 | ||||
| -rw-r--r-- | 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 e4b2cc3517..c38f163ab8 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 40da199497..1e84e4c8d9 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 a94c102939..fdc9e8d00e 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 dafe9a21e9..aac4c1c8b6 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 |