module PlutusCore.Generators.QuickCheck.Unification where
import PlutusPrelude
import PlutusCore.Generators.QuickCheck.Common
import PlutusCore.Generators.QuickCheck.GenerateTypes
import PlutusCore.Generators.QuickCheck.Substitutions
import PlutusCore.Generators.QuickCheck.Utils
import PlutusCore.Default
import PlutusCore.Name.Unique
import PlutusIR
import Control.Monad (when)
import Control.Monad.Except (MonadError, throwError)
import Control.Monad.Reader (ReaderT, ask, local, runReaderT)
import Control.Monad.State.Strict (StateT, execStateT, get, put)
import Data.Map.Strict.Internal qualified as Map
import Data.Set (Set)
import Data.Set qualified as Set
unificationFailure :: (MonadError String m, Pretty a, Pretty b) => a -> b -> m any
unificationFailure :: forall (m :: * -> *) a b any.
(MonadError String m, Pretty a, Pretty b) =>
a -> b -> m any
unificationFailure a
x b
y = String -> m any
forall a. String -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> m any) -> String -> m any
forall a b. (a -> b) -> a -> b
$ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[ String
"Failed to unify\n\n "
, a -> String
forall str a. (Pretty a, Render str) => a -> str
display a
x
, String
"\n\nand\n\n "
, b -> String
forall str a. (Pretty a, Render str) => a -> str
display b
y
, String
"\n\n"
]
resolutionFailure :: MonadError String m => TyName -> Type TyName DefaultUni () -> String -> m any
resolutionFailure :: forall (m :: * -> *) any.
MonadError String m =>
TyName -> Type TyName DefaultUni () -> String -> m any
resolutionFailure TyName
name1 Type TyName DefaultUni ()
ty2 String
reason = String -> m any
forall a. String -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> m any) -> String -> m any
forall a b. (a -> b) -> a -> b
$ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[ String
"Unification failure: cannot resolve '"
, TyName -> String
forall str a. (Pretty a, Render str) => a -> str
display TyName
name1
, String
" as\n\n "
, Type TyName DefaultUni () -> String
forall str a. (Pretty a, Render str) => a -> str
display Type TyName DefaultUni ()
ty2
, String
"\n\n because "
, String
reason
]
unifyType :: TypeCtx
-> Set TyName
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> Either String TypeSub
unifyType :: TypeCtx
-> Set TyName
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> Either String TypeSub
unifyType TypeCtx
ctx Set TyName
flex Type TyName DefaultUni ()
a0 Type TyName DefaultUni ()
b0 =
StateT TypeSub (Either String) ()
-> TypeSub -> Either String TypeSub
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT (ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
-> Set TyName -> StateT TypeSub (Either String) ()
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
goType (Type TyName DefaultUni () -> Type TyName DefaultUni ()
normalizeTy Type TyName DefaultUni ()
a0) (Type TyName DefaultUni () -> Type TyName DefaultUni ()
normalizeTy Type TyName DefaultUni ()
b0)) Set TyName
forall a. Set a
Set.empty) TypeSub
forall k a. Map k a
Map.empty
where
goTyName :: TyName
-> Type TyName DefaultUni ()
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
goTyName :: TyName
-> Type TyName DefaultUni ()
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
goTyName TyName
name1 Type TyName DefaultUni ()
ty2 =
Bool
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (() -> TyName -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
name1 Type TyName DefaultUni () -> Type TyName DefaultUni () -> Bool
forall a. Eq a => a -> a -> Bool
/= Type TyName DefaultUni ()
ty2) (ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ())
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
forall a b. (a -> b) -> a -> b
$ do
Set TyName
locals <- ReaderT (Set TyName) (StateT TypeSub (Either String)) (Set TyName)
forall r (m :: * -> *). MonadReader r m => m r
ask
TypeSub
sub <- ReaderT (Set TyName) (StateT TypeSub (Either String)) TypeSub
forall s (m :: * -> *). MonadState s m => m s
get
case TyName -> TypeSub -> Maybe (Type TyName DefaultUni ())
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup TyName
name1 TypeSub
sub of
Just Type TyName DefaultUni ()
ty1' -> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
goType Type TyName DefaultUni ()
ty1' Type TyName DefaultUni ()
ty2
Maybe (Type TyName DefaultUni ())
Nothing -> do
let fvs :: Set TyName
fvs = TypeSub -> Type TyName DefaultUni () -> Set TyName
fvTypeR TypeSub
sub Type TyName DefaultUni ()
ty2
Bool
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ TyName -> Set TyName -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member TyName
name1 Set TyName
flex) (ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ())
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
forall a b. (a -> b) -> a -> b
$
TyName
-> Type TyName DefaultUni ()
-> String
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
forall (m :: * -> *) any.
MonadError String m =>
TyName -> Type TyName DefaultUni () -> String -> m any
resolutionFailure TyName
name1 Type TyName DefaultUni ()
ty2 String
"the variable is not meta"
Bool
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (TyName -> Set TyName -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member TyName
name1 Set TyName
locals) (ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ())
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
forall a b. (a -> b) -> a -> b
$
TyName
-> Type TyName DefaultUni ()
-> String
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
forall (m :: * -> *) any.
MonadError String m =>
TyName -> Type TyName DefaultUni () -> String -> m any
resolutionFailure TyName
name1 Type TyName DefaultUni ()
ty2 String
"the variable is bound"
Bool
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (TyName -> Set TyName -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member TyName
name1 Set TyName
fvs) (ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ())
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
forall a b. (a -> b) -> a -> b
$
TyName
-> Type TyName DefaultUni ()
-> String
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
forall (m :: * -> *) any.
MonadError String m =>
TyName -> Type TyName DefaultUni () -> String -> m any
resolutionFailure TyName
name1 Type TyName DefaultUni ()
ty2 String
"the variable appears free in the type"
case TypeCtx -> Type TyName DefaultUni () -> Kind () -> Either String ()
checkKind TypeCtx
ctx Type TyName DefaultUni ()
ty2 (Kind () -> TyName -> TypeCtx -> Kind ()
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> Kind ()
forall a. HasCallStack => String -> a
error String
"impossible") TyName
name1 TypeCtx
ctx ) of
Left String
msg -> TyName
-> Type TyName DefaultUni ()
-> String
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
forall (m :: * -> *) any.
MonadError String m =>
TyName -> Type TyName DefaultUni () -> String -> m any
resolutionFailure TyName
name1 Type TyName DefaultUni ()
ty2 (String
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ())
-> String
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
forall a b. (a -> b) -> a -> b
$ String
"of kind mismatch:\n\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
msg
Right () -> () -> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
forall a.
a -> ReaderT (Set TyName) (StateT TypeSub (Either String)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
Bool
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not (Bool -> Bool) -> (Set TyName -> Bool) -> Set TyName -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set TyName -> Bool
forall a. Set a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Set TyName -> Bool) -> Set TyName -> Bool
forall a b. (a -> b) -> a -> b
$ Set TyName -> Set TyName -> Set TyName
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection Set TyName
fvs Set TyName
locals) (ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ())
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
forall a b. (a -> b) -> a -> b
$
TyName
-> Type TyName DefaultUni ()
-> String
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
forall (m :: * -> *) any.
MonadError String m =>
TyName -> Type TyName DefaultUni () -> String -> m any
resolutionFailure TyName
name1 Type TyName DefaultUni ()
ty2 (String
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ())
-> String
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
forall a b. (a -> b) -> a -> b
$
String
"the type contains bound variables: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [TyName] -> String
forall str a. (Pretty a, Render str) => a -> str
display (Set TyName -> [TyName]
forall a. Set a -> [a]
Set.toList Set TyName
locals)
TypeSub -> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (TypeSub
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ())
-> TypeSub
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
forall a b. (a -> b) -> a -> b
$ TyName -> Type TyName DefaultUni () -> TypeSub -> TypeSub
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert TyName
name1 Type TyName DefaultUni ()
ty2 TypeSub
sub
goType :: Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
goType :: Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
goType (TyVar ()
_ TyName
x) Type TyName DefaultUni ()
b = TyName
-> Type TyName DefaultUni ()
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
goTyName TyName
x Type TyName DefaultUni ()
b
goType Type TyName DefaultUni ()
a (TyVar ()
_ TyName
y) = TyName
-> Type TyName DefaultUni ()
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
goTyName TyName
y Type TyName DefaultUni ()
a
goType (TyFun ()
_ Type TyName DefaultUni ()
a1 Type TyName DefaultUni ()
a2) (TyFun ()
_ Type TyName DefaultUni ()
b1 Type TyName DefaultUni ()
b2) = Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
goType Type TyName DefaultUni ()
a1 Type TyName DefaultUni ()
b1 ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
forall a b.
ReaderT (Set TyName) (StateT TypeSub (Either String)) a
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) b
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
goType Type TyName DefaultUni ()
a2 Type TyName DefaultUni ()
b2
goType (TyApp ()
_ Type TyName DefaultUni ()
a1 Type TyName DefaultUni ()
a2) (TyApp ()
_ Type TyName DefaultUni ()
b1 Type TyName DefaultUni ()
b2) = Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
goType Type TyName DefaultUni ()
a1 Type TyName DefaultUni ()
b1 ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
forall a b.
ReaderT (Set TyName) (StateT TypeSub (Either String)) a
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) b
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
goType Type TyName DefaultUni ()
a2 Type TyName DefaultUni ()
b2
goType (TyBuiltin ()
_ SomeTypeIn DefaultUni
c1) (TyBuiltin ()
_ SomeTypeIn DefaultUni
c2) = Bool
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (SomeTypeIn DefaultUni
c1 SomeTypeIn DefaultUni -> SomeTypeIn DefaultUni -> Bool
forall a. Eq a => a -> a -> Bool
/= SomeTypeIn DefaultUni
c2) (ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ())
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
forall a b. (a -> b) -> a -> b
$ SomeTypeIn DefaultUni
-> SomeTypeIn DefaultUni
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
forall (m :: * -> *) a b any.
(MonadError String m, Pretty a, Pretty b) =>
a -> b -> m any
unificationFailure SomeTypeIn DefaultUni
c1 SomeTypeIn DefaultUni
c2
goType (TyIFix ()
_ Type TyName DefaultUni ()
a1 Type TyName DefaultUni ()
a2) (TyIFix ()
_ Type TyName DefaultUni ()
b1 Type TyName DefaultUni ()
b2) = Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
goType Type TyName DefaultUni ()
a1 Type TyName DefaultUni ()
b1 ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
forall a b.
ReaderT (Set TyName) (StateT TypeSub (Either String)) a
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) b
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
goType Type TyName DefaultUni ()
a2 Type TyName DefaultUni ()
b2
goType (TyForall ()
_ TyName
x Kind ()
k Type TyName DefaultUni ()
a') (TyForall ()
_ TyName
y Kind ()
l Type TyName DefaultUni ()
b') = do
Bool
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Kind ()
k Kind () -> Kind () -> Bool
forall a. Eq a => a -> a -> Bool
/= Kind ()
l) (ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ())
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
forall a b. (a -> b) -> a -> b
$ Kind ()
-> Kind ()
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
forall (m :: * -> *) a b any.
(MonadError String m, Pretty a, Pretty b) =>
a -> b -> m any
unificationFailure Kind ()
k Kind ()
l
Set TyName
locals <- ReaderT (Set TyName) (StateT TypeSub (Either String)) (Set TyName)
forall r (m :: * -> *). MonadReader r m => m r
ask
let z :: TyName
z = Set TyName -> TyName -> TyName
freshenTyNameWith (Set TyName
locals Set TyName -> Set TyName -> Set TyName
forall a. Semigroup a => a -> a -> a
<> TypeCtx -> Set TyName
forall k a. Map k a -> Set k
Map.keysSet TypeCtx
ctx) TyName
x
(Set TyName -> Set TyName)
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
forall a.
(Set TyName -> Set TyName)
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) a
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (TyName -> Set TyName -> Set TyName
forall a. Ord a => a -> Set a -> Set a
Set.insert TyName
z) (ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ())
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
forall a b. (a -> b) -> a -> b
$ Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
goType (TyName
-> TyName -> Type TyName DefaultUni () -> Type TyName DefaultUni ()
renameVar TyName
x TyName
z Type TyName DefaultUni ()
a') (TyName
-> TyName -> Type TyName DefaultUni () -> Type TyName DefaultUni ()
renameVar TyName
y TyName
z Type TyName DefaultUni ()
b')
goType (TyLam ()
_ TyName
x Kind ()
k Type TyName DefaultUni ()
a') (TyLam ()
_ TyName
y Kind ()
l Type TyName DefaultUni ()
b') = do
Bool
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Kind ()
k Kind () -> Kind () -> Bool
forall a. Eq a => a -> a -> Bool
/= Kind ()
l) (ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ())
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
forall a b. (a -> b) -> a -> b
$ Kind ()
-> Kind ()
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
forall (m :: * -> *) a b any.
(MonadError String m, Pretty a, Pretty b) =>
a -> b -> m any
unificationFailure Kind ()
k Kind ()
l
Set TyName
locals <- ReaderT (Set TyName) (StateT TypeSub (Either String)) (Set TyName)
forall r (m :: * -> *). MonadReader r m => m r
ask
let z :: TyName
z = Set TyName -> TyName -> TyName
freshenTyNameWith (Set TyName
locals Set TyName -> Set TyName -> Set TyName
forall a. Semigroup a => a -> a -> a
<> TypeCtx -> Set TyName
forall k a. Map k a -> Set k
Map.keysSet TypeCtx
ctx) TyName
x
(Set TyName -> Set TyName)
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
forall a.
(Set TyName -> Set TyName)
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) a
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (TyName -> Set TyName -> Set TyName
forall a. Ord a => a -> Set a -> Set a
Set.insert TyName
z) (ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ())
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
forall a b. (a -> b) -> a -> b
$ Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
goType (TyName
-> TyName -> Type TyName DefaultUni () -> Type TyName DefaultUni ()
renameVar TyName
x TyName
z Type TyName DefaultUni ()
a') (TyName
-> TyName -> Type TyName DefaultUni () -> Type TyName DefaultUni ()
renameVar TyName
y TyName
z Type TyName DefaultUni ()
b')
goType (TySOP ()
_ [[Type TyName DefaultUni ()]]
sum1) (TySOP ()
_ [[Type TyName DefaultUni ()]]
sum2)
| Just [([Type TyName DefaultUni ()], [Type TyName DefaultUni ()])]
sum12 <- [[Type TyName DefaultUni ()]]
-> [[Type TyName DefaultUni ()]]
-> Maybe
[([Type TyName DefaultUni ()], [Type TyName DefaultUni ()])]
forall a b. [a] -> [b] -> Maybe [(a, b)]
zipExact [[Type TyName DefaultUni ()]]
sum1 [[Type TyName DefaultUni ()]]
sum2
= [([Type TyName DefaultUni ()], [Type TyName DefaultUni ()])]
-> (([Type TyName DefaultUni ()], [Type TyName DefaultUni ()])
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ())
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ [([Type TyName DefaultUni ()], [Type TyName DefaultUni ()])]
sum12 ((([Type TyName DefaultUni ()], [Type TyName DefaultUni ()])
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ())
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ())
-> (([Type TyName DefaultUni ()], [Type TyName DefaultUni ()])
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ())
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
forall a b. (a -> b) -> a -> b
$ \([Type TyName DefaultUni ()]
prod1, [Type TyName DefaultUni ()]
prod2) -> do
case [Type TyName DefaultUni ()]
-> [Type TyName DefaultUni ()]
-> Maybe [(Type TyName DefaultUni (), Type TyName DefaultUni ())]
forall a b. [a] -> [b] -> Maybe [(a, b)]
zipExact [Type TyName DefaultUni ()]
prod1 [Type TyName DefaultUni ()]
prod2 of
Maybe [(Type TyName DefaultUni (), Type TyName DefaultUni ())]
Nothing -> [Type TyName DefaultUni ()]
-> [Type TyName DefaultUni ()]
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
forall (m :: * -> *) a b any.
(MonadError String m, Pretty a, Pretty b) =>
a -> b -> m any
unificationFailure [Type TyName DefaultUni ()]
prod1 [Type TyName DefaultUni ()]
prod2
Just [(Type TyName DefaultUni (), Type TyName DefaultUni ())]
prod12 -> ((Type TyName DefaultUni (), Type TyName DefaultUni ())
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ())
-> [(Type TyName DefaultUni (), Type TyName DefaultUni ())]
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ ((Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ())
-> (Type TyName DefaultUni (), Type TyName DefaultUni ())
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
goType) [(Type TyName DefaultUni (), Type TyName DefaultUni ())]
prod12
goType Type TyName DefaultUni ()
a Type TyName DefaultUni ()
b = Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> ReaderT (Set TyName) (StateT TypeSub (Either String)) ()
forall (m :: * -> *) a b any.
(MonadError String m, Pretty a, Pretty b) =>
a -> b -> m any
unificationFailure Type TyName DefaultUni ()
a Type TyName DefaultUni ()
b