    {-# 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 = 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 (xs :: [k]) (f :: k -> *).
    SListIN NP xs =>
    (forall (a :: k). f a) -> NP f 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 Dict Top a
    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 :: forall {k} (xss :: [[k]]). All SListI xss => 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 (xs :: [[k]]) (f :: k -> *).
    SListIN POP xs =>
    (forall (a :: k). f a) -> POP f 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 Dict Top a
    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 {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 = (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 Dict c a -> Dict d a
    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 {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 = (Dict (All (All d)) xss -> Dict (All (All d)) xss
    forall {k} (c :: k -> Constraint) (xss :: [[k]]).
    Dict (All (All c)) xss -> Dict (All (All c)) xss
    all2 (Dict (All (All d)) xss -> Dict (All (All d)) xss)
    -> (Dict (All2 c) xss -> Dict (All (All d)) xss)
    -> Dict (All2 c) xss
    -> Dict (All (All 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 (All (All 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 Dict c a -> Dict d a
    forall (a :: k). Dict c a -> Dict d a
    f) (Dict (All2 c) xss -> Dict (All (All d)) xss)
    -> (Dict (All2 c) xss -> Dict (All2 c) xss)
    -> Dict (All2 c) xss
    -> Dict (All (All 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 :: 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 = 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 :: 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 = 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 :: forall {k} (c :: k -> Constraint) (xs :: [k]).
    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 NP (Dict c) xs
    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 :: forall {k} (c :: k -> Constraint) (xss :: [[k]]).
    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 POP (Dict c) xss
    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 :: forall {k} (c :: k -> Constraint) (xs :: [k]).
    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) Dict (All c) xs
    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 :: forall {k} (xss :: [[k]]) (c :: k -> Constraint).
    SListI xss =>
    POP (Dict c) xss -> Dict (All2 c) xss
    all_POP = Dict (All (All c)) xss -> Dict (All (All c)) xss
    forall {k} (c :: k -> Constraint) (xss :: [[k]]).
    Dict (All (All c)) xss -> Dict (All (All c)) xss
    all2 (Dict (All (All c)) xss -> Dict (All (All c)) xss)
    -> (POP (Dict c) xss -> Dict (All (All c)) xss)
    -> POP (Dict c) xss
    -> Dict (All (All c)) xss
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NP (Dict (All c)) xss -> Dict (All (All 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 (All (All c)) xss)
    -> (POP (Dict c) xss -> NP (Dict (All c)) xss)
    -> POP (Dict c) xss
    -> Dict (All (All 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 NP (Dict c) a -> Dict (All c) a
    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 :: forall {k} (c :: k -> Constraint) (xss :: [[k]]).
    Dict (All (All c)) xss -> Dict (All (All 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 :: forall {k} (c :: k -> Constraint) (xss :: [[k]]).
    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 :: forall {k} (c :: k -> Constraint) (a :: k) r.
    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 :: forall {k} {l} (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
           (xs :: l).
    (AllN h c xs, HPure h) =>
    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
    forall (c :: k -> Constraint) (xs :: l)
           (proxy :: (k -> Constraint) -> *) (f :: k -> *).
    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) Dict c a
    forall (a :: k). c a => Dict c a
    forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
    Dict