Inferred types cause unsoundness in the importing module (leaking False)?

[julbinb]

[This is for 9.10.1; I haven't checked earlier versions]

When I am trying to use type inference for top-level functions exported from the module, it seems that LH infers False/bottom that leaks into the importing module and makes all the checks pass.

Here is an example:

Lib.hs

{-# OPTIONS_GHC -fplugin=LiquidHaskell #-}

module Lib where

{-@ c5 :: {v:Int | _} @-}
c5 :: Int
c5 = 5

Main.hs

{-# OPTIONS_GHC -fplugin=LiquidHaskell #-}

module Main where

import Lib

{-@ c7 :: {v:Int | v==7} @-}
c7 :: Int
c7 = 5

main :: IO ()
main = putStrLn "Hello, Haskell!"

The compiler says

[1 of 2] Compiling Lib
**** LIQUID: SAFE (0 constraints checked) **************************************
[2 of 2] Compiling Main
**** LIQUID: SAFE (1 constraints checked) **************************************

If I remove the inference annotation on c5, then I get an error for c7 in Main as expected.

Another option is to use a function instead of a constant, e.g. in Lib.hs, write

{-@ ispos :: x:Int -> {v:Bool | _} @-}
ispos :: Int -> Bool
ispos x = x > 0

and then modify c7 in Main.hs like this:

c7 = if ispos 0 then 5 else 5

Note that if ispos is not called, then I do get an error. That's why I suspect that it is a call ispos 0 that introduces some kind of False into the context, whereas with c5, such a False is already in the context.

And I'd guess that False gets inferred because there are no use sites of c5 and ispos within Lib.hs.

But! When I hover over types of c5 and ispos in the produced HTML file, they are just Int and Int -> Bool. I don't see any False... I am puzzled :)

UPD Replacing the hole in c5 with an explicit False causes a compilation error

    The inferred type
      VV : {v : GHC.Types.Int | v == (5 : int)}
    .
    is not a subtype of the required type
      VV : {VV##361 : GHC.Types.Int | GHC.Types.False}

[ranjitjhala]

Ugh. I have a feeling this bug is because

1. We are not supposed to have _ in public signatures,
2. If you do have a _ then the thing that gets imported has an "unconstrained" $k-var which
3. In the client's context is treated as False.

IMO, the fix is to handle _ in public functions by either

• rejecting them wholesale, or
• replacing the relevant $k-vars with True

In both the c5 and the isPos case, the $k-vars corresponding to the holes are getting solved to False by fixpoint because the relevant constraints are getting "sliced away" since the $k-vars are "dead" (i.e. don't appear in any LHS), i.e. the constraints for the Lib file are trivially satisfied regardless of what the $k is solved to.

So we really need to either reject or replace-with-true.

[julbinb]

I don't know much about a typical workflow of a Haskell/LH programmer, but assuming that people start working on modules with everything exported by default, rejecting all the _ could be rather annoying during the development.

If resolving to True essentially produces the same result as exporting a bare Haskell signature, that seems like a reasonable solution.

Also, is there a reason to keep a $k-variable at all once the module is type checked? If I understood your comment correctly, we do not literally get False in the c5 signature. Feels like when all the work on a module is done, there should be no intermediate things left.

[ranjitjhala]

You make a very good point -- maybe defaulting to True for those holes is better (I just worry that if that is done "silently" that may be a bit confusing too?)

TBH I cannot recall if the $k-variable is actually kept, I suspect its replaced with the "solution" False but I'll have to check! (I totally agree that there should be no intermediate things left.)

[julbinb]

I agree that everything silent may be confusing. A warning for exported functions with inferred (and True-adjusted) types? Being user-friendly is hard :)