Mentions légales du service

Skip to content
Snippets Groups Projects
Closed return type and coercions
  • View options
  • return type and coercions

  • View options
  • Closed Issue created by Jean-Christophe Filliâtre

    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

    Edited by Guillaume Melquiond

    Linked items ... 0

  • Activity

    • All activity
    • Comments only
    • History only
    • Newest first
    • Oldest first
    Loading Loading Loading Loading Loading Loading Loading Loading Loading Loading