Commits:

• Fix Sized types (successor style): semi-continuity check not implemented #8829 by adding semi-continuity check

  Claude interaction

  There is test/Bugs/SizedTypesLoopDueInadmissibility.agda that allows a diverging program diverge.
  This is due to an admissibility test for types missing when recursion is justified via sizes,
  if the "successor style" is used for defining sized data types (like Nat in the reproducer).
  It is not needed when the Size< style is used. (See the paper $HOME/public_html/jfp15.pdf.)

  This test is described for a simpler type system in my CSL 2026 paper, see $HOME/public_html/lmcs07.pdf (journal version).
  It is also implemented in MiniAgda, see $HOME/miniagda/src/TypeChecker.hs, functions with name containing "SemiCont".

  Please make a plan where to integrate this check into the --sized-types machinery in Agda.

  Also, can the lack of this check also be exploited to proof absurdity? (The current counterexample is only about lacking termination.)

  Answer

  Short answer to your second question: yes, it proves ⊥

  The current Agda (2.9.0-2906817) accepts this file. It needs only --sized-types and successor-style sizes. It never uses Size<, so the known ∞ < ∞ problem plays no part.

  {-# OPTIONS --sized-types #-}
  open import Agda.Builtin.Size
  open import Agda.Builtin.Nat
  data ⊥ : Set where
  
  -- Big i n is inhabited iff n < i.
  data Big : Size → Nat → Set where
    stop : ∀ {i}   →           Big (↑ i) zero
    more : ∀ {i n} → Big i n → Big (↑ i) (suc n)
  
  shift : ∀ {i} → ((n : Nat) → Big (↑ i) n) → (n : Nat) → Big i n
  shift f n with f (suc n)
  ... | more b = b
  
  -- (n : Nat) → Big i n is empty for all finite i but inhabited at ω:
  -- not lower semi-continuous in i.
  loop : ∀ {i} → ((n : Nat) → Big i n) → ⊥
  loop f with f zero
  ... | stop = loop (shift f)
  
  big : (n : Nat) → Big ∞ n
  big zero    = stop
  big (suc n) = more (big n)
  
  absurd : ⊥
  absurd = loop big

  The file is at <scratchpad>/SizedFalse.agda. -vterm.matrices:40 shows that the only decrease is the -1 on the size argument: the dot pattern .(↑ j) in with-46 against the call argument j. This is the general principle in your paper: an inadmissible type lets you derive T ∞ from ∀ i<∞. T i. Choose T i = A i → ⊥ with A not lower semi-continuous (LSC), so that A ω is inhabited while every A k is empty, and you get a proof of ⊥ instead of just divergence. The Size< version of Big can't be written this way, because shift would need one bound j for all n.

  Where the unsound decrease comes from

  • Agda has no real matching on Size. In successor style, a size only gets the form ↑ j through unification: matching stop/suc against D i sets i := ↑ j, which leaves a dot pattern.
  • termToPattern in Termination/TermCheck.hs (around line 680, via parseDotP in termClause) turns a dot pattern ↑ t into a fake constructor pattern for SIZESUC. compareTerm' (around line 1450) then counts j < ↑ j as a decrease.
  • Size<-style recursion goes through compareVar and the SIZELT hypotheses instead (terSizeDepth, isBounded). That is well-founded recursion, as in JFP'15, so it needs no check.

  So the semi-continuity check only has to guard the SIZESUC decrease.

  Plan

  1. New module Agda/TypeChecking/SizedTypes/SemiContinuity.hs (TCM), modelled on MiniAgda's szCheckIndFunSize, lowerSemiContinuous and endsInSizedCo':

  • upperSemiContinuous i t decides whether the rest of a function type after the size binder i is admissible for recursion on i. Use telView, then:

    • every domain must be LSC in i;
    • the codomain must be upper semi-continuous (USC): monotone, or a sized coinductive type at i;
    • domains before the binder for i are not checked.

  • lowerSemiContinuous i a:

    • antitone (polarity i a ∈ {Nonvariant, Contravariant}, reusing Agda.TypeChecking.Polarity.polarity): yes.
    • Size< i (bounded quantification): yes.
    • D ps i ixs where D is a sized inductive type, the size index is exactly var i, and i is free nowhere else: yes. "Sized inductive" should mean that sizePolarity (Polarity.hs:283) confirmed the type, i.e. its constructors pass the checkSizeIndex and covariance checks. A type like w : Weird ∞ must not count. I'd store that result explicitly on Datatype rather than inferring it from the polarity being Covariant. Storing it bumps the interface version.
    • Phase 2: inductive non-recursive records and data whose field types are all LSC (Maybe (Nat i), Σ). Use a call stack against loops, as MiniAgda does.
    • Phase 3: recursive containers (Thm 4.18, e.g. List (Nat i)); Size<-style data that is sized by a parameter (LSC by construction); coinductive records with Size< fields as USC targets.
    • Otherwise: no. In particular B → C i is not LSC, which is exactly the reproducer.

    Using polarity rather than leqType against ↑ i keeps the check syntactic and free of constraints. It is conservative, because Invariant falls through to "no".

  2. Use it in the termination checker, not in LHS checking. Mirror the existing --without-K masks:

  • Precompute a mask. Next to terProjectedNameToMaskArgs and argumentMasksForPath, which already handle copattern paths, compute a per-(f, path) ListInf Bool "size-suc admissible" mask. Set the flag only at argument positions whose type is a size (isSizeType, including Size< u), and set it to the result of upperSemiContinuous on the rest of the type. Do this only under sizedTypesOption, and lazily: only when a clause actually yields a SIZESUC pattern at that position.
  • Apply it in termClause. After parseDotP, turn a top-level SIZESUC pattern back into a plain dot pattern at any masked position. That call then gets ? instead of -1.
  • What still passes. Definitions that terminate for other reasons still pass, e.g. the structural first clause of loop in the reproducer. Only the unjustified decrease is lost.
  • With-functions. These get the check too, since their generated types contain the same domains (with-46 : {i} → ((n : Nat) → Big i n) → Big i 0 → ⊥). Watch for false negatives from extra with-abstracted types, e.g. inspect-style equations whose polarity is Invariant.

  3. Diagnostics. Have the masking record which size argument it dropped and the first domain that failed. Attach that to the TerminationError payload (Monad/Base.hs) and print it in TypeChecking/Errors.hs, e.g. "Decrease of size i via ↑ not used: argument type (n : Nat) → Big i n is not lower semi-continuous in i". This needs no new ErrorName.

  4. Rejected alternative: MiniAgda's place (checkPattern). A hard error when LHS unification instantiates a size parameter of the function to ↑ j would also reject successor-style programs that never use the decrease for termination. It would also need a new error and the five-place error registration. The termination-checker mask is less intrusive.

  5. Nested sizes. Look at ↑ dot patterns nested inside constructor patterns. compareConArgs multiplies the argument orders, so c {↑ j} x → c {j} x counts as a decrease. I couldn't quickly build an exploit, because the other fields must compare as ≤, but the plan should either apply the mask there too or argue why it's safe.

  6. Tests and docs:

  • Move SizedTypesLoopDueInadmissibility.agda from test/Bugs to test/Fail, and add SizedFalse there as well.
  • Add test/Succeed cases for admissible types: Nat i → Nat i, Maybe (Nat i) domains, antitone domains, and with-functions.
  • 51 of the 106 --sized-types tests in test/Succeed contain successor-style-looking syntax (rough grep), so run make succeed and the std-lib suite to measure fallout. std-lib's Codata.Sized uses Size< and should be unaffected.
  • Add a CHANGELOG entry and a section on admissibility in the user manual's sized-types chapter.

  Prompt 2

  I now reported the new proof of False as issue Sized types (successor style): semi-continuity check not implemented #8829 (your repro with some small changes for clarity), please use this as test/Fail/Issue8829.agda (this superseds SizedTypesLoopDueInadmissibility.agda which can be deleted once the issue is fixed).

  One refinement idea: B → C i can be LSC if B is finite (e.g. Bool) and C is LSC.
  We already have some analysis of finiteness for types for Cubical Agda, if I am not mistaken (see Dom type).
  Can we reuse this concept to make the check more liberal?

  Answer 2

  I added the test and put it on a new branch:

  • Branch: issue8829, created from master.
  • Test: test/Fail/Issue8829.agda holds the code from issue Sized types (successor style): semi-continuity check not implemented #8829, with a short header comment. It isn't committed yet.
  • Current behaviour: run from test/Fail, today's agda accepts it (exit code 0). That confirms the bug.
  • No .err file yet: the expected-error file can only be generated once the fix exists. Until then the fail suite will report this test.
  • test/Bugs/SizedTypesLoopDueInadmissibility.agda: I'll delete it together with the fix.

  What your version adds to the plan

  The decrease now comes through the where-function aux, not a with-function. The termination checker's call matrices show the same pattern:

  aux --> loop
     =    ?    ?    ?
     ?   -1    ?   -1
  

  The rule "this size argument's ↑ pattern doesn't count" is attached to each function's own type, so it covers this case automatically. aux's type includes the enclosing function's arguments, so it is (i : Size) → T i → IsNat i zero → ⊥, and the argument type T i fails the check.

  The second -1 comes from comparing the size j with the constructor pattern isZero j, of which it is a part. On its own it gives no decrease when the calls are combined, because aux's fourth argument is f zero, which compares as unknown (?). Once the fix is in, I'll check the debug output to confirm that this route doesn't keep loop passing.

  Finite domains: yes, but domIsFinite isn't the tool

  Why the refinement is sound. Take a domain B that is finite and doesn't mention i. If each C b i is lower semi-continuous in i, then (b : B) → C b i is too. The key fact is that the "eventually always" limit (liminf) commutes with finite intersections: given x ∈ ⋂_{α≤i<λ} A i and x ∈ ⋂_{β≤i<λ} A' i, take max α β as the common starting point. With an infinite index set there may be no common starting point, which is exactly what T i = ∀ n → IsNat i n exploits.

  What domIsFinite actually is. It isn't a finiteness analysis of types. It's a flag on function domains, set by the cubical primitives (Primitive/Base.hs:81) for the irrelevant IsOne φ argument of Partial φ A. Conversion.hs:447 uses it to compare functions face by face. It never marks something like Bool as finite, so it can't be reused for that.

  What it does point to. A domain with at most one element is trivially finite. Such domains are:

  • domains marked with domIsFinite;
  • irrelevant domains (.(x : B) →);
  • domains whose type lives in Prop or SProp.

  These can be accepted with no further analysis, and IsOne is just one instance of them.

  Proposed isFiniteType (in the new SizedTypes/SemiContinuity.hs)

  lowerSemiContinuous i ((b : B) → C)  =  i ∉ FV(B)  ∧  isFiniteType B  ∧  lowerSemiContinuous i C
  

  isFiniteType B returns yes when either:

  • B is a subsingleton domain, as listed above; or
  • B reduces to an inductive data type or record D ps that isn't recursive and whose constructor arguments are all finite types. This covers Bool, ⊤, ⊥, Maybe Bool and finite tuples.

  Further details:

  • Constructor argument types: compute them after plugging in the parameters, reusing the constructor-type helpers in TypeChecking/Datatypes.hs.
  • Recursive types: keep a stack of the definitions being visited, as MiniAgda does, and answer no when D is reached again.
  • Indexed families: they are fine. Ignoring the index can only add constructors that don't apply, so the answer stays correct, just less precise.
  • Erased (@0) arguments: they still count as data and must be finite themselves. Only irrelevant arguments collapse.
  • Everything else is a no, including Nat, Size, Level, function types and Fin n. Fin n is finite for each n, but it's recursive, so the check can't see that.

  Nothing like this exists in the code base yet. The nearest existing checks only decide emptiness or the singleton property for eta-expansion.

  Prompt 3

  Ok, the plan looks good, please go ahead and implement it.
  If I understand correctly, the semi-continuity and finiteness checks only run when size-based termination is actually tried; this would be important, to not waste computation time when sized types are not involved or the Size< style is used rather than the successor-size style.

  Please make sure there are enough tests so that all cases of LSC/USC are executed at least once (test case coverage).

  Answer 3

  I've implemented the check on branch issue8829; nothing is committed yet. Issue Sized types (successor style): semi-continuity check not implemented #8829, the old reproducer and the 13 failure cases in the new tests are now rejected. Two library tests that used to pass are now rejected as well, and how to handle them is your decision (end of this message).

  When the check runs. It only runs when a clause actually has a .(↑ j) dot pattern in a size argument, which is the only way the termination checker gets a SIZESUC decrease. Without --sized-types that never happens, and Size<-style recursion never produces such patterns. In both cases no semi-continuity or finiteness check runs. Results are cached per function, projection path and argument position.

  How it works:

  • Termination checker (Termination/TermCheck.hs): after the dot patterns of a clause are parsed, revertInadmissibleSizeSuc turns a top-level ↑ pattern back into a plain dot pattern if the function's type is not upper semi-continuous in that size. The type is followed through projection patterns, so copattern definitions are covered too. Only the unjustified decrease is lost; structural recursion still works.
  • New module TypeChecking/SizedTypes/SemiContinuity.hs: the rules we discussed, including finite domains. Irrelevant domains, Prop domains and IsOne (domIsFinite) count as finite. A data type counts as sized-inductive in an argument position only if:
    • that position is its first index, of type Size;
    • sizePolarity found that index covariant;
    • none of its constructors uses the musical ∞.
  • Error message: when termination fails, it now says why, naming the offending type; with-functions are reported under their parent function's name:

    Note: matching a size against a successor does not provide
    termination evidence if the type of the function is not upper
    semi-continuous in the size:
      aux: argument type T i is not lower semi-continuous in i
    

  • I also exported polarity from Polarity.hs, added a CHANGELOG entry marked BREAKING, and added a user-manual section. The manual's literate file type-checks, but I couldn't render it with Sphinx (sphinxcontrib.jquery is missing here).

  Tests and coverage. I traced the rules with -v term.size.semicont:20. Every success and failure case of LSC, USC and finiteness fires at least once, and both the plain-argument and the copattern paths are taken. The only branch not exercised is a defensive fallback for when the type can't be followed along the patterns, which shouldn't happen for well-typed clauses.

  • test/Succeed/Issue8829Admissible.agda: 20 functions that terminate only thanks to the size, one per success rule, including with-functions, where-functions and copatterns.
  • test/Succeed/Issue8829Cubical.agda: the Partial/IsOne finite-domain case.
  • test/Fail/Issue8829Inadmissible.agda: 13 failing cases, each .err entry naming its reason.
  • test/Fail/Issue8829.agda: your issue reproducer. test/Bugs/SizedTypesLoopDueInadmissibility.agda is deleted, as you asked.
  • --no-double-check: the new tests need this flag, as many sized-types tests already do; otherwise double-checking reports unsolved size constraints.

  Results. succeed (2092) and fail (1880) pass, as do cubical-succeed and interaction-simple. The two failures in bugs are your untracked UnusedImportedModules/WarningUnusedModules tests and are unrelated. Getting there needed three existing tests changed:

  • Succeed/Issue1209-3 → Fail/Issue1209-3b: this is itself a proof of ⊥ (musical Mu-co with --guardedness --sized-types), and it is now rejected.
  • Succeed/Issue59b → Fail/Issue59b: Heap i j has two size indices, but only the first is covariant. Agda gives Heap the polarity [+], so the j position is invariant and therefore not LSC. If you'd rather keep this test passing, the size-polarity check would need to certify more than one size index.
  • Fail/Issue1946-4.err: iter on Mu F i with F a variable is now rejected as well, in addition to the error the test already expected.

  Decision needed: 2 of 25 std-lib-succeed tests now fail.

  1. Termination/Sized/DeBruijnExSubstSized: the result type of evalNAT is eval {ι} (lamE f t) ≡ lam f (eval {ι} t). Here ι appears only inside terms, so my rule "the indices must not mention i" rejects it. Since sizes are erased and can't be matched on, a term's meaning can't depend on its size arguments. I'd suggest ignoring occurrences of i in arguments that are neither types nor of type Size. That would accept this test and seems sound under the erasure model. Should I implement it?
  2. SizeInconsistentMeta4: the argument _<_ {z} x y is not recognised as a sized type, because z also occurs in the other indices x y : Type z, so sizePolarity marks z as invariant. Under the exact reading of that index, LSC really does fail at ∞, so I think the rejection is principled. Accepting it would mean extending sizePolarity; the alternative is to treat this as a known breaking change.

• Remove use of IORefs; precompute SizeSucVerdicts

  Claude interaction

  Prompt 4

  The current implementation (committed) uses IORef, but we discourage use of IORef .
  Please present a plan for a solution without imperative features like IORef.

  Answer 4

  The IORef does two jobs, and both can be done without it:

  1. Cache: the admissibility verdict per (function, projection path, argument position), so it is computed once, not once per clause.
  2. Collected reasons: read back on the failure path to build the note in TerminationError.

  Recommended: precompute the verdicts into an immutable map in TerEnv

  This follows the pattern the --without-K argument masks already use: buildNodeAndProjectionMaps precomputes them per SCC in TCM and hands them to the termination checker through the reader environment.

  1. New pre-pass buildSizeSucVerdicts :: Set QName -> TCM SizeSucVerdicts (in TermCheck.hs, next to buildNodeAndProjectionMaps).

  • When it runs: only when sizeSucName is Just, i.e. with --sized-types and the SIZESUC builtin bound. Otherwise it returns Map.empty and costs nothing.
  • Which slots: for each function in the SCC and each clause, find the top-level argument positions holding a dot pattern whose term, reduced in the clause telescope, is ↑ t. To keep this test identical to the one in termToPattern, factor out isSizeSucTerm :: Term -> TCM Bool and call it from both places.
  • Verdicts: for each distinct (f, path, slot) found, run the existing walk/admissibleForSizeRecursion once and store the verdict.
  • Cost: with sized types on, the top-level dot patterns of each clause are reduced once more. The semi-continuity and finiteness checks still run only for positions that really have a successor pattern, so Size<-style and non-sized code still pay nothing.

  2. TerEnv: replace terSizeSucVerdicts :: Maybe (IORef SizeSucVerdicts) with terSizeSucVerdicts :: !SizeSucVerdicts, default Map.empty. In termMutual, set it in runTerm alongside terSetProjectedNameToMaskArgs. Creating the ref in runTerDefault goes away, along with the Data.IORef imports in Monad.hs and TermCheck.hs.

  3. sizeSucAdmissible becomes a pure lookup.

  • Hit: use the stored verdict.
  • Miss: possible only if the pre-pass and termToPattern ever disagree. It counts as inadmissible with no reason given, so a mismatch can only cost precision, never soundness. It also emits a debug message at term.size.semicont, so a mismatch shows up while debugging.

  4. Reasons: terGetInadmissibleSizes reads the same map with terAsks, keeps the SizeSucInadmissible (Just cl) entries, and maps with-functions to their parent function as it does now. The two TerminatesNot branches (termMutual', termFunction) need no other changes.

  5. Tests: the existing tests already cover this, since every rule and both the plain-argument and copattern paths are exercised. As a check, I'd compare -v term.size.semicont:10 before and after on Issue8829Admissible/Issue8829Inadmissible. The same (f, path, slot) keys should be checked, but each only once even for multi-clause functions. Then re-run succeed, fail and std-lib-succeed.

  Simpler alternative: no cache at all

  • Admissibility: recompute it per clause inside termClause, purely in TCM, with no cache. It still runs only for successor slots. The price is that a function with several clauses matching on ↑ checks the same type several times; the check is linear in the size of the type.
  • Reasons: recompute them only on the failure path. When TerminatesNot is reached, rescan the clauses of the functions in the SCC and run the check again to build the notes. The success path never pays for this.

  This touches less code but repeats work in the common case, so I'd go with the precomputed map. I'd avoid making TerM a StateT or adding a Writer: that is more invasive because of the many terLocal uses and forM' folds, and it stays imperative in spirit.

  Shall I implement the precomputed-map version?

  Prompt 5

  please implement the precomputed-map version

  Answer 5

  The IORef is gone: the verdicts are now computed in advance into a read-only map in the termination checker's environment.

  What changed:

  • New pre-pass buildSizeSucVerdicts. It runs once per SCC in termMutual, next to buildNodeAndProjectionMaps, and returns Map.empty straight away if sizeSucName is Nothing. Otherwise it looks at each clause's top-level dot patterns in the clause telescope and records the positions that reduce to ↑ t. Each distinct (function, projection path, position) is then checked once by sizeSucVerdict, which is the old type walk turned into a top-level TCM function.
  • Shared successor test. The pre-pass and termToPattern use the same helpers, reduceDotPatternTerm and isSizeSucApp, so they recognise ↑ dot patterns in the same way.
  • TerEnv. The field terSizeSucVerdicts is now an immutable SizeSucVerdicts map with default Map.empty, set through terSetSizeSucVerdicts. runTerDefault no longer creates a ref, and the Data.IORef imports are gone.
  • sizeSucAdmissible is a pure lookup. If no verdict is found, the pattern counts as inadmissible and a debug message is printed, so a mismatch between the pre-pass and termToPattern could only lose precision, never soundness.
  • Failure notes. terGetInadmissibleSizes reads the reasons from the same map, still reporting with-functions under their parent's name.

• Separate test cases that need --guardedness

• Move Size-related functions from TermCheck into new module