Zulip Chat Archive

Stream: mathlib4

Topic: failed to synthesize instance Applicative id


Arien Malec (Dec 11 2022 at 02:04):

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 (Dec 11 2022 at 05:34):

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 (Dec 11 2022 at 16:17):

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

Does the documentation for id.mk need changing?

Arien Malec (Dec 11 2022 at 16:21):

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

Floris van Doorn (Dec 11 2022 at 16:26):

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

Arien Malec (Dec 11 2022 at 16:32):

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 (Dec 11 2022 at 19:07):

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

Arien Malec (Dec 11 2022 at 20:20):

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 (Dec 11 2022 at 20:24):

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

Winston Yin (Dec 14 2022 at 01:19):

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 (Dec 14 2022 at 02:36):

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 (Mar 11 2023 at 09:47):

This helped with !4#2804


Last updated: Dec 20 2023 at 11:08 UTC