GitLab

Coercions are not applied in this example, resulting in a type error:

let f () : (int63, int63)
  ensures { let x, y = result in x = 42 }
  = 42, 89

It looks like the postcondition is typed and then the type found for result (here (int, 'a)) is unified with the given return type (here (int63, int63)), resulting in a failure.

It would be more natural to give result the user-given type (when there is one) and then to type-check the postcondition. (It seems that the code at typing.ml:549 is precisely doing that, but apparently not; I surely missed something.)

Note: rather surprinsingly, there is no such issue with a simpler example where the return type is not a compound type:

let g () : int63 ensures { result = 42 } = 42

PS: to reproduce the issue, add a use import mach.int.Int63