[erlang-questions] I'm impressed, but how on earth did Dialyzer figure this out?

[Yestin L Harrison]

Right, so, I have a module with a big important central function that takes a
proplist of options, and I have a product type annotated representing valid
options, opt(). Then, I've got:

-type opts() :: [opt()].

I've got functions:

-spec default_options() -> opts().
%% you can imagine what this looks like

-spec options(opts()) -> opts().
options(Options) ->
	Default = maps:from_list(proplists:unfold(default_options())),
	New = maps:from_list(proplists:unfold(Options)),
	proplists:compact(maps:to_list(maps:merge(Default, New))).

I run Dialyzer on my project, and... this typechecks just fine?

It was my understanding that Dialyzer spits errors on a potential violation of
stated success typing, and I figured that after going through all the
functions in the maps and proplists module, that static analysis would only
be able to determine that the output of maps:to_list/1 would be
{term(), term()}? Or am I not giving Dialyzer enough credit? Is this what the
PLT is for, statically stepping through the modules it contains?

Really, in any case,
a) This is amazing,
b) I would love any resources anyone is aware of on the workings of Dialyzer,
   besides the obvious look through the source code, which I might attempt
   after getting a bit of a better feel for what it does.