-- editorconfig-checker-disable-file

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
    ]

{- Note [The unification algorithm]
Type unification expects a context (mapping from type variables to their kinds) and a set of
flexible type variables, also called metas (those that can get resolved). The context is used for
kind checking solutions as well as generation of fresh variables.

Internally type unification maintains a set of locals ('TyLam'- or 'TyForall'-bound variables
encountered during unification). Those are stored in a reader monad, since they depend on the
current scope and need to be adjusted when the scope changes, which is best modelled by a reader
monad.

Type unification also maintains a substitution (mapping from a possibly empty subset of metas to
their instantiations) and eventually that substitution is returned as a result of unification. The
substitution is passed around in a state monad, since unification results in one part of the
unification problem are relevant in all the other parts too (this is not in conflict with locals
being scope-specific, because flexible variable resolution cannot capture a locally bound
variable). Type unification could take a substitution as an input and extend it instead of always
making the initial substitution empty, but we didn't need this extra functionality, so we didn't
implement it for the sake of keeping the interface to the unifier simpler.

Type unification proceeds by recursion on the spines of the two types. We don't attempt to do
higher-order unification at all, so we don't have the usual unification business like pruning,
blocking, pattern unification etc. In particular, in our setting two type applications can unify
only if the functions and the arguments unify separately (with higher-order unification it would be
possible to unify type applications whose function parts differ, because functions compute and the
results may unify even if the functions don't).

We handle 'TyIFix' and 'TyFun' the same way as type applications by decomposing them into their
constituents and unifying them separately. These two would look the same in a higher-order setting.

'TyLam' and 'TyForall' being binders require a bit of special care: we rename the bound variables in
the bodies of the binders, so that the two sides of the unification equation bind the same variable,
see Note [Renaming during unification]. We do not attempt to perform unification modulo eta.

Two 'TyBuiltin's unify when they are the same built-in type.

The only remaining case is when one of the sides is a type variable (or both). There's a number of
checks that we perform in order to ensure that it's fine to resolve the variable as the given type,
those are documented alongside the code performing the checks.
-}

{- Note [Renaming during unification]
When we go under twin binders, we rename the variables that the binders introduce, so that they have
the same name. This requires travering both the sides of the unification problem before unification
can proceed. This is inefficient, instead we could do the same thing that we do for checking
equality and keep two separate maps tracking renamings of local variables. Although the types AST is
lazy, so maybe it's not a big deal in the end. Although even with laziness, we still have quadratic
behavior currently.

Note that generating a new name is also a rather expensive operation requiring to traverse the whole
context, so that's another source of inefficiency.
-}

-- See Note [The unification algorithm].
-- | Perform unification. Sound but not complete.
unifyType :: TypeCtx
          -- ^ Type context
          -> Set TyName
          -- ^ @flex@, the flexible variables (those that can be unified)
          -> Type TyName DefaultUni ()
          -- ^ @t1@
          -> Type TyName DefaultUni ()
          -- ^ @t2@
          -> Either String TypeSub
          -- ^ Either an error or a substitution (from a subset of @flex@) unifying @t1@ and @t2@
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 =
      -- If the variable is unified with itself, we don't need to do anything.
      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
          -- If the meta is already resolved, then look it up in the substitution and continue
          -- unification.
          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
            -- When a meta gets resolved, we do no substitute for all the variables in the solution,
            -- i.e. the solution can contain variables that themselves are resolved metas. Hence for
            -- computing the free variables of a type we have to look in the substitution to find
            -- the free variables of already resolved metas in there.
            -- See the definition of 'fvTypeR'.
            let fvs :: Set TyName
fvs = TypeSub -> Type TyName DefaultUni () -> Set TyName
fvTypeR TypeSub
sub Type TyName DefaultUni ()
ty2
            -- Cannot resolve a non-flexible type variable.
            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"
            -- Cannot resolve a locally bound type variable.
            -- Covers situations like @(\x -> x) =?= (\x -> integer)@.
            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"
            -- Occurs check. Covers situations like @_x =?= _x -> integer@.
            -- Note that our occurs check is pretty naive, e.g. we could've solved @_x =?= _f _x@ as
            -- @[_f := \x -> x]@ or @[_f := \_ -> _x]@, but we don't attempt to cover the
            -- higher-order case.
            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"
            -- Cannot resolve a meta to an ill-kinded 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 ()
            -- Cannot capture a locally bound variable.
            -- Covers situations like @(\x -> _y) =?= (\x -> x)@.
            -- As naive as the occurs check.
            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
    -- This is only structural recursion, because we don't attempt to do higher-order unification.
    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
      -- See Note [Renaming during unification].
      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
      -- See Note [Renaming during unification].
      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)
        -- Sums must be of the same arity.
        | 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
            -- Products within sums must be of the same arity.
            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
                -- SOPs unify componentwise.
                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