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)