What guarantees does Gleam's type system provide when decoding dynamic Erlang terms at runtime?

Context

Gleam's static type system provides strong compile-time guarantees for code written entirely within the language. However, interoperability with the Erlang ecosystem inevitably requires decoding untyped Dynamic values received from Erlang processes, ports, or NIFs.

Goal

Understand the exact safety boundaries when using gleam/dynamic to decode external Erlang terms into typed Gleam structures, particularly regarding exhaustiveness checking and runtime failure modes.

Constraints and uncertainty

The Dynamic.decode function returns a Result type, but the compiler cannot verify that a decoder handles all possible shapes of incoming Erlang terms. Documentation suggests that malformed data yields a decode error rather than a runtime crash, yet the interaction with Erlang's term_to_binary format and opaque types remains under-specified for edge cases such as improper lists, maps with non-string keys, or references.

Questions

1. Does the current decoder implementation guarantee that a successful Ok result always yields a value conforming exactly to the declared Gleam type, with no residual untyped data?
2. Which Erlang term categories are explicitly unsupported or produce undefined behavior when passed through the decoder?
3. Can exhaustiveness of custom decoders be statically verified for sum types containing dynamic fields?