[Git][ghc/ghc][wip/marge_bot_batch_merge_job] 4 commits: Check for duplicate variables in associated default equations
Marge Bot
gitlab at gitlab.haskell.org
Tue May 7 21:45:35 UTC 2019
Marge Bot pushed to branch wip/marge_bot_batch_merge_job 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
- - - - -
dfd25c30 by Ryan Scott at 2019-05-07T21:45:28Z
Fix #16603 by documenting some important changes in changelogs
This addresses some glaring omissions from
`libraries/base/changelog.md` and
`docs/users_guide/8.8.1-notes.rst`, fixing #16603 in the process.
- - - - -
979108ca by Ryan Scott at 2019-05-07T21:45:29Z
Fix #16632 by using the correct SrcSpan in checkTyClHdr
`checkTyClHdr`'s case for `HsTyVar` was grabbing the wrong `SrcSpan`,
which lead to error messages pointing to the wrong location. Easily
fixed.
- - - - -
14 changed files:
- compiler/parser/RdrHsSyn.hs
- compiler/typecheck/TcTyClsDecls.hs
- docs/users_guide/8.8.1-notes.rst
- libraries/base/changelog.md
- testsuite/tests/indexed-types/should_compile/T11361a.stderr
- + testsuite/tests/indexed-types/should_compile/T16632.hs
- + testsuite/tests/indexed-types/should_compile/T16632.stderr
- testsuite/tests/indexed-types/should_compile/all.T
- 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/typecheck/should_compile/T505.hs
- testsuite/tests/typecheck/should_compile/all.T
Changes:
=====================================
compiler/parser/RdrHsSyn.hs
=====================================
@@ -955,8 +955,8 @@ checkTyClHdr is_cls ty
; let name = mkOccName tcClsName (starSym isUni)
; return (cL l (Unqual name), acc, fix, (ann ++ mkParensApiAnn lp)) }
- go l (HsTyVar _ _ (dL->L _ tc)) acc ann fix
- | isRdrTc tc = return (cL l tc, acc, fix, ann)
+ go _ (HsTyVar _ _ ltc@(dL->L _ tc)) acc ann fix
+ | isRdrTc tc = return (ltc, acc, fix, ann)
go _ (HsOpTy _ t1 ltc@(dL->L _ tc) t2) acc ann _fix
| isRdrTc tc = return (ltc, HsValArg t1:HsValArg t2:acc, Infix, ann)
go l (HsParTy _ ty) acc ann fix = goL ty acc (ann ++mkParensApiAnn l) fix
=====================================
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
=====================================
docs/users_guide/8.8.1-notes.rst
=====================================
@@ -23,6 +23,21 @@ Full details
Language
~~~~~~~~
+- GHC now supports visible kind applications, as described in
+ `GHC proposal #15 <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0015-type-level-type-applications.rst>`__. This extends the existing
+ :ref:`visible type applications <visible-type-application>` feature to permit
+ type applications at the type level (e.g., ``f :: Proxy ('Just @Bool 'True)``) in
+ addition to the term level (e.g., ``g = Just @Bool True``).
+
+- GHC now allows explicitly binding type variables in type family instances and
+ rewrite rules, as described in
+ `GHC proposal #7 <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0007-instance-foralls.rst>`__. For instance: ::
+
+ type family G a b where
+ forall x y. G [x] (Proxy y) = Double
+ forall z. G z z = Bool
+ {-# RULES "example" forall a. forall (x :: a). id x = x #-}
+
- :extension:`ScopedTypeVariables`: The type variable that a type signature on
a pattern can bring into scope can now stand for arbitrary types. Previously,
they could only stand in for other type variables, but this restriction was deemed
@@ -76,6 +91,13 @@ Language
Compiler
~~~~~~~~
+- The final phase of the ``MonadFail`` proposal has been implemented.
+ Accordingly, the ``MonadFailDesugaring`` language extension is now
+ deprecated, as its effects are always enabled. Similarly, the
+ ``-Wnoncanonical-monadfail-instances`` flag is also deprecated, as there is
+ no longer any way to define a "non-canonical" ``Monad`` or ``MonadFail``
+ instance.
+
- New :ghc-flag:`-keep-hscpp-files` to keep the output of the CPP pre-processor.
- The :ghc-flag:`-Wcompat` warning group now includes :ghc-flag:`-Wstar-is-type`.
@@ -143,6 +165,13 @@ Template Haskell
longer included when reifying ``C``. It's possible that this may break some
code which assumes the existence of ``forall a. C a =>``.
+- Template Haskell has been updated to support visible kind applications and
+ explicit ``foralls`` in type family instances and ``RULES``. These required
+ a couple of backwards-incompatible changes to the ``template-haskell`` API.
+ Please refer to the
+ `GHC 8.8 Migration Guide <https://gitlab.haskell.org/ghc/ghc/wikis/migration/8.8#template-haskell-21500>`__
+ for more details.
+
- Template Haskell now supports implicit parameters and recursive do.
``ghc-prim`` library
@@ -164,6 +193,20 @@ Template Haskell
``base`` library
~~~~~~~~~~~~~~~~
+- The final phase of the ``MonadFail`` proposal has been implemented. As a
+ result of this change:
+
+ - The ``fail`` method of ``Monad`` has been removed in favor of the method of
+ the same name in the ``MonadFail`` class.
+
+ - ``MonadFail(fail)`` is now re-exported from the ``Prelude`` and
+ ``Control.Monad`` modules.
+
+ These are breaking changes that may require you to update your code. Please
+ refer to the
+ `GHC 8.8 Migration Guide <https://gitlab.haskell.org/ghc/ghc/wikis/migration/8.8#base-41300>`__
+ for more details.
+
- Support the characters from recent versions of Unicode (up to v. 12) in literals
(see :ghc-ticket:`5518`).
=====================================
libraries/base/changelog.md
=====================================
@@ -8,6 +8,14 @@
## 4.13.0.0 *TBA*
* Bundled with GHC *TBA*
+ * The final phase of the `MonadFail` proposal has been implemented:
+
+ * The `fail` method of `Monad` has been removed in favor of the method of
+ the same name in the `MonadFail` class.
+
+ * `MonadFail(fail)` is now re-exported from the `Prelude` and
+ `Control.Monad` modules.
+
* Fix `Show` instance of `Data.Fixed`: Negative numbers are now parenthesized
according to their surrounding context. I.e. `Data.Fixed.show` produces
syntactically correct Haskell for expressions like `Just (-1 :: Fixed E2)`.
=====================================
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_compile/T16632.hs
=====================================
@@ -0,0 +1,5 @@
+{-# LANGUAGE TypeFamilies #-}
+module T16632 where
+
+type family F a b c
+type instance F Char b Int = ()
=====================================
testsuite/tests/indexed-types/should_compile/T16632.stderr
=====================================
@@ -0,0 +1,6 @@
+
+T16632.hs:5:22: warning: [-Wunused-type-patterns]
+ Defined but not used on the right hand side: type variable ‘b’
+ |
+5 | type instance F Char b Int = ()
+ | ^
=====================================
testsuite/tests/indexed-types/should_compile/all.T
=====================================
@@ -286,3 +286,4 @@ test('T15711', normal, compile, ['-ddump-types'])
test('T15852', normal, compile, ['-ddump-types'])
test('T15764a', normal, compile, [''])
test('T15740a', normal, compile, [''])
+test('T16632', normal, compile, ['-Wunused-type-patterns -fdiagnostics-show-caret'])
=====================================
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/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/43489d7930ba05162e6ea87276ea56ec58611c44...979108ca527367767b12decedd3697ae06891f7c
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/compare/43489d7930ba05162e6ea87276ea56ec58611c44...979108ca527367767b12decedd3697ae06891f7c
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/3b341021/attachment-0001.html>
More information about the ghc-commits
mailing list