non-monadic sizing, partial sizing, both broken?

minimal.tel

@@ -0,0 +1,16 @@
+thing = { \i -> i
+        , \recur i -> recur (left i)
+        , \i -> i
+        }
+
+valid = \x -> assert (not ($33 left x)) " "
+
+main = \input -> let userInput = left input
+                     firstChar = left userInput
+                     limInput : valid = firstChar
+                     oldState = right input
+
+                     output = if thing limInput then "!" else "#"
+                 in if not input
+                    then (" ", 1)
+                    else (output, 0)

src/Telomare.hs

@@ -908,3 +908,10 @@ pattern AbortAny :: IExpr
 pattern AbortAny = Pair (Pair (Pair Zero Zero) Zero) Zero
 pattern AbortUnsizeable :: IExpr -> IExpr
 pattern AbortUnsizeable t = Pair (Pair (Pair (Pair Zero Zero) Zero) Zero) t
+
+convertAbortMessage :: IExpr -> String
+convertAbortMessage = \case
+  AbortRecursion -> "recursion overflow (should be caught by other means)"
+  AbortUser s -> "user abort: " <> g2s s
+  AbortAny -> "user abort of all possible abort reasons (non-deterministic input)"
+  x -> "unexpected abort: " <> show x

src/Telomare/Eval.hs

@@ -29,8 +29,8 @@ import Telomare (BreakState, BreakState', ExprA (..), FragExpr (..),
                  PartialType (..), RecursionPieceFrag,
                  RecursionSimulationPieces (..), RunResult, RunTimeError (..),
                  TelomareLike (..), Term3 (Term3), Term4 (Term4),
-                 UnsizedRecursionToken (..), app, appF, eval, deferF, forget, g2s, innerChurchF,
-                 insertAndGetKey, pairF, pattern AbortAny, pattern AbortRecursion,
+                 UnsizedRecursionToken (..), app, appF, eval, convertAbortMessage, deferF, forget, g2s,
+                 innerChurchF, insertAndGetKey, pairF, pattern AbortAny, pattern AbortRecursion,
                  pattern AbortUser, rootFrag, s2g, setEnvF, tag, unFragExprUR)
 import Telomare.Optimizer (optimize)
 import Telomare.Parser (AnnotatedUPT, UnprocessedParsedTerm (..), parsePrelude)
@@ -178,13 +178,6 @@ removeChecks (Term4 m) =
         insertAndGetKey $ DummyLoc :< DeferFragF envDefer
   in Term4 $ Map.map (transform f) newM
 
-convertAbortMessage :: IExpr -> String
-convertAbortMessage = \case
-  AbortRecursion -> "recursion overflow (should be caught by other means)"
-  AbortUser s -> "user abort: " <> g2s s
-  AbortAny -> "user abort of all possible abort reasons (non-deterministic input)"
-  x -> "unexpected abort: " <> show x
-
 runStaticChecks :: Term4 -> Either EvalError Term4
 runStaticChecks t@(Term4 termMap) =
   let result = evalA combine (Just Zero) t