From ffe79ce974125733ae3eab92e13bc9f457b64482 Mon Sep 17 00:00:00 2001
From: Iavor Diatchki <iavor.diatchki@gmail.com>
Date: Tue, 3 Sep 2024 14:28:18 -0700
Subject: [PATCH] Add a comment.

---
 src/Cryptol/TypeCheck/SimpType.hs | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/Cryptol/TypeCheck/SimpType.hs b/src/Cryptol/TypeCheck/SimpType.hs
index d994dc3d7..fdadc3c18 100644
--- a/src/Cryptol/TypeCheck/SimpType.hs
+++ b/src/Cryptol/TypeCheck/SimpType.hs
@@ -113,7 +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 argumet
+       is finite and less than the first;  the second should have been handleed
+       by the first equation above `tOp`. -}
+
   | Just 0 <- yNum = x
   | Just k <- yNum
   , TCon (TF TCAdd) [a,b] <- tNoUser x