Opened 6 years ago

Last modified 14 months ago

#281 new feature

Well-formedness check for distinct witnesses is too strict.

Reported by: tranma Owned by:
Priority: normal Milestone:
Component: Core Type Checker Version: 0.2.1
Keywords: distinct witness Cc:

Description (last modified by benl)

As a fix for #259, we made Distinctn stricter than necessary:

> :check..
letregion  r1 in
letregions r2 r3 with {w : Distinct3 r1 r2 r3} in ();;
When checking expression.
  Witness type is not for bound regions.
        letregion binds: r2 r3
    but witness type is: w : Distinct3 r1 r2 r3
  
  with: letregions r2 r3 with {w : Distinct3 r1 r2 r3} in
        ()

this is not ideal, but currently the only other alternative is to search the environment for witnesses that prove Distinctn-1.

Change History (4)

comment:1 Changed 6 years ago by benl

  • Description modified (diff)
  • Milestone changed from none to 0.4.0

comment:2 Changed 5 years ago by benl

  • Milestone 0.4.0 deleted

comment:3 Changed 21 months ago by benl

  • Owner tranma deleted

comment:4 Changed 14 months ago by benl

  • Type changed from enhancement to feature
Note: See TracTickets for help on using tickets.