update to current master againwip/T13904

27 files changed, 642 insertions, 0 deletions

diff --git a/testsuite/tests/quantified-constraints/Makefile b/testsuite/tests/quantified-constraints/Makefile
new file mode 100644
index 0000000000..9a36a1c5fe
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/Makefile
@@ -0,0 +1,3 @@
+TOP=../..
+include $(TOP)/mk/boilerplate.mk
+include $(TOP)/mk/test.mk
diff --git a/testsuite/tests/quantified-constraints/T14833.hs b/testsuite/tests/quantified-constraints/T14833.hs
new file mode 100644
index 0000000000..43b6491def
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T14833.hs
@@ -0,0 +1,28 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE UndecidableInstances #-}
+module T14833 where
+
+data Dict c where
+  Dict :: c => Dict c
+
+class    (a => b) => Implies a b
+instance (a => b) => Implies a b
+
+-- Works ok
+iota1 :: (() => a) => Dict a
+iota1 = Dict
+
+iota2 :: Implies () a => Dict a
+iota2 = Dict
+
+{-
+[G] Implies () a
+[G] (() => a)      -- By superclass
+
+[W] a
+-}
diff --git a/testsuite/tests/quantified-constraints/T14835.hs b/testsuite/tests/quantified-constraints/T14835.hs
new file mode 100644
index 0000000000..de9b450b7c
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T14835.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE UndecidableInstances #-}
+module Bug where
+
+data Dict c where
+  Dict :: c => Dict c
+
+class    (a => b) => Implies a b
+instance (a => b) => Implies a b
+
+curryC1 :: ((a, b) => c) => Dict (Implies a (Implies b c))
+curryC1 = Dict
+
+curryC2 :: Implies (a, b) c => Dict (Implies a (Implies b c))
+curryC2 = Dict
diff --git a/testsuite/tests/quantified-constraints/T14863.hs b/testsuite/tests/quantified-constraints/T14863.hs
new file mode 100644
index 0000000000..35e1a14b42
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T14863.hs
@@ -0,0 +1,27 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ImpredicativeTypes #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE UndecidableInstances #-}
+module T14863 where
+
+data Dict c where
+  Dict :: c => Dict c
+
+class    (a => b) => Implies a b
+instance (a => b) => Implies a b
+
+uncurryCImpredic1 :: forall a b c. Implies a (b => c) => Dict (Implies (a, b) c)
+uncurryCImpredic1 = Dict
+
+uncurryCImpredic2 :: forall a b c. a => Implies b c => Dict (Implies (a, b) c)
+uncurryCImpredic2 = Dict
+
+uncurryC1 :: forall a b c. (a => b => c) => Dict (Implies (a, b) c)
+uncurryC1 = Dict
+
+uncurryC2 :: forall a b c. Implies a (Implies b c) => Dict (Implies (a, b) c)
+uncurryC2 = Dict
diff --git a/testsuite/tests/quantified-constraints/T14961.hs b/testsuite/tests/quantified-constraints/T14961.hs
new file mode 100644
index 0000000000..6f15ceb572
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T14961.hs
@@ -0,0 +1,98 @@
+{-# LANGUAGE ConstraintKinds           #-}
+{-# LANGUAGE InstanceSigs              #-}
+{-# LANGUAGE FlexibleContexts          #-}
+{-# LANGUAGE FlexibleInstances         #-}
+{-# LANGUAGE GADTs                     #-}
+{-# LANGUAGE MultiParamTypeClasses     #-}
+{-# LANGUAGE RankNTypes                #-}
+{-# LANGUAGE TypeFamilies              #-}
+{-# LANGUAGE TypeFamilyDependencies    #-}
+{-# LANGUAGE TypeInType                #-}
+{-# LANGUAGE TypeOperators             #-}
+{-# LANGUAGE UndecidableInstances      #-}
+{-# LANGUAGE QuantifiedConstraints     #-}
+
+module T14961 where
+
+import           Data.Kind
+
+import           Control.Arrow              (left, right, (&&&), (|||))
+import           Control.Category
+import           Prelude                    hiding (id, (.))
+
+import           Data.Coerce
+
+class    (forall x. f x => g x) => f ~=> g
+instance (forall x. f x => g x) => f ~=> g
+
+type family (#) (p :: Type -> Type -> Type) (ab :: (Type, Type))
+  = (r :: Type) | r -> p ab where
+  p # '(a, b) = p a b
+
+newtype Glass
+  :: ((Type -> Type -> Type) -> Constraint)
+  -> (Type, Type) -> (Type, Type) -> Type where
+  Glass :: (forall p. z p => p # ab -> p # st) -> Glass z st ab
+
+data A_Prism
+
+type family ConstraintOf (tag :: Type)
+  = (r :: (Type -> Type -> Type) -> Constraint) where
+  ConstraintOf A_Prism = Choice
+
+_Left0
+  :: Glass Choice
+       '(Either a x, Either b x)
+       '(a, b)
+_Left0 = Glass left'
+
+_Left1
+  :: c ~=> Choice
+  => Glass c '(Either a x, Either b x) '(a, b)
+_Left1 = Glass left'
+
+-- fails with
+-- • Could not deduce (Choice p)
+-- _Left2
+--   :: (forall p. c p => ConstraintOf A_Prism p)
+--   => Glass c '(Either a x, Either b x) '(a, b)
+-- _Left2 = Glass left'
+
+_Left3
+  :: d ~ ConstraintOf A_Prism
+  => (forall p . c p => d p)
+  => Glass c
+       '(Either a x, Either b x)
+       '(a, b)
+_Left3 = Glass left'
+
+-- fails to typecheck unless at least a partial type signature is provided
+-- l :: c ~=> Choice => Glass c _ _
+-- l = _Left1 . _Left1
+
+newtype Optic o st ab where
+  Optic
+    :: (forall c d. (d ~ ConstraintOf o, c ~=> d) => Glass c st ab)
+    -> Optic o st ab
+
+_Left
+  :: Optic A_Prism
+       '(Either a x, Either b x)
+       '(a, b)
+_Left = Optic _Left1
+
+instance Category (Glass z) where
+  id :: Glass z a a
+  id = Glass id
+
+  (.) :: Glass z uv ab -> Glass z st uv -> Glass z st ab
+  Glass abuv . Glass uvst = Glass (uvst . abuv)
+
+class Profunctor (p :: Type -> Type -> Type) where
+  dimap :: (a -> b) -> (c -> d) -> p b c -> p a d
+  lmap :: (a -> b) -> p b c -> p a c
+  rmap :: (b -> c) -> p a b -> p a c
+
+class Profunctor p => Choice (p :: Type -> Type -> Type) where
+  left' :: p a b -> p (Either a c) (Either b c)
+  right' :: p a b -> p (Either c a) (Either c b)
diff --git a/testsuite/tests/quantified-constraints/T15231.hs b/testsuite/tests/quantified-constraints/T15231.hs
new file mode 100644
index 0000000000..7b7834d1f2
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T15231.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+module Bug where
+
+import Data.Kind
+
+data ECC :: Constraint -> Type -> Type
+
+class Y a
+class Z a
+
+instance  c         => Y (ECC c a)
+instance (c => Z a) => Z (ECC c a)
diff --git a/testsuite/tests/quantified-constraints/T15231.stderr b/testsuite/tests/quantified-constraints/T15231.stderr
new file mode 100644
index 0000000000..afb7ac3a25
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T15231.stderr
@@ -0,0 +1,7 @@
+
+T15231.hs:15:10: error:
+    • Variable ‘c’ occurs more often
+        in the constraint ‘c’ than in the instance head ‘Z a’
+      (Use UndecidableInstances to permit this)
+    • In the quantified constraint ‘c => Z a’
+      In the instance declaration for ‘Z (ECC c a)’
diff --git a/testsuite/tests/quantified-constraints/T15244.hs b/testsuite/tests/quantified-constraints/T15244.hs
new file mode 100644
index 0000000000..16d2b65d53
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T15244.hs
@@ -0,0 +1,69 @@
+{-# LANGUAGE QuantifiedConstraints, TypeFamilies #-}
+
+module T15244 where
+class (forall t . Eq (c t)) => Blah c
+
+-- Unquantified works
+foo :: (Eq (a t), Eq (b t), a ~ b) => a t -> b t -> Bool
+foo a b = a == b
+-- Works
+
+-- Two quantified instances fail with double ambiguity check errors
+bar :: (forall t . Eq (a t), forall t . Eq (b t), a ~ b) => a t -> b t -> Bool
+bar a b = a == b
+-- Minimal.hs:11:8: error:
+--     • Could not deduce (Eq (b t1))
+--       from the context: (forall t1. Eq (a t1), forall t1. Eq (b t1),
+--                          a ~ b)
+--         bound by the type signature for:
+--                    bar :: forall (a :: * -> *) (b :: * -> *) t.
+--                           (forall t1. Eq (a t1), forall t1. Eq (b t1), a ~ b) =>
+--                           a t -> b t -> Bool
+--         at Minimal.hs:11:8-78
+--     • In the ambiguity check for ‘bar’
+--       To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
+--       In the type signature:
+--         bar :: (forall t. Eq (a t), forall t. Eq (b t), a ~ b) =>
+--                a t -> b t -> Bool
+--    |
+-- 11 | bar :: (forall t . Eq (a t), forall t . Eq (b t), a ~ b) => a t -> b t -> Bool
+--    |
+-- [And then another copy of the same error]
+
+-- Two copies from superclass instances fail
+baz :: (Blah a, Blah b, a ~ b) => a t -> b t -> Bool
+baz a b = a == b
+-- Minimal.hs:34:11: error:
+--     • Could not deduce (Eq (b t)) arising from a use of ‘==’
+--       from the context: (Blah a, Blah b, a ~ b)
+--         bound by the type signature for:
+--                    baz :: forall (a :: * -> *) (b :: * -> *) t.
+--                           (Blah a, Blah b, a ~ b) =>
+--                           a t -> b t -> Bool
+--         at Minimal.hs:33:1-52
+--     • In the expression: a == b
+--       In an equation for ‘baz’: baz a b = a == b
+--    |
+-- 34 | baz a b = a == b
+--    |
+
+-- Two copies from superclass from same declaration also fail
+mugga :: (Blah a, Blah a) => a t -> a t -> Bool
+mugga a b = a == b
+--     • Could not deduce (Eq (a t)) arising from a use of ‘==’
+--       from the context: (Blah a, Blah a)
+--         bound by the type signature for:
+--                    mugga :: forall (a :: * -> *) t.
+--                             (Blah a, Blah a) =>
+--                             a t -> a t -> Bool
+--         at Minimal.hs:50:1-47
+--     • In the expression: a == b
+--       In an equation for ‘mugga’: mugga a b = a == b
+--    |
+-- 51 | mugga a b = a == b
+--    |
+
+-- One copy works
+quux :: (Blah a, a ~ b) => a t -> b t -> Bool
+quux a b = a == b
+-- Works
diff --git a/testsuite/tests/quantified-constraints/T15290.hs b/testsuite/tests/quantified-constraints/T15290.hs
new file mode 100644
index 0000000000..8a0c3d989f
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T15290.hs
@@ -0,0 +1,35 @@
+{-# LANGUAGE TypeApplications, ImpredicativeTypes, ScopedTypeVariables,
+             QuantifiedConstraints, StandaloneDeriving, GeneralizedNewtypeDeriving #-}
+
+module T15290 where
+
+import Prelude hiding ( Monad(..) )
+import Data.Coerce ( Coercible, coerce )
+
+class Monad m where
+  join  :: m (m a) -> m a
+
+newtype StateT s m a = StateT { runStateT :: s -> m (s, a) }
+
+newtype IntStateT m a = IntStateT { runIntStateT :: StateT Int m a }
+
+instance Monad m => Monad (StateT s m) where
+  join = error "urk"
+
+instance (Monad m, forall p q. Coercible p q => Coercible (m p) (m q))
+      => Monad (IntStateT m) where
+
+--   Fails with the impredicative instantiation of coerce, succeeds without
+
+-- Impredicative version (fails)
+--    join = coerce
+--          @(forall a. StateT Int m (StateT Int m a) -> StateT Int m a)
+--          @(forall a. IntStateT m (IntStateT m a)   -> IntStateT m a)
+--          join
+
+
+-- Predicative version (succeeds)
+    join = (coerce
+           @(StateT Int m (StateT Int m a) -> StateT Int m a)
+           @(IntStateT m (IntStateT m a)   -> IntStateT m a)
+           join) :: forall a. IntStateT m (IntStateT m a)   -> IntStateT m a
diff --git a/testsuite/tests/quantified-constraints/T15290a.hs b/testsuite/tests/quantified-constraints/T15290a.hs
new file mode 100644
index 0000000000..bfb5b2a069
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T15290a.hs
@@ -0,0 +1,35 @@
+{-# LANGUAGE TypeApplications, ImpredicativeTypes, ScopedTypeVariables,
+             QuantifiedConstraints, StandaloneDeriving, GeneralizedNewtypeDeriving #-}
+
+module T15290a where
+
+import Prelude hiding ( Monad(..) )
+import Data.Coerce ( Coercible, coerce )
+
+class Monad m where
+  join  :: m (m a) -> m a
+
+newtype StateT s m a = StateT { runStateT :: s -> m (s, a) }
+
+newtype IntStateT m a = IntStateT { runIntStateT :: StateT Int m a }
+
+instance Monad m => Monad (StateT s m) where
+  join = error "urk"
+
+instance (Monad m, forall p q. Coercible p q => Coercible (m p) (m q))
+      => Monad (IntStateT m) where
+
+--   Fails with the impredicative instantiation of coerce, succeeds without
+
+-- Impredicative version (fails)
+    join = coerce
+          @(forall a. StateT Int m (StateT Int m a) -> StateT Int m a)
+          @(forall a. IntStateT m (IntStateT m a)   -> IntStateT m a)
+          join
+
+
+-- Predicative version (succeeds)
+--    join = (coerce
+--           @(StateT Int m (StateT Int m a) -> StateT Int m a)
+--           @(IntStateT m (IntStateT m a)   -> IntStateT m a)
+--           join) :: forall a. IntStateT m (IntStateT m a)   -> IntStateT m a
diff --git a/testsuite/tests/quantified-constraints/T15290a.stderr b/testsuite/tests/quantified-constraints/T15290a.stderr
new file mode 100644
index 0000000000..2efd784f31
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T15290a.stderr
@@ -0,0 +1,22 @@
+
+T15290a.hs:25:12: error:
+    • Couldn't match representation of type ‘m (Int, IntStateT m a1)’
+                               with that of ‘m (Int, StateT Int m a1)’
+        arising from a use of ‘coerce’
+      NB: We cannot know what roles the parameters to ‘m’ have;
+        we must assume that the role is nominal
+    • In the expression:
+        coerce
+          @(forall a. StateT Int m (StateT Int m a) -> StateT Int m a)
+          @(forall a. IntStateT m (IntStateT m a) -> IntStateT m a)
+          join
+      In an equation for ‘join’:
+          join
+            = coerce
+                @(forall a. StateT Int m (StateT Int m a) -> StateT Int m a)
+                @(forall a. IntStateT m (IntStateT m a) -> IntStateT m a)
+                join
+      In the instance declaration for ‘Monad (IntStateT m)’
+    • Relevant bindings include
+        join :: IntStateT m (IntStateT m a) -> IntStateT m a
+          (bound at T15290a.hs:25:5)
diff --git a/testsuite/tests/quantified-constraints/T15290b.hs b/testsuite/tests/quantified-constraints/T15290b.hs
new file mode 100644
index 0000000000..ce99aa9454
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T15290b.hs
@@ -0,0 +1,28 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE ImpredicativeTypes #-}
+{-# LANGUAGE InstanceSigs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+module T15290b where
+
+import Data.Coerce
+import Data.Kind
+
+type Representational1 m = (forall a b. Coercible a b => Coercible (m a) (m b) :: Constraint)
+
+class Representational1 f => Functor' f where
+  fmap' :: (a -> b) -> f a -> f b
+
+class Functor' f => Applicative' f where
+  pure'  :: a -> f a
+  (<*>@) :: f (a -> b) -> f a -> f b
+
+class Functor' t => Traversable' t where
+  traverse' :: Applicative' f => (a -> f b) -> t a -> f (t b)
+
+-- Typechecks
+newtype T1 m a = MkT1 (m a) deriving (Functor', Traversable')
diff --git a/testsuite/tests/quantified-constraints/T15290b.stderr b/testsuite/tests/quantified-constraints/T15290b.stderr
new file mode 100644
index 0000000000..7dc1852c6d
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T15290b.stderr
@@ -0,0 +1,14 @@
+
+T15290b.hs:28:49: error:
+    • Couldn't match representation of type ‘f (m b)’
+                               with that of ‘f (T1 m b)’
+        arising from the coercion of the method ‘traverse'’
+          from type ‘forall (f :: * -> *) a b.
+                     Applicative' f =>
+                     (a -> f b) -> m a -> f (m b)’
+            to type ‘forall (f :: * -> *) a b.
+                     Applicative' f =>
+                     (a -> f b) -> T1 m a -> f (T1 m b)’
+      NB: We cannot know what roles the parameters to ‘f’ have;
+        we must assume that the role is nominal
+    • When deriving the instance for (Traversable' (T1 m))
diff --git a/testsuite/tests/quantified-constraints/T15316.hs b/testsuite/tests/quantified-constraints/T15316.hs
new file mode 100644
index 0000000000..07539e3183
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T15316.hs
@@ -0,0 +1,21 @@
+{-# LANGUAGE RankNTypes, QuantifiedConstraints, ConstraintKinds  #-}
+-- NB: disabling these if enabled:
+{-# LANGUAGE NoUndecidableInstances, NoUndecidableSuperClasses #-}
+
+module T15316 where
+
+import Data.Proxy
+
+{-
+class Class a where
+         method :: a
+
+subsume :: (Class a => Class b) => Proxy a -> Proxy b -> ((Class a => Class b) => r) -> r
+subsume _ _ x = x
+
+value :: Proxy a -> a
+value p = subsume p p method
+-}
+
+subsume' :: Proxy c -> ((c => c) => r) -> r
+subsume' _ x = x
diff --git a/testsuite/tests/quantified-constraints/T15316.stderr b/testsuite/tests/quantified-constraints/T15316.stderr
new file mode 100644
index 0000000000..4444c2c453
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T15316.stderr
@@ -0,0 +1,6 @@
+
+T15316.hs:20:13: error:
+    • The constraint ‘c’ is no smaller than the instance head ‘c’
+      (Use UndecidableInstances to permit this)
+    • In the quantified constraint ‘c => c’
+      In the type signature: subsume' :: Proxy c -> ((c => c) => r) -> r
diff --git a/testsuite/tests/quantified-constraints/T15334.hs b/testsuite/tests/quantified-constraints/T15334.hs
new file mode 100644
index 0000000000..88d7c3f376
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T15334.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE MultiParamTypeClasses, PolyKinds, QuantifiedConstraints, RankNTypes #-}
+
+module T15334 where
+
+class C m a
+class D m a
+
+f :: (forall a. Eq a => (C m a, D m a)) => m a
+f = undefined
diff --git a/testsuite/tests/quantified-constraints/T15334.stderr b/testsuite/tests/quantified-constraints/T15334.stderr
new file mode 100644
index 0000000000..902d7a71e5
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T15334.stderr
@@ -0,0 +1,6 @@
+
+T15334.hs:8:6: error:
+    • You can't specify an instance for a tuple constraint
+    • In the quantified constraint ‘forall a. Eq a => (C m a, D m a)’
+      In the type signature:
+        f :: (forall a. Eq a => (C m a, D m a)) => m a
diff --git a/testsuite/tests/quantified-constraints/T15359.hs b/testsuite/tests/quantified-constraints/T15359.hs
new file mode 100644
index 0000000000..7ef1cc5572
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T15359.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE MultiParamTypeClasses, GADTs, RankNTypes,
+             ConstraintKinds, QuantifiedConstraints #-}
+
+module T15359 where
+
+class C a b
+
+data Dict c where
+  Dict :: c => Dict c
+
+foo :: (forall a b. C a b => a ~ b) => Dict (C a b) -> a -> b
+foo Dict x = x
diff --git a/testsuite/tests/quantified-constraints/T15359a.hs b/testsuite/tests/quantified-constraints/T15359a.hs
new file mode 100644
index 0000000000..6ec5f861a8
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T15359a.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE MultiParamTypeClasses, GADTs, RankNTypes,
+             ConstraintKinds, QuantifiedConstraints,
+             UndecidableInstances #-}
+
+module T15359a where
+
+class C a b
+class a ~ b => D a b
+
+data Dict c where
+  Dict :: c => Dict c
+
+foo :: (forall a b. C a b => D a b) => Dict (C a b) -> a -> b
+foo Dict x = x
diff --git a/testsuite/tests/quantified-constraints/T15625.hs b/testsuite/tests/quantified-constraints/T15625.hs
new file mode 100644
index 0000000000..8fe092da98
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T15625.hs
@@ -0,0 +1,16 @@
+{-# Language GADTs, MultiParamTypeClasses, QuantifiedConstraints #-}
+
+module T15625 where
+
+import Data.Coerce
+
+class a ~ b => Equal a b
+
+test1 :: (forall b. a ~ b) => a
+test1 = False
+
+test2 :: (forall b. Equal a b) => a
+test2 = False
+
+test3 :: (forall b. Coercible a b) => a
+test3 = coerce False
diff --git a/testsuite/tests/quantified-constraints/T15625a.hs b/testsuite/tests/quantified-constraints/T15625a.hs
new file mode 100644
index 0000000000..ca049cb19d
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T15625a.hs
@@ -0,0 +1,20 @@
+{-# Language RankNTypes, ConstraintKinds, QuantifiedConstraints,
+             PolyKinds, GADTs, MultiParamTypeClasses,
+             DataKinds, FlexibleInstances #-}
+
+module T15625a where
+
+import Data.Kind
+
+type Cat ob = ob -> ob -> Type
+
+data KLEISLI (m :: Type -> Type) :: Cat (KL_kind m) where
+  MkKLEISLI :: (a -> m b) -> KLEISLI(m) (KL a) (KL b)
+
+data KL_kind (m :: Type -> Type) = KL Type
+
+class    (a ~ KL xx) => AsKL a xx
+instance (a ~ KL xx) => AsKL a xx
+
+ekki__ :: Monad m => (forall xx. AsKL a xx) => KLEISLI m a a
+ekki__ = MkKLEISLI undefined
diff --git a/testsuite/tests/quantified-constraints/T2893.hs b/testsuite/tests/quantified-constraints/T2893.hs
new file mode 100644
index 0000000000..ffec2cf72d
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T2893.hs
@@ -0,0 +1,18 @@
+{-# LANGUAGE QuantifiedConstraints  #-}
+
+-- Two simple examples that should work
+
+module T2893 where
+
+f :: forall b c. (Eq b, forall a. Eq a => Eq (c a)) => c b -> Bool
+{-# NOINLINE f #-}
+f x = x==x
+
+g x = f [x]
+
+data Rose f x = Rose x (f (Rose f x))
+
+instance (Eq a, forall b. Eq b => Eq (f b))
+      => Eq (Rose f a)  where
+  (Rose x1 rs1) == (Rose x2 rs2)
+     = x1==x2 && rs1 == rs2
diff --git a/testsuite/tests/quantified-constraints/T2893a.hs b/testsuite/tests/quantified-constraints/T2893a.hs
new file mode 100644
index 0000000000..187029fdd5
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T2893a.hs
@@ -0,0 +1,27 @@
+{-# LANGUAGE
+    GADTs
+  , FlexibleContexts
+  , RankNTypes
+  , ScopedTypeVariables
+  , QuantifiedConstraints #-}
+
+module T2893a where
+
+import Control.Monad.ST
+import Data.Array.ST
+
+sortM
+  :: forall a s.
+     (Ord a, MArray (STUArray s) a (ST s))
+  => [a]
+  -> ST s [a]
+sortM xs = do
+  arr <- newListArray (1, length xs) xs
+           :: ST s (STUArray s Int a)
+  -- do some in-place sorting here
+  getElems arr
+
+sortP_3
+  :: (Ord a, forall s. MArray (STUArray s) a (ST s))
+  => [a] -> [a]
+sortP_3 xs = runST (sortM xs)
diff --git a/testsuite/tests/quantified-constraints/T2893c.hs b/testsuite/tests/quantified-constraints/T2893c.hs
new file mode 100644
index 0000000000..832d0f8428
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T2893c.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE QuantifiedConstraints  #-}
+
+module T2893c where
+
+data Rose f x = Rose x (f (Rose f x))
+
+instance Eq a => Eq (Rose f a)  where
+  (Rose x1 _) == (Rose x2 _) = x1==x2
+
+-- Needs superclasses
+instance (Ord a, forall b. Ord b => Ord (f b))
+      => Ord (Rose f a)  where
+  (Rose x1 rs1) >= (Rose x2 rs2)
+     = x1 >= x2 && rs1 == rs2
+  a <= b = False  -- Just to suppress the warning
diff --git a/testsuite/tests/quantified-constraints/T9123.hs b/testsuite/tests/quantified-constraints/T9123.hs
new file mode 100644
index 0000000000..130312b150
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T9123.hs
@@ -0,0 +1,25 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE InstanceSigs, RoleAnnotations  #-}
+
+module T9123 where
+
+import Data.Coerce
+
+type role Wrap representational nominal
+newtype Wrap m a = Wrap (m a)
+
+class Monad' m where
+  join' :: forall a. m (m a) -> m a
+
+-- Tests the superclass stuff
+instance (forall p q. Coercible p q => Coercible (m p) (m q), Monad' m) => Monad' (Wrap m) where
+  join' :: forall a. Wrap m (Wrap m a) -> Wrap m a
+  join' = coerce @(m (m a) -> m a)
+                 @(Wrap m (Wrap m a) -> Wrap m a)
+                 join'
+
diff --git a/testsuite/tests/quantified-constraints/T9123a.hs b/testsuite/tests/quantified-constraints/T9123a.hs
new file mode 100644
index 0000000000..76379b6c00
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T9123a.hs
@@ -0,0 +1,30 @@
+{-# LANGUAGE QuantifiedConstraints, PolyKinds, ScopedTypeVariables
+           , StandaloneDeriving, RoleAnnotations, TypeApplications
+           , UndecidableInstances, InstanceSigs
+           , GeneralizedNewtypeDeriving #-}
+
+module T9123a where
+
+import Data.Coerce
+
+class MyMonad m where
+  join :: m (m a) -> m a
+
+newtype StateT s m a = StateT (s -> m (a, s))
+
+type role StateT nominal representational nominal   -- as inferred
+
+instance MyMonad m => MyMonad (StateT s m) where
+  join = error "urk"  -- A good impl exists, but is not
+                      -- of interest for this test case
+
+newtype IntStateT m a = IntStateT (StateT Int m a)
+
+type role IntStateT representational nominal   -- as inferred
+
+instance (MyMonad m, forall p q. Coercible p q => Coercible (m p) (m q))
+               => MyMonad (IntStateT m) where
+  join :: forall a. IntStateT m (IntStateT m a) -> IntStateT m a
+  join = coerce @(StateT Int m (StateT Int m a) -> StateT Int m a)
+                @(IntStateT  m (IntStateT  m a) -> IntStateT  m a)
+                join
diff --git a/testsuite/tests/quantified-constraints/all.T b/testsuite/tests/quantified-constraints/all.T
new file mode 100644
index 0000000000..1e2eca8358
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/all.T
@@ -0,0 +1,22 @@
+
+test('T14833', normal, compile, [''])
+test('T14835', normal, compile, [''])
+test('T2893', normal, compile, [''])
+test('T2893a', normal, compile, [''])
+test('T2893c', normal, compile, [''])
+test('T9123', normal, compile, [''])
+test('T14863', normal, compile, [''])
+test('T14961', normal, compile, [''])
+test('T9123a', normal, compile, [''])
+test('T15244', normal, compile, [''])
+test('T15231', normal, compile_fail, [''])
+
+test('T15290', normal, compile, [''])
+test('T15290a', normal, compile_fail, [''])
+test('T15290b', normal, compile_fail, [''])
+test('T15316', normal, compile_fail, [''])
+test('T15334', normal, compile_fail, [''])
+test('T15359', normal, compile, [''])
+test('T15359a', normal, compile, [''])
+test('T15625', normal, compile, [''])
+test('T15625a', normal, compile, [''])