Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add trustworthiness pragma #1829

Merged
merged 1 commit into from
Mar 30, 2021
Merged

Add trustworthiness pragma #1829

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions liquid-base/src/Data/Bits.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
{-# LANGUAGE Trustworthy #-}
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I am surprised we need to add the pragma for anything except Prelude. For this and the other modules GHC should just transitively infer. But it looks like that wasn't the case?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

First, I tried to insert pragma only in Prelude but GHC still complained about safe import Data.Bits and safe import Data.Word in the project I was building. It didn't compile until I inserted pragmas in all liquid modules that the project uses.

Should I also file an issue to GHC about not inferring safety?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Uhm, maybe this is actually expected after all? I was just reading the Safe Haskell Inference section in GHC's documentation, and it says:

"[..]In the case where a module is compiled without one of -XSafe, -XTrustworthy or -XUnsafe being used, GHC will try to figure out itself if the module can be considered safe. This safety inference will never mark a module as trustworthy, only as either unsafe or as safe. GHC uses a simple method to determine this for a module M: If M would compile without error under the -XSafe flag, then M is marked as safe. If M would fail to compile under the -XSafe flag, then it is marked as unsafe.[...]"

So perhaps the extra pragmas were necessary, although it's a bit unsatisfactory. I am also noticing that the original base modules have different inferred degree of safety: Data.Bits and Prelude for example are marked Trustworthy, but Data.Word is marked as Safe, so perhaps this has something to do with the chain of pragmas you had to add. Perhaps @kosmikus can shed some extra light here?

module Data.Bits ( module Exports ) where

import "base" Data.Bits as Exports
3 changes: 2 additions & 1 deletion liquid-base/src/Data/Typeable.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
{-# LANGUAGE Trustworthy #-}
module Data.Typeable (module Exports) where

import "base" Data.Typeable as Exports
import "base" Data.Typeable as Exports
1 change: 1 addition & 0 deletions liquid-base/src/Data/Word.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
{-# LANGUAGE Trustworthy #-}
module Data.Word ( module Exports) where

import "base" Data.Word as Exports
1 change: 1 addition & 0 deletions liquid-base/src/Prelude.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
{-# LANGUAGE Trustworthy #-}
module Prelude (module Exports) where

import Data.Foldable
Expand Down
1 change: 1 addition & 0 deletions liquid-bytestring/src/Data/ByteString.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
{-# LANGUAGE Trustworthy #-}
module Data.ByteString ( module Exports ) where

import Data.String
Expand Down
1 change: 1 addition & 0 deletions liquid-bytestring/src/Data/ByteString/Char8.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
{-# LANGUAGE CPP #-}
{-# LANGUAGE Trustworthy #-}
module Data.ByteString.Char8 ( module Exports ) where

import Data.Int
Expand Down