Internal error "Impossible: cycle detected after cycle detection has passed" when a pointer typedef is declared before its struct

Filing this as the error message requests:

```
Unexpected error: Failure("Impossible: cycle detected after cycle detection has passed")
Please file a bug report, ideally with a minimized version of the source program that triggered the error.
```

**Versions:** PAL `a9ebbed` · F\*/Pulse nightly `2026-08-27` · Clang 20.1.8

## Minimal repro

Translation succeeds with no errors; the failure happens when F\* loads the generated modules.

```c
#include "pal.h"

/* A. inline self-reference, no pointer typedef. VERIFIES */
typedef struct a_t {
int tag;
struct a_t *next;
} a_t;

int fa(a_t *p) { return p->tag; }

/* B. pointer typedef declared BEFORE the struct, used as the field type. FAILS */
typedef struct b_t *bptr;
typedef struct b_t {
int tag;
bptr next;
} b_t;

int fb(bptr p) { return p->tag; }

/* C. pointer typedef declared AFTER the struct. VERIFIES */
typedef struct c_t {
int tag;
struct c_t *next;
} c_t;
typedef c_t *cptr;

int fc(cptr p) { return p->tag; }
```

```
$ pal --outdir out repro.c # no errors
$ run-fstar.sh --include out out/Func_fa.fst # Verified module: Func_fa
$ run-fstar.sh --include out out/Func_fb.fst
Unexpected error: Failure("Impossible: cycle detected after cycle detection has passed")
$ run-fstar.sh --include out out/Func_fc.fst # Verified module: Func_fc
```

## What the controls isolate

The three cases differ only in *how* the self-reference is spelled, and each function body is a single field read — no arrays, no loops, no annotations.

| case | shape | result |
|---|---|---|
| `fa` | inline `struct a_t *next` | verifies |
| **`fb`** | **pointer typedef declared *before* the struct, used as the field type** | **internal error** |
| `fc` | pointer typedef declared *after* the struct | verifies |

So it is not self-reference as such — it is specifically the forward-declared pointer typedef, which is the standard C idiom for a self-referential type.

## Impact

We are using PAL to prove spatial memory safety (every array access in bounds) on the Olden and Ptrdist benchmark suites, holding the C source fixed and adding only annotations.

On `olden/bh` (Barnes-Hut) this blocks **70 of 73** array-bounds obligations. `bh` is built on `bodyptr`/`nodeptr`/`cellptr`/`treeptr`, all declared with this idiom, so nearly every bound-bearing function hits the error before any annotation is evaluated:

| function | bounds obligations blocked |
|---|---:|
| `old_main` | 16 |
| `intcoord` | 15 |
| `subindex` | 13 |
| `ic_test` | 9 |
| `intcoord1` | 6 |
| `expandbox` | 4 |
| `hackcofm` | 3 |
| `stepsystem`, `computegrav`, `maketree`, `walksub` | 1 each |

None of those obligations is otherwise difficult — the `intcoord`/`subindex`/`intcoord1`/`ic_test` cluster is ordinary fixed-size coordinate math over `real[NDIM]`, which a counted-loop invariant handles directly. The one function in `bh` we could prove is precisely the one whose type footprint avoids these structs.

## Notes

- No workaround is available from the annotation side: the failure occurs during module loading, before any user annotation is consulted.
- Possibly related to #77 (*Recursive structures*, closed) — this may be a regression, or a distinct path through the same machinery.
- We hit a second, different problem on a similar shape (a self-referential struct with an `_array` field of pointers to itself produces an unqualified type name). Filing that separately, since it presents differently and needs an `_array` field to trigger.

Happy to test a fix against the benchmark suite.

Start with the minimal repro and compare the generated modules for cases `fa`, `fb`, and `fc`; translation succeeds, but loading `out/Func_fb.fst` fails during F* verification. Trace the cycle-detection path involved in the forward-declared pointer typedef and verify the fix by rerunning the three `pal` and `run-fstar.sh` commands, including the Olden `bh` benchmark if available.

Written by the indexing model from the issue text.