{-# 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 :: forall {k} (xs :: [k]). SListI xs => Dict (All Top) xs
pureAll = forall {k} (c :: k -> Constraint) (xs :: [k]).
NP (Dict c) xs -> Dict (All c) xs
all_NP (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 {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 :: forall {k} (xss :: [[k]]). All SListI xss => Dict (All2 Top) xss
pureAll2 = forall {k} (xss :: [[k]]) (c :: k -> Constraint).
SListI xss =>
POP (Dict c) xss -> Dict (All2 c) xss
all_POP (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 {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 {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 (All c) xs
Dict = (forall {k} (c :: k -> Constraint) (xs :: [k]).
NP (Dict c) xs -> Dict (All c) xs
all_NP forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (c :: k -> Constraint) (xs :: [k]).
Dict (All c) xs -> NP (Dict c) xs
unAll_NP) 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 {k} (c :: k -> Constraint) (d :: k -> Constraint)
       (xss :: [[k]]).
(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 = (forall {k} (c :: k -> Constraint) (xss :: [[k]]).
Dict (All (All c)) xss -> Dict (All (All c)) xss
all2 forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 {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) forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 :: forall {k} (c :: k -> Constraint) (xs :: [k])
       (d :: k -> Constraint).
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 = forall {k} (c :: k -> Constraint) (xs :: [k]).
NP (Dict c) xs -> Dict (All c) xs
all_NP (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 -> forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict) (forall {k} (c :: k -> Constraint) (xs :: [k]).
Dict (All c) xs -> NP (Dict c) xs
unAll_NP Dict (All c) xs
dc) (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 :: forall {k} (xss :: [[k]]) (c :: k -> Constraint)
       (d :: k -> Constraint).
All SListI xss =>
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 = forall {k} (xss :: [[k]]) (c :: k -> Constraint).
SListI xss =>
POP (Dict c) xss -> Dict (All2 c) xss
all_POP (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 -> forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict) (forall {k} (c :: k -> Constraint) (xss :: [[k]]).
Dict (All2 c) xss -> POP (Dict c) xss
unAll_POP Dict (All2 c) xss
dc) (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 :: forall {k} (c :: k -> Constraint) (xs :: [k]).
Dict (All c) xs -> NP (Dict c) xs
unAll_NP Dict (All c) xs
d = forall {k} (c :: k -> Constraint) (a :: k) r.
Dict c a -> (c a => r) -> r
withDict Dict (All c) xs
d 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 :: forall {k} (c :: k -> Constraint) (xss :: [[k]]).
Dict (All2 c) xss -> POP (Dict c) xss
unAll_POP Dict (All2 c) xss
d = forall {k} (c :: k -> Constraint) (a :: k) r.
Dict c a -> (c a => r) -> r
withDict Dict (All2 c) xss
d 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 :: forall {k} (c :: k -> Constraint) (xs :: [k]).
NP (Dict c) xs -> Dict (All c) xs
all_NP NP (Dict c) xs
Nil          = forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
all_NP (Dict c x
Dict :* NP (Dict c) xs
ds) = forall {k} (c :: k -> Constraint) (a :: k) r.
Dict c a -> (c a => r) -> r
withDict (forall {k} (c :: k -> Constraint) (xs :: [k]).
NP (Dict c) xs -> Dict (All c) xs
all_NP NP (Dict c) xs
ds) 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 :: forall {k} (xss :: [[k]]) (c :: k -> Constraint).
SListI xss =>
POP (Dict c) xss -> Dict (All2 c) xss
all_POP = forall {k} (c :: k -> Constraint) (xss :: [[k]]).
Dict (All (All c)) xss -> Dict (All (All c)) xss
all2 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (c :: k -> Constraint) (xs :: [k]).
NP (Dict c) xs -> Dict (All c) xs
all_NP forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 {k} (c :: k -> Constraint) (xs :: [k]).
NP (Dict c) xs -> Dict (All c) xs
all_NP forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 :: forall {k} (c :: k -> Constraint) (xss :: [[k]]).
Dict (All (All c)) xss -> Dict (All (All c)) xss
unAll2 = 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 :: forall {k} (c :: k -> Constraint) (xss :: [[k]]).
Dict (All (All c)) xss -> Dict (All (All c)) xss
all2 = 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 :: forall {k} (c :: k -> Constraint) (a :: k) r.
Dict c a -> (c a => r) -> r
withDict Dict c a
Dict c a => r
x = 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 :: forall {k} {l} (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l).
(AllN h c xs, HPure h) =>
h (Dict c) xs
hdicts = 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 (forall {k} (t :: k). Proxy t
Proxy :: Proxy c) forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict