`impl Trait` generates incorrect coma code

[arnaudgolfouse]

The following:

fn f(x : impl Clone) {}

Causes creusot to generate an incorrect coma declaration:

module Myfile_F
  type impl clone
  (* ... *)
  let rec f (x : impl clone) = (* ... *)
end

This is a syntax error on both lines.

We should either accept this by changing the generated name, or raise an error on compilation.

[xldenis]

oh, yes we should definitely raise an error on compilation, I've never looked into implementing support for impl trait, though I suspect it wouldn't be particularly challenging.

[jhjourdan]

I'm not asking to implement that, but in argument position I don't expect this to be very hard, since (I think) this could be encoded using generics.

That's an other story in return position: we would have to consider the type and its impls to be opaque.

[xldenis]

I'm not asking to implement that, but in argument position I don't expect this to be very hard, since (I think) this could be encoded using generics.

Agreed. However, we don't really use generics for functions, instead we create a new opaque type for each generic parameter (which works perfectly for impl trait). This would work as well when calling functions which return impl trait types.

When verifying such functions we would need to behave differently (aka operate in "Reveal" mode I think) to see the definition of the impl trait.