Dredge.hs

{-# LANGUAGE CPP #-}
#if (__GLASGOW_HASKELL__ < 709)
-- TryCollectionList needs overlap
{-# LANGUAGE OverlappingInstances #-}
{-# OPTIONS_GHC -fno-warn-unrecognised-pragmas #-}
#endif
{- | Description: access nested records/variants given only the last label along a path -}
module Data.HList.Dredge where

import Data.HList.Record
import Data.HList.Variant
import Data.HList.HList
import Data.HList.TIP
import Data.HList.TIC
import Data.HList.FakePrelude
import Data.HList.Labelable
import LensDefs (isSimple)
import Data.HList.TypeEqO () -- if this is missing, dredge fails


#if (__GLASGOW_HASKELL__ == 800)
-- https://ghc.haskell.org/trac/ghc/ticket/13371
toLabelx x = toLabelSym x
#else
toLabelx x = toLabel x
#endif

{- |

Using HListPP syntax for short hand, @dredge `foo@ expands out to
something like @`path . `to . `foo@, with the restriction that
there is only one possible @`path .  `to@ which leads to the
label @foo@.

For example, if we have the following definitions,

> type BVal a = Record '[Tagged "x" a, Tagged "a" Char]
> type R a = Record  [Tagged "a" Int, Tagged "b" (BVal a)]
> type V a = Variant [Tagged "a" Int, Tagged "b" (BVal a)]
> lx = Label :: Label "x"

Then we have:

> dredge `x :: Lens (R a) (R b) a b
> dredge lx :: Lens (R a) (R b) a b

> dredge `x :: Traversal (V a) (V b) a b -- there were only variants along the path we'd get a Prism
> dredge lx :: Traversal (V a) (V b) a b

[@result-type directed operations are supported@]

There are two ways to access a field with tag @a@ in the R type
defined above, but they result in fields with different types
being looked up:

> `a        :: Lens' (R a) Char
> `b . `a   :: Lens' (R a) Int

so provided that the result type is disambiguated by the context,
the following two types can happen

> dredge `a :: Lens' (R a) Char
> dredge `a :: Lens' (R a) Int


[@TIP & TIC@]

type indexed collections are allowed along those paths, but
as explained in the 'Labelable' instances, only simple optics
(Lens' / Prism' / Traversal' ) are produced. @dredgeTI'@
works better if the target is a TIP or TIC

-}
dredge label = getSAfromOutputOptic $ \ pr pa ->
      hLens'Path (labelPathEndingWithTD pr (toLabelx label) pa)



getSAfromOutputOptic :: (p a fb -> p rs rft) ~ stab
                => (Proxy (rs :: *) -> Proxy (a :: *) -> stab) -> stab
getSAfromOutputOptic f = f Proxy Proxy


-- | 'dredge' except a simple (s ~ t, a ~ b) optic is produced
dredge' label = isSimple (dredge label)


-- | dredgeND (named directed only) is the same as 'dredge', except the
-- result type (@a@) is not used when the label would otherwise
-- be ambiguous. dredgeND might give better type errors, but otherwise
-- there should be no reason to pick it over dredge
dredgeND label = getSAfromOutputOptic $ \ pr _a ->
      hLens'Path (labelPathEndingWith pr (toLabelx label))


-- | 'dredgeND' except a simple (s ~ t, a ~ b) optic is produced
dredgeND' label = isSimple (dredgeND label)


{- | The same as dredgeND', except intended for TIP/TICs because
the assumption is made that @l ~ v@ for the @Tagged l v@ elements.
In other words, ticPrism' and 'tipyLens'' could usually
be replaced by

> dredgeTI' :: _ => Label a -> Lens'  (TIP s) a
> dredgeTI' :: _ => Label a -> Prism' (TIC s) a

where we might have @s ~ '[Tagged a a, Tagged b b]@

-}
dredgeTI' label = isSimple lens where
        lens = getSAfromOutputOptic $ \ pr pa ->
            hLens'Path (labelPathEndingWith pr (pa `proxyTypeOf` label))

        proxyTypeOf :: p a -> q a -> Label a
        proxyTypeOf _ _ = Label


-- | @HSingleton msg xs x@ is like @'[x] ~ xs@ if that constraint can hold,
-- otherwise it is @Fail msg@. See comments on 'Fail' about how its kind
-- varies with ghc version.
class HSingleton (msgAmb :: m) (msgEmpty :: m2) (ns :: [k]) (p :: k) | ns -> p
instance HSingleton m1 m2 '[n] n
instance (Fail m2, Any ~ a) => HSingleton m1 m2 '[] a
instance (Fail m1, Any ~ a) => HSingleton m1 m2 (n1 ': n2 ': n3) a


-- | @HGuardNonNull msg xs@ is like @when (null xs) (fail msg)@
class HGuardNonNull emptymsg (xs :: [k])

instance Fail msg => HGuardNonNull msg '[]
instance             HGuardNonNull msg (x ': xs)


-- | @ConsTrue b x xs r@ is like @r = if b then x:xs else xs@
class ConsTrue (b :: Bool) (x :: k) (xs :: [k]) (r :: [k]) | b x xs -> r, r b -> xs, x xs r -> b
instance ConsTrue True x xs (x ': xs)
instance ConsTrue False x xs xs

-- | @FilterLastEq x xs ys ys'@ determines ys' such that it
-- contains all of the @ys !! i@ such that @last (xs !! i) == x@.
-- In other words it is like
--
-- > ys' = [ y |  (xsElt, y) <- zip xs ys, last xsElt == x ]
class FilterLastEq (x :: k) (xs :: [[k]]) (ys :: [m]) (ys' :: [m]) | x xs ys -> ys'
instance (HReverse path (y' ': rest), HEq y y' b, ConsTrue b z r1 r,
          FilterLastEq y xs zs r1) => FilterLastEq y (path ': xs) (z ': zs) r

instance FilterLastEq y '[] '[] '[]

-- | The same as 'FilterLastEq' except @id@ is used instead of @last@
class FilterVEq (v :: *) (vs :: [*]) (ns :: [k]) (ns' :: [k]) | v vs ns -> ns'

instance FilterVEq v '[] '[] '[]

instance
   (HEq v v' b,
    ConsTrue b n ns1 ns2,
    FilterVEq v vs ns ns1)
    => FilterVEq v (v' ': vs) (n ': ns) ns2

-- | like @FilterVEq@, except if there is
class FilterVEq1 (v :: *) (vs :: [*]) (ns :: [k]) (ns' :: [k]) | v vs ns -> ns'
instance (v ~ v') => FilterVEq1 v '[ v' ] ns ns
instance FilterVEq1 v '[] '[] '[]
instance FilterVEq v (a ': b ': c)  ns ns' => FilterVEq1 v (a ': b ': c) ns ns'

-- | @LabelPathEndingWith r l path@
--
-- determines a unique path suitable for 'hLookupByLabelPath'
-- (calling 'Fail' otherwise) through the
-- nested records/variants in r ending with l
class LabelPathEndingWith (r :: *) (l :: k) (path :: [*]) | r l -> path where
    labelPathEndingWith :: proxy r -> Label l -> Label path
    labelPathEndingWith _ _ = Label

instance
   (FieldTree r ns,
    FilterLastEq (Label l) ns ns ns',
    HSingleton (NonUnique' r l) (NamesDontMatch r ns l) ns' path)
    => LabelPathEndingWith r l path


labelPathEndingWithTD :: forall r l v path
                                vs vs1 ns ns1 ns2.
   (SameLength ns vs,
    SameLength ns1 vs1,
    FieldTree r ns,
    FieldTreeVal r vs,
    FilterLastEq (Label l) ns ns ns1,
    FilterLastEq (Label l) ns vs vs1,
    FilterVEq1 v vs1 ns1 ns2,

    HGuardNonNull (NamesDontMatch r ns l) ns1,

    -- '[path] ~ ns2, plus error reporting if ns2 has >1 or 0 elements
    HSingleton (NonUnique r v l) (TypesDontMatch r ns1 vs1 v) ns2 path)
    => Proxy r -> Label l -> Proxy v -> Label path
labelPathEndingWithTD _ _ _ = Label


type NamesDontMatch r ns l = ErrShowType r
  :$$: ErrText "has paths"  :<>: ErrShowType ns
  :$$: ErrText "but none which end in the desired label" :<>: ErrShowType l

type NonUnique' r l = ErrText "Path ending in label " :<>: ErrShowType l
  :$$: ErrText "is not unique in " :<>: ErrShowType r

type NonUnique r v l = NonUnique' r l
  :$$: ErrText "also considering the v type " :<>: ErrShowType v

{- | XXX

> let x = 'x'; y = [pun| x |]; z = [pun| y |]
> z & dredge (Label :: Label "x") %~ (succ :: Int -> Int)

Should reference this type error, but for whatever reason it doesn't

-}
type TypesDontMatch r ns1 vs1 v = ErrShowType r
  :$$: ErrText "has potential paths with the right labels" :<>: ErrShowType ns1
  :$$: ErrText "which point at types" :<>: ErrShowType vs1 :<>: ErrText "respectively"
  :$$: ErrText "but none of these match the desired type" :<>: ErrShowType v

-- | see 'hLookupByLabelPath'
hLookupByLabelDredge l r = labelPathEndingWith (toProxy r) l `hLookupByLabelPath` r
  where toProxy :: r x -> Proxy x
        toProxy _ = Proxy

{- | lookup along a path

>>> let v = mkVariant1 Label (mkVariant1 Label 'r') :: Variant '[Tagged "x" (Variant '[Tagged "y" Char])]
>>> let r = hBuild (hBuild 'r') :: Record '[Tagged "x" (Record '[Tagged "y" Char])]
>>> let p = Label :: Label [Label "x", Label "y"]
>>> let lx = Label :: Label "y"

>>> hLookupByLabelPath p v
Just 'r'

>>> hLookupByLabelPath p r
'r'

>>> hLookupByLabelDredge lx v
Just 'r'

>>> hLookupByLabelDredge lx r
'r'

-}
hLookupByLabelPath :: HasFieldPath False ls r v => Label ls -> r -> v
hLookupByLabelPath labels r = hLookupByLabelPath1 hFalse labels r

{- |

> hLens'Path labc == hLens' la . hLens' lb . hLens' lc
>  where
>       la :: Label "a"
>       lb :: Label "b"
>       lc :: Label "c"
>       labc :: Label '["a", "b", "c"]

-}
class LabelablePath (xs :: [*]) apb spt | spt xs -> apb where
    hLens'Path :: Label xs -> apb -> spt

instance (Labelable x r s t a b,
          j ~ (a `p` f b),
          k ~ (r s `p` f (r t)),
          ty ~ LabelableTy r,
          LabeledOpticP ty p,
          LabeledOpticF ty f,
          LabeledOpticTo ty x (->),
          LabelablePath xs i j) => LabelablePath (Label x ': xs) i k where
    hLens'Path _ = (hLens' (Label :: Label x) :: j -> k) . hLens'Path (Label :: Label xs)

instance (x ~ x') => LabelablePath '[] x x' where
    hLens'Path _ = id

class HasFieldPath (needJust :: Bool) (ls :: [*]) r v | needJust ls r -> v where
    -- | use 'hLookupByLabelPath' instead
    hLookupByLabelPath1 :: Proxy needJust -> Label ls -> r -> v

instance HasFieldPath False '[] v v where
    hLookupByLabelPath1 _ _ = id

instance HasFieldPath True '[] v (Maybe v) where
    hLookupByLabelPath1 _ _ = Just

instance (HasField l (Record r) u, HasFieldPath needJust ls u v)
    => HasFieldPath needJust (Label l ': ls) (Record r) v where
     hLookupByLabelPath1 needJust _ = hLookupByLabelPath1 needJust (Label :: Label ls)
                                . hLookupByLabel (Label :: Label l)

instance (HasField l (Variant r) (Maybe u), HasFieldPath True ls u (Maybe v))
    => HasFieldPath needJust (Label l ': ls) (Variant r) (Maybe v) where
     hLookupByLabelPath1 _ _ v = hLookupByLabelPath1 hTrue (Label :: Label ls) =<< hLookupByLabel (Label :: Label l) v





{- | @(FieldTree r ns, FieldTreeVal r vs)@

defines ns and vs such that looking up path (ns !! i) in r gives the type
(vs !! i). This is almost @HasFieldPath False (ns !! i) (vs !! i)@, except
there is no additional Maybe when a Variant is encountered along the path
(and we don't have a type level @!!@)
-}
class FieldTreeVal (r :: *) (v :: [*]) | r -> v

class MapFieldTreeVal (r :: *) (ns :: Maybe [*]) (vs :: [*]) | r ns -> vs

instance (TryCollectionList r ns, MapFieldTreeVal r ns v) => FieldTreeVal r v

instance MapFieldTreeVal r Nothing '[]

instance ( MapFieldTreeVal r (Just xs) out2,
           FieldTreeVal v out1,
           (v ': HAppendListR out1 out2) ~ out)
  => MapFieldTreeVal r (Just (Tagged n v ': xs))  out

instance MapFieldTreeVal r (Just '[]) '[]

{- | list all paths through nested records or variants.
An example instance would be

> FieldTree r v

where

> v ~ [[ Label "x",  Label Dat ], '[Label "y"], '[Label "x"] ]
> r ~ Record [ Tagged "x" x, Tagged "y" String ]
>
> x ~ Variant '[ Tagged Dat Char ]

-}
class FieldTree (r :: *) (v :: [[*]]) | r -> v

-- | the only instance
instance (TryCollectionList r ns, MapFieldTree ns vs) => FieldTree r vs


#if (__GLASGOW_HASKELL__ >= 800)
-- possibly https://ghc.haskell.org/trac/ghc/ticket/13284
-- dredge' x = (isSimple . dredge) x
--     • Overlapping instances for TryCollectionList r0 ns0
--         arising from a use of ‘dredge’
--       Matching instances:
--         instance [overlappable] nothing ~ 'Nothing =>
--                                 TryCollectionList x nothing
--           -- Defined at /home/aavogt/wip/HList/HList/Data/HList/Dredge.hs:340:31
--         ...plus four instances involving out-of-scope types
--         (use -fprint-potential-instances to see them all)
--       (The choice depends on the instantiation of ‘r0, ns0’
--        To pick the first instance above, use IncoherentInstances
--        when compiling the other instance declarations)
--
-- attempt to resolve that with a closed type family

type family TryCollectionListTF (r :: *) :: Maybe [*] where
  TryCollectionListTF (Record r) = Just r
  TryCollectionListTF (Variant r) = Just r
  TryCollectionListTF (TIC r) = Just r
  TryCollectionListTF (TIP r) = Just r
  TryCollectionListTF nothing = Nothing

type TryCollectionList r v = (v ~ TryCollectionListTF r)

#else
-- | try to extract the list applied to the Record or Variant
class TryCollectionList (r :: *) (v :: Maybe [*]) | r -> v

instance {-# OVERLAPPABLE #-} (nothing ~ Nothing) => TryCollectionList x nothing
instance {-# OVERLAPPING  #-} TryCollectionList (Record  r) (Just r)
instance {-# OVERLAPPING  #-} TryCollectionList (Variant r) (Just r)
instance {-# OVERLAPPING  #-} TryCollectionList (TIC r) (Just r)
instance {-# OVERLAPPING  #-} TryCollectionList (TIP r) (Just r)
#endif

class MapFieldTree (ns :: Maybe [*]) (vs :: [[*]]) | ns -> vs

instance MapFieldTree Nothing '[]

-- | recursive case
instance (
    MapFieldTree (Just xs) vs3,
    FieldTree v vs1,
    MapCons (Label n) ('[] ': vs1) vs2,
    HAppendListR vs2 vs3 ~ vs)
    => MapFieldTree (Just (Tagged n v ': xs)) vs

instance MapFieldTree (Just '[]) '[]

-- | MapCons x xs xxs is like  xxs = map (x : ) xs
class MapCons (x :: k) (xs :: [[k]]) (xxs :: [[k]]) | x xs -> xxs
instance MapCons x '[] '[]
instance MapCons x b r => MapCons x (a ': b) ( (x ':  a) ': r)