return type and coercions
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