{-# 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 -> y
toLabelx x
x = forall x y. EnsureLabel x y => x -> y
toLabel x
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 :: x -> p v fb -> p r rft
dredge x
label = forall {k} (p :: * -> k -> *) a (fb :: k) rs (rft :: k) stab.
((p a fb -> p rs rft) ~ stab) =>
(Proxy rs -> Proxy a -> stab) -> stab
getSAfromOutputOptic forall a b. (a -> b) -> a -> b
$ \ Proxy r
pr Proxy v
pa ->
      forall (xs :: [*]) apb spt.
LabelablePath xs apb spt =>
Label xs -> apb -> spt
hLens'Path (forall {k} r (l :: k) 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,
 HSingleton
   (NonUnique r v l) (TypesDontMatch r ns1 vs1 v) ns2 path) =>
Proxy r -> Label l -> Proxy v -> Label path
labelPathEndingWithTD Proxy r
pr (forall x y. EnsureLabel x y => x -> y
toLabelx x
label) Proxy v
pa)



getSAfromOutputOptic :: (p a fb -> p rs rft) ~ stab
                => (Proxy (rs :: *) -> Proxy (a :: *) -> stab) -> stab
getSAfromOutputOptic :: forall {k} (p :: * -> k -> *) a (fb :: k) rs (rft :: k) stab.
((p a fb -> p rs rft) ~ stab) =>
(Proxy rs -> Proxy a -> stab) -> stab
getSAfromOutputOptic Proxy rs -> Proxy a -> stab
f = Proxy rs -> Proxy a -> stab
f forall {k} (t :: k). Proxy t
Proxy forall {k} (t :: k). Proxy t
Proxy


-- | 'dredge' except a simple (s ~ t, a ~ b) optic is produced
dredge' :: x -> p a (f a) -> p s (f s)
dredge' x
label = forall {k1} {k2} optic (p :: k1 -> k2 -> *) (a :: k1)
       (f :: k1 -> k2) (s :: k1).
(optic ~ (p a (f a) -> p s (f s))) =>
optic -> optic
isSimple (forall {k} {k} {r} {ns :: [[*]]} {xs :: [*]} {p :: * -> k -> *} {v}
       {fb :: k} {rft :: k} {vs :: [*]} {ns1 :: [[*]]} {vs1 :: [*]}
       {l :: k} {ns2 :: [[*]]} {x}.
(MapFieldTree (TryCollectionListTF r) ns,
 LabelablePath xs (p v fb) (p r rft), SameLength' ns vs,
 SameLength' ns1 vs1, SameLength' vs ns, SameLength' vs1 ns1,
 MapFieldTreeVal r (TryCollectionListTF 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,
 HSingleton (NonUnique r v l) (TypesDontMatch r ns1 vs1 v) ns2 xs,
 EnsureLabel x (Label l)) =>
x -> p v fb -> p r rft
dredge x
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 :: x -> p a fb -> p r rft
dredgeND x
label = forall {k} (p :: * -> k -> *) a (fb :: k) rs (rft :: k) stab.
((p a fb -> p rs rft) ~ stab) =>
(Proxy rs -> Proxy a -> stab) -> stab
getSAfromOutputOptic forall a b. (a -> b) -> a -> b
$ \ Proxy r
pr Proxy a
_a ->
      forall (xs :: [*]) apb spt.
LabelablePath xs apb spt =>
Label xs -> apb -> spt
hLens'Path (forall k r (l :: k) (path :: [*]) (proxy :: * -> *).
LabelPathEndingWith r l path =>
proxy r -> Label l -> Label path
labelPathEndingWith Proxy r
pr (forall x y. EnsureLabel x y => x -> y
toLabelx x
label))


-- | 'dredgeND' except a simple (s ~ t, a ~ b) optic is produced
dredgeND' :: x -> p a (f a) -> p s (f s)
dredgeND' x
label = forall {k1} {k2} optic (p :: k1 -> k2 -> *) (a :: k1)
       (f :: k1 -> k2) (s :: k1).
(optic ~ (p a (f a) -> p s (f s))) =>
optic -> optic
isSimple (forall {k} {k} {xs :: [*]} {p :: * -> k -> *} {a} {fb :: k} {r}
       {rft :: k} {ns :: [[*]]} {l :: k} {ns' :: [[*]]} {x}.
(LabelablePath xs (p a fb) (p r rft),
 MapFieldTree (TryCollectionListTF r) ns,
 FilterLastEq (Label l) ns ns ns',
 HSingleton (NonUnique' r l) (NamesDontMatch r ns l) ns' xs,
 EnsureLabel x (Label l)) =>
x -> p a fb -> p r rft
dredgeND x
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' :: q a -> p a (f a) -> p s (f s)
dredgeTI' q a
label = forall {k1} {k2} optic (p :: k1 -> k2 -> *) (a :: k1)
       (f :: k1 -> k2) (s :: k1).
(optic ~ (p a (f a) -> p s (f s))) =>
optic -> optic
isSimple p a (f a) -> p s (f s)
lens where
        lens :: p a (f a) -> p s (f s)
lens = forall {k} (p :: * -> k -> *) a (fb :: k) rs (rft :: k) stab.
((p a fb -> p rs rft) ~ stab) =>
(Proxy rs -> Proxy a -> stab) -> stab
getSAfromOutputOptic forall a b. (a -> b) -> a -> b
$ \ Proxy s
pr Proxy a
pa ->
            forall (xs :: [*]) apb spt.
LabelablePath xs apb spt =>
Label xs -> apb -> spt
hLens'Path (forall k r (l :: k) (path :: [*]) (proxy :: * -> *).
LabelPathEndingWith r l path =>
proxy r -> Label l -> Label path
labelPathEndingWith Proxy s
pr (Proxy a
pa forall {k} (p :: k -> *) (a :: k) (q :: k -> *).
p a -> q a -> Label a
`proxyTypeOf` q a
label))

        proxyTypeOf :: p a -> q a -> Label a
        proxyTypeOf :: forall {k} (p :: k -> *) (a :: k) (q :: k -> *).
p a -> q a -> Label a
proxyTypeOf p a
_ q a
_ = forall {k} (l :: k). Label l
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 proxy r
_ Label l
_ = forall {k} (l :: k). Label l
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 :: forall {k} r (l :: k) 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,
 HSingleton
   (NonUnique r v l) (TypesDontMatch r ns1 vs1 v) ns2 path) =>
Proxy r -> Label l -> Proxy v -> Label path
labelPathEndingWithTD Proxy r
_ Label l
_ Proxy v
_ = forall {k} (l :: k). Label l
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 :: Label l -> r r -> v
hLookupByLabelDredge Label l
l r r
r = forall k r (l :: k) (path :: [*]) (proxy :: * -> *).
LabelPathEndingWith r l path =>
proxy r -> Label l -> Label path
labelPathEndingWith (forall {k} (r :: k -> *) (x :: k). r x -> Proxy x
toProxy r r
r) Label l
l forall (ls :: [*]) r v.
HasFieldPath 'False ls r v =>
Label ls -> r -> v
`hLookupByLabelPath` r r
r
  where toProxy :: r x -> Proxy x
        toProxy :: forall {k} (r :: k -> *) (x :: k). r x -> Proxy x
toProxy r x
_ = forall {k} (t :: k). Proxy t
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 :: forall (ls :: [*]) r v.
HasFieldPath 'False ls r v =>
Label ls -> r -> v
hLookupByLabelPath Label ls
labels r
r = forall (needJust :: Bool) (ls :: [*]) r v.
HasFieldPath needJust ls r v =>
Proxy needJust -> Label ls -> r -> v
hLookupByLabelPath1 Proxy 'False
hFalse Label ls
labels r
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 :: Label (Label x : xs) -> i -> k
hLens'Path Label (Label x : xs)
_ = (forall k (x :: k) (r :: [*] -> *) (s :: [*]) (t :: [*]) a b.
Labelable x r s t a b =>
Label x -> LabeledOptic x r s t a b
hLens' (forall {k} (l :: k). Label l
Label :: Label x) :: j -> k) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (xs :: [*]) apb spt.
LabelablePath xs apb spt =>
Label xs -> apb -> spt
hLens'Path (forall {k} (l :: k). Label l
Label :: Label xs)

instance (x ~ x') => LabelablePath '[] x x' where
    hLens'Path :: Label '[] -> x -> x'
hLens'Path Label '[]
_ = forall a. a -> a
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 :: Proxy 'False -> Label '[] -> v -> v
hLookupByLabelPath1 Proxy 'False
_ Label '[]
_ = forall a. a -> a
id

instance HasFieldPath True '[] v (Maybe v) where
    hLookupByLabelPath1 :: Proxy 'True -> Label '[] -> v -> Maybe v
hLookupByLabelPath1 Proxy 'True
_ Label '[]
_ = forall a. a -> Maybe a
Just

instance (HasField l (Record r) u, HasFieldPath needJust ls u v)
    => HasFieldPath needJust (Label l ': ls) (Record r) v where
     hLookupByLabelPath1 :: Proxy needJust -> Label (Label l : ls) -> Record r -> v
hLookupByLabelPath1 Proxy needJust
needJust Label (Label l : ls)
_ = forall (needJust :: Bool) (ls :: [*]) r v.
HasFieldPath needJust ls r v =>
Proxy needJust -> Label ls -> r -> v
hLookupByLabelPath1 Proxy needJust
needJust (forall {k} (l :: k). Label l
Label :: Label ls)
                                forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (l :: k) r v. HasField l r v => Label l -> r -> v
hLookupByLabel (forall {k} (l :: k). Label l
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 :: Proxy needJust -> Label (Label l : ls) -> Variant r -> Maybe v
hLookupByLabelPath1 Proxy needJust
_ Label (Label l : ls)
_ Variant r
v = forall (needJust :: Bool) (ls :: [*]) r v.
HasFieldPath needJust ls r v =>
Proxy needJust -> Label ls -> r -> v
hLookupByLabelPath1 Proxy 'True
hTrue (forall {k} (l :: k). Label l
Label :: Label ls) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall k (l :: k) r v. HasField l r v => Label l -> r -> v
hLookupByLabel (forall {k} (l :: k). Label l
Label :: Label l) Variant r
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)