Fix axiom and expr

package.yaml

@@ -81,6 +81,7 @@ library:
   - hashable
   - deepseq
   - bytestring
+  - time
 
 tests:
   pantomime-test:

pantomime.cabal

@@ -108,6 +108,7 @@ library
     , primitive
     , template-haskell
     , text
+    , time
     , transformers
     , unordered-containers
   default-language: Haskell2010

src/Pantomime/Axiom.hs

@@ -52,7 +52,7 @@ import GHC.Utils.Outputable
 
 import GHC.Exts (IsList (..))
 
-import Control.Monad ((>=>), guard, when)
+import Control.Monad ((>=>), guard)
 import Control.Applicative (Alternative (..))
 
 import Data.Data (Data)
@@ -348,9 +348,8 @@ resolvePluginAxioms PluginAxioms { .. } = do
     let dictEm' = maybe [] (: []) dictEm
     let dictsNew = dictCo' <> dictEm'
 
-    -- Throw an error if we could not create any.
-    when (null dictsNew) do
-      throwError @String "resolvePluginAxioms: could not create any Embeddable or Coercible dictionaries for the given axioms"
+    -- Skip if we could not create any dictionaries. This happens for
+    -- kind-polymorphic primitive TyCons like State#.
 
     -- Insert all dictionaries.
     pure $ foldlBy dicts dictsNew \acc dict -> do

src/Pantomime/Expr.hs

@@ -893,8 +893,24 @@ collectScrut = \case
       EnumCon _ tc | dc : _ <- tyConDataCons tc -> pure dc
       _ -> throwE @String "collectScrut: expected a DataCon or EnumCon with data constructors"
 
-    -- Push the coercion into the arguments.
-    (_univ, args') <- liftEff $ pushCoDataCon dc args co
+    -- Push the coercion into the arguments. When TyCons differ (e.g. because a
+    -- type axiom remapped Ptr to FakePtr), the data constructor's field
+    -- structure may not match the coercion target. Keep the original args in
+    -- that case.
+    let dcTyCon = dataConTyCon dc
+    let coTyCon = fmap fst (splitTyConApp_maybe (coercionRKind co))
+    (_univ, args') <-
+      if Just dcTyCon == coTyCon
+        then liftEff $ pushCoDataCon dc args co
+        else do
+          -- Skipping the coercion push is only safe when the data constructor
+          -- has no existential type variables. Otherwise, the field types
+          -- could reference those existentials and would need remapping.
+          let exVars = dataConExTyCoVars dc
+          unless (null exVars) $ throwE @String $
+            "collectScrut: cannot skip coercion push for data constructor with existential type variables: "
+            ++ GHC.showSDocUnsafe (GHC.ppr dc)
+          pure ([], drop (length (dataConUnivTyVars dc)) args)
     pure (Right spine', unthunk <$> args')
 
   -- If not a cast, we attempt to get the literal at the spine and return the
@@ -927,8 +943,6 @@ pushCoDataCon dc args co = do
   -- Check whether the outer type is a TyConAppCo.
   let tyR = coercionRKind co
   (tcR, univArgsR) <- failWith @String "pushCoDataCon: expected a TyConApp coercion" $ splitTyConApp_maybe tyR
-  unless (tcR == dataConTyCon dc) do
-    throwError @String "pushCoDataCon: TyCon mismatch in coercion"
 
   -- Gather information on type variables of the DataCon.
   let dcUnivVars = dataConUnivTyVars dc

src/Pantomime/Passes.hs

@@ -7,7 +7,7 @@
 import GHC.Core.Lint
 import GHC.Driver.Config.Core.Lint (initLintConfig)
 
 import GHC.Core.Make (mkStringExpr)
 
 import Grisette
   ( GrisetteSMTConfig (..)
@@ -20,6 +20,9 @@
 import Data.Traversable (for)
 import Data.Maybe (catMaybes)
 import Data.ByteString.Char8 qualified as BS8
+import Data.Time.Clock (getCurrentTime, diffUTCTime, UTCTime)
+import System.IO (hPutStrLn, stderr)
+import Text.Printf (printf)
 import Pantomime.Marker
 
 import Control.Error
@@ -144,10 +147,14 @@
   . runErrorWith @(LookupError TH.Name) propagateErrorShow
   where
     -- TODO: We could let the user decide which solver no?
+    -- Per-property timing is measured and reported explicitly in
+    -- 'checkValidityAndEmbed' instead, so each number is attributable to a
+    -- property name rather than relying on interleaved, unlabelled solver
+    -- output ('verbose'/'PrintTiming').
     solver = z3
       { sbvConfig = (sbvConfig z3)
-        { verbose = True
-        , timing = PrintTiming
+        { verbose = False
+        , timing = NoTiming
         }
       }
 
@@ -198,8 +205,16 @@
   debug res
   pure bind
 
+-- | Wall-clock milliseconds between two timestamps, for reporting per-property
+-- verification time. Printed to stderr as it is measured, rather than parsed
+-- out of the solver's own (unlabelled, interleaved) timing output, so each
+-- number can be attributed to the property that produced it.
+elapsedMs :: UTCTime -> UTCTime -> Double
+elapsedMs startTime endTime =
+  realToFrac (diffUTCTime endTime startTime) * 1000
+
 checkValidityAndEmbed
   :: ( HasCallStack
      , Error String :> es
      , Error (LookupError Name) :> es
      , Error (LookupError TH.Name) :> es
@@ -226,9 +241,13 @@
 
   (binds, results) <- fmap unzip $ for (mg_binds guts) \case
     NonRec x e | Just (Theory axioms) <- lookupUFM anns $ varName x -> do
+      let varNameStr = getOccString x
       axioms' <- resolvePluginAxioms axioms
+      startTime <- liftIO getCurrentTime
       mCounterexample <- checkValid axioms' e
-      let varNameStr = getOccString x
+      endTime <- liftIO getCurrentTime
+      liftIO $ hPutStrLn stderr $
+        printf "PANTOMIME-TIMING %s %.3fms" varNameStr (elapsedMs startTime endTime)
       case mCounterexample of
         Nothing -> do
           pure (NonRec x e, Just (varNameStr, Var nothingId))

src/Pantomime/Solve.hs

@@ -32,7 +32,7 @@
   , Bind (..)
   , Var
   , exprType
   , varType
   , vcat
   , emptyInScopeSet
   , getOccString
@@ -249,11 +249,13 @@
       -- TODO: I should probably check whether the arguments are recursive
       -- before printing? Alternatively, I could just have a maximum depth.
       args' <- inject args
-      let bindings = flip map args' \(bndr, arg) ->
-            let arg' = evalSym True model arg
-                name = getOccString bndr
-                value = showSDocUnsafe (pprArg id arg')
-            in (name, value)
+      -- Force each binding's value string fully here, so we can display the
+      -- counterexample.
+      bindings <- for args' \(bndr, arg) -> do
+        let arg' = evalSym True model arg
+            name = getOccString bndr
+            value = showSDocUnsafe (pprArg id arg')
+        length value `seq` pure (name, value)
       pure $ Just (Counterexample bindings)
     Unsatisfiable -> do
       dbg @SDoc "Expression was valid!"

src/Pantomime/Symbolise.hs

@@ -84,7 +84,13 @@ symbolise = go
           let dc = mkDataCon @64 GHC.unitDataCon
           pure $ mkCon dc
 
-        -- TODO: Give this a proper error.
+        -- Variables of type `forall a. a` are error/bottom functions
+        -- (overflowError, succError, predError, etc.). Treat as UB.
+        | Just (bv, rty) <- GHC.splitForAllTyCoVar_maybe (GHC.varType var)
+        , GHC.isTyVar bv
+        , GHC.isTyVarTy rty
+        -> mkUB
+
         | otherwise -> do
           dbgE
             [ GHC.ppr $ GHC.varType var