From ca4793ca24e165ee2addbeb98bbfb0ecda478408 Mon Sep 17 00:00:00 2001 From: Wind Date: Sun, 31 May 2026 14:05:32 +0200 Subject: [PATCH 1/8] Experiments with embedding counterexamples in TemplateHaskell instead of crashing the compiler and dumping them in the log --- package.yaml | 1 + pantomime.cabal | 3 + src/Pantomime.hs | 7 ++ src/Pantomime/BuiltIn.hs | 1 + src/Pantomime/Marker.hs | 17 +++++ src/Pantomime/Passes.hs | 128 +++++++++++++++++++++++++++++------ src/Pantomime/Solve.hs | 35 ++++++---- src/Pantomime/TH.hs | 14 ++++ test/Spec.hs | 140 ++++++++++++--------------------------- tests/ForceEmbedding.hs | 20 ------ tests/Prune.hs | 45 ------------- 11 files changed, 214 insertions(+), 197 deletions(-) create mode 100644 src/Pantomime/Marker.hs create mode 100644 src/Pantomime/TH.hs delete mode 100644 tests/ForceEmbedding.hs delete mode 100644 tests/Prune.hs diff --git a/package.yaml b/package.yaml index 8c73ad9..477b5b7 100644 --- a/package.yaml +++ b/package.yaml @@ -80,6 +80,7 @@ library: - text - hashable - deepseq + - bytestring tests: pantomime-test: diff --git a/pantomime.cabal b/pantomime.cabal index 24b26b9..bb4ad2d 100644 --- a/pantomime.cabal +++ b/pantomime.cabal @@ -49,6 +49,7 @@ library Pantomime.Grisette.Mergeable Pantomime.Grisette.UnionT Pantomime.Literal + Pantomime.Marker Pantomime.Orphan.GHC Pantomime.Orphan.Grisette Pantomime.Passes @@ -56,6 +57,7 @@ library Pantomime.Solve Pantomime.Subst Pantomime.Symbolise + Pantomime.TH Pantomime.Unification Pantomime.Util other-modules: @@ -92,6 +94,7 @@ library ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -Wprepositive-qualified-module build-depends: base >=4.7 && <5 + , bytestring , composition , constraints >=0.14.2 , containers diff --git a/src/Pantomime.hs b/src/Pantomime.hs index b8374a6..e2f1172 100644 --- a/src/Pantomime.hs +++ b/src/Pantomime.hs @@ -5,6 +5,10 @@ module Pantomime , Theory (..) , PluginAxioms (..) + , pantomime + , pantomimeMarker + , pantomimeNothing + , pantomimeJust ) where import GHC.Plugins hiding (empty, (<>)) @@ -12,6 +16,9 @@ import GHC.Plugins hiding (empty, (<>)) import Pantomime.Annotation import Pantomime.Axiom import Pantomime.Passes +import Pantomime.TH (pantomime) +import Pantomime.Marker + plugin :: Plugin plugin = defaultPlugin diff --git a/src/Pantomime/BuiltIn.hs b/src/Pantomime/BuiltIn.hs index ccd3427..cb2e43d 100644 --- a/src/Pantomime/BuiltIn.hs +++ b/src/Pantomime/BuiltIn.hs @@ -626,6 +626,7 @@ pattern False <- (convert -> Prelude.False) {-# COMPLETE True, False #-} -- | Convert the standard Haskell Boolean to a symbolic Boolean. +{-# INLINE boolean #-} boolean :: Prelude.Bool -> Bool boolean = \case Prelude.True -> True diff --git a/src/Pantomime/Marker.hs b/src/Pantomime/Marker.hs new file mode 100644 index 0000000..92fbf6d --- /dev/null +++ b/src/Pantomime/Marker.hs @@ -0,0 +1,17 @@ +module Pantomime.Marker + ( pantomimeMarker + , pantomimeNothing + , pantomimeJust + ) where + +pantomimeMarker :: String -> Maybe String +pantomimeMarker _ = Nothing +{-# NOINLINE pantomimeMarker #-} + +pantomimeNothing :: Maybe String +pantomimeNothing = Nothing +{-# NOINLINE pantomimeNothing #-} + +pantomimeJust :: String -> Maybe String +pantomimeJust x = Just x +{-# NOINLINE pantomimeJust #-} diff --git a/src/Pantomime/Passes.hs b/src/Pantomime/Passes.hs index a43469a..f3f5b93 100644 --- a/src/Pantomime/Passes.hs +++ b/src/Pantomime/Passes.hs @@ -16,6 +16,9 @@ import Grisette import Data.Data (Data) import Data.Traversable (for) +import Data.Maybe (catMaybes) +import Data.ByteString.Char8 qualified as BS8 +import Pantomime.Marker import Control.Error @@ -174,7 +177,7 @@ runSymbolic guts checkValidityPass :: CoreToDo checkValidityPass = do let name = TH.nameBase 'checkValidityPass - let pass guts = runSymbolic guts $ annBindsPass checkValidity guts + let pass guts = runSymbolic guts $ checkValidityAndEmbed guts CoreDoPluginPass name pass printAndLint @@ -193,24 +196,105 @@ printAndLint bind = do debug res pure bind -checkValidity - :: HasCallStack - => Error () :> es - => Error (LookupError Name) :> es - => Error (LookupError TH.Name) :> es - => Error SolverError :> es - => Context Reader CoreProgram :> es - => Context Reader [TyCon] :> es - => Provider_ Solver () :> es - => HasFamInstEnvs :> es - => HasThings :> es - => THNameToGHCName :> es - => Theory - -> CoreBind' - -> Eff es CoreBind' --- TODO: The check itself permits recursive binders, so we should not restrict --- the input here really! -checkValidity (Theory axioms) (Bind' var expr) = do - axioms' <- resolvePluginAxioms axioms - checkValid axioms' expr - pure $ Bind' var expr +checkValidityAndEmbed + :: ( HasCallStack + , Error () :> es + , Error (LookupError Name) :> es + , Error (LookupError TH.Name) :> es + , Error SolverError :> es + , Context Reader CoreProgram :> es + , Context Reader [TyCon] :> es + , Provider_ Solver () :> es + , HasFamInstEnvs :> es + , HasThings :> es + , THNameToGHCName :> es + , HasAnnotations :> es + , CoreE :> es + , IOE :> es + ) + => ModGuts + -> Eff es ModGuts +checkValidityAndEmbed guts = do + (_, anns) <- getFirstAnnotations @Theory deserializeWithData guts + + markerId <- thNameToGhcName 'pantomimeMarker >>= lookupIdAll + nothingId <- thNameToGhcName 'pantomimeNothing >>= lookupIdAll + justId <- thNameToGhcName 'pantomimeJust >>= lookupIdAll + + (binds, results) <- fmap unzip $ for (mg_binds guts) \case + NonRec x e | Just (Theory axioms) <- lookupUFM anns $ varName x -> do + axioms' <- resolvePluginAxioms axioms + mCounterexample <- checkValid axioms' e + let varNameStr = getOccString x + case mCounterexample of + Nothing -> do + let replacementExpr = Var nothingId + pure (NonRec x e, Just (varNameStr, replacementExpr)) + Just counterexample -> do + let counterexampleStr = showSDocUnsafe (ppr counterexample) + strExpr <- liftCore $ mkStringExpr counterexampleStr + let replacementExpr = App (Var justId) strExpr + pure (NonRec x e, Just (varNameStr, replacementExpr)) + b -> pure (b, Nothing) + + let results' = catMaybes results + let binds' = replaceMarkerInBinds markerId results' binds + pure guts { mg_binds = binds' } + +-- | Recursively traverses all bindings in the module and replaces occurrences of +-- the 'pantomimeMarker' call with the pre-generated proof result expressions. +replaceMarkerInBinds + :: Id + -> [(String, CoreExpr)] + -> [CoreBind] + -> [CoreBind] +replaceMarkerInBinds markerId results = map goBind + where + goBind (NonRec b e) = NonRec b (replaceMarker markerId results e) + goBind (Rec bs) = Rec (map (\(b, e) -> (b, replaceMarker markerId results e)) bs) + +-- | Replaces any application of the 'pantomimeMarker' with its corresponding +-- compile-time Z3 proof result expression (either 'pantomimeNothing' or +-- 'pantomimeJust "counterexample"'). +replaceMarker + :: Id + -> [(String, CoreExpr)] + -> CoreExpr + -> CoreExpr +replaceMarker markerId results expr = go expr + where + go :: CoreExpr -> CoreExpr + go (App (Var v) argExpr) + | v == markerId = + case exprToString argExpr of + Just assertionName -> + case lookup assertionName results of + Just replacementExpr -> replacementExpr + Nothing -> App (Var v) (go argExpr) + Nothing -> App (Var v) (go argExpr) + + go (Var v) = Var v + go (Lit l) = Lit l + go (App f a) = App (go f) (go a) + go (Lam b e) = Lam b (go e) + go (Let (NonRec b r) e) = Let (NonRec b (go r)) (go e) + go (Let (Rec bs) e) = Let (Rec (map (\(b, r) -> (b, go r)) bs)) (go e) + go (Case e b t alts) = Case (go e) b t (map goAlt alts) + go (Cast e c) = Cast (go e) c + go (Tick t e) = Tick t (go e) + go (Type t) = Type t + go (Coercion c) = Coercion c + + goAlt (Alt con binders e) = Alt con binders (go e) + +-- | Rxtract a Haskell 'String' value from a GHC 'CoreExpr' +-- representing a string literal. Return Nothing if the expression is not +-- a string literal. +exprToString :: CoreExpr -> Maybe String +exprToString (Tick _ e) = exprToString e +exprToString (Cast e _) = exprToString e +exprToString (App (Var f) (Lit (LitString bs))) + | getOccString f == "unpackCString#" || getOccString f == "unpackCStringUtf8#" = + Just (BS8.unpack bs) +exprToString (Lit (LitString bs)) = Just (BS8.unpack bs) +exprToString _ = Nothing diff --git a/src/Pantomime/Solve.hs b/src/Pantomime/Solve.hs index 74c61f5..d219c99 100644 --- a/src/Pantomime/Solve.hs +++ b/src/Pantomime/Solve.hs @@ -15,6 +15,7 @@ module Pantomime.Solve ( checkValid + , Counterexample (..) ) where import GHC.Core qualified as GHC @@ -37,13 +38,13 @@ import GHC.Utils.Outputable , IsLine (..) , SDoc , (<+>) + , empty ) import Grisette (LogicalOp (..), EvalSym (..), Union, SymBool, onUnion) import Control.DeepSeq (NFData (..)) -import Data.Foldable (for_) import Data.Traversable (for) import Language.Haskell.TH qualified as TH @@ -169,6 +170,21 @@ construct prim PluginAxiomsR { .. } program expr = inject @SymboliseEff $ withDe Right value -> value pure (eq, Lie $ pure args) +data Counterexample = Counterexample + { counterexampleBindings :: [(Var, Arg)] + } + +instance Outputable Counterexample where + ppr (Counterexample bindings) = pprBindings bindings + where + pprBindings [] = empty + pprBindings ((bndr, arg) : rest) = vcat + [ "===================" + , ppr bndr <+> "::" <+> ppr (varType bndr) + , pprArg id arg + , pprBindings rest + ] + checkValid :: forall es . HasCallStack @@ -183,7 +199,7 @@ checkValid => Provider_ Solver () :> es => PluginAxiomsR -> CoreExpr - -> Eff es () + -> Eff es (Maybe Counterexample) checkValid axioms expr = runBuiltInTypes do -- TODO: Somehow this code doesn't read very nice. I think I should review it. program <- get @CoreProgram @@ -223,18 +239,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 - for_ args' \(bndr, arg) -> do - let arg' = evalSym True model arg - let argdoc = pprArg id arg' - dbg $ vcat - [ "===================" - , ppr bndr <+> "::" <+> ppr (varType bndr) - , argdoc - ] - error "Expression was **not** valid!" + let bindings = flip map args' \(bndr, arg) -> + let arg' = evalSym True model arg + in (bndr, arg') + pure $ Just (Counterexample bindings) Unsatisfiable -> do dbg @SDoc "Expression was valid!" - pure () + pure Nothing -- FIXME: I don't think this is always true. e.g. not sure about some of the -- floating point stuff for example. Unknown -> throwIO $ ErrorCall "checks are in decidable fragment" diff --git a/src/Pantomime/TH.hs b/src/Pantomime/TH.hs new file mode 100644 index 0000000..07e633f --- /dev/null +++ b/src/Pantomime/TH.hs @@ -0,0 +1,14 @@ +{-# LANGUAGE TemplateHaskellQuotes #-} + +module Pantomime.TH + ( pantomime + ) where + +import Language.Haskell.TH qualified as TH +import Pantomime.Marker + +pantomime :: TH.Name -> TH.Q TH.Exp +pantomime name = do + let nameStr = TH.nameBase name + [| pantomimeMarker nameStr |] + diff --git a/test/Spec.hs b/test/Spec.hs index d0b61ae..91d4f76 100644 --- a/test/Spec.hs +++ b/test/Spec.hs @@ -1,3 +1,6 @@ +{-# OPTIONS_GHC -fplugin=Pantomime #-} +{-# LANGUAGE BlockArguments #-} + module Main ( main ) where @@ -5,104 +8,45 @@ module Main import Test.Hspec import Test.HUnit -import System.Directory (listDirectory) - -import GHC -import GHC.Paths (libdir) -import GHC.Plugins (HasDynFlags (..), showGhcExceptionUnsafe) --- import GHC.Utils.Panic (handleGhcException) -import GHC.Driver.Session (updOptLevel) -import GHC.Data.EnumSet qualified as EnumSet - -import Language.Haskell.TH.LanguageExtensions - -import Control.Monad (forM_) - -import Data.Function ((&)) -import Data.List (isSuffixOf) - --- | Plugin setup. --- --- This ensure the flags and session are set up to test out plugin. -setupPlugin :: Ghc () -setupPlugin = do - dflags <- getDynFlags - setSessionDynFlags $ updOptLevel 1 dflags - { pluginModNames = mkModuleName "Pantomime" : pluginModNames dflags - , extensionFlags = extensionFlags dflags - & EnumSet.insert TemplateHaskellQuotes - , generalFlags = generalFlags dflags - & EnumSet.insert Opt_ExposeAllUnfoldings - -- & EnumSet.delete Opt_KeepHiFiles - -- & EnumSet.delete Opt_KeepOFiles - } - --- | Run the ghc monad. -runGhc' :: Ghc a -> IO a -runGhc' = runGhc $ Just libdir - --- | Compile the given file. --- --- This will additionally return an error if it occurred during the compilation. --- FIXME: It seems GHC already catches all thrown errors from the plugin. Can -compile :: FilePath -> Ghc (Either GhcException ()) -compile path = do - -- Compile the given module. - _ <- compileToCoreModule path - - -- Remove the target after compiling to ensure we don't run it twice. - target <- guessTarget path Nothing Nothing - removeTarget $ targetId target +import Pantomime +import Pantomime.BuiltIn qualified as Pantomime + +-- ============================================================================= +-- Test Case Definitions +-- ============================================================================= + +-- | Peirce's Law: ((p -> q) -> p) -> p. +-- This is a classical logic tautology that is non-trivial to prove/recognize. +{-# ANN validAssertion (Theory mempty) #-} +validAssertion :: Bool -> Bool -> Pantomime.Bool +validAssertion p q = + let p' = Pantomime.boolean p + q' = Pantomime.boolean q + in ((p' `Pantomime.implies` q') `Pantomime.implies` p') `Pantomime.implies` p' + +-- | Fallacy of Affirming the Consequent: ((p -> q) ∧ q) -> p. +-- This is invalid: if p is False and q is True, the premise holds but the conclusion is False. +{-# ANN invalidAssertion (Theory mempty) #-} +invalidAssertion :: Bool -> Bool -> Pantomime.Bool +invalidAssertion p q = + let p' = Pantomime.boolean p + q' = Pantomime.boolean q + (&&.) = (Pantomime.&&) + in ((p' `Pantomime.implies` q') &&. q') `Pantomime.implies` p' + +-- ============================================================================= +-- Test Suite +-- ============================================================================= - pure $ Right () - - -- let handler = pure . Left - -- operation - -- handleGhcException handler operation - --- | Fetches the files we consider for tests. -progPaths :: IO [FilePath] -progPaths = do - let listDirectory' dir = do - files <- listDirectory dir - pure $ fmap (dir <>) files - paths <- listDirectory' "tests/" - let isSrc path = isSuffixOf ".hs" path && not ("ForceEmbedding.hs" `isSuffixOf` path) - pure $ filter isSrc paths - --- -- | Compiles the given files, running them through the plugin. --- runFiles :: [FilePath] -> IO [Either GhcException ()] --- runFiles paths = runGhc' $ do --- setupPlugin --- forM paths compile - --- -- | Check the result of the compilation. --- check :: FilePath -> Either GhcException () -> SpecWith () --- check path result = do --- it ("checks " <> "\"" <> path <> "\"") $ do --- let pprFail = assertFailure . flip showGhcExceptionUnsafe "" --- either pprFail pure result - -check' :: FilePath -> SpecWith () -check' path = do - it ("checks " <> "\"" <> path <> "\"") $ do - -- result <- hSilence [stdout, stderr] . runGhc' $ do - result <- runGhc' $ do - setupPlugin - compile path - - let pprFail = assertFailure . flip showGhcExceptionUnsafe "" - either pprFail pure result - - -- let pprFail = assertFailure . flip showGhcExceptionUnsafe "" - -- either pprFail pure result - --- | Performs the plugin in a number of files. main :: IO () main = hspec $ do - paths <- runIO progPaths - forM_ paths check' - -- results <- runIO $ runFiles paths - - -- let results' = zip paths results - -- forM_ results' $ uncurry check + describe "Pantomime Symbolic Checker Unit Tests" $ do + it "verifies validAssertion (should succeed with Nothing)" $ do + $(pantomime 'validAssertion) `shouldBe` Nothing + + it "detects invalidAssertion (should fail with Just Counterexample)" $ do + case $(pantomime 'invalidAssertion) of + Just counterexample -> do + putStrLn $ "Counterexample:\n" ++ counterexample + counterexample `shouldContain` "False" + Nothing -> assertFailure "Expected invalid counterexample but got Nothing" diff --git a/tests/ForceEmbedding.hs b/tests/ForceEmbedding.hs deleted file mode 100644 index d8884d6..0000000 --- a/tests/ForceEmbedding.hs +++ /dev/null @@ -1,20 +0,0 @@ -module ForceEmbeddings - ( theory - ) where - --- FIXME: Right now, 'collectScrut' will throw an error if we force a --- literal. I'm not 100% sure what the behaviour should be, but it --- definitely shouldn't throw. The only thing I'm not sure about, is --- what to do with constraints: should they now be part of the outer --- expression? --- --- Example faulting expression. I was not able to reproduce it for a --- different type than an embedded Array type... I think it's due to --- the way it is embedded (that is, it is a 'Cast' at the outer layer). -{-# NOINLINE test #-} -test :: Memory -> Pantomime.Bool -test !_ = Pantomime.True - -{-# ANN theory (Theory $ Base.axioms <> Clash.axioms <> RISCV.axioms) #-} -theory :: Pantomime.Bool -theory = test $ constM 0 diff --git a/tests/Prune.hs b/tests/Prune.hs deleted file mode 100644 index d53a46a..0000000 --- a/tests/Prune.hs +++ /dev/null @@ -1,45 +0,0 @@ -{-# LANGUAGE BlockArguments #-} -{-# LANGUAGE ImportQualifiedPost #-} - -module Prune - ( loopy - , doubleCase - , share - ) where - -import GHC.Base (noinline) -import Pantomime -import Pantomime.BuiltIn qualified as Pantomime - -{-# ANN loopy (Theory mempty) #-} -loopy :: Bool -> Pantomime.Bool -loopy value = Pantomime.boolean do - let go x = case x of - True -> True - False -> go $ not x - go value - -infinite :: a -infinite = noinline infinite - -{-# ANN doubleCase (Theory mempty) #-} -doubleCase :: Bool -> Pantomime.Bool -doubleCase value = Pantomime.boolean do - case value of - True -> True - False -> case value of - True -> infinite - False -> True - -{-# ANN share (Theory mempty) #-} -share :: Bool -> Bool -> Pantomime.Bool -share lhs rhs = Pantomime.boolean do - let x = case lhs || rhs of - True -> True - False -> infinite - case lhs of - True -> x - False -> case rhs of - True -> x - False -> True - From 838a1d44dbeb2b109ea92e2112ae930d05ee7a47 Mon Sep 17 00:00:00 2001 From: Wind Date: Sun, 31 May 2026 14:28:20 +0200 Subject: [PATCH 2/8] Check for ANN tags at compile time --- src/Pantomime/Marker.hs | 3 ++- src/Pantomime/Passes.hs | 40 ++++++++++++++++++++++++++++++++++++++++ 2 files changed, 42 insertions(+), 1 deletion(-) diff --git a/src/Pantomime/Marker.hs b/src/Pantomime/Marker.hs index 92fbf6d..4bc8486 100644 --- a/src/Pantomime/Marker.hs +++ b/src/Pantomime/Marker.hs @@ -5,7 +5,8 @@ module Pantomime.Marker ) where pantomimeMarker :: String -> Maybe String -pantomimeMarker _ = Nothing +pantomimeMarker name = error $ + "The marker function 'pantomimeMarker' for '" ++ name ++ "' was not replaced by the GHC compiler plugin pass." {-# NOINLINE pantomimeMarker #-} pantomimeNothing :: Maybe String diff --git a/src/Pantomime/Passes.hs b/src/Pantomime/Passes.hs index f3f5b93..88df0b3 100644 --- a/src/Pantomime/Passes.hs +++ b/src/Pantomime/Passes.hs @@ -238,6 +238,14 @@ checkValidityAndEmbed guts = do b -> pure (b, Nothing) let results' = catMaybes results + + let resultNames = map fst results' + case findMissingAnnotations markerId resultNames binds of + [] -> pure () + (missing : _) -> + throwIO $ PprProgramError "checkValidityPass" $ + text ("Symbolic check result not found for '" ++ missing ++ "'. Did you forget to add the {-# ANN " ++ missing ++ " (Theory ...) #-} annotation?") + let binds' = replaceMarkerInBinds markerId results' binds pure guts { mg_binds = binds' } @@ -298,3 +306,35 @@ exprToString (App (Var f) (Lit (LitString bs))) Just (BS8.unpack bs) exprToString (Lit (LitString bs)) = Just (BS8.unpack bs) exprToString _ = Nothing + +-- | Scans the Core bindings for any call to 'pantomimeMarker' and returns the +-- names of all assertions that are referenced by a splice but lack the corresponding +-- 'Theory' annotation. +findMissingAnnotations + :: Id + -> [String] + -> [CoreBind] + -> [String] +findMissingAnnotations markerId resultNames binds = concatMap (goExpr . getExpr) binds + where + getExpr (NonRec _ e) = e + getExpr (Rec bs) = Let (Rec bs) (Var markerId) + + goExpr :: CoreExpr -> [String] + goExpr (App (Var v) argExpr) + | v == markerId = + case exprToString argExpr of + Just assertionName + | assertionName `notElem` resultNames -> [assertionName] + _ -> goExpr argExpr + goExpr (Var _) = [] + goExpr (Lit _) = [] + goExpr (App f a) = goExpr f ++ goExpr a + goExpr (Lam _ e) = goExpr e + goExpr (Let (NonRec _ r) e) = goExpr r ++ goExpr e + goExpr (Let (Rec bs) e) = concatMap (goExpr . snd) bs ++ goExpr e + goExpr (Case e _ _ alts) = goExpr e ++ concatMap (\(Alt _ _ body) -> goExpr body) alts + goExpr (Cast e _) = goExpr e + goExpr (Tick _ e) = goExpr e + goExpr (Type _) = [] + goExpr (Coercion _) = [] From f816b7fddf7cc7709963f5820b52923527fb272a Mon Sep 17 00:00:00 2001 From: Wind Date: Sun, 31 May 2026 15:58:59 +0200 Subject: [PATCH 3/8] Make pantomine return list of argument and counterexample expressions instead --- src/Pantomime/Fresh.hs | 11 +++++------ src/Pantomime/Marker.hs | 6 +++--- src/Pantomime/Passes.hs | 11 ++++++++--- src/Pantomime/Solve.hs | 24 +++++++++++++++++++++++- test/Spec.hs | 8 +++++--- 5 files changed, 44 insertions(+), 16 deletions(-) diff --git a/src/Pantomime/Fresh.hs b/src/Pantomime/Fresh.hs index 0643b9d..5300a2b 100644 --- a/src/Pantomime/Fresh.hs +++ b/src/Pantomime/Fresh.hs @@ -402,21 +402,20 @@ freshArgs => Context Reader BuiltInTyCon :> es => Context Reader FamInstEnvs :> es => TypeAxiomsR + -> [String] -> Type -> InScopeSet -> Eff es ([(Var, Arg)], InScopeSet) -freshArgs axioms ty scope0 = do +freshArgs axioms valNames ty scope0 = do -- Gather the argument types. let (tyVars, funTy) = splitForAllTyVars ty let (argTys, _resTy) = splitFunTys funTy - -- TODO: Isn't there some infinite sequence of names that could be used - -- instead of this? - -- Names for the arguments. - let names = repeat "arg" + -- Names for the arguments as FastStrings. + let names = map GHC.fsLit $ valNames ++ repeat "arg" -- Create fresh type arguments. - let kinds = zip names $ fmap tyVarKind tyVars + let kinds = zip (repeat (GHC.fsLit "arg")) $ fmap tyVarKind tyVars let (tyArgs, scope1) = freshTyVars kinds scope0 -- Create fresh value arguments. diff --git a/src/Pantomime/Marker.hs b/src/Pantomime/Marker.hs index 4bc8486..b5894f5 100644 --- a/src/Pantomime/Marker.hs +++ b/src/Pantomime/Marker.hs @@ -4,15 +4,15 @@ module Pantomime.Marker , pantomimeJust ) where -pantomimeMarker :: String -> Maybe String +pantomimeMarker :: String -> Maybe [(String, String)] pantomimeMarker name = error $ "The marker function 'pantomimeMarker' for '" ++ name ++ "' was not replaced by the GHC compiler plugin pass." {-# NOINLINE pantomimeMarker #-} -pantomimeNothing :: Maybe String +pantomimeNothing :: Maybe [(String, String)] pantomimeNothing = Nothing {-# NOINLINE pantomimeNothing #-} -pantomimeJust :: String -> Maybe String +pantomimeJust :: [(String, String)] -> Maybe [(String, String)] pantomimeJust x = Just x {-# NOINLINE pantomimeJust #-} diff --git a/src/Pantomime/Passes.hs b/src/Pantomime/Passes.hs index 88df0b3..7428ff0 100644 --- a/src/Pantomime/Passes.hs +++ b/src/Pantomime/Passes.hs @@ -231,9 +231,14 @@ checkValidityAndEmbed guts = do let replacementExpr = Var nothingId pure (NonRec x e, Just (varNameStr, replacementExpr)) Just counterexample -> do - let counterexampleStr = showSDocUnsafe (ppr counterexample) - strExpr <- liftCore $ mkStringExpr counterexampleStr - let replacementExpr = App (Var justId) strExpr + let counterexamplePairs = counterexampleToPairs counterexample + pairExprs <- for counterexamplePairs \(nameStr, valStr) -> do + nameExpr <- liftCore $ mkStringExpr nameStr + valExpr <- liftCore $ mkStringExpr valStr + pure $ mkCoreTup [nameExpr, valExpr] + let pairTy = mkBoxedTupleTy [stringTy, stringTy] + let listExpr = mkListExpr pairTy pairExprs + let replacementExpr = App (Var justId) listExpr pure (NonRec x e, Just (varNameStr, replacementExpr)) b -> pure (b, Nothing) diff --git a/src/Pantomime/Solve.hs b/src/Pantomime/Solve.hs index d219c99..d5b6c3c 100644 --- a/src/Pantomime/Solve.hs +++ b/src/Pantomime/Solve.hs @@ -16,6 +16,7 @@ module Pantomime.Solve ( checkValid , Counterexample (..) + , counterexampleToPairs ) where import GHC.Core qualified as GHC @@ -31,6 +32,9 @@ import GHC.Plugins , varType , vcat , emptyInScopeSet + , getOccString + , showSDocUnsafe + , isId ) import GHC.Types.Id.Make (nospecId) import GHC.Utils.Outputable @@ -152,7 +156,7 @@ construct prim PluginAxiomsR { .. } program expr = inject @SymboliseEff $ withDe -- Create fresh arguments. let ty = exprType expr - (args, _scope) <- freshArgs typeAxiomsR ty emptyInScopeSet + (args, _scope) <- freshArgs typeAxiomsR (collectValBinders expr) ty emptyInScopeSet result <- defer do fun <- symbolise subst expr @@ -174,6 +178,13 @@ data Counterexample = Counterexample { counterexampleBindings :: [(Var, Arg)] } +-- | Formats a counterexample into a list of name-value string pairs. +counterexampleToPairs :: Counterexample -> [(String, String)] +counterexampleToPairs (Counterexample bindings) = map formatBinding bindings + where + formatBinding (bndr, arg) = + (getOccString bndr, showSDocUnsafe (pprArg id arg)) + instance Outputable Counterexample where ppr (Counterexample bindings) = pprBindings bindings where @@ -249,3 +260,14 @@ checkValid axioms expr = runBuiltInTypes do -- FIXME: I don't think this is always true. e.g. not sure about some of the -- floating point stuff for example. Unknown -> throwIO $ ErrorCall "checks are in decidable fragment" + +collectValBinders :: CoreExpr -> [String] +collectValBinders expr = go expr + where + go (GHC.Lam b e) + | isId b = getOccString b : go e + | otherwise = go e + go (GHC.Tick _ e) = go e + go (GHC.Cast e _) = go e + go (GHC.Let _ e) = go e + go _ = [] diff --git a/test/Spec.hs b/test/Spec.hs index 91d4f76..10c87d3 100644 --- a/test/Spec.hs +++ b/test/Spec.hs @@ -8,6 +8,7 @@ module Main import Test.Hspec import Test.HUnit +import Data.List (isInfixOf) import Pantomime import Pantomime.BuiltIn qualified as Pantomime @@ -46,7 +47,8 @@ main = hspec $ do it "detects invalidAssertion (should fail with Just Counterexample)" $ do case $(pantomime 'invalidAssertion) of - Just counterexample -> do - putStrLn $ "Counterexample:\n" ++ counterexample - counterexample `shouldContain` "False" + Just counterexamples -> do + putStrLn "Counterexamples:" + mapM_ (\(name, val) -> putStrLn $ name ++ " = " ++ val) counterexamples + counterexamples `shouldSatisfy` any (\(_, v) -> "False" `isInfixOf` v || "True" `isInfixOf` v) Nothing -> assertFailure "Expected invalid counterexample but got Nothing" From 2c08eeace15c87933c532b9be04b0d370942e00d Mon Sep 17 00:00:00 2001 From: Wind Date: Sun, 31 May 2026 16:55:26 +0200 Subject: [PATCH 4/8] Generate counterexample expressions --- src/Pantomime.hs | 1 + src/Pantomime/Marker.hs | 39 ++++++++++++++-- src/Pantomime/Passes.hs | 99 ++++++++++++++++++++++++++--------------- src/Pantomime/Solve.hs | 33 +++++++++++++- src/Pantomime/TH.hs | 2 +- test/Spec.hs | 9 +--- 6 files changed, 133 insertions(+), 50 deletions(-) diff --git a/src/Pantomime.hs b/src/Pantomime.hs index e2f1172..b2b1c1b 100644 --- a/src/Pantomime.hs +++ b/src/Pantomime.hs @@ -9,6 +9,7 @@ module Pantomime , pantomimeMarker , pantomimeNothing , pantomimeJust + , PantomimeType (..) ) where import GHC.Plugins hiding (empty, (<>)) diff --git a/src/Pantomime/Marker.hs b/src/Pantomime/Marker.hs index b5894f5..5098ce6 100644 --- a/src/Pantomime/Marker.hs +++ b/src/Pantomime/Marker.hs @@ -1,18 +1,51 @@ +{-# LANGUAGE FunctionalDependencies #-} + module Pantomime.Marker ( pantomimeMarker , pantomimeNothing , pantomimeJust + , PantomimeType (..) ) where -pantomimeMarker :: String -> Maybe [(String, String)] +import Pantomime.BuiltIn qualified as Pantomime + +pantomimeMarker :: String -> Maybe res pantomimeMarker name = error $ "The marker function 'pantomimeMarker' for '" ++ name ++ "' was not replaced by the GHC compiler plugin pass." {-# NOINLINE pantomimeMarker #-} -pantomimeNothing :: Maybe [(String, String)] +pantomimeNothing :: Maybe res pantomimeNothing = Nothing {-# NOINLINE pantomimeNothing #-} -pantomimeJust :: [(String, String)] -> Maybe [(String, String)] +pantomimeJust :: res -> Maybe res pantomimeJust x = Just x {-# NOINLINE pantomimeJust #-} + +class PantomimeType assertion res | assertion -> res where + pantomimeMarker' :: assertion -> String -> Maybe res + pantomimeMarker' _ name = pantomimeMarker name + {-# NOINLINE pantomimeMarker' #-} + +instance PantomimeType Pantomime.Bool () +instance PantomimeType (a -> Pantomime.Bool) a +instance PantomimeType (a -> b -> Pantomime.Bool) (a, b) +instance PantomimeType (a -> b -> c -> Pantomime.Bool) (a, b, c) +instance PantomimeType (a -> b -> c -> d -> Pantomime.Bool) (a, b, c, d) +instance PantomimeType (a -> b -> c -> d -> e -> Pantomime.Bool) (a, b, c, d, e) +instance PantomimeType (a -> b -> c -> d -> e -> f -> Pantomime.Bool) (a, b, c, d, e, f) +instance PantomimeType (a -> b -> c -> d -> e -> f -> g -> Pantomime.Bool) (a, b, c, d, e, f, g) +instance PantomimeType (a -> b -> c -> d -> e -> f -> g -> h -> Pantomime.Bool) (a, b, c, d, e, f, g, h) +instance PantomimeType (a -> b -> c -> d -> e -> f -> g -> h -> i -> Pantomime.Bool) (a, b, c, d, e, f, g, h, i) +instance PantomimeType (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> Pantomime.Bool) (a, b, c, d, e, f, g, h, i, j) +instance PantomimeType (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> Pantomime.Bool) (a, b, c, d, e, f, g, h, i, j, k) +instance PantomimeType (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> Pantomime.Bool) (a, b, c, d, e, f, g, h, i, j, k, l) +instance PantomimeType (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> Pantomime.Bool) (a, b, c, d, e, f, g, h, i, j, k, l, m) +instance PantomimeType (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> Pantomime.Bool) (a, b, c, d, e, f, g, h, i, j, k, l, m, n) +instance PantomimeType (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> Pantomime.Bool) (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o) +instance PantomimeType (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> Pantomime.Bool) (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) +instance PantomimeType (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> q -> Pantomime.Bool) (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q) +instance PantomimeType (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> q -> r -> Pantomime.Bool) (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) +instance PantomimeType (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> q -> r -> s -> Pantomime.Bool) (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s) +instance PantomimeType (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> q -> r -> s -> t -> Pantomime.Bool) (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t) + diff --git a/src/Pantomime/Passes.hs b/src/Pantomime/Passes.hs index 7428ff0..deac820 100644 --- a/src/Pantomime/Passes.hs +++ b/src/Pantomime/Passes.hs @@ -4,6 +4,7 @@ module Pantomime.Passes ) where import GHC.Plugins hiding (empty, (<>), thNameToGhcName, getFirstAnnotations) +import GHC.Core.TyCo.Rep (scaledThing) import GHC.Core.Lint import GHC.Driver.Config.Core.Lint (initLintConfig) @@ -211,13 +212,17 @@ checkValidityAndEmbed , HasAnnotations :> es , CoreE :> es , IOE :> es + , HasDynFlagsE :> es ) => ModGuts -> Eff es ModGuts checkValidityAndEmbed guts = do (_, anns) <- getFirstAnnotations @Theory deserializeWithData guts - markerId <- thNameToGhcName 'pantomimeMarker >>= lookupIdAll + dflags <- getDynFlags + let platform = targetPlatform dflags + + markerPrimeId <- thNameToGhcName 'pantomimeMarker' >>= lookupIdAll nothingId <- thNameToGhcName 'pantomimeNothing >>= lookupIdAll justId <- thNameToGhcName 'pantomimeJust >>= lookupIdAll @@ -226,69 +231,76 @@ checkValidityAndEmbed guts = do axioms' <- resolvePluginAxioms axioms mCounterexample <- checkValid axioms' e let varNameStr = getOccString x + let ty = varType x + (_, funTy) = splitForAllTyVars ty + (argTys, _resTy) = splitFunTys funTy + argTys' = map scaledThing argTys + tupleTy = case argTys' of + [] -> mkBoxedTupleTy [] + [t] -> t + ts -> mkBoxedTupleTy ts case mCounterexample of Nothing -> do - let replacementExpr = Var nothingId - pure (NonRec x e, Just (varNameStr, replacementExpr)) + let replacementExpr = App (Var nothingId) (Type tupleTy) + pure (NonRec x e, Just (varNameStr, (tupleTy, replacementExpr))) Just counterexample -> do - let counterexamplePairs = counterexampleToPairs counterexample - pairExprs <- for counterexamplePairs \(nameStr, valStr) -> do - nameExpr <- liftCore $ mkStringExpr nameStr - valExpr <- liftCore $ mkStringExpr valStr - pure $ mkCoreTup [nameExpr, valExpr] - let pairTy = mkBoxedTupleTy [stringTy, stringTy] - let listExpr = mkListExpr pairTy pairExprs - let replacementExpr = App (Var justId) listExpr - pure (NonRec x e, Just (varNameStr, replacementExpr)) + let valBindings = filter (isId . fst) (counterexampleBindings counterexample) + valExprs <- for valBindings \(_, arg) -> do + liftCore $ argToCoreExpr platform arg + let tupleExpr = case valExprs of + [] -> mkCoreTup [] + [expr'] -> expr' + exprs -> mkCoreTup exprs + let replacementExpr = App (App (Var justId) (Type tupleTy)) tupleExpr + pure (NonRec x e, Just (varNameStr, (tupleTy, replacementExpr))) b -> pure (b, Nothing) let results' = catMaybes results let resultNames = map fst results' - case findMissingAnnotations markerId resultNames binds of + case findMissingAnnotations markerPrimeId resultNames binds of [] -> pure () (missing : _) -> throwIO $ PprProgramError "checkValidityPass" $ text ("Symbolic check result not found for '" ++ missing ++ "'. Did you forget to add the {-# ANN " ++ missing ++ " (Theory ...) #-} annotation?") - let binds' = replaceMarkerInBinds markerId results' binds + let binds' = replaceMarkerInBinds markerPrimeId results' binds pure guts { mg_binds = binds' } -- | Recursively traverses all bindings in the module and replaces occurrences of -- the 'pantomimeMarker' call with the pre-generated proof result expressions. replaceMarkerInBinds :: Id - -> [(String, CoreExpr)] + -> [(String, (Type, CoreExpr))] -> [CoreBind] -> [CoreBind] -replaceMarkerInBinds markerId results = map goBind +replaceMarkerInBinds markerPrimeId results = map goBind where - goBind (NonRec b e) = NonRec b (replaceMarker markerId results e) - goBind (Rec bs) = Rec (map (\(b, e) -> (b, replaceMarker markerId results e)) bs) + goBind (NonRec b e) = NonRec b (replaceMarker markerPrimeId results e) + goBind (Rec bs) = Rec (map (\(b, e) -> (b, replaceMarker markerPrimeId results e)) bs) -- | Replaces any application of the 'pantomimeMarker' with its corresponding --- compile-time Z3 proof result expression (either 'pantomimeNothing' or --- 'pantomimeJust "counterexample"'). +-- compile-time Z3 proof result expression. replaceMarker :: Id - -> [(String, CoreExpr)] + -> [(String, (Type, CoreExpr))] -> CoreExpr -> CoreExpr -replaceMarker markerId results expr = go expr +replaceMarker markerPrimeId results expr = go expr where go :: CoreExpr -> CoreExpr - go (App (Var v) argExpr) - | v == markerId = - case exprToString argExpr of + go (App f a) + | Just () <- isMarkerPrimeCall f = + case exprToString a of Just assertionName -> case lookup assertionName results of - Just replacementExpr -> replacementExpr - Nothing -> App (Var v) (go argExpr) - Nothing -> App (Var v) (go argExpr) + Just (_, replacementExpr) -> replacementExpr + Nothing -> App (go f) (go a) + Nothing -> App (go f) (go a) + | otherwise = App (go f) (go a) go (Var v) = Var v go (Lit l) = Lit l - go (App f a) = App (go f) (go a) go (Lam b e) = Lam b (go e) go (Let (NonRec b r) e) = Let (NonRec b (go r)) (go e) go (Let (Rec bs) e) = Let (Rec (map (\(b, r) -> (b, go r)) bs)) (go e) @@ -300,6 +312,13 @@ replaceMarker markerId results expr = go expr goAlt (Alt con binders e) = Alt con binders (go e) + isMarkerPrimeCall :: CoreExpr -> Maybe () + isMarkerPrimeCall (Var v) | v == markerPrimeId = Just () + isMarkerPrimeCall (App f' _) = isMarkerPrimeCall f' + isMarkerPrimeCall (Cast e' _) = isMarkerPrimeCall e' + isMarkerPrimeCall (Tick _ e') = isMarkerPrimeCall e' + isMarkerPrimeCall _ = Nothing + -- | Rxtract a Haskell 'String' value from a GHC 'CoreExpr' -- representing a string literal. Return Nothing if the expression is not -- a string literal. @@ -320,21 +339,22 @@ findMissingAnnotations -> [String] -> [CoreBind] -> [String] -findMissingAnnotations markerId resultNames binds = concatMap (goExpr . getExpr) binds +findMissingAnnotations markerPrimeId resultNames binds = concatMap (goExpr . getExpr) binds where getExpr (NonRec _ e) = e - getExpr (Rec bs) = Let (Rec bs) (Var markerId) + getExpr (Rec bs) = Let (Rec bs) (Var markerPrimeId) goExpr :: CoreExpr -> [String] - goExpr (App (Var v) argExpr) - | v == markerId = - case exprToString argExpr of + goExpr (App f a) = + case isMarkerPrimeCall f of + Just () -> + case exprToString a of Just assertionName | assertionName `notElem` resultNames -> [assertionName] - _ -> goExpr argExpr + _ -> goExpr f ++ goExpr a + Nothing -> goExpr f ++ goExpr a goExpr (Var _) = [] goExpr (Lit _) = [] - goExpr (App f a) = goExpr f ++ goExpr a goExpr (Lam _ e) = goExpr e goExpr (Let (NonRec _ r) e) = goExpr r ++ goExpr e goExpr (Let (Rec bs) e) = concatMap (goExpr . snd) bs ++ goExpr e @@ -343,3 +363,10 @@ findMissingAnnotations markerId resultNames binds = concatMap (goExpr . getExpr) goExpr (Tick _ e) = goExpr e goExpr (Type _) = [] goExpr (Coercion _) = [] + + isMarkerPrimeCall :: CoreExpr -> Maybe () + isMarkerPrimeCall (Var v) | v == markerPrimeId = Just () + isMarkerPrimeCall (App f' _) = isMarkerPrimeCall f' + isMarkerPrimeCall (Cast e' _) = isMarkerPrimeCall e' + isMarkerPrimeCall (Tick _ e') = isMarkerPrimeCall e' + isMarkerPrimeCall _ = Nothing diff --git a/src/Pantomime/Solve.hs b/src/Pantomime/Solve.hs index d5b6c3c..81b001e 100644 --- a/src/Pantomime/Solve.hs +++ b/src/Pantomime/Solve.hs @@ -1,6 +1,8 @@ {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ImpredicativeTypes #-} {-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE TypeApplications #-} -- TODO: I want to remove many of these pragmas, also for the other files. Most -- of them should just be included in the top-level flags. There also seems to -- be a lot of obsolete stuff. Perhaps its good to first find out which flags @@ -17,6 +19,7 @@ module Pantomime.Solve ( checkValid , Counterexample (..) , counterexampleToPairs + , argToCoreExpr ) where import GHC.Core qualified as GHC @@ -35,7 +38,13 @@ import GHC.Plugins , getOccString , showSDocUnsafe , isId + , dataConWorkId + , tyConDataCons + , trueDataCon + , falseDataCon ) +import GHC.Core.Make (mkIntegerExpr) +import GHC.Platform (Platform) import GHC.Types.Id.Make (nospecId) import GHC.Utils.Outputable ( Outputable (..) @@ -45,7 +54,7 @@ import GHC.Utils.Outputable , empty ) -import Grisette (LogicalOp (..), EvalSym (..), Union, SymBool, onUnion) +import Grisette (LogicalOp (..), EvalSym (..), Union, SymBool, onUnion, toCon, ToCon (..), pattern Single) import Control.DeepSeq (NFData (..)) @@ -62,12 +71,13 @@ import Pantomime.Expr , pprArg , runRuntime , throwE + , Constructor (..) ) import Pantomime.Literal (BuiltInTyCon (..)) import Pantomime.Symbolise import Pantomime.Subst import Pantomime.Fresh -import Pantomime.Util (dbg) +import Pantomime.Util (dbg, BitVec) import Pantomime.Axiom (PluginAxiomsR (..)) import Pantomime.PrimOps (PrimOp) import Pantomime.Defer (defer, withDeferrable) @@ -271,3 +281,22 @@ collectValBinders expr = go expr go (GHC.Cast e _) = go e go (GHC.Let _ e) = go e go _ = [] + +argToCoreExpr :: MonadThings m => Platform -> Arg -> m CoreExpr +argToCoreExpr platform arg = + case runRuntime arg of + Single (Right (Lit (Bool sb))) + | Just b <- toCon sb -> + pure $ if b then GHC.Var (dataConWorkId trueDataCon) else GHC.Var (dataConWorkId falseDataCon) + Single (Right (Lit (Integer si))) + | Just i <- toCon si -> + pure $ mkIntegerExpr platform i + Single (Right (Con (DataCon dc))) -> + pure $ GHC.Var (dataConWorkId dc) + Single (Right (Con (EnumCon @n tag tc))) + | Just t <- toCon @_ @(BitVec n) tag -> do + let dcs = tyConDataCons tc + dc = dcs !! fromIntegral t + pure $ GHC.Var (dataConWorkId dc) + _ -> + error "Unsupported counterexample argument type" diff --git a/src/Pantomime/TH.hs b/src/Pantomime/TH.hs index 07e633f..2a31e21 100644 --- a/src/Pantomime/TH.hs +++ b/src/Pantomime/TH.hs @@ -10,5 +10,5 @@ import Pantomime.Marker pantomime :: TH.Name -> TH.Q TH.Exp pantomime name = do let nameStr = TH.nameBase name - [| pantomimeMarker nameStr |] + pure $ TH.AppE (TH.AppE (TH.VarE 'pantomimeMarker') (TH.VarE name)) (TH.LitE (TH.StringL nameStr)) diff --git a/test/Spec.hs b/test/Spec.hs index 10c87d3..86ba6e6 100644 --- a/test/Spec.hs +++ b/test/Spec.hs @@ -6,9 +6,7 @@ module Main ) where import Test.Hspec -import Test.HUnit -import Data.List (isInfixOf) import Pantomime import Pantomime.BuiltIn qualified as Pantomime @@ -46,9 +44,4 @@ main = hspec $ do $(pantomime 'validAssertion) `shouldBe` Nothing it "detects invalidAssertion (should fail with Just Counterexample)" $ do - case $(pantomime 'invalidAssertion) of - Just counterexamples -> do - putStrLn "Counterexamples:" - mapM_ (\(name, val) -> putStrLn $ name ++ " = " ++ val) counterexamples - counterexamples `shouldSatisfy` any (\(_, v) -> "False" `isInfixOf` v || "True" `isInfixOf` v) - Nothing -> assertFailure "Expected invalid counterexample but got Nothing" + $(pantomime 'invalidAssertion) `shouldBe` Just (False, True) From 5402556b1cfbe2b0701515751118f9177af79cfa Mon Sep 17 00:00:00 2001 From: Wind Date: Sun, 31 May 2026 18:07:14 +0200 Subject: [PATCH 5/8] More informative errors --- src/Pantomime/Axiom.hs | 5 ++- src/Pantomime/Embed.hs | 52 +++++++++++++------------ src/Pantomime/Expr.hs | 74 ++++++++++++++++++------------------ src/Pantomime/Fresh.hs | 11 +++--- src/Pantomime/Literal.hs | 13 ++++--- src/Pantomime/Passes.hs | 6 +-- src/Pantomime/PrimOps.hs | 54 +++++++++++++------------- src/Pantomime/Solve.hs | 9 +++-- src/Pantomime/Subst.hs | 11 +++--- src/Pantomime/Symbolise.hs | 37 ++++++++++-------- src/Pantomime/Unification.hs | 6 +-- 11 files changed, 146 insertions(+), 132 deletions(-) diff --git a/src/Pantomime/Axiom.hs b/src/Pantomime/Axiom.hs index f6ad2a1..7e3eabd 100644 --- a/src/Pantomime/Axiom.hs +++ b/src/Pantomime/Axiom.hs @@ -44,6 +44,7 @@ import GHC.Utils.Outputable ( Outputable (..) , IsDoc (..) , IsLine (fsep, (<+>), text) + , SDoc , hang , punctuate , comma @@ -236,7 +237,7 @@ instance Monoid PluginAxiomsR where resolvePluginAxioms :: HasCallStack -- TODO: Adjust these errors! - => Error () :> es + => Error String :> es => Error (LookupError TH.Name) :> es => Error (LookupError Name) :> es => THNameToGHCName :> es @@ -350,7 +351,7 @@ resolvePluginAxioms PluginAxioms { .. } = do -- Throw an error if we could not create any. when (null dictsNew) do - throwError () + throwError "resolvePluginAxioms: could not create any Embeddable or Coercible dictionaries for the given axioms" -- Insert all dictionaries. pure $ foldlBy dicts dictsNew \acc dict -> do diff --git a/src/Pantomime/Embed.hs b/src/Pantomime/Embed.hs index 99ff8f0..cf85583 100644 --- a/src/Pantomime/Embed.hs +++ b/src/Pantomime/Embed.hs @@ -22,6 +22,8 @@ import Effectful import Effectful.Error.Static (Error, HasCallStack) import Effectful.Context +import GHC.Utils.Outputable (SDoc, text) + import GHC.Builtin.Types.Literals (typeNatAddTyCon) import GHC.Builtin.Uniques (mkAlphaTyVarUnique) import GHC.Core.Type (substTy) @@ -274,7 +276,7 @@ embed :: forall a es . HasCallStack => Deferrable es - => Error () :> es + => Error String :> es => Context Reader BuiltInTyCon :> es => Context Reader FamInstEnvs :> es => Reflect a @@ -287,7 +289,7 @@ project :: forall a es . HasCallStack => Deferrable es - => Error () :> es + => Error String :> es => Context Reader BuiltInTyCon :> es => Context Reader FamInstEnvs :> es => Reflect a @@ -301,7 +303,7 @@ project subst = project' subst $ reflect @a embed' :: HasCallStack => Deferrable es - => Error () :> es + => Error String :> es => Context Reader BuiltInTyCon :> es => Context Reader FamInstEnvs :> es => Subst @@ -323,7 +325,7 @@ embed' subst sty repr = case sty of Reduction co _ <- liftEff $ normaliseSTy subst Nominal sty let co' = mkSymCo $ mkSubCo co mkCast lit co' - SPrimitiveTy _ -> throwE () + SPrimitiveTy _ -> throwE "embed': cannot directly embed a PrimitiveTy — use project' first" SLambda aty rty -> do -- Gather the type for the lambda. ty <- liftEff $ embedSTy subst sty @@ -353,8 +355,8 @@ embed' subst sty repr = case sty of SNaturalTy -> hoistEff repr >>= absurd SNatural -> hoistEff repr >>= absurd SAddTy _ _ -> hoistEff repr >>= absurd - SLEqTy _ _ -> throwE () - SKnownNatTy _n -> throwE () + SLEqTy _ _ -> throwE "embed': SLEqTy cannot be embedded directly" + SKnownNatTy _n -> throwE "embed': SKnownNatTy cannot be embedded directly" STYPE _ -> absurd <$> hoistEff repr SRuntimeRepTy -> absurd <$> hoistEff repr SBoxedRep _ -> absurd <$> hoistEff repr @@ -363,12 +365,12 @@ embed' subst sty repr = case sty of SUnsafeEqualityTy {} -> do -- Get the type of the expression. ty <- liftEff $ embedSTy subst sty - (tc, args) <- failWithE () $ splitTyConApp_maybe ty + (tc, args) <- failWithE "embed': expected TyCon application for UnsafeEqualityTy" $ splitTyConApp_maybe ty -- Fetch the 'UnsafeRefl' DataCon. dc <- case tyConDataCons_maybe tc of Just [dc] -> pure dc - _ -> throwE () + _ -> throwE "embed': expected a single data constructor for UnsafeEqualityTy" -- Construct the spine. let spine = mkCon $ mkDataCon @64 dc @@ -376,7 +378,7 @@ embed' subst sty repr = case sty of -- Fetch the type arguments directly. (kind, tyL, tyR) <- case args of [kind, tyL, tyR] -> pure (kind, tyL, tyR) - _ -> throwE () + _ -> throwE "embed': expected exactly three type arguments for UnsafeEqualityTy" -- Force the coercion. co <- hoistEff repr @@ -387,7 +389,7 @@ embed' subst sty repr = case sty of project' :: HasCallStack => Deferrable es - => Error () :> es + => Error String :> es => Context Reader BuiltInTyCon :> es => Context Reader FamInstEnvs :> es => Subst @@ -397,24 +399,24 @@ project' project' subst sty expr = case sty of SBoolTy -> hoistEff expr >>= \case Lit (Bool b) -> pure b - _ -> throwE () + _ -> throwE "project': expected a Bool literal" SIntegerTy -> hoistEff expr >>= \case Lit (Integer i) -> pure i - _ -> throwE () + _ -> throwE "project': expected an Integer literal" SBitVecTy _n -> do Reduction co _ <- liftEff $ normaliseSTy subst Nominal sty inner <- hoistEff expr expr' <- mkCast inner $ mkSubCo co case expr' of Lit (BitVec bv) -> pure $ SomeBitVec bv - _ -> throwE () + _ -> throwE "project': expected a BitVec literal" SArrayTy _ _ -> do Reduction co _ <- liftEff $ normaliseSTy subst Nominal sty inner <- hoistEff expr expr' <- mkCast inner $ mkSubCo co case expr' of Lit (Array bv) -> pure $ SomeArray bv - _ -> throwE () + _ -> throwE "project': expected an Array literal" SPrimitiveTy pty -> do _ <- hoistEff expr pty' <- liftEff $ embedSTy subst pty @@ -440,9 +442,9 @@ project' subst sty expr = case sty of Reduction co _ <- liftEff $ normaliseSTy subst Nominal sty repr <- hoistEff expr mkCast repr $ mkSubCo co - SNaturalTy -> throwE () - SNatural -> throwE () - SAddTy _ _ -> throwE () + SNaturalTy -> throwE "project': SNaturalTy cannot be projected directly" + SNatural -> throwE "project': SNatural cannot be projected directly" + SAddTy _ _ -> throwE "project': SAddTy cannot be projected directly" SLEqTy _ _ -> do -- TODO: I guess we should actually ensure that this is well formed? It's -- a type family though, so I'm not sure how much actually remains of this @@ -455,7 +457,7 @@ project' subst sty expr = case sty of -- Construct a coercion from the Pantomime 'KnownNat' to 'Integer'. Note -- that we do not want to fully instantiate newtypes as this would lead us -- to the Haskell 'Integer'. - co <- failWithE () do + co <- failWithE "project': could not construct KnownNat to Integer coercion" do (tc, args) <- splitTyConApp_maybe ty (ty', co) <- instNewTyCon_maybe tc args (tc', args') <- splitTyConApp_maybe ty' @@ -471,18 +473,18 @@ project' subst sty expr = case sty of -- value, the error should be something closed to an 'unknown' SMT solver -- result. Nothing in fact is invalid, it is just not solvable. Lit (Integer i) | Just n <- toCon i >>= someNatVal -> pure n - _ -> throwE () - STYPE _ -> throwE () - SRuntimeRepTy -> throwE () - SBoxedRep _ -> throwE () - SLevityTy -> throwE () - SLifted -> throwE () + _ -> throwE "project': expected a concrete Integer for KnownNat projection" + STYPE _ -> throwE "project': STYPE cannot be projected directly" + SRuntimeRepTy -> throwE "project': SRuntimeRepTy cannot be projected directly" + SBoxedRep _ -> throwE "project': SBoxedRep cannot be projected directly" + SLevityTy -> throwE "project': SLevityTy cannot be projected directly" + SLifted -> throwE "project': SLifted cannot be projected directly" SUnsafeEqualityTy {} -> do expr' <- hoistEff expr let (_spine, args) = collectArgs expr' case args of [_kind, _ty, co] -> liftEff $ forceCo co - _ -> throwE () + _ -> throwE "project': expected exactly three arguments for UnsafeEqualityTy" embedSTy :: HasCallStack diff --git a/src/Pantomime/Expr.hs b/src/Pantomime/Expr.hs index cf46045..fff209a 100644 --- a/src/Pantomime/Expr.hs +++ b/src/Pantomime/Expr.hs @@ -76,7 +76,9 @@ import GHC.Utils.Outputable ( Outputable (..) , IsLine (..) , SDoc + , text , ($+$) + , (<+>) , parens , hang , nest @@ -437,16 +439,16 @@ mkEnumCon :: forall n es . KnownPos n => Deferrable es - => Error () :> es + => Error String :> es => Context Reader BuiltInTyCon :> es => SymBitVec n -> Type -> Eval es Expr mkEnumCon tag ty = do -- Ensure we have an enumeration type. - (tc, targs) <- failWithE () $ splitTyConApp_maybe ty + (tc, targs) <- failWithE "Expected a TyCon application for enumeration type" $ splitTyConApp_maybe ty unless (isEnumerationTyCon tc) do - throwE () + throwE "Expected an enumeration TyCon for mkEnumCon" -- Construct the data constructor and its type arguments. let dc = mkCon $ EnumCon tag tc @@ -461,7 +463,7 @@ constructorTyCon = \case -- | Get the 'Type' of a constructor. constructorType - :: Error () :> es + :: Error String :> es => Constructor -> Eff es Type constructorType con = do @@ -469,7 +471,7 @@ constructorType con = do DataCon dc -> pure dc EnumCon _tag tc | dc : _ <- tyConDataCons tc -> pure dc - | otherwise -> throwError () + | otherwise -> throwError "Cannot get constructor type: enumeration TyCon has no data constructors" pure $ varType (dataConWorkId dc) pprExpr @@ -607,7 +609,7 @@ mkLam ty closure = Lam ty <$> deferE closure mkApp :: HasCallStack => Deferrable es - => Error () :> es + => Error String :> es => Context Reader BuiltInTyCon :> es => Expr -> Arg @@ -626,12 +628,12 @@ mkApp fun arg = case fun of | isForAllTy ty -> do forced <- forceTyCo arg pure $ App fun (Forced forced) - | otherwise -> throwError () + | otherwise -> throwError "Cannot apply argument: expression type is neither a function nor a forall" pushCoArg :: HasCallStack => Deferrable es - => Error () :> es + => Error String :> es => Context Reader BuiltInTyCon :> es => CoercionR -> Arg @@ -643,14 +645,14 @@ pushCoArg co arg = if ty <- forceTy arg -- Attempt to push the coercion into the type argument. - (ty', rco) <- failWith () $ pushCoTyArg co ty + (ty', rco) <- failWith "pushCoArg: could not push coercion into type argument" $ pushCoTyArg co ty -- Return the type argument and result coercion. pure (pure $ mkType ty', rco) | otherwise -> do -- Attempt to split the coercion into an argument and result coercion. - (aco, rco) <- failWith () $ pushCoValArg co + (aco, rco) <- failWith "pushCoArg: could not push coercion into value argument" $ pushCoValArg co -- Cast the argument and return the result coercion. arg' <- defer do @@ -662,7 +664,7 @@ pushCoArg co arg = if mkApps :: HasCallStack => Deferrable es - => Error () :> es + => Error String :> es => Context Reader BuiltInTyCon :> es => Expr -> [Arg] @@ -671,7 +673,7 @@ mkApps = foldM mkApp mkCastMCo :: HasCallStack - => Error () :> es + => Error String :> es => Context Reader BuiltInTyCon :> es => Expr -> MCoercionR @@ -682,7 +684,7 @@ mkCastMCo expr = \case mkCast :: HasCallStack - => Error () :> es + => Error String :> es => Context Reader BuiltInTyCon :> es => Expr -> CoercionR @@ -690,14 +692,12 @@ mkCast mkCast expr co = do -- Ensure the coercion has role representational. unless (coercionRole co == Representational) do - -- FIXME: Make this a proper error. - throwE () + throwE "mkCast: coercion role must be Representational" -- Ensure the cast can be applied to the expression. ty <- liftEff $ exprType expr unless (eqType ty $ coercionLKind co) do - -- FIXME: Make this a proper error. - throwE () + throwE "mkCast: expression type does not match coercion source type" case expr of Cast body co' -> do @@ -746,7 +746,7 @@ mkRaise = mkVariant . Raise forceTyCo :: forall es . HasCallStack - => Error () :> es + => Error String :> es => Arg -> Eff es (Either Type Coercion) forceTyCo = runRuntime >>> \case @@ -756,30 +756,30 @@ forceTyCo = runRuntime >>> \case | Coercion co <- value -> pure $ Right co -- The expression was not in the expected shape. - _ -> throwError () + _ -> throwError "forceTyCo: expected a single Type or Coercion expression" -- | Force an expression into a type using 'forceTyCo'. forceTy :: HasCallStack - => Error () :> es + => Error String :> es => Arg -> Eff es Type -forceTy = forceTyCo >=> either pure (const $ throwError ()) +forceTy = forceTyCo >=> either pure (const $ throwError "forceTy: expected a Type, got a Coercion") -- | Force an expression into a coercion using 'forceTyCo'. forceCo :: HasCallStack - => Error () :> es + => Error String :> es => Arg -> Eff es Coercion -forceCo = forceTyCo >=> either (const $ throwError ()) pure +forceCo = forceTyCo >=> either (const $ throwError "forceCo: expected a Coercion, got a Type") pure -- | Equivalence between constructors. -- -- Will throw an error if the types do not match. eqCon :: HasCallStack - => Error () :> es + => Error String :> es => Constructor -> Constructor -> Eff es SymBool @@ -789,20 +789,20 @@ eqCon = \cases (EnumCon @l ltag ltc) (EnumCon @r rtag rtc) | ltc == rtc , Just Refl <- eqT @l @r -> pure $ ltag .== rtag - _ _ -> throwError () + _ _ -> throwError "eqCon: mismatched constructor types" -- TODO: This function deserves some clean-up! My syntax highlighter is even -- breaking on it... exprType :: HasCallStack - => Error () :> es + => Error String :> es => Context Reader BuiltInTyCon :> es => Expr -> Eff es Type exprType = \case Lit lit -> embedLitTyOf lit Con con -> constructorType con - Type _ -> throwError () + Type _ -> throwError "exprType: cannot get the type of a Type expression" Coercion co -> pure $ coercionType co Lam ty _ -> pure ty App fun arg -> do @@ -813,14 +813,14 @@ exprType = \case aty <- case arg of Forced (Right co) -> pure $ mkCoercionTy co Forced (Left ty) -> pure ty - _ -> throwError () + _ -> throwError "exprType: expected a forced Type or Coercion argument" let scope = mkInScopeSet $ tyCoVarsOfTypes [aty, rty] let subst = GHC.extendTCvSubst (GHC.mkEmptySubst scope) var aty pure $ GHC.substTy subst rty | Just (_, _, _, rty) <- splitFunTy_maybe fty -> pure rty - | otherwise -> throwError () + | otherwise -> throwError "exprType: expected a function or forall type in application" Cast _ co -> pure $ coercionRKind co -- | Collect the arguments of an application. @@ -868,7 +868,7 @@ unthunk = \case collectScrut :: HasCallStack => Deferrable es - => Error () :> es + => Error String :> es => Context Reader BuiltInTyCon :> es => Expr -> Eval es (Either Expr Constructor, [Arg]) @@ -883,7 +883,7 @@ collectScrut = \case let (spine, args) = collectThunks body' spine' <- case spine of Con lit -> pure lit - _ -> throwE () + _ -> throwE "collectScrut: expected a constructor at the spine of a cast expression" -- Only a DataCon spine may have its arguments pushed. dc <- case spine' of @@ -891,7 +891,7 @@ collectScrut = \case -- Any Enum DataCon suffices, as we only use its type (and all enum con -- have the same type). EnumCon _ tc | dc : _ <- tyConDataCons tc -> pure dc - _ -> throwE () + _ -> throwE "collectScrut: expected a DataCon or EnumCon with data constructors" -- Push the coercion into the arguments. (_univ, args') <- liftEff $ pushCoDataCon dc args co @@ -917,7 +917,7 @@ collectScrut = \case pushCoDataCon :: HasCallStack => Deferrable es - => Error () :> es + => Error String :> es => Context Reader BuiltInTyCon :> es => DataCon -> [Thunk] @@ -926,9 +926,9 @@ pushCoDataCon pushCoDataCon dc args co = do -- Check whether the outer type is a TyConAppCo. let tyR = coercionRKind co - (tcR, univArgsR) <- failWith () $ splitTyConApp_maybe tyR + (tcR, univArgsR) <- failWith "pushCoDataCon: expected a TyConApp coercion" $ splitTyConApp_maybe tyR unless (tcR == dataConTyCon dc) do - throwError () + throwError "pushCoDataCon: TyCon mismatch in coercion" -- Gather information on type variables of the DataCon. let dcUnivVars = dataConUnivTyVars dc @@ -940,10 +940,10 @@ pushCoDataCon dc args co = do exTys <- for exArgs \case -- TODO: Do we need to wrap Coercions with mkCoercionTy? Forced (Left ty) -> pure ty - _ -> throwError () + _ -> throwError "pushCoDataCon: expected forced type arguments for existential type variables" valArgs' <- for valArgs \case Thunked value -> pure value - Forced _ -> throwError () + Forced _ -> throwError "pushCoDataCon: expected thunked value arguments" pure (exTys, valArgs') -- Get coercions for the universal type variables. diff --git a/src/Pantomime/Fresh.hs b/src/Pantomime/Fresh.hs index 5300a2b..e5c5054 100644 --- a/src/Pantomime/Fresh.hs +++ b/src/Pantomime/Fresh.hs @@ -12,7 +12,7 @@ import GHC.Core.TyCo.Rep (scaledThing, UnivCoProvenance (..)) import GHC.Core.TyCon.Env (TyConEnv, lookupTyConEnv) import GHC.Core.Unify (tcUnifyTysFG, alwaysBindFun, UnifyResultM (..)) import GHC.Types.Unique (Uniquable (..), getKey) -import GHC.Utils.Outputable (Outputable (..)) +import GHC.Utils.Outputable (Outputable (..), text, (<+>), showSDocUnsafe) import GHC.Plugins qualified as GHC import GHC.Plugins ( Var @@ -159,7 +159,7 @@ symbolicVar var dst = case varArgs var of freshExpr :: HasCallStack => Deferrable es - => Error () :> es + => Error String :> es => Context Reader FamInstEnvs :> es => Context Reader BuiltInTyCon :> es => TyConEnv TyCon @@ -193,7 +193,7 @@ freshExpr axioms root = do -- some sort of 'asum' like operation? Actually, NonDet from 'effectful' -- would be perfect! We should move the code that deals with -- reifyLitType adjecent to its call once we do this! - result <- liftEff . runErrorNoCallStack @() $ projectLitTy ty + result <- liftEff . runErrorNoCallStack @String $ projectLitTy ty let isEqPred' ty' = do (tc, args) <- splitTyConApp_maybe ty' @@ -383,10 +383,9 @@ freshExpr axioms root = do -- For enum TyCon, we of course do plan to use it, so there we do need -- the Unreachable statement. - -- TODO: Throw proper error! | otherwise -> do dbgE ["could not create fresh value for", ppr ty] - throwE () + throwE $ showSDocUnsafe $ text "Could not create a fresh symbolic value for type:" <+> ppr ty go Variable { varName = GHC.varName root @@ -398,7 +397,7 @@ freshExpr axioms root = do freshArgs :: HasCallStack => Deferrable es - => Error () :> es + => Error String :> es => Context Reader BuiltInTyCon :> es => Context Reader FamInstEnvs :> es => TypeAxiomsR diff --git a/src/Pantomime/Literal.hs b/src/Pantomime/Literal.hs index 2b8a3d1..f89cef3 100644 --- a/src/Pantomime/Literal.hs +++ b/src/Pantomime/Literal.hs @@ -47,6 +47,7 @@ import GHC.Plugins , Outputable (..) , SDoc , IsLine (..) + , text , mkTyConTy , mkNumLitTy , mkTyConApp @@ -347,7 +348,7 @@ embedLitTyOf (Literal ty _) = embedLitTy ty -- reduced. projectLitTy :: HasCallStack - => Error () :> es + => Error String :> es => Context Reader BuiltInTyCon :> es => Context Reader FamInstEnvs :> es => Type @@ -367,13 +368,13 @@ projectLitTy ty = do -- any type families or aliases. projectLitTy' :: HasCallStack - => Error () :> es + => Error String :> es => Context Reader BuiltInTyCon :> es => Type -> Eff es SomeLiteralType projectLitTy' ty = do -- TODO: We should fix the recursive callstack grow! - (tc, targs) <- failWith () $ splitTyConApp_maybe ty + (tc, targs) <- failWith "projectLitTy': expected a TyCon application" $ splitTyConApp_maybe ty BuiltInTyCon { .. } <- get if | tc == tcBool @@ -385,8 +386,8 @@ projectLitTy' ty = do | tc == tcBitVec , [narg] <- targs -> do let knownNatTy = isNumLitTy >=> someNatVal - SomeNat @n _ <- failWith () $ knownNatTy narg - Dict <- failWith () $ posNat @n + SomeNat @n _ <- failWith "projectLitTy': expected a KnownNat literal" $ knownNatTy narg + Dict <- failWith "projectLitTy': expected a positive Nat for BitVec size" $ posNat @n pure $ SomeLiteralType (BitVecType @n) | tc == tcArray @@ -395,4 +396,4 @@ projectLitTy' ty = do SomeLiteralType valTy' <- projectLitTy' valTy pure $ SomeLiteralType (ArrayType keyTy' valTy') - | otherwise -> throwError () + | otherwise -> throwError "projectLitTy': unsupported literal type" diff --git a/src/Pantomime/Passes.hs b/src/Pantomime/Passes.hs index deac820..d70dad7 100644 --- a/src/Pantomime/Passes.hs +++ b/src/Pantomime/Passes.hs @@ -104,7 +104,7 @@ runSymbolic , Error OversaturatedError , Error UnificationError , Error SolverError - , Error () + , Error String , Provider_ Solver () , HasAnnotations , THNameToGHCName @@ -135,7 +135,7 @@ runSymbolic guts . runThNameToGhcName . runHasAnnotations . runProvider_ (const $ runSolver solver) - . runErrorWith @() propagateErrorShow + . runErrorWith @String propagateErrorShow . runErrorWith @SolverError propagateErrorShow . runErrorWith @UnificationError propagateError . runErrorWith @OversaturatedError propagateError @@ -199,7 +199,7 @@ printAndLint bind = do checkValidityAndEmbed :: ( HasCallStack - , Error () :> es + , Error String :> es , Error (LookupError Name) :> es , Error (LookupError TH.Name) :> es , Error SolverError :> es diff --git a/src/Pantomime/PrimOps.hs b/src/Pantomime/PrimOps.hs index c489f71..5c9f625 100644 --- a/src/Pantomime/PrimOps.hs +++ b/src/Pantomime/PrimOps.hs @@ -81,6 +81,7 @@ import Effectful.Error.Static (HasCallStack, Error) import GHC.Core.FamInstEnv (FamInstEnvs) import GHC.Core.TyCo.Rep (UnivCoProvenance(..)) import GHC.Plugins (Role (..), emptySubst, dataConTagZ, mkUnivCo) +import GHC.Utils.Outputable (SDoc, text) import GHC.TypeLits (type (<=), SomeNat (..), natVal, pattern SNat) import Grisette @@ -138,6 +139,7 @@ import Prelude , Num (..) , Integral (..) , Maybe (..) + , String , type (~) , ($) , (<$>) @@ -159,7 +161,7 @@ import Prelude type PrimOp es = HasCallStack => Deferrable es - => Error () :> es + => Error String :> es => Context Reader BuiltInTyCon :> es => Context Reader FamInstEnvs :> es => Eval es Expr @@ -190,7 +192,7 @@ type TagToEnumOp tagToEnum :: PrimOp es tagToEnum = embed2 @TagToEnumOp \ty bvE -> do SomeBitVec @n bv <- hoistEff bvE - Refl <- failWithE () $ eqT @n @64 + Refl <- failWithE "tagToEnum: expected 64-bit bitvector" $ eqT @n @64 -- TODO: I'm not sure how this interacts with the whole type normalisation. -- I don't think this is correct. Maybe we should reduce the type first? I -- guess we could also opt to do this within the embedding. This one is likely @@ -221,7 +223,7 @@ embed2 => Wrapped (Deferred a) ~ Runtime (Repr ty) => Defer es a => Wrap (Deferred a) - => Error () :> es + => Error String :> es => Context Reader BuiltInTyCon :> es => Context Reader FamInstEnvs :> es => a @@ -245,7 +247,7 @@ dataToTag = embed2 @DataToTagOp \_ _ valueE -> do case fst $ collectArgs value of Con (DataCon dc) -> pure $ SomeBitVec @64 (fromIntegral $ dataConTagZ dc) Con (EnumCon @n tag _) | Just Refl <- eqT @n @64 -> pure $ SomeBitVec tag - _ -> throwE () + _ -> throwE "dataToTag: expected a DataCon or EnumCon constructor" type RaiseOp = Forall 0 LevityTy @@ -285,7 +287,7 @@ not = embed2 @(BoolTy :-> BoolTy) \value -> do boolbinary :: HasCallStack => Deferrable es - => Error () :> es + => Error String :> es => Context Reader BuiltInTyCon :> es => Context Reader FamInstEnvs :> es => (SymBool -> SymBool -> SymBool) @@ -320,7 +322,7 @@ type IntegerBitVecOp i2bv :: PrimOp es i2bv = embed2 @IntegerBitVecOp \_ n _ i -> do SomeNat @n _ <- hoistEff n - Dict <- failWithE () $ posNat @n + Dict <- failWithE "i2bv: expected a positive Nat" $ posNat @n i' <- hoistEff i pure $ SomeBitVec @n (symFromIntegral i') @@ -335,7 +337,7 @@ iabs = embed2 @(IntegerTy :-> IntegerTy) \value -> do ibinary :: HasCallStack => Deferrable es - => Error () :> es + => Error String :> es => Context Reader BuiltInTyCon :> es => Context Reader FamInstEnvs :> es => (SymInteger -> SymInteger -> SymInteger) @@ -360,7 +362,7 @@ imod = ibinary mod icompare :: HasCallStack => Deferrable es - => Error () :> es + => Error String :> es => Context Reader BuiltInTyCon :> es => Context Reader FamInstEnvs :> es => (SymInteger -> SymInteger -> SymBool) @@ -410,7 +412,7 @@ type UnBitVecOp bvunary :: HasCallStack => Deferrable es - => Error () :> es + => Error String :> es => Context Reader BuiltInTyCon :> es => Context Reader FamInstEnvs :> es => (forall n. KnownPos n => SymBitVec n -> SymBitVec n) @@ -436,7 +438,7 @@ type BinBitVecOp bvbinary :: HasCallStack => Deferrable es - => Error () :> es + => Error String :> es => Context Reader BuiltInTyCon :> es => Context Reader FamInstEnvs :> es => (forall n. KnownPos n => SymBitVec n -> SymBitVec n -> SymBitVec n) @@ -444,7 +446,7 @@ bvbinary bvbinary f = embed2 @BinBitVecOp \_n lhs rhs -> do SomeBitVec @nl lhs' <- hoistEff lhs SomeBitVec @nr rhs' <- hoistEff rhs - Refl <- failWithE () $ eqT @nl @nr + Refl <- failWithE "Bitvector binary operation: width mismatch" $ eqT @nl @nr pure $ SomeBitVec (f lhs' rhs') asSignedBin @@ -522,7 +524,7 @@ type CompareBitVecOp bvcompare :: HasCallStack => Deferrable es - => Error () :> es + => Error String :> es => Context Reader BuiltInTyCon :> es => Context Reader FamInstEnvs :> es => (forall n. KnownPos n => SymBitVec n -> SymBitVec n -> SymBool) @@ -530,7 +532,7 @@ bvcompare bvcompare f = embed2 @CompareBitVecOp \_ lhs rhs -> do SomeBitVec @nl lhs' <- hoistEff lhs SomeBitVec @nr rhs' <- hoistEff rhs - Refl <- failWithE () $ eqT @nl @nr + Refl <- failWithE "Bitvector comparison: width mismatch" $ eqT @nl @nr pure $ f lhs' rhs' asSignedCmp @@ -598,8 +600,8 @@ bvextend bvextend f = embed2 @ExtendBitVecOp \_ _ r _ bv -> do SomeBitVec @l bv' <- hoistEff bv SomeNat @r _ <- hoistEff r - Dict <- failWithE () $ leqNat @l @r - Dict <- failWithE () $ posNat @r + Dict <- failWithE "Bitvector extend: size constraint violation (l <= r)" $ leqNat @l @r + Dict <- failWithE "Bitvector extend: expected positive result size" $ posNat @r pure $ SomeBitVec (f (Proxy @r) bv') bvzext :: PrimOp es @@ -631,9 +633,9 @@ bvselect = embed2 @SelectBitVecOp \_ _ _ idx width _ _ bv -> do SomeNat @idx _ <- hoistEff idx SomeNat @width _ <- hoistEff width SomeBitVec @n bv' <- hoistEff bv - Dict <- failWithE () $ posNat @width + Dict <- failWithE "Bitvector select: expected positive width" $ posNat @width SNat @sum <- pure $ SNat @idx %+ SNat @width - Dict <- failWithE () $ leqNat @sum @n + Dict <- failWithE "Bitvector select: index+width exceeds bitvector size" $ leqNat @sum @n pure $ SomeBitVec (sizedBVSelect (Proxy @idx) (Proxy @width) bv') -- :: forall k v. Primitive k => Primitive v => v -> Array k v @@ -653,7 +655,7 @@ aconst = embed2 @ArrayConstOp \_ _ pk _ valE -> do -- Gather the literal, knowing it is one due to the constraint. Literal @v vty val <- hoistEff valE >>= \case Lit lit -> pure lit - _ -> throwE () + _ -> throwE "aconst: expected a literal value" -- Gather evidence required to perform the array operation. Dict <- pure $ evidence kty @@ -679,10 +681,10 @@ aselect = embed2 @ArraySelectOp \_ _ arrE keyE -> do -- Gather the literal, knowing it is one due to the constraint. Literal kty key <- hoistEff keyE >>= \case Lit lit -> pure lit - _ -> throwE () + _ -> throwE "aselect: expected a literal key" -- Gather evidence required to perform the array operation. - Refl <- failWithE () $ eqLiteralType (literalType @k) kty + Refl <- failWithE "aselect: key type mismatch" $ eqLiteralType (literalType @k) kty -- Select the value out of the array and wrap it back into an expression. let val = Literal (literalType @v) $ Array.select arr key @@ -705,16 +707,16 @@ astore = embed2 @ArrayStoreOp \_ _ arrE keyE valE -> do -- Gather the literal, knowing it is one due to the constraint. Literal kty key <- hoistEff keyE >>= \case Lit lit -> pure lit - _ -> throwE () + _ -> throwE "astore: expected a literal key" -- Gather the literal, knowing it is one due to the constraint. Literal vty val <- hoistEff valE >>= \case Lit lit -> pure lit - _ -> throwE () + _ -> throwE "astore: expected a literal value" -- Gather evidence required to perform the array operation. - Refl <- failWithE () $ eqLiteralType (literalType @k) kty - Refl <- failWithE () $ eqLiteralType (literalType @v) vty + Refl <- failWithE "astore: key type mismatch" $ eqLiteralType (literalType @k) kty + Refl <- failWithE "astore: value type mismatch" $ eqLiteralType (literalType @v) vty -- Create the modified array. let array = Array.store arr key val @@ -732,6 +734,6 @@ aeq = embed2 @ArrayEqOp \_ _ arrL arrR -> do SomeArray @kL @vL arrL' <- hoistEff arrL SomeArray @kR @vR arrR' <- hoistEff arrR - Refl <- failWithE () $ eqLiteralType (literalType @kL) (literalType @kR) - Refl <- failWithE () $ eqLiteralType (literalType @vL) (literalType @vR) + Refl <- failWithE "Array equality: key type mismatch" $ eqLiteralType (literalType @kL) (literalType @kR) + Refl <- failWithE "Array equality: value type mismatch" $ eqLiteralType (literalType @vL) (literalType @vR) pure $ arrL' .== arrR' diff --git a/src/Pantomime/Solve.hs b/src/Pantomime/Solve.hs index 81b001e..bee2154 100644 --- a/src/Pantomime/Solve.hs +++ b/src/Pantomime/Solve.hs @@ -50,6 +50,7 @@ import GHC.Utils.Outputable ( Outputable (..) , IsLine (..) , SDoc + , text , (<+>) , empty ) @@ -118,7 +119,7 @@ type SymboliseEff = [ Context Reader BuiltInTyCon , Context Reader InterfaceThings , Context Reader FamInstEnvs - , Error () + , Error String ] newtype Lie a where @@ -133,7 +134,7 @@ construct => Context Reader BuiltInTyCon :> es => Context Reader InterfaceThings :> es => Context Reader FamInstEnvs :> es - => Error () :> es + => Error String :> es => [(Var, forall fs. PrimOp fs)] -> PluginAxiomsR -> CoreProgram @@ -173,7 +174,7 @@ construct prim PluginAxiomsR { .. } program expr = inject @SymboliseEff $ withDe res <- mkApps fun $ fmap snd args case res of Lit (Bool value) -> pure value - _ -> throwE () + _ -> throwE @String "Result of symbolic evaluation is not a Boolean literal" -- TODO: What to do about raise? Do we really just want to return false? I -- guess for now it is fine. @@ -209,7 +210,7 @@ instance Outputable Counterexample where checkValid :: forall es . HasCallStack - => Error () :> es + => Error String :> es => Error (LookupError TH.Name) :> es => Error (LookupError Name) :> es => Error SolverError :> es diff --git a/src/Pantomime/Subst.hs b/src/Pantomime/Subst.hs index 813a1e6..46ff9a1 100644 --- a/src/Pantomime/Subst.hs +++ b/src/Pantomime/Subst.hs @@ -30,6 +30,7 @@ import GHC.Plugins , extendVarEnv , lookupVarEnv ) +import GHC.Utils.Outputable (SDoc, text) import Control.Monad (foldM) @@ -60,7 +61,7 @@ mkEmptySubst = Subst -- | Extend the substitution with the given mapping. extendSubst :: HasCallStack - => Error () :> es + => Error String :> es => Subst -> Var -> Arg @@ -92,7 +93,7 @@ extendSubst subst var arg = if -- | Extend the substitution with the given mappings. extendSubstMany :: HasCallStack - => Error () :> es + => Error String :> es => Foldable f => Subst -> f (Var, Arg) @@ -102,7 +103,7 @@ extendSubstMany = foldM $ uncurry . extendSubst -- | Extend the identifier substitution with the given mapping. extendIdSubst :: HasCallStack - => Error () :> es + => Error String :> es => Subst -> Id -> Spine @@ -112,12 +113,12 @@ extendIdSubst subst var arg = if -- Extend the identifier substitution. let idSubst' = extendVarEnv (idSubst subst) var arg pure subst { idSubst = idSubst' } - | otherwise -> throwError () + | otherwise -> throwError "extendIdSubst: expected an Id variable" -- | Extend the identifier substitution with the given mappings. extendIdSubstMany :: HasCallStack - => Error () :> es + => Error String :> es => Foldable f => Subst -> f (Id, Spine) diff --git a/src/Pantomime/Symbolise.hs b/src/Pantomime/Symbolise.hs index d80c3fc..7341d96 100644 --- a/src/Pantomime/Symbolise.hs +++ b/src/Pantomime/Symbolise.hs @@ -7,6 +7,7 @@ module Pantomime.Symbolise ) where import GHC.Plugins qualified as GHC +import GHC.Utils.Outputable (SDoc, text, ($+$), (<+>), showSDocUnsafe) import GHC.Builtin.Types.Prim ( intPrimTyCon , int8PrimTyCon @@ -41,7 +42,7 @@ import Effectful.Context symbolise :: HasCallStack => Deferrable es - => Error () :> es + => Error String :> es => Context Reader BuiltInTyCon :> es => Context Reader InterfaceThings :> es => Subst @@ -90,7 +91,12 @@ symbolise = go , GHC.ppr var , GHC.ppr $ GHC.idDetails var ] - throwE () + throwE $ showSDocUnsafe $ + text "Unbound variable in symbolise:" <+> GHC.ppr var + <+> text "of type:" <+> GHC.ppr (GHC.varType var) + $+$ text "The variable is not in the substitution, has no unfolding," + <+> text "is not a data constructor, and is not erased evidence." + $+$ text "Consider providing a term axiom mapping for this variable." GHC.Lit lit -> symboliseLit subst lit @@ -120,7 +126,8 @@ symbolise = go let expectedTy = substTy subst $ GHC.varType bndr scrutTy <- liftEff $ exprType scrut' unless (eqType scrutTy expectedTy) do - throwE () + throwE $ showSDocUnsafe $ text "Case scrutinee type mismatch: expected" + <+> GHC.ppr expectedTy <+> text "but got" <+> GHC.ppr scrutTy -- TODO: This is a bit ugly now. I guess it handles all the cases, but -- it could deserve some cleanup. It somehow feels weird to gather the @@ -158,7 +165,7 @@ symbolise = go GHC.LitAlt lit | Left spine' <- spine -> do symboliseEqLit subst spine' lit GHC.DEFAULT -> pure true - _ -> throwE () + _ -> throwE "Unsupported case alternative: expected DataAlt, LitAlt, or DEFAULT" -- TODO: Perhaps it's a good idea to check that the number of -- arguments match the binders (unless it is a DEFAULT, in which case @@ -195,7 +202,7 @@ symboliseBind :: forall es . HasCallStack => Deferrable es - => Error () :> es + => Error String :> es => Context Reader BuiltInTyCon :> es => Context Reader InterfaceThings :> es => Subst @@ -219,7 +226,7 @@ symboliseBindMany . HasCallStack => Deferrable es => Foldable f - => Error () :> es + => Error String :> es => Context Reader BuiltInTyCon :> es => Context Reader InterfaceThings :> es => Subst @@ -251,7 +258,7 @@ isPrimType ty = case GHC.splitTyConApp_maybe ty of symboliseLit :: HasCallStack => Deferrable es - => Error () :> es + => Error String :> es => Context Reader BuiltInTyCon :> es => Context Reader InterfaceThings :> es => Subst @@ -278,11 +285,11 @@ symboliseLit subst lit = do GHC.LitNumWord16 -> pure (toWord16Id, BitVec @16 num') GHC.LitNumWord32 -> pure (toWord32Id, BitVec @32 num') GHC.LitNumWord64 -> pure (toWord64Id, BitVec @64 num') - GHC.LitNumBigNat -> throwE () - _ -> throwE () + GHC.LitNumBigNat -> throwE "BigNat literals are not supported" + _ -> throwE "Unsupported literal type" -- Lookup the equality function. - convert <- failWithE () $ lookupIdSubst subst convertId + convert <- failWithE "Conversion function for literal type not found in substitution" $ lookupIdSubst subst convertId convert' <- hoistEff convert mkApps convert' [pure $ mkLit lit'] @@ -294,7 +301,7 @@ symboliseLit subst lit = do symboliseEqLit :: HasCallStack => Deferrable es - => Error () :> es + => Error String :> es => Context Reader InterfaceThings :> es => Context Reader BuiltInTyCon :> es => Subst @@ -316,11 +323,11 @@ symboliseEqLit subst lhs rhs = do GHC.LitNumWord16 -> pure eqWord16Id GHC.LitNumWord32 -> pure eqWord32Id GHC.LitNumWord64 -> pure eqWord64Id - GHC.LitNumBigNat -> throwE () - _ -> throwE () + GHC.LitNumBigNat -> throwE "BigNat literals are not supported in equality check" + _ -> throwE "Unsupported literal type in equality check" -- Lookup the equality function. - eq <- failWithE () $ GHC.maybeUnfoldingTemplate (GHC.realIdUnfolding eqId) + eq <- failWithE "Equality function for literal type not found" $ GHC.maybeUnfoldingTemplate (GHC.realIdUnfolding eqId) eq' <- symbolise subst eq lit <- deferE $ symboliseLit subst rhs @@ -329,4 +336,4 @@ symboliseEqLit subst lhs rhs = do result <- mkApps eq' [pure lhs, lit] case result of Lit (Bool result') -> pure result' - _ -> throwE () + _ -> throwE "Literal equality check did not produce a Boolean result" diff --git a/src/Pantomime/Unification.hs b/src/Pantomime/Unification.hs index 59243d8..d8f8184 100644 --- a/src/Pantomime/Unification.hs +++ b/src/Pantomime/Unification.hs @@ -388,7 +388,7 @@ unifyExprs lhs rhs = do -- functions in this module as well! subsumeExpr :: HasCallStack - => Error () :> es + => Error String :> es => TypeMap CoreExpr -> CoreExpr -> Type @@ -399,7 +399,7 @@ subsumeExpr dicts expr ty = do let (reqTv, reqEv, reqTy) = tcSplitSigmaTy ty -- Match the types and add all dictionaries we care about. - let err = () -- TODO: This should be a better error. + let err = "subsumeExpr: type matching failed" -- TODO: This should be a better error. subst <- failWith err $ tcMatchTy curTy reqTy -- Make evidence variables. @@ -412,7 +412,7 @@ subsumeExpr dicts expr ty = do insertTM (varType ev) (Var ev) acc let curEv' = substTy subst <$> curEv argsEv <- for curEv' \ev -> do - failWith () $ lookupTM ev dicts' + failWith "subsumeExpr: type variable instance not found in dictionary" $ lookupTM ev dicts' -- Construct the new expression. let open = mkApps expr $ fmap Type argsTv <> argsEv From e1fe436420b7cde585c1b2caa09883c71173fa10 Mon Sep 17 00:00:00 2001 From: Wind Date: Sun, 31 May 2026 18:17:08 +0200 Subject: [PATCH 6/8] Get rid of warnings --- src/Pantomime/Axiom.hs | 3 +-- src/Pantomime/Embed.hs | 44 +++++++++++++++++------------------- src/Pantomime/Expr.hs | 42 +++++++++++++++++----------------- src/Pantomime/Literal.hs | 8 +++---- src/Pantomime/PrimOps.hs | 37 +++++++++++++++--------------- src/Pantomime/Solve.hs | 1 - src/Pantomime/Subst.hs | 1 - src/Pantomime/Symbolise.hs | 2 +- src/Pantomime/Unification.hs | 4 ++-- 9 files changed, 68 insertions(+), 74 deletions(-) diff --git a/src/Pantomime/Axiom.hs b/src/Pantomime/Axiom.hs index 7e3eabd..79c04e5 100644 --- a/src/Pantomime/Axiom.hs +++ b/src/Pantomime/Axiom.hs @@ -44,7 +44,6 @@ import GHC.Utils.Outputable ( Outputable (..) , IsDoc (..) , IsLine (fsep, (<+>), text) - , SDoc , hang , punctuate , comma @@ -351,7 +350,7 @@ resolvePluginAxioms PluginAxioms { .. } = do -- Throw an error if we could not create any. when (null dictsNew) do - throwError "resolvePluginAxioms: could not create any Embeddable or Coercible dictionaries for the given axioms" + throwError @String "resolvePluginAxioms: could not create any Embeddable or Coercible dictionaries for the given axioms" -- Insert all dictionaries. pure $ foldlBy dicts dictsNew \acc dict -> do diff --git a/src/Pantomime/Embed.hs b/src/Pantomime/Embed.hs index cf85583..93a8970 100644 --- a/src/Pantomime/Embed.hs +++ b/src/Pantomime/Embed.hs @@ -22,8 +22,6 @@ import Effectful import Effectful.Error.Static (Error, HasCallStack) import Effectful.Context -import GHC.Utils.Outputable (SDoc, text) - import GHC.Builtin.Types.Literals (typeNatAddTyCon) import GHC.Builtin.Uniques (mkAlphaTyVarUnique) import GHC.Core.Type (substTy) @@ -325,7 +323,7 @@ embed' subst sty repr = case sty of Reduction co _ <- liftEff $ normaliseSTy subst Nominal sty let co' = mkSymCo $ mkSubCo co mkCast lit co' - SPrimitiveTy _ -> throwE "embed': cannot directly embed a PrimitiveTy — use project' first" + SPrimitiveTy _ -> throwE @String "embed': cannot directly embed a PrimitiveTy — use project' first" SLambda aty rty -> do -- Gather the type for the lambda. ty <- liftEff $ embedSTy subst sty @@ -355,8 +353,8 @@ embed' subst sty repr = case sty of SNaturalTy -> hoistEff repr >>= absurd SNatural -> hoistEff repr >>= absurd SAddTy _ _ -> hoistEff repr >>= absurd - SLEqTy _ _ -> throwE "embed': SLEqTy cannot be embedded directly" - SKnownNatTy _n -> throwE "embed': SKnownNatTy cannot be embedded directly" + SLEqTy _ _ -> throwE @String "embed': SLEqTy cannot be embedded directly" + SKnownNatTy _n -> throwE @String "embed': SKnownNatTy cannot be embedded directly" STYPE _ -> absurd <$> hoistEff repr SRuntimeRepTy -> absurd <$> hoistEff repr SBoxedRep _ -> absurd <$> hoistEff repr @@ -365,12 +363,12 @@ embed' subst sty repr = case sty of SUnsafeEqualityTy {} -> do -- Get the type of the expression. ty <- liftEff $ embedSTy subst sty - (tc, args) <- failWithE "embed': expected TyCon application for UnsafeEqualityTy" $ splitTyConApp_maybe ty + (tc, args) <- failWithE @String "embed': expected TyCon application for UnsafeEqualityTy" $ splitTyConApp_maybe ty -- Fetch the 'UnsafeRefl' DataCon. dc <- case tyConDataCons_maybe tc of Just [dc] -> pure dc - _ -> throwE "embed': expected a single data constructor for UnsafeEqualityTy" + _ -> throwE @String "embed': expected a single data constructor for UnsafeEqualityTy" -- Construct the spine. let spine = mkCon $ mkDataCon @64 dc @@ -378,7 +376,7 @@ embed' subst sty repr = case sty of -- Fetch the type arguments directly. (kind, tyL, tyR) <- case args of [kind, tyL, tyR] -> pure (kind, tyL, tyR) - _ -> throwE "embed': expected exactly three type arguments for UnsafeEqualityTy" + _ -> throwE @String "embed': expected exactly three type arguments for UnsafeEqualityTy" -- Force the coercion. co <- hoistEff repr @@ -399,24 +397,24 @@ project' project' subst sty expr = case sty of SBoolTy -> hoistEff expr >>= \case Lit (Bool b) -> pure b - _ -> throwE "project': expected a Bool literal" + _ -> throwE @String "project': expected a Bool literal" SIntegerTy -> hoistEff expr >>= \case Lit (Integer i) -> pure i - _ -> throwE "project': expected an Integer literal" + _ -> throwE @String "project': expected an Integer literal" SBitVecTy _n -> do Reduction co _ <- liftEff $ normaliseSTy subst Nominal sty inner <- hoistEff expr expr' <- mkCast inner $ mkSubCo co case expr' of Lit (BitVec bv) -> pure $ SomeBitVec bv - _ -> throwE "project': expected a BitVec literal" + _ -> throwE @String "project': expected a BitVec literal" SArrayTy _ _ -> do Reduction co _ <- liftEff $ normaliseSTy subst Nominal sty inner <- hoistEff expr expr' <- mkCast inner $ mkSubCo co case expr' of Lit (Array bv) -> pure $ SomeArray bv - _ -> throwE "project': expected an Array literal" + _ -> throwE @String "project': expected an Array literal" SPrimitiveTy pty -> do _ <- hoistEff expr pty' <- liftEff $ embedSTy subst pty @@ -442,9 +440,9 @@ project' subst sty expr = case sty of Reduction co _ <- liftEff $ normaliseSTy subst Nominal sty repr <- hoistEff expr mkCast repr $ mkSubCo co - SNaturalTy -> throwE "project': SNaturalTy cannot be projected directly" - SNatural -> throwE "project': SNatural cannot be projected directly" - SAddTy _ _ -> throwE "project': SAddTy cannot be projected directly" + SNaturalTy -> throwE @String "project': SNaturalTy cannot be projected directly" + SNatural -> throwE @String "project': SNatural cannot be projected directly" + SAddTy _ _ -> throwE @String "project': SAddTy cannot be projected directly" SLEqTy _ _ -> do -- TODO: I guess we should actually ensure that this is well formed? It's -- a type family though, so I'm not sure how much actually remains of this @@ -457,7 +455,7 @@ project' subst sty expr = case sty of -- Construct a coercion from the Pantomime 'KnownNat' to 'Integer'. Note -- that we do not want to fully instantiate newtypes as this would lead us -- to the Haskell 'Integer'. - co <- failWithE "project': could not construct KnownNat to Integer coercion" do + co <- failWithE @String "project': could not construct KnownNat to Integer coercion" do (tc, args) <- splitTyConApp_maybe ty (ty', co) <- instNewTyCon_maybe tc args (tc', args') <- splitTyConApp_maybe ty' @@ -473,18 +471,18 @@ project' subst sty expr = case sty of -- value, the error should be something closed to an 'unknown' SMT solver -- result. Nothing in fact is invalid, it is just not solvable. Lit (Integer i) | Just n <- toCon i >>= someNatVal -> pure n - _ -> throwE "project': expected a concrete Integer for KnownNat projection" - STYPE _ -> throwE "project': STYPE cannot be projected directly" - SRuntimeRepTy -> throwE "project': SRuntimeRepTy cannot be projected directly" - SBoxedRep _ -> throwE "project': SBoxedRep cannot be projected directly" - SLevityTy -> throwE "project': SLevityTy cannot be projected directly" - SLifted -> throwE "project': SLifted cannot be projected directly" + _ -> throwE @String "project': expected a concrete Integer for KnownNat projection" + STYPE _ -> throwE @String "project': STYPE cannot be projected directly" + SRuntimeRepTy -> throwE @String "project': SRuntimeRepTy cannot be projected directly" + SBoxedRep _ -> throwE @String "project': SBoxedRep cannot be projected directly" + SLevityTy -> throwE @String "project': SLevityTy cannot be projected directly" + SLifted -> throwE @String "project': SLifted cannot be projected directly" SUnsafeEqualityTy {} -> do expr' <- hoistEff expr let (_spine, args) = collectArgs expr' case args of [_kind, _ty, co] -> liftEff $ forceCo co - _ -> throwE "project': expected exactly three arguments for UnsafeEqualityTy" + _ -> throwE @String "project': expected exactly three arguments for UnsafeEqualityTy" embedSTy :: HasCallStack diff --git a/src/Pantomime/Expr.hs b/src/Pantomime/Expr.hs index fff209a..9e7ffb5 100644 --- a/src/Pantomime/Expr.hs +++ b/src/Pantomime/Expr.hs @@ -446,9 +446,9 @@ mkEnumCon -> Eval es Expr mkEnumCon tag ty = do -- Ensure we have an enumeration type. - (tc, targs) <- failWithE "Expected a TyCon application for enumeration type" $ splitTyConApp_maybe ty + (tc, targs) <- failWithE @String "Expected a TyCon application for enumeration type" $ splitTyConApp_maybe ty unless (isEnumerationTyCon tc) do - throwE "Expected an enumeration TyCon for mkEnumCon" + throwE @String "Expected an enumeration TyCon for mkEnumCon" -- Construct the data constructor and its type arguments. let dc = mkCon $ EnumCon tag tc @@ -471,7 +471,7 @@ constructorType con = do DataCon dc -> pure dc EnumCon _tag tc | dc : _ <- tyConDataCons tc -> pure dc - | otherwise -> throwError "Cannot get constructor type: enumeration TyCon has no data constructors" + | otherwise -> throwError @String "Cannot get constructor type: enumeration TyCon has no data constructors" pure $ varType (dataConWorkId dc) pprExpr @@ -628,7 +628,7 @@ mkApp fun arg = case fun of | isForAllTy ty -> do forced <- forceTyCo arg pure $ App fun (Forced forced) - | otherwise -> throwError "Cannot apply argument: expression type is neither a function nor a forall" + | otherwise -> throwError @String "Cannot apply argument: expression type is neither a function nor a forall" pushCoArg :: HasCallStack @@ -645,14 +645,14 @@ pushCoArg co arg = if ty <- forceTy arg -- Attempt to push the coercion into the type argument. - (ty', rco) <- failWith "pushCoArg: could not push coercion into type argument" $ pushCoTyArg co ty + (ty', rco) <- failWith @String "pushCoArg: could not push coercion into type argument" $ pushCoTyArg co ty -- Return the type argument and result coercion. pure (pure $ mkType ty', rco) | otherwise -> do -- Attempt to split the coercion into an argument and result coercion. - (aco, rco) <- failWith "pushCoArg: could not push coercion into value argument" $ pushCoValArg co + (aco, rco) <- failWith @String "pushCoArg: could not push coercion into value argument" $ pushCoValArg co -- Cast the argument and return the result coercion. arg' <- defer do @@ -692,12 +692,12 @@ mkCast mkCast expr co = do -- Ensure the coercion has role representational. unless (coercionRole co == Representational) do - throwE "mkCast: coercion role must be Representational" + throwE @String "mkCast: coercion role must be Representational" -- Ensure the cast can be applied to the expression. ty <- liftEff $ exprType expr unless (eqType ty $ coercionLKind co) do - throwE "mkCast: expression type does not match coercion source type" + throwE @String "mkCast: expression type does not match coercion source type" case expr of Cast body co' -> do @@ -756,7 +756,7 @@ forceTyCo = runRuntime >>> \case | Coercion co <- value -> pure $ Right co -- The expression was not in the expected shape. - _ -> throwError "forceTyCo: expected a single Type or Coercion expression" + _ -> throwError @String "forceTyCo: expected a single Type or Coercion expression" -- | Force an expression into a type using 'forceTyCo'. forceTy @@ -764,7 +764,7 @@ forceTy => Error String :> es => Arg -> Eff es Type -forceTy = forceTyCo >=> either pure (const $ throwError "forceTy: expected a Type, got a Coercion") +forceTy = forceTyCo >=> either pure (const $ throwError @String "forceTy: expected a Type, got a Coercion") -- | Force an expression into a coercion using 'forceTyCo'. forceCo @@ -772,7 +772,7 @@ forceCo => Error String :> es => Arg -> Eff es Coercion -forceCo = forceTyCo >=> either (const $ throwError "forceCo: expected a Coercion, got a Type") pure +forceCo = forceTyCo >=> either (const $ throwError @String "forceCo: expected a Coercion, got a Type") pure -- | Equivalence between constructors. -- @@ -789,7 +789,7 @@ eqCon = \cases (EnumCon @l ltag ltc) (EnumCon @r rtag rtc) | ltc == rtc , Just Refl <- eqT @l @r -> pure $ ltag .== rtag - _ _ -> throwError "eqCon: mismatched constructor types" + _ _ -> throwError @String "eqCon: mismatched constructor types" -- TODO: This function deserves some clean-up! My syntax highlighter is even -- breaking on it... @@ -802,7 +802,7 @@ exprType exprType = \case Lit lit -> embedLitTyOf lit Con con -> constructorType con - Type _ -> throwError "exprType: cannot get the type of a Type expression" + Type _ -> throwError @String "exprType: cannot get the type of a Type expression" Coercion co -> pure $ coercionType co Lam ty _ -> pure ty App fun arg -> do @@ -813,14 +813,14 @@ exprType = \case aty <- case arg of Forced (Right co) -> pure $ mkCoercionTy co Forced (Left ty) -> pure ty - _ -> throwError "exprType: expected a forced Type or Coercion argument" + _ -> throwError @String "exprType: expected a forced Type or Coercion argument" let scope = mkInScopeSet $ tyCoVarsOfTypes [aty, rty] let subst = GHC.extendTCvSubst (GHC.mkEmptySubst scope) var aty pure $ GHC.substTy subst rty | Just (_, _, _, rty) <- splitFunTy_maybe fty -> pure rty - | otherwise -> throwError "exprType: expected a function or forall type in application" + | otherwise -> throwError @String "exprType: expected a function or forall type in application" Cast _ co -> pure $ coercionRKind co -- | Collect the arguments of an application. @@ -883,7 +883,7 @@ collectScrut = \case let (spine, args) = collectThunks body' spine' <- case spine of Con lit -> pure lit - _ -> throwE "collectScrut: expected a constructor at the spine of a cast expression" + _ -> throwE @String "collectScrut: expected a constructor at the spine of a cast expression" -- Only a DataCon spine may have its arguments pushed. dc <- case spine' of @@ -891,7 +891,7 @@ collectScrut = \case -- Any Enum DataCon suffices, as we only use its type (and all enum con -- have the same type). EnumCon _ tc | dc : _ <- tyConDataCons tc -> pure dc - _ -> throwE "collectScrut: expected a DataCon or EnumCon with data constructors" + _ -> throwE @String "collectScrut: expected a DataCon or EnumCon with data constructors" -- Push the coercion into the arguments. (_univ, args') <- liftEff $ pushCoDataCon dc args co @@ -926,9 +926,9 @@ pushCoDataCon pushCoDataCon dc args co = do -- Check whether the outer type is a TyConAppCo. let tyR = coercionRKind co - (tcR, univArgsR) <- failWith "pushCoDataCon: expected a TyConApp coercion" $ splitTyConApp_maybe tyR + (tcR, univArgsR) <- failWith @String "pushCoDataCon: expected a TyConApp coercion" $ splitTyConApp_maybe tyR unless (tcR == dataConTyCon dc) do - throwError "pushCoDataCon: TyCon mismatch in coercion" + throwError @String "pushCoDataCon: TyCon mismatch in coercion" -- Gather information on type variables of the DataCon. let dcUnivVars = dataConUnivTyVars dc @@ -940,10 +940,10 @@ pushCoDataCon dc args co = do exTys <- for exArgs \case -- TODO: Do we need to wrap Coercions with mkCoercionTy? Forced (Left ty) -> pure ty - _ -> throwError "pushCoDataCon: expected forced type arguments for existential type variables" + _ -> throwError @String "pushCoDataCon: expected forced type arguments for existential type variables" valArgs' <- for valArgs \case Thunked value -> pure value - Forced _ -> throwError "pushCoDataCon: expected thunked value arguments" + Forced _ -> throwError @String "pushCoDataCon: expected thunked value arguments" pure (exTys, valArgs') -- Get coercions for the universal type variables. diff --git a/src/Pantomime/Literal.hs b/src/Pantomime/Literal.hs index f89cef3..d5d2f16 100644 --- a/src/Pantomime/Literal.hs +++ b/src/Pantomime/Literal.hs @@ -374,7 +374,7 @@ projectLitTy' -> Eff es SomeLiteralType projectLitTy' ty = do -- TODO: We should fix the recursive callstack grow! - (tc, targs) <- failWith "projectLitTy': expected a TyCon application" $ splitTyConApp_maybe ty + (tc, targs) <- failWith @String "projectLitTy': expected a TyCon application" $ splitTyConApp_maybe ty BuiltInTyCon { .. } <- get if | tc == tcBool @@ -386,8 +386,8 @@ projectLitTy' ty = do | tc == tcBitVec , [narg] <- targs -> do let knownNatTy = isNumLitTy >=> someNatVal - SomeNat @n _ <- failWith "projectLitTy': expected a KnownNat literal" $ knownNatTy narg - Dict <- failWith "projectLitTy': expected a positive Nat for BitVec size" $ posNat @n + SomeNat @n _ <- failWith @String "projectLitTy': expected a KnownNat literal" $ knownNatTy narg + Dict <- failWith @String "projectLitTy': expected a positive Nat for BitVec size" $ posNat @n pure $ SomeLiteralType (BitVecType @n) | tc == tcArray @@ -396,4 +396,4 @@ projectLitTy' ty = do SomeLiteralType valTy' <- projectLitTy' valTy pure $ SomeLiteralType (ArrayType keyTy' valTy') - | otherwise -> throwError "projectLitTy': unsupported literal type" + | otherwise -> throwError @String "projectLitTy': unsupported literal type" diff --git a/src/Pantomime/PrimOps.hs b/src/Pantomime/PrimOps.hs index 5c9f625..8426167 100644 --- a/src/Pantomime/PrimOps.hs +++ b/src/Pantomime/PrimOps.hs @@ -81,7 +81,6 @@ import Effectful.Error.Static (HasCallStack, Error) import GHC.Core.FamInstEnv (FamInstEnvs) import GHC.Core.TyCo.Rep (UnivCoProvenance(..)) import GHC.Plugins (Role (..), emptySubst, dataConTagZ, mkUnivCo) -import GHC.Utils.Outputable (SDoc, text) import GHC.TypeLits (type (<=), SomeNat (..), natVal, pattern SNat) import Grisette @@ -192,7 +191,7 @@ type TagToEnumOp tagToEnum :: PrimOp es tagToEnum = embed2 @TagToEnumOp \ty bvE -> do SomeBitVec @n bv <- hoistEff bvE - Refl <- failWithE "tagToEnum: expected 64-bit bitvector" $ eqT @n @64 + Refl <- failWithE @String "tagToEnum: expected 64-bit bitvector" $ eqT @n @64 -- TODO: I'm not sure how this interacts with the whole type normalisation. -- I don't think this is correct. Maybe we should reduce the type first? I -- guess we could also opt to do this within the embedding. This one is likely @@ -247,7 +246,7 @@ dataToTag = embed2 @DataToTagOp \_ _ valueE -> do case fst $ collectArgs value of Con (DataCon dc) -> pure $ SomeBitVec @64 (fromIntegral $ dataConTagZ dc) Con (EnumCon @n tag _) | Just Refl <- eqT @n @64 -> pure $ SomeBitVec tag - _ -> throwE "dataToTag: expected a DataCon or EnumCon constructor" + _ -> throwE @String "dataToTag: expected a DataCon or EnumCon constructor" type RaiseOp = Forall 0 LevityTy @@ -322,7 +321,7 @@ type IntegerBitVecOp i2bv :: PrimOp es i2bv = embed2 @IntegerBitVecOp \_ n _ i -> do SomeNat @n _ <- hoistEff n - Dict <- failWithE "i2bv: expected a positive Nat" $ posNat @n + Dict <- failWithE @String "i2bv: expected a positive Nat" $ posNat @n i' <- hoistEff i pure $ SomeBitVec @n (symFromIntegral i') @@ -446,7 +445,7 @@ bvbinary bvbinary f = embed2 @BinBitVecOp \_n lhs rhs -> do SomeBitVec @nl lhs' <- hoistEff lhs SomeBitVec @nr rhs' <- hoistEff rhs - Refl <- failWithE "Bitvector binary operation: width mismatch" $ eqT @nl @nr + Refl <- failWithE @String "Bitvector binary operation: width mismatch" $ eqT @nl @nr pure $ SomeBitVec (f lhs' rhs') asSignedBin @@ -532,7 +531,7 @@ bvcompare bvcompare f = embed2 @CompareBitVecOp \_ lhs rhs -> do SomeBitVec @nl lhs' <- hoistEff lhs SomeBitVec @nr rhs' <- hoistEff rhs - Refl <- failWithE "Bitvector comparison: width mismatch" $ eqT @nl @nr + Refl <- failWithE @String "Bitvector comparison: width mismatch" $ eqT @nl @nr pure $ f lhs' rhs' asSignedCmp @@ -600,8 +599,8 @@ bvextend bvextend f = embed2 @ExtendBitVecOp \_ _ r _ bv -> do SomeBitVec @l bv' <- hoistEff bv SomeNat @r _ <- hoistEff r - Dict <- failWithE "Bitvector extend: size constraint violation (l <= r)" $ leqNat @l @r - Dict <- failWithE "Bitvector extend: expected positive result size" $ posNat @r + Dict <- failWithE @String "Bitvector extend: size constraint violation (l <= r)" $ leqNat @l @r + Dict <- failWithE @String "Bitvector extend: expected positive result size" $ posNat @r pure $ SomeBitVec (f (Proxy @r) bv') bvzext :: PrimOp es @@ -633,9 +632,9 @@ bvselect = embed2 @SelectBitVecOp \_ _ _ idx width _ _ bv -> do SomeNat @idx _ <- hoistEff idx SomeNat @width _ <- hoistEff width SomeBitVec @n bv' <- hoistEff bv - Dict <- failWithE "Bitvector select: expected positive width" $ posNat @width + Dict <- failWithE @String "Bitvector select: expected positive width" $ posNat @width SNat @sum <- pure $ SNat @idx %+ SNat @width - Dict <- failWithE "Bitvector select: index+width exceeds bitvector size" $ leqNat @sum @n + Dict <- failWithE @String "Bitvector select: index+width exceeds bitvector size" $ leqNat @sum @n pure $ SomeBitVec (sizedBVSelect (Proxy @idx) (Proxy @width) bv') -- :: forall k v. Primitive k => Primitive v => v -> Array k v @@ -655,7 +654,7 @@ aconst = embed2 @ArrayConstOp \_ _ pk _ valE -> do -- Gather the literal, knowing it is one due to the constraint. Literal @v vty val <- hoistEff valE >>= \case Lit lit -> pure lit - _ -> throwE "aconst: expected a literal value" + _ -> throwE @String "aconst: expected a literal value" -- Gather evidence required to perform the array operation. Dict <- pure $ evidence kty @@ -681,10 +680,10 @@ aselect = embed2 @ArraySelectOp \_ _ arrE keyE -> do -- Gather the literal, knowing it is one due to the constraint. Literal kty key <- hoistEff keyE >>= \case Lit lit -> pure lit - _ -> throwE "aselect: expected a literal key" + _ -> throwE @String "aselect: expected a literal key" -- Gather evidence required to perform the array operation. - Refl <- failWithE "aselect: key type mismatch" $ eqLiteralType (literalType @k) kty + Refl <- failWithE @String "aselect: key type mismatch" $ eqLiteralType (literalType @k) kty -- Select the value out of the array and wrap it back into an expression. let val = Literal (literalType @v) $ Array.select arr key @@ -707,16 +706,16 @@ astore = embed2 @ArrayStoreOp \_ _ arrE keyE valE -> do -- Gather the literal, knowing it is one due to the constraint. Literal kty key <- hoistEff keyE >>= \case Lit lit -> pure lit - _ -> throwE "astore: expected a literal key" + _ -> throwE @String "astore: expected a literal key" -- Gather the literal, knowing it is one due to the constraint. Literal vty val <- hoistEff valE >>= \case Lit lit -> pure lit - _ -> throwE "astore: expected a literal value" + _ -> throwE @String "astore: expected a literal value" -- Gather evidence required to perform the array operation. - Refl <- failWithE "astore: key type mismatch" $ eqLiteralType (literalType @k) kty - Refl <- failWithE "astore: value type mismatch" $ eqLiteralType (literalType @v) vty + Refl <- failWithE @String "astore: key type mismatch" $ eqLiteralType (literalType @k) kty + Refl <- failWithE @String "astore: value type mismatch" $ eqLiteralType (literalType @v) vty -- Create the modified array. let array = Array.store arr key val @@ -734,6 +733,6 @@ aeq = embed2 @ArrayEqOp \_ _ arrL arrR -> do SomeArray @kL @vL arrL' <- hoistEff arrL SomeArray @kR @vR arrR' <- hoistEff arrR - Refl <- failWithE "Array equality: key type mismatch" $ eqLiteralType (literalType @kL) (literalType @kR) - Refl <- failWithE "Array equality: value type mismatch" $ eqLiteralType (literalType @vL) (literalType @vR) + Refl <- failWithE @String "Array equality: key type mismatch" $ eqLiteralType (literalType @kL) (literalType @kR) + Refl <- failWithE @String "Array equality: value type mismatch" $ eqLiteralType (literalType @vL) (literalType @vR) pure $ arrL' .== arrR' diff --git a/src/Pantomime/Solve.hs b/src/Pantomime/Solve.hs index bee2154..ea2f92b 100644 --- a/src/Pantomime/Solve.hs +++ b/src/Pantomime/Solve.hs @@ -50,7 +50,6 @@ import GHC.Utils.Outputable ( Outputable (..) , IsLine (..) , SDoc - , text , (<+>) , empty ) diff --git a/src/Pantomime/Subst.hs b/src/Pantomime/Subst.hs index 46ff9a1..1458812 100644 --- a/src/Pantomime/Subst.hs +++ b/src/Pantomime/Subst.hs @@ -30,7 +30,6 @@ import GHC.Plugins , extendVarEnv , lookupVarEnv ) -import GHC.Utils.Outputable (SDoc, text) import Control.Monad (foldM) diff --git a/src/Pantomime/Symbolise.hs b/src/Pantomime/Symbolise.hs index 7341d96..de0b4d7 100644 --- a/src/Pantomime/Symbolise.hs +++ b/src/Pantomime/Symbolise.hs @@ -7,7 +7,7 @@ module Pantomime.Symbolise ) where import GHC.Plugins qualified as GHC -import GHC.Utils.Outputable (SDoc, text, ($+$), (<+>), showSDocUnsafe) +import GHC.Utils.Outputable (text, ($+$), (<+>), showSDocUnsafe) import GHC.Builtin.Types.Prim ( intPrimTyCon , int8PrimTyCon diff --git a/src/Pantomime/Unification.hs b/src/Pantomime/Unification.hs index d8f8184..b405d9d 100644 --- a/src/Pantomime/Unification.hs +++ b/src/Pantomime/Unification.hs @@ -399,7 +399,7 @@ subsumeExpr dicts expr ty = do let (reqTv, reqEv, reqTy) = tcSplitSigmaTy ty -- Match the types and add all dictionaries we care about. - let err = "subsumeExpr: type matching failed" -- TODO: This should be a better error. + let err = "subsumeExpr: type matching failed" :: String -- TODO: This should be a better error. subst <- failWith err $ tcMatchTy curTy reqTy -- Make evidence variables. @@ -412,7 +412,7 @@ subsumeExpr dicts expr ty = do insertTM (varType ev) (Var ev) acc let curEv' = substTy subst <$> curEv argsEv <- for curEv' \ev -> do - failWith "subsumeExpr: type variable instance not found in dictionary" $ lookupTM ev dicts' + failWith @String "subsumeExpr: type variable instance not found in dictionary" $ lookupTM ev dicts' -- Construct the new expression. let open = mkApps expr $ fmap Type argsTv <> argsEv From c8022497edaf4f14408f171dfcdbc1177367102b Mon Sep 17 00:00:00 2001 From: Wind Date: Mon, 1 Jun 2026 22:03:06 +0200 Subject: [PATCH 7/8] Give up on reconstructing counterexample expression --- package.yaml | 1 + pantomime.cabal | 1 + src/Pantomime.hs | 1 - src/Pantomime/Marker.hs | 39 +++----------------------------- src/Pantomime/Passes.hs | 39 +++++++++----------------------- src/Pantomime/Solve.hs | 50 +++++++++-------------------------------- src/Pantomime/TH.hs | 3 +-- test/Spec.hs | 15 +++++++++++-- 8 files changed, 41 insertions(+), 108 deletions(-) diff --git a/package.yaml b/package.yaml index 477b5b7..3543e12 100644 --- a/package.yaml +++ b/package.yaml @@ -93,6 +93,7 @@ tests: dependencies: - pantomime - hspec + - hspec-expectations - HUnit - ghc-paths - directory diff --git a/pantomime.cabal b/pantomime.cabal index bb4ad2d..912a8c2 100644 --- a/pantomime.cabal +++ b/pantomime.cabal @@ -156,6 +156,7 @@ test-suite pantomime-test , ghc-paths , grisette >=0.13.0.0 , hspec + , hspec-expectations , mtl , pantomime , silently diff --git a/src/Pantomime.hs b/src/Pantomime.hs index b2b1c1b..e2f1172 100644 --- a/src/Pantomime.hs +++ b/src/Pantomime.hs @@ -9,7 +9,6 @@ module Pantomime , pantomimeMarker , pantomimeNothing , pantomimeJust - , PantomimeType (..) ) where import GHC.Plugins hiding (empty, (<>)) diff --git a/src/Pantomime/Marker.hs b/src/Pantomime/Marker.hs index 5098ce6..4bc8486 100644 --- a/src/Pantomime/Marker.hs +++ b/src/Pantomime/Marker.hs @@ -1,51 +1,18 @@ -{-# LANGUAGE FunctionalDependencies #-} - module Pantomime.Marker ( pantomimeMarker , pantomimeNothing , pantomimeJust - , PantomimeType (..) ) where -import Pantomime.BuiltIn qualified as Pantomime - -pantomimeMarker :: String -> Maybe res +pantomimeMarker :: String -> Maybe String pantomimeMarker name = error $ "The marker function 'pantomimeMarker' for '" ++ name ++ "' was not replaced by the GHC compiler plugin pass." {-# NOINLINE pantomimeMarker #-} -pantomimeNothing :: Maybe res +pantomimeNothing :: Maybe String pantomimeNothing = Nothing {-# NOINLINE pantomimeNothing #-} -pantomimeJust :: res -> Maybe res +pantomimeJust :: String -> Maybe String pantomimeJust x = Just x {-# NOINLINE pantomimeJust #-} - -class PantomimeType assertion res | assertion -> res where - pantomimeMarker' :: assertion -> String -> Maybe res - pantomimeMarker' _ name = pantomimeMarker name - {-# NOINLINE pantomimeMarker' #-} - -instance PantomimeType Pantomime.Bool () -instance PantomimeType (a -> Pantomime.Bool) a -instance PantomimeType (a -> b -> Pantomime.Bool) (a, b) -instance PantomimeType (a -> b -> c -> Pantomime.Bool) (a, b, c) -instance PantomimeType (a -> b -> c -> d -> Pantomime.Bool) (a, b, c, d) -instance PantomimeType (a -> b -> c -> d -> e -> Pantomime.Bool) (a, b, c, d, e) -instance PantomimeType (a -> b -> c -> d -> e -> f -> Pantomime.Bool) (a, b, c, d, e, f) -instance PantomimeType (a -> b -> c -> d -> e -> f -> g -> Pantomime.Bool) (a, b, c, d, e, f, g) -instance PantomimeType (a -> b -> c -> d -> e -> f -> g -> h -> Pantomime.Bool) (a, b, c, d, e, f, g, h) -instance PantomimeType (a -> b -> c -> d -> e -> f -> g -> h -> i -> Pantomime.Bool) (a, b, c, d, e, f, g, h, i) -instance PantomimeType (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> Pantomime.Bool) (a, b, c, d, e, f, g, h, i, j) -instance PantomimeType (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> Pantomime.Bool) (a, b, c, d, e, f, g, h, i, j, k) -instance PantomimeType (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> Pantomime.Bool) (a, b, c, d, e, f, g, h, i, j, k, l) -instance PantomimeType (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> Pantomime.Bool) (a, b, c, d, e, f, g, h, i, j, k, l, m) -instance PantomimeType (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> Pantomime.Bool) (a, b, c, d, e, f, g, h, i, j, k, l, m, n) -instance PantomimeType (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> Pantomime.Bool) (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o) -instance PantomimeType (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> Pantomime.Bool) (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -instance PantomimeType (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> q -> Pantomime.Bool) (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q) -instance PantomimeType (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> q -> r -> Pantomime.Bool) (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -instance PantomimeType (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> q -> r -> s -> Pantomime.Bool) (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s) -instance PantomimeType (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> q -> r -> s -> t -> Pantomime.Bool) (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t) - diff --git a/src/Pantomime/Passes.hs b/src/Pantomime/Passes.hs index d70dad7..58d47b7 100644 --- a/src/Pantomime/Passes.hs +++ b/src/Pantomime/Passes.hs @@ -4,10 +4,11 @@ module Pantomime.Passes ) where import GHC.Plugins hiding (empty, (<>), thNameToGhcName, getFirstAnnotations) -import GHC.Core.TyCo.Rep (scaledThing) import GHC.Core.Lint import GHC.Driver.Config.Core.Lint (initLintConfig) +import GHC.Core.Make (mkStringExpr) + import Grisette ( GrisetteSMTConfig (..) , SMTConfig (..) @@ -25,8 +26,8 @@ import Control.Error import Language.Haskell.TH qualified as TH -import Pantomime.Unification import Pantomime.Solve +import Pantomime.Unification import Pantomime.Axiom (resolvePluginAxioms) import Pantomime.Annotation @@ -219,10 +220,7 @@ checkValidityAndEmbed checkValidityAndEmbed guts = do (_, anns) <- getFirstAnnotations @Theory deserializeWithData guts - dflags <- getDynFlags - let platform = targetPlatform dflags - - markerPrimeId <- thNameToGhcName 'pantomimeMarker' >>= lookupIdAll + markerPrimeId <- thNameToGhcName 'pantomimeMarker >>= lookupIdAll nothingId <- thNameToGhcName 'pantomimeNothing >>= lookupIdAll justId <- thNameToGhcName 'pantomimeJust >>= lookupIdAll @@ -231,28 +229,13 @@ checkValidityAndEmbed guts = do axioms' <- resolvePluginAxioms axioms mCounterexample <- checkValid axioms' e let varNameStr = getOccString x - let ty = varType x - (_, funTy) = splitForAllTyVars ty - (argTys, _resTy) = splitFunTys funTy - argTys' = map scaledThing argTys - tupleTy = case argTys' of - [] -> mkBoxedTupleTy [] - [t] -> t - ts -> mkBoxedTupleTy ts case mCounterexample of Nothing -> do - let replacementExpr = App (Var nothingId) (Type tupleTy) - pure (NonRec x e, Just (varNameStr, (tupleTy, replacementExpr))) + pure (NonRec x e, Just (varNameStr, Var nothingId)) Just counterexample -> do - let valBindings = filter (isId . fst) (counterexampleBindings counterexample) - valExprs <- for valBindings \(_, arg) -> do - liftCore $ argToCoreExpr platform arg - let tupleExpr = case valExprs of - [] -> mkCoreTup [] - [expr'] -> expr' - exprs -> mkCoreTup exprs - let replacementExpr = App (App (Var justId) (Type tupleTy)) tupleExpr - pure (NonRec x e, Just (varNameStr, (tupleTy, replacementExpr))) + let ceStr = showSDocUnsafe (ppr counterexample) + ceExpr <- liftCore $ mkStringExpr ceStr + pure (NonRec x e, Just (varNameStr, App (Var justId) ceExpr)) b -> pure (b, Nothing) let results' = catMaybes results @@ -271,7 +254,7 @@ checkValidityAndEmbed guts = do -- the 'pantomimeMarker' call with the pre-generated proof result expressions. replaceMarkerInBinds :: Id - -> [(String, (Type, CoreExpr))] + -> [(String, CoreExpr)] -> [CoreBind] -> [CoreBind] replaceMarkerInBinds markerPrimeId results = map goBind @@ -283,7 +266,7 @@ replaceMarkerInBinds markerPrimeId results = map goBind -- compile-time Z3 proof result expression. replaceMarker :: Id - -> [(String, (Type, CoreExpr))] + -> [(String, CoreExpr)] -> CoreExpr -> CoreExpr replaceMarker markerPrimeId results expr = go expr @@ -294,7 +277,7 @@ replaceMarker markerPrimeId results expr = go expr case exprToString a of Just assertionName -> case lookup assertionName results of - Just (_, replacementExpr) -> replacementExpr + Just replacementExpr -> replacementExpr Nothing -> App (go f) (go a) Nothing -> App (go f) (go a) | otherwise = App (go f) (go a) diff --git a/src/Pantomime/Solve.hs b/src/Pantomime/Solve.hs index ea2f92b..a6c79f9 100644 --- a/src/Pantomime/Solve.hs +++ b/src/Pantomime/Solve.hs @@ -19,11 +19,11 @@ module Pantomime.Solve ( checkValid , Counterexample (..) , counterexampleToPairs - , argToCoreExpr ) where import GHC.Core qualified as GHC import GHC.Core.FamInstEnv (FamInstEnvs) +import GHC.Types.Id.Make (nospecId) import GHC.Generics (Generic) import GHC.Plugins ( CoreProgram @@ -38,23 +38,17 @@ import GHC.Plugins , getOccString , showSDocUnsafe , isId - , dataConWorkId - , tyConDataCons - , trueDataCon - , falseDataCon ) -import GHC.Core.Make (mkIntegerExpr) -import GHC.Platform (Platform) -import GHC.Types.Id.Make (nospecId) import GHC.Utils.Outputable ( Outputable (..) , IsLine (..) , SDoc + , text , (<+>) , empty ) -import Grisette (LogicalOp (..), EvalSym (..), Union, SymBool, onUnion, toCon, ToCon (..), pattern Single) +import Grisette (LogicalOp (..), EvalSym (..), Union, SymBool, onUnion) import Control.DeepSeq (NFData (..)) @@ -71,13 +65,12 @@ import Pantomime.Expr , pprArg , runRuntime , throwE - , Constructor (..) ) import Pantomime.Literal (BuiltInTyCon (..)) import Pantomime.Symbolise import Pantomime.Subst import Pantomime.Fresh -import Pantomime.Util (dbg, BitVec) +import Pantomime.Util (dbg) import Pantomime.Axiom (PluginAxiomsR (..)) import Pantomime.PrimOps (PrimOp) import Pantomime.Defer (defer, withDeferrable) @@ -185,24 +178,20 @@ construct prim PluginAxiomsR { .. } program expr = inject @SymboliseEff $ withDe pure (eq, Lie $ pure args) data Counterexample = Counterexample - { counterexampleBindings :: [(Var, Arg)] + { counterexampleBindings :: [(String, String)] } -- | Formats a counterexample into a list of name-value string pairs. counterexampleToPairs :: Counterexample -> [(String, String)] -counterexampleToPairs (Counterexample bindings) = map formatBinding bindings - where - formatBinding (bndr, arg) = - (getOccString bndr, showSDocUnsafe (pprArg id arg)) +counterexampleToPairs = counterexampleBindings instance Outputable Counterexample where ppr (Counterexample bindings) = pprBindings bindings where pprBindings [] = empty - pprBindings ((bndr, arg) : rest) = vcat + pprBindings ((name, val) : rest) = vcat [ "===================" - , ppr bndr <+> "::" <+> ppr (varType bndr) - , pprArg id arg + , text name <+> "=" <+> text val , pprBindings rest ] @@ -262,7 +251,9 @@ checkValid axioms expr = runBuiltInTypes do args' <- inject args let bindings = flip map args' \(bndr, arg) -> let arg' = evalSym True model arg - in (bndr, arg') + name = getOccString bndr + value = showSDocUnsafe (pprArg id arg') + in (name, value) pure $ Just (Counterexample bindings) Unsatisfiable -> do dbg @SDoc "Expression was valid!" @@ -281,22 +272,3 @@ collectValBinders expr = go expr go (GHC.Cast e _) = go e go (GHC.Let _ e) = go e go _ = [] - -argToCoreExpr :: MonadThings m => Platform -> Arg -> m CoreExpr -argToCoreExpr platform arg = - case runRuntime arg of - Single (Right (Lit (Bool sb))) - | Just b <- toCon sb -> - pure $ if b then GHC.Var (dataConWorkId trueDataCon) else GHC.Var (dataConWorkId falseDataCon) - Single (Right (Lit (Integer si))) - | Just i <- toCon si -> - pure $ mkIntegerExpr platform i - Single (Right (Con (DataCon dc))) -> - pure $ GHC.Var (dataConWorkId dc) - Single (Right (Con (EnumCon @n tag tc))) - | Just t <- toCon @_ @(BitVec n) tag -> do - let dcs = tyConDataCons tc - dc = dcs !! fromIntegral t - pure $ GHC.Var (dataConWorkId dc) - _ -> - error "Unsupported counterexample argument type" diff --git a/src/Pantomime/TH.hs b/src/Pantomime/TH.hs index 2a31e21..b50cb71 100644 --- a/src/Pantomime/TH.hs +++ b/src/Pantomime/TH.hs @@ -10,5 +10,4 @@ import Pantomime.Marker pantomime :: TH.Name -> TH.Q TH.Exp pantomime name = do let nameStr = TH.nameBase name - pure $ TH.AppE (TH.AppE (TH.VarE 'pantomimeMarker') (TH.VarE name)) (TH.LitE (TH.StringL nameStr)) - + pure $ TH.AppE (TH.VarE 'pantomimeMarker) (TH.LitE (TH.StringL nameStr)) diff --git a/test/Spec.hs b/test/Spec.hs index 86ba6e6..fca6e6a 100644 --- a/test/Spec.hs +++ b/test/Spec.hs @@ -6,6 +6,7 @@ module Main ) where import Test.Hspec +import Test.Hspec.Expectations (expectationFailure) import Pantomime import Pantomime.BuiltIn qualified as Pantomime @@ -43,5 +44,15 @@ main = hspec $ do it "verifies validAssertion (should succeed with Nothing)" $ do $(pantomime 'validAssertion) `shouldBe` Nothing - it "detects invalidAssertion (should fail with Just Counterexample)" $ do - $(pantomime 'invalidAssertion) `shouldBe` Just (False, True) + it "detects invalidAssertion (should fail with Just counterexample)" $ do + checkInvalid $(pantomime 'invalidAssertion) + +-- | Assert that a counterexample was found and print it. +checkInvalid :: Maybe String -> Expectation +checkInvalid = \case + Just ce -> do + putStrLn "" + putStrLn "Counterexample found:" + putStrLn ce + putStrLn "" + Nothing -> expectationFailure "Expected a counterexample but assertion was valid" From bb61e491b510d81b0a0e99c50232aa0afb23e21e Mon Sep 17 00:00:00 2001 From: Wind Date: Sat, 6 Jun 2026 22:05:25 +0200 Subject: [PATCH 8/8] more detailed error --- src/Pantomime/Unification.hs | 340 ++++++++++++++++++----------------- 1 file changed, 175 insertions(+), 165 deletions(-) diff --git a/src/Pantomime/Unification.hs b/src/Pantomime/Unification.hs index b405d9d..1462c3b 100644 --- a/src/Pantomime/Unification.hs +++ b/src/Pantomime/Unification.hs @@ -1,48 +1,44 @@ {-# LANGUAGE OverloadedStrings #-} + -- TODO: Rename to Pantomime.Unify, I think it's cleaner and it also mirrors the -- naming from GHC. -- TODO: Add module docs. module Pantomime.Unification - ( UnificationError (..) - , OversaturatedError (..) - , unifyApp - , unifyApps - , unifyExprs - , resolveInstances - , resolveInstancesWith - , subsumeExpr - ) where - -import Prelude hiding (break) + ( UnificationError (..), + OversaturatedError (..), + unifyApp, + unifyApps, + unifyExprs, + resolveInstances, + resolveInstancesWith, + subsumeExpr, + ) +where -import GHC.Plugins hiding ((<>)) +import Control.Applicative (Alternative ((<|>))) +import Control.Error (LookupError (..)) +import Control.Monad (when) +import Data.List (intersperse) +import Data.Traversable (for) +import Effectful +import Effectful.Break +import Effectful.Context +import Effectful.Error.Static +import Effectful.GHC.External (HasInstEnvs, lookupUniqueInst) import GHC.Core.Class (Class) -import GHC.Core.Unify (tcUnifyTys, alwaysBindFun, tcMatchTy) +import GHC.Core.InstEnv (instanceDFunId) import GHC.Core.Map.Type (TypeMap) import GHC.Core.Predicate (isEvVar) -import GHC.Core.InstEnv (instanceDFunId) -import GHC.Core.TyCo.Rep (Type (..), Scaled (..), scaledThing) -import GHC.Data.TrieMap (TrieMap (..), insertTM) +import GHC.Core.TyCo.Rep (Scaled (..), Type (..), scaledThing) +import GHC.Core.Unify (alwaysBindFun, tcMatchTy, tcUnifyTys) import GHC.Data.Maybe (rightToMaybe, whenIsJust) -import GHC.Tc.Utils.TcType (tcSplitSigmaTy, substTy) - -import Data.List (intersperse) -import Data.Traversable (for) - -import Control.Applicative (Alternative ((<|>))) -import Control.Monad (when) -import Control.Error (LookupError (..)) - +import GHC.Data.TrieMap (TrieMap (..), insertTM) +import GHC.Plugins hiding ((<>)) +import GHC.Tc.Utils.TcType (substTy, tcSplitSigmaTy) import Lens.Micro import Lens.Micro.Extras (view) - import Pantomime.Util - -import Effectful -import Effectful.Error.Static -import Effectful.Break -import Effectful.Context -import Effectful.GHC.External (HasInstEnvs, lookupUniqueInst) +import Prelude hiding (break) -- | Error to indicate unification failure. -- @@ -67,65 +63,70 @@ instance Outputable OversaturatedError where let vsep' = vcat' . intersperse "" -- Pretty print an expression with its type. - let pprExpr expr = vcat' - [ "::" <+> ppr (exprType expr) - , ppr expr - ] + let pprExpr expr = + vcat' + [ "::" <+> ppr (exprType expr), + ppr expr + ] -- The actual pretty print. vsep' [ hang "Function is oversaturated" 2 do - pprExpr fun - , hang "Given arguments" 2 do - vsep' $ fmap pprExpr args + pprExpr fun, + hang "Given arguments" 2 do + vsep' $ fmap pprExpr args ] -- | Mapping used to track information for unification. data Unification = Unification - { _substitution :: Subst - -- ^ The substitution as dictated by a GHC unification. - , _dictionaries :: TypeMap CoreExpr - -- ^ The dictionary expressions/variables currently in-scope. - , _quantifiers :: DTyCoVarSet - -- ^ The quantifiers currently in use. + { -- | The substitution as dictated by a GHC unification. + _substitution :: Subst, + -- | The dictionary expressions/variables currently in-scope. + _dictionaries :: TypeMap CoreExpr, + -- | The quantifiers currently in use. + _quantifiers :: DTyCoVarSet } -- | An empty unification mapping. emptyUnif :: Unification -emptyUnif = Unification - { _substitution = emptySubst - , _dictionaries = emptyTM - , _quantifiers = emptyDVarSet - } +emptyUnif = + Unification + { _substitution = emptySubst, + _dictionaries = emptyTM, + _quantifiers = emptyDVarSet + } -- | Lens into substitution of the 'Unification'. substitution :: Lens' Unification Subst substitution f unif = do - let rebuild subst = Unification - { _substitution = subst - , _dictionaries = _dictionaries unif - , _quantifiers = _quantifiers unif - } + let rebuild subst = + Unification + { _substitution = subst, + _dictionaries = _dictionaries unif, + _quantifiers = _quantifiers unif + } rebuild <$> f (_substitution unif) -- | Lens into dictionaries of the 'Unification'. dictionaries :: Lens' Unification (TypeMap CoreExpr) dictionaries f unif = do - let rebuild dict = Unification - { _substitution = _substitution unif - , _dictionaries = dict - , _quantifiers = _quantifiers unif - } + let rebuild dict = + Unification + { _substitution = _substitution unif, + _dictionaries = dict, + _quantifiers = _quantifiers unif + } rebuild <$> f (_dictionaries unif) -- | Lens into quantifiers of the 'Unification'. quantifiers :: Lens' Unification DVarSet quantifiers f unif = do - let rebuild quants = Unification - { _substitution = _substitution unif - , _dictionaries = _dictionaries unif - , _quantifiers = quants - } + let rebuild quants = + Unification + { _substitution = _substitution unif, + _dictionaries = _dictionaries unif, + _quantifiers = quants + } rebuild <$> f (_quantifiers unif) -- | A lens into the 'InScopeSet' of a 'Subst'. @@ -138,11 +139,11 @@ scopeSubst f (Subst scope' ids tvs cvs) = do -- -- This will not resolve instances. The purpose of this lookup is to not have -- duplicate dictionary constraints in a unified expression. -lookupDict - :: Context Reader Unification :> es - => Context Writer Unification :> es - => Type - -> Eff es CoreExpr +lookupDict :: + (Context Reader Unification :> es) => + (Context Writer Unification :> es) => + Type -> + Eff es CoreExpr lookupDict ty = runBreak do -- We need to use the new type for lookup in order to properly deduplicate -- constraints. @@ -165,23 +166,23 @@ lookupDict ty = runBreak do pure fresh' -- | Multiple lookups using 'lookupDict'. -lookupDicts - :: Context Reader Unification :> es - => Context Writer Unification :> es - => Traversable f - => f Type - -> Eff es (f CoreExpr) +lookupDicts :: + (Context Reader Unification :> es) => + (Context Writer Unification :> es) => + (Traversable f) => + f Type -> + Eff es (f CoreExpr) lookupDicts = traverse lookupDict -- | Lookup the unifying type of a type variable. -- -- This will additionally track the type variables that are used by the new, -- unified type in the unification map. -lookupTy - :: Context Reader Unification :> es - => Context Writer Unification :> es - => TyVar - -> Eff es Type +lookupTy :: + (Context Reader Unification :> es) => + (Context Writer Unification :> es) => + TyVar -> + Eff es Type lookupTy var = do -- Lookup the unifying type. unif <- get @Unification @@ -201,21 +202,21 @@ lookupTy var = do pure ty -- | Multiple lookups using 'lookupTy'. -lookupTys - :: Context Reader Unification :> es - => Context Writer Unification :> es - => Traversable f - => f TyVar - -> Eff es (f Type) +lookupTys :: + (Context Reader Unification :> es) => + (Context Writer Unification :> es) => + (Traversable f) => + f TyVar -> + Eff es (f Type) lookupTys = traverse lookupTy -- | Fetches all free type variables. -- -- The intent for this is to close expressions which we unified using -- 'applyUnification'. -freeTyVars - :: Context Reader Unification :> es - => Eff es [TyVar] +freeTyVars :: + (Context Reader Unification :> es) => + Eff es [TyVar] freeTyVars = do unif <- get @Unification pure $ unif ^. quantifiers . to dVarSetElems @@ -224,9 +225,9 @@ freeTyVars = do -- -- The intent for this is to close expressions which we unified using -- 'applyUnification'. -freeDictIds - :: Context Reader Unification :> es - => Eff es [DictId] +freeDictIds :: + (Context Reader Unification :> es) => + Eff es [DictId] freeDictIds = do unif <- get @Unification let select = \case @@ -238,10 +239,10 @@ freeDictIds = do -- -- It is assumed that this expression has been first unified using the -- 'applyUnification'. -closeExpr - :: Context Reader Unification :> es - => CoreExpr - -> Eff es CoreExpr +closeExpr :: + (Context Reader Unification :> es) => + CoreExpr -> + Eff es CoreExpr closeExpr expr = do tyVars <- freeTyVars dictIds <- freeDictIds @@ -252,21 +253,21 @@ splitExprTy :: CoreExpr -> ([TyVar], ThetaType, Type) splitExprTy = tcSplitSigmaTy . exprType -- | Unify two types using 'unifyTypes'. -unifyType - :: Error UnificationError :> es - => Type - -> Type - -> Eff es Unification +unifyType :: + (Error UnificationError :> es) => + Type -> + Type -> + Eff es Unification unifyType lhs rhs = unifyTypes [(lhs, rhs)] -- | Unify the given types. -- -- Creates a unification map for use in 'applyUnification'. -unifyTypes - :: HasCallStack - => Error UnificationError :> es - => [(Type, Type)] - -> Eff es Unification +unifyTypes :: + (HasCallStack) => + (Error UnificationError :> es) => + [(Type, Type)] -> + Eff es Unification unifyTypes tys = do let err = UnificationError tys let (lhs, rhs) = unzip tys @@ -282,11 +283,11 @@ unifyTypes tys = do -- The returned expression will have free variables as dictated by the -- unification mapping. However way the expression is used, make sure to -- eventually close the expression using 'closeExpr'. -applyUnification - :: Context Reader Unification :> es - => Context Writer Unification :> es - => CoreExpr - -> Eff es CoreExpr +applyUnification :: + (Context Reader Unification :> es) => + (Context Writer Unification :> es) => + CoreExpr -> + Eff es CoreExpr applyUnification expr = do -- Split the type variables and theta type. let (tyVars, thetaTy, _) = splitExprTy expr @@ -300,22 +301,22 @@ applyUnification expr = do pure $ mkApps expr args -- | Multiple applications of the unification via 'applyUnification'. -applyUnifications - :: Context Reader Unification :> es - => Context Writer Unification :> es - => Traversable f - => f CoreExpr - -> Eff es (f CoreExpr) +applyUnifications :: + (Context Reader Unification :> es) => + (Context Writer Unification :> es) => + (Traversable f) => + f CoreExpr -> + Eff es (f CoreExpr) applyUnifications = traverse applyUnification -- | A single unifying application using 'unifyApps'. -unifyApp - :: HasCallStack - => Error UnificationError :> es - => Error OversaturatedError :> es - => CoreExpr - -> CoreArg - -> Eff es CoreExpr +unifyApp :: + (HasCallStack) => + (Error UnificationError :> es) => + (Error OversaturatedError :> es) => + CoreExpr -> + CoreArg -> + Eff es CoreExpr unifyApp fun arg = unifyApps fun [arg] -- | Application that unifies polymorphic types. @@ -323,13 +324,13 @@ unifyApp fun arg = unifyApps fun [arg] -- This will apply the given arguments to the spine. Any type or dictionary -- variables that occur prior any of the body type are unified and placed as -- outer type and dictionary variables. -unifyApps - :: HasCallStack - => Error UnificationError :> es - => Error OversaturatedError :> es - => CoreExpr - -> [CoreArg] - -> Eff es CoreExpr +unifyApps :: + (HasCallStack) => + (Error UnificationError :> es) => + (Error OversaturatedError :> es) => + CoreExpr -> + [CoreArg] -> + Eff es CoreExpr unifyApps fun args = do -- Get the base types without type variables or theta type of all expressions. let bodyTy = view _3 . splitExprTy @@ -356,11 +357,11 @@ unifyApps fun args = do -- -- This can be used to compare two expressions that are quantified different, -- but are otherwise comparable. -unifyExprs - :: Error UnificationError :> es - => CoreExpr - -> CoreExpr - -> Eff es (CoreExpr, CoreExpr) +unifyExprs :: + (Error UnificationError :> es) => + CoreExpr -> + CoreExpr -> + Eff es (CoreExpr, CoreExpr) unifyExprs lhs rhs = do -- Get the unifiable part of the type. let bodyTy = view _3 . splitExprTy @@ -386,24 +387,29 @@ unifyExprs lhs rhs = do -- TODO: Using 'TypeMap CoreExpr' for instances is extremely fragile. It would -- be a lot better to use InstEnv to resolve typeclasses. This goes for other -- functions in this module as well! -subsumeExpr - :: HasCallStack - => Error String :> es - => TypeMap CoreExpr - -> CoreExpr - -> Type - -> Eff es CoreExpr +subsumeExpr :: + (HasCallStack) => + (Error String :> es) => + TypeMap CoreExpr -> + CoreExpr -> + Type -> + Eff es CoreExpr subsumeExpr dicts expr ty = do -- Get the unifiable part of the type. let (curTv, curEv, curTy) = splitExprTy expr let (reqTv, reqEv, reqTy) = tcSplitSigmaTy ty -- Match the types and add all dictionaries we care about. - let err = "subsumeExpr: type matching failed" :: String -- TODO: This should be a better error. + let err = + "subsumeExpr: type matching failed" + <> "\n current type: " + <> showSDocUnsafe (ppr curTy) + <> "\n required type: " + <> showSDocUnsafe (ppr reqTy) subst <- failWith err $ tcMatchTy curTy reqTy -- Make evidence variables. - let names = ("dict", ) . unrestricted <$> reqEv + let names = ("dict",) . unrestricted <$> reqEv let (lamEv, _) = freshIds names $ mkInScopeSetList reqTv -- Construct the arguments to supply to the expression to unify. @@ -412,7 +418,11 @@ subsumeExpr dicts expr ty = do insertTM (varType ev) (Var ev) acc let curEv' = substTy subst <$> curEv argsEv <- for curEv' \ev -> do - failWith @String "subsumeExpr: type variable instance not found in dictionary" $ lookupTM ev dicts' + let err' = + "subsumeExpr: type variable instance not found in dictionary" + <> "\n type: " + <> showSDocUnsafe (ppr ev) + failWith @String err' $ lookupTM ev dicts' -- Construct the new expression. let open = mkApps expr $ fmap Type argsTv <> argsEv @@ -421,13 +431,13 @@ subsumeExpr dicts expr ty = do -- | Lookup a class instance in the instantiation environment. -- -- This will return a dictionary instance as core expression. -lookupClassInst - :: forall es - . HasCallStack - => Error (LookupError Type) :> es - => HasInstEnvs :> es - => Type - -> Eff es CoreExpr +lookupClassInst :: + forall es. + (HasCallStack) => + (Error (LookupError Type) :> es) => + (HasInstEnvs :> es) => + Type -> + Eff es CoreExpr lookupClassInst ty = do let failWith' :: Maybe a -> Eff es a failWith' = failWith $ LookupError ty @@ -452,10 +462,10 @@ lookupClassInst ty = do -- typeclass. Instead, this function is intended to be used together with other -- unification-like functions in this module, as these unifications can create -- resolvable typeclass constraints. -resolveInstances - :: HasInstEnvs :> es - => CoreExpr - -> Eff es CoreExpr +resolveInstances :: + (HasInstEnvs :> es) => + CoreExpr -> + Eff es CoreExpr resolveInstances expr = do -- Get a mapping from constraints to instances. let theta = splitExprTy expr ^. _2 @@ -465,17 +475,17 @@ resolveInstances expr = do -- Convert this mapping into a trie map. let dicts = foldlBy emptyTM instances \acc (ty, inst) -> do - -- Alter the dictionary map if we found an instance. - alterTM ty (inst <|>) acc + -- Alter the dictionary map if we found an instance. + alterTM ty (inst <|>) acc -- Resolve the instances with this mapping. pure $ resolveInstancesWith dicts expr -resolveInstancesWith - :: TypeMap CoreExpr - -- ^ Mapping from dictionary types to their instance. - -> CoreExpr - -> CoreExpr +resolveInstancesWith :: + -- | Mapping from dictionary types to their instance. + TypeMap CoreExpr -> + CoreExpr -> + CoreExpr resolveInstancesWith dicts expr = do -- Set this dictionary for a unification. let unif = emptyUnif & dictionaries .~ dicts