Problems with MonadLift Id m

Stream: batteries

[Paul Reichert]

@Robin Arnez noticed that the MonadLift Id m instance has some problems. The gist:

• This instance is tried lots of times whenever a MonadListT instance is being synthesized.
• It also causes lots of non-canonical instances -- at least one non-canonical instance for every MonadList instance.

I wonder what we could do to improve this situation. Robin has made an interesting suggestion: If we only provide a (high-priority) MonadLiftT Id m instance (T), the first problem disappears and the second problem hopefully less worse due to the priority.

This proposal makes a lot of sense and I think this is by far the best idea I know regarding how to address this issue, but it still has problems. I don't like that we manually create a MonadLiftT instance, even though the docstring says that MonadLiftT is the reflexive-transitive closure of MonadLift. The part about using priorities to handle canonicity violations might work but could be a bit fragile.

Hence, I'd like to ask you all to think about MonadLift Id m. What would be the best way forward in your opinion?

[Quang Dao]

Is it even possible to make the instance canonical?

I agree with your solution, though my knowledge of this topic is very limited

[François G. Dorais]

This is similar to the Coe mayhem from long ago. The solution there was a complex web of classes: https://github.com/leanprover/lean4/blob/1e752b0a01bafdbcea6496ac4add09226b92aa99/src/Init/Coe.lean#L12

MonadLift probably doesn't need as complex solution (at least not right now). The first attempt at solving the Coe problem was to insert some problematic coercions directly in CoeT, which is similar to what is proposed. That can probably work for a while, as it did for Coe. Anyway, I think it's worthwhile to revisit the Coe story to avoid early mistakes.

[Paul Reichert]

Interesting, thanks for the backstory.

[Jovan Gerbscheid]

Even worse than causing non-canonical instances, the instance MonadLift Id m causes a looping instance search (which doesn't loop forever in lean4 luckily). It seems that the CoeTail class was made to solve this problem for coercions. So I think the same can be done here, making a MonadLiftTail class, with the instance MonadLiftTail Id m. And then the current MonadLiftT should be renamed to MonadLiftTC, and we define the class MonadLiftT to have an instance coming either directly from MonadLiftTC, or from that combined with MonadLiftTail. So then if we really wanted, we could chain MonadLiftTail Id m with an instance of MonadLift _ Id.

[Robin Arnez]

Is there a reason to though? Using Tail implies that there would be a situation where you would want to lift to Id (and then use the Tail to lift into an arbitrary monad). However, Id doesn't have any inner monads so using it in MonadLiftT should be enough.

[François G. Dorais]

After this discussion, I think batteries#1242 should be closed in favor of a core solution. Agreed?

[Paul Reichert]

Note that this is a PR into a PR-testing branch. The base PR upstreamed LawfulMonadLift into core, initially originally including MonadLift Id m. However, having noticed its complications and having removed MonadLift Id m from the upstreaming PR, I strongly prefer decoupling these topics instead of piggybacking on the LawfulMonadLift topic. That's why said PR reverts the deletion of MonadLift Id m in Batteries as part of the (yet unmerged) PR-testing branch.

Right now, Batteries contains MonadLift Id m. Just closing above PR will have the effect of actively deleting it from Batteries with the next toolchain bump, without solving the problem that there's no core solution yet.

[Paul Reichert]

Update: I turns out that Batteries already has been bumped. (It was probably not a good idea to merge the lean4 PR without waiting for the PR-testing pull request being accepted, sorry!) Closed it now and opened a new PR restoring the instance: https://github.com/leanprover-community/batteries/pull/1259

Because some people might depend on this instance, I think we should restore the old instance and can improve it afterwards.

[François G. Dorais]

Note that PRs marked WIP never get merged.

[François G. Dorais]

I don't see why reintroducing this instance is necessary. Nobody has complained that it went missing.

[Paul Reichert]

My bad regarding the WIP label! Besides that, it would be fine for me to close 1259 if you think that the instance isn't needed. (Update: Closed for now.)