Positivity checking runs on reexports?

[gergoerdi]

With the classic non-positive type definition:

{-@ LIQUID "--no-positivity-check" @-}
module Debug.Liquid.PositivityChecker.Mod where

data Neg = MkNeg (Neg -> ())

I was surprised that the following module then ALSO fails the positivity checker:

module Debug.Liquid.PositivityChecker.Use (module M) where

import Debug.Liquid.PositivityChecker.Mod as M

This fails with (note the missing source location):

Source error while processing module Debug.Liquid.PositivityChecker.Use:
  <no location info>: error:
      Negative occurence of Debug.Liquid.PositivityChecker.Mod.Neg in Debug.Liquid.PositivityChecker.Mod.MkNeg : (Debug.Liquid.PositivityChecker.Mod.Neg -> ())
%1 -> Debug.Liquid.PositivityChecker.Mod.Neg


To deactivate or understand the need of positivity check, see:
  https://ucsd-progsys.github.io/liquidhaskell/options/#positivity-check

Is this intentional?

(As a side note, I love "to deactivate or understand" in a warning message 😆)

[nikivazou]

To me, it makes sense that you need the non-positivity check also in the modules that import and use the non-positive data.
But I am not opposed to, by default, deactivate it, if you think it is unreasonable.

[gergoerdi]

To me, it makes sense that you need the non-positivity check also in the modules that import and use the non-positive data. But I am not opposed to, by default, deactivate it, if you think it is unreasonable.

Hmm OK, so it is intentional. But then this leads to the question of is it possible to turn off positivity checking for a single datatype definition? Otherwise, the flag becomes very "infectious" on other modules.