Is Std.Internal.IO.Async.MonadAsync.toMonad a bad instance?

Stream: lean4

[Eric Wieser]

docs#Std.Internal.IO.Async.MonadAsync seems to break the rule of "a 2-ary typeclass should never extend a 1-ary one", as there is no way to determine what t should be used to find Monad m from MonadAsync t m:

Std.Internal.IO.Async.MonadAwait.toMonad (t : Type → Type) {m : Type → Type}
  [self : Std.Internal.IO.Async.MonadAwait t m] : Monad m

[Eric Wieser]

You can see this blow-up in action (on mathlib stable or the latest mathlib) in:

import Lake.Load.Resolve
import Std.Internal.Async.Basic

open Lake

variable {m} [Monad m] [MonadError m]

#synth MonadWorkspace (ResolveT m)

[Eric Wieser]

docs#Std.Internal.IO.Async.MonadAwait seems similarly bad

[Eric Wieser]

"the rule" I mention is the one in #mil; I've created https://github.com/avigad/mathematics_in_lean_source/pull/316 to track that the error message it reports seems to no longer occur.

[Eric Wieser]

cc @Anne Baanen, since I think your thesis discusses such instances

[Anne Baanen]

Yes, such extends clauses cause underdetermined instances, and would generally be a bad idea unless t is a (semi)outparam. Normally this should cause an error "cannot find synthesization order for instance ... all remaining arguments have metavariables". Indeed if I make a declaration with the same type I see the error. Weird that the check does not seem to fire on the definition of MonadAsync.

[Eric Wieser]

cannot find synthesization order for instance ... all remaining arguments have metavariables

This error no longer files if you define Module this way either:

import Mathlib

class Module' (R : Type) [Ring R] (M : Type) extends AddCommGroup M, SMul R M where
  zero_smul : ∀ m : M, (0 : R) • m = 0
  one_smul : ∀ m : M, (1 : R) • m = m
  mul_smul : ∀ (a b : R) (m : M), (a * b) • m = a • b • m
  add_smul : ∀ (a b : R) (m : M), (a + b) • m = a • m + b • m
  smul_add : ∀ (a : R) (m n : M), a • (m + n) = a • m + a • n

[Jovan Gerbscheid]

I was working on a fix for this type class issue in lean#9638 (see also #lean4 > projection instance binderinfo problem ). And on the toolchain of that PR, the definition of MonadAwait indeed throws an error.

But the strange thing is that the CI on the PR was green, so I didn't notice this bad instance (I did notice some in Batteries and Mathlib). Is this some sort of bootstrapping thing where it doesn't do a second build?

[Jovan Gerbscheid]

The lack of this error message was introduced by lean#5376

[Jovan Gerbscheid]

Anyways, in this case I think the t argument in MonadAsync and MonadAwait should be a semiOutParam.

[Robin Arnez]

I'd actually argue that we shouldn't extend Monad in the first place but use [Monad m] - take something like
docs#Std.Internal.IO.Async.concurrentlyAll which already says [Monad m] [MonadAwait t m] [MonadAsync t m] which would be three different monad instances!

[Jovan Gerbscheid]

It has [MonadAwait Task m] [MonadAsync t m] [MonadAwait t m] [Monad m], so I'm counting 4 different monad instances :laughing:

But yes, if we ever want to combine [MonadAsync t m] and [MonadAwait t m], then these classes should certainly not extend Monad m.

[Henrik Böving]

CC @Sofia Rodrigues

[Sofia Rodrigues]

I opened PR #10173 that removes extends Monad from both type classes.

[Eric Wieser]

Probably it should be backported, since I assume these bad instances can impact more than just lake

[Markus Himmel]

Are you actively affected by this?

[Eric Wieser]

I don't know yet, but my understanding is that a backport (at least to 4.23.0) is as simple as adding a label

[Eric Wieser]

I understand backporting to 4.22.0 is more work

[Markus Himmel]

It's as simple as adding a label as long as you don't need an rc3.

[Eric Wieser]

I guess I'd advocate putting it on the branch in case something _else_ justifies a new RC release

[Markus Himmel]

Already done :)

[Eric Wieser]

What should the action be on https://github.com/avigad/mathematics_in_lean_source/pull/316 ?

[Eric Wieser]

Is the error message supposed to be produced?

[Jovan Gerbscheid]

Yes, the error message is supposed to be produced. This is part of the problem I wanted to fix.