Opened 6 years ago

Closed 6 years ago

#259 closed defect (fixed)

Well-formedness check for distinct witnesses is too weak.

Reported by: benl Owned by: tranma
Priority: blocker Milestone: 0.3.0
Component: Core Type Checker Version: 0.2.1
Keywords: Cc:

Description (last modified by tranma)

check..
/\(r1 r2 : %).
letregion r3 with {w : Distinct3 r1 r2 r3} in ();;

/\(r1 r2 : %).
letregion r3 with {w : Distinct3 r1 r2 r3} in
()
:*: [r1 r2 : %].Unit
:!: !0
:$: $0

Regions r1 and r2 might not be distinct.


fixed by making Distinctn for n > 2 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 at least safe. Distinct2 works as normal:

> :check..
letregion r1                             in
letregion r2 with { w1: Distinct2 r1 r2 } in ();;
letregion r1 in
letregion r2 with {w1 : Distinct2 r1 r2} in
()
:*: Unit
:!: !0
:$: $0

Change History (5)

comment:1 Changed 6 years ago by benl

  • Component changed from Unknown to Core Type Checker

comment:2 Changed 6 years ago by benl

  • Priority changed from high to blocker

comment:3 Changed 6 years ago by tranma

To check if it is possible to construct a witness of type Distinctn r0 ... rn, the type checker will have to prove distinctness for all pairs of regions. The simplest way to do this is to search the environment for any witnesses in scope that can prove the property. For example to construct Distinct4 r0 r1 r2 r3 we need either Distinct3 r0 r1 r2 or (Distinct r1 r2) ∧ (Distinct r2 r3). This results in a combinatorial explosion, yikes!

For now we will restrict Distinctn to only be allowed in the letregions introducing all the arguments needed, e.g. letregions r0 r1 r2 with { w : Distinct3 r0 r1 r2 } in ...

comment:4 Changed 6 years ago by tranma

  • Status changed from new to assigned

comment:5 Changed 6 years ago by tranma

  • Description modified (diff)
  • Resolution set to fixed
  • Status changed from assigned to closed
Note: See TracTickets for help on using tickets.