{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneDeriving #-}
-- | Explicit dictionaries.
--
-- When working with compound constraints such as constructed
-- using 'All' or 'All2', GHC cannot always prove automatically
-- what one would expect to hold.
--
-- This module provides a way of explicitly proving
-- conversions between such constraints to GHC. Such conversions
-- still have to be manually applied.
--
-- This module remains somewhat experimental.
-- It is therefore not exported via the main module and
-- has to be imported explicitly.
--
module Data.SOP.Dict where

import Data.Proxy
import Data.SOP.Classes
import Data.SOP.Constraint
import Data.SOP.NP

-- | An explicit dictionary carrying evidence of a
-- class constraint.
--
-- The constraint parameter is separated into a
-- second argument so that @'Dict' c@ is of the correct
-- kind to be used directly as a parameter to e.g. 'NP'.
--
-- @since 0.2
--
data Dict (c :: k -> Constraint) (a :: k) where
  Dict :: c a => Dict c a

deriving instance Show (Dict c a)

-- | A proof that the trivial constraint holds
-- over all type-level lists.
--
-- @since 0.2
--
pureAll :: SListI xs => Dict (All Top) xs
pureAll :: Dict (All Top) xs
pureAll = NP (Dict Top) xs -> Dict (All Top) xs
forall k (c :: k -> Constraint) (xs :: [k]).
NP (Dict c) xs -> Dict (All c) xs
all_NP ((forall (a :: k). Dict Top a) -> NP (Dict Top) xs
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *).
(HPure h, SListIN h xs) =>
(forall (a :: k). f a) -> h f xs
hpure forall (a :: k). Dict Top a
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict)

-- | A proof that the trivial constraint holds
-- over all type-level lists of lists.
--
-- @since 0.2
--
pureAll2 :: All SListI xss => Dict (All2 Top) xss
pureAll2 :: Dict (All2 Top) xss
pureAll2 = POP (Dict Top) xss -> Dict (All2 Top) xss
forall k (xss :: [[k]]) (c :: k -> Constraint).
SListI xss =>
POP (Dict c) xss -> Dict (All2 c) xss
all_POP ((forall (a :: k). Dict Top a) -> POP (Dict Top) xss
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *).
(HPure h, SListIN h xs) =>
(forall (a :: k). f a) -> h f xs
hpure forall (a :: k). Dict Top a
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict)

-- | Lifts a dictionary conversion over a type-level list.
--
-- @since 0.2
--
mapAll :: forall c d xs .
          (forall a . Dict c a -> Dict d a)
       -> Dict (All c) xs -> Dict (All d) xs
mapAll :: (forall (a :: k). Dict c a -> Dict d a)
-> Dict (All c) xs -> Dict (All d) xs
mapAll forall (a :: k). Dict c a -> Dict d a
f Dict (All c) xs
Dict = (NP (Dict d) xs -> Dict (All d) xs
forall k (c :: k -> Constraint) (xs :: [k]).
NP (Dict c) xs -> Dict (All c) xs
all_NP (NP (Dict d) xs -> Dict (All d) xs)
-> (Dict (All c) xs -> NP (Dict d) xs)
-> Dict (All c) xs
-> Dict (All d) xs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (a :: k). Dict c a -> Dict d a)
-> NP (Dict c) xs -> NP (Dict d) xs
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
       (f' :: k -> *).
(SListIN (Prod h) xs, HAp h) =>
(forall (a :: k). f a -> f' a) -> h f xs -> h f' xs
hmap forall (a :: k). Dict c a -> Dict d a
f (NP (Dict c) xs -> NP (Dict d) xs)
-> (Dict (All c) xs -> NP (Dict c) xs)
-> Dict (All c) xs
-> NP (Dict d) xs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dict (All c) xs -> NP (Dict c) xs
forall k (c :: k -> Constraint) (xs :: [k]).
Dict (All c) xs -> NP (Dict c) xs
unAll_NP) Dict (All c) xs
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict

-- | Lifts a dictionary conversion over a type-level list
-- of lists.
--
-- @since 0.2
--
mapAll2 :: forall c d xss .
           (forall a . Dict c a -> Dict d a)
        -> Dict (All2 c) xss -> Dict (All2 d) xss
mapAll2 :: (forall (a :: k). Dict c a -> Dict d a)
-> Dict (All2 c) xss -> Dict (All2 d) xss
mapAll2 forall (a :: k). Dict c a -> Dict d a
f d :: Dict (All2 c) xss
d@Dict (All2 c) xss
Dict = (Dict (All2 d) xss -> Dict (All2 d) xss
forall k (c :: k -> Constraint) (xss :: [[k]]).
Dict (All (All c)) xss -> Dict (All (All c)) xss
all2 (Dict (All2 d) xss -> Dict (All2 d) xss)
-> (Dict (All2 c) xss -> Dict (All2 d) xss)
-> Dict (All2 c) xss
-> Dict (All2 d) xss
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (a :: [k]). Dict (All c) a -> Dict (All d) a)
-> Dict (All2 c) xss -> Dict (All2 d) xss
forall k (c :: k -> Constraint) (d :: k -> Constraint) (xs :: [k]).
(forall (a :: k). Dict c a -> Dict d a)
-> Dict (All c) xs -> Dict (All d) xs
mapAll ((forall (a :: k). Dict c a -> Dict d a)
-> Dict (All c) a -> Dict (All d) a
forall k (c :: k -> Constraint) (d :: k -> Constraint) (xs :: [k]).
(forall (a :: k). Dict c a -> Dict d a)
-> Dict (All c) xs -> Dict (All d) xs
mapAll forall (a :: k). Dict c a -> Dict d a
f) (Dict (All2 c) xss -> Dict (All2 d) xss)
-> (Dict (All2 c) xss -> Dict (All2 c) xss)
-> Dict (All2 c) xss
-> Dict (All2 d) xss
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dict (All2 c) xss -> Dict (All2 c) xss
forall k (c :: k -> Constraint) (xss :: [[k]]).
Dict (All (All c)) xss -> Dict (All (All c)) xss
unAll2) Dict (All2 c) xss
d

-- | If two constraints 'c' and 'd' hold over a type-level
-- list 'xs', then the combination of both constraints holds
-- over that list.
--
-- @since 0.2
--
zipAll :: Dict (All c) xs -> Dict (All d) xs -> Dict (All (c `And` d)) xs
zipAll :: Dict (All c) xs -> Dict (All d) xs -> Dict (All (And c d)) xs
zipAll dc :: Dict (All c) xs
dc@Dict (All c) xs
Dict Dict (All d) xs
dd = NP (Dict (And c d)) xs -> Dict (All (And c d)) xs
forall k (c :: k -> Constraint) (xs :: [k]).
NP (Dict c) xs -> Dict (All c) xs
all_NP ((forall (a :: k). Dict c a -> Dict d a -> Dict (And c d) a)
-> Prod NP (Dict c) xs -> NP (Dict d) xs -> NP (Dict (And c d)) xs
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
       (f' :: k -> *) (f'' :: k -> *).
(SListIN (Prod h) xs, HAp h, HAp (Prod h)) =>
(forall (a :: k). f a -> f' a -> f'' a)
-> Prod h f xs -> h f' xs -> h f'' xs
hzipWith (\ Dict c a
Dict Dict d a
Dict -> Dict (And c d) a
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict) (Dict (All c) xs -> NP (Dict c) xs
forall k (c :: k -> Constraint) (xs :: [k]).
Dict (All c) xs -> NP (Dict c) xs
unAll_NP Dict (All c) xs
dc) (Dict (All d) xs -> NP (Dict d) xs
forall k (c :: k -> Constraint) (xs :: [k]).
Dict (All c) xs -> NP (Dict c) xs
unAll_NP Dict (All d) xs
dd))

-- | If two constraints 'c' and 'd' hold over a type-level
-- list of lists 'xss', then the combination of both constraints
-- holds over that list of lists.
--
-- @since 0.2
--
zipAll2 :: All SListI xss => Dict (All2 c) xss -> Dict (All2 d) xss -> Dict (All2 (c `And` d)) xss
zipAll2 :: Dict (All2 c) xss -> Dict (All2 d) xss -> Dict (All2 (And c d)) xss
zipAll2 Dict (All2 c) xss
dc Dict (All2 d) xss
dd = POP (Dict (And c d)) xss -> Dict (All2 (And c d)) xss
forall k (xss :: [[k]]) (c :: k -> Constraint).
SListI xss =>
POP (Dict c) xss -> Dict (All2 c) xss
all_POP ((forall (a :: k). Dict c a -> Dict d a -> Dict (And c d) a)
-> Prod POP (Dict c) xss
-> POP (Dict d) xss
-> POP (Dict (And c d)) xss
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
       (f' :: k -> *) (f'' :: k -> *).
(SListIN (Prod h) xs, HAp h, HAp (Prod h)) =>
(forall (a :: k). f a -> f' a -> f'' a)
-> Prod h f xs -> h f' xs -> h f'' xs
hzipWith (\ Dict c a
Dict Dict d a
Dict -> Dict (And c d) a
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict) (Dict (All2 c) xss -> POP (Dict c) xss
forall k (c :: k -> Constraint) (xss :: [[k]]).
Dict (All2 c) xss -> POP (Dict c) xss
unAll_POP Dict (All2 c) xss
dc) (Dict (All2 d) xss -> POP (Dict d) xss
forall k (c :: k -> Constraint) (xss :: [[k]]).
Dict (All2 c) xss -> POP (Dict c) xss
unAll_POP Dict (All2 d) xss
dd))
-- TODO: I currently don't understand why the All constraint in the beginning
-- cannot be inferred.

-- | If we have a constraint 'c' that holds over a type-level
-- list 'xs', we can create a product containing proofs that
-- each individual list element satisfies 'c'.
--
-- @since 0.2
--
unAll_NP :: forall c xs . Dict (All c) xs -> NP (Dict c) xs
unAll_NP :: Dict (All c) xs -> NP (Dict c) xs
unAll_NP Dict (All c) xs
d = Dict (All c) xs -> (All c xs => NP (Dict c) xs) -> NP (Dict c) xs
forall k (c :: k -> Constraint) (a :: k) r.
Dict c a -> (c a => r) -> r
withDict Dict (All c) xs
d All c xs => NP (Dict c) xs
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l).
(AllN h c xs, HPure h) =>
h (Dict c) xs
hdicts

-- | If we have a constraint 'c' that holds over a type-level
-- list of lists 'xss', we can create a product of products
-- containing proofs that all the inner elements satisfy 'c'.
--
-- @since 0.2
--
unAll_POP :: forall c xss . Dict (All2 c) xss -> POP (Dict c) xss
unAll_POP :: Dict (All2 c) xss -> POP (Dict c) xss
unAll_POP Dict (All2 c) xss
d = Dict (All2 c) xss
-> (All2 c xss => POP (Dict c) xss) -> POP (Dict c) xss
forall k (c :: k -> Constraint) (a :: k) r.
Dict c a -> (c a => r) -> r
withDict Dict (All2 c) xss
d All2 c xss => POP (Dict c) xss
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l).
(AllN h c xs, HPure h) =>
h (Dict c) xs
hdicts

-- | If we have a product containing proofs that each element
-- of 'xs' satisfies 'c', then @'All' c@ holds for 'xs'.
--
-- @since 0.2
--
all_NP :: NP (Dict c) xs -> Dict (All c) xs
all_NP :: NP (Dict c) xs -> Dict (All c) xs
all_NP NP (Dict c) xs
Nil          = Dict (All c) xs
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
all_NP (Dict c x
Dict :* NP (Dict c) xs
ds) = Dict (All c) xs -> (All c xs => Dict (All c) xs) -> Dict (All c) xs
forall k (c :: k -> Constraint) (a :: k) r.
Dict c a -> (c a => r) -> r
withDict (NP (Dict c) xs -> Dict (All c) xs
forall k (c :: k -> Constraint) (xs :: [k]).
NP (Dict c) xs -> Dict (All c) xs
all_NP NP (Dict c) xs
ds) All c xs => Dict (All c) xs
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict

-- | If we have a product of products containing proofs that
-- each inner element of 'xss' satisfies 'c', then @'All2' c@
-- holds for 'xss'.
--
-- @since 0.2
--
all_POP :: SListI xss => POP (Dict c) xss -> Dict (All2 c) xss
all_POP :: POP (Dict c) xss -> Dict (All2 c) xss
all_POP = Dict (All2 c) xss -> Dict (All2 c) xss
forall k (c :: k -> Constraint) (xss :: [[k]]).
Dict (All (All c)) xss -> Dict (All (All c)) xss
all2 (Dict (All2 c) xss -> Dict (All2 c) xss)
-> (POP (Dict c) xss -> Dict (All2 c) xss)
-> POP (Dict c) xss
-> Dict (All2 c) xss
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NP (Dict (All c)) xss -> Dict (All2 c) xss
forall k (c :: k -> Constraint) (xs :: [k]).
NP (Dict c) xs -> Dict (All c) xs
all_NP (NP (Dict (All c)) xss -> Dict (All2 c) xss)
-> (POP (Dict c) xss -> NP (Dict (All c)) xss)
-> POP (Dict c) xss
-> Dict (All2 c) xss
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (a :: [k]). NP (Dict c) a -> Dict (All c) a)
-> NP (NP (Dict c)) xss -> NP (Dict (All c)) xss
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
       (f' :: k -> *).
(SListIN (Prod h) xs, HAp h) =>
(forall (a :: k). f a -> f' a) -> h f xs -> h f' xs
hmap forall (a :: [k]). NP (Dict c) a -> Dict (All c) a
forall k (c :: k -> Constraint) (xs :: [k]).
NP (Dict c) xs -> Dict (All c) xs
all_NP (NP (NP (Dict c)) xss -> NP (Dict (All c)) xss)
-> (POP (Dict c) xss -> NP (NP (Dict c)) xss)
-> POP (Dict c) xss
-> NP (Dict (All c)) xss
forall b c a. (b -> c) -> (a -> b) -> a -> c
. POP (Dict c) xss -> NP (NP (Dict c)) xss
forall k (f :: k -> *) (xss :: [[k]]). POP f xss -> NP (NP f) xss
unPOP
-- TODO: Is the constraint necessary?

-- | The constraint @'All2' c@ is convertible to @'All' ('All' c)@.
--
-- @since 0.2
--
unAll2 :: Dict (All2 c) xss -> Dict (All (All c)) xss
unAll2 :: Dict (All2 c) xss -> Dict (All2 c) xss
unAll2 = Dict (All2 c) xss -> Dict (All2 c) xss
forall a. a -> a
id
{-# DEPRECATED unAll2 "'All2 c' is now a synonym of 'All (All c)'" #-}

-- | The constraint @'All' ('All' c)@ is convertible to @'All2' c@.
--
-- @since 0.2
--
all2 :: Dict (All (All c)) xss -> Dict (All2 c) xss
all2 :: Dict (All (All c)) xss -> Dict (All (All c)) xss
all2 = Dict (All (All c)) xss -> Dict (All (All c)) xss
forall a. a -> a
id
{-# DEPRECATED all2 "'All2 c' is now a synonym of 'All (All c)'" #-}

-- | If we have an explicit dictionary, we can unwrap it and
-- pass a function that makes use of it.
--
-- @since 0.2
--
withDict :: Dict c a -> (c a => r) -> r
withDict :: Dict c a -> (c a => r) -> r
withDict Dict c a
Dict c a => r
x = r
c a => r
x

-- | A structure of dictionaries.
--
-- @since 0.2.3.0
--
hdicts :: forall h c xs . (AllN h c xs, HPure h) => h (Dict c) xs
hdicts :: h (Dict c) xs
hdicts = Proxy c -> (forall (a :: k). c a => Dict c a) -> h (Dict c) xs
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *).
(HPure h, AllN h c xs) =>
proxy c -> (forall (a :: k). c a => f a) -> h f xs
hcpure (Proxy c
forall k (t :: k). Proxy t
Proxy :: Proxy c) forall (a :: k). c a => Dict c a
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict