search

flux-rs / flux

Refinement Types for Rust
MIT License
632 stars 17 forks source link

Improvements to `extern_spec` #575

Closed ranjitjhala closed 8 months ago

ranjitjhala commented 9 months ago

That allow, refining (impl of) types with

  1. Default type parameters,
  2. Bounds in type parameters,
  3. Multiple impl blocks

See

Lots of broken things remain (see TODO)

ranjitjhala commented 8 months ago

@nilehmann I added some minor tweaks to support a bit of vec in case you want to check.

ranjitjhala commented 8 months ago

The error also happens with iterating over RSet .. wonder why not with RVec???

On Mon, Dec 18, 2023 at 2:51 PM Nico Lehmann @.***> wrote:

@.**** commented on this pull request.

In crates/flux-refineck/src/type_env.rs https://urldefense.com/v3/__https://github.com/flux-rs/flux/pull/575*discussion_r1430727280__;Iw!!Mih3wA!CjaZCkfTESuhewkELgkcMJxzAd3fUO1ay3ynfyloaC20KkJMjmgD2crjf3GySK2Z7-xRYXbwJmHW2fv4YUDzA7Gs$ :

@@ -508,8 +508,8 @@ impl BasicBlockEnvShape { (GenericArg::BaseTy(), GenericArg::BaseTy()) => { tracked_span_bug!("generic argument join for base types is not implemented") }

  • (GenericArg::Lifetime(re1), GenericArg::Lifetime(re2)) => {
  • debug_assert_eq!(re1, re2);
  • (GenericArg::Lifetime(re1), GenericArg::Lifetime(_re2)) => {
  • // CHECK: debug_assert_eq!(re1, re2);

Just realize this is inside join and not subtyping. This feels bad. Can you minimize an example that needs this change?

— Reply to this email directly, view it on GitHub https://urldefense.com/v3/__https://github.com/flux-rs/flux/pull/575*pullrequestreview-1787834694__;Iw!!Mih3wA!CjaZCkfTESuhewkELgkcMJxzAd3fUO1ay3ynfyloaC20KkJMjmgD2crjf3GySK2Z7-xRYXbwJmHW2fv4YWluFoTM$, or unsubscribe https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OH3WXNOWKV2Z3YOLWLYKDCHNAVCNFSM6AAAAABASNZM36VHI2DSMVQWIX3LMV43YUDVNRWFEZLROVSXG5CSMV3GSZLXHMYTOOBXHAZTINRZGQ__;!!Mih3wA!CjaZCkfTESuhewkELgkcMJxzAd3fUO1ay3ynfyloaC20KkJMjmgD2crjf3GySK2Z7-xRYXbwJmHW2fv4YXqRbbGe$ . You are receiving this because you authored the thread.Message ID: @.***>

ranjitjhala commented 8 months ago

ok let me revert that assert and the associated tests; its orthogonal to this PR anyways, so I've made a separate issue.