Fix for #1904 autolifting of data fields

[Fizzixnerd]

As discussed in the issue (#1904), this proceeds with Solution B.

I am looking to write more tests for this change, but I'm not quite sure the best way to do so. I was hoping to add the following, and was hoping reviewers might be able to suggest others:

• POS test where the data decl in LH and Haskell do not match but the LH one is a subtype
• NEG test where the data decl in LH and Haskell do not match and the LH one is not a subtype
• POS test where the data decl in LH and Haskell give different names to the fields, but use them in valid ways. I believe this is required for compatibility, and if a change is wanted here it should be done in a separate PR.
• NEG test where the data decl in LH and Haskell give different names to the fields, but use them in non-valid ways, such as comparing their results (??). Not sure this is really necessary, and might conflict with the following one.
• POS test where the data decl in LH is missing but uses a LH-refined type alias correctly (tests/datacons/pos/AutoliftedFields.hs)
• NEG test where the data decl in LH is missing and uses a LH-refined type alias incorrectly (tests/datacons/neg/AutoliftedFields.hs)

[Fizzixnerd]

I have added more tests. The second test in the checklist fails, and I'm not sure why. LH doesn't declare it unsafe, it seems to just issue an error, so the test is "correct", but not outputting what the test harness expects. Not sure how to deal with this. Additionally, the third test has been added but does not pass. I will wait until I get confirmation that it should before I start work on it, however.

[facundominguez]

Looks pretty good!

It surprises me a bit that all that was needed was to generate the appropriate selector names.

There is one test that looks amiss though (tests/datacon/neg/AutoliftedFields00.hs).

[facundominguez]

If x is a Nat, as the type of getT says, shouldn't this function be accepted by LH?
If I try the following program, supposedly equivalent to this test, LH accepts it.

{-@ LIQUID "--exact-data-cons" @-}
module AutoliftedFields00 where

{-@ type Nat = { v : Int | v >= 0 } @-}
type Nat = Int

{-@ data T = T { getT :: Nat } @-}
data T = T { getT :: Nat }

{-@ f :: { t : T | getT t <= 0 } -> Nat @-}
f :: T -> Nat
f (T x) = x

[Fizzixnerd]

I can confirm your program is accepted while the one I wrote is not... though I'm not sure why!

I do not understand fully why the one with the explicit data decl is accepted. My understanding is that if getT :: Nat and getT t <= 0 then the only available value for the function to return is when x == 0. I suppose that subtypes Nat, and that's why it's accepted, since there is no "true" (in the HM sense) refinement type for anything?

Then it must be that Nat is being used as Int in the no decl case... No, I still don't understand. Since, getT t <= 0 would imply x <= 0 which subtypes Int, just like in the above case! I will investigate further.

[facundominguez]

I understand it this way. LH needs to prove that f returns a Nat, since that is what the specification says. There are two hypothesis to accomplish this

1. the returned x is a Nat because t = T x (inferred from the pattern matching), and T :: Nat -> T.
2. x = getT t && getT t <= 0

So LH completes the proof using hypothesis (1).

[Fizzixnerd]

I can confirm that the reason is that the fields are being inferred to have (refinement) type GHC.Types.Int instead of AutoliftedFields00.Nat. With the specification, the type is correctly Nat. @nikivazou, do you happen to have an idea of why this would be? I'm vaguely aware of expansion being done using the Expand typeclass, and I suspect it's being done too early on for fields/data decls, so that the alias is being expanded before LH has a chance to see it and know that it should use the corresponding LH alias. However, the details are much more complicated than what I've been able to figure out myself. For example, I don't know when the type for the field is first grabbed from GHC; if you knew this or could point me in the right direction it would be greatly appreciated!

[facundominguez]

I would have expected naming a field differently in the specification to be an error. Shouldn't it fail?

[Fizzixnerd]

I have tried many times to get this to work, but I can't seem to. I thought I was close at one point, but I can't seem to close the deal! Was wondering if @nikivazou had any hints?

Consider the following LH program, where I have double-primed Nat just so that it doesn't get confused with the Nat in the liquid-prelude, since I was messing around with qualification and expansion.

{-@ LIQUID "--exact-data-cons" @-}

-- data decl in LH is missing but uses a LH-refined type alias correctly

module AutoliftedFields000 where

{-@ type Nat'' = { v : Int | v >= 0 } @-}
type Nat'' = Int

data T = T { getT :: Nat'' }

f :: Int -> Nat''
f = getT . T

g :: Int -> Nat''
g z = getT (T z)

x :: T
x = T 0

y :: Nat''
y = getT x

We would like this program to fail with errors about f and g. If we add a {-@ data T ... -@} declaration, this indeed occurs. However, when I generate the field names as already done in this PR, there is an issue: the fields have their type synonyms expanded before they are analyzed by Liquid. That is, the above program is deemed safe by LH, because Nat'' is interpreted as an Int in the field declaration, instead of the refined type synonym.

With some effort, I was able to disable this early expansion, but then of course we fail with sort errors because Nat'' doesn't unify with int. See https://github.com/Fizzixnerd/liquidhaskell/tree/expansion-experiments (or Fizzixnerd@70ef76a) for a dirty look at the changes I attempted. The idea is to use the RTEnv to expand later in the pipeline, with qualifyExpand and this is done by defining a ofTypeNoExpand function that defers the alias expansion until later.

Right now I am able to defer expansion, but I can't manage to actually execute it later.

[Fizzixnerd]

I have converted to a draft until I can wrap my head around this better, and will be working on other simpler issues.

[nikivazou]

Sorry!!! I totally miss that :(
Let's have a call to discuss after ICFP deadline (week of March 7)?