{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE UndecidableInstances #-}

-- | Row types
module Hyper.Syntax.Row
    ( RowConstraints (..)
    , RowKey
    , RowExtend (..)
    , eKey
    , eVal
    , eRest
    , W_RowExtend (..)
    , FlatRowExtends (..)
    , freExtends
    , freRest
    , W_FlatRowExtends (..)
    , MorphWitness (..)
    , flattenRow
    , flattenRowExtend
    , unflattenRow
    , verifyRowExtendConstraints
    , rowExtendStructureMismatch
    , rowElementInfer
    ) where

import Control.Lens (Lens', Prism', contains)
import qualified Control.Lens as Lens
import Control.Monad (foldM)
import qualified Data.Map as Map
import Generics.Constraints (Constraints, makeDerivings, makeInstances)
import Hyper
import Hyper.Unify
import Hyper.Unify.New (newTerm, newUnbound)
import Hyper.Unify.Term (UTerm (..), UTermBody (..), uBody, _UTerm)
import Text.Show.Combinators (showCon, (@|))

import Hyper.Internal.Prelude

class
    (Ord (RowConstraintsKey constraints), TypeConstraints constraints) =>
    RowConstraints constraints
    where
    type RowConstraintsKey constraints
    forbidden :: Lens' constraints (Set (RowConstraintsKey constraints))

type RowKey typ = RowConstraintsKey (TypeConstraintsOf typ)

-- | Row-extend primitive for use in both value-level and type-level
data RowExtend key val rest h = RowExtend
    { forall key (val :: HyperType) (rest :: HyperType)
       (h :: AHyperType).
RowExtend key val rest h -> key
_eKey :: key
    , forall key (val :: HyperType) (rest :: HyperType)
       (h :: AHyperType).
RowExtend key val rest h -> h :# val
_eVal :: h :# val
    , forall key (val :: HyperType) (rest :: HyperType)
       (h :: AHyperType).
RowExtend key val rest h -> h :# rest
_eRest :: h :# rest
    }
    deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall key (val :: HyperType) (rest :: HyperType) (h :: AHyperType)
       x.
Rep (RowExtend key val rest h) x -> RowExtend key val rest h
forall key (val :: HyperType) (rest :: HyperType) (h :: AHyperType)
       x.
RowExtend key val rest h -> Rep (RowExtend key val rest h) x
$cto :: forall key (val :: HyperType) (rest :: HyperType) (h :: AHyperType)
       x.
Rep (RowExtend key val rest h) x -> RowExtend key val rest h
$cfrom :: forall key (val :: HyperType) (rest :: HyperType) (h :: AHyperType)
       x.
RowExtend key val rest h -> Rep (RowExtend key val rest h) x
Generic)

data FlatRowExtends key val rest h = FlatRowExtends
    { forall key (val :: HyperType) (rest :: HyperType)
       (h :: AHyperType).
FlatRowExtends key val rest h -> Map key (h :# val)
_freExtends :: Map key (h :# val)
    , forall key (val :: HyperType) (rest :: HyperType)
       (h :: AHyperType).
FlatRowExtends key val rest h -> h :# rest
_freRest :: h :# rest
    }
    deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall key (val :: HyperType) (rest :: HyperType) (h :: AHyperType)
       x.
Rep (FlatRowExtends key val rest h) x
-> FlatRowExtends key val rest h
forall key (val :: HyperType) (rest :: HyperType) (h :: AHyperType)
       x.
FlatRowExtends key val rest h
-> Rep (FlatRowExtends key val rest h) x
$cto :: forall key (val :: HyperType) (rest :: HyperType) (h :: AHyperType)
       x.
Rep (FlatRowExtends key val rest h) x
-> FlatRowExtends key val rest h
$cfrom :: forall key (val :: HyperType) (rest :: HyperType) (h :: AHyperType)
       x.
FlatRowExtends key val rest h
-> Rep (FlatRowExtends key val rest h) x
Generic)

makeLenses ''RowExtend
makeLenses ''FlatRowExtends
makeCommonInstances [''FlatRowExtends]
makeZipMatch ''RowExtend
makeHContext ''RowExtend
makeHMorph ''RowExtend
makeHTraversableApplyAndBases ''RowExtend
makeHTraversableApplyAndBases ''FlatRowExtends
makeDerivings [''Eq, ''Ord] [''RowExtend]
makeInstances [''Binary, ''NFData] [''RowExtend]

instance
    Constraints (RowExtend key val rest h) Show =>
    Show (RowExtend key val rest h)
    where
    showsPrec :: Int -> RowExtend key val rest h -> ShowS
showsPrec Int
p (RowExtend key
h GetHyperType h ('AHyperType val)
v GetHyperType h ('AHyperType rest)
r) = (String -> PrecShowS
showCon String
"RowExtend" forall a. Show a => PrecShowS -> a -> PrecShowS
@| key
h forall a. Show a => PrecShowS -> a -> PrecShowS
@| GetHyperType h ('AHyperType val)
v forall a. Show a => PrecShowS -> a -> PrecShowS
@| GetHyperType h ('AHyperType rest)
r) Int
p

{-# INLINE flattenRowExtend #-}
flattenRowExtend ::
    (Ord key, Monad m) =>
    (v # rest -> m (Maybe (RowExtend key val rest # v))) ->
    RowExtend key val rest # v ->
    m (FlatRowExtends key val rest # v)
flattenRowExtend :: forall key (m :: * -> *) (v :: HyperType) (rest :: HyperType)
       (val :: HyperType).
(Ord key, Monad m) =>
((v # rest) -> m (Maybe (RowExtend key val rest # v)))
-> (RowExtend key val rest # v)
-> m (FlatRowExtends key val rest # v)
flattenRowExtend (v # rest) -> m (Maybe (RowExtend key val rest # v))
nextExtend (RowExtend key
h 'AHyperType v :# val
v 'AHyperType v :# rest
rest) =
    forall key (m :: * -> *) (v :: HyperType) (rest :: HyperType)
       (val :: HyperType).
(Ord key, Monad m) =>
((v # rest) -> m (Maybe (RowExtend key val rest # v)))
-> (v # rest) -> m (FlatRowExtends key val rest # v)
flattenRow (v # rest) -> m (Maybe (RowExtend key val rest # v))
nextExtend 'AHyperType v :# rest
rest
        forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> forall key (val :: HyperType) (rest :: HyperType) (h :: AHyperType)
       key (val :: HyperType).
Lens
  (FlatRowExtends key val rest h)
  (FlatRowExtends key val rest h)
  (Map key (h :# val))
  (Map key (h :# val))
freExtends forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith (forall a. HasCallStack => String -> a
error String
"Colliding keys") (forall k a. k -> a -> Map k a
Map.singleton key
h 'AHyperType v :# val
v)

{-# INLINE flattenRow #-}
flattenRow ::
    (Ord key, Monad m) =>
    (v # rest -> m (Maybe (RowExtend key val rest # v))) ->
    v # rest ->
    m (FlatRowExtends key val rest # v)
flattenRow :: forall key (m :: * -> *) (v :: HyperType) (rest :: HyperType)
       (val :: HyperType).
(Ord key, Monad m) =>
((v # rest) -> m (Maybe (RowExtend key val rest # v)))
-> (v # rest) -> m (FlatRowExtends key val rest # v)
flattenRow (v # rest) -> m (Maybe (RowExtend key val rest # v))
nextExtend v # rest
x =
    (v # rest) -> m (Maybe (RowExtend key val rest # v))
nextExtend v # rest
x
        forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall key (val :: HyperType) (rest :: HyperType)
       (h :: AHyperType).
Map key (h :# val) -> (h :# rest) -> FlatRowExtends key val rest h
FlatRowExtends forall a. Monoid a => a
mempty v # rest
x)) (forall key (m :: * -> *) (v :: HyperType) (rest :: HyperType)
       (val :: HyperType).
(Ord key, Monad m) =>
((v # rest) -> m (Maybe (RowExtend key val rest # v)))
-> (RowExtend key val rest # v)
-> m (FlatRowExtends key val rest # v)
flattenRowExtend (v # rest) -> m (Maybe (RowExtend key val rest # v))
nextExtend)

{-# INLINE unflattenRow #-}
unflattenRow ::
    Monad m =>
    (RowExtend key val rest # v -> m (v # rest)) ->
    FlatRowExtends key val rest # v ->
    m (v # rest)
unflattenRow :: forall (m :: * -> *) key (val :: HyperType) (rest :: HyperType)
       (v :: HyperType).
Monad m =>
((RowExtend key val rest # v) -> m (v # rest))
-> (FlatRowExtends key val rest # v) -> m (v # rest)
unflattenRow (RowExtend key val rest # v) -> m (v # rest)
mkExtend (FlatRowExtends Map key ('AHyperType v :# val)
fields 'AHyperType v :# rest
rest) =
    Map key ('AHyperType v :# val)
fields forall s i a. s -> IndexedGetting i (Endo [(i, a)]) s a -> [(i, a)]
^@.. forall i (t :: * -> *) a b.
TraversableWithIndex i t =>
IndexedTraversal i (t a) (t b) a b
Lens.itraversed forall a b. a -> (a -> b) -> b
& forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (v # rest) -> (key, v # val) -> m (v # rest)
f 'AHyperType v :# rest
rest
    where
        f :: (v # rest) -> (key, v # val) -> m (v # rest)
f v # rest
acc (key
key, v # val
val) = forall key (val :: HyperType) (rest :: HyperType)
       (h :: AHyperType).
key -> (h :# val) -> (h :# rest) -> RowExtend key val rest h
RowExtend key
key v # val
val v # rest
acc forall a b. a -> (a -> b) -> b
& (RowExtend key val rest # v) -> m (v # rest)
mkExtend

-- Helpers for Unify instances of type-level RowExtends:

{-# INLINE verifyRowExtendConstraints #-}
verifyRowExtendConstraints ::
    RowConstraints (TypeConstraintsOf rowTyp) =>
    (TypeConstraintsOf rowTyp -> TypeConstraintsOf valTyp) ->
    TypeConstraintsOf rowTyp ->
    RowExtend (RowKey rowTyp) valTyp rowTyp # h ->
    Maybe (RowExtend (RowKey rowTyp) valTyp rowTyp # WithConstraint h)
verifyRowExtendConstraints :: forall (rowTyp :: HyperType) (valTyp :: HyperType)
       (h :: HyperType).
RowConstraints (TypeConstraintsOf rowTyp) =>
(TypeConstraintsOf rowTyp -> TypeConstraintsOf valTyp)
-> TypeConstraintsOf rowTyp
-> (RowExtend (RowKey rowTyp) valTyp rowTyp # h)
-> Maybe
     (RowExtend (RowKey rowTyp) valTyp rowTyp # WithConstraint h)
verifyRowExtendConstraints TypeConstraintsOf rowTyp -> TypeConstraintsOf valTyp
toChildC TypeConstraintsOf rowTyp
c (RowExtend RowConstraintsKey (TypeConstraintsOf rowTyp)
h 'AHyperType h :# valTyp
v 'AHyperType h :# rowTyp
rest)
    | TypeConstraintsOf rowTyp
c forall s a. s -> Getting a s a -> a
^. forall constraints.
RowConstraints constraints =>
Lens' constraints (Set (RowConstraintsKey constraints))
forbidden forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall m. Contains m => Index m -> Lens' m Bool
contains RowConstraintsKey (TypeConstraintsOf rowTyp)
h = forall a. Maybe a
Nothing
    | Bool
otherwise =
        forall key (val :: HyperType) (rest :: HyperType)
       (h :: AHyperType).
key -> (h :# val) -> (h :# rest) -> RowExtend key val rest h
RowExtend
            RowConstraintsKey (TypeConstraintsOf rowTyp)
h
            (forall (h :: HyperType) (ast :: AHyperType).
TypeConstraintsOf (GetHyperType ast)
-> h ast -> WithConstraint h ast
WithConstraint (TypeConstraintsOf rowTyp
c forall a b. a -> (a -> b) -> b
& forall constraints.
RowConstraints constraints =>
Lens' constraints (Set (RowConstraintsKey constraints))
forbidden forall s t a b. ASetter s t a b -> b -> s -> t
.~ forall a. Monoid a => a
mempty forall a b. a -> (a -> b) -> b
& TypeConstraintsOf rowTyp -> TypeConstraintsOf valTyp
toChildC) 'AHyperType h :# valTyp
v)
            (forall (h :: HyperType) (ast :: AHyperType).
TypeConstraintsOf (GetHyperType ast)
-> h ast -> WithConstraint h ast
WithConstraint (TypeConstraintsOf rowTyp
c forall a b. a -> (a -> b) -> b
& forall constraints.
RowConstraints constraints =>
Lens' constraints (Set (RowConstraintsKey constraints))
forbidden forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall m. Contains m => Index m -> Lens' m Bool
contains RowConstraintsKey (TypeConstraintsOf rowTyp)
h forall s t a b. ASetter s t a b -> b -> s -> t
.~ Bool
True) 'AHyperType h :# rowTyp
rest)
            forall a b. a -> (a -> b) -> b
& forall a. a -> Maybe a
Just

{-# INLINE rowExtendStructureMismatch #-}
rowExtendStructureMismatch ::
    Ord key =>
    ( Unify m rowTyp
    , Unify m valTyp
    ) =>
    (forall c. Unify m c => UVarOf m # c -> UVarOf m # c -> m (UVarOf m # c)) ->
    Prism' (rowTyp # UVarOf m) (RowExtend key valTyp rowTyp # UVarOf m) ->
    RowExtend key valTyp rowTyp # UVarOf m ->
    RowExtend key valTyp rowTyp # UVarOf m ->
    m ()
rowExtendStructureMismatch :: forall key (m :: * -> *) (rowTyp :: HyperType)
       (valTyp :: HyperType).
(Ord key, Unify m rowTyp, Unify m valTyp) =>
(forall (c :: HyperType).
 Unify m c =>
 (UVarOf m # c) -> (UVarOf m # c) -> m (UVarOf m # c))
-> Prism'
     (rowTyp # UVarOf m) (RowExtend key valTyp rowTyp # UVarOf m)
-> (RowExtend key valTyp rowTyp # UVarOf m)
-> (RowExtend key valTyp rowTyp # UVarOf m)
-> m ()
rowExtendStructureMismatch forall (c :: HyperType).
Unify m c =>
(UVarOf m # c) -> (UVarOf m # c) -> m (UVarOf m # c)
match Prism' (rowTyp # UVarOf m) (RowExtend key valTyp rowTyp # UVarOf m)
extend RowExtend key valTyp rowTyp # UVarOf m
r0 RowExtend key valTyp rowTyp # UVarOf m
r1 =
    do
        FlatRowExtends key valTyp rowTyp # UVarOf m
flat0 <- forall key (m :: * -> *) (v :: HyperType) (rest :: HyperType)
       (val :: HyperType).
(Ord key, Monad m) =>
((v # rest) -> m (Maybe (RowExtend key val rest # v)))
-> (RowExtend key val rest # v)
-> m (FlatRowExtends key val rest # v)
flattenRowExtend (UVarOf m # rowTyp)
-> m (Maybe (RowExtend key valTyp rowTyp # UVarOf m))
nextExtend RowExtend key valTyp rowTyp # UVarOf m
r0
        FlatRowExtends key valTyp rowTyp # UVarOf m
flat1 <- forall key (m :: * -> *) (v :: HyperType) (rest :: HyperType)
       (val :: HyperType).
(Ord key, Monad m) =>
((v # rest) -> m (Maybe (RowExtend key val rest # v)))
-> (RowExtend key val rest # v)
-> m (FlatRowExtends key val rest # v)
flattenRowExtend (UVarOf m # rowTyp)
-> m (Maybe (RowExtend key valTyp rowTyp # UVarOf m))
nextExtend RowExtend key valTyp rowTyp # UVarOf m
r1
        forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
Map.intersectionWith forall (c :: HyperType).
Unify m c =>
(UVarOf m # c) -> (UVarOf m # c) -> m (UVarOf m # c)
match (FlatRowExtends key valTyp rowTyp # UVarOf m
flat0 forall s a. s -> Getting a s a -> a
^. forall key (val :: HyperType) (rest :: HyperType) (h :: AHyperType)
       key (val :: HyperType).
Lens
  (FlatRowExtends key val rest h)
  (FlatRowExtends key val rest h)
  (Map key (h :# val))
  (Map key (h :# val))
freExtends) (FlatRowExtends key valTyp rowTyp # UVarOf m
flat1 forall s a. s -> Getting a s a -> a
^. forall key (val :: HyperType) (rest :: HyperType) (h :: AHyperType)
       key (val :: HyperType).
Lens
  (FlatRowExtends key val rest h)
  (FlatRowExtends key val rest h)
  (Map key (h :# val))
  (Map key (h :# val))
freExtends)
            forall a b. a -> (a -> b) -> b
& forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Applicative f) =>
t (f a) -> f ()
sequenceA_
        UVarOf m # rowTyp
restVar <- forall (v :: HyperType) (ast :: AHyperType).
TypeConstraintsOf (GetHyperType ast) -> UTerm v ast
UUnbound forall a. Monoid a => a
mempty forall a b. a -> (a -> b) -> b
& forall (v :: HyperType) (m :: * -> *) (t :: HyperType).
BindingDict v m t -> (UTerm v # t) -> m (v # t)
newVar forall (m :: * -> *) (t :: HyperType).
Unify m t =>
BindingDict (UVarOf m) m t
binding
        let side :: (FlatRowExtends key valTyp rowTyp # UVarOf m)
-> (FlatRowExtends key valTyp rowTyp # UVarOf m)
-> m (UVarOf m # rowTyp)
side FlatRowExtends key valTyp rowTyp # UVarOf m
x FlatRowExtends key valTyp rowTyp # UVarOf m
y =
                forall (m :: * -> *) key (val :: HyperType) (rest :: HyperType)
       (v :: HyperType).
Monad m =>
((RowExtend key val rest # v) -> m (v # rest))
-> (FlatRowExtends key val rest # v) -> m (v # rest)
unflattenRow
                    (RowExtend key valTyp rowTyp # UVarOf m) -> m (UVarOf m # rowTyp)
mkExtend
                    FlatRowExtends
                        { _freExtends :: Map key ('AHyperType (UVarOf m) :# valTyp)
_freExtends =
                            (FlatRowExtends key valTyp rowTyp # UVarOf m
x forall s a. s -> Getting a s a -> a
^. forall key (val :: HyperType) (rest :: HyperType) (h :: AHyperType)
       key (val :: HyperType).
Lens
  (FlatRowExtends key val rest h)
  (FlatRowExtends key val rest h)
  (Map key (h :# val))
  (Map key (h :# val))
freExtends) forall k a b. Ord k => Map k a -> Map k b -> Map k a
`Map.difference` (FlatRowExtends key valTyp rowTyp # UVarOf m
y forall s a. s -> Getting a s a -> a
^. forall key (val :: HyperType) (rest :: HyperType) (h :: AHyperType)
       key (val :: HyperType).
Lens
  (FlatRowExtends key val rest h)
  (FlatRowExtends key val rest h)
  (Map key (h :# val))
  (Map key (h :# val))
freExtends)
                        , _freRest :: 'AHyperType (UVarOf m) :# rowTyp
_freRest = UVarOf m # rowTyp
restVar
                        }
                    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (c :: HyperType).
Unify m c =>
(UVarOf m # c) -> (UVarOf m # c) -> m (UVarOf m # c)
match (FlatRowExtends key valTyp rowTyp # UVarOf m
y forall s a. s -> Getting a s a -> a
^. forall key (val :: HyperType) (rest :: HyperType) (h :: AHyperType)
       (rest :: HyperType).
Lens
  (FlatRowExtends key val rest h)
  (FlatRowExtends key val rest h)
  (h :# rest)
  (h :# rest)
freRest)
        UVarOf m # rowTyp
_ <- (FlatRowExtends key valTyp rowTyp # UVarOf m)
-> (FlatRowExtends key valTyp rowTyp # UVarOf m)
-> m (UVarOf m # rowTyp)
side FlatRowExtends key valTyp rowTyp # UVarOf m
flat0 FlatRowExtends key valTyp rowTyp # UVarOf m
flat1
        UVarOf m # rowTyp
_ <- (FlatRowExtends key valTyp rowTyp # UVarOf m)
-> (FlatRowExtends key valTyp rowTyp # UVarOf m)
-> m (UVarOf m # rowTyp)
side FlatRowExtends key valTyp rowTyp # UVarOf m
flat1 FlatRowExtends key valTyp rowTyp # UVarOf m
flat0
        forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    where
        mkExtend :: (RowExtend key valTyp rowTyp # UVarOf m) -> m (UVarOf m # rowTyp)
mkExtend RowExtend key valTyp rowTyp # UVarOf m
ext = forall (v :: HyperType) (ast :: AHyperType).
TypeConstraintsOf (GetHyperType ast)
-> (ast :# v) -> UTermBody v ast
UTermBody forall a. Monoid a => a
mempty (Prism' (rowTyp # UVarOf m) (RowExtend key valTyp rowTyp # UVarOf m)
extend forall t b. AReview t b -> b -> t
# RowExtend key valTyp rowTyp # UVarOf m
ext) forall a b. a -> (a -> b) -> b
& forall (v :: HyperType) (ast :: AHyperType).
UTermBody v ast -> UTerm v ast
UTerm forall a b. a -> (a -> b) -> b
& forall (v :: HyperType) (m :: * -> *) (t :: HyperType).
BindingDict v m t -> (UTerm v # t) -> m (v # t)
newVar forall (m :: * -> *) (t :: HyperType).
Unify m t =>
BindingDict (UVarOf m) m t
binding
        nextExtend :: (UVarOf m # rowTyp)
-> m (Maybe (RowExtend key valTyp rowTyp # UVarOf m))
nextExtend UVarOf m # rowTyp
v = forall (m :: * -> *) (t :: HyperType).
Unify m t =>
(UVarOf m # t) -> m (UVarOf m # t, UTerm (UVarOf m) # t)
semiPruneLookup UVarOf m # rowTyp
v forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (forall s a. s -> Getting (First a) s a -> Maybe a
^? forall s t a b. Field2 s t a b => Lens s t a b
Lens._2 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (v :: HyperType) (ast :: AHyperType).
Prism' (UTerm v ast) (UTermBody v ast)
_UTerm forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (v1 :: HyperType) (ast :: AHyperType) (v2 :: HyperType).
Lens (UTermBody v1 ast) (UTermBody v2 ast) (ast :# v1) (ast :# v2)
uBody forall b c a. (b -> c) -> (a -> b) -> a -> c
. Prism' (rowTyp # UVarOf m) (RowExtend key valTyp rowTyp # UVarOf m)
extend)

-- Helper for infering row usages of a row element,
-- such as getting a field from a record or injecting into a sum type.
-- Returns a unification variable for the element and for the whole row.
{-# INLINE rowElementInfer #-}
rowElementInfer ::
    forall m valTyp rowTyp.
    ( UnifyGen m valTyp
    , UnifyGen m rowTyp
    , RowConstraints (TypeConstraintsOf rowTyp)
    ) =>
    (RowExtend (RowKey rowTyp) valTyp rowTyp # UVarOf m -> rowTyp # UVarOf m) ->
    RowKey rowTyp ->
    m (UVarOf m # valTyp, UVarOf m # rowTyp)
rowElementInfer :: forall (m :: * -> *) (valTyp :: HyperType) (rowTyp :: HyperType).
(UnifyGen m valTyp, UnifyGen m rowTyp,
 RowConstraints (TypeConstraintsOf rowTyp)) =>
((RowExtend (RowKey rowTyp) valTyp rowTyp # UVarOf m)
 -> rowTyp # UVarOf m)
-> RowKey rowTyp -> m (UVarOf m # valTyp, UVarOf m # rowTyp)
rowElementInfer (RowExtend
   (RowConstraintsKey (TypeConstraintsOf rowTyp)) valTyp rowTyp
 # UVarOf m)
-> rowTyp # UVarOf m
extendToRow RowConstraintsKey (TypeConstraintsOf rowTyp)
h =
    do
        UVarOf m # rowTyp
restVar <-
            forall (m :: * -> *) (t :: HyperType).
UnifyGen m t =>
Proxy t -> m (TypeConstraintsOf t)
scopeConstraints (forall {k} (t :: k). Proxy t
Proxy @rowTyp)
                forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (v :: HyperType) (m :: * -> *) (t :: HyperType).
BindingDict v m t -> (UTerm v # t) -> m (v # t)
newVar forall (m :: * -> *) (t :: HyperType).
Unify m t =>
BindingDict (UVarOf m) m t
binding forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (v :: HyperType) (ast :: AHyperType).
TypeConstraintsOf (GetHyperType ast) -> UTerm v ast
UUnbound forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall constraints.
RowConstraints constraints =>
Lens' constraints (Set (RowConstraintsKey constraints))
forbidden forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall m. Contains m => Index m -> Lens' m Bool
contains RowConstraintsKey (TypeConstraintsOf rowTyp)
h forall s t a b. ASetter s t a b -> b -> s -> t
.~ Bool
True)
        UVarOf m # valTyp
part <- forall (m :: * -> *) (t :: HyperType).
UnifyGen m t =>
m (UVarOf m # t)
newUnbound
        UVarOf m # rowTyp
whole <- forall key (val :: HyperType) (rest :: HyperType)
       (h :: AHyperType).
key -> (h :# val) -> (h :# rest) -> RowExtend key val rest h
RowExtend RowConstraintsKey (TypeConstraintsOf rowTyp)
h UVarOf m # valTyp
part UVarOf m # rowTyp
restVar forall a b. a -> (a -> b) -> b
& (RowExtend
   (RowConstraintsKey (TypeConstraintsOf rowTyp)) valTyp rowTyp
 # UVarOf m)
-> rowTyp # UVarOf m
extendToRow forall a b. a -> (a -> b) -> b
& forall (m :: * -> *) (t :: HyperType).
UnifyGen m t =>
(t # UVarOf m) -> m (UVarOf m # t)
newTerm
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (UVarOf m # valTyp
part, UVarOf m # rowTyp
whole)