Apparently if one mutters "quantified constraints" under their breath, I have no choice but to materialize there and then ðŸ§ž

I discussed this with @Mikolaj , and while I think we have strayed very far from the original bug report about the confusing error message, perhaps it would be good to weigh in on @simonpj 's "Eek" consternation above, because I'd very much like for the workaround to keep working

```
class C a where
type family F x :: Type -> Type
```

`ghc`

will not let us write

```
fun :: (forall a. C a => C (F x a)) => Proxy x -> ()
fun = undefined
```

but *will* let us write this (a.k.a. "the workaround"):

```
class C (F x a) => CF x a
instance C (F x a) => CF x a
fun' :: (forall a. C a => CF x a) => Proxy x -> ()
fun' = undefined
```

This works in all recent ghc (including HEAD, I just checked), and I would very much like for it to continue to work :) @simonpj 's "eek" moment above is that during type inference,

`forall a. C a => CF x a`

turns into

`forall a. C a => C (F x a)`

if we replace the class alias with its superclass constraints, and this does not work. Indeed, I agree that it is weird that the class alias trick works, but it *does* work and it is very useful.

As for the relevance of arity: my (possibly completely wrong) understanding of the constraint resolution of `forall a. C a => CF x a`

is that we need to solve `C z => CF x z`

for some new skolem variable `z`

; this means we can introduce a given constraint `C z`

and need to solve a wanted constraint `CF x z`

, and therefore `C (F x z)`

; if `F`

would have arity 2, then it would not be able to reduce with that skolem variable as argument and `ghc`

would rightly get stuck proving the constraint. However, if `F`

has arity one, it *can* reduce, and all is well. This is reasonable to me; a constraint such as `forall a. C (F x a)`

*should* be unprovable if `F`

cannot reduce without a concrete value for `a`

.

FWIW, the workaround discussed in #14860 does seem to work here, too:

```
class Ob (Cod f) (f a) => ObCod f a
instance Ob (Cod f) (f a) => ObCod f a
class (forall a. Ob (Dom f) a => ObCod f a) => Functor' f where
type Dom f
type Cod f
liftOb :: forall f a. (Functor' f, Ob (Dom f) a) => Dict (Ob (Cod f) (f a))
liftOb = Dict
```

As I am preparing a discussion of quantified constraints for the Haskell Unfolder, I was studying this ticket again, and wrote a summary of it; perhaps others might benefit from this summary also:

```
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-}
module SummaryOf14860 where
import Data.Kind
import Data.Proxy
--
-- Problem statement:
-- We cannot refer to type families in quantified constraints.
--
class C a where
type family F x :: Type -> Type
-- This is not accepted:
-- fun :: (forall a. C a => C (F x a)) => Proxy x -> ()
-- fun = undefined
--
-- Partial first workaround:
-- Introduce type variable for the type family application.
--
fun' :: (F x ~ f, forall a. C a => C (f a)) => Proxy x -> ()
fun' = undefined
--
-- Problem statement (cont.):
-- The first workaround does not work for superclass constraints
--
-- This is not accepted, just as above:
-- class (forall a. C a => C (F x a)) => D x where
-- But the workaround also does not work ("not in scope: f")
-- class (F x ~ f, forall a. C a => C (f a)) => D x where
--
-- Better workaround: define a class alias
--
class C (F x a) => CF x a
instance C (F x a) => CF x a
-- This works for functions
fun'' :: (forall a. C a => CF x a) => Proxy x -> ()
fun'' = undefined
-- As well as class superclass constraints
class (forall a. C a => CF x a) => D'' x where
--
-- Discussion: Type family of arity 2
--
-- Suppose we have a type family of arity 2:
type family F2 x y :: Type
-- And we're trying to define
--
-- > fun2 :: (forall a. C a => C (F2 x a)) => Proxy x -> ()
-- > fun2 = undefined
--
-- then it's very clear the first work-around does not apply:
--
-- > fun2' :: (F2 x ~ f, forall a. C a => C (f a)) => Proxy x -> ()
-- > fun2' = undefined
--
-- will result inn "F2 should have 2 arguments, but has been given 1".
-- It's less obvious what happens with the second workaround.
-- After all, we /can/ define
class C (F2 x a) => CF2 x a
instance C (F2 x a) => CF2 x a
fun2'' :: (forall a. C a => CF2 x a) => Proxy x -> ()
fun2'' = undefined
-- However, this constraint is basically unsatisfiable.
-- I think this is reasonable, actually. It's not clear what
--
-- > forall a. C a => C (F2 x a)
--
-- even /means/ if F2 has arity two: how would we prove @F2 x a@ for a
-- universally quantified @a@? The type family would be stuck.
```

Full failure report:

```
[1 of 1] Compiling T ( T.hs, T.o )
*** Core Lint errors : in result of Desugar (before optimization) ***
T.hs:15:5: warning:
The type variable @a_aNk[sk:2] is out of scope
In the RHS of f :: forall (arr :: * -> * -> *) t.
ArrowChoice arr =>
(Int -> Int -> Bool) -> arr Int t -> arr (Int, Int) t
In the body of lambda with binder arr_aKT :: * -> * -> *
In the body of lambda with binder t_aKU :: *
In the body of lambda with binder $dArrowChoice_aKV :: ArrowChoice
arr_aKT
In the body of letrec with binders $dNum_aNr :: Num Int
In the body of letrec with binders $dNum_aNt :: Num Int
In the body of letrec with binders $dNum_aNx :: Num Int
In the body of letrec with binders $dNum_aNz :: Num Int
In the body of letrec with binders $dArrowChoice_aNg :: ArrowChoice
arr_aKT
In the body of letrec with binders $dArrow_aNC :: Arrow arr_aKT
In the body of letrec with binders $dCategory_aND :: Category
arr_aKT
In the body of letrec with binders $dArrow_aKZ :: Arrow arr_aKT
In the body of letrec with binders $dArrow_aLC :: Arrow arr_aKT
In the body of lambda with binder p_azE :: Int -> Int -> Bool
In the body of lambda with binder f_azF :: arr_aKT Int t_aKU
In the body of letrec with binders ds_dO1 :: forall b c.
(b -> c) -> arr_aKT b c
In the body of letrec with binders ds_dO2 :: forall {a} {b} {c}.
arr_aKT a b -> arr_aKT b c -> arr_aKT a c
In the body of letrec with binders ds_dO3 :: forall b c d.
arr_aKT b c -> arr_aKT (b, d) (c, d)
In the body of letrec with binders ds_dO4 :: forall b d c.
arr_aKT b d
-> arr_aKT c d -> arr_aKT (Either b c) d
In the body of lambda with binder ds_dOd :: ((Int, Int), ())
In the result-type of a case with scrutinee: ds_dOd
In the type â€˜a_aNk[sk:2]â€™
Substitution: <InScope = {arr_aKT t_aKU}
IdSubst = []
TvSubst = [aKT :-> arr_aKT, aKU :-> t_aKU]
CvSubst = []>
*** Offending Program ***
Rec {
$trModule :: Module
[LclIdX]
$trModule = Module (TrNameS "main"#) (TrNameS "T"#)
ifThenElse :: forall a. Bool -> a -> a -> a
[LclIdX]
ifThenElse
= \ (@a_aKP) (b_azB :: Bool) (x_azC :: a_aKP) (y_azD :: a_aKP) ->
ifThenElse @a_aKP b_azB x_azC y_azD
f :: forall (arr :: * -> * -> *) t.
ArrowChoice arr =>
(Int -> Int -> Bool) -> arr Int t -> arr (Int, Int) t
[LclIdX]
f = \ (@(arr_aKT :: * -> * -> *))
(@t_aKU)
($dArrowChoice_aKV :: ArrowChoice arr_aKT) ->
let {
$dNum_aNr :: Num Int
[LclId]
$dNum_aNr = $fNumInt } in
let {
$dNum_aNt :: Num Int
[LclId]
$dNum_aNt = $dNum_aNr } in
let {
$dNum_aNx :: Num Int
[LclId]
$dNum_aNx = $dNum_aNr } in
let {
$dNum_aNz :: Num Int
[LclId]
$dNum_aNz = $dNum_aNr } in
let {
$dArrowChoice_aNg :: ArrowChoice arr_aKT
[LclId]
$dArrowChoice_aNg = $dArrowChoice_aKV } in
let {
$dArrow_aNC :: Arrow arr_aKT
[LclId]
$dArrow_aNC = $p1ArrowChoice @arr_aKT $dArrowChoice_aKV } in
let {
$dCategory_aND :: Category arr_aKT
[LclId]
$dCategory_aND = $p1Arrow @arr_aKT $dArrow_aNC } in
let {
$dArrow_aKZ :: Arrow arr_aKT
[LclId]
$dArrow_aKZ = $dArrow_aNC } in
let {
$dArrow_aLC :: Arrow arr_aKT
[LclId]
$dArrow_aLC = $dArrow_aNC } in
\ (p_azE :: Int -> Int -> Bool) (f_azF :: arr_aKT Int t_aKU) ->
let {
ds_dO1 :: forall b c. (b -> c) -> arr_aKT b c
[LclId]
ds_dO1 = arr @arr_aKT $dArrow_aKZ } in
let {
ds_dO2
:: forall {a} {b} {c}. arr_aKT a b -> arr_aKT b c -> arr_aKT a c
[LclId]
ds_dO2
= \ (@a_aLj) (@b_aLk) (@c_aLl) ->
let {
$dCategory_aLx :: Category arr_aKT
[LclId]
$dCategory_aLx = $dCategory_aND } in
>>> @(*) @arr_aKT @a_aLj @b_aLk @c_aLl $dCategory_aLx } in
let {
ds_dO3 :: forall b c d. arr_aKT b c -> arr_aKT (b, d) (c, d)
[LclId]
ds_dO3 = first @arr_aKT $dArrow_aLC } in
let {
ds_dO4
:: forall b d c.
arr_aKT b d -> arr_aKT c d -> arr_aKT (Either b c) d
[LclId]
ds_dO4 = ||| @arr_aKT $dArrowChoice_aNg } in
ds_dO2
@(Int, Int)
@((Int, Int), ())
@t_aKU
(ds_dO1
@(Int, Int)
@((Int, Int), ())
(\ (ds_dOe :: (Int, Int)) ->
case ds_dOe of wild_00 { (x_azG, y_azH) -> ((x_azG, y_azH), ()) }))
(ds_dO2
@((Int, Int), ())
@(Either (Int, ()) (Int, ()))
@t_aKU
(ds_dO1
@((Int, Int), ())
@(Either (Int, ()) (Int, ()))
(\ (ds_dOd :: ((Int, Int), ())) ->
case ds_dOd of ds_dOd { (ds_dOc, ds_dOb) ->
case ds_dOc of ds_dOc { (x_azG, y_azH) ->
ifThenElse
@a_aNk[sk:2]
(p_azE x_azG y_azH)
(Left @(Int, ()) @(Int, ()) (x_azG, ds_dOb))
(Right @(Int, ()) @(Int, ()) (y_azH, ds_dOb))
}
}))
(ds_dO4
@(Int, ())
@t_aKU
@(Int, ())
(ds_dO2
@(Int, ())
@Int
@t_aKU
(ds_dO1
@(Int, ())
@Int
(\ (ds_dO7 :: (Int, ())) ->
case ds_dO7 of ds_dO7 { (ds_dO6, ds_dO5) ->
let {
x_azG :: Int
[LclId]
x_azG = ds_dO6 } in
+ @Int $dNum_aNr x_azG (I# 1#)
}))
f_azF)
(ds_dO2
@(Int, ())
@Int
@t_aKU
(ds_dO1
@(Int, ())
@Int
(\ (ds_dOa :: (Int, ())) ->
case ds_dOa of ds_dOa { (ds_dO9, ds_dO8) ->
let {
y_azH :: Int
[LclId]
y_azH = ds_dO9 } in
+ @Int $dNum_aNx y_azH (I# 2#)
}))
f_azF)))
end Rec }
*** End of Offense ***
<no location info>: error:
Compilation had errors
<no location info>: error: ExitFailure 1
```

The below module causes a panic about "no skolem info" in ghc 8.6, 8.8 and 8.10, and a core lint error in ghc 9.0, 9.2, 9.4, and 9.7.20230301

```
{-# LANGUAGE Arrows #-}
{-# LANGUAGE RebindableSyntax #-}
{-# OPTIONS_GHC -dcore-lint #-}
module T where
import Prelude
import Control.Arrow
ifThenElse :: Bool -> a -> a -> a
ifThenElse b x y = if b then x else y
f :: ArrowChoice arr => (Int -> Int -> Bool) -> arr Int t -> arr (Int, Int) t
f p f = proc (x,y) ->
if p x y
then f -< x+1
else f -< y+2
```

Oh no

Plugin order is important, because the output of one plugin can feed into another plugin. The GHC manual says that "Plugins are loaded in order". However, this order seems to have been reversed in ghc 9.4: prior to 9.4, plugins were loaded in *reverse* order to how they appear in `OPTIONS_GHC`

, whereas in 9.4 they are in *order*. This means that CPP may now be required (in code that supports multiple ghc versions) to correctly load multiple plugins.

Consider this simple plugin code that adds some `suffix`

to every string literal in a module:

```
{-# LANGUAGE CPP #-}
{-# LANGUAGE GADTs #-}
module Plugin (Plugin, pluginWithSuffix) where
import Data.Data
import GHC.Plugins
import GHC.Hs
pluginWithSuffix :: String -> Plugin
pluginWithSuffix suffix = defaultPlugin {
parsedResultAction = \_ _ -> return .
ignoreMessages (modifyStrings suffix)
}
where
#if __GLASGOW_HASKELL__ >= 904
ignoreMessages f (ParsedResult modl msgs) = ParsedResult (f modl) msgs
#else
ignoreMessages = id
#endif
modifyStrings :: String -> HsParsedModule -> HsParsedModule
modifyStrings suffix m@HsParsedModule{hpm_module} =
m{hpm_module = go hpm_module}
where
go :: forall a. Data a => a -> a
go x =
case (isHsExpr x, x) of
(Just Refl, HsLit e1 (HsString e2 str)) ->
HsLit e1 (HsString e2 (mappend str (fsLit suffix)))
_otherwise ->
gmapT go x
isHsExpr :: forall a. Data a => a -> Maybe (a :~: HsExpr GhcPs)
isHsExpr _ = eqT
```

We can then define 3 plugins with different suffices; `A`

:

```
module PluginA (plugin) where
import Plugin
plugin :: Plugin
plugin = pluginWithSuffix"A"
```

`B`

:

```
module PluginB (plugin) where
import Plugin
plugin :: Plugin
plugin = pluginWithSuffix "B"
```

and `C`

:

```
module PluginC (plugin) where
import Plugin
plugin :: Plugin
plugin = pluginWithSuffix "C"
```

Then here is a simple test:

```
{-# OPTIONS_GHC -fplugin=PluginA #-}
{-# OPTIONS_GHC -fplugin=PluginB #-}
{-# OPTIONS_GHC -fplugin=PluginC #-}
module Main (main) where
main :: IO ()
main = putStrLn "Hi"
```

It doesn't matter if these are separate `OPTIONS_GHC`

pragmas or a single one.

Running the above code with ghc 9.2 gives

`HiCBA`

whereas in ghc 9.4 it gives

`HiABC`

- GHC version used: ghc 9.2.7, ghc 9.4.4

Plugin order is important, because the output of one plugin can feed into another plugin. The GHC manual says that "Plugins are loaded in order". However, this order seems to have been reversed in ghc 9.4: prior to 9.4, plugins were loaded in *reverse* order to how they appear in `OPTIONS_GHC`

, whereas in 9.4 they are in *order*. This means that CPP may now be required (in code that supports multiple ghc versions) to correctly load multiple plugins.

Consider this simple plugin code that adds some `suffix`

to every string literal in a module:

```
{-# LANGUAGE CPP #-}
{-# LANGUAGE GADTs #-}
module Plugin (Plugin, pluginWithSuffix) where
import Data.Data
import GHC.Plugins
import GHC.Hs
pluginWithSuffix :: String -> Plugin
pluginWithSuffix suffix = defaultPlugin {
parsedResultAction = \_ _ -> return .
ignoreMessages (modifyStrings suffix)
}
where
#if __GLASGOW_HASKELL__ >= 904
ignoreMessages f (ParsedResult modl msgs) = ParsedResult (f modl) msgs
#else
ignoreMessages = id
#endif
modifyStrings :: String -> HsParsedModule -> HsParsedModule
modifyStrings suffix m@HsParsedModule{hpm_module} =
m{hpm_module = go hpm_module}
where
go :: forall a. Data a => a -> a
go x =
case (isHsExpr x, x) of
(Just Refl, HsLit e1 (HsString e2 str)) ->
HsLit e1 (HsString e2 (mappend str (fsLit suffix)))
_otherwise ->
gmapT go x
isHsExpr :: forall a. Data a => a -> Maybe (a :~: HsExpr GhcPs)
isHsExpr _ = eqT
```

We can then define 3 plugins with different suffices; `A`

:

```
module PluginA (plugin) where
import Plugin
plugin :: Plugin
plugin = pluginWithSuffix"A"
```

`B`

:

```
module PluginB (plugin) where
import Plugin
plugin :: Plugin
plugin = pluginWithSuffix "B"
```

and `C`

:

```
module PluginC (plugin) where
import Plugin
plugin :: Plugin
plugin = pluginWithSuffix "C"
```

Then here is a simple test:

```
{-# OPTIONS_GHC -fplugin=PluginA #-}
{-# OPTIONS_GHC -fplugin=PluginB #-}
{-# OPTIONS_GHC -fplugin=PluginC #-}
module Main (main) where
main :: IO ()
main = putStrLn "Hi"
```

It doesn't matter if these are separate `OPTIONS_GHC`

pragmas or a single one.

Running the above code with ghc 9.2 gives

`HiCBA`

whereas in ghc 9.4 it gives

`HiABC`

- GHC version used: ghc 9.2.7, ghc 9.4.4

"but the way to show multiplicities is to turn on `-XLinearTypes`

" . Is that even the case..?

```
ghci> :set -XLinearTypes
ghci> :t \x -> x
\x -> x :: p -> p
```

Perhaps a step towards an alternative approach, done entirely in user-land: https://well-typed.com/blog/2021/12/type-level-sharing-now/.

I'm working on a blog post that shows how to avoid these large coercions purely in user-land. It's still in draft, but you might find it interesting: https://www-staging.well-typed.com/staging-large-rec-ics31o/blog/2021/09/large-records-part-2/ .