[Git][ghc/ghc][wip/T23764] Fix quantification order for a `op` b and a %m -> b
Krzysztof Gogolewski (@monoidal)
gitlab at gitlab.haskell.org
Thu Aug 3 20:24:07 UTC 2023
Krzysztof Gogolewski pushed to branch wip/T23764 at Glasgow Haskell Compiler / GHC
Commits:
7a485e44 by Krzysztof Gogolewski at 2023-08-03T22:23:52+02:00
Fix quantification order for a `op` b and a %m -> b
Fixes #23764
Updates haddock submodule.
- - - - -
8 changed files:
- compiler/GHC/Rename/HsType.hs
- docs/users_guide/9.10.1-notes.rst
- testsuite/tests/linear/should_compile/MultConstructor.hs
- testsuite/tests/linear/should_fail/LinearErrOrigin.stderr
- testsuite/tests/linear/should_fail/LinearVar.stderr
- + testsuite/tests/typecheck/should_compile/T23764.hs
- testsuite/tests/typecheck/should_compile/all.T
- utils/haddock
Changes:
=====================================
compiler/GHC/Rename/HsType.hs
=====================================
@@ -1714,6 +1714,9 @@ FreeKiTyVars, which notably includes the `extract-` family of functions
(extractHsTysRdrTyVars, extractHsTyVarBndrsKVs, etc.).
These functions thus promise to keep left-to-right ordering.
+Note that for 'HsFunTy m ty1 ty2', we quantify in the order ty1, m, ty2,
+since this type is written ty1 %m -> ty2 in the source syntax.
+
Note [Implicit quantification in type synonyms]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We typically bind type/kind variables implicitly when they are in a kind
@@ -1928,12 +1931,12 @@ extract_lty (L _ ty) acc
HsListTy _ ty -> extract_lty ty acc
HsTupleTy _ _ tys -> extract_ltys tys acc
HsSumTy _ tys -> extract_ltys tys acc
- HsFunTy _ w ty1 ty2 -> extract_lty ty1 $
- extract_lty ty2 $
- extract_hs_arrow w acc
+ HsFunTy _ m ty1 ty2 -> extract_lty ty1 $
+ extract_hs_arrow m $ -- See Note [Ordering of implicit variables]
+ extract_lty ty2 acc
HsIParamTy _ _ ty -> extract_lty ty acc
- HsOpTy _ _ ty1 tv ty2 -> extract_tv tv $
- extract_lty ty1 $
+ HsOpTy _ _ ty1 tv ty2 -> extract_lty ty1 $
+ extract_tv tv $
extract_lty ty2 acc
HsParTy _ ty -> extract_lty ty acc
HsSpliceTy {} -> acc -- Type splices mention no tvs
=====================================
docs/users_guide/9.10.1-notes.rst
=====================================
@@ -18,6 +18,20 @@ Language
This feature is guarded behind :extension:`RequiredTypeArguments` and :extension:`ExplicitNamespaces`.
+- The ordering of variables used for visible type application has been changed in two cases.
+ It is supposed to be left-to-right, but due to an oversight, it was wrong:
+
+ - in an infix application ``f :: a `op` b``, it is now ``forall a op b.`` rather than
+ ``forall op a b.``
+ - in a linear type ``f :: a %m -> b``, it is now ``forall a m b.`` rather than
+ ``forall a b m.``.
+
+ This change is backwards-incompatible, although in practice we don't expect it
+ to cause significant disruption.
+
+- Normally, variables used for visible type application are collected left-to-right in a type signature.
+ However, this feature had a bug in two places: for infix oepr
+
Compiler
~~~~~~~~
=====================================
testsuite/tests/linear/should_compile/MultConstructor.hs
=====================================
@@ -26,3 +26,9 @@ g2 (MkE x) = x
vta :: Int %1 -> Existential Int
vta x = MkE @Int @'One x
+
+h :: a %m -> b
+h = h
+
+vta2 :: Int %1 -> Bool -- see #23764
+vta2 = h @Int @One @Bool
=====================================
testsuite/tests/linear/should_fail/LinearErrOrigin.stderr
=====================================
@@ -3,13 +3,13 @@ LinearErrOrigin.hs:7:7: error: [GHC-25897]
• Couldn't match type ‘p’ with ‘q’ arising from multiplicity of ‘x’
‘p’ is a rigid type variable bound by
the type signature for:
- foo :: forall a b (p :: GHC.Types.Multiplicity)
+ foo :: forall a (p :: GHC.Types.Multiplicity) b
(q :: GHC.Types.Multiplicity).
(a %p -> b) -> a %q -> b
at LinearErrOrigin.hs:6:1-31
‘q’ is a rigid type variable bound by
the type signature for:
- foo :: forall a b (p :: GHC.Types.Multiplicity)
+ foo :: forall a (p :: GHC.Types.Multiplicity) b
(q :: GHC.Types.Multiplicity).
(a %p -> b) -> a %q -> b
at LinearErrOrigin.hs:6:1-31
=====================================
testsuite/tests/linear/should_fail/LinearVar.stderr
=====================================
@@ -5,7 +5,7 @@ LinearVar.hs:5:5: error: [GHC-25897]
Actual: a -> b
‘m’ is a rigid type variable bound by
the type signature for:
- f :: forall a b (m :: GHC.Types.Multiplicity). a %m -> b
+ f :: forall a (m :: GHC.Types.Multiplicity) b. a %m -> b
at LinearVar.hs:4:1-14
• In the expression: undefined :: a -> b
In an equation for ‘f’: f = undefined :: a -> b
=====================================
testsuite/tests/typecheck/should_compile/T23764.hs
=====================================
@@ -0,0 +1,7 @@
+module T23764 where
+
+f :: a `op` b
+f = f
+
+g :: (Int, Bool)
+g = f @Int @(,) @Bool
=====================================
testsuite/tests/typecheck/should_compile/all.T
=====================================
@@ -891,3 +891,4 @@ test('T18986b', normal, compile, [''])
test('T23413', normal, compile, [''])
test('TcIncompleteRecSel', normal, compile, ['-Wincomplete-record-selectors'])
test('InstanceWarnings', normal, multimod_compile, ['InstanceWarnings', ''])
+test('T23764', normal, compile, [''])
=====================================
utils/haddock
=====================================
@@ -1 +1 @@
-Subproject commit b96241bad1cd59c65a89dab74e6cba114129e521
+Subproject commit 31551d1df39a642101559425170b9d54db71630e
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/7a485e440b3e8351f5c53d207c1e3674e54f4953
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/7a485e440b3e8351f5c53d207c1e3674e54f4953
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/20230803/53bd3753/attachment-0001.html>
More information about the ghc-commits
mailing list