diff --git a/compiler/GHC/Rename/HsType.hs b/compiler/GHC/Rename/HsType.hs
index fd169a7e0b42dc7154d8999dca23dd569777b553..c0a952066b9eec37eb1266b40daa88db69ec8e9c 100644
--- a/compiler/GHC/Rename/HsType.hs
+++ b/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
diff --git a/docs/users_guide/9.12.1-notes.rst b/docs/users_guide/9.12.1-notes.rst
index dfe94e5cae8b80d7c370be8724d56046d1c67876..7340b4a6c36f19ac2898fb93c9d77608b58d97e6 100644
--- a/docs/users_guide/9.12.1-notes.rst
+++ b/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
~~~~~~~~
diff --git a/testsuite/tests/linear/should_compile/MultConstructor.hs b/testsuite/tests/linear/should_compile/MultConstructor.hs
index 66ac13697daa9f2367e3a606f6c0abddd8c68c6e..7e70d0fff844d1b2ee5b60b783c85ab33713cebe 100644
--- a/testsuite/tests/linear/should_compile/MultConstructor.hs
+++ b/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
diff --git a/testsuite/tests/linear/should_fail/LinearErrOrigin.stderr b/testsuite/tests/linear/should_fail/LinearErrOrigin.stderr
index dd7e04d9362df63af62d770508811a02c4aab845..c3175e1256c98663bb45127b74f0d9ea4aae18ad 100644
--- a/testsuite/tests/linear/should_fail/LinearErrOrigin.stderr
+++ b/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
diff --git a/testsuite/tests/linear/should_fail/LinearVar.stderr b/testsuite/tests/linear/should_fail/LinearVar.stderr
index bb01d563f3a441a86cb6a7e26b41a9d195ff7505..d66f3b46d883d9bc4b4810966fc93677b2b17b30 100644
--- a/testsuite/tests/linear/should_fail/LinearVar.stderr
+++ b/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
diff --git a/testsuite/tests/typecheck/should_compile/T23764.hs b/testsuite/tests/typecheck/should_compile/T23764.hs
new file mode 100644
index 0000000000000000000000000000000000000000..70269386257d28c17fc92009b46a1f892fdd6c02
--- /dev/null
+++ 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
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 5d2de89fe796870fa64d1d3816d94bc83d67be5e..2b6d2108041d5d7134da17861122d374b2417bc3 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/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, [''])
diff --git a/utils/haddock b/utils/haddock
index 504d4c1842db93704b4c5e158ecc3af7050ba9fe..358307f6fa52daa2c2411a4975c87b30932af3dc 160000
--- a/utils/haddock
+++ b/utils/haddock
@@ -1 +1 @@
-Subproject commit 504d4c1842db93704b4c5e158ecc3af7050ba9fe
+Subproject commit 358307f6fa52daa2c2411a4975c87b30932af3dc