{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}

module Data.Constraint.Extras where

import Data.Constraint
import Data.Constraint.Compose
import Data.Constraint.Flip
import Data.Constraint.Forall

-- | Morally, this class is for GADTs whose indices can be finitely enumerated. It provides operations which will
-- select the appropriate type class dictionary from among a list of contenders based on a value of the type.
-- There are a few different variations of this which we'd like to be able to support, and they're all implemented
-- in the same fashion at the term level, by pattern matching on the constructors of the GADT, and producing Dict
-- as the result.
-- It would be nice to have some way to stop the proliferation of these variants and unify the existing ones, but
-- at the moment, it appears to require honest type level functions. (Closed type families which must be fully
-- applied didn't quite cut it when I tried). Some symbolic type-level application could do the trick, but I didn't
-- want to go quite that far at the time of writing.

class ArgDict (c :: k -> Constraint) (f :: k -> *) where
  type ConstraintsFor f (c :: k -> Constraint) :: Constraint
  argDict :: ConstraintsFor f c => f a -> Dict (c a)

type ConstraintsFor' f (c :: k -> Constraint) (g :: k' -> k) = ConstraintsFor f (ComposeC c g)

argDict' :: forall f c g a. (Has' c f g) => f a -> Dict (c (g a))
argDict' :: f a -> Dict (c (g a))
argDict' tag :: f a
tag = case f a -> Dict (ComposeC c g a)
forall k (c :: k -> Constraint) (f :: k -> *) (a :: k).
(ArgDict c f, ConstraintsFor f c) =>
f a -> Dict (c a)
argDict f a
tag of
  (Dict (ComposeC c g a)
Dict :: Dict (ComposeC c g a)) -> Dict (c (g a))
forall (a :: Constraint). a => Dict a
Dict

type ConstraintsForV (f :: (k -> k') -> *) (c :: k' -> Constraint) (g :: k) = ConstraintsFor f (FlipC (ComposeC c) g)

argDictV :: forall f c g v. (HasV c f g) => f v -> Dict (c (v g))
argDictV :: f v -> Dict (c (v g))
argDictV tag :: f v
tag = case f v -> Dict (FlipC (ComposeC c) g v)
forall k (c :: k -> Constraint) (f :: k -> *) (a :: k).
(ArgDict c f, ConstraintsFor f c) =>
f a -> Dict (c a)
argDict f v
tag of
  (Dict (FlipC (ComposeC c) g v)
Dict :: Dict (FlipC (ComposeC c) g a)) -> Dict (c (v g))
forall (a :: Constraint). a => Dict a
Dict

{-# DEPRECATED ArgDictV "Just use 'ArgDict'" #-}
type ArgDictV f c = ArgDict f c

type Has (c :: k -> Constraint) f = (ArgDict c f, ConstraintsFor f c)
type Has' (c :: k -> Constraint) f (g :: k' -> k) = (ArgDict (ComposeC c g) f, ConstraintsFor' f c g)
type HasV c f g = (ArgDict (FlipC (ComposeC c) g) f, ConstraintsForV f c g)

has :: forall c f a r. (Has c f) => f a -> (c a => r) -> r
has :: f a -> (c a => r) -> r
has k :: f a
k r :: c a => r
r | (Dict (c a)
Dict :: Dict (c a)) <- f a -> Dict (c a)
forall k (c :: k -> Constraint) (f :: k -> *) (a :: k).
(ArgDict c f, ConstraintsFor f c) =>
f a -> Dict (c a)
argDict f a
k = r
c a => r
r

has' :: forall c g f a r. (Has' c f g) => f a -> (c (g a) => r) -> r
has' :: f a -> (c (g a) => r) -> r
has' k :: f a
k r :: c (g a) => r
r | (Dict (c (g a))
Dict :: Dict (c (g a))) <- f a -> Dict (c (g a))
forall k' k (f :: k' -> *) (c :: k -> Constraint) (g :: k' -> k)
       (a :: k').
Has' c f g =>
f a -> Dict (c (g a))
argDict' f a
k = r
c (g a) => r
r

hasV :: forall c g f v r. (HasV c f g) => f v -> (c (v g) => r) -> r
hasV :: f v -> (c (v g) => r) -> r
hasV k :: f v
k r :: c (v g) => r
r | (Dict (c (v g))
Dict :: Dict (c (v g))) <- f v -> Dict (c (v g))
forall k k' (f :: (k -> k') -> *) (c :: k' -> Constraint) (g :: k)
       (v :: k -> k').
HasV c f g =>
f v -> Dict (c (v g))
argDictV f v
k = r
c (v g) => r
r

whichever :: forall c t a r. (ForallF c t) => (c (t a) => r) -> r
whichever :: (c (t a) => r) -> r
whichever r :: c (t a) => r
r = c (t a) => r
r (c (t a) => r) -> (ForallF c t :- c (t a)) -> r
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ (ForallF c t :- c (t a)
forall k2 k1 (p :: k2 -> Constraint) (f :: k1 -> k2) (a :: k1).
ForallF p f :- p (f a)
instF :: ForallF c t :- c (t a))

-- | Allows explicit specification of constraint implication
class Implies1 c d where
  implies1 :: c a :- d a