Misc.hs

-----------------------------------------------------------------------------
-- |
-- Module    : TestSuite.CantTypeCheck.Misc
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Test suite for things that should not type-check
-----------------------------------------------------------------------------

{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE FlexibleInstances    #-}

-- Defer type-errors is essential here!
{-# OPTIONS_GHC -Wall -Werror -Wno-orphans -Wno-deferred-type-errors -fdefer-type-errors #-}

module TestSuite.CantTypeCheck.Misc(tests) where

import Control.DeepSeq (NFData(..))
import Utils.SBVTestFramework

-- Only used safely!
import System.IO.Unsafe(unsafePerformIO)
instance NFData (IO Bool) where
  rnf iob = rnf (unsafePerformIO iob) `seq` ()

type Val = (Integer, Integer)

instance Num Val where
  (+)         = undefined
  (*)         = undefined
  (-)         = undefined
  signum      = undefined
  abs         = undefined
  fromInteger = undefined

tests :: TestTree
tests = testGroup "CantTypeCheck.Misc" [
           testCase "noTypeCheckBad01"  $ shouldNotTypeCheck $ isTheorem t1
         , testCase "noTypeCheckBad02"  $ shouldNotTypeCheck $ isTheorem t2
         , testCase "noTypeCheckBad03"  $ shouldNotTypeCheck   runSko
         , testCase "noTypeCheckBad04"  $ shouldNotTypeCheck   runNoNum
         , testCase "noTypeCheckGood01" $                      assertIsSat t1
         , testCase "noTypeCheckGood02" $                      assertIsSat t2

         -- Just so we got something other than our stuff..
         , testCase "noTypeCheck05"     $ shouldNotTypeCheck (1 :: String)
         ]
  where t1 :: SInteger -> ConstraintSet
        t1 x = do { constrain ( x .> (5::SInteger)) }

        t2 :: ConstraintSet
        t2 = pure ()

        -- shouldn't be able to skolemize like this
        sko :: Forall "y" Integer -> SInteger
        sko = skolemize fml
          where fml :: Exists "x" Integer -> Forall "y" Integer -> SInteger
                fml (Exists x) (Forall y) = x + y

        -- We have to reduce the above to a IO Bool so the rnf instance does the right thing!
        -- Oh the horrors of "deferring type errors"
        runSko :: IO Bool
        runSko = isSatisfiable $ sko (Forall (literal 3))

        -- can't add SBV Val
        noNumSBV :: SBV Val -> SBV Val -> SBV Val
        noNumSBV x y = x + y

        runNoNum :: IO Bool
        runNoNum = isSatisfiable noNumSBV