Map measures also generate erroneous constraints when applied to non-polymorphic datatypes

[clayrat]

As expected, we can create a test case analogous to #2272 that crashes LH when working with Maps containing types that are not convertible to Int.

{-@ LIQUID "--reflection"     @-}

module PolyMapBug where

import Language.Haskell.Liquid.Bag

data Lst a = Emp | Cons a (Lst a)

{-@ measure lstHd @-}
lstHd :: Ord a => Lst a -> Bag a
lstHd  Emp       = empty
lstHd (Cons x _) = put x empty

{-@ lcons :: p: Lst l -> {v:Lst (Lst l) | v = Cons p Emp } @-}
lcons :: Lst l -> Lst (Lst l)
lcons p = Cons p Emp

This crashes with

crash: SMTLIB2 respSat = Error "line 3 column 34267: unknown constant smt_map_sel ((Array Int Int) (PolyMap.Lst Int)) declared: (declare-fun smt_map_sel ((Array Int Int) Int) Int) "

Since ucsd-progsys/liquid-fixpoint#688 deals only with Sets, this issue is intended to serve as a test case for a follow-up PR that would also elaborate the Map theory into Arrays.