    {-# LANGUAGE CPP #-}
    {-# LANGUAGE FunctionalDependencies #-}
    {-# LANGUAGE UndecidableInstances #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE FlexibleInstances #-}
    {-# LANGUAGE ConstraintKinds #-}
    {-# LANGUAGE TypeOperators #-}
    {-# LANGUAGE TypeFamilies #-}
    {-# LANGUAGE RankNTypes #-}
    {-# LANGUAGE PolyKinds #-}
    {-# LANGUAGE UndecidableSuperClasses #-}
    {-# LANGUAGE Trustworthy #-}
    {-# LANGUAGE FlexibleContexts #-}
    {-# LANGUAGE QuantifiedConstraints #-}
    {-# LANGUAGE GADTs #-}

    -- |
    -- Copyright   :  (C) 2011-2021 Edward Kmett,
    --                (C) 2015 Ørjan Johansen,
    --                (C) 2016 David Feuer
    -- License     :  BSD-style (see the file LICENSE)
    --
    -- Maintainer  :  Edward Kmett <ekmett@gmail.com>
    -- Stability   :  experimental
    -- Portability :  non-portable
    --
    -- This module uses a trick to provide quantification over constraints.

    module Data.Constraint.Forall
      ( Forall, inst
      , ForallF, instF
      , Forall1, inst1
      , ForallT, instT
      , ForallV, InstV (instV)
      , forall_
      ) where

    import Data.Constraint
    import Unsafe.Coerce (unsafeCoerce)

    class (forall a. p a) => Forall (p :: k -> Constraint)
    instance (forall a. p a) => Forall (p :: k -> Constraint)

    -- | Instantiate a quantified @'Forall' p@ constraint at type @a@.
    inst :: forall p a. Forall p :- p a
    inst :: forall {k} (p :: k -> Constraint) (a :: k). Forall p :- p a
    inst = (Forall p => Dict (p a)) -> Forall p :- p a
    forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
    Sub Dict (p a)
    Forall p => Dict (p a)
    forall (a :: Constraint). a => Dict a
    Dict

    data Dict1 p where
      Dict1 :: (forall a. p a) => Dict1 p

    forallish :: forall p. Dict1 p -> Dict (Forall p)
    forallish :: forall {k} (p :: k -> Constraint). Dict1 p -> Dict (Forall p)
    forallish Dict1 p
    Dict1 = Dict (Forall p)
    forall (a :: Constraint). a => Dict a
    Dict

    forall_ :: forall p. (forall a. Dict (p a)) -> Dict (Forall p)
    forall_ :: forall {k} (p :: k -> Constraint).
    (forall (a :: k). Dict (p a)) -> Dict (Forall p)
    forall_ forall (a :: k). Dict (p a)
    d = Dict1 p -> Dict (Forall p)
    forall {k} (p :: k -> Constraint). Dict1 p -> Dict (Forall p)
    forallish (Dict (p (ZonkAny 0)) -> Dict1 p
    forall a b. a -> b
    unsafeCoerce Dict (p (ZonkAny 0))
    forall (a :: k). Dict (p a)
    d)

    -- | Composition for constraints.
    class p (f a) => ComposeC (p :: k2 -> Constraint) (f :: k1 -> k2) (a :: k1)
    instance p (f a) => ComposeC p f a

    -- | A representation of the quantified constraint @forall a. p (f a)@.
    class Forall (ComposeC p f) => ForallF (p :: k2 -> Constraint) (f :: k1 -> k2)
    instance Forall (ComposeC p f) => ForallF p f

    -- | Instantiate a quantified @'ForallF' p f@ constraint at type @a@.
    instF :: forall p f a . ForallF p f :- p (f a)
    instF :: forall {k2} {k1} (p :: k2 -> Constraint) (f :: k1 -> k2) (a :: k1).
    ForallF p f :- p (f a)
    instF = (ForallF p f => Dict (p (f a))) -> ForallF p f :- p (f a)
    forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
    Sub ((ForallF p f => Dict (p (f a))) -> ForallF p f :- p (f a))
    -> (ForallF p f => Dict (p (f a))) -> ForallF p f :- p (f a)
    forall a b. (a -> b) -> a -> b
    $
      case Forall (ComposeC p f) :- ComposeC p f a
    forall {k} (p :: k -> Constraint) (a :: k). Forall p :- p a
    inst :: Forall (ComposeC p f) :- ComposeC p f a of
        Sub Dict (ComposeC p f a)
    Forall (ComposeC p f) => Dict (ComposeC p f a)
    Dict -> Dict (p (f a))
    forall (a :: Constraint). a => Dict a
    Dict

    -- Classes building up to ForallT
    class p (t a b) => R (p :: k3 -> Constraint) (t :: k1 -> k2 -> k3) (a :: k1) (b :: k2)
    instance p (t a b) => R p t a b
    class Forall (R p t a) => Q (p :: k3 -> Constraint) (t :: k1 -> k2 -> k3) (a :: k1)
    instance Forall (R p t a) => Q p t a

    -- | A representation of the quantified constraint @forall f a. p (t f a)@.
    class Forall (Q p t) => ForallT (p :: k4 -> Constraint) (t :: (k1 -> k2) -> k3 -> k4)
    instance Forall (Q p t) => ForallT p t

    -- | Instantiate a quantified @'ForallT' p t@ constraint at types @f@ and @a@.
    instT :: forall k1 k2 k3 k4 (p :: k4 -> Constraint) (t :: (k1 -> k2) -> k3 -> k4) (f :: k1 -> k2) (a :: k3). ForallT p t :- p (t f a)
    instT :: forall k1 k2 k3 k4 (p :: k4 -> Constraint)
           (t :: (k1 -> k2) -> k3 -> k4) (f :: k1 -> k2) (a :: k3).
    ForallT p t :- p (t f a)
    instT = (ForallT p t => Dict (p (t f a))) -> ForallT p t :- p (t f a)
    forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
    Sub ((ForallT p t => Dict (p (t f a))) -> ForallT p t :- p (t f a))
    -> (ForallT p t => Dict (p (t f a))) -> ForallT p t :- p (t f a)
    forall a b. (a -> b) -> a -> b
    $
      case Forall (Q p t) :- Q p t f
    forall {k} (p :: k -> Constraint) (a :: k). Forall p :- p a
    inst :: Forall (Q p t) :- Q p t f of { Sub Dict (Q p t f)
    Forall (Q p t) => Dict (Q p t f)
    Dict ->
      case Forall (R p t f) :- R p t f a
    forall {k} (p :: k -> Constraint) (a :: k). Forall p :- p a
    inst :: Forall (R p t f) :- R p t f a of
        Sub Dict (R p t f a)
    Forall (R p t f) => Dict (R p t f a)
    Dict -> Dict (p (t f a))
    forall (a :: Constraint). a => Dict a
    Dict }

    type Forall1 p = Forall p
    -- | Instantiate a quantified constraint on kind @* -> *@.
    -- This is now redundant since @'inst'@ became polykinded.
    inst1 :: forall (p :: (* -> *) -> Constraint) (f :: * -> *). Forall p :- p f
    inst1 :: forall (p :: (* -> *) -> Constraint) (f :: * -> *). Forall p :- p f
    inst1 = Forall p :- p f
    forall {k} (p :: k -> Constraint) (a :: k). Forall p :- p a
    inst

    -- | A representation of the quantified constraint
    -- @forall a1 a2 ... an . p a1 a2 ... an@, supporting a variable number of
    -- parameters.
    type family ForallV :: k -> Constraint
    type instance ForallV = ForallV_

    class ForallV' p => ForallV_ (p :: k)
    instance ForallV' p => ForallV_ p

    -- | Instantiate a quantified @'ForallV' p@ constraint as @c@, where
    -- @c ~ p a1 a2 ... an@.
    class InstV (p :: k) c | k c -> p where
      type ForallV' (p :: k) :: Constraint
      instV :: ForallV p :- c

    instance p ~ c => InstV (p :: Constraint) c where
      type ForallV' (p :: Constraint) = p
      instV :: ForallV p :- c
    instV = (ForallV_ c => Dict c) -> ForallV_ c :- c
    forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
    Sub Dict c
    ForallV_ c => Dict c
    forall (a :: Constraint). a => Dict a
    Dict

    -- Treating 1 argument specially rather than recursing as a bit of (premature?)
    -- optimization
    instance p a ~ c => InstV (p :: k -> Constraint) c where
      type ForallV' (p :: k -> Constraint) = Forall p
      instV :: ForallV p :- c
    instV = (ForallV p => Dict c) -> ForallV p :- c
    forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
    Sub ((ForallV p => Dict c) -> ForallV p :- c)
    -> (ForallV p => Dict c) -> ForallV p :- c
    forall a b. (a -> b) -> a -> b
    $ case Forall p :- c
    Forall p :- p a
    forall {k} (p :: k -> Constraint) (a :: k). Forall p :- p a
    inst :: Forall p :- c of
        Sub Dict c
    Forall p => Dict c
    Dict -> Dict c
    forall (a :: Constraint). a => Dict a
    Dict

    instance InstV (p a) c => InstV (p :: k1 -> k2 -> k3) c where
      type ForallV' (p :: k1 -> k2 -> k3) = ForallF ForallV p
      instV :: ForallV p :- c
    instV = (ForallV p => Dict c) -> ForallV p :- c
    forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
    Sub ((ForallV p => Dict c) -> ForallV p :- c)
    -> (ForallV p => Dict c) -> ForallV p :- c
    forall a b. (a -> b) -> a -> b
    $ case ForallF ForallV_ p :- ForallV_ (p a)
    ForallF ForallV p :- ForallV (p a)
    forall {k2} {k1} (p :: k2 -> Constraint) (f :: k1 -> k2) (a :: k1).
    ForallF p f :- p (f a)
    instF :: ForallF ForallV p :- ForallV (p a) of
        Sub Dict (ForallV (p a))
    ForallF ForallV p => Dict (ForallV (p a))
    Dict -> case ForallV (p a) :- c
    forall k (p :: k) (c :: Constraint). InstV p c => ForallV p :- c
    instV :: ForallV (p a) :- c of
          Sub Dict c
    ForallV (p a) => Dict c
    Dict -> Dict c
    forall (a :: Constraint). a => Dict a
    Dict