Merge pull request #4300 from IntersectMBO/PR-assert-hotfix

`constrained-generators`: hotfix of latest derp...

libs/constrained-generators/src/Constrained/Base.hs

@@ -978,7 +978,15 @@ linearize ::
   (MonadGenError m, BaseUniverse fn) => [Pred fn] -> DependGraph fn -> m [(Name fn, [Pred fn])]
 linearize preds graph = do
   sorted <- case topsort graph of
-    Left cycle -> fatalError ["dependency cycle in graph", show cycle, show graph]
+    Left cycle ->
+      fatalError $
+        [ "linearize: Dependency cycle in graph: "
+        , "  cycle: " ++ show cycle
+        , "  preds:"
+        ]
+          ++ [show $ indent 4 (pretty p) | p <- preds]
+          ++ [ "  graph: " ++ show graph
+             ]
     Right sorted -> pure sorted
   go sorted [(freeVarSet ps, ps) | ps <- filter isRelevantPred preds]
   where
@@ -995,7 +1003,12 @@ linearize preds graph = do
             then pure []
             else genError ["Linearize const False"]
       | otherwise =
-          fatalError $ "Dependency error in `linearize`: " : show graph : map (mappend "  " . show) ps
+          fatalError $
+            [ "Dependency error in `linearize`: "
+            , "  graph: " ++ show graph
+            , "  the following left-over constraints are not defining constraints for a unique variable: "
+            ]
+              ++ [show $ indent 4 (pretty p) | (_, p) <- ps]
     go (n : ns) ps = do
       let (nps, ops) = partition (isLastVariable n . fst) ps
       ((n, map snd nps) :) <$> go ns ops
@@ -3783,7 +3796,11 @@ reify t f body =
     ]
 
 assertReified :: HasSpec fn a => Term fn a -> (a -> Bool) -> Pred fn
-assertReified = reifies (lit True)
+-- Note, it is necessary to introduce the extra variable from the `exists` here
+-- to make things like `assertRealMultiple` work, if you don't have it then the
+-- `reifies` isn't a defining constraint for anything any more.
+assertReified t f =
+  reify t f assert
 
 reifies :: (HasSpec fn a, HasSpec fn b) => Term fn b -> Term fn a -> (a -> b) -> Pred fn
 reifies = Reifies

libs/constrained-generators/src/Constrained/Examples/Basic.hs

@@ -156,3 +156,10 @@ assertReal = constrained $ \x ->
   [ assert $ x <=. 10
   , assertReified x (<= 10)
   ]
+
+assertRealMultiple :: Specification BaseFn (Int, Int)
+assertRealMultiple = constrained' $ \x y ->
+  [ assert $ x <=. 10
+  , assert $ 11 <=. y
+  , assertReified (pair_ x y) $ uncurry (/=)
+  ]

libs/constrained-generators/test/Constrained/Test.hs

@@ -45,6 +45,7 @@ tests :: Spec
 tests =
   describe "constrained" $ do
     testSpec "assertReal" assertReal
+    testSpec "assertRealMultiple" assertRealMultiple
     testSpec "setSpec" setSpec
     testSpec "leqPair" leqPair
     testSpec "setPair" setPair