Typechecking the following program:

{-@ LIQUID "--reflection" @-} module SngBug where import Data.Set data Lst a = Emp | Cons a (Lst a) {-@ measure lstHd @-} lstHd :: Ord a => Lst a -> Set a lstHd Emp = empty lstHd (Cons x _) = singleton x lcons :: Lst l -> Lst (Lst l) {-@ lcons :: p: Lst l -> {v:Lst (Lst l) | v = Cons p Emp } @-} lcons p = Cons p Emp

crashes with the error:

crash: SMTLIB2 respSat = Error "line 3 column 25217: unknown constant smt_set_sng ((SngBug.Lst Int)) declared: (declare-fun smt_set_sng (Int) (Array Int Bool)) "

The error disappears if lstHd is declared reflect instead of measure. It triggers both with and without PLE.

It looks like the internal Lst l type doesn't get converted to Int which is what the encoding of sets as Array Int Bool expects. We currently think there are two possible solutions for this:

1. Only generate set operations for elements whose type can be encoded as Int (simpler solution, will turn a crash into a proper typechecking error)
2. Generate multiple set types for each potential set element type (more complex, but allows for expressing more programs)