[Git][ghc/ghc][wip/scoped-kind-variables] 3 commits: Check for duplicate variables in associated default equations
Vladislav Zavialov
gitlab at gitlab.haskell.org
Wed May 8 01:38:46 UTC 2019
Vladislav Zavialov pushed to branch wip/scoped-kind-variables 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).
- - - - -
f58ea556 by Kevin Buhr at 2019-05-07T21:09:13Z
Add regression test for old typechecking issue #505
- - - - -
a0fd8edd by Vladislav Zavialov at 2019-05-08T01:38:35Z
Scoped kind variables (#16635)
- - - - -
15 changed files:
- compiler/rename/RnTypes.hs
- compiler/typecheck/TcHsType.hs
- 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
- + testsuite/tests/rename/should_fail/T16635a.hs
- + testsuite/tests/rename/should_fail/T16635a.stderr
- + testsuite/tests/rename/should_fail/T16635b.hs
- + testsuite/tests/rename/should_fail/T16635b.stderr
- testsuite/tests/rename/should_fail/all.T
- + testsuite/tests/typecheck/should_compile/T505.hs
- testsuite/tests/typecheck/should_compile/all.T
Changes:
=====================================
compiler/rename/RnTypes.hs
=====================================
@@ -563,8 +563,9 @@ rnHsTyKi env t@(HsKindSig _ ty k)
= do { checkPolyKinds env t
; kind_sigs_ok <- xoptM LangExt.KindSignatures
; unless kind_sigs_ok (badKindSigErr (rtke_ctxt env) ty)
- ; (ty', fvs1) <- rnLHsTyKi env ty
; (k', fvs2) <- rnLHsTyKi (env { rtke_level = KindLevel }) k
+ ; (ty', fvs1) <- bindSigTyVarsFV (hsScopedKvs k') $
+ rnLHsTyKi env ty
; return (HsKindSig noExt ty' k', fvs1 `plusFV` fvs2) }
-- Unboxed tuples are allowed to have poly-typed arguments. These
@@ -646,6 +647,10 @@ rnHsTyKi env (HsWildCardTy _)
= do { checkAnonWildCard env
; return (HsWildCardTy noExt, emptyFVs) }
+hsScopedKvs :: LHsType GhcRn -> [Name]
+hsScopedKvs (L _ (HsForAllTy { hst_bndrs = tvs })) = hsLTyVarNames tvs
+hsScopedKvs _ = []
+
--------------
rnTyVar :: RnTyKiEnv -> RdrName -> RnM Name
rnTyVar env rdr_name
=====================================
compiler/typecheck/TcHsType.hs
=====================================
@@ -587,7 +587,8 @@ tc_infer_hs_type mode (HsKindSig _ ty sig)
-- things like instantiate its foralls, so it needs
-- to be fully determined (#14904)
; traceTc "tc_infer_hs_type:sig" (ppr ty $$ ppr sig')
- ; ty' <- tc_lhs_type mode ty sig'
+ ; ty' <- tcExtendTyVarEnv (fst (tcSplitForAllTys sig')) $
+ tc_lhs_type mode ty sig'
; return (ty', sig') }
-- HsSpliced is an annotation produced by 'RnSplice.rnSpliceType' to communicate
=====================================
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, [''])
=====================================
testsuite/tests/rename/should_fail/T16635a.hs
=====================================
@@ -0,0 +1,11 @@
+{-# LANGUAGE NoScopedTypeVariables, ExplicitForAll #-}
+{-# LANGUAGE DataKinds, PolyKinds, TypeApplications #-}
+
+module T16635a where
+
+data Unit = U
+data P a = MkP
+
+-- ScopedTypeVariables are disabled.
+-- Fails because because @a is not in scope.
+type F = (Just @a :: forall a. a -> Maybe a) U
=====================================
testsuite/tests/rename/should_fail/T16635a.stderr
=====================================
@@ -0,0 +1,2 @@
+
+T16635a.hs:11:17: error: Not in scope: type variable ‘a’
=====================================
testsuite/tests/rename/should_fail/T16635b.hs
=====================================
@@ -0,0 +1,14 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE DataKinds, PolyKinds, TypeApplications #-}
+
+module T16635b where
+
+data Unit = U
+data P a = MkP
+
+-- OK.
+f = (Just @a :: forall a. a -> Maybe a) U
+
+-- Fails because we cannot generalize to (/\a. Just @a)
+-- but NOT because @a is not in scope.
+type F = (Just @a :: forall a. a -> Maybe a) U
=====================================
testsuite/tests/rename/should_fail/T16635b.stderr
=====================================
@@ -0,0 +1,6 @@
+
+T16635b.hs:14:11: error:
+ • Expected kind ‘forall a. a -> Maybe a’,
+ but ‘Just @a’ has kind ‘a -> Maybe a’
+ • In the type ‘(Just @a :: forall a. a -> Maybe a) U’
+ In the type declaration for ‘F’
=====================================
testsuite/tests/rename/should_fail/all.T
=====================================
@@ -149,3 +149,5 @@ test('ExplicitForAllRules2', normal, compile_fail, [''])
test('T15957_Fail', normal, compile_fail, ['-Werror -Wall -Wno-missing-signatures'])
test('T16385', normal, compile_fail, [''])
test('T16504', normal, compile_fail, [''])
+test('T16635a', normal, compile_fail, [''])
+test('T16635b', normal, compile_fail, [''])
=====================================
testsuite/tests/typecheck/should_compile/T505.hs
=====================================
@@ -0,0 +1,14 @@
+{-# OPTIONS_GHC -Wno-inline-rule-shadowing #-}
+module Bug where
+
+foo 1 = 2
+bar 0 = 1
+
+-- regression test for #505:
+-- the following rule should not case a panic
+
+{-# RULES
+ "foo/bar" foo bar = foobar
+ #-}
+
+foobar = 2
=====================================
testsuite/tests/typecheck/should_compile/all.T
=====================================
@@ -671,4 +671,5 @@ test('T16204b', normal, compile, [''])
test('T16225', normal, compile, [''])
test('T13951', normal, compile, [''])
test('T16411', normal, compile, [''])
-test('T16609', normal, compile, [''])
\ No newline at end of file
+test('T16609', normal, compile, [''])
+test('T505', normal, compile, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/compare/20ade93b367963c14deb4d02021241b0857f80dd...a0fd8edde589c8df10b0e4ef7e6d2a56bb1f408d
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/compare/20ade93b367963c14deb4d02021241b0857f80dd...a0fd8edde589c8df10b0e4ef7e6d2a56bb1f408d
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/b35dd2b6/attachment-0001.html>
More information about the ghc-commits
mailing list