content: {-# 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 = all_NP (hpure 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 = all_POP (hpure 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 f Dict = (all_NP . hmap f . unAll_NP) 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 f d@Dict = (all2 . mapAll (mapAll f) . unAll2) 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 dc@Dict dd = all_NP (hzipWith (\ Dict Dict -> Dict) (unAll_NP dc) (unAll_NP 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 dc dd = all_POP (hzipWith (\ Dict Dict -> Dict) (unAll_POP dc) (unAll_POP 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 d = withDict d 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 d = withDict d 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 Nil          = Dict
  all_NP (Dict :* ds) = withDict (all_NP ds) 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 = all2 . all_NP . hmap all_NP . 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 = 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 = 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 x = 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 = hcpure (Proxy :: Proxy c) Dict
  