fix indep redex test, take 2

hackworthltd · Jul 14, 2023 · 930bf8f · 930bf8f
1 parent 8d4eda8
commit 930bf8f
Showing 1 changed file with 11 additions and 3 deletions.
diff --git a/primer/test/Tests/Eval.hs b/primer/test/Tests/Eval.hs
@@ -1444,8 +1444,12 @@ tasty_type_preservation =
 -- then @j ∈ redexes e'@,
 -- unless one of the following is true
 -- - @j@ no longer exists in @e'@
--- - @j@ was a rename-binding which is no longer required because @i@ was eliding a let
+-- - @j@ was a rename-binding which is no longer required
+--       (e.g. because @i@ was eliding a let, or reducing inside the binding of
+--       a let removing a variable reference)
 -- - @i@ was a PushLet, which can intersperse itself inside the parts of @j@'s redex, blocking it
+-- - @j@ was a PushLet surrounding @i@, and @i@ either reduced to a leaf or
+--       removed a variable reference, causing us to not PushLet, but ElideLet
 tasty_redex_independent :: Property
 tasty_redex_independent =
   let testModules = [builtinModule, pure primitiveModule]
@@ -1470,9 +1474,13 @@ tasty_redex_independent =
                   then do
                     sj <- failWhenSevereLogs $ step @EvalLog tds globs t dir j
                     case (sj, siDetails) of
-                      (Right (_, BindRename{}), LetRemoval{})  -> success
-                      (Right (_, BindRename{}), TLetRemoval{})  -> success
+                      (Right (_, BindRename{}), _)  -> success
                       (_, PushLetDown{})  -> success
                       (_, PushLetDownTy{})  -> success
+                      (Right (_, PushLetDown{}), CaseReduction{})  -> success
+                      (Right (_, PushLetDown{}), CaseReductionTrivial{})  -> success
+                      (Right (_, PushLetDown{}), RemoveAnn{})  -> success
+                      (Right (_, PushLetDown{}), LetRemoval{})  -> success
+                      (Right (_, PushLetDownTy{}), TLetRemoval{})  -> success
                       _ -> assert . elem j =<< failWhenSevereLogs (redexes @EvalLog tds globs dir s')
                   else success