Implement QuantifiedConstraints

We have wanted quantified constraints for ages and, as I hoped,
they proved remarkably simple to implement.   All the machinery was
already in place.

The main ticket is Trac #2893, but also relevant are
  #5927
  #8516
  #9123 (especially!  higher kinded roles)
  #14070
  #14317

The wiki page is
  https://ghc.haskell.org/trac/ghc/wiki/QuantifiedConstraints
which in turn contains a link to the GHC Proposal where the change
is specified.

Here is the relevant Note:

Note [Quantified constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The -XQuantifiedConstraints extension allows type-class contexts like
this:

  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

Note the (forall b. Eq b => Eq (f b)) in the instance contexts.
This quantified constraint is needed to solve the
 [W] (Eq (f (Rose f x)))
constraint which arises form the (==) definition.

Here are the moving parts
  * Language extension {-# LANGUAGE QuantifiedConstraints #-}
    and add it to ghc-boot-th:GHC.LanguageExtensions.Type.Extension

  * A new form of evidence, EvDFun, that is used to discharge
    such wanted constraints

  * checkValidType gets some changes to accept forall-constraints
    only in the right places.

  * Type.PredTree gets a new constructor ForAllPred, and
    and classifyPredType analyses a PredType to decompose
    the new forall-constraints

  * Define a type TcRnTypes.QCInst, which holds a given
    quantified constraint in the inert set

  * TcSMonad.InertCans gets an extra field, inert_insts :: [QCInst],
    which holds all the Given forall-constraints.  In effect,
    such Given constraints are like local instance decls.

  * When trying to solve a class constraint, via
    TcInteract.matchInstEnv, use the InstEnv from inert_insts
    so that we include the local Given forall-constraints
    in the lookup.  (See TcSMonad.getInstEnvs.)

  * topReactionsStage calls doTopReactOther for CIrredCan and
    CTyEqCan, so they can try to react with any given
    quantified constraints (TcInteract.matchLocalInst)

  * TcCanonical.canForAll deals with solving a
    forall-constraint.  See
       Note [Solving a Wanted forall-constraint]
       Note [Solving a Wanted forall-constraint]

  * We augment the kick-out code to kick out an inert
    forall constraint if it can be rewritten by a new
    type equality; see TcSMonad.kick_out_rewritable

Some other related refactoring
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

* Move SCC on evidence bindings to post-desugaring, which fixed
  #14735, and is generally nicer anyway because we can use
  existing CoreSyn free-var functions.  (Quantified constraints
  made the free-vars of an ev-term a bit more complicated.)

* In LookupInstResult, replace GenInst with OneInst and NotSure,
  using the latter for multiple matches and/or one or more
  unifiers

11 files changed, 301 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/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..71f5b9159a
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/all.T
@@ -0,0 +1,10 @@
+
+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, [''])