Engine: `Concrete` `ImplExpr`s are not imported correctly

[paulmure]

Consider this example:

trait Foo {
    fn do_thing(self: &Self) -> u64;
}

struct Bar {
    n: u64,
}

impl Foo for Bar {
    fn do_thing(self: &Self) -> u64 {
        self.n
    }
}

fn call_foo<F: Foo>(foo: &F) -> u64 {
    foo.do_thing()
}

fn use_bar() -> u64 {
    let b = Bar { n: 42 };
    call_foo(&b)
}

One of the trait bounds in the call to call_foo in the function use_bar is the fact that Bar implements Foo.

This information is exported as an ImplExpr::Concrete. The exported json looks something like this:

{
  "trait": {
    "def_id": {
      "krate": "scratch",
      "path": [
        {
          "data": {
            "TypeNs": "Foo"
          },
          "disambiguator": 0
        }
      ],
      "index": [
        0,
        3
      ]
    },
    "generic_args": [
      {
        "Type": {
          "Adt": {
            "generic_args": [],
            "trait_refs": [],
            "def_id": {
              "krate": "scratch",
              "path": [
                {
                  "data": {
                    "TypeNs": "Bar"
                  },
                  "disambiguator": 0
                }
              ],
              "index": [
                0,
                5
              ]
            }
          }
        }
      }
    ]
  },
  "impl": {
    "Concrete": {
      "id": {
        "krate": "scratch",
        "path": [
          {
            "data": "Impl",
            "disambiguator": 0
          }
        ],
        "index": [
          0,
          7
        ]
      },
      "generics": []
    }
  },
  "args": []
}

The information about what type was used to implement what trait is stored in the trait field, whereas the impl field stores some useless marker.

The importer incorrectly imports the impl field as the final trait goal. Resulting in a junk impl_expr like this:

[
  "Concrete",
  {
    "trait": {
      "def_id": {
        "krate": "scratch",
        "path": [
          {
            "data": [
              "Impl"
            ],
            "disambiguator": 0
          }
        ]
      },
      "kind": [
        "Impl"
      ]
    },
    "args": []
  }
]

[W95Psp]

Hi, what you say here is that you want the information "what is the trait being used" rather than "what impl block is being used"? That's what I understand from the examples you give.

The scratch::Impl#0 is not a useless marker, it is where the impl is actually defined.

Maybe what we need here is to store both trait and impl info in the AST, wdyt?

[paulmure]

Hi, what you say here is that you want the information "what is the trait being used" rather than "what impl block is being used"? That's what I understand from the examples you give.

The scratch::Impl#0 is not a useless marker, it is where the impl is actually defined.

Maybe what we need here is to store both trait and impl info in the AST, wdyt?

I see, my misunderstanding then, thanks for pointing that out. Yes, I think we need both information about what impl block is used as well as the trait goal.

I will update the PR then. Since we will preserve both information, I should be able to make the old tests pass.

[franziskuskiefer]

This may be already fixed. Please check and close, or describe what's not working.