[Git][ghc/ghc][wip/T23764] Fix quantification order for a `op` b and a %m -> b
Vladislav Zavialov (@int-index)
gitlab at gitlab.haskell.org
Fri Apr 19 16:57:48 UTC 2024
Vladislav Zavialov pushed to branch wip/T23764 at Glasgow Haskell Compiler / GHC
Commits:
61f4bebd by Krzysztof Gogolewski at 2024-04-19T18:57:37+02:00
Fix quantification order for a `op` b and a %m -> b
Fixes #23764
Implements https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0640-tyop-quantification-order.rst
Updates haddock submodule.
- - - - -
8 changed files:
- compiler/GHC/Rename/HsType.hs
- docs/users_guide/9.12.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
=====================================
@@ -1731,6 +1731,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
@@ -2056,12 +2059,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.12.1-notes.rst
=====================================
@@ -12,6 +12,17 @@ Language
~~~~~~~~
+- 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.
+
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
=====================================
@@ -914,3 +914,4 @@ test('T17594f', normal, compile, [''])
test('WarnDefaultedExceptionContext', normal, compile, ['-Wdefaulted-exception-context'])
test('T24470b', normal, compile, [''])
test('T24566', [], makefile_test, [])
+test('T23764', normal, compile, [''])
=====================================
utils/haddock
=====================================
@@ -1 +1 @@
-Subproject commit 504d4c1842db93704b4c5e158ecc3af7050ba9fe
+Subproject commit 358307f6fa52daa2c2411a4975c87b30932af3dc
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/61f4bebd4780be190b8a8df4019b3a4bee8d18ce
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/61f4bebd4780be190b8a8df4019b3a4bee8d18ce
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/20240419/40c99026/attachment-0001.html>
More information about the ghc-commits
mailing list