failed to synthesize instance Applicative id

Stream: mathlib4

[Arien Malec]

I have a port in progress (mathlib4#948) that has most of the failures with the above message; it's confusing because the docu for id.mk states that this is Pure for id as an Applicative, but I don't see an instance definition of Monad etc for id (for Id, yes); these are definitions that worked in Lean 3...

[Reid Barton]

In this context (and probably any other one in which id.mk appears) I think it would be appropriate to replace Lean 3 id by Lean 4 Id.

[Arien Malec]

Id.run I assume provides the id-like identity map?

Does the documentation for id.mk need changing?

[Arien Malec]

No, b/c Id.run has the wrong signature... ugh.

[Floris van Doorn]

I think the docstring of id.mk should be fixed. id is not registered as a monad in Lean 4, Id is.

[Arien Malec]

I'll do a PR here. Now I'm getting mixed up where Id.pure should provide the identity function but Lean 4 complains that Id.pure doesn't exist...

[Kevin Buzzard]

In Control.Traversable.Basic I used (pure : α → Id α)

[Arien Malec]

Any downside to solving the problem like:

instance hasFunctor_id : Functor id where
  map := id.mk

instance hasApplicative_id: Applicative id where
  pure := id.mk
  seq f x := f (x ())

instance hasMonad_id: Monad id where
  pure := id.mk
  bind x f := f x

[Reid Barton]

I think id is intentionally not any of those things--you're supposed to use Id for them instead

[Winston Yin]

For future reference, id no longer has a Monad instance. Instead, we have the Id, which specifically acts on Types and does have a Monad instance. I've changed id.mk to pure, sometimes needing to write (m := Id) to help Lean find Monad Id. With these, mathlib4#948 is now ready, I believe

[Arien Malec]

Thanks -- sorry, lost time to work on this but don't think I'd ever have hit on m := Id -- had tried many combinations of Id, pure, etc. to see what stuck.

[Jeremy Tan]

This helped with !4#2804