When to use opaque types from Dialyzer?

Background

I have my app divided in separate layers. Layers from above are able to talk to layers bellow and to answer to layers above them, a normal layered architecture:

Now, each layer has a public interface, a unique point of entry.
This public API uses dialyzer to define some specs and types.

Problem

I don’t want the above layers to see the internals of the types I define in other layers. This way if I change the implementation details of layer 3, layer 2 wont care because layer 2 is not dependent on the internal structure of layer 3.

To achieve this I think opaque types could be the answer:

Questions

However, it says that opaque types are problematic and shouldn’t really be used because they are buggy.
This brings 2 questions:

  1. Have opaque types been improved since the author has written that article? (as in, are they still somewhat buggy, or are they no longer buggy)?
  2. If opaque types are still buggy, in what situations do they work as expected? What use cases are known to work properly?

The question bothers me, too and I would like to know if there is an answer.

The article already provides a possible solution. Also I haven’t experienced any issue by using opaque types. So either it’s solved or it’s less buggy than it seems to be implicated.

Afaik, dialzyer still suffers from the same problems. Quoting the article:

Sometimes the implementation of opaque data types is either not strong enough to do what it should or is actually problematic (i.e. buggy). Dialyzer does not take the spec of a function into account until it has first inferred the success typing for the function.

To this end, I have started exploring other options to dialyzer, namely Gradient.
However, this tool also has its fair share of issues, and its still being worked on.