From 25dfe47ecd19b36a343aa9515b5d649cf4dc3dff Mon Sep 17 00:00:00 2001 From: Wind Date: Mon, 6 Jul 2026 11:02:16 +0200 Subject: [PATCH 1/4] handle type errors in edge cases --- src/Pantomime/Axiom.hs | 7 +++---- src/Pantomime/Symbolise.hs | 8 +++++++- 2 files changed, 10 insertions(+), 5 deletions(-) diff --git a/src/Pantomime/Axiom.hs b/src/Pantomime/Axiom.hs index 79c04e5..d79ea27 100644 --- a/src/Pantomime/Axiom.hs +++ b/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 diff --git a/src/Pantomime/Symbolise.hs b/src/Pantomime/Symbolise.hs index de0b4d7..cf5bca8 100644 --- a/src/Pantomime/Symbolise.hs +++ b/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 From d292ff14f2c53ba440eb0810ed7d61954bac8a30 Mon Sep 17 00:00:00 2001 From: Wind Date: Mon, 6 Jul 2026 11:17:22 +0200 Subject: [PATCH 2/4] fallback to original expression when type mismatch due to axioms --- src/Pantomime/Expr.hs | 22 ++++++++++++++++++---- 1 file changed, 18 insertions(+), 4 deletions(-) diff --git a/src/Pantomime/Expr.hs b/src/Pantomime/Expr.hs index 9e7ffb5..e559b31 100644 --- a/src/Pantomime/Expr.hs +++ b/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 From 47dd4aa58eb53e323ac7a8a0e1c9f22d3be17316 Mon Sep 17 00:00:00 2001 From: Wind Date: Mon, 6 Jul 2026 17:13:19 +0200 Subject: [PATCH 3/4] force evaluate counterexample --- src/Pantomime/Solve.hs | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/src/Pantomime/Solve.hs b/src/Pantomime/Solve.hs index a6c79f9..a29d908 100644 --- a/src/Pantomime/Solve.hs +++ b/src/Pantomime/Solve.hs @@ -249,11 +249,13 @@ checkValid axioms expr = runBuiltInTypes do -- 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!" From 451c62c6e1ffd2652255290e60fced5897d37830 Mon Sep 17 00:00:00 2001 From: Wind Date: Wed, 8 Jul 2026 16:07:34 +0200 Subject: [PATCH 4/4] more percise time measuring --- package.yaml | 1 + pantomime.cabal | 1 + src/Pantomime/Passes.hs | 25 ++++++++++++++++++++++--- 3 files changed, 24 insertions(+), 3 deletions(-) diff --git a/package.yaml b/package.yaml index c8e6337..c828578 100644 --- a/package.yaml +++ b/package.yaml @@ -81,6 +81,7 @@ library: - hashable - deepseq - bytestring + - time tests: pantomime-test: diff --git a/pantomime.cabal b/pantomime.cabal index 3f92e5e..0989eaa 100644 --- a/pantomime.cabal +++ b/pantomime.cabal @@ -108,6 +108,7 @@ library , primitive , template-haskell , text + , time , transformers , unordered-containers default-language: Haskell2010 diff --git a/src/Pantomime/Passes.hs b/src/Pantomime/Passes.hs index 58d47b7..0a1ac56 100644 --- a/src/Pantomime/Passes.hs +++ b/src/Pantomime/Passes.hs @@ -20,6 +20,9 @@ import Data.Data (Data) 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 @@ runSymbolic guts . 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,6 +205,14 @@ printAndLint bind = do 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 @@ -226,9 +241,13 @@ checkValidityAndEmbed guts = do (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))