inspection-testing 0.4.6.1 → 0.5

raw patch · 6 files changed

+370/−86 lines, 6 filesdep ~basePVP ok

version bump matches the API change (PVP)

Dependency ranges changed: base

API changes (from Hackage documentation)

Files

• ChangeLog.md +5/−0
• examples/LetsTest.hs +56/−0
• inspection-testing.cabal +11/−1
• src/Test/Inspection.hs +29/−10
• src/Test/Inspection/Core.hs +263/−72
• src/Test/Inspection/Plugin.hs +6/−3

@@ -1,5 +1,10 @@ # Revision history for inspection-testing +## 0.5 -- 2022-06-15++* New equivalence `==~` that accepts different order of bindings in lets. (thanks @phadej)+* When printing terms that differ, common up a common prefix of lambdas (thanks @phadej)+ ## 0.4.6.1 -- 2022-05-20  * Support GHC 9.4 (thanks @parsonsmatt)

@@ -0,0 +1,56 @@+{-# LANGUAGE TemplateHaskell #-}+{-# OPTIONS_GHC -dsuppress-all #-}+module Main (main) where++import Test.Inspection+import Data.Char (toUpper)+import System.Exit++lhs1, rhs1 :: Char -> Char -> String++lhs1 x y = let x' = toUpper x+               y' = toUpper y+           in [x', x', y', y']++rhs1 x y = let y' = toUpper y+               x' = toUpper x+           in [x', x', y', y']++-- recursive+lhs2, rhs2, rhs2b :: String+lhs2 = let zs = 'z' : xs+           xs = 'x' : ys+           ys = 'y' : xs+       in zs++rhs2 = let ys = 'y' : xs+           xs = 'x' : ys+           zs = 'z' : xs+       in zs++rhs2b = let ys = 'y' : xs+            xs = 'x' : ys+            zs = 'z' : ys+        in zs++printResult :: Result -> IO ()+printResult (Success s) = putStrLn s+printResult (Failure s) = putStrLn s++isSuccess :: Result -> Bool+isSuccess (Success _) = True+isSuccess (Failure _) = False++results :: [Result]+results =+    [ $(inspectTest $ 'lhs1 ==~ 'rhs1)+    , $(inspectTest $ 'lhs2 ==- 'rhs2) -- here GHC orders let bindings by itself!+    , $(inspectTest $ 'lhs2 =/~ 'rhs2b)+    ]++main :: IO ()+main = do+    mapM_ printResult results+    if map isSuccess results == [True, True, False]+    then exitSuccess+    else exitFailure

@@ -1,5 +1,5 @@ name:                inspection-testing-version:             0.4.6.1+version:             0.5 synopsis:            GHC plugin to do inspection testing description:         Some carefully crafted libraries make promises to their                      users beyond functionality and performance.@@ -91,6 +91,16 @@   type:                exitcode-stdio-1.0   hs-source-dirs:      examples   main-is:             SimpleTest.hs+  build-depends:       inspection-testing+  build-depends:       base+  default-language:    Haskell2010+  if impl(ghc < 8.4)+      ghc-options:       -fplugin=Test.Inspection.Plugin++test-suite lets-test+  type:                exitcode-stdio-1.0+  hs-source-dirs:      examples+  main-is:             LetsTest.hs   build-depends:       inspection-testing   build-depends:       base   default-language:    Haskell2010

@@ -23,10 +23,11 @@     inspectTest,     Result(..),     -- * Defining obligations-    Obligation(..), mkObligation, Property(..),+    Obligation(..), mkObligation, Equivalence (..), Property(..),     -- * Convenience functions     -- $convenience-    (===), (==-), (=/=), (=/-), hasNoType, hasNoGenerics,+    (===), (==-), (=/=), (=/-), (==~), (=/~),+    hasNoType, hasNoGenerics,     hasNoTypeClasses, hasNoTypeClassesExcept,     doesNotUse, coreOf, ) where@@ -112,9 +113,8 @@     -- In general @f@ and @g@ need to be defined in this module, so that their     -- actual defintions can be inspected.     ---    -- If the boolean flag is true, then ignore types and hpc ticks-    -- during the comparison.-    = EqualTo Name Bool+    -- The `Equivalence` indicates how strict to check for equality+    = EqualTo Name Equivalence      -- | Do none of these types appear anywhere in the definition of the function     -- (neither locally bound nor passed as arguments)@@ -133,6 +133,13 @@     | CoreOf     deriving Data +-- | Equivalence of terms.+data Equivalence+    = StrictEquiv               -- ^ strict term equality+    | IgnoreTypesAndTicksEquiv  -- ^ ignore types and hpc ticks during the comparison+    | UnorderedLetsEquiv        -- ^ allow permuted let bindings, ignore types and hpc tick during comparison+    deriving Data+ -- | Creates an inspection obligation for the given function name -- with default values for the optional fields. mkObligation :: Name -> Property -> Obligation@@ -152,29 +159,41 @@  -- | Declare two functions to be equal (see 'EqualTo') (===) :: Name -> Name -> Obligation-(===) = mkEquality False False+(===) = mkEquality False StrictEquiv infix 9 ===  -- | Declare two functions to be equal, but ignoring -- type lambdas, type arguments, type casts and hpc ticks (see 'EqualTo'). -- Note that @-fhpc@ can prevent some optimizations; build without for more reliable analysis. (==-) :: Name -> Name -> Obligation-(==-) = mkEquality False True+(==-) = mkEquality False IgnoreTypesAndTicksEquiv infix 9 ==- +-- | Declare two functions to be equal as @('==-')@ but also ignoring+-- let bindings ordering (see 'EqualTo').+(==~) :: Name -> Name -> Obligation+(==~) = mkEquality False UnorderedLetsEquiv+infix 9 ==~+ -- | Declare two functions to be equal, but expect the test to fail (see 'EqualTo' and 'expectFail') -- (This is useful for documentation purposes, or as a TODO list.) (=/=) :: Name -> Name -> Obligation-(=/=) = mkEquality True False+(=/=) = mkEquality True StrictEquiv infix 9 =/=  -- | Declare two functions to be equal up to types (see '(==-)'), -- but expect the test to fail (see 'expectFail'), (=/-) :: Name -> Name -> Obligation-(=/-) = mkEquality False False+(=/-) = mkEquality False IgnoreTypesAndTicksEquiv infix 9 =/- -mkEquality :: Bool -> Bool -> Name -> Name -> Obligation+-- | Declare two functions to be equal up to let binding ordering (see '(==~)'),+-- but expect the test to fail (see 'expectFail'),+(=/~) :: Name -> Name -> Obligation+(=/~) = mkEquality False UnorderedLetsEquiv+infix 9 =/~++mkEquality :: Bool -> Equivalence -> Name -> Name -> Obligation mkEquality expectFail ignore_types n1 n2 =     (mkObligation n1 (EqualTo n2 ignore_types))         { expectFail = expectFail }

@@ -1,6 +1,6 @@ -- | This module implements some analyses of Core expressions necessary for -- "Test.Inspection". Normally, users of this package can ignore this module.-{-# LANGUAGE CPP, FlexibleContexts, PatternSynonyms #-}+{-# LANGUAGE CPP, FlexibleContexts, PatternSynonyms, MultiWayIf #-} module Test.Inspection.Core   ( slice   , pprSlice@@ -20,9 +20,12 @@ import GHC.Types.Var as Var import GHC.Types.Id import GHC.Types.Name+import GHC.Types.Literal import GHC.Types.Var.Env+import GHC.Types.Unique import GHC.Utils.Outputable as Outputable import GHC.Core.Ppr+import GHC.Core.Subst import GHC.Core.Coercion import GHC.Utils.Misc import GHC.Core.DataCon@@ -30,10 +33,12 @@ #else import CoreSyn import CoreUtils+import CoreSubst import TyCoRep import Type import Var import Id+import Literal import Name import VarEnv import Outputable@@ -41,6 +46,7 @@ import Coercion import Util import DataCon+import Unique import TyCon (TyCon, isClassTyCon) #endif @@ -50,16 +56,25 @@  import qualified Data.Set as S import Control.Monad.State.Strict-import Control.Monad.Trans.Maybe-import Data.List (nub)+import Data.List (nub, intercalate) import Data.Maybe +import Test.Inspection (Equivalence (..))++-- Uncomment to enable debug traces+-- import Debug.Trace++tracePut :: Monad m => Int -> String -> String -> m ()+-- tracePut lv name msg = traceM $ replicate lv ' ' ++ name ++ ": " ++ msg+tracePut _  _    _ = return ()+ #if !MIN_VERSION_ghc(9,2,0) pattern Alt :: a -> b -> c -> (a, b, c) pattern Alt a b c = (a, b, c) {-# COMPLETE Alt #-} #endif + type Slice = [(Var, CoreExpr)]  -- | Selects those bindings that define the given variable (with this variable first)@@ -102,14 +117,53 @@  -- | Pretty-print two slices, after removing variables occurring in both pprSliceDifference :: Slice -> Slice -> SDoc-pprSliceDifference slice1 slice2 =-    hang (text "LHS" Outputable.<> colon) 4 (pprSlice slice1') $$-    hang (text "RHS" Outputable.<> colon) 4 (pprSlice slice2')+pprSliceDifference slice1 slice2+    | [(v1,e1)] <- slice1'+    , [(v2,e2)] <- slice2'+    = pprSingletonSliceDifference v1 v2 e1 e2++    | otherwise =+        hang (text "LHS" Outputable.<> colon) 4 (pprSlice slice1') $$+        hang (text "RHS" Outputable.<> colon) 4 (pprSlice slice2')   where     both = S.intersection (S.fromList (map fst slice1)) (S.fromList (map fst slice2))     slice1' = filter (\(v,_) -> v `S.notMember` both) slice1     slice2' = filter (\(v,_) -> v `S.notMember` both) slice2 +pprSingletonSliceDifference :: Var -> Var -> CoreExpr -> CoreExpr -> SDoc+pprSingletonSliceDifference v1 v2 e1 e2 =+    ctxDoc $+    hang (text "LHS" Outputable.<> colon) 4 (hang (pprPrefixOcc v1) 2 (eqSign <+> pprCoreExpr e1')) $$+    hang (text "RHS" Outputable.<> colon) 4 (hang (pprPrefixOcc v2) 2 (eqSign <+> pprCoreExpr e2'))+  where+    hasContext = not (null ctxt)++    ctxDoc | hasContext = id+           | otherwise = (hang (text "In") 4 (ppr $ mkContextExpr (reverse (map snd ctxt))) $$)++    eqSign | hasContext = text "= ..."+           | otherwise  = equals++    (e1', e2', ctxt) = go e1 e2 [] (mkRnEnv2 emptyInScopeSet)++    go :: CoreExpr -> CoreExpr -> [(Var, Var)] -> RnEnv2 -> (CoreExpr, CoreExpr, [(Var, Var)])+    go (Lam b1 t1) (Lam b2 t2) ctxt env+        | eqTypeX env (varType b1) (varType b2)+        = go t1 t2 ((b1,b2):ctxt) (rnBndr2 env b1 b2)+      where+    go x y ctxt _env = (rename ctxt x, y, ctxt)++    mkContextExpr :: [Var] -> CoreExpr+    mkContextExpr []       = ellipsis+    mkContextExpr (x:rest) = Lam x (mkContextExpr rest)++    ellipsis :: CoreExpr+#if MIN_VERSION_ghc(8,8,0)+    ellipsis = Lit $ mkLitString "..."+#else+    ellipsis = Lit $ mkMachString "..."+#endif+ withLessDetail :: SDoc -> SDoc #if MIN_VERSION_GLASGOW_HASKELL(8,2,0,0) && !MIN_VERSION_GLASGOW_HASKELL(9,0,0,0) withLessDetail sdoc = sdocWithDynFlags $ \dflags ->@@ -125,42 +179,80 @@ -- have auxiliary variables in the right order. -- (This is mostly to work-around the buggy CSE in GHC-8.0) -- It also breaks if there is shadowing.-eqSlice :: Bool {- ^ ignore types and hpc ticks -} -> Slice -> Slice -> Bool+eqSlice :: Equivalence -> Slice -> Slice -> Bool eqSlice _ slice1 slice2 | null slice1 || null slice2 = null slice1 == null slice2   -- Mostly defensive programming (slices should not be empty)-eqSlice it slice1 slice2-  = step (S.singleton (fst (head slice1), fst (head slice2))) S.empty+eqSlice eqv slice1 slice2+    -- slices are equal if there exist any result with no "unification" obligations left.+    = any (S.null . snd) results   where-    step :: VarPairSet -> VarPairSet -> Bool-    step wanted done-        | wanted `S.isSubsetOf` done-        = True -- done-        | (x,y) : _ <- S.toList (wanted `S.difference` done)-        , (Just _, wanted') <- runState (runMaybeT (equate x y)) wanted-        = step wanted' (S.insert (x,y) done)-        | otherwise-        = False+    -- ignore types and hpc ticks+    it :: Bool+    it = case eqv of+        StrictEquiv              -> False+        IgnoreTypesAndTicksEquiv -> True+        UnorderedLetsEquiv       -> True +    -- unordered lets+    ul :: Bool+    ul = case eqv of+        StrictEquiv              -> False+        IgnoreTypesAndTicksEquiv -> False+        UnorderedLetsEquiv       -> True -    equate :: Var -> Var -> MaybeT (State VarPairSet) ()-    equate x y-        | Just e1 <- lookup x slice1-        , Just x' <- essentiallyVar e1-        , x' `elem` map fst slice1-        = lift $ modify (S.insert (x',y))-        | Just e2 <- lookup y slice2-        , Just y' <- essentiallyVar e2-        , y' `elem` map fst slice2-        = lift $ modify (S.insert (x,y'))-        | Just e1 <- lookup x slice1-        , Just e2 <- lookup y slice2-        = go (mkRnEnv2 emptyInScopeSet) e1 e2-    equate _ _ = mzero+    -- results. If there are no pairs to be equated, all is fine.+    results :: [((), VarPairSet)]+    results = runStateT (loop' (mkRnEnv2 emptyInScopeSet) S.empty (fst (head slice1)) (fst (head slice2))) S.empty -    equated :: Var -> Var -> MaybeT (State VarPairSet) ()-    equated x y | x == y = return ()-    equated x y = lift $ modify (S.insert (x,y))+    -- while there are obligations left, try to equate them.+    loop :: RnEnv2 -> VarPairSet -> StateT VarPairSet [] ()+    loop env done = do+        vars <- get+        case S.minView vars of+            Nothing -> return () -- nothing to do, done.+            Just ((x, y), vars') -> do+                put vars'+                if (x, y) `S.member` done+                then loop env done+                else loop' env done x y +    loop' :: RnEnv2 -> VarPairSet -> Var -> Var -> StateT VarPairSet [] ()+    loop' env done x y = do+        tracePut 0 "TOP" (varToString x ++ " =?= " ++ varToString y)+        tracePut 0 "DONESET" (showVarPairSet done)++        -- if x or y expressions are essentially a variable x' or y' respectively+        -- add an obligation to check x' = y (or x = y').+        if | Just e1 <- lookup x slice1+           , Just x' <- essentiallyVar e1+           , x' `elem` map fst slice1+           -> do modify' (S.insert (x', y))+                 loop env done++           | Just e2 <- lookup y slice2+           , Just y' <- essentiallyVar e2+           , y' `elem` map fst slice2+           -> do modify' (S.insert (x, y'))+                 loop env done++            -- otherwise if neither x and y expressions are variables+            -- 1. compare the expressions (already assuming that x and y are equal)+            -- 2. comparison may create new obligations, loop.+           | Just e1 <- lookup x slice1+           , Just e2 <- lookup y slice2+           -> do+               let env' = rnBndr2 env x y+                   done' = S.insert (x, y) done++               go 0 env' e1 e2+               loop env' done'++            -- and finally, if x or y are not in the slice, we abort.+           | otherwise+           -> do+              tracePut 0 "TOP" (varToString x ++ " =?= " ++ varToString y ++ " NOT IN SLICES")+              mzero+     essentiallyVar :: CoreExpr -> Maybe Var     essentiallyVar (App e a)  | it, isTyCoArg a = essentiallyVar e     essentiallyVar (Lam v e)  | it, isTyCoVar v = essentiallyVar e@@ -172,64 +264,91 @@     essentiallyVar (Tick HpcTick{} e) | it      = essentiallyVar e     essentiallyVar _                            = Nothing -    go :: RnEnv2 -> CoreExpr -> CoreExpr -> MaybeT (State (S.Set (Var,Var))) ()-    go env (Var v1) (Var v2) | rnOccL env v1 == rnOccR env v2 = pure ()-                             | otherwise = equated v1 v2-    go _   (Lit lit1)    (Lit lit2)        = guard $ lit1 == lit2-    go env (Type t1)     (Type t2)         = guard $ eqTypeX env t1 t2-    go env (Coercion co1) (Coercion co2)   = guard $ eqCoercionX env co1 co2+    go :: Int -> RnEnv2 -> CoreExpr -> CoreExpr -> StateT VarPairSet [] ()+    go lv env (Var v1) (Var v2) = do+        if | v1 == v2 -> do+            tracePut lv "VAR" (varToString v1 ++ " =?= " ++ varToString v2 ++ " SAME")+            return ()+           | rnOccL env v1 == rnOccR env v2 -> do+            tracePut lv "VAR" (varToString v1 ++ " =?= " ++ varToString v2 ++ " IN ENV")+            return ()+           | otherwise -> do+            tracePut lv "VAR" (varToString v1 ++ " =?= " ++ varToString v2 ++ " OBLIGATION")+            modify (S.insert (v1, v2)) -    go env (Cast e1 _) e2 | it             = go env e1 e2-    go env e1 (Cast e2 _) | it             = go env e1 e2+    go lv _   (Lit lit1)    (Lit lit2)        = do+        tracePut lv "LIT" "???" -- no Show for Literal :(+        guard $ lit1 == lit2++    go _  env (Type t1)     (Type t2)         = guard $ eqTypeX env t1 t2+    go _  env (Coercion co1) (Coercion co2)   = guard $ eqCoercionX env co1 co2++    go lv env (Cast e1 _) e2 | it             = go lv env e1 e2+    go lv env e1 (Cast e2 _) | it             = go lv env e1 e2 #if MIN_VERSION_ghc(9,0,0)-    go env (Case s _ _ [Alt _ _ e1]) e2 | it, isUnsafeEqualityProof s = go env e1 e2-    go env e1 (Case s _ _ [Alt _ _ e2]) | it, isUnsafeEqualityProof s = go env e1 e2+    go lv env (Case s _ _ [Alt _ _ e1]) e2 | it, isUnsafeEqualityProof s = go lv env e1 e2+    go lv env e1 (Case s _ _ [Alt _ _ e2]) | it, isUnsafeEqualityProof s = go lv env e1 e2 #endif-    go env (Cast e1 co1) (Cast e2 co2)     = do guard (eqCoercionX env co1 co2)-                                                go env e1 e2+    go lv env (Cast e1 co1) (Cast e2 co2)     = traceBlock lv "CAST" "" $ \lv -> do+                                                   guard (eqCoercionX env co1 co2)+                                                   go lv env e1 e2 -    go env (App e1 a) e2 | it, isTyCoArg a = go env e1 e2-    go env e1 (App e2 a) | it, isTyCoArg a = go env e1 e2-    go env (App f1 a1)   (App f2 a2)       = go env f1 f2 >> go env a1 a2-    go env (Tick HpcTick{} e1) e2 | it     = go env e1 e2-    go env e1 (Tick HpcTick{} e2) | it     = go env e1 e2-    go env (Tick n1 e1)  (Tick n2 e2)      = guard (go_tick env n1 n2) >> go env e1 e2+    go lv env (App e1 a) e2 | it, isTyCoArg a = go lv env e1 e2+    go lv env e1 (App e2 a) | it, isTyCoArg a = go lv env e1 e2+    go lv env (App f1 a1)   (App f2 a2)       = traceBlock lv "APP" "" $ \lv -> do+                                                   go lv env f1 f2+                                                   go lv env a1 a2+    go lv env (Tick HpcTick{} e1) e2 | it     = go lv env e1 e2+    go lv env e1 (Tick HpcTick{} e2) | it     = go lv env e1 e2+    go lv env (Tick n1 e1)  (Tick n2 e2)      = traceBlock lv "TICK" "" $ \lv -> do+                                                   guard (go_tick env n1 n2)+                                                   go lv env e1 e2 -    go env (Lam b e1) e2 | it, isTyCoVar b = go env e1 e2-    go env e1 (Lam b e2) | it, isTyCoVar b = go env e1 e2-    go env (Lam b1 e1)  (Lam b2 e2)-      = do guard (it || eqTypeX env (varType b1) (varType b2))-                -- False for Id/TyVar combination-           go (rnBndr2 env b1 b2) e1 e2+    go lv env (Lam b e1) e2 | it, isTyCoVar b = go lv env e1 e2+    go lv env e1 (Lam b e2) | it, isTyCoVar b = go lv env e1 e2+    go lv env (Lam b1 e1)  (Lam b2 e2)        = traceBlock lv "LAM" (varToString b1 ++ " ~ " ++ varToString b2) $ \lv -> do+           guard (it || eqTypeX env (varType b1) (varType b2))+           go lv (rnBndr2 env b1 b2) e1 e2 -    go env (Let (NonRec v1 r1) e1) (Let (NonRec v2 r2) e2)-      = do go env r1 r2  -- No need to check binder types, since RHSs match-           go (rnBndr2 env v1 v2) e1 e2+    go lv env e1@(Let _ _) e2@(Let _ _)+      | ul+      , (ps1, e1') <- peelLets e1+      , (ps2, e2') <- peelLets e2+      = traceBlock lv "LET" (showVars ps1 ++ " ~ " ++ showVars ps2) $ \lv -> do+           guard $ equalLength ps1 ps2+           env' <- goBinds lv env ps1 ps2+           go lv env' e1' e2' -    go env (Let (Rec ps1) e1) (Let (Rec ps2) e2)+    go lv env (Let (NonRec v1 r1) e1) (Let (NonRec v2 r2) e2)+      = do go lv env r1 r2  -- No need to check binder types, since RHSs match+           go lv (rnBndr2 env v1 v2) e1 e2++    go lv env (Let (Rec ps1) e1) (Let (Rec ps2) e2)       = do guard $ equalLength ps1 ps2-           sequence_ $ zipWith (go env') rs1 rs2-           go env' e1 e2+           sequence_ $ zipWith (go lv env') rs1 rs2+           go lv env' e1 e2       where         (bs1,rs1) = unzip ps1         (bs2,rs2) = unzip ps2         env' = rnBndrs2 env bs1 bs2 -    go env (Case e1 b1 t1 a1) (Case e2 b2 t2 a2)+    go lv env (Case e1 b1 t1 a1) (Case e2 b2 t2 a2)       | null a1   -- See Note [Empty case alternatives] in TrieMap       = do guard (null a2)-           go env e1 e2+           go lv env e1 e2            guard (it || eqTypeX env t1 t2)       | otherwise       = do guard $ equalLength a1 a2-           go env e1 e2-           sequence_ $ zipWith (go_alt (rnBndr2 env b1 b2)) a1 a2+           go lv env e1 e2+           sequence_ $ zipWith (go_alt lv (rnBndr2 env b1 b2)) a1 a2 -    go _ _ _ = guard False+    go lv _ e1 e2 = do+        tracePut lv "FAIL" (conToString e1 ++ " =/= " ++ conToString e2)+        mzero      ------------    go_alt env (Alt c1 bs1 e1) (Alt c2 bs2 e2)-      = guard (c1 == c2) >> go (rnBndrs2 env bs1 bs2) e1 e2+    go_alt lv env (Alt c1 bs1 e1) (Alt c2 bs2 e2)+      = guard (c1 == c2) >> go lv (rnBndrs2 env bs1 bs2) e1 e2  #if MIN_VERSION_ghc(9,2,0)     go_tick :: RnEnv2 -> CoreTickish -> CoreTickish -> Bool@@ -241,8 +360,68 @@           = lid == rid  &&  map (rnOccL env) lids == map (rnOccR env) rids     go_tick _ l r = l == r +    peelLets (Let (NonRec v r) e) = let (xs, e') = peelLets e in ((v,r):xs, e')+    peelLets (Let (Rec bs) e)     = let (xs, e') = peelLets e in (bs ++ xs, e')+    peelLets e                    = ([], e) +    goBinds :: Int -> RnEnv2 -> [(Var, CoreExpr)] -> [(Var, CoreExpr)] -> StateT VarPairSet [] RnEnv2+    goBinds _  env []           []    = return env+    goBinds _  _   []           (_:_) = mzero+    goBinds lv env ((v1,b1):xs) ys'   = do+        -- select a binding+        ((v2,b2), ys) <- lift (choices ys') +        traceBlock lv "LET*" (varToString v1 ++ " =?= " ++ varToString v2) $ \lv ->+            go lv env b1 b2++        -- if match succeeds, delete it from the obligations+        modify (S.delete (v1, v2))+        -- continue with the rest of bindings, adding a pair as matching one.+        goBinds lv (rnBndr2 env v1 v2) xs ys+++traceBlock :: Monad m => Int -> String -> String -> (Int -> m ()) -> m ()+traceBlock lv name msg action = do+    tracePut lv name msg+    action (lv + 1)+    tracePut lv name $ msg ++ " OK"++showVars :: [(Var, a)] -> String+showVars xs = intercalate ", " [ varToString x | (x, _) <- xs ]++showVarPairSet :: VarPairSet -> String+showVarPairSet xs = intercalate ", " [ varToString x ++ " ~ " ++ varToString y | (x, y) <- S.toList xs ]++varToString :: Var -> String+varToString v = occNameString (occName (tyVarName v)) ++ "_" ++ show (getUnique v)+-- using tyVarName as varName is ambiguous.++conToString :: CoreExpr -> [Char]+conToString Var {}      = "Var"+conToString Lit {}      = "Lit"+conToString App {}      = "App"+conToString Lam {}      = "Lam"+conToString Let {}      = "Let"+conToString Case {}     = "Case"+conToString Cast {}     = "Cast"+conToString Tick {}     = "Tick"+conToString Type {}     = "Type"+conToString Coercion {} = "Coercion"++-- |+--+-- >>> choices ""+-- []+--+-- >>> choices "abcde"+-- [('a',"bcde"),('b',"acde"),('c',"abde"),('d',"abce"),('e',"abcd")]+--+choices :: [a] -> [(a, [a])]+choices = go id where+    go :: ([a] -> [a]) -> [a] -> [(a, [a])]+    go _ [] = []+    go f (x:xs) = (x, f xs) : go (f . (x :)) xs+ -- | Returns @True@ if the given core expression mentions no type constructor -- anywhere that has the given name. freeOfType :: Slice -> [Name] -> Maybe (Var, CoreExpr)@@ -370,3 +549,15 @@ doesNotContainTypeClasses :: Slice -> [Name] -> Maybe (Var, CoreExpr, [TyCon]) doesNotContainTypeClasses slice tcNs     = allTyCons (\tc -> not (isClassTyCon tc) || any (getName tc ==) tcNs) slice++rename :: [(Var, Var)] -> CoreExpr -> CoreExpr+rename rn = substExpr' sub where+    -- convert RnEnv2 to Subst+    -- here we forget about tyvars and covars, but mostly this is good enough.+    sub = mkOpenSubst emptyInScopeSet [ (v1, if isTyVar v2 then Type (mkTyVarTy v2) else if isCoVar v2 then Coercion (mkCoVarCo v2) else Var v2 ) | (v1, v2) <- rn]++#if MIN_VERSION_GLASGOW_HASKELL(9,0,0,0)+    substExpr' = substExpr+#else+    substExpr' = substExpr empty+#endif

@@ -38,7 +38,7 @@ import GHC.Types.TyThing #endif -import Test.Inspection (Obligation(..), Property(..), Result(..))+import Test.Inspection (Obligation(..), Equivalence (..), Property(..), Result(..)) import Test.Inspection.Core  -- | The plugin. It supports some options:@@ -105,8 +105,7 @@  prettyProperty :: (TH.Name -> String) -> TH.Name -> Property -> String prettyProperty showName target = \case-  EqualTo n2 False -> showName target ++ " === " ++ showName n2-  EqualTo n2 True  -> showName target ++ " ==- " ++ showName n2+  EqualTo n2 eqv   -> showName target ++ " " ++ showEquiv eqv ++ " " ++ showName n2   NoTypes [t]      -> showName target ++ " `hasNoType` " ++ showName t   NoTypes ts       -> showName target ++ " mentions none of " ++ intercalate ", " (map showName ts)   NoAllocation     -> showName target ++ " does not allocate"@@ -114,6 +113,10 @@   NoTypeClasses ts -> showName target ++ " does not contain dictionary values except of " ++ intercalate ", " (map showName ts)   NoUseOf ns       -> showName target ++ " uses none of " ++ intercalate ", " (map showName ns)   CoreOf           -> showName target ++ " core dump" -- :)+  where+    showEquiv StrictEquiv              = "==="+    showEquiv IgnoreTypesAndTicksEquiv = "==-"+    showEquiv UnorderedLetsEquiv       = "==~"  -- | Like show, but omit the module name if it is he current module showTHName :: Module -> TH.Name -> String