From 9462d0b632c106d1aca2bee7a68a513c119c208f Mon Sep 17 00:00:00 2001 From: Krzysztof Gogolewski Date: Sat, 21 Aug 2021 00:42:00 +0200 Subject: Reject type family equation with wrong name (#20260) We should reject "type family Foo where Bar = ()". This check was done in kcTyFamInstEqn but not in tcTyFamInstEqn. I factored out arity checking, which was duplicated. --- compiler/GHC/Tc/TyCl.hs | 49 +++++++++++----------- testsuite/tests/typecheck/should_fail/T20260.hs | 8 ++++ .../tests/typecheck/should_fail/T20260.stderr | 6 +++ testsuite/tests/typecheck/should_fail/all.T | 1 + 4 files changed, 39 insertions(+), 25 deletions(-) create mode 100644 testsuite/tests/typecheck/should_fail/T20260.hs create mode 100644 testsuite/tests/typecheck/should_fail/T20260.stderr diff --git a/compiler/GHC/Tc/TyCl.hs b/compiler/GHC/Tc/TyCl.hs index 08370c2a89..968baad524 100644 --- a/compiler/GHC/Tc/TyCl.hs +++ b/compiler/GHC/Tc/TyCl.hs @@ -2985,32 +2985,19 @@ kcTyFamInstEqn tc_fam_tc , text "fam_tc =" <+> ppr tc_fam_tc <+> dcolon <+> ppr (tyConKind tc_fam_tc) , text "feqn_bndrs =" <+> ppr outer_bndrs , text "feqn_pats =" <+> ppr hs_pats ]) - -- this check reports an arity error instead of a kind error; easier for user - ; let vis_pats = numVisibleArgs hs_pats - -- First, check if we're dealing with a closed type family equation, and - -- if so, ensure that each equation's type constructor is for the right - -- type family. E.g. barf on - -- type family F a where { G Int = Bool } - ; checkTc (tc_fam_tc_name == eqn_tc_name) $ - wrongTyFamName tc_fam_tc_name eqn_tc_name - - ; checkTc (vis_pats == vis_arity) $ - wrongNumberOfParmsErr vis_arity + ; checkTyFamInstEqn tc_fam_tc eqn_tc_name hs_pats ; discardResult $ bindOuterFamEqnTKBndrs_Q_Tv outer_bndrs $ do { (_fam_app, res_kind) <- tcFamTyPats tc_fam_tc hs_pats ; tcCheckLHsType hs_rhs_ty (TheKind res_kind) } - -- Why "_Tv" here? Consider (#14066 + -- Why "_Tv" here? Consider (#14066) -- type family Bar x y where -- Bar (x :: a) (y :: b) = Int -- Bar (x :: c) (y :: d) = Bool -- During kind-checking, a,b,c,d should be TyVarTvs and unify appropriately } - where - vis_arity = length (tyConVisibleTyVars tc_fam_tc) - tc_fam_tc_name = getName tc_fam_tc -------------------------- tcTyFamInstEqn :: TcTyCon -> AssocInstInfo -> LTyFamInstEqn GhcRn @@ -3019,7 +3006,8 @@ tcTyFamInstEqn :: TcTyCon -> AssocInstInfo -> LTyFamInstEqn GhcRn -- (typechecked here) have TyFamInstEqns tcTyFamInstEqn fam_tc mb_clsinfo - (L loc (FamEqn { feqn_bndrs = outer_bndrs + (L loc (FamEqn { feqn_tycon = L _ eqn_tc_name + , feqn_bndrs = outer_bndrs , feqn_pats = hs_pats , feqn_rhs = hs_rhs_ty })) = setSrcSpanA loc $ @@ -3030,15 +3018,8 @@ tcTyFamInstEqn fam_tc mb_clsinfo NotAssociated {} -> empty InClsInst { ai_class = cls } -> text "class" <+> ppr cls <+> pprTyVars (classTyVars cls) ] - -- First, check the arity of visible arguments - -- If we wait until validity checking, we'll get kind errors - -- below when an arity error will be much easier to understand. - -- Note that for closed type families, kcTyFamInstEqn has already - -- checked the arity previously. - ; let vis_arity = length (tyConVisibleTyVars fam_tc) - vis_pats = numVisibleArgs hs_pats - ; checkTc (vis_pats == vis_arity) $ - wrongNumberOfParmsErr vis_arity + ; checkTyFamInstEqn fam_tc eqn_tc_name hs_pats + ; (qtvs, pats, rhs_ty) <- tcTyFamInstEqnGuts fam_tc mb_clsinfo outer_bndrs hs_pats hs_rhs_ty -- Don't print results they may be knot-tied @@ -3047,6 +3028,24 @@ tcTyFamInstEqn fam_tc mb_clsinfo (map (const Nominal) qtvs) (locA loc)) } +checkTyFamInstEqn :: TcTyCon -> Name -> [HsArg tm ty] -> TcM () +checkTyFamInstEqn tc_fam_tc eqn_tc_name hs_pats = + do { -- Ensure that each equation's type constructor is for the right + -- type family. E.g. barf on + -- type family F a where { G Int = Bool } + let tc_fam_tc_name = getName tc_fam_tc + ; checkTc (tc_fam_tc_name == eqn_tc_name) $ + wrongTyFamName tc_fam_tc_name eqn_tc_name + + -- Check the arity of visible arguments + -- If we wait until validity checking, we'll get kind errors + -- below when an arity error will be much easier to understand. + ; let vis_arity = length (tyConVisibleTyVars tc_fam_tc) + vis_pats = numVisibleArgs hs_pats + ; checkTc (vis_pats == vis_arity) $ + wrongNumberOfParmsErr vis_arity + } + {- Note [Instantiating a family tycon] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ It's possible that kind-checking the result of a family tycon applied to diff --git a/testsuite/tests/typecheck/should_fail/T20260.hs b/testsuite/tests/typecheck/should_fail/T20260.hs new file mode 100644 index 0000000000..1e828f9123 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T20260.hs @@ -0,0 +1,8 @@ +{-# LANGUAGE TypeFamilies, StandaloneKindSignatures #-} +module T20260 where + +data Bar + +type Foo :: * +type family Foo where + Bar = () diff --git a/testsuite/tests/typecheck/should_fail/T20260.stderr b/testsuite/tests/typecheck/should_fail/T20260.stderr new file mode 100644 index 0000000000..574d72163d --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T20260.stderr @@ -0,0 +1,6 @@ + +T20260.hs:8:3: error: + • Mismatched type name in type family instance. + Expected: Foo + Actual: Bar + • In the type family declaration for ‘Foo’ diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T index 20b30d3deb..c5a89afc90 100644 --- a/testsuite/tests/typecheck/should_fail/all.T +++ b/testsuite/tests/typecheck/should_fail/all.T @@ -636,4 +636,5 @@ test('T17817_elab', normal, compile_fail, ['-fprint-typechecker-elaboration']) test('T19978', normal, compile_fail, ['']) test('T20122', normal, compile_fail, ['']) test('T20241b', normal, compile_fail, ['']) +test('T20260', normal, compile_fail, ['']) test('OrdErr', normal, compile_fail, ['']) -- cgit v1.2.1