search

ucsd-progsys / liquidhaskell

Liquid Types For Haskell
BSD 3-Clause "New" or "Revised" License
1.2k stars 139 forks source link

Positivity checking runs on reexports? #2382

Open gergoerdi opened 1 month ago

gergoerdi commented 1 month ago

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 commented 1 month ago

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 commented 1 month ago

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.