Yichen Xu

Thanks for your interest in our work! We'll check this soon.

Currently in #14754 we only record equalities between singleton types. So we will not record a constraint like `m.type // ... ``` we will be able to record the equality...

So to make the approach that changes the definition to `proof : m.type IsLessThan Succ[N]` to work, we would need `proof` typed as `proof : Succ[predM.type] isLessThan Succ[N]`, which would...

I checked this example again and found that we could add a type member to `NatT` indicating the 'precise' type of the value to make the snippet compile (with the...

Thanks for the fix! Although this does fix the issues, I think that freezing the GADT constraints when RHS is not an alias cannot cover all unsoundness problems here--since the...

Btw, I think we should keep the `tp1IsSingleton` check, since this at least prevents the unsound cases brought by upcasting singleton types. The following code, which is modified from the...

您好，`develop`分支仍在开发中，在合并入`main`分支后将发布新的`pypi`包。若你希望在现在就使用`develop`分支上的代码，可以`git clone`我们的仓库至本地，随后在仓库的目录内执行： ```bash pip install -e ./ ```

Hi! Glad to see this PR can benefit real-world development. It is currently blocked by #14776. This is a bug discovered when developing this PR and the tests currently broken...

Just verified that the following snippet compiles on this branch. :) ```scala trait T[X] case object Foo extends T[Unit] trait AsMember { type L val tl: T[L] } def testMember(am:...

test performance please