OptionCase without caseNone type annotation causes a confusing "Unexpected type" RewriterException

## Description

When using `OptionCase` without manually writing a type annotation on the `caseNone` lambda, we get a frustrating/confusing error message. If the error is intended (preferably it should work out of the box, as it works with TLC), the user is given no useful information that points towards a missing type annotation.

```
problemOperator(self) ==
  LET q1 == operator1(self) IN
  IF IsNone(q1) THEN None ELSE (
    LET v1 == OptionGetOrElse(q1, self) IN
    OptionCase(operator2(self, v1),
      \* @type: Int => Some(<<Int, Int>>) | None(UNIT);
      LAMBDA v2: Some(<<v1, v2>>),
      \* Broken without below type annotation
      \* type: UNIT => Some(<<Int, Int>>) | None(UNIT);
      LAMBDA u: None
    )
  )
```

Error message:

```
PASS #13: BoundedChecker                                          I@22:59:22.961
Step 0: picking a transition out of 1 transition(s)               I@22:59:23.667
<unknown>: rewriter error: Unexpected type a140 when generating a default value E@22:59:23.756
at.forsyte.apalache.infra.AdaptedException: <unknown>: rewriter error: Unexpected type a140 when generating a default value
	at at.forsyte.apalache.infra.passes.PassChainExecutor$.run(PassChainExecutor.scala:39)
	at at.forsyte.apalache.tla.tooling.opt.CheckCmd.run(CheckCmd.scala:136)
	at at.forsyte.apalache.tla.Tool$.runCommand(Tool.scala:139)
	at at.forsyte.apalache.tla.Tool$.run(Tool.scala:119)
	at at.forsyte.apalache.tla.Tool$.main(Tool.scala:40)
	at at.forsyte.apalache.tla.Tool.main(Tool.scala)
Please report an issue at [https://github.com/informalsystems/apalache/issues]: at.forsyte.apalache.infra.AdaptedException: <unknown>: rewriter error: Unexpected type a140 when generating a default value
```

## Impact

Can be worked around, but very frustrating/confusing error message for the user.

## Input specification

```
\* apalache-mc check --debug --write-intermediate OptionCaseBug.tla 

------------------------------- MODULE OptionCaseBug -------------------------------
EXTENDS Integers, Sequences, FiniteSets, TLC, Option

VARIABLES
  \* @type: Int -> Str;
  myPc

\* @type: Seq((Int -> Str));
vars == <<myPc>>

ThreadInit(t) ==
  /\ myPc = [ x \in t |-> "Idle" ]

\* @type: Int => Some(Int) | None(UNIT);
operator1(x) ==
  IF (x % 2) = 0 THEN
    Some(x)
  ELSE
    None

\* @type: (Int, Int) => Some(Int) | None(UNIT);
operator2(x, y) ==
  IF ((x + y) % 2) = 0 THEN
    Some(x + y)
  ELSE
    None

\* @type: Int => Some(<<Int, Int>>) | None(UNIT);
problemOperator(self) ==
  LET q1 == operator1(self) IN
  IF IsNone(q1) THEN None ELSE (
    LET v1 == OptionGetOrElse(q1, self) IN
    OptionCase(operator2(self, v1),
      \* @type: Int => Some(<<Int, Int>>) | None(UNIT);
      LAMBDA v2: Some(<<v1, v2>>),
      \* Broken without below type annotation
      \* type: UNIT => Some(<<Int, Int>>) | None(UNIT);
      LAMBDA u: None
    )
  )

\* @type: Int => Some(<<Int, Int>>) | None(UNIT);
problemOperatorAlsoBroken(self) == \* broken
  LET q1 == operator1(self) IN
  IF IsNone(q1) THEN None ELSE (
    LET
      v1 == OptionGetOrElse(q1, self)
      \* @type: Int => Some(<<Int, Int>>) | None(UNIT);
      caseSome(v2) == Some(<<v1, v2>>)
      \* Broken without below type annotation
      \* type: UNIT => Some(<<Int, Int>>) | None(UNIT);
      caseNone(u) == None
    IN
    OptionCase(operator2(self, v1),
      caseSome,
      caseNone
    )
  )

\* Alternate working formulation without LAMBDAs that avoids this bug
\* @type: Int => Some(<<Int, Int>>) | None(UNIT);
problemOperatorAlternate(self) ==
  LET q1 == operator1(self) IN
  IF IsNone(q1) THEN None ELSE
    LET v1 == OptionGetOrElse(q1, self) IN
    LET q2 == operator2(self, v1) IN
    IF IsNone(q2) THEN None ELSE
      Some(<<v1, OptionGetOrElse(q2, Guess(1..100))>>)

\* @type: Int => Bool;
ThreadNext(self) ==
  /\ IsSome(problemOperator(self))
  /\ myPc' = [myPc EXCEPT ![self] = "abcdef"]

Threads == {1, 2, 3, 4, 5, 6, 7, 8}
Init == ThreadInit(Threads)
Terminating == /\ \A s \in Threads: myPc[s] = "Done"
               /\ UNCHANGED vars
Next ==
  \/ (\E self \in Threads: ThreadNext(self))
  \/ Terminating
Spec == Init /\ [][Next]_vars

=============================================================================
````

## The command line parameters used to run the tool

```
--debug --write-intermediate
```

## Expected behavior

Either no error (ideally) or a more user-friendly error instructing the user on how to fix the problem.
TLC runs this spec perfectly (after copying `.tla` stubs as needed) fine with no issues.

## Log files

<details>

```
2025-07-18T22:59:17,923 [main] INFO  a.f.a.t.Tool\$ - # APALACHE version: 56462d3 | build: 56462d3
2025-07-18T22:59:17,958 [main] INFO  a.f.a.t.t.o.CheckCmd - Tuning: search.outputTraces=false
2025-07-18T22:59:18,295 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #0: SanyParser
2025-07-18T22:59:19,492 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #0: SanyParser [OK]
2025-07-18T22:59:19,493 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #1: TypeCheckerSnowcat
2025-07-18T22:59:19,493 [main] INFO  a.f.a.t.p.t.EtcTypeCheckerPassImpl -  > Running Snowcat .::.
2025-07-18T22:59:21,448 [main] INFO  a.f.a.t.p.t.EtcTypeCheckerPassImpl -  > Your types are purrfect!
2025-07-18T22:59:21,449 [main] INFO  a.f.a.t.p.t.EtcTypeCheckerPassImpl -  > All expressions are typed
2025-07-18T22:59:21,533 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #1: TypeCheckerSnowcat [OK]
2025-07-18T22:59:21,535 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #2: ConfigurationPass
2025-07-18T22:59:21,544 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > Set the initialization predicate to Init
2025-07-18T22:59:21,545 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > Set the transition predicate to Next
2025-07-18T22:59:21,634 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #2: ConfigurationPass [OK]
2025-07-18T22:59:21,635 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #3: DesugarerPass
2025-07-18T22:59:21,635 [main] INFO  a.f.a.t.p.p.DesugarerPassImpl -   > Desugaring...
2025-07-18T22:59:22,290 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #3: DesugarerPass [OK]
2025-07-18T22:59:22,291 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #4: InlinePass
2025-07-18T22:59:22,292 [main] INFO  a.f.a.t.p.p.InlinePassImpl - Leaving only relevant operators: CInitPrimed, Init, InitPrimed, Next
2025-07-18T22:59:22,501 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #4: InlinePass [OK]
2025-07-18T22:59:22,502 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #5: TemporalPass
2025-07-18T22:59:22,502 [main] INFO  a.f.a.t.p.p.TemporalPassImpl -   > Rewriting temporal operators...
2025-07-18T22:59:22,502 [main] INFO  a.f.a.t.p.p.TemporalPassImpl -   > No temporal property specified, nothing to encode
2025-07-18T22:59:22,524 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #5: TemporalPass [OK]
2025-07-18T22:59:22,525 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #6: InlinePass
2025-07-18T22:59:22,526 [main] INFO  a.f.a.t.p.p.InlinePassImpl - Leaving only relevant operators: CInitPrimed, Init, InitPrimed, Next
2025-07-18T22:59:22,559 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #6: InlinePass [OK]
2025-07-18T22:59:22,560 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #7: PrimingPass
2025-07-18T22:59:22,567 [main] INFO  a.f.a.t.p.a.PrimingPassImpl -   > Introducing InitPrimed for Init'
2025-07-18T22:59:22,608 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #7: PrimingPass [OK]
2025-07-18T22:59:22,608 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #8: VCGen
2025-07-18T22:59:22,609 [main] INFO  a.f.a.t.b.p.VCGenPassImpl -   > No invariant given. Only deadlocks will be checked
2025-07-18T22:59:22,628 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #8: VCGen [OK]
2025-07-18T22:59:22,629 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #9: PreprocessingPass
2025-07-18T22:59:22,630 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > Before preprocessing: unique renaming
2025-07-18T22:59:22,648 [main] INFO  a.f.a.t.p.p.PreproPassImpl -  > Applying standard transformations:
2025-07-18T22:59:22,649 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > PrimePropagation
2025-07-18T22:59:22,666 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > Desugarer
2025-07-18T22:59:22,694 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > UniqueRenamer
2025-07-18T22:59:22,716 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > Normalizer
2025-07-18T22:59:22,742 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > Keramelizer
2025-07-18T22:59:22,772 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > After preprocessing: UniqueRenamer
2025-07-18T22:59:22,814 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #9: PreprocessingPass [OK]
2025-07-18T22:59:22,815 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #10: TransitionFinderPass
2025-07-18T22:59:22,840 [main] INFO  a.f.a.t.p.a.TransitionPassImpl -   > Found 1 initializing transitions
2025-07-18T22:59:22,850 [main] INFO  a.f.a.t.p.a.TransitionPassImpl -   > Found 2 transitions
2025-07-18T22:59:22,851 [main] INFO  a.f.a.t.p.a.TransitionPassImpl -   > No constant initializer
2025-07-18T22:59:22,853 [main] INFO  a.f.a.t.p.a.TransitionPassImpl -   > Applying unique renaming
2025-07-18T22:59:22,868 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #10: TransitionFinderPass [OK]
2025-07-18T22:59:22,869 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #11: OptimizationPass
2025-07-18T22:59:22,882 [main] INFO  a.f.a.t.p.p.OptPassImpl -  > Applying optimizations:
2025-07-18T22:59:22,884 [main] INFO  a.f.a.t.p.p.OptPassImpl -   > ConstSimplifier
2025-07-18T22:59:22,889 [main] INFO  a.f.a.t.p.p.OptPassImpl -   > ExprOptimizer
2025-07-18T22:59:22,892 [main] INFO  a.f.a.t.p.p.OptPassImpl -   > SetMembershipSimplifier
2025-07-18T22:59:22,893 [main] INFO  a.f.a.t.p.p.OptPassImpl -   > ConstSimplifier
2025-07-18T22:59:22,915 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #11: OptimizationPass [OK]
2025-07-18T22:59:22,915 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #12: AnalysisPass
2025-07-18T22:59:22,923 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -  > Marking skolemizable existentials and sets to be expanded...
2025-07-18T22:59:22,924 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -   > Skolemization
2025-07-18T22:59:22,925 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -   > Expansion
2025-07-18T22:59:22,929 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -   > Remove unused let-in defs
2025-07-18T22:59:22,936 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -  > Running analyzers...
2025-07-18T22:59:22,960 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -   > Introduced expression grades
2025-07-18T22:59:22,960 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #12: AnalysisPass [OK]
2025-07-18T22:59:22,961 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #13: BoundedChecker
2025-07-18T22:59:22,999 [main] DEBUG a.f.a.t.b.s.Z3SolverContext - Creating Z3 solver context 0
2025-07-18T22:59:23,592 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #0, transition #0
2025-07-18T22:59:23,593 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT
2025-07-18T22:59:23,659 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 0: Transition #0. Is it enabled?
2025-07-18T22:59:23,662 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 0: Transition #0 is enabled
2025-07-18T22:59:23,667 [main] INFO  a.f.a.t.b.t.TransitionExecutorImpl - Step 0: picking a transition out of 1 transition(s)
2025-07-18T22:59:23,674 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #1, transition #0
2025-07-18T22:59:23,674 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT
2025-07-18T22:59:23,752 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - Adapted exception intercepted: 
at.forsyte.apalache.tla.bmcmt.RewriterException: Unexpected type a140 when generating a default value
	at at.forsyte.apalache.tla.bmcmt.rules.aux.DefaultValueFactory.makeUpValue(DefaultValueFactory.scala:113)
	at at.forsyte.apalache.tla.bmcmt.rules.aux.RecordAndVariantOps.\$anonfun\$makeVariant\$1(RecordAndVariantOps.scala:100)
	at scala.collection.StrictOptimizedSortedMapOps.map(StrictOptimizedSortedMapOps.scala:30)
	at scala.collection.StrictOptimizedSortedMapOps.map\$(StrictOptimizedSortedMapOps.scala:29)
	at scala.collection.immutable.TreeMap.map(TreeMap.scala:73)
	at at.forsyte.apalache.tla.bmcmt.rules.aux.RecordAndVariantOps.makeVariant(RecordAndVariantOps.scala:96)
	at at.forsyte.apalache.tla.bmcmt.rules.VariantOpsRule.translateVariant(VariantOpsRule.scala:63)
	at at.forsyte.apalache.tla.bmcmt.rules.VariantOpsRule.apply(VariantOpsRule.scala:33)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteOnce(SymbStateRewriterImpl.scala:357)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.doRecursive\$1(SymbStateRewriterImpl.scala:390)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteUntilDone(SymbStateRewriterImpl.scala:424)
	at at.forsyte.apalache.tla.bmcmt.rules.IfThenElseRule.apply(IfThenElseRule.scala:43)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteOnce(SymbStateRewriterImpl.scala:357)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.doRecursive\$1(SymbStateRewriterImpl.scala:390)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteUntilDone(SymbStateRewriterImpl.scala:424)
	at at.forsyte.apalache.tla.bmcmt.rules.LetInRule.apply(LetInRule.scala:27)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteOnce(SymbStateRewriterImpl.scala:357)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.doRecursive\$1(SymbStateRewriterImpl.scala:390)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteUntilDone(SymbStateRewriterImpl.scala:424)
	at at.forsyte.apalache.tla.bmcmt.rules.IfThenElseRule.apply(IfThenElseRule.scala:43)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteOnce(SymbStateRewriterImpl.scala:357)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.doRecursive\$1(SymbStateRewriterImpl.scala:390)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteUntilDone(SymbStateRewriterImpl.scala:424)
	at at.forsyte.apalache.tla.bmcmt.rules.LetInRule.apply(LetInRule.scala:27)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteOnce(SymbStateRewriterImpl.scala:357)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.doRecursive\$1(SymbStateRewriterImpl.scala:390)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteUntilDone(SymbStateRewriterImpl.scala:424)
	at at.forsyte.apalache.tla.bmcmt.rules.VariantOpsRule.translateVariantTag(VariantOpsRule.scala:117)
	at at.forsyte.apalache.tla.bmcmt.rules.VariantOpsRule.apply(VariantOpsRule.scala:40)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteOnce(SymbStateRewriterImpl.scala:357)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.doRecursive\$1(SymbStateRewriterImpl.scala:390)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteUntilDone(SymbStateRewriterImpl.scala:424)
	at at.forsyte.apalache.tla.bmcmt.rules.EqRule.apply(EqRule.scala:47)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteOnce(SymbStateRewriterImpl.scala:357)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.doRecursive\$1(SymbStateRewriterImpl.scala:390)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteUntilDone(SymbStateRewriterImpl.scala:424)
	at at.forsyte.apalache.tla.bmcmt.rules.AndRule.mapArg\$1(AndRule.scala:62)
	at at.forsyte.apalache.tla.bmcmt.rules.AndRule.\$anonfun\$apply\$2(AndRule.scala:66)
	at scala.collection.immutable.List.map(List.scala:247)
	at scala.collection.immutable.List.map(List.scala:79)
	at at.forsyte.apalache.tla.bmcmt.rules.AndRule.apply(AndRule.scala:66)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteOnce(SymbStateRewriterImpl.scala:357)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.doRecursive\$1(SymbStateRewriterImpl.scala:390)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteUntilDone(SymbStateRewriterImpl.scala:424)
	at at.forsyte.apalache.tla.bmcmt.rules.QuantRule.skolemExistsInStaticallyNonEmptySet(QuantRule.scala:268)
	at at.forsyte.apalache.tla.bmcmt.rules.QuantRule.skolemExistsInSet(QuantRule.scala:239)
	at at.forsyte.apalache.tla.bmcmt.rules.QuantRule.apply(QuantRule.scala:50)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteOnce(SymbStateRewriterImpl.scala:357)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.doRecursive\$1(SymbStateRewriterImpl.scala:390)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteUntilDone(SymbStateRewriterImpl.scala:424)
	at at.forsyte.apalache.tla.bmcmt.trex.TransitionExecutorImpl.prepareTransition(TransitionExecutorImpl.scala:107)
	at at.forsyte.apalache.tla.bmcmt.trex.FilteredTransitionExecutor.prepareTransition(FilteredTransitionExecutor.scala:48)
	at at.forsyte.apalache.tla.bmcmt.trex.ConstrainedTransitionExecutor.prepareTransition(ConstrainedTransitionExecutor.scala:98)
	at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.\$anonfun\$prepareTransitionsAndCheckInvariants\$5(SeqModelChecker.scala:217)
	at scala.runtime.java8.JFunction1\$mcVI\$sp.apply(JFunction1\$mcVI\$sp.scala:18)
	at scala.collection.immutable.Range.foreach(Range.scala:190)
	at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.prepareTransitionsAndCheckInvariants(SeqModelChecker.scala:211)
	at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.makeStep(SeqModelChecker.scala:123)
	at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.run(SeqModelChecker.scala:66)
	at at.forsyte.apalache.tla.bmcmt.passes.BoundedCheckerPassImpl.runIncrementalChecker(BoundedCheckerPassImpl.scala:138)
	at at.forsyte.apalache.tla.bmcmt.passes.BoundedCheckerPassImpl.execute(BoundedCheckerPassImpl.scala:91)
	at at.forsyte.apalache.infra.passes.PassChainExecutor\$.exec(PassChainExecutor.scala:64)
	at at.forsyte.apalache.infra.passes.PassChainExecutor\$.\$anonfun\$runPassOnModule\$3(PassChainExecutor.scala:53)
	at scala.util.Either.flatMap(Either.scala:360)
	at at.forsyte.apalache.infra.passes.PassChainExecutor\$.\$anonfun\$runPassOnModule\$1(PassChainExecutor.scala:51)
	at scala.collection.LinearSeqOps.foldLeft(LinearSeq.scala:183)
	at scala.collection.LinearSeqOps.foldLeft\$(LinearSeq.scala:179)
	at scala.collection.immutable.List.foldLeft(List.scala:79)
	at at.forsyte.apalache.infra.passes.PassChainExecutor\$.runOnPasses(PassChainExecutor.scala:44)
	at at.forsyte.apalache.infra.passes.PassChainExecutor\$.run(PassChainExecutor.scala:34)
	at at.forsyte.apalache.tla.tooling.opt.CheckCmd.run(CheckCmd.scala:136)
	at at.forsyte.apalache.tla.Tool\$.runCommand(Tool.scala:139)
	at at.forsyte.apalache.tla.Tool\$.run(Tool.scala:119)
	at at.forsyte.apalache.tla.Tool\$.main(Tool.scala:40)
	at at.forsyte.apalache.tla.Tool.main(Tool.scala)
2025-07-18T22:59:23,756 [main] ERROR a.f.a.t.Tool\$ - <unknown>: rewriter error: Unexpected type a140 when generating a default value
at.forsyte.apalache.infra.AdaptedException: <unknown>: rewriter error: Unexpected type a140 when generating a default value
	at at.forsyte.apalache.infra.passes.PassChainExecutor\$.run(PassChainExecutor.scala:39)
	at at.forsyte.apalache.tla.tooling.opt.CheckCmd.run(CheckCmd.scala:136)
	at at.forsyte.apalache.tla.Tool\$.runCommand(Tool.scala:139)
	at at.forsyte.apalache.tla.Tool\$.run(Tool.scala:119)
	at at.forsyte.apalache.tla.Tool\$.main(Tool.scala:40)
	at at.forsyte.apalache.tla.Tool.main(Tool.scala)
```
</details>

## System information

- Apalache version: `56462d3 build 56462d3` (revision `56462d384d63853ceb503c8eb86a4eff02572529` from `main` branch)
- OS: Ubuntu Linux x86_64 24.04
- JDK version: `21.0.3`

## Triage checklist (for maintainers)



- [ ] Reproduce the bug on the main development branch.
- [ ] Add the issue to the apalache GitHub project.
- [ ] If the bug is high impact, ensure someone available is assigned to fix it.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Uh oh!

OptionCase without caseNone type annotation causes a confusing "Unexpected type" RewriterException #3116

Description

Impact

Input specification

The command line parameters used to run the tool

Expected behavior

Log files

System information

Triage checklist (for maintainers)

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Uh oh!

OptionCase without caseNone type annotation causes a confusing "Unexpected type" RewriterException #3116

Description

Description

Impact

Input specification

The command line parameters used to run the tool

Expected behavior

Log files

System information

Triage checklist (for maintainers)

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions