Major refactor in the handling of equality constraints

This MR substantially refactors the way in which the constraint
solver deals with equality constraints.  The big thing is:

* Intead of a pipeline in which we /first/ canonicalise and /then/
  interact (the latter including performing unification) the two steps
  are more closely integreated into one.  That avoids the current
  rather indirect communication between the two steps.

The proximate cause for this refactoring is fixing #22194, which involve
solving   [W] alpha[2] ~ Maybe (F beta[4])
by doing this:
          alpha[2] := Maybe delta[2]
          [W] delta[2] ~ F beta[4]
That is, we don't promote beta[4]!  This is very like introducing a cycle
breaker, and was very awkward to do before, but now it is all nice.
See GHC.Tc.Utils.Unify Note [Promotion and level-checking] and
Note [Family applications in canonical constraints].

The big change is this:

* Several canonicalisation checks (occurs-check, cycle-breaking,
  checking for concreteness) are combined into one new function:
     GHC.Tc.Utils.Unify.checkTyEqRhs

  This function is controlled by `TyEqFlags`, which says what to do
  for foralls, type families etc.

* `canEqCanLHSFinish` now sees if unification is possible, and if so,
  actually does it: see `canEqCanLHSFinish_try_unification`.

There are loads of smaller changes:

* The on-the-fly unifier `GHC.Tc.Utils.Unify.unifyType` has a
  cheap-and-cheerful version of `checkTyEqRhs`, called
  `simpleUnifyCheck`.  If `simpleUnifyCheck` succeeds, it can unify,
  otherwise it defers by emitting a constraint. This is simpler than
  before.

* I simplified the swapping code in `GHC.Tc.Solver.Equality.canEqCanLHS`.
  Especially the nasty stuff involving `swap_for_occurs` and
  `canEqTyVarFunEq`.  Much nicer now.  See
      Note [Orienting TyVarLHS/TyFamLHS]
      Note [Orienting TyFamLHS/TyFamLHS]

* Added `cteSkolemOccurs`, `cteConcrete`, and `cteCoercionHole` to the
  problems that can be discovered by `checkTyEqRhs`.

* I fixed #23199 `pickQuantifiablePreds`, which actually allows GHC to
  to accept both cases in #22194 rather than rejecting both.

Yet smaller:

* Added a `synIsConcrete` flag to `SynonymTyCon` (alongside `synIsFamFree`)
  to reduce the need for synonym expansion when checking concreteness.
  Use it in `isConcreteType`.

* Renamed `isConcrete` to `isConcreteType`

* Defined `GHC.Core.TyCo.FVs.isInjectiveInType` as a more efficient
  way to find if a particular type variable is used injectively than
  finding all the injective variables.  It is called in
  `GHC.Tc.Utils.Unify.definitely_poly`, which in turn is used quite a
  lot.

* Moved `rewriterView` to `GHC.Core.Type`, so we can use it from the
  constraint solver.

Fixes #22194, #23199

Compile times decrease by an average of 0.1%; but there is a 7.4%
drop in compiler allocation on T15703.

Metric Decrease:
    T15703

20 files changed, 120 insertions, 75 deletions

diff --git a/testsuite/tests/ado/T16135.stderr b/testsuite/tests/ado/T16135.stderr
new file mode 100644
index 0000000000..e6a77cdfe6
--- /dev/null
+++ b/testsuite/tests/ado/T16135.stderr
@@ -0,0 +1,14 @@
+T16135.hs:11:18: error: [GHC-83865]
+    • Couldn't match type ‘a0’ with ‘a’
+      Expected: f a0
+        Actual: f a
+      ‘a’ is a rigid type variable bound by
+        a pattern with constructor:
+          MkT :: forall {k} (f :: k -> *) (a :: k). f a -> T f,
+        in a pattern binding in
+             a 'do' block
+        at T16135.hs:10:5-10
+    • In the first argument of ‘MkT’, namely ‘fa’
+      In the second argument of ‘($)’, namely ‘MkT fa’
+      In a stmt of a 'do' block: return $ MkT fa
+    • Relevant bindings include fa :: f a (bound at T16135.hs:10:9)
diff --git a/testsuite/tests/ado/all.T b/testsuite/tests/ado/all.T
index c46ea88404..0568cd00e9 100644
--- a/testsuite/tests/ado/all.T
+++ b/testsuite/tests/ado/all.T
@@ -20,5 +20,5 @@ test('T15344', normal, compile_and_run, [''])
 test('T16628', normal, compile_fail, [''])
 test('T17835', normal, compile, [''])
 test('T20540', normal, compile, [''])
-test('T16135', [when(compiler_debugged(),expect_broken(16135)), js_broken(22576)], compile, [''])
+test('T16135', [when(compiler_debugged(),expect_broken(16135)), js_broken(22576)], compile_fail, [''])
 test('T22483', normal, compile, ['-Wall'])
diff --git a/testsuite/tests/indexed-types/should_compile/T3208b.stderr b/testsuite/tests/indexed-types/should_compile/T3208b.stderr
index 45a3b9b74c..9cb2670505 100644
--- a/testsuite/tests/indexed-types/should_compile/T3208b.stderr
+++ b/testsuite/tests/indexed-types/should_compile/T3208b.stderr
@@ -1,6 +1,6 @@
 
 T3208b.hs:15:10: error: [GHC-05617]
-    • Could not deduce ‘OTerm o0 ~ STerm a’ arising from a use of ‘fce’
+    • Could not deduce ‘STerm o0 ~ OTerm a’ arising from a use of ‘fce’
       from the context: (OTerm a ~ STerm a, OBJECT a, SUBST a)
         bound by the type signature for:
                    fce' :: forall a c.
@@ -15,7 +15,7 @@ T3208b.hs:15:10: error: [GHC-05617]
         fce' :: a -> c (bound at T3208b.hs:15:1)
 
 T3208b.hs:15:15: error: [GHC-05617]
-    • Could not deduce ‘STerm o0 ~ STerm a’
+    • Could not deduce ‘OTerm o0 ~ OTerm a’
         arising from a use of ‘apply’
       from the context: (OTerm a ~ STerm a, OBJECT a, SUBST a)
         bound by the type signature for:
@@ -23,7 +23,7 @@ T3208b.hs:15:15: error: [GHC-05617]
                            (OTerm a ~ STerm a, OBJECT a, SUBST a) =>
                            a -> c
         at T3208b.hs:14:1-56
-      NB: ‘STerm’ is a non-injective type family
+      NB: ‘OTerm’ is a non-injective type family
       The type variable ‘o0’ is ambiguous
     • In the first argument of ‘fce’, namely ‘(apply f)’
       In the expression: fce (apply f)
diff --git a/testsuite/tests/indexed-types/should_fail/T8227.stderr b/testsuite/tests/indexed-types/should_fail/T8227.stderr
index 64792ae0e9..3d20ee24ca 100644
--- a/testsuite/tests/indexed-types/should_fail/T8227.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T8227.stderr
@@ -1,9 +1,10 @@
 
 T8227.hs:24:27: error: [GHC-83865]
     • Couldn't match type: Scalar (V a)
-                     with: t0 -> t0
+                     with: p0 -> p0
       Expected: Scalar (V a)
-        Actual: Scalar (V (t0 -> t0)) -> Scalar (V (t0 -> t0))
+        Actual: Scalar (V (Scalar (V p0) -> p0))
+                -> Scalar (V (Scalar (V p0) -> p0))
     • In the expression: arcLengthToParam eps eps
       In an equation for ‘absoluteToParam’:
           absoluteToParam eps seg = arcLengthToParam eps eps
@@ -14,9 +15,9 @@ T8227.hs:24:27: error: [GHC-83865]
           (bound at T8227.hs:24:1)
 
 T8227.hs:24:48: error: [GHC-27958]
-    • Couldn't match type ‘t0’ with ‘Scalar (V t0)’
-        arising from a type equality Scalar (V a) ~ t0 -> t0
-      The type variable ‘t0’ is ambiguous
+    • Couldn't match type ‘p0’ with ‘Scalar (V p0)’
+        arising from a type equality Scalar (V a) ~ Scalar (V p0) -> p0
+      The type variable ‘p0’ is ambiguous
     • In the second argument of ‘arcLengthToParam’, namely ‘eps’
       In the expression: arcLengthToParam eps eps
       In an equation for ‘absoluteToParam’:
diff --git a/testsuite/tests/partial-sigs/should_fail/T14040a.stderr b/testsuite/tests/partial-sigs/should_fail/T14040a.stderr
index 5614422045..fc3c1e0c8b 100644
--- a/testsuite/tests/partial-sigs/should_fail/T14040a.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/T14040a.stderr
@@ -1,7 +1,7 @@
 
 T14040a.hs:26:46: error: [GHC-46956]
-    • Couldn't match kind ‘k1’ with ‘WeirdList z’
-      Expected kind ‘WeirdList k1’,
+    • Couldn't match kind ‘k0’ with ‘WeirdList z’
+      Expected kind ‘WeirdList k0’,
         but ‘xs’ has kind ‘WeirdList (WeirdList z)’
         because kind variable ‘z’ would escape its scope
       This (rigid, skolem) kind variable is bound by
@@ -25,8 +25,8 @@ T14040a.hs:26:46: error: [GHC-46956]
                                                                                            -> p _ wl
 
 T14040a.hs:27:27: error: [GHC-46956]
-    • Couldn't match kind ‘k0’ with ‘z’
-      Expected kind ‘WeirdList k0’,
+    • Couldn't match kind ‘k1’ with ‘z’
+      Expected kind ‘WeirdList k1’,
         but ‘WeirdCons x xs’ has kind ‘WeirdList z’
         because kind variable ‘z’ would escape its scope
       This (rigid, skolem) kind variable is bound by
diff --git a/testsuite/tests/polykinds/T14939.hs b/testsuite/tests/polykinds/T14939.hs
index f1387a00ab..39b9784d1f 100644
--- a/testsuite/tests/polykinds/T14939.hs
+++ b/testsuite/tests/polykinds/T14939.hs
@@ -16,4 +16,4 @@ data AlgCat (cls::Type -> Constraint) :: Cat (Alg cls Type) where
   AlgCat :: (cls a, cls b) => (a -> b) -> AlgCat cls a b
 
 leftAdj :: AlgCat cls (Frí cls a) b -> (a -> b)
-leftAdj (AlgCat f) a = undefined
\ No newline at end of file
+leftAdj (AlgCat f) a = undefined
diff --git a/testsuite/tests/polykinds/T18451a.hs b/testsuite/tests/polykinds/T18451a.hs
index 5611a7afcb..b7c5f983ea 100644
--- a/testsuite/tests/polykinds/T18451a.hs
+++ b/testsuite/tests/polykinds/T18451a.hs
@@ -10,3 +10,9 @@ type Const a b = a
 
 foo :: forall a b (c :: Const Type b). Proxy '[a, c]
 foo = error "ruk"
+
+-- We infer a :: k0,  k0 ~ Const Type b
+-- We unify k0 := Const Type b (in the eager unifier)
+-- And that leaves us with
+--    forall (a :: Const Type b) (b :: Type) (c :: Const Type b). ...a
+-- Bad!  But delicate because we could expand the synonym
diff --git a/testsuite/tests/polykinds/T18451b.hs b/testsuite/tests/polykinds/T18451b.hs
deleted file mode 100644
index 5611a7afcb..0000000000
--- a/testsuite/tests/polykinds/T18451b.hs
+++ /dev/null
@@ -1,12 +0,0 @@
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE DataKinds #-}
-module Bug where
-
-import Data.Kind
-import Data.Proxy
-
-type Const a b = a
-
-foo :: forall a b (c :: Const Type b). Proxy '[a, c]
-foo = error "ruk"
diff --git a/testsuite/tests/polykinds/T18451b.stderr b/testsuite/tests/polykinds/T18451b.stderr
deleted file mode 100644
index 9389400d6d..0000000000
--- a/testsuite/tests/polykinds/T18451b.stderr
+++ /dev/null
@@ -1,7 +0,0 @@
-
-T18451b.hs:11:15: error: [GHC-97739]
-    • These kind and type variables: a b (c :: Const Type b)
-      are out of dependency order. Perhaps try this ordering:
-        (b :: k) (a :: Const (*) b) (c :: Const (*) b)
-    • In the type signature:
-        foo :: forall a b (c :: Const Type b). Proxy '[a, c]
diff --git a/testsuite/tests/polykinds/T22793.stderr b/testsuite/tests/polykinds/T22793.stderr
index 8082fa5be0..fc91382642 100644
--- a/testsuite/tests/polykinds/T22793.stderr
+++ b/testsuite/tests/polykinds/T22793.stderr
@@ -1,36 +1,13 @@
 
 T22793.hs:15:42: error: [GHC-25897]
-    • Couldn't match kind ‘ka’ with ‘k1’
-      Expected kind ‘ks’, but ‘a’ has kind ‘ka’
+    • Expected kind ‘ks’, but ‘a’ has kind ‘ka’
       ‘ka’ is a rigid type variable bound by
         the type signature for ‘bob’
         at T22793.hs:13:26-27
-      ‘k1’ is a rigid type variable bound by
-        the type signature for ‘bob’
-        at T22793.hs:13:16-17
-    • In the second argument of ‘Foo’, namely ‘a’
-      In the type signature:
-        bob :: forall {k1}
-                      {ks}
-                      {ka}
-                      q
-                      (p :: k1 -> q -> Type)
-                      (f :: ka -> q)
-                      (s :: ks)
-                      (t :: ks)
-                      (a :: ka)
-                      (b :: ka). Foo s a => p a (f b) -> p s (f t)
-
-T22793.hs:16:11: error: [GHC-25897]
-    • Couldn't match kind ‘ks’ with ‘k1’
-      Expected kind ‘k1’, but ‘a’ has kind ‘ka’
       ‘ks’ is a rigid type variable bound by
         the type signature for ‘bob’
         at T22793.hs:13:21-22
-      ‘k1’ is a rigid type variable bound by
-        the type signature for ‘bob’
-        at T22793.hs:13:16-17
-    • In the first argument of ‘p’, namely ‘a’
+    • In the second argument of ‘Foo’, namely ‘a’
       In the type signature:
         bob :: forall {k1}
                       {ks}
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index e16789136f..7a8d5aa7b4 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -226,7 +226,6 @@ test('T17963', normal, compile_fail, [''])
 test('T18300', normal, compile_fail, [''])
 test('T18451', normal, compile_fail, [''])
 test('T18451a', normal, compile_fail, [''])
-test('T18451b', normal, compile_fail, [''])
 test('NestedProxies', normal, compile, [''])
 test('T18522-ppr', normal, ghci_script, ['T18522-ppr.script'])
 test('T18855', normal, compile, [''])
diff --git a/testsuite/tests/rep-poly/RepPolyBackpack1.stderr b/testsuite/tests/rep-poly/RepPolyBackpack1.stderr
index cfdf4cf2bd..320ba6a6e1 100644
--- a/testsuite/tests/rep-poly/RepPolyBackpack1.stderr
+++ b/testsuite/tests/rep-poly/RepPolyBackpack1.stderr
@@ -1,6 +1,6 @@
 [1 of 1] Processing number-unknown
-  [1 of 2] Compiling NumberUnknown[sig] ( number-unknown\NumberUnknown.hsig, nothing )
-  [2 of 2] Compiling NumberStuff      ( number-unknown\NumberStuff.hs, nothing )
+  [1 of 2] Compiling NumberUnknown[sig] ( number-unknown/NumberUnknown.hsig, nothing )
+  [2 of 2] Compiling NumberStuff      ( number-unknown/NumberStuff.hs, nothing )
 
 RepPolyBackpack1.bkp:17:5: error: [GHC-55287]
     The second pattern in the equation for ‘funcA’
diff --git a/testsuite/tests/rep-poly/RepPolyInferPatBind.stderr b/testsuite/tests/rep-poly/RepPolyInferPatBind.stderr
index 486de932bd..a9643f4b73 100644
--- a/testsuite/tests/rep-poly/RepPolyInferPatBind.stderr
+++ b/testsuite/tests/rep-poly/RepPolyInferPatBind.stderr
@@ -8,6 +8,8 @@ RepPolyInferPatBind.hs:21:2: error: [GHC-55287]
     • The pattern binding does not have a fixed runtime representation.
       Its type is:
         T :: TYPE R
+      Cannot unify ‘R’ with the type variable ‘p0’
+      because it is not a concrete ‘RuntimeRep’.
     • When checking that the pattern signature: T
         fits the type of its context: T
       In the pattern: x :: T
diff --git a/testsuite/tests/rep-poly/RepPolyInferPatSyn.stderr b/testsuite/tests/rep-poly/RepPolyInferPatSyn.stderr
index 7f5c4f1ca7..4515832b21 100644
--- a/testsuite/tests/rep-poly/RepPolyInferPatSyn.stderr
+++ b/testsuite/tests/rep-poly/RepPolyInferPatSyn.stderr
@@ -4,6 +4,8 @@ RepPolyInferPatSyn.hs:22:16: error: [GHC-55287]
       does not have a fixed runtime representation.
       Its type is:
         T :: TYPE R
+      Cannot unify ‘R’ with the type variable ‘p0’
+      because it is not a concrete ‘RuntimeRep’.
     • When checking that the pattern signature: T
         fits the type of its context: T
       In the pattern: a :: T
diff --git a/testsuite/tests/typecheck/no_skolem_info/T14040.stderr b/testsuite/tests/typecheck/no_skolem_info/T14040.stderr
index c5e44796e1..966e19bec7 100644
--- a/testsuite/tests/typecheck/no_skolem_info/T14040.stderr
+++ b/testsuite/tests/typecheck/no_skolem_info/T14040.stderr
@@ -1,7 +1,7 @@
 
 T14040.hs:27:46: error: [GHC-46956]
-    • Couldn't match kind ‘k1’ with ‘WeirdList z’
-      Expected kind ‘WeirdList k1’,
+    • Couldn't match kind ‘k0’ with ‘WeirdList z’
+      Expected kind ‘WeirdList k0’,
         but ‘xs’ has kind ‘WeirdList (WeirdList z)’
         because kind variable ‘z’ would escape its scope
       This (rigid, skolem) kind variable is bound by
@@ -25,8 +25,8 @@ T14040.hs:27:46: error: [GHC-46956]
                                                                                            -> p _ wl
 
 T14040.hs:28:27: error: [GHC-46956]
-    • Couldn't match kind ‘k0’ with ‘z’
-      Expected kind ‘WeirdList k0’,
+    • Couldn't match kind ‘k1’ with ‘z’
+      Expected kind ‘WeirdList k1’,
         but ‘WeirdCons x xs’ has kind ‘WeirdList z’
         because kind variable ‘z’ would escape its scope
       This (rigid, skolem) kind variable is bound by
diff --git a/testsuite/tests/typecheck/should_compile/T22194.hs b/testsuite/tests/typecheck/should_compile/T22194.hs
new file mode 100644
index 0000000000..70a3988b7c
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T22194.hs
@@ -0,0 +1,64 @@
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PartialTypeSignatures #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE MagicHash, UnboxedTuples #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE NoMonoLocalBinds #-}
+
+module Test where
+
+import Data.Kind
+import GHC.Exts
+
+--import Control.Monad.Primitive -- primitive-0.7.4.0
+--import Data.Primitive.MutVar -- primitive-0.7.4.0
+
+class Monad m => PrimMonad m where
+  type PrimState m
+  primitive :: (State# (PrimState m) -> (# State# (PrimState m), a #)) -> m a
+
+data MutVar s a = MutVar (MutVar# s a)
+
+newMutVar :: PrimMonad m => a -> m (MutVar (PrimState m) a)
+newMutVar = error "urk"
+
+writeMutVar :: PrimMonad m => MutVar (PrimState m) a -> a -> m ()
+writeMutVar  = error "Urk"
+
+-----------
+
+class Monad m => New a m where
+  new :: m a
+
+class Monad m => Add a m e | a -> e where
+  add :: a -> e -> m ()
+
+data T (m :: Type -> Type) = T
+
+instance PrimMonad m => New (T m) m where
+  new = return T
+
+instance PrimMonad m => Add (T m) m Int where
+  add _ _ = return ()
+
+test1 :: forall m. PrimMonad m => m ()
+test1 = do
+  ref <- newMutVar (undefined :: T m)
+  let g () = do
+        t <- new
+        add t (0 :: Int)
+        writeMutVar ref t
+  g ()
+
+test2 :: forall m. PrimMonad m => m ()
+test2 = do
+  (ref :: MutVar (PrimState m) (T m)) <- newMutVar undefined
+  let g () = do
+        t <- new
+        add t (0 :: Int)
+        writeMutVar ref t
+  g ()
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index b2232d8f6e..b3a24ba4bf 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -867,6 +867,7 @@ test('T23018', normal, compile, [''])
 test('T21909', normal, compile, [''])
 test('T21909b', normal, compile, [''])
 test('T21443', normal, compile, [''])
+test('T22194', normal, compile, [''])
 test('QualifiedRecordUpdate',
     [ extra_files(['QualifiedRecordUpdate_aux.hs']) ]
     , multimod_compile, ['QualifiedRecordUpdate', '-v0'])
diff --git a/testsuite/tests/typecheck/should_fail/T12785b.stderr b/testsuite/tests/typecheck/should_fail/T12785b.stderr
index abcdee7619..5957527a61 100644
--- a/testsuite/tests/typecheck/should_fail/T12785b.stderr
+++ b/testsuite/tests/typecheck/should_fail/T12785b.stderr
@@ -1,6 +1,6 @@
 
 T12785b.hs:30:65: error: [GHC-25897]
-    • Could not deduce ‘Payload (S n) (Payload n s1) ~ s’
+    • Could not deduce ‘s ~ Payload (S n) (Payload n s1)’
         arising from a use of ‘SBranchX’
       from the context: m ~ S n
         bound by a pattern with constructor:
diff --git a/testsuite/tests/typecheck/should_fail/T7869.stderr b/testsuite/tests/typecheck/should_fail/T7869.stderr
index f6aa8d0bfc..d8532ea365 100644
--- a/testsuite/tests/typecheck/should_fail/T7869.stderr
+++ b/testsuite/tests/typecheck/should_fail/T7869.stderr
@@ -1,18 +1,16 @@
 
 T7869.hs:3:12: error: [GHC-25897]
-    • Couldn't match type ‘a1’ with ‘a’
+    • Couldn't match type ‘b1’ with ‘b’
       Expected: [a1] -> b1
         Actual: [a] -> b
-      ‘a1’ is a rigid type variable bound by
+      ‘b1’ is a rigid type variable bound by
         an expression type signature:
           forall a1 b1. [a1] -> b1
         at T7869.hs:3:20-27
-      ‘a’ is a rigid type variable bound by
+      ‘b’ is a rigid type variable bound by
         the inferred type of f :: [a] -> b
         at T7869.hs:3:1-27
     • In the expression: f x
       In the expression: (\ x -> f x) :: [a] -> b
       In an equation for ‘f’: f = (\ x -> f x) :: [a] -> b
-    • Relevant bindings include
-        x :: [a1] (bound at T7869.hs:3:7)
-        f :: [a] -> b (bound at T7869.hs:3:1)
+    • Relevant bindings include f :: [a] -> b (bound at T7869.hs:3:1)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail097.stderr b/testsuite/tests/typecheck/should_fail/tcfail097.stderr
index bad134d6bd..1caa93ab8d 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail097.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail097.stderr
@@ -8,9 +8,9 @@ tcfail097.hs:5:6: error: [GHC-39999]
       The type variable ‘a0’ is ambiguous
       Potentially matching instances:
         instance Eq Ordering -- Defined in ‘GHC.Classes’
-        instance Eq Integer -- Defined in ‘GHC.Num.Integer’
-        ...plus 23 others
-        ...plus four instances involving out-of-scope types
+        instance Eq a => Eq (Solo a) -- Defined in ‘GHC.Classes’
+        ...plus 22 others
+        ...plus five instances involving out-of-scope types
         (use -fprint-potential-instances to see them all)
     • In the ambiguity check for ‘f’
       To defer the ambiguity check to use sites, enable AllowAmbiguousTypes