{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE UndecidableInstances #-}
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)
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
{-# 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)
{-# 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)