Aleksander Boruch-Gruszecki

I don't see a good way of making this example work, unfortunately. Pattern matching can't really reconstruct the bound `M = Succ[predM]` simply from `m : M` matching `Succ(predM)`, since...

Alternatively, we will soon be merging a PR where we will reconstruct the bound `m.type

Even if the pattern is `Succ(predM) : Succ[predM]`, we can't conclude that `M = Succ[predM]`. If not for the `proof` argument, we could have a call like this one: ```scala...

The PR I mentioned is https://github.com/lampepfl/dotty/pull/14754 .

The return type is just one way to use the reconstructed bound. In general it simply doesn't need to be the case that `X = String`, like the snippet shows....

@Bersier think about it this way: `X = T` is exactly the same as `X

It feels like the warning is a warning because we thought that indenting too much is harmless, but here the indentation is evidently misleading. One of the basic reasons we...

@pikinier20 It wasn't really a goal to be 100% compliant with the old parser. If you take a look at https://dotty.epfl.ch/docs/usage/scaladoc/linking.html, the extensions mentioned there are technically incompatible with the...

@bblfish DRI is internal Scala3doc terminology. I agree we should avoid it in the error message, it's certainly not helpful. We could just say that we failed to resolve a...

In your specific case, this one : ` run.cosy.http.headers.Rfc5234` ? If that's a valid identifier, then not looking it up is 100% a bug, please open an issue and someone...