Elixir / Erlang Dialyzer : Why behaviour callback&

Question

I have a behaviour X and a callback function with parameter type:

%{a: any}

Module Y implements behaviour X and the callback function in implementing module Y has parameter type:

%{a: any, b: any}

Dialyzer doesn't like that and complains:

(#{'a':=_, 'b':=_, _=>_}) 
is not a supertype of 
#{'a':=_}

This implies dialyzer attempts to determine if callback parameter's type in implementing module Y is a supertype of param type in behaviour X. In other words, it asks:

Is behaviour X's callback param type %{a: any} a subtype of implementing module Y's param type %{a: any, b: any}?

Why does dialyzer expect behaviour callback's param type to be a subtype instead of a supertype?

In the context of programming language type theory, subtype is defined as:

type S is a subtype of a type T, written S <: T, if an expression of type S can be used in any context that expects an element of type T. Another way of putting this is that any expression of type S can masquerade as an expression of type T.

In light of the definition above, it makes sense to me if parameter type of behaviour callback is T and that of implementing module is S. Because implementing module still keeps the behaviour contract. However, I'm clueless as to why dialyzer expects the other way around.

Please help me understand this.

Note: This question is a follow-up but independent of another SO question Erlang (Elixir) Dialyzer - confusing supertype error.

Answer 1

Dialyzer is correct. If there is a behaviour X with a callback of type %{a: any}, the user should be able to call that function of any module that claims to implement this behaviour with e.g. %{a: 1}. Your module's function takes %{a: any, b: any} which is a subtype of %{a: any}, which means that function cannot be called with %{a: 1} anymore which does not comply with the behaviour.

On the other hand, if the behaviour's callback had the type %{a: any, b: any} and your module's function had the type %{a: any}, that would have been fine because %{a: any} is a supertype of %{a: any, b: any} and your module can be called with %{a: 1, b: 2} -- it can just ignore the extra field.