Merge pull request #1742 from GaloisInc/issue_1741

Simplify `inf - x` to `inf`
GaloisInc · Sep 4, 2024 · c73d1d8 · c73d1d8
2 parents e2cd5f0 + 3dafe2b
commit c73d1d8
Showing 1 changed file with 7 additions and 0 deletions.
diff --git a/src/Cryptol/TypeCheck/SimpType.hs b/src/Cryptol/TypeCheck/SimpType.hs
@@ -113,6 +113,13 @@ tSub :: Type -> Type -> Type
 tSub x y
   | Just t <- tOp TCSub (op2 nSub) [x,y] = t
   | tIsInf y  = tError (tf2 TCSub x y)
+
+  | tIsInf x = x
+    {- This assumes that `y` is finite and not error.  The first should
+       follow from the typing on `tSub`, which asserts that the second argument
+       is finite and less than the first;  the second should have been handled
+       by the first equation above, see `tOp`. -}
+
   | Just 0 <- yNum = x
   | Just k <- yNum
   , TCon (TF TCAdd) [a,b] <- tNoUser x