{-# 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 Any) -> Dict1 p
forall a b. a -> b
unsafeCoerce Dict (p Any)
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