How are types unified

Stream: new members

[Hossam Karim]

I am trying to understand how Tsk.run compiles in the example below. The .functor and .monad branches should evaluate to Either String β right? Or is it because α β : Type u for some u?

abbrev Either := Sum

instance : Monad (Either ε) where
  pure := .inr
  bind := fun
    | .inl e, _ => .inl e
    | .inr a, f => f a

inductive Tsk : Type _ -> Type _ where
  | pure (a : α) : Tsk α
  | failed {α} (error : String) : Tsk α
  | recovered (self : Tsk α) (a : α) : Tsk α
  | delayed (a : Unit -> α) : Tsk α
  | functor (self : Tsk α) (f : α -> β) : Tsk β
  | monad (self : Tsk α) (f : α -> Tsk β) : Tsk β

instance : Monad Tsk where
  pure := Tsk.pure
  bind := Tsk.monad

def Tsk.run [ei : Monad (Either String)] : (self : Tsk α) -> Either String α
  | .pure a        => .inr a
  | .failed e      => .inl e
  | .recovered t a => match t.run with | .inl _ => .inr a | .inr x => .inr x
  | .delayed f     => .inr (f ())
  | .functor t f   => ei.map f (t.run)
  | .monad t f     => t.run >>= (λ x => (f x).run)

def mk : Tsk String := do
  let x <- .delayed λ _ => 4
  let failed := @Tsk.failed String "oops"
  let recovered <- Tsk.recovered failed "OK:"
  let y <- .pure s!"{recovered} lean {x}"
  let z <- .pure s!"{y} is awesome"
  return z

#eval mk.run

[Kyle Miller]

Here are some type annotations to try to make it a bit clearer (and I switched ei.map to Functor.map, notated <$>):

def Tsk.run [Monad (Either String)] : (self : Tsk α) -> Either String α
  | .pure a        => .inr a
  | .failed e      => .inl e
  | .recovered t a => match t.run with | .inl _ => .inr a | .inr x => .inr x
  | .delayed f     => .inr (f ())
  | .functor (α := α) (β := β) t f   => (f <$> (t.run : Either String α) : Either String β)
  | .monad (α := α) (β := β) t f     => ((t.run : Either String α) >>=
                                            (λ x => (f x).run) : Either String β)

[Kyle Miller]

It's a bit counterintuitive, but the branches are meant to evaluate to Either String β since the type gets switched out in the inductive declaration for these constructors