Monad instance complains about missing fields

Stream: new members

[jthulhu]

I am trying to create a product monad from two monads:

def Product (m₁ : Type → Type) (m₂ : Type → Type) (α : Type) : Type := (m₁ α) × (m₂ α)

instance [Monad m₁] [Monad m₂] : Monad (Product m₁ m₂) where
  pure x := (pure x, pure x)
  bind o f :=
    let y₁ := do
      let y ← o.1
      f y |>.1
    let y₂ := do
      let y ← o.2
      f y |>.2
    (y₁, y₂)

I thought it was enough to provide the pure and bind implementations to define the instance. Yet, lean complains that fields missing: 'map', 'mapConst', 'seq', 'seqLeft'. I have tried to create other monad instances, again providing only the pure and bind implementations, and it worked. I don't understand why, in this particular example, it doesn't work.

[Eric Wieser]

Something weird is definitely going on here. This works:

instance [Pure m₁] [Pure m₂] : Pure (Product m₁ m₂) where pure x := (pure x, pure x)
instance [Bind m₁] [Bind m₂] : Bind (Product m₁ m₂) where bind o f :=
    let y₁ := do
      let y ← o.1
      f y |>.1
    let y₂ := do
      let y ← o.2
      f y |>.2
    (y₁, y₂)

instance [Monad m₁] [Monad m₂] : Monad (Product m₁ m₂) where

[Eric Wieser]

As does

instance [Monad m₁] [Monad m₂] : Monad (Product m₁ m₂) where
  pure x := (pure x, pure x)
  bind o f := (do f (← o.1) |>.1, do f (← o.2) |>.2)

[jthulhu]

Extracting the definitions also seems to solve the issue:

def Product.pure [ι₁ : Monad m₁] [ι₂ : Monad m₂] {α : Type} (x : α) := (ι₁.pure x, ι₂.pure x)
def Product.bind [Monad m₁] [Monad m₂] {α β : Type} (x : Product m₁ m₂ α) (f : α → Product m₁ m₂ β) :=
  let y₁ := do
    let y ← x.1
    f y |>.1
  let y₂ := do
    let y ← x.2
    f y |>.2
  (y₁, y₂)

instance [Monad m₁] [Monad m₂] : Monad (Product m₁ m₂) where
  pure := Product.pure
  bind := Product.bind

although in this case, for the pure definition, I have to explicitly name the instances. I assume this is because the definition happens in the Product namespace, and therefore the pure defintion shadows the standard library's pure.

[Eric Wieser]

Use nonrec def or protected defto avoid that