{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE KindSignatures        #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeApplications      #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE QuantifiedConstraints #-}

-- | van Laarhoven lenses for large records.
-- The type synonym
--
-- @
--   type Lens' s a = forall f. Functor f => (a -> f a) -> s -> f s
-- @
-- Appears below, however it is not exported to avoid conflicts with other
-- libraries defining equivalent synonyms.
module Data.Record.Generic.Lens.VL (
    -- * Lenses for records
    SimpleRecordLens(..)
  , HKRecordLens(..)
  , RegularRecordLens(..)
  , lensesForSimpleRecord
  , lensesForHKRecord
  , lensesForRegularRecord
    -- * Regular records
  , RegularField(..)
  , IsRegularField(..)
    -- * Lenses into 'Rep'
  , RepLens(..)
  , repLenses
    -- * General purpose lenses
  , genericLens
  , normalForm1Lens
  , interpretedLens
  , standardInterpretationLens
  ) where

import Data.Kind

import Data.Record.Generic
import Data.Record.Generic.Transform

import qualified Data.Record.Generic.Rep as Rep

-- | The standard van Laarhoven representation for a monomorphic lens
type Lens' s a = forall f. Functor f => (a -> f a) -> s -> f s

{-------------------------------------------------------------------------------
  Simple records (in contrast to higher-kinded records, see below)
-------------------------------------------------------------------------------}

data SimpleRecordLens a b where
  SimpleRecordLens :: Lens' a b -> SimpleRecordLens a b

-- | Construct lenses for each field in the record
--
-- NOTE: This is of limited use since we cannot pattern match on the resulting
-- 'Rep' in any meaningful way. It is possible to go through the SOP adapter,
-- but if we do, we incur quadratic cost again.
--
-- We can do better for higher-kinded records, and better still for regular
-- higher-kinded records. See 'lensesForHKRecord' and 'lensesForRegularRecord'.
lensesForSimpleRecord :: forall a. Generic a => Rep (SimpleRecordLens a) a
lensesForSimpleRecord :: forall a. Generic a => Rep (SimpleRecordLens a) a
lensesForSimpleRecord =
    (forall x. RepLens I a x -> SimpleRecordLens a x)
-> Rep (RepLens I a) a -> Rep (SimpleRecordLens a) a
forall a (f :: * -> *) (g :: * -> *).
Generic a =>
(forall x. f x -> g x) -> Rep f a -> Rep g a
Rep.map (\(RepLens Lens' (Rep I a) (I x)
l) -> Lens' a x -> SimpleRecordLens a x
forall a b. Lens' a b -> SimpleRecordLens a b
SimpleRecordLens (Lens' a x -> SimpleRecordLens a x)
-> Lens' a x -> SimpleRecordLens a x
forall a b. (a -> b) -> a -> b
$ \x -> f x
f -> Lens' (Rep I a) (I x) -> Lens' a x
forall x. Lens' (Rep I a) (I x) -> Lens' a x
aux (I x -> f (I x)) -> Rep I a -> f (Rep I a)
Lens' (Rep I a) (I x)
l x -> f x
f) Rep (RepLens I a) a
forall a (f :: * -> *). Generic a => Rep (RepLens f a) a
repLenses
  where
    aux :: Lens' (Rep I a) (I x) -> Lens' a x
    aux :: forall x. Lens' (Rep I a) (I x) -> Lens' a x
aux Lens' (Rep I a) (I x)
l x -> f x
f a
a = Rep I a -> a
forall a. Generic a => Rep I a -> a
to (Rep I a -> a) -> f (Rep I a) -> f a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (I x -> f (I x)) -> Rep I a -> f (Rep I a)
Lens' (Rep I a) (I x)
l (\(I x
x) -> x -> I x
forall a. a -> I a
I (x -> I x) -> f x -> f (I x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> x -> f x
f x
x) (a -> Rep I a
forall a. Generic a => a -> Rep I a
from a
a)

{-------------------------------------------------------------------------------
  Higher-kinded records (records with a functor parameter)
-------------------------------------------------------------------------------}

-- | Lens for higher-kinded record
--
-- See 'lensesForHKRecord' for details.
data HKRecordLens d (f :: Type -> Type) tbl x where
  HKRecordLens :: Lens' (tbl f) (Interpret (d f) x) -> HKRecordLens d f tbl x

-- | Lenses for higher-kinded records
--
-- NOTE: The lenses constructed by this function are primarily intended for
-- further processing, either by 'lensesForRegularRecord' or using application
-- specific logic. Details below.
--
-- Suppose we have a record @tbl f@ which is indexed by a functor @f@, and we
-- want to construct lenses from @tbl f@ to each field in the record. Using the
-- @Transform@ infrastructure, we can construct a lens
--
-- > tbl f ~~> Rep I (tbl f) ~~> Rep (Interpret (d f)) (tbl Uninterpreted)
--
-- Using 'repLenses' we can construct a lens of type
--
-- > Rep (Interpret (d f)) (tbl Uninterpreted) ~~> Interpret (d f) x
--
-- for every field of type @x@. Putting these two together gives us a lens
--
-- > tbl f ~~> Interpret (d f) x
--
-- for every field in @tbl Uninterpreted@. We cannot simplify this, because we
-- do not know anything about the shape of @x@; specifically, it might not be
-- equal to @Uninterpreted x'@ for some @x'@, and hence we cannot simplify the
-- target type of the lens. We can do better for records with regular fields;
-- see 'lensesForRegularRecord'.
lensesForHKRecord :: forall d tbl f.
     ( Generic (tbl f)
     , Generic (tbl Uninterpreted)
     , HasNormalForm (d f) (tbl f) (tbl Uninterpreted)
     )
  => Proxy d -> Rep (HKRecordLens d f tbl) (tbl Uninterpreted)
lensesForHKRecord :: forall (d :: (* -> *) -> *) (tbl :: (* -> *) -> *) (f :: * -> *).
(Generic (tbl f), Generic (tbl Uninterpreted),
 HasNormalForm (d f) (tbl f) (tbl Uninterpreted)) =>
Proxy d -> Rep (HKRecordLens d f tbl) (tbl Uninterpreted)
lensesForHKRecord Proxy d
d = (forall x.
 RepLens (Interpret (d f)) (tbl Uninterpreted) x
 -> HKRecordLens d f tbl x)
-> Rep
     (RepLens (Interpret (d f)) (tbl Uninterpreted)) (tbl Uninterpreted)
-> Rep (HKRecordLens d f tbl) (tbl Uninterpreted)
forall a (f :: * -> *) (g :: * -> *).
Generic a =>
(forall x. f x -> g x) -> Rep f a -> Rep g a
Rep.map RepLens (Interpret (d f)) (tbl Uninterpreted) x
-> HKRecordLens d f tbl x
forall x.
RepLens (Interpret (d f)) (tbl Uninterpreted) x
-> HKRecordLens d f tbl x
aux Rep
  (RepLens (Interpret (d f)) (tbl Uninterpreted)) (tbl Uninterpreted)
fromRepLenses
  where
    fromRepLenses :: Rep (RepLens (Interpret (d f)) (tbl Uninterpreted)) (tbl Uninterpreted)
    fromRepLenses :: Rep
  (RepLens (Interpret (d f)) (tbl Uninterpreted)) (tbl Uninterpreted)
fromRepLenses = Rep
  (RepLens (Interpret (d f)) (tbl Uninterpreted)) (tbl Uninterpreted)
forall a (f :: * -> *). Generic a => Rep (RepLens f a) a
repLenses

    aux :: forall x. RepLens (Interpret (d f)) (tbl Uninterpreted) x -> HKRecordLens d f tbl x
    aux :: forall x.
RepLens (Interpret (d f)) (tbl Uninterpreted) x
-> HKRecordLens d f tbl x
aux (RepLens Lens'
  (Rep (Interpret (d f)) (tbl Uninterpreted)) (Interpret (d f) x)
l) = Lens' (tbl f) (Interpret (d f) x) -> HKRecordLens d f tbl x
forall (tbl :: (* -> *) -> *) (f :: * -> *) (d :: (* -> *) -> *) x.
Lens' (tbl f) (Interpret (d f) x) -> HKRecordLens d f tbl x
HKRecordLens (Lens' (tbl f) (Interpret (d f) x) -> HKRecordLens d f tbl x)
-> Lens' (tbl f) (Interpret (d f) x) -> HKRecordLens d f tbl x
forall a b. (a -> b) -> a -> b
$
          (Rep I (tbl f) -> f (Rep I (tbl f))) -> tbl f -> f (tbl f)
forall a. Generic a => Lens' a (Rep I a)
Lens' (tbl f) (Rep I (tbl f))
genericLens
        ((Rep I (tbl f) -> f (Rep I (tbl f))) -> tbl f -> f (tbl f))
-> ((Interpret (d f) x -> f (Interpret (d f) x))
    -> Rep I (tbl f) -> f (Rep I (tbl f)))
-> (Interpret (d f) x -> f (Interpret (d f) x))
-> tbl f
-> f (tbl f)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy d
-> Lens'
     (Rep I (tbl f)) (Rep (Interpret (d f)) (tbl Uninterpreted))
forall (d :: (* -> *) -> *) (f :: * -> *) (x :: (* -> *) -> *).
HasNormalForm (d f) (x f) (x Uninterpreted) =>
Proxy d
-> Lens' (Rep I (x f)) (Rep (Interpret (d f)) (x Uninterpreted))
normalForm1Lens Proxy d
d
        ((Rep (Interpret (d f)) (tbl Uninterpreted)
  -> f (Rep (Interpret (d f)) (tbl Uninterpreted)))
 -> Rep I (tbl f) -> f (Rep I (tbl f)))
-> ((Interpret (d f) x -> f (Interpret (d f) x))
    -> Rep (Interpret (d f)) (tbl Uninterpreted)
    -> f (Rep (Interpret (d f)) (tbl Uninterpreted)))
-> (Interpret (d f) x -> f (Interpret (d f) x))
-> Rep I (tbl f)
-> f (Rep I (tbl f))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Interpret (d f) x -> f (Interpret (d f) x))
-> Rep (Interpret (d f)) (tbl Uninterpreted)
-> f (Rep (Interpret (d f)) (tbl Uninterpreted))
Lens'
  (Rep (Interpret (d f)) (tbl Uninterpreted)) (Interpret (d f) x)
l

{-------------------------------------------------------------------------------
  Regular records
-------------------------------------------------------------------------------}

-- | Proof that @x@ is a regular field
--
-- See 'IsRegularField'
data RegularField f x where
  RegularField :: RegularField f (f x)

-- | Regular record fields
--
-- For a higher-kinded record @tbl f@, parameterized over some functor @f@,
-- we say that the fields are /regular/ iff every field has the form @f x@
-- for some @x@.
class IsRegularField f x where
  isRegularField :: Proxy (f x) -> RegularField f x

instance IsRegularField f (f x) where
  isRegularField :: Proxy (f (f x)) -> RegularField f (f x)
isRegularField Proxy (f (f x))
_ = RegularField f (f x)
forall (f :: * -> *) x. RegularField f (f x)
RegularField

{-------------------------------------------------------------------------------
  Lenses into regular records
-------------------------------------------------------------------------------}

-- | Lens into a regular record
--
-- See 'lensesForRegularRecord'
data RegularRecordLens tbl f x where
  RegularRecordLens :: Lens' (tbl f) (f x) -> RegularRecordLens tbl f x

-- | Lenses into higher-kinded records with regular fields
--
-- We can use 'lensesForHKRecord' to construct a 'Rep' of lenses into a higher-kinded
-- record. If in addition the record is regular, we can use the record type
-- /itself/ to store all the lenses.
lensesForRegularRecord :: forall d tbl f.
     ( Generic (tbl (RegularRecordLens tbl f))
     , Generic (tbl Uninterpreted)
     , Generic (tbl f)
     , HasNormalForm (d (RegularRecordLens tbl f)) (tbl (RegularRecordLens tbl f)) (tbl Uninterpreted)
     , HasNormalForm (d f) (tbl f) (tbl Uninterpreted)
     , Constraints (tbl Uninterpreted) (IsRegularField Uninterpreted)
     , StandardInterpretation d (RegularRecordLens tbl f)
     , StandardInterpretation d f
     )
  => Proxy d -> tbl (RegularRecordLens tbl f)
lensesForRegularRecord :: forall (d :: (* -> *) -> *) (tbl :: (* -> *) -> *) (f :: * -> *).
(Generic (tbl (RegularRecordLens tbl f)),
 Generic (tbl Uninterpreted), Generic (tbl f),
 HasNormalForm
   (d (RegularRecordLens tbl f))
   (tbl (RegularRecordLens tbl f))
   (tbl Uninterpreted),
 HasNormalForm (d f) (tbl f) (tbl Uninterpreted),
 Constraints (tbl Uninterpreted) (IsRegularField Uninterpreted),
 StandardInterpretation d (RegularRecordLens tbl f),
 StandardInterpretation d f) =>
Proxy d -> tbl (RegularRecordLens tbl f)
lensesForRegularRecord Proxy d
d = Rep I (tbl (RegularRecordLens tbl f))
-> tbl (RegularRecordLens tbl f)
forall a. Generic a => Rep I a -> a
to (Rep I (tbl (RegularRecordLens tbl f))
 -> tbl (RegularRecordLens tbl f))
-> (Rep
      (Interpret (d (RegularRecordLens tbl f))) (tbl Uninterpreted)
    -> Rep I (tbl (RegularRecordLens tbl f)))
-> Rep
     (Interpret (d (RegularRecordLens tbl f))) (tbl Uninterpreted)
-> tbl (RegularRecordLens tbl f)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy d
-> Rep
     (Interpret (d (RegularRecordLens tbl f))) (tbl Uninterpreted)
-> Rep I (tbl (RegularRecordLens tbl f))
forall {k} {dom} (d :: (k -> *) -> dom) (f :: k -> *)
       (x :: (k -> *) -> *).
HasNormalForm (d f) (x f) (x Uninterpreted) =>
Proxy d -> Rep (Interpret (d f)) (x Uninterpreted) -> Rep I (x f)
denormalize1 Proxy d
d (Rep (Interpret (d (RegularRecordLens tbl f))) (tbl Uninterpreted)
 -> tbl (RegularRecordLens tbl f))
-> Rep
     (Interpret (d (RegularRecordLens tbl f))) (tbl Uninterpreted)
-> tbl (RegularRecordLens tbl f)
forall a b. (a -> b) -> a -> b
$
    Proxy (IsRegularField Uninterpreted)
-> (forall x.
    IsRegularField Uninterpreted x =>
    HKRecordLens d f tbl x
    -> Interpret (d (RegularRecordLens tbl f)) x)
-> Rep (HKRecordLens d f tbl) (tbl Uninterpreted)
-> Rep
     (Interpret (d (RegularRecordLens tbl f))) (tbl Uninterpreted)
forall a (c :: * -> Constraint) (f :: * -> *) (g :: * -> *).
(Generic a, Constraints a c) =>
Proxy c -> (forall x. c x => f x -> g x) -> Rep f a -> Rep g a
Rep.cmap
      (forall {k} (t :: k). Proxy t
forall (t :: * -> Constraint). Proxy t
Proxy @(IsRegularField Uninterpreted))
      HKRecordLens d f tbl x -> Interpret (d (RegularRecordLens tbl f)) x
forall x.
IsRegularField Uninterpreted x =>
HKRecordLens d f tbl x -> Interpret (d (RegularRecordLens tbl f)) x
aux
      (Proxy d -> Rep (HKRecordLens d f tbl) (tbl Uninterpreted)
forall (d :: (* -> *) -> *) (tbl :: (* -> *) -> *) (f :: * -> *).
(Generic (tbl f), Generic (tbl Uninterpreted),
 HasNormalForm (d f) (tbl f) (tbl Uninterpreted)) =>
Proxy d -> Rep (HKRecordLens d f tbl) (tbl Uninterpreted)
lensesForHKRecord Proxy d
d)
  where
    aux :: forall x.
         IsRegularField Uninterpreted x
      => HKRecordLens d f tbl x
      -> Interpret (d (RegularRecordLens tbl f)) x
    aux :: forall x.
IsRegularField Uninterpreted x =>
HKRecordLens d f tbl x -> Interpret (d (RegularRecordLens tbl f)) x
aux (HKRecordLens Lens' (tbl f) (Interpret (d f) x)
l) =
        case Proxy (Uninterpreted x) -> RegularField Uninterpreted x
forall (f :: * -> *) x.
IsRegularField f x =>
Proxy (f x) -> RegularField f x
isRegularField (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(Uninterpreted x)) of
          RegularField Uninterpreted x
RegularField -> Proxy d
-> RegularRecordLens tbl f x
-> Interpret (d (RegularRecordLens tbl f)) (Uninterpreted x)
forall {k} {dom} (d :: (k -> *) -> dom) (f :: k -> *) (x :: k).
StandardInterpretation d f =>
Proxy d -> f x -> Interpret (d f) (Uninterpreted x)
toStandardInterpretation Proxy d
d (RegularRecordLens tbl f x
 -> Interpret (d (RegularRecordLens tbl f)) (Uninterpreted x))
-> RegularRecordLens tbl f x
-> Interpret (d (RegularRecordLens tbl f)) (Uninterpreted x)
forall a b. (a -> b) -> a -> b
$ Lens' (tbl f) (f x) -> RegularRecordLens tbl f x
forall (tbl :: (* -> *) -> *) (f :: * -> *) x.
Lens' (tbl f) (f x) -> RegularRecordLens tbl f x
RegularRecordLens (Lens' (tbl f) (f x) -> RegularRecordLens tbl f x)
-> Lens' (tbl f) (f x) -> RegularRecordLens tbl f x
forall a b. (a -> b) -> a -> b
$
             (Interpret (d f) x -> f (Interpret (d f) x)) -> tbl f -> f (tbl f)
Lens' (tbl f) (Interpret (d f) x)
l ((Interpret (d f) x -> f (Interpret (d f) x))
 -> tbl f -> f (tbl f))
-> ((f x -> f (f x)) -> Interpret (d f) x -> f (Interpret (d f) x))
-> (f x -> f (f x))
-> tbl f
-> f (tbl f)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy d -> Lens' (Interpret (d f) (Uninterpreted x)) (f x)
forall (d :: (* -> *) -> *) (f :: * -> *) x.
StandardInterpretation d f =>
Proxy d -> Lens' (Interpret (d f) (Uninterpreted x)) (f x)
standardInterpretationLens Proxy d
d

{-------------------------------------------------------------------------------
  Lenses into 'Rep'
-------------------------------------------------------------------------------}

data RepLens f a x where
  RepLens :: Lens' (Rep f a) (f x) -> RepLens f a x

repLenses :: Generic a => Rep (RepLens f a) a
repLenses :: forall a (f :: * -> *). Generic a => Rep (RepLens f a) a
repLenses = (forall x. Index a x -> RepLens f a x)
-> Rep (Index a) a -> Rep (RepLens f a) a
forall a (f :: * -> *) (g :: * -> *).
Generic a =>
(forall x. f x -> g x) -> Rep f a -> Rep g a
Rep.map Index a x -> RepLens f a x
forall x. Index a x -> RepLens f a x
forall a x (f :: * -> *). Index a x -> RepLens f a x
aux Rep (Index a) a
forall a. Generic a => Rep (Index a) a
Rep.allIndices
  where
    aux :: Rep.Index a x -> RepLens f a x
    aux :: forall a x (f :: * -> *). Index a x -> RepLens f a x
aux Index a x
ix = Lens' (Rep f a) (f x) -> RepLens f a x
forall (f :: * -> *) a x. Lens' (Rep f a) (f x) -> RepLens f a x
RepLens (Lens' (Rep f a) (f x) -> RepLens f a x)
-> Lens' (Rep f a) (f x) -> RepLens f a x
forall a b. (a -> b) -> a -> b
$ Index a x -> (f x -> f (f x)) -> Rep f a -> f (Rep f a)
forall (m :: * -> *) a x (f :: * -> *).
Functor m =>
Index a x -> (f x -> m (f x)) -> Rep f a -> m (Rep f a)
Rep.updateAtIndex Index a x
ix

{-------------------------------------------------------------------------------
  General purpose lenses
-------------------------------------------------------------------------------}

genericLens :: Generic a => Lens' a (Rep I a)
genericLens :: forall a. Generic a => Lens' a (Rep I a)
genericLens Rep I a -> f (Rep I a)
f a
a = Rep I a -> a
forall a. Generic a => Rep I a -> a
to (Rep I a -> a) -> f (Rep I a) -> f a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Rep I a -> f (Rep I a)
f (a -> Rep I a
forall a. Generic a => a -> Rep I a
from a
a)

normalForm1Lens ::
     HasNormalForm (d f) (x f) (x Uninterpreted)
  => Proxy d
  -> Lens' (Rep I (x f)) (Rep (Interpret (d f)) (x Uninterpreted))
normalForm1Lens :: forall (d :: (* -> *) -> *) (f :: * -> *) (x :: (* -> *) -> *).
HasNormalForm (d f) (x f) (x Uninterpreted) =>
Proxy d
-> Lens' (Rep I (x f)) (Rep (Interpret (d f)) (x Uninterpreted))
normalForm1Lens Proxy d
p Rep (Interpret (d f)) (x Uninterpreted)
-> f (Rep (Interpret (d f)) (x Uninterpreted))
f Rep I (x f)
a = Proxy d -> Rep (Interpret (d f)) (x Uninterpreted) -> Rep I (x f)
forall {k} {dom} (d :: (k -> *) -> dom) (f :: k -> *)
       (x :: (k -> *) -> *).
HasNormalForm (d f) (x f) (x Uninterpreted) =>
Proxy d -> Rep (Interpret (d f)) (x Uninterpreted) -> Rep I (x f)
denormalize1 Proxy d
p (Rep (Interpret (d f)) (x Uninterpreted) -> Rep I (x f))
-> f (Rep (Interpret (d f)) (x Uninterpreted)) -> f (Rep I (x f))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Rep (Interpret (d f)) (x Uninterpreted)
-> f (Rep (Interpret (d f)) (x Uninterpreted))
f (Proxy d -> Rep I (x f) -> Rep (Interpret (d f)) (x Uninterpreted)
forall {k} {dom} (d :: (k -> *) -> dom) (f :: k -> *)
       (x :: (k -> *) -> *).
HasNormalForm (d f) (x f) (x Uninterpreted) =>
Proxy d -> Rep I (x f) -> Rep (Interpret (d f)) (x Uninterpreted)
normalize1 Proxy d
p Rep I (x f)
a)

interpretedLens :: Lens' (Interpret d x) (Interpreted d x)
interpretedLens :: forall d x (f :: * -> *).
Functor f =>
(Interpreted d x -> f (Interpreted d x))
-> Interpret d x -> f (Interpret d x)
interpretedLens Interpreted d x -> f (Interpreted d x)
f (Interpret Interpreted d x
x) = Interpreted d x -> Interpret d x
forall {dom} (d :: dom) x. Interpreted d x -> Interpret d x
Interpret (Interpreted d x -> Interpret d x)
-> f (Interpreted d x) -> f (Interpret d x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Interpreted d x -> f (Interpreted d x)
f Interpreted d x
x

standardInterpretationLens :: forall d f x.
     StandardInterpretation d f
  => Proxy d
  -> Lens' (Interpret (d f) (Uninterpreted x)) (f x)
standardInterpretationLens :: forall (d :: (* -> *) -> *) (f :: * -> *) x.
StandardInterpretation d f =>
Proxy d -> Lens' (Interpret (d f) (Uninterpreted x)) (f x)
standardInterpretationLens Proxy d
p f x -> f (f x)
f Interpret (d f) (Uninterpreted x)
x =
    Proxy d -> f x -> Interpret (d f) (Uninterpreted x)
forall {k} {dom} (d :: (k -> *) -> dom) (f :: k -> *) (x :: k).
StandardInterpretation d f =>
Proxy d -> f x -> Interpret (d f) (Uninterpreted x)
toStandardInterpretation Proxy d
p (f x -> Interpret (d f) (Uninterpreted x))
-> f (f x) -> f (Interpret (d f) (Uninterpreted x))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
      f x -> f (f x)
f (Proxy d -> Interpret (d f) (Uninterpreted x) -> f x
forall {k} {dom} (d :: (k -> *) -> dom) (f :: k -> *) (x :: k).
StandardInterpretation d f =>
Proxy d -> Interpret (d f) (Uninterpreted x) -> f x
fromStandardInterpretation Proxy d
p Interpret (d f) (Uninterpreted x)
x)