{-# 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