This module:

module A
let x = List.length

resolves x to just FStar.List.Tot.Base.length, so that's the only module that needs to be loaded.

However the dependency analysis (fstar.exe --dep full A.fst) makes it depend on the full FStar.List module

A.fst.checked: A.fst\
	/home/guido/r/fstar/guido_tactics/bin/../ulib/.cache/FStar.List.fst.checked\
	/home/guido/r/fstar/guido_tactics/bin/../ulib/.cache/FStar.Pervasives.fsti.checked\
	/home/guido/r/fstar/guido_tactics/bin/../ulib/.cache/prims.fst.checked

This seems hard to improve, since we don't have the module parsed nor loaded at the time of the dependency analysis, but at least I'm making a note for it so we can refer to it. (I've just realized myself this was the case.)