[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:18:17 UTC 2023



Krzysztof Gogolewski pushed to branch wip/T23764 at Glasgow Haskell Compiler / GHC


Commits:
8da4156f by Krzysztof Gogolewski at 2023-08-03T22:18:08+02:00
Fix quantification order for a `op` b and a %m -> b

Fixes #23764

- - - - -


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/8da4156f0ad7cdf13b54e93454ad66653a5c5e08

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/8da4156f0ad7cdf13b54e93454ad66653a5c5e08
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/9dc93cec/attachment-0001.html>


More information about the ghc-commits mailing list