KaRaMeL extraction: type alias not normalized in alloc, causes subtype mismatch

## Summary

When extracting Pulse code to C via `--codegen krml`, F* emits a type alias (e.g., `ASpec_mybyte`) for the array element type in `alloc` but emits the concrete base type (`uint8_t`) for the initializer literal. KaRaMeL sees these as mismatched types and drops the function with Warning 4.

## Minimal reproducer

**`ASpec.fst`** — defines a type alias:
```fstar
module ASpec
type mybyte = FStar.UInt8.t
```

**`ABuf.fsti`** — interface using the alias:
```fstar
module ABuf
open Pulse.Lib.Pervasives
open Pulse.Lib.Vec
open FStar.SizeT
module SZ = FStar.SizeT

noeq type my_buf = { data: Pulse.Lib.Box.box (vec ASpec.mybyte); len: SZ.t }

val create (n: SZ.t{SZ.v n > 0})
: stt my_buf emp (fun _ -> emp)
```

**`ABuf.fst`** — implementation:
```fstar
module ABuf
#lang-pulse
open Pulse.Lib.Pervasives
open Pulse.Lib.Vec
open FStar.SizeT
module SZ = FStar.SizeT
module B = Pulse.Lib.Box
open Pulse.Lib.Box { box, (:=), (!) }

fn create (n: SZ.t{SZ.v n > 0})
requires emp
returns s : my_buf
ensures emp
{
let v : vec ASpec.mybyte = alloc #ASpec.mybyte 0uy n;
let b = B.alloc #(vec ASpec.mybyte) v;
admit();
{ data = b; len = n }
}
```

**`Wrap.fst`** — wrapper (no `.fsti`) to make function public in krml:
```fstar
module Wrap
#lang-pulse
open Pulse.Lib.Pervasives
open FStar.SizeT
module SZ = FStar.SizeT

fn wrap_create (n: SZ.t{SZ.v n > 0})
requires emp
returns s : ABuf.my_buf
ensures emp
{ ABuf.create n }
```

## Steps to reproduce

```bash
PULSE_ROOT=~/pulse

# Extract all modules to krml
for mod in ASpec ABuf Wrap; do
fstar.exe ${mod}.fst \
--include $PULSE_ROOT/out/lib/pulse \
--include $PULSE_ROOT/out/lib/pulse/lib \
--cache_checked_modules --cache_dir _cache --odir _output \
--already_cached 'Prims,FStar,Pulse.Nolib,Pulse.Lib,Pulse.Class,PulseCore' \
--warn_error -321 --ext optimize_let_vc \
--codegen krml --extract_module $mod
done

# Bundle WITHOUT ASpec.krml → ABuf.create is DROPPED
krml -skip-compilation -skip-makefiles -skip-linking \
-bundle 'Wrap=Wrap,ABuf' -tmpdir _c_bug \
_output/Wrap.krml _output/ABuf.krml
```

## Observed behavior

```
Cannot re-check ABuf.create as valid Low* and will not extract it.

Warning 4: in the definition of v, in top-level declaration ABuf.create, in file Wrap:
Malformed input:
subtype mismatch:
uint8_t (a.k.a. uint8_t) vs:
ASpec_mybyte (a.k.a. ASpec_mybyte)
```

`ABuf.create` is silently dropped from the C output.

## Root cause

In the krml AST for `ABuf.create`, the `alloc` call has:
- **Buffer element type**: `ASpec_mybyte` (unresolved alias)
- **Initializer literal**: `0uint8_t` (concrete type)

KaRaMeL's monomorphization sees `ASpec_mybyte` ≠ `uint8_t` and rejects the function.

## Workaround

Include the type-defining module's krml in the bundle:
```bash
krml -bundle 'Wrap=Wrap,ABuf,ASpec' _output/*.krml # works
```

## Expected behavior

F*'s `--codegen krml` should normalize type aliases to their base types in the krml output, so that `alloc #ASpec.mybyte 0uy n` produces consistent types for both the buffer element type and the initializer. This would eliminate the dependency on having the type-alias-defining module's krml present.

## Versions

- F* 2025.12.15~dev
- KaRaMeL d6607b99
- Pulse: current main

Use ASpec.fst, ABuf.fsti, ABuf.fst, and Wrap.fst to reproduce the issue with F* --codegen krml and the shown krml bundle command. Trace how the krml AST represents the alloc element type and initializer; done means the generated types are consistent and ABuf.create is retained without bundling ASpec.krml.

Written by the indexing model from the issue text.