Bind methods in pure

[Nadrieril]

The last few Charon PRs made it so we can support cases where the generics for a method fn item aren't a simple concatenation of the trait_decl/trait_impl generics + the method generics. I hadn't yet propagated these changes into Pure; this PR does that. This happens to simplify the extraction of impl methods quite a bit because we now have the correct explicit_info available.

For simplicity I did not attempt to make the de_bruijn_ids correct in Pure since we don't need them to be. I commented the relevant places appropriately so we know what's happening if we end up needing more complex binding situations in the future.

[sonmarcho]

Looks good! Checking that I understand: the generic_origin is useful only when extracting trait impls, because there we do need two levels of bindings, one for the generics bound at the level of the trait impl, and another at the level of the item itself, like so:

struct FooImpl T { (* Item level *)
    f = fun U -> f0 T U (* Method level *)
}

Correct?

[Nadrieril]

the generic_origin is useful only when extracting trait impls

There are also two levels of bindings in trait decls:

Record OfType_t (Self : Type) := mkOfType_t { (* Item level *)
  OfType_t_of_type : forall {T : Type} (toTypeInst : ToType_t T Self), T ->  (* Method level *)
    result Self;
}.

but yes that's exactly the idea.