[Git][ghc/ghc][master] Check for duplicate variables in associated default equations
Marge Bot
gitlab at gitlab.haskell.org
Tue May 7 21:09:10 UTC 2019
Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC
Commits:
78a5c4ce by Ryan Scott at 2019-05-07T21:03:04Z
Check for duplicate variables in associated default equations
A follow-up to !696's, which attempted to clean up the error messages
for ill formed associated type family default equations. The previous
attempt, !696, forgot to account for the possibility of duplicate
kind variable arguments, as in the following example:
```hs
class C (a :: j) where
type T (a :: j) (b :: k)
type T (a :: k) (b :: k) = k
```
This patch addresses this shortcoming by adding an additional check
for this. Fixes #13971 (hopefully for good this time).
- - - - -
6 changed files:
- compiler/typecheck/TcTyClsDecls.hs
- testsuite/tests/indexed-types/should_compile/T11361a.stderr
- testsuite/tests/indexed-types/should_fail/T13971.stderr
- + testsuite/tests/indexed-types/should_fail/T13971b.hs
- + testsuite/tests/indexed-types/should_fail/T13971b.stderr
- testsuite/tests/indexed-types/should_fail/all.T
Changes:
=====================================
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
=====================================
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’
=====================================
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’
=====================================
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
=====================================
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’
=====================================
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, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/commit/78a5c4ce6bae233b655097ada3901028104f0f27
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/commit/78a5c4ce6bae233b655097ada3901028104f0f27
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20190507/961ea230/attachment-0001.html>
More information about the ghc-commits
mailing list