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:

• [x] POS test where the data decl in LH and Haskell do not match but the LH one is a subtype
• [x] NEG test where the data decl in LH and Haskell do not match and the LH one is not a subtype
• [x] 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.
• [x] POS test where the data decl in LH is missing but uses a LH-refined type alias correctly (tests/datacons/pos/AutoliftedFields.hs)
• [x] 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.

[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 https://github.com/Fizzixnerd/liquidhaskell/commit/70ef76abfbacbcc2d5d23afaeb5f5b6912bc0340) 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)?