ucsd-progsys / liquidhaskell

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

Liquid Haskell is not safe wrt Safe Haskell #1827

Open oquechy opened 3 years ago

oquechy commented 3 years ago

Safe Haskell transitively infers safety of Haskell modules. It checks for usages of dangerous functions like unsafePerformIO. The safety of a module and its exported functions can be overridden with pragmas such as {-# LANGUAGE Trustworthy #-} which tells to count the module as safe despite usages of unsafe code.

Modules from liquid-base have different safety properties than modules from base. This makes it harder to transition from base to liquid-base for projects that care about safety. For example, safe import Prelude in such projects doesn't work with liquid Prelude while it works with Prelude from base. Then, the modules that import liquid Prelude without safe import can't be annotated with {-# LANGUAGE Safe #-}.

For comparison:

Possible fixes:

kosmikus commented 3 years ago

After discussion, we currently think that we should be able to fix most of the problems by just marking Prelude from liquid-base as Trustworthy. This one is getting inferred as None because it imports GHC.Exts (but doesn't re-export anything from it). Because Prelude from liquid-base is then imported implicitly by nearly every other module, everything is None. But with Prelude being marked Trustworthy, safety inference should be doing the right thing for most modules in the liquid-* package ecosystem.