Quantification over user-defined types

[LeventErkok]

Here's an example. Note that this is a bit mouthful. It is possible to define mkConstraint/skolemize etc. to make this look pretty, but unless we add some generic way of making general product types usable this way, it's probably too advanced for most users. Something to think about.

At the least, we should put this into documentation somewhere:

{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE OverloadedRecordDot #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module T(main) where

import Data.SBV

import GHC.TypeLits

data T f a = T { foo :: f a
               , bar :: f a
               }

type ST = T SBV

newtype ExistsT (nm :: Symbol) a = ExistsT (ST a)
existsT :: KnownSymbol nm
        => (ExistsT nm a -> b)
        -> Exists (AppendSymbol nm "_foo") a
        -> Exists (AppendSymbol nm "_bar") a
        -> b
existsT f = \(Exists tfoo) (Exists tbar) -> f (ExistsT T{foo = tfoo, bar = tbar})

newtype ForallT (nm :: Symbol) a = ForallT (ST a)
forallT :: KnownSymbol nm
        => (ForallT nm a -> b)
        -> Forall (AppendSymbol nm "_foo") a
        -> Forall (AppendSymbol nm "_bar") a
        -> b
forallT f = \(Forall tfoo) (Forall tbar) -> f (ForallT T{foo = tfoo, bar = tbar})

ex :: IO SatResult
ex = sat cstrs
  where cstrs :: ConstraintSet
        cstrs = constrain $ skolemize prop

        prop = forallT $ \(ForallT @"at" at) -> existsT $ \(ExistsT @"et" et) -> check at et
          where check at et = at.foo + at.bar .== et.foo + (et.bar :: SInteger)

main :: IO ()
main = print =<< ex

This prints:

*T> main
Satisfiable. Model:
  et_bar :: Integer -> Integer -> Integer
  et_bar _ _ = 0

  et_foo :: Integer -> Integer -> Integer
  et_foo at_foo at_bar = at_foo + at_bar

[LeventErkok]

Here's one attempt to do generic types. Though how this fits into existing SBV requires more experimentation:

{-# LANGUAGE DefaultSignatures    #-}
{-# LANGUAGE DeriveAnyClass       #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE UndecidableInstances #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module T where

import qualified GHC.Generics as G

data SBV a = SBV a
  deriving Show

type family SymRep a where
  SymRep Int = Int
  SymRep a   = G.Rep a a

class SymVal a where
  literal   :: a -> SBV (SymRep a)
  unliteral :: SBV (SymRep a) -> Maybe a

  default literal :: (G.Generic a, SymRep a ~ G.Rep a f) => a -> SBV (SymRep a)
  literal a = SBV (G.from a)

  default unliteral :: (G.Generic a, SymRep a ~ G.Rep a f) => SBV (SymRep a) -> Maybe a
  unliteral (SBV a) = Just (G.to a)

data T = T1 { a :: Int
            , b :: Int
            }
       | T2 Bool
       deriving (Show, G.Generic, SymVal)

instance SymVal Int where
  literal = SBV
  unliteral (SBV i) = Just i

You can try:

*T> literal (T1 2 3)
SBV (M1 {unM1 = L1 (M1 {unM1 = M1 {unM1 = K1 {unK1 = 2}} :*: M1 {unM1 = K1 {unK1 = 3}}})})
*T> unliteral (literal (T1 2 3)) :: Maybe T
Just (T1 {a = 2, b = 3})

[LeventErkok]

This requires changing SymVal class, so representation type can differ from the type itself. Which is probably how it should've been designed in the first place. Alas, too late for that,.