Using uninterpreted types/functions to simulate fake polymorphism

gistfile1.hs

{-# LANGUAGE DeriveDataTypeable   #-}

import Data.SBV
import Data.Generics

-- boilerplate to get A to be an SMT-Lib uninterpreted sort
data A = A () deriving (Eq, Ord, Data, Typeable, Read, Show)
instance SymWord A
instance HasKind A
type SA = SBV A

-- define the various injections we'd like to use:
class ToA x where
  toA :: SBV x -> SA

instance ToA Integer where toA = uninterpret "int2A"
instance ToA Bool    where toA = uninterpret "bool2A"

-- This is the prop function that works over the uninterpreted sort A
prop :: SA -> SBool
prop = uninterpret "prop"

-- Get a simple sat result; note the explicit injections
test :: IO SatResult
test = sat $ do x1 <- sInteger "x1"
                x2 <- sBool    "x2"
                return $ prop (toA x1) &&& prop (toA x2)