search

ucsd-progsys / liquid-fixpoint

Horn Clause Constraint Solving for Liquid Types
BSD 3-Clause "New" or "Revised" License
132 stars 60 forks source link

Crash during elaboration when projecting a `Set_Set` out of a polymorphic datatype #701

Closed nilehmann closed 2 weeks ago

nilehmann commented 2 weeks ago

The following

(datatype (MyData 1) ((mkdata ((field1 @(0))))))

(constraint
  (forall ((x (MyData (Set_Set int))) (true))
    ((= true (Set_mem 0 (field1 x))))
  )
)

crashes with

Crash!: :1:1-1:1: Error
  elaborate solver failed on:
      true == select (field1 x##1) 0
  with error
      Cannot unify (Array_t @(42)) with Set_Set in expression: select (field1 x##1) 
  in environment
      field1 := func(1 , [(MyData @(0)); @(0)])

      select := func(1 , [(Array_t @(0) bool); @(0); bool])

      x##1 := (MyData (Set_Set int))
CRASH: -1 : ""

If the datatype is not polymorphic I don't see the crash

(datatype (MyData 0) ((mkdata ((field1 (Set_Set int))))))

(constraint
  (forall ((x MyData) (true))
    ((= true (Set_mem 0 (field1 x))))
  )
)

Maybe related to https://github.com/ucsd-progsys/liquid-fixpoint/pull/688