diff options
6 files changed, 81 insertions, 15 deletions
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs index 114d839df5..8b5142158d 100644 --- a/compiler/typecheck/TcTyClsDecls.hs +++ b/compiler/typecheck/TcTyClsDecls.hs @@ -73,7 +73,9 @@ import BasicTypes import qualified GHC.LanguageExtensions as LangExt import Control.Monad +import Data.Foldable import Data.List +import qualified Data.List.NonEmpty as NE import Data.List.NonEmpty ( NonEmpty(..) ) import qualified Data.Set as Set @@ -1544,13 +1546,15 @@ tcDefaultAssocDecl fam_tc [dL->L loc (FamEqn { feqn_tycon = L _ tc_name hs_pats hs_rhs_ty ; let fam_tvs = tyConTyVars fam_tc + ppr_eqn = ppr_default_eqn pats rhs_ty ; traceTc "tcDefaultAssocDecl 2" (vcat [ text "fam_tvs" <+> ppr fam_tvs , text "qtvs" <+> ppr qtvs , text "pats" <+> ppr pats , text "rhs_ty" <+> ppr rhs_ty ]) - ; pat_tvs <- traverse (extract_tv pats rhs_ty) pats + ; pat_tvs <- traverse (extract_tv ppr_eqn) pats + ; check_all_distinct_tvs ppr_eqn pat_tvs ; let subst = zipTvSubst pat_tvs (mkTyVarTys fam_tvs) ; pure $ Just (substTyUnchecked subst rhs_ty, loc) -- We also perform other checks for well-formedness and validity @@ -1561,14 +1565,12 @@ tcDefaultAssocDecl fam_tc [dL->L loc (FamEqn { feqn_tycon = L _ tc_name -- variable. If so, return the underlying type variable, and if -- not, throw an error. -- See Note [Type-checking default assoc decls] - extract_tv :: [Type] -- All default instance type patterns - -- (only used for error message purposes) - -> Type -- The default instance's right-hand side type + extract_tv :: SDoc -- The pretty-printed default equation -- (only used for error message purposes) -> Type -- The particular type pattern from which to extract -- its underlying type variable -> TcM TyVar - extract_tv pats rhs_ty pat = + extract_tv ppr_eqn pat = case getTyVar_maybe pat of Just tv -> pure tv Nothing -> @@ -1579,10 +1581,39 @@ tcDefaultAssocDecl fam_tc [dL->L loc (FamEqn { feqn_tycon = L _ tc_name -- error message with -fprint-explicit-kinds enabled. failWithTc $ pprWithExplicitKindsWhen True $ hang (text "Illegal argument" <+> quotes (ppr pat) <+> text "in:") - 2 (vcat [ quotes (text "type" <+> ppr (mkTyConApp fam_tc pats) - <+> equals <+> ppr rhs_ty) - , text "The arguments to" <+> quotes (ppr fam_tc) - <+> text "must all be type variables" ]) + 2 (vcat [ppr_eqn, suggestion]) + + + -- Checks that no type variables in an associated default declaration are + -- duplicated. If that is the case, throw an error. + -- See Note [Type-checking default assoc decls] + check_all_distinct_tvs :: SDoc -- The pretty-printed default equation + -- (only used for error message purposes) + -> [TyVar] -- The type variable arguments in the + -- associated default declaration + -> TcM () + check_all_distinct_tvs ppr_eqn tvs = + let dups = findDupsEq (==) tvs in + traverse_ + (\d -> -- Per Note [Type-checking default assoc decls], we already + -- know by this point that if any arguments in the default + -- instance are duplicates, then they must be + -- invisible kind arguments. Therefore, always display the + -- error message with -fprint-explicit-kinds enabled. + failWithTc $ pprWithExplicitKindsWhen True $ + hang (text "Illegal duplicate variable" + <+> quotes (ppr (NE.head d)) <+> text "in:") + 2 (vcat [ppr_eqn, suggestion])) + dups + + ppr_default_eqn :: [Type] -> Type -> SDoc + ppr_default_eqn pats rhs_ty = + quotes (text "type" <+> ppr (mkTyConApp fam_tc pats) + <+> equals <+> ppr rhs_ty) + + suggestion :: SDoc + suggestion = text "The arguments to" <+> quotes (ppr fam_tc) + <+> text "must all be distinct type variables" tcDefaultAssocDecl _ [dL->L _ (XFamEqn _)] = panic "tcDefaultAssocDecl" tcDefaultAssocDecl _ [dL->L _ (FamEqn _ _ _ (XLHsQTyVars _) _ _)] = panic "tcDefaultAssocDecl" @@ -1610,10 +1641,15 @@ We do this by creating a substitution [j |-> k, x |-> a, b |-> y] and applying this substitution to the RHS. In order to create this substitution, we must first ensure that all of -the arguments in the default instance consist of type variables. The parser -already checks this to a certain degree (see RdrHsSyn.checkTyVars), but -we must be wary of kind arguments being instantiated, which the parser cannot -catch so easily. Consider this erroneous program (inspired by #11361): +the arguments in the default instance consist of distinct type variables. +This property has already been checked to some degree earlier in the compiler: +RdrHsSyn.checkTyVars ensures that all visible type arguments are type +variables, and RnTypes.bindLHsTyVarBndrs ensures that no visible type arguments +are duplicated. But these only check /visible/ arguments, however, so we still +must check the invisible kind arguments to see if these invariants are upheld. + +First, we must check that all arguments are type variables. As a motivating +example, consider this erroneous program (inspired by #11361): class C a where type F (a :: k) b :: Type @@ -1622,6 +1658,19 @@ catch so easily. Consider this erroneous program (inspired by #11361): If you squint, you'll notice that the kind of `x` is actually Type. However, we cannot substitute from [Type |-> k], so we reject this default. +Next, we must check that all arguments are distinct. Here is another offending +example, this time taken from #13971: + + class C2 (a :: j) where + type F2 (a :: j) (b :: k) + type F2 (x :: z) (y :: z) = z + +All of the arguments in the default equation for `F2` are type variables, so +that passes the first check. However, if we were to build this substitution, +then both `j` and `k` map to `z`! In terms of visible kind application, it's as +if we had written `type F2 @z @z x y = z`, which makes it clear that we have +duplicated a use of `z`. Therefore, `F2`'s default is also rejected. + Since the LHS of an associated type family default is always just variables, it won't contain any tycons. Accordingly, the patterns used in the substitution won't actually be knot-tied, even though we're in the knot. This is too diff --git a/testsuite/tests/indexed-types/should_compile/T11361a.stderr b/testsuite/tests/indexed-types/should_compile/T11361a.stderr index bf6d22c4df..a3e3a22a31 100644 --- a/testsuite/tests/indexed-types/should_compile/T11361a.stderr +++ b/testsuite/tests/indexed-types/should_compile/T11361a.stderr @@ -2,6 +2,6 @@ T11361a.hs:7:3: error: • Illegal argument ‘*’ in: ‘type F @* x = x’ - The arguments to ‘F’ must all be type variables + The arguments to ‘F’ must all be distinct type variables • In the default type instance declaration for ‘F’ In the class declaration for ‘C’ diff --git a/testsuite/tests/indexed-types/should_fail/T13971.stderr b/testsuite/tests/indexed-types/should_fail/T13971.stderr index df1a6bae3e..eec7ad11e6 100644 --- a/testsuite/tests/indexed-types/should_fail/T13971.stderr +++ b/testsuite/tests/indexed-types/should_fail/T13971.stderr @@ -2,6 +2,6 @@ T13971.hs:7:3: error: • Illegal argument ‘*’ in: ‘type T @{k} @* a = Int’ - The arguments to ‘T’ must all be type variables + The arguments to ‘T’ must all be distinct type variables • In the default type instance declaration for ‘T’ In the class declaration for ‘C’ diff --git a/testsuite/tests/indexed-types/should_fail/T13971b.hs b/testsuite/tests/indexed-types/should_fail/T13971b.hs new file mode 100644 index 0000000000..1df11cc545 --- /dev/null +++ b/testsuite/tests/indexed-types/should_fail/T13971b.hs @@ -0,0 +1,9 @@ +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE TypeFamilies #-} +module T13971b where + +import Data.Kind + +class C (a :: j) where + type T (a :: j) (b :: k) + type T (a :: k) (b :: k) = k diff --git a/testsuite/tests/indexed-types/should_fail/T13971b.stderr b/testsuite/tests/indexed-types/should_fail/T13971b.stderr new file mode 100644 index 0000000000..cf64125fbb --- /dev/null +++ b/testsuite/tests/indexed-types/should_fail/T13971b.stderr @@ -0,0 +1,7 @@ + +T13971b.hs:9:3: error: + • Illegal duplicate variable ‘k’ in: + ‘type T @k @k a b = k’ + The arguments to ‘T’ must all be distinct type variables + • In the default type instance declaration for ‘T’ + In the class declaration for ‘C’ diff --git a/testsuite/tests/indexed-types/should_fail/all.T b/testsuite/tests/indexed-types/should_fail/all.T index 27c1f5ac37..e154a31dd0 100644 --- a/testsuite/tests/indexed-types/should_fail/all.T +++ b/testsuite/tests/indexed-types/should_fail/all.T @@ -137,6 +137,7 @@ test('T13674', normal, compile_fail, ['']) test('T13784', normal, compile_fail, ['']) test('T13877', normal, compile_fail, ['']) test('T13971', normal, compile_fail, ['']) +test('T13971b', normal, compile_fail, ['']) test('T13972', normal, compile, ['']) test('T14033', normal, compile_fail, ['']) test('T14045a', normal, compile, ['']) |