{-# LANGUAGE FlexibleContexts #-}
module Hyper.Class.Unify
( Unify(..), UVarOf
, UnifyGen(..)
, BindingDict(..)
, applyBindings, semiPruneLookup, occursError
) where
import Control.Monad (unless)
import Control.Monad.Error.Class (MonadError(..))
import Control.Monad.Trans.Class (MonadTrans(..))
import Control.Monad.Trans.State (runStateT, get, put)
import Data.Kind (Type)
import Hyper.Class.Nodes (HNodes(..), (#>))
import Hyper.Class.Optic (HSubset(..), HSubset')
import Hyper.Class.Recursive
import Hyper.Class.Traversable (htraverse)
import Hyper.Class.ZipMatch (ZipMatch)
import Hyper.Type (HyperType, type (#))
import Hyper.Type.Pure (Pure, _Pure)
import Hyper.Unify.Constraints
import Hyper.Unify.Error (UnifyError(..))
import Hyper.Unify.QuantifiedVar (MonadQuantify(..), HasQuantifiedVar(..))
import Hyper.Unify.Term (UTerm(..), UTermBody(..), uBody)
import Hyper.Internal.Prelude
type family UVarOf (m :: Type -> Type) :: HyperType
data BindingDict v m t = BindingDict
{ BindingDict v m t -> (v # t) -> m (UTerm v # t)
lookupVar :: !(v # t -> m (UTerm v # t))
, BindingDict v m t -> (UTerm v # t) -> m (v # t)
newVar :: !(UTerm v # t -> m (v # t))
, BindingDict v m t -> (v # t) -> (UTerm v # t) -> m ()
bindVar :: !(v # t -> UTerm v # t -> m ())
}
class
( Eq (UVarOf m # t)
, RTraversable t
, ZipMatch t
, HasTypeConstraints t
, HasQuantifiedVar t
, Monad m
, MonadQuantify (TypeConstraintsOf t) (QVar t) m
) => Unify m t where
binding :: BindingDict (UVarOf m) m t
unifyError :: UnifyError t # UVarOf m -> m a
default unifyError ::
(MonadError (e # Pure) m, HSubset' e (UnifyError t)) =>
UnifyError t # UVarOf m -> m a
unifyError UnifyError t # UVarOf m
e =
Dict (HNodesConstraint t (Unify m))
-> (HNodesConstraint t (Unify m) => m a) -> m a
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (Proxy m -> Proxy t -> Dict (HNodesConstraint t (Unify m))
forall (m :: * -> *) (t :: HyperType).
Unify m t =>
Proxy m -> Proxy t -> Dict (HNodesConstraint t (Unify m))
unifyRecursive (Proxy m
forall k (t :: k). Proxy t
Proxy @m) (Proxy t
forall k (t :: k). Proxy t
Proxy @t)) ((HNodesConstraint t (Unify m) => m a) -> m a)
-> (HNodesConstraint t (Unify m) => m a) -> m a
forall a b. (a -> b) -> a -> b
$
(forall (n :: HyperType).
HWitness (UnifyError t) n -> (UVarOf m # n) -> m (Pure # n))
-> (UnifyError t # UVarOf m) -> m (UnifyError t # Pure)
forall (f :: * -> *) (h :: HyperType) (p :: HyperType)
(q :: HyperType).
(Applicative f, HTraversable h) =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> f (q # n))
-> (h # p) -> f (h # q)
htraverse (Proxy (Unify m)
forall k (t :: k). Proxy t
Proxy @(Unify m) Proxy (Unify m)
-> (Unify m n => (UVarOf m # n) -> m (Pure # n))
-> HWitness (UnifyError t) n
-> (UVarOf m # n)
-> m (Pure # n)
forall (h :: HyperType) (c :: HyperType -> Constraint)
(n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> Unify m n => (UVarOf m # n) -> m (Pure # n)
forall (m :: * -> *) (t :: HyperType).
Unify m t =>
(UVarOf m # t) -> m (Pure # t)
applyBindings) UnifyError t # UVarOf m
e
m (UnifyError t # Pure) -> ((UnifyError t # Pure) -> m a) -> m a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (e # Pure) -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ((e # Pure) -> m a)
-> ((UnifyError t # Pure) -> e # Pure)
-> (UnifyError t # Pure)
-> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Tagged (UnifyError t # Pure) (Identity (UnifyError t # Pure))
-> Tagged (e # Pure) (Identity (e # Pure))
forall (s :: HyperType) (t :: HyperType) (a :: HyperType)
(b :: HyperType) (h :: HyperType).
HSubset s t a b =>
Prism (s # h) (t # h) (a # h) (b # h)
hSubset (Tagged (UnifyError t # Pure) (Identity (UnifyError t # Pure))
-> Tagged (e # Pure) (Identity (e # Pure)))
-> (UnifyError t # Pure) -> e # Pure
forall t b. AReview t b -> b -> t
#)
structureMismatch ::
(forall c. Unify m c => UVarOf m # c -> UVarOf m # c -> m (UVarOf m # c)) ->
t # UVarOf m -> t # UVarOf m -> m ()
structureMismatch forall (c :: HyperType).
Unify m c =>
(UVarOf m # c) -> (UVarOf m # c) -> m (UVarOf m # c)
_ t # UVarOf m
x t # UVarOf m
y = (UnifyError t # UVarOf m) -> m ()
forall (m :: * -> *) (t :: HyperType) a.
Unify m t =>
(UnifyError t # UVarOf m) -> m a
unifyError ((t # UVarOf m) -> (t # UVarOf m) -> UnifyError t # UVarOf m
forall (t :: HyperType) (h :: AHyperType).
t h -> t h -> UnifyError t h
Mismatch t # UVarOf m
x t # UVarOf m
y)
unifyRecursive :: Proxy m -> Proxy t -> Dict (HNodesConstraint t (Unify m))
{-# INLINE unifyRecursive #-}
default unifyRecursive ::
HNodesConstraint t (Unify m) =>
Proxy m -> Proxy t -> Dict (HNodesConstraint t (Unify m))
unifyRecursive Proxy m
_ Proxy t
_ = Dict (HNodesConstraint t (Unify m))
forall (a :: Constraint). a => Dict a
Dict
instance Recursive (Unify m) where
{-# INLINE recurse #-}
recurse :: proxy (Unify m h) -> Dict (HNodesConstraint h (Unify m))
recurse = Proxy m -> Proxy h -> Dict (HNodesConstraint h (Unify m))
forall (m :: * -> *) (t :: HyperType).
Unify m t =>
Proxy m -> Proxy t -> Dict (HNodesConstraint t (Unify m))
unifyRecursive (Proxy m
forall k (t :: k). Proxy t
Proxy @m) (Proxy h -> Dict (HNodesConstraint h (Unify m)))
-> (proxy (Unify m h) -> Proxy h)
-> proxy (Unify m h)
-> Dict (HNodesConstraint h (Unify m))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. proxy (Unify m h) -> Proxy h
forall (proxy :: Constraint -> *) (f :: HyperType -> Constraint)
(h :: HyperType).
proxy (f h) -> Proxy h
proxyArgument
class Unify m t => UnifyGen m t where
scopeConstraints :: Proxy t -> m (TypeConstraintsOf t)
unifyGenRecursive :: Proxy m -> Proxy t -> Dict (HNodesConstraint t (UnifyGen m))
{-# INLINE unifyGenRecursive #-}
default unifyGenRecursive ::
HNodesConstraint t (UnifyGen m) =>
Proxy m -> Proxy t -> Dict (HNodesConstraint t (UnifyGen m))
unifyGenRecursive Proxy m
_ Proxy t
_ = Dict (HNodesConstraint t (UnifyGen m))
forall (a :: Constraint). a => Dict a
Dict
instance Recursive (UnifyGen m) where
{-# INLINE recurse #-}
recurse :: proxy (UnifyGen m h) -> Dict (HNodesConstraint h (UnifyGen m))
recurse = Proxy m -> Proxy h -> Dict (HNodesConstraint h (UnifyGen m))
forall (m :: * -> *) (t :: HyperType).
UnifyGen m t =>
Proxy m -> Proxy t -> Dict (HNodesConstraint t (UnifyGen m))
unifyGenRecursive (Proxy m
forall k (t :: k). Proxy t
Proxy @m) (Proxy h -> Dict (HNodesConstraint h (UnifyGen m)))
-> (proxy (UnifyGen m h) -> Proxy h)
-> proxy (UnifyGen m h)
-> Dict (HNodesConstraint h (UnifyGen m))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. proxy (UnifyGen m h) -> Proxy h
forall (proxy :: Constraint -> *) (f :: HyperType -> Constraint)
(h :: HyperType).
proxy (f h) -> Proxy h
proxyArgument
{-# INLINE semiPruneLookup #-}
semiPruneLookup ::
Unify m t =>
UVarOf m # t ->
m (UVarOf m # t, UTerm (UVarOf m) # t)
semiPruneLookup :: (UVarOf m # t) -> m (UVarOf m # t, UTerm (UVarOf m) # t)
semiPruneLookup UVarOf m # t
v0 =
BindingDict (UVarOf m) m t
-> (UVarOf m # t) -> m (UTerm (UVarOf m) # t)
forall (v :: HyperType) (m :: * -> *) (t :: HyperType).
BindingDict v m t -> (v # t) -> m (UTerm v # t)
lookupVar BindingDict (UVarOf m) m t
forall (m :: * -> *) (t :: HyperType).
Unify m t =>
BindingDict (UVarOf m) m t
binding UVarOf m # t
v0
m (UTerm (UVarOf m) # t)
-> ((UTerm (UVarOf m) # t)
-> m (UVarOf m # t, UTerm (UVarOf m) # t))
-> m (UVarOf m # t, UTerm (UVarOf m) # t)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
\case
UToVar UVarOf m # t
v1 ->
do
(UVarOf m # t
v, UTerm (UVarOf m) # t
r) <- (UVarOf m # t) -> m (UVarOf m # t, UTerm (UVarOf m) # t)
forall (m :: * -> *) (t :: HyperType).
Unify m t =>
(UVarOf m # t) -> m (UVarOf m # t, UTerm (UVarOf m) # t)
semiPruneLookup UVarOf m # t
v1
BindingDict (UVarOf m) m t
-> (UVarOf m # t) -> (UTerm (UVarOf m) # t) -> m ()
forall (v :: HyperType) (m :: * -> *) (t :: HyperType).
BindingDict v m t -> (v # t) -> (UTerm v # t) -> m ()
bindVar BindingDict (UVarOf m) m t
forall (m :: * -> *) (t :: HyperType).
Unify m t =>
BindingDict (UVarOf m) m t
binding UVarOf m # t
v0 ((UVarOf m # t) -> UTerm (UVarOf m) # t
forall (v :: HyperType) (ast :: AHyperType). v ast -> UTerm v ast
UToVar UVarOf m # t
v)
(UVarOf m # t, UTerm (UVarOf m) # t)
-> m (UVarOf m # t, UTerm (UVarOf m) # t)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UVarOf m # t
v, UTerm (UVarOf m) # t
r)
UTerm (UVarOf m) # t
t -> (UVarOf m # t, UTerm (UVarOf m) # t)
-> m (UVarOf m # t, UTerm (UVarOf m) # t)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UVarOf m # t
v0, UTerm (UVarOf m) # t
t)
{-# INLINE applyBindings #-}
applyBindings ::
forall m t.
Unify m t =>
UVarOf m # t ->
m (Pure # t)
applyBindings :: (UVarOf m # t) -> m (Pure # t)
applyBindings UVarOf m # t
v0 =
(UVarOf m # t)
-> m (UVarOf m # t, UTerm (UVarOf m) ('AHyperType t))
forall (m :: * -> *) (t :: HyperType).
Unify m t =>
(UVarOf m # t) -> m (UVarOf m # t, UTerm (UVarOf m) # t)
semiPruneLookup UVarOf m # t
v0
m (UVarOf m # t, UTerm (UVarOf m) ('AHyperType t))
-> ((UVarOf m # t, UTerm (UVarOf m) ('AHyperType t))
-> m (Pure # t))
-> m (Pure # t)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
\(UVarOf m # t
v1, UTerm (UVarOf m) ('AHyperType t)
x) ->
let result :: (Pure # t) -> m (Pure # t)
result Pure # t
r = Pure # t
r (Pure # t) -> m () -> m (Pure # t)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ BindingDict (UVarOf m) m t
-> (UVarOf m # t) -> UTerm (UVarOf m) ('AHyperType t) -> m ()
forall (v :: HyperType) (m :: * -> *) (t :: HyperType).
BindingDict v m t -> (v # t) -> (UTerm v # t) -> m ()
bindVar BindingDict (UVarOf m) m t
forall (m :: * -> *) (t :: HyperType).
Unify m t =>
BindingDict (UVarOf m) m t
binding UVarOf m # t
v1 ((Pure # t) -> UTerm (UVarOf m) ('AHyperType t)
forall (v :: HyperType) (ast :: AHyperType).
Pure ast -> UTerm v ast
UResolved Pure # t
r)
quantify :: TypeConstraintsOf t -> m (Pure # t)
quantify TypeConstraintsOf t
c =
TypeConstraintsOf t -> m (QVar t)
forall typeConstraints q (m :: * -> *).
MonadQuantify typeConstraints q m =>
typeConstraints -> m q
newQuantifiedVariable TypeConstraintsOf t
c m (QVar t) -> (QVar t -> Pure # t) -> m (Pure # t)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (Tagged (t # Pure) (Identity (t # Pure))
-> Tagged (Pure # t) (Identity (Pure # t))
forall (h :: HyperType) (j :: HyperType).
Iso (Pure # h) (Pure # j) (h # Pure) (j # Pure)
_Pure (Tagged (t # Pure) (Identity (t # Pure))
-> Tagged (Pure # t) (Identity (Pure # t)))
-> (Tagged (QVar t) (Identity (QVar t))
-> Tagged (t # Pure) (Identity (t # Pure)))
-> Tagged (QVar t) (Identity (QVar t))
-> Tagged (Pure # t) (Identity (Pure # t))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tagged (QVar t) (Identity (QVar t))
-> Tagged (t # Pure) (Identity (t # Pure))
forall (t :: HyperType) (f :: AHyperType).
HasQuantifiedVar t =>
Prism' (t f) (QVar t)
quantifiedVar (Tagged (QVar t) (Identity (QVar t))
-> Tagged (Pure # t) (Identity (Pure # t)))
-> QVar t -> Pure # t
forall t b. AReview t b -> b -> t
#)
m (Pure # t) -> ((Pure # t) -> m (Pure # t)) -> m (Pure # t)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (Pure # t) -> m (Pure # t)
result
in
case UTerm (UVarOf m) ('AHyperType t)
x of
UResolving UTermBody (UVarOf m) ('AHyperType t)
t -> (UVarOf m # t)
-> UTermBody (UVarOf m) ('AHyperType t) -> m (Pure # t)
forall (m :: * -> *) (t :: HyperType) a.
Unify m t =>
(UVarOf m # t) -> (UTermBody (UVarOf m) # t) -> m a
occursError UVarOf m # t
v1 UTermBody (UVarOf m) ('AHyperType t)
t
UResolved Pure # t
t -> (Pure # t) -> m (Pure # t)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Pure # t
t
UUnbound TypeConstraintsOf (GetHyperType ('AHyperType t))
c -> TypeConstraintsOf t -> m (Pure # t)
quantify TypeConstraintsOf t
TypeConstraintsOf (GetHyperType ('AHyperType t))
c
USkolem TypeConstraintsOf (GetHyperType ('AHyperType t))
c -> TypeConstraintsOf t -> m (Pure # t)
quantify TypeConstraintsOf t
TypeConstraintsOf (GetHyperType ('AHyperType t))
c
UTerm UTermBody (UVarOf m) ('AHyperType t)
b ->
do
(t # Pure
r, Bool
anyChild) <-
Dict (HNodesConstraint t (Unify m))
-> (HNodesConstraint t (Unify m) => m (t # Pure, Bool))
-> m (t # Pure, Bool)
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (Proxy m -> Proxy t -> Dict (HNodesConstraint t (Unify m))
forall (m :: * -> *) (t :: HyperType).
Unify m t =>
Proxy m -> Proxy t -> Dict (HNodesConstraint t (Unify m))
unifyRecursive (Proxy m
forall k (t :: k). Proxy t
Proxy @m) (Proxy t
forall k (t :: k). Proxy t
Proxy @t)) ((HNodesConstraint t (Unify m) => m (t # Pure, Bool))
-> m (t # Pure, Bool))
-> (HNodesConstraint t (Unify m) => m (t # Pure, Bool))
-> m (t # Pure, Bool)
forall a b. (a -> b) -> a -> b
$
(forall (n :: HyperType).
HWitness t n -> (UVarOf m # n) -> StateT Bool m (Pure # n))
-> (t # UVarOf m) -> StateT Bool m (t # Pure)
forall (f :: * -> *) (h :: HyperType) (p :: HyperType)
(q :: HyperType).
(Applicative f, HTraversable h) =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> f (q # n))
-> (h # p) -> f (h # q)
htraverse
( Proxy (Unify m)
forall k (t :: k). Proxy t
Proxy @(Unify m) Proxy (Unify m)
-> (Unify m n => (UVarOf m # n) -> StateT Bool m (Pure # n))
-> HWitness t n
-> (UVarOf m # n)
-> StateT Bool m (Pure # n)
forall (h :: HyperType) (c :: HyperType -> Constraint)
(n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#>
\UVarOf m # n
c ->
do
StateT Bool m Bool
forall (m :: * -> *) s. Monad m => StateT s m s
get StateT Bool m Bool
-> (Bool -> StateT Bool m ()) -> StateT Bool m ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= m () -> StateT Bool m ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> StateT Bool m ())
-> (Bool -> m ()) -> Bool -> StateT Bool m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
`unless` BindingDict (UVarOf m) m t
-> (UVarOf m # t) -> UTerm (UVarOf m) ('AHyperType t) -> m ()
forall (v :: HyperType) (m :: * -> *) (t :: HyperType).
BindingDict v m t -> (v # t) -> (UTerm v # t) -> m ()
bindVar BindingDict (UVarOf m) m t
forall (m :: * -> *) (t :: HyperType).
Unify m t =>
BindingDict (UVarOf m) m t
binding UVarOf m # t
v1 (UTermBody (UVarOf m) ('AHyperType t)
-> UTerm (UVarOf m) ('AHyperType t)
forall (v :: HyperType) (ast :: AHyperType).
UTermBody v ast -> UTerm v ast
UResolving UTermBody (UVarOf m) ('AHyperType t)
b))
Bool -> StateT Bool m ()
forall (m :: * -> *) s. Monad m => s -> StateT s m ()
put Bool
True
(UVarOf m # n) -> m (Pure # n)
forall (m :: * -> *) (t :: HyperType).
Unify m t =>
(UVarOf m # t) -> m (Pure # t)
applyBindings UVarOf m # n
c m (Pure # n)
-> (m (Pure # n) -> StateT Bool m (Pure # n))
-> StateT Bool m (Pure # n)
forall a b. a -> (a -> b) -> b
& m (Pure # n) -> StateT Bool m (Pure # n)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift
) (UTermBody (UVarOf m) ('AHyperType t)
b UTermBody (UVarOf m) ('AHyperType t)
-> Getting
(t # UVarOf m)
(UTermBody (UVarOf m) ('AHyperType t))
(t # UVarOf m)
-> t # UVarOf m
forall s a. s -> Getting a s a -> a
^. Getting
(t # UVarOf m)
(UTermBody (UVarOf m) ('AHyperType t))
(t # UVarOf m)
forall (v1 :: HyperType) (ast :: AHyperType) (v2 :: HyperType).
Lens (UTermBody v1 ast) (UTermBody v2 ast) (ast :# v1) (ast :# v2)
uBody)
StateT Bool m (t # Pure)
-> (StateT Bool m (t # Pure) -> m (t # Pure, Bool))
-> m (t # Pure, Bool)
forall a b. a -> (a -> b) -> b
& (StateT Bool m (t # Pure) -> Bool -> m (t # Pure, Bool)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
`runStateT` Bool
False)
Tagged (t # Pure) (Identity (t # Pure))
-> Tagged (Pure # t) (Identity (Pure # t))
forall (h :: HyperType) (j :: HyperType).
Iso (Pure # h) (Pure # j) (h # Pure) (j # Pure)
_Pure (Tagged (t # Pure) (Identity (t # Pure))
-> Tagged (Pure # t) (Identity (Pure # t)))
-> (t # Pure) -> Pure # t
forall t b. AReview t b -> b -> t
# t # Pure
r (Pure # t) -> ((Pure # t) -> m (Pure # t)) -> m (Pure # t)
forall a b. a -> (a -> b) -> b
& if Bool
anyChild then (Pure # t) -> m (Pure # t)
result else (Pure # t) -> m (Pure # t)
forall (f :: * -> *) a. Applicative f => a -> f a
pure
UToVar{} -> [Char] -> m (Pure # t)
forall a. HasCallStack => [Char] -> a
error [Char]
"lookup not expected to result in var"
UConverted{} -> [Char] -> m (Pure # t)
forall a. HasCallStack => [Char] -> a
error [Char]
"conversion state not expected in applyBindings"
UInstantiated{} ->
TypeConstraintsOf t -> m (Pure # t)
quantify TypeConstraintsOf t
forall a. Monoid a => a
mempty
occursError ::
Unify m t =>
UVarOf m # t -> UTermBody (UVarOf m) # t -> m a
occursError :: (UVarOf m # t) -> (UTermBody (UVarOf m) # t) -> m a
occursError UVarOf m # t
v (UTermBody TypeConstraintsOf (GetHyperType ('AHyperType t))
c 'AHyperType t :# UVarOf m
b) =
do
QVar t
q <- TypeConstraintsOf t -> m (QVar t)
forall typeConstraints q (m :: * -> *).
MonadQuantify typeConstraints q m =>
typeConstraints -> m q
newQuantifiedVariable TypeConstraintsOf t
TypeConstraintsOf (GetHyperType ('AHyperType t))
c
BindingDict (UVarOf m) m t
-> (UVarOf m # t) -> (UTerm (UVarOf m) # t) -> m ()
forall (v :: HyperType) (m :: * -> *) (t :: HyperType).
BindingDict v m t -> (v # t) -> (UTerm v # t) -> m ()
bindVar BindingDict (UVarOf m) m t
forall (m :: * -> *) (t :: HyperType).
Unify m t =>
BindingDict (UVarOf m) m t
binding UVarOf m # t
v (Pure ('AHyperType t) -> UTerm (UVarOf m) # t
forall (v :: HyperType) (ast :: AHyperType).
Pure ast -> UTerm v ast
UResolved (Tagged (t # Pure) (Identity (t # Pure))
-> Tagged (Pure ('AHyperType t)) (Identity (Pure ('AHyperType t)))
forall (h :: HyperType) (j :: HyperType).
Iso (Pure # h) (Pure # j) (h # Pure) (j # Pure)
_Pure (Tagged (t # Pure) (Identity (t # Pure))
-> Tagged (Pure ('AHyperType t)) (Identity (Pure ('AHyperType t))))
-> (Tagged (QVar t) (Identity (QVar t))
-> Tagged (t # Pure) (Identity (t # Pure)))
-> Tagged (QVar t) (Identity (QVar t))
-> Tagged (Pure ('AHyperType t)) (Identity (Pure ('AHyperType t)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tagged (QVar t) (Identity (QVar t))
-> Tagged (t # Pure) (Identity (t # Pure))
forall (t :: HyperType) (f :: AHyperType).
HasQuantifiedVar t =>
Prism' (t f) (QVar t)
quantifiedVar (Tagged (QVar t) (Identity (QVar t))
-> Tagged (Pure ('AHyperType t)) (Identity (Pure ('AHyperType t))))
-> QVar t -> Pure ('AHyperType t)
forall t b. AReview t b -> b -> t
# QVar t
q))
(UnifyError t # UVarOf m) -> m a
forall (m :: * -> *) (t :: HyperType) a.
Unify m t =>
(UnifyError t # UVarOf m) -> m a
unifyError (t ('AHyperType (UVarOf m))
-> t ('AHyperType (UVarOf m)) -> UnifyError t # UVarOf m
forall (t :: HyperType) (h :: AHyperType).
t h -> t h -> UnifyError t h
Occurs (Tagged (QVar t) (Identity (QVar t))
-> Tagged
(t ('AHyperType (UVarOf m)))
(Identity (t ('AHyperType (UVarOf m))))
forall (t :: HyperType) (f :: AHyperType).
HasQuantifiedVar t =>
Prism' (t f) (QVar t)
quantifiedVar (Tagged (QVar t) (Identity (QVar t))
-> Tagged
(t ('AHyperType (UVarOf m)))
(Identity (t ('AHyperType (UVarOf m)))))
-> QVar t -> t ('AHyperType (UVarOf m))
forall t b. AReview t b -> b -> t
# QVar t
q) t ('AHyperType (UVarOf m))
'AHyperType t :# UVarOf m
b)