start adding type-level simplification tests

package.yaml

@@ -70,3 +70,11 @@ dependencies:
 
 library:
   source-dirs: src
+
+tests:
+  spec:
+    source-dirs: test
+    main: Main.hs
+    dependencies:
+    - rerefined
+    - type-spec ^>= 0.4.0.0

rerefined.cabal

@@ -81,3 +81,34 @@ library
     , text-builder-linear >=0.1.2 && <0.2
     , type-level-show >=0.2.1 && <0.4
   default-language: GHC2021
+
+test-suite spec
+  type: exitcode-stdio-1.0
+  main-is: Main.hs
+  other-modules:
+      Paths_rerefined
+  hs-source-dirs:
+      test
+  default-extensions:
+      LambdaCase
+      NoStarIsType
+      DerivingVia
+      DeriveAnyClass
+      GADTs
+      RoleAnnotations
+      DefaultSignatures
+      TypeFamilies
+      DataKinds
+      MagicHash
+  ghc-options: -Wall -Wno-unticked-promoted-constructors
+  build-depends:
+      QuickCheck >=2.14 && <2.16
+    , base >=4.18 && <5
+    , mono-traversable >=1.0.17.0 && <1.1
+    , rerefined
+    , template-haskell >=2.19.0.0 && <2.23
+    , text >=2.0 && <2.2
+    , text-builder-linear >=0.1.2 && <0.2
+    , type-level-show >=0.2.1 && <0.4
+    , type-spec >=0.4.0.0 && <0.5
+  default-language: GHC2021

test/Main.hs

@@ -0,0 +1,30 @@
+module Main where
+
+import Test.TypeSpec hiding ( And )
+import Rerefined.Simplify
+import Rerefined.Predicates
+import Rerefined.Predicate
+import TypeLevelShow.Utils ( type (++) )
+
+main :: IO ()
+main = print spec
+
+spec :: Expect
+    (And Fail    Succeed `SimplifiesTo` Fail
+ -/- And Succeed Fail    `SimplifiesTo` Fail
+ -/- And Succeed Succeed `SimplifiesTo` Succeed
+ -/- And Fail    Fail    `SimplifiesTo` Fail
+
+ -/- Or  Succeed Fail    `SimplifiesTo` Succeed
+ -/- Or  Fail    Succeed `SimplifiesTo` Succeed
+ -/- Or  Succeed Succeed `SimplifiesTo` Succeed
+ -/- Or  Fail    Fail    `SimplifiesTo` Fail
+ -/- And (CompareLength RelOpLT 3) (CompareLength RelOpGT 3)
+        `SimplifiesTo` Fail
+    )
+spec = Valid
+
+-- | TODO I'd like to write my own message here, but type-spec is complicated.
+type SimplifiesTo p p' = It
+    (PredicateName 0 p ++ " simplifies to " ++ PredicateName 0 p')
+    (TrySimplify p `Is` Just p')