import Lean.Elab

structure 
WithLog: Type → Type → Type
WithLog (
logged: Type
logged : 
Type: Type 1
Type) (
α: Type
α : 
Type: Type 1
Type) where
  
log: {logged α : Type} → WithLog logged α → List logged
log : 
List: Type → Type
List 
logged: Type
logged
  
val: {logged α : Type} → WithLog logged α → α
val : 
α: Type
α

instance: {logged : Type} → Monad (WithLog logged)
instance : 
Monad: (Type → Type) → Type 1
Monad <| 
WithLog: Type → Type → Type
WithLog 
logged: Type
logged where
  pure 
val: α✝
val := ⟨
[]: List logged
[], 
val: α✝
val⟩
  bind 
item: WithLog logged α✝
item 
next: α✝ → WithLog logged β✝
next :=
    let rec 
nextItem: {logged α β : Type} → WithLog logged α → (α → WithLog logged β) → WithLog logged β
nextItem := 
next: α✝ → WithLog logged β✝
next 
item: WithLog logged α✝
item.
val: {logged α : Type} → WithLog logged α → α
val
    ⟨
item: WithLog logged α✝
item.
log: {logged α : Type} → WithLog logged α → List logged
log ++ 
nextItem: WithLog logged β✝
nextItem.
log: {logged α : Type} → WithLog logged α → List logged
log, 
nextItem: WithLog logged β✝
nextItem.
val: {logged α : Type} → WithLog logged α → α
val⟩

set_option relaxedAutoImplicit false
set_option autoImplicit false
set_option pp.all true
set_option pp.analyze true
set_option trace.Meta.synthInstance true
set_option synthInstance.checkSynthOrder true

def 
Option': Type u_1 → Type u_1
Option' := 
Option: Type u_1 → Type u_1
Option

-- The error is now gone
-- /--
-- error: fields missing: 'map', 'mapConst', 'seq', 'seqLeft'
-- -/
-- #guard_msgs(error, drop info) in
instance: Monad.{u_1, u_1} Option'.{u_1}
instance : 
Monad: (Type u_1 → Type u_1) → Type (u_1 + 1)
Monad 
Option': Type u_1 → Type u_1
Option' where
  pure := 
Option.some: {α : Type u_1} → α → Option.{u_1} α
Option.some
  bind 
a: Option'.{u_1} α✝
a 
f: α✝ → Option'.{u_1} β✝
f :=
    let 
b: Option.{u_1} β✝
b := 
Option.bind: {α β : Type u_1} → Option.{u_1} α → (α → Option.{u_1} β) → Option.{u_1} β
Option.bind 
a: Option'.{u_1} α✝
a 
f: α✝ → Option'.{u_1} β✝
f
    
b: Option.{u_1} β✝
b
[Meta.synthInstance] ❌️ Functor.{?u.985, ?u.985} Option'.{?u.985}
  [Meta.synthInstance] new goal Functor.{?u.985, ?u.985} Option'.{?u.985}
    [Meta.synthInstance.instances] #[@Applicative.toFunctor.{?u.1003, ?u.1004}]
  [Meta.synthInstance] ✅️ apply @Applicative.toFunctor.{?u.985, ?u.985} to Functor.{?u.985, ?u.985} Option'.{?u.985}
    [Meta.synthInstance.tryResolve] ✅️ Functor.{?u.985, ?u.985}
          Option'.{?u.985} ≟ Functor.{?u.985, ?u.985} Option'.{?u.985}
    [Meta.synthInstance] new goal Applicative.{?u.985, ?u.985} Option'.{?u.985}
      [Meta.synthInstance.instances] #[@Monad.toApplicative.{?u.1010,
              ?u.1011}, @Alternative.toApplicative.{?u.1012, ?u.1013}]
  [Meta.synthInstance] ✅️ apply @Alternative.toApplicative.{?u.985,
          ?u.985} to Applicative.{?u.985, ?u.985} Option'.{?u.985}
    [Meta.synthInstance.tryResolve] ✅️ Applicative.{?u.985, ?u.985}
          Option'.{?u.985} ≟ Applicative.{?u.985, ?u.985} Option'.{?u.985}
    [Meta.synthInstance] no instances for Alternative.{?u.985, ?u.985} Option'.{?u.985}
      [Meta.synthInstance.instances] #[]
  [Meta.synthInstance] ✅️ apply @Monad.toApplicative.{?u.985, ?u.985} to Applicative.{?u.985, ?u.985} Option'.{?u.985}
    [Meta.synthInstance.tryResolve] ✅️ Applicative.{?u.985, ?u.985}
          Option'.{?u.985} ≟ Applicative.{?u.985, ?u.985} Option'.{?u.985}
    [Meta.synthInstance] no instances for Monad.{?u.985, ?u.985} Option'.{?u.985}
      [Meta.synthInstance.instances] #[]
  [Meta.synthInstance] result <not-available>
[Meta.synthInstance] ❌️ Seq.{?u.985, ?u.985} Option'.{?u.985}
  [Meta.synthInstance] new goal Seq.{?u.985, ?u.985} Option'.{?u.985}
    [Meta.synthInstance.instances] #[@Applicative.toSeq.{?u.1048, ?u.1049}]
  [Meta.synthInstance] ✅️ apply @Applicative.toSeq.{?u.985, ?u.985} to Seq.{?u.985, ?u.985} Option'.{?u.985}
    [Meta.synthInstance.tryResolve] ✅️ Seq.{?u.985, ?u.985} Option'.{?u.985} ≟ Seq.{?u.985, ?u.985} Option'.{?u.985}
    [Meta.synthInstance] new goal Applicative.{?u.985, ?u.985} Option'.{?u.985}
      [Meta.synthInstance.instances] #[@Monad.toApplicative.{?u.1055,
              ?u.1056}, @Alternative.toApplicative.{?u.1057, ?u.1058}]
  [Meta.synthInstance] ✅️ apply @Alternative.toApplicative.{?u.985,
          ?u.985} to Applicative.{?u.985, ?u.985} Option'.{?u.985}
    [Meta.synthInstance.tryResolve] ✅️ Applicative.{?u.985, ?u.985}
          Option'.{?u.985} ≟ Applicative.{?u.985, ?u.985} Option'.{?u.985}
    [Meta.synthInstance] no instances for Alternative.{?u.985, ?u.985} Option'.{?u.985}
      [Meta.synthInstance.instances] #[]
  [Meta.synthInstance] ✅️ apply @Monad.toApplicative.{?u.985, ?u.985} to Applicative.{?u.985, ?u.985} Option'.{?u.985}
    [Meta.synthInstance.tryResolve] ✅️ Applicative.{?u.985, ?u.985}
          Option'.{?u.985} ≟ Applicative.{?u.985, ?u.985} Option'.{?u.985}
    [Meta.synthInstance] no instances for Monad.{?u.985, ?u.985} Option'.{?u.985}
      [Meta.synthInstance.instances] #[]
  [Meta.synthInstance] result <not-available>
[Meta.synthInstance] ❌️ SeqLeft.{?u.985, ?u.985} Option'.{?u.985}
  [Meta.synthInstance] new goal SeqLeft.{?u.985, ?u.985} Option'.{?u.985}
    [Meta.synthInstance.instances] #[@Applicative.toSeqLeft.{?u.1073, ?u.1074}]
  [Meta.synthInstance] ✅️ apply @Applicative.toSeqLeft.{?u.985, ?u.985} to SeqLeft.{?u.985, ?u.985} Option'.{?u.985}
    [Meta.synthInstance.tryResolve] ✅️ SeqLeft.{?u.985, ?u.985}
          Option'.{?u.985} ≟ SeqLeft.{?u.985, ?u.985} Option'.{?u.985}
    [Meta.synthInstance] new goal Applicative.{?u.985, ?u.985} Option'.{?u.985}
      [Meta.synthInstance.instances] #[@Monad.toApplicative.{?u.1080,
              ?u.1081}, @Alternative.toApplicative.{?u.1082, ?u.1083}]
  [Meta.synthInstance] ✅️ apply @Alternative.toApplicative.{?u.985,
          ?u.985} to Applicative.{?u.985, ?u.985} Option'.{?u.985}
    [Meta.synthInstance.tryResolve] ✅️ Applicative.{?u.985, ?u.985}
          Option'.{?u.985} ≟ Applicative.{?u.985, ?u.985} Option'.{?u.985}
    [Meta.synthInstance] no instances for Alternative.{?u.985, ?u.985} Option'.{?u.985}
      [Meta.synthInstance.instances] #[]
  [Meta.synthInstance] ✅️ apply @Monad.toApplicative.{?u.985, ?u.985} to Applicative.{?u.985, ?u.985} Option'.{?u.985}
    [Meta.synthInstance.tryResolve] ✅️ Applicative.{?u.985, ?u.985}
          Option'.{?u.985} ≟ Applicative.{?u.985, ?u.985} Option'.{?u.985}
    [Meta.synthInstance] no instances for Monad.{?u.985, ?u.985} Option'.{?u.985}
      [Meta.synthInstance.instances] #[]
  [Meta.synthInstance] result <not-available>
[Meta.synthInstance] ❌️ SeqRight.{?u.985, ?u.985} Option'.{?u.985}
  [Meta.synthInstance] new goal SeqRight.{?u.985, ?u.985} Option'.{?u.985}
    [Meta.synthInstance.instances] #[@Applicative.toSeqRight.{?u.1098, ?u.1099}]
  [Meta.synthInstance] ✅️ apply @Applicative.toSeqRight.{?u.985, ?u.985} to SeqRight.{?u.985, ?u.985} Option'.{?u.985}
    [Meta.synthInstance.tryResolve] ✅️ SeqRight.{?u.985, ?u.985}
          Option'.{?u.985} ≟ SeqRight.{?u.985, ?u.985} Option'.{?u.985}
    [Meta.synthInstance] new goal Applicative.{?u.985, ?u.985} Option'.{?u.985}
      [Meta.synthInstance.instances] #[@Monad.toApplicative.{?u.1105,
              ?u.1106}, @Alternative.toApplicative.{?u.1107, ?u.1108}]
  [Meta.synthInstance] ✅️ apply @Alternative.toApplicative.{?u.985,
          ?u.985} to Applicative.{?u.985, ?u.985} Option'.{?u.985}
    [Meta.synthInstance.tryResolve] ✅️ Applicative.{?u.985, ?u.985}
          Option'.{?u.985} ≟ Applicative.{?u.985, ?u.985} Option'.{?u.985}
    [Meta.synthInstance] no instances for Alternative.{?u.985, ?u.985} Option'.{?u.985}
      [Meta.synthInstance.instances] #[]
  [Meta.synthInstance] ✅️ apply @Monad.toApplicative.{?u.985, ?u.985} to Applicative.{?u.985, ?u.985} Option'.{?u.985}
    [Meta.synthInstance.tryResolve] ✅️ Applicative.{?u.985, ?u.985}
          Option'.{?u.985} ≟ Applicative.{?u.985, ?u.985} Option'.{?u.985}
    [Meta.synthInstance] no instances for Monad.{?u.985, ?u.985} Option'.{?u.985}
      [Meta.synthInstance.instances] #[]
  [Meta.synthInstance] result <not-available>

variable (
logged: Type
logged : 
Type: Type 1
Type) in
#synth 
Monad: (Type → Type) → Type 1
Monad <| 
WithLog: Type → Type → Type
WithLog 
logged: Type
logged
@instMonadWithLog logged
[Meta.synthInstance] ✅️ Monad.{0, 0} (WithLog logged)
  [Meta.synthInstance] new goal Monad.{0, 0} (WithLog logged)
    [Meta.synthInstance.instances] #[@instMonadWithLog]
  [Meta.synthInstance] ✅️ apply @instMonadWithLog to Monad.{0, 0} (WithLog logged)
    [Meta.synthInstance.tryResolve] ✅️ Monad.{0, 0} (WithLog logged) ≟ Monad.{0, 0} (WithLog logged)
    [Meta.synthInstance.answer] ✅️ Monad.{0, 0} (WithLog logged)
  [Meta.synthInstance] result @instMonadWithLog logged

-- instance : Pure <| WithLog logged where
--   pure val := ⟨[], val⟩

-- -- instance : Bind <| WithLog logged where
-- --   bind item next :=
-- --     let {log := thisLog, .. } := item
-- --     let {log := nextOut, val := nextRes} := next item.val
-- --     ⟨thisLog ++ nextOut, nextRes⟩

-- instance : Bind <| WithLog logged where
--   bind item next :=
--     let nextItem := next item.val
--     ⟨item.log ++ nextItem.log, nextItem.val⟩

-- section CheckInstances

-- variable (logged : Type)

-- /-
-- failed to synthesize
--   Applicative (WithLog logged)
-- -/
-- #synth Applicative <| WithLog logged

-- /-
-- failed to synthesize
--   Monad (WithLog logged)
-- -/
-- #synth Monad <| WithLog logged

-- /-
-- [Meta.synthInstance] ✅ Monad (WithLog logged) ▼
--   [] new goal Monad (WithLog logged) ▶
--   [] ✅ apply @instMonadWithLog to Monad (WithLog logged) ▼
--     [tryResolve] ✅ Monad (WithLog logged) ≟ Monad (WithLog logged)
--   [] result instMonadWithLog
-- -/
-- #synth Monad <| WithLog logged

-- end CheckInstances

-- /-
-- [Meta.synthInstance] ❌ Applicative (WithLog logged) ▶


-- [Meta.synthInstance] ❌ Functor (WithLog logged) ▶


-- [Meta.synthInstance] ✅ Pure (WithLog logged) ▶


-- [Meta.synthInstance] ❌ Seq (WithLog logged) ▶


-- [Meta.synthInstance] ❌ SeqLeft (WithLog logged) ▶


-- [Meta.synthInstance] ❌ SeqRight (WithLog logged) ▶


-- [Meta.synthInstance] ✅ Bind (WithLog logged) ▶
-- -/
-- instance : Monad <| WithLog logged where -- no error

-- variable (logged : Type) in
-- #synth Monad <| WithLog logged

-- def Option' := Option

-- #print Monad.map._default

-- structure A where
--   a : Nat -> Nat := fun x => x

-- structure B extends A where
--   a := A.a._default

/-
@[reducible] def Applicative.map._default.{u_1, u_2} : {f : Type u_1 → Type u_2} →
  Pure.{u_1, u_2} f → Seq.{u_1, u_2} f → {α β : Type u_1} → (α → β) → f α → f β :=
fun {f : Type u_1 → Type u_2} (toPure : Pure.{u_1, u_2} f) (toSeq : Seq.{u_1, u_2} f) =>
  @id.{max (u_1 + 2) (u_2 + 1)} ({α β : Type u_1} → (α → β) → f α → f β) fun {α β : Type u_1} (x : α → β) (y : f α) =>
    @Seq.seq.{u_1, u_2} f toSeq α β (@Pure.pure.{u_1, u_2} f toPure (α → β) x) fun (x : Unit) => y
-/
#print
@[reducible] def Applicative.map._default.{u_1, u_2} : {f : Type u_1 → Type u_2} →
  Pure.{u_1, u_2} f → Seq.{u_1, u_2} f → {α β : Type u_1} → (α → β) → f α → f β :=
fun {f : Type u_1 → Type u_2} (toPure : Pure.{u_1, u_2} f) (toSeq : Seq.{u_1, u_2} f) =>
  @id.{max (u_1 + 2) (u_2 + 1)} ({α β : Type u_1} → (α → β) → f α → f β) fun {α β : Type u_1} (x : α → β) (y : f α) =>
    @Seq.seq.{u_1, u_2} f toSeq α β (@Pure.pure.{u_1, u_2} f toPure (α → β) x) fun (x : Unit) => y 
Applicative.map._default: {f : Type u_1 → Type u_2} → Pure.{u_1, u_2} f → Seq.{u_1, u_2} f → {α β : Type u_1} → (α → β) → f α → f β
Applicative.map._default

/-
@[reducible] def Monad.map._default.{u_1, u_2} : {m : Type u_1 → Type u_2} →
  Applicative m → Bind m → {α β : Type u_1} → (α → β) → m α → m β :=
fun {m} toApplicative toBind => @id ({α β : Type u_1} → (α → β) → m α → m β) fun {α β} f x => x >>= pure ∘ f
-/
#print
@[reducible] def Monad.map._default.{u_1, u_2} : {m : Type u_1 → Type u_2} →
  Applicative.{u_1, u_2} m → Bind.{u_1, u_2} m → {α β : Type u_1} → (α → β) → m α → m β :=
fun {m : Type u_1 → Type u_2} (toApplicative : Applicative.{u_1, u_2} m) (toBind : Bind.{u_1, u_2} m) =>
  @id.{max (u_1 + 2) (u_2 + 1)} ({α β : Type u_1} → (α → β) → m α → m β) fun {α β : Type u_1} (f : α → β) (x : m α) =>
    @Bind.bind.{u_1, u_2} m toBind α β x
      (@Function.comp.{u_1 + 1, u_1 + 1, u_2 + 1} α β (m β)
        (@Pure.pure.{u_1, u_2} m (@Applicative.toPure.{u_1, u_2} m toApplicative) β) f) 
Monad.map._default: {m : Type u_1 → Type u_2} → Applicative.{u_1, u_2} m → Bind.{u_1, u_2} m → {α β : Type u_1} → (α → β) → m α → m β
Monad.map._default

set_option structureDiamondWarning true

-- instance : Monad Option' where
--   pure := Option.some
--   bind := Option.bind
--   map := Monad.map._default

-- instance : Monad Option' where
--   pure := Option.some
--   bind a f :=
--     let b := Option.bind a f
--     b
--   map f x := Monad.map._default _ _ f x

-- instance : Monad Option' where
--   pure := Option.some
--   bind a f :=
--     let rec b := Option.bind a f
--     b
--   map f x := Monad.map._default _ _ f x

instance: Monad.{u_1, u_1} Option'.{u_1}
instance : 
Monad: (Type u_1 → Type u_1) → Type (u_1 + 1)
Monad 
Option': Type u_1 → Type u_1
Option' where
  pure := 
Option.some: {α : Type u_1} → α → Option.{u_1} α
Option.some
  bind 
a: Option'.{u_1} α✝
a 
f: α✝ → Option'.{u_1} β✝
f :=
    let 
c: Option.{u_1} β✝
c :=
      let rec 
b: Option.{u_1} β✝
b := 
Option.bind: {α β : Type u_1} → Option.{u_1} α → (α → Option.{u_1} β) → Option.{u_1} β
Option.bind 
a: Option'.{u_1} α✝
a 
f: α✝ → Option'.{u_1} β✝
f
      
b: Option.{u_1} β✝
b
    
c: Option.{u_1} β✝
c
[Meta.synthInstance] ✅️ Functor.{?u.1460, ?u.1460} Option'.{?u.1460}
  [Meta.synthInstance] new goal Functor.{?u.1460, ?u.1460} Option'.{?u.1460}
    [Meta.synthInstance.instances] #[@Applicative.toFunctor.{?u.1478, ?u.1479}]
  [Meta.synthInstance] ✅️ apply @Applicative.toFunctor.{?u.1460,
          ?u.1460} to Functor.{?u.1460, ?u.1460} Option'.{?u.1460}
    [Meta.synthInstance.tryResolve] ✅️ Functor.{?u.1460, ?u.1460}
          Option'.{?u.1460} ≟ Functor.{?u.1460, ?u.1460} Option'.{?u.1460}
    [Meta.synthInstance] new goal Applicative.{?u.1460, ?u.1460} Option'.{?u.1460}
      [Meta.synthInstance.instances] #[@Monad.toApplicative.{?u.1485,
              ?u.1486}, @Alternative.toApplicative.{?u.1487, ?u.1488}]
  [Meta.synthInstance] ✅️ apply @Alternative.toApplicative.{?u.1460,
          ?u.1460} to Applicative.{?u.1460, ?u.1460} Option'.{?u.1460}
    [Meta.synthInstance.tryResolve] ✅️ Applicative.{?u.1460, ?u.1460}
          Option'.{?u.1460} ≟ Applicative.{?u.1460, ?u.1460} Option'.{?u.1460}
    [Meta.synthInstance] no instances for Alternative.{?u.1460, ?u.1460} Option'.{?u.1460}
      [Meta.synthInstance.instances] #[]
  [Meta.synthInstance] ✅️ apply @Monad.toApplicative.{?u.1460,
          ?u.1460} to Applicative.{?u.1460, ?u.1460} Option'.{?u.1460}
    [Meta.synthInstance.tryResolve] ✅️ Applicative.{?u.1460, ?u.1460}
          Option'.{?u.1460} ≟ Applicative.{?u.1460, ?u.1460} Option'.{?u.1460}
    [Meta.synthInstance] new goal Monad.{?u.1460, ?u.1460} Option'.{?u.1460}
      [Meta.synthInstance.instances] #[instMonadOption'.{?u.1499}]
  [Meta.synthInstance] ✅️ apply instMonadOption'.{?u.1460} to Monad.{?u.1460, ?u.1460} Option'.{?u.1460}
    [Meta.synthInstance.tryResolve] ✅️ Monad.{?u.1460, ?u.1460}
          Option'.{?u.1460} ≟ Monad.{?u.1460, ?u.1460} Option'.{?u.1460}
    [Meta.synthInstance.answer] ✅️ Monad.{?u.1460, ?u.1460} Option'.{?u.1460}
  [Meta.synthInstance.resume] propagating Monad.{?u.1460, ?u.1460}
        Option'.{?u.1460} to subgoal Monad.{?u.1460, ?u.1460}
        Option'.{?u.1460} of Applicative.{?u.1460, ?u.1460} Option'.{?u.1460}
    [Meta.synthInstance.resume] size: 1
    [Meta.synthInstance.answer] ✅️ Applicative.{?u.1460, ?u.1460} Option'.{?u.1460}
  [Meta.synthInstance.resume] propagating Applicative.{?u.1460, ?u.1460}
        Option'.{?u.1460} to subgoal Applicative.{?u.1460, ?u.1460}
        Option'.{?u.1460} of Functor.{?u.1460, ?u.1460} Option'.{?u.1460}
    [Meta.synthInstance.resume] size: 2
    [Meta.synthInstance.answer] ✅️ Functor.{?u.1460, ?u.1460} Option'.{?u.1460}
  [Meta.synthInstance] result @Applicative.toFunctor.{?u.1460, ?u.1460} Option'.{?u.1460}
        (@Monad.toApplicative.{?u.1460, ?u.1460} Option'.{?u.1460} instMonadOption'.{?u.1460})
[Meta.synthInstance] ✅️ Seq.{?u.1460, ?u.1460} Option'.{?u.1460}
  [Meta.synthInstance] new goal Seq.{?u.1460, ?u.1460} Option'.{?u.1460}
    [Meta.synthInstance.instances] #[@Applicative.toSeq.{?u.1520, ?u.1521}]
  [Meta.synthInstance] ✅️ apply @Applicative.toSeq.{?u.1460, ?u.1460} to Seq.{?u.1460, ?u.1460} Option'.{?u.1460}
    [Meta.synthInstance.tryResolve] ✅️ Seq.{?u.1460, ?u.1460}
          Option'.{?u.1460} ≟ Seq.{?u.1460, ?u.1460} Option'.{?u.1460}
    [Meta.synthInstance] new goal Applicative.{?u.1460, ?u.1460} Option'.{?u.1460}
      [Meta.synthInstance.instances] #[@Monad.toApplicative.{?u.1527,
              ?u.1528}, @Alternative.toApplicative.{?u.1529, ?u.1530}]
  [Meta.synthInstance] ✅️ apply @Alternative.toApplicative.{?u.1460,
          ?u.1460} to Applicative.{?u.1460, ?u.1460} Option'.{?u.1460}
    [Meta.synthInstance.tryResolve] ✅️ Applicative.{?u.1460, ?u.1460}
          Option'.{?u.1460} ≟ Applicative.{?u.1460, ?u.1460} Option'.{?u.1460}
    [Meta.synthInstance] no instances for Alternative.{?u.1460, ?u.1460} Option'.{?u.1460}
      [Meta.synthInstance.instances] #[]
  [Meta.synthInstance] ✅️ apply @Monad.toApplicative.{?u.1460,
          ?u.1460} to Applicative.{?u.1460, ?u.1460} Option'.{?u.1460}
    [Meta.synthInstance.tryResolve] ✅️ Applicative.{?u.1460, ?u.1460}
          Option'.{?u.1460} ≟ Applicative.{?u.1460, ?u.1460} Option'.{?u.1460}
    [Meta.synthInstance] new goal Monad.{?u.1460, ?u.1460} Option'.{?u.1460}
      [Meta.synthInstance.instances] #[instMonadOption'.{?u.1537}]
  [Meta.synthInstance] ✅️ apply instMonadOption'.{?u.1460} to Monad.{?u.1460, ?u.1460} Option'.{?u.1460}
    [Meta.synthInstance.tryResolve] ✅️ Monad.{?u.1460, ?u.1460}
          Option'.{?u.1460} ≟ Monad.{?u.1460, ?u.1460} Option'.{?u.1460}
    [Meta.synthInstance.answer] ✅️ Monad.{?u.1460, ?u.1460} Option'.{?u.1460}
  [Meta.synthInstance.resume] propagating Monad.{?u.1460, ?u.1460}
        Option'.{?u.1460} to subgoal Monad.{?u.1460, ?u.1460}
        Option'.{?u.1460} of Applicative.{?u.1460, ?u.1460} Option'.{?u.1460}
    [Meta.synthInstance.resume] size: 1
    [Meta.synthInstance.answer] ✅️ Applicative.{?u.1460, ?u.1460} Option'.{?u.1460}
  [Meta.synthInstance.resume] propagating Applicative.{?u.1460, ?u.1460}
        Option'.{?u.1460} to subgoal Applicative.{?u.1460, ?u.1460}
        Option'.{?u.1460} of Seq.{?u.1460, ?u.1460} Option'.{?u.1460}
    [Meta.synthInstance.resume] size: 2
    [Meta.synthInstance.answer] ✅️ Seq.{?u.1460, ?u.1460} Option'.{?u.1460}
  [Meta.synthInstance] result @Applicative.toSeq.{?u.1460, ?u.1460} Option'.{?u.1460}
        (@Monad.toApplicative.{?u.1460, ?u.1460} Option'.{?u.1460} instMonadOption'.{?u.1460})
[Meta.synthInstance] ✅️ SeqLeft.{?u.1460, ?u.1460} Option'.{?u.1460}
  [Meta.synthInstance] new goal SeqLeft.{?u.1460, ?u.1460} Option'.{?u.1460}
    [Meta.synthInstance.instances] #[@Applicative.toSeqLeft.{?u.1539, ?u.1540}]
  [Meta.synthInstance] ✅️ apply @Applicative.toSeqLeft.{?u.1460,
          ?u.1460} to SeqLeft.{?u.1460, ?u.1460} Option'.{?u.1460}
    [Meta.synthInstance.tryResolve] ✅️ SeqLeft.{?u.1460, ?u.1460}
          Option'.{?u.1460} ≟ SeqLeft.{?u.1460, ?u.1460} Option'.{?u.1460}
    [Meta.synthInstance] new goal Applicative.{?u.1460, ?u.1460} Option'.{?u.1460}
      [Meta.synthInstance.instances] #[@Monad.toApplicative.{?u.1546,
              ?u.1547}, @Alternative.toApplicative.{?u.1548, ?u.1549}]
  [Meta.synthInstance] ✅️ apply @Alternative.toApplicative.{?u.1460,
          ?u.1460} to Applicative.{?u.1460, ?u.1460} Option'.{?u.1460}
    [Meta.synthInstance.tryResolve] ✅️ Applicative.{?u.1460, ?u.1460}
          Option'.{?u.1460} ≟ Applicative.{?u.1460, ?u.1460} Option'.{?u.1460}
    [Meta.synthInstance] no instances for Alternative.{?u.1460, ?u.1460} Option'.{?u.1460}
      [Meta.synthInstance.instances] #[]
  [Meta.synthInstance] ✅️ apply @Monad.toApplicative.{?u.1460,
          ?u.1460} to Applicative.{?u.1460, ?u.1460} Option'.{?u.1460}
    [Meta.synthInstance.tryResolve] ✅️ Applicative.{?u.1460, ?u.1460}
          Option'.{?u.1460} ≟ Applicative.{?u.1460, ?u.1460} Option'.{?u.1460}
    [Meta.synthInstance] new goal Monad.{?u.1460, ?u.1460} Option'.{?u.1460}
      [Meta.synthInstance.instances] #[instMonadOption'.{?u.1556}]
  [Meta.synthInstance] ✅️ apply instMonadOption'.{?u.1460} to Monad.{?u.1460, ?u.1460} Option'.{?u.1460}
    [Meta.synthInstance.tryResolve] ✅️ Monad.{?u.1460, ?u.1460}
          Option'.{?u.1460} ≟ Monad.{?u.1460, ?u.1460} Option'.{?u.1460}
    [Meta.synthInstance.answer] ✅️ Monad.{?u.1460, ?u.1460} Option'.{?u.1460}
  [Meta.synthInstance.resume] propagating Monad.{?u.1460, ?u.1460}
        Option'.{?u.1460} to subgoal Monad.{?u.1460, ?u.1460}
        Option'.{?u.1460} of Applicative.{?u.1460, ?u.1460} Option'.{?u.1460}
    [Meta.synthInstance.resume] size: 1
    [Meta.synthInstance.answer] ✅️ Applicative.{?u.1460, ?u.1460} Option'.{?u.1460}
  [Meta.synthInstance.resume] propagating Applicative.{?u.1460, ?u.1460}
        Option'.{?u.1460} to subgoal Applicative.{?u.1460, ?u.1460}
        Option'.{?u.1460} of SeqLeft.{?u.1460, ?u.1460} Option'.{?u.1460}
    [Meta.synthInstance.resume] size: 2
    [Meta.synthInstance.answer] ✅️ SeqLeft.{?u.1460, ?u.1460} Option'.{?u.1460}
  [Meta.synthInstance] result @Applicative.toSeqLeft.{?u.1460, ?u.1460} Option'.{?u.1460}
        (@Monad.toApplicative.{?u.1460, ?u.1460} Option'.{?u.1460} instMonadOption'.{?u.1460})
[Meta.synthInstance] ✅️ SeqRight.{?u.1460, ?u.1460} Option'.{?u.1460}
  [Meta.synthInstance] new goal SeqRight.{?u.1460, ?u.1460} Option'.{?u.1460}
    [Meta.synthInstance.instances] #[@Applicative.toSeqRight.{?u.1558, ?u.1559}]
  [Meta.synthInstance] ✅️ apply @Applicative.toSeqRight.{?u.1460,
          ?u.1460} to SeqRight.{?u.1460, ?u.1460} Option'.{?u.1460}
    [Meta.synthInstance.tryResolve] ✅️ SeqRight.{?u.1460, ?u.1460}
          Option'.{?u.1460} ≟ SeqRight.{?u.1460, ?u.1460} Option'.{?u.1460}
    [Meta.synthInstance] new goal Applicative.{?u.1460, ?u.1460} Option'.{?u.1460}
      [Meta.synthInstance.instances] #[@Monad.toApplicative.{?u.1565,
              ?u.1566}, @Alternative.toApplicative.{?u.1567, ?u.1568}]
  [Meta.synthInstance] ✅️ apply @Alternative.toApplicative.{?u.1460,
          ?u.1460} to Applicative.{?u.1460, ?u.1460} Option'.{?u.1460}
    [Meta.synthInstance.tryResolve] ✅️ Applicative.{?u.1460, ?u.1460}
          Option'.{?u.1460} ≟ Applicative.{?u.1460, ?u.1460} Option'.{?u.1460}
    [Meta.synthInstance] no instances for Alternative.{?u.1460, ?u.1460} Option'.{?u.1460}
      [Meta.synthInstance.instances] #[]
  [Meta.synthInstance] ✅️ apply @Monad.toApplicative.{?u.1460,
          ?u.1460} to Applicative.{?u.1460, ?u.1460} Option'.{?u.1460}
    [Meta.synthInstance.tryResolve] ✅️ Applicative.{?u.1460, ?u.1460}
          Option'.{?u.1460} ≟ Applicative.{?u.1460, ?u.1460} Option'.{?u.1460}
    [Meta.synthInstance] new goal Monad.{?u.1460, ?u.1460} Option'.{?u.1460}
      [Meta.synthInstance.instances] #[instMonadOption'.{?u.1575}]
  [Meta.synthInstance] ✅️ apply instMonadOption'.{?u.1460} to Monad.{?u.1460, ?u.1460} Option'.{?u.1460}
    [Meta.synthInstance.tryResolve] ✅️ Monad.{?u.1460, ?u.1460}
          Option'.{?u.1460} ≟ Monad.{?u.1460, ?u.1460} Option'.{?u.1460}
    [Meta.synthInstance.answer] ✅️ Monad.{?u.1460, ?u.1460} Option'.{?u.1460}
  [Meta.synthInstance.resume] propagating Monad.{?u.1460, ?u.1460}
        Option'.{?u.1460} to subgoal Monad.{?u.1460, ?u.1460}
        Option'.{?u.1460} of Applicative.{?u.1460, ?u.1460} Option'.{?u.1460}
    [Meta.synthInstance.resume] size: 1
    [Meta.synthInstance.answer] ✅️ Applicative.{?u.1460, ?u.1460} Option'.{?u.1460}
  [Meta.synthInstance.resume] propagating Applicative.{?u.1460, ?u.1460}
        Option'.{?u.1460} to subgoal Applicative.{?u.1460, ?u.1460}
        Option'.{?u.1460} of SeqRight.{?u.1460, ?u.1460} Option'.{?u.1460}
    [Meta.synthInstance.resume] size: 2
    [Meta.synthInstance.answer] ✅️ SeqRight.{?u.1460, ?u.1460} Option'.{?u.1460}
  [Meta.synthInstance] result @Applicative.toSeqRight.{?u.1460, ?u.1460} Option'.{?u.1460}
        (@Monad.toApplicative.{?u.1460, ?u.1460} Option'.{?u.1460} instMonadOption'.{?u.1460})


#check
Lean.Elab.Term.elabLetDecl : Lean.Elab.Term.TermElab 
Lean.Elab.Term.elabLetDecl: Lean.Elab.Term.TermElab
Lean.Elab.Term.elabLetDecl
#check
Lean.Elab.Term.elabLetRec : Lean.Elab.Term.TermElab 
Lean.Elab.Term.elabLetRec: Lean.Elab.Term.TermElab
Lean.Elab.Term.elabLetRec
#check
Lean.Elab.Structural.preprocess (e : Lean.Expr) (recFnNames : Array.{0} Lean.Name) : Lean.Core.CoreM Lean.Expr 
Lean.Elab.Structural.preprocess: Lean.Expr → Array.{0} Lean.Name → Lean.Core.CoreM Lean.Expr
Lean.Elab.Structural.preprocess
#check
Lean.Elab.Command.elabDeclaration : Lean.Elab.Command.CommandElab 
Lean.Elab.Command.elabDeclaration: Lean.Elab.Command.CommandElab
Lean.Elab.Command.elabDeclaration