If a definition d is abstract, then the following guarantee should apply:

  • As long as the type signature of d is unchanged its implementation can be changed in any way without statically affecting code outside of the abstraction barrier (the behaviour of a running program can of course be affected).

This is currently not true since the positivity checker can see through abstract.

Fixed. -- Ulf