Adding refinements to a module can break encapsulation

[rosekunkel]

Suppose I have the following modules:

Foo.hs

module Foo ( Foo(..) ) where

data Foo = A | B

FooInterface.hs

module FooInterface ( createFoo, useFoo ) where

import Foo

createFoo :: Foo
createFoo = A

useFoo :: Foo -> ()
useFoo A = ()

Example.hs

module Example where

import FooInterface

example = useFoo createFoo

The intention with these modules is that consumers of the Foo library can only create and use Foos via the corresponding functions in FooInterface. However, I want to use Liquid Haskell to check that this code is correct. In particular, I want to make useFoo into a total function. I can add these annotations:

Foo.hs

module Foo ( Foo(..), isA ) where

data Foo = A | B

{-@ measure isA @-}
isA :: Foo -> Bool
isA A = True
isA _ = False

FooInterface.hs

module FooInterface ( createFoo, useFoo ) where

import Foo

{-@ createFoo :: {v:Foo | isA v} @-}
createFoo :: Foo
createFoo = A

{-@ useFoo :: {v:Foo | isA v} -> () @-}
useFoo :: Foo -> ()
useFoo A = ()

But now running Liquid Haskell on Example.hs will give the following error:

Error: GHC Error

 5 | {-@ measure isA @-}
                 ^

     Not in scope: variable or data constructor 'isA'

To fix this, I have to modify Example.hs to import Foo:

module Example where

import FooInterface
import Foo

example = useFoo createFoo

This is undesirable: it means that you have to expose the implementation details of your library to the user. Ideally, Liquid Haskell would be able to verify that this code is correct without needing isA to be in scope, in the same way that GHC can verify that this code is type-correct even though the type Foo is not in scope.

[ranjitjhala]

This is related to another similar module re-export issue.

Unfortunately its totally unclear how to to address this.

The error gets thrown because we "eagerly" try to Resolve the name isFoo which is in the signature of FooInterface but which is itself not exported by FooInterface.

If infact, we want to preserve encapsulation, we probably need some notion of "internal" (private) vs. "external" (public) signatures for FooInterface where I'm guessing the former should be a sub-type of the latter.

Looks like an interesting research question!