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

Fix for #1904 autolifting of data fields #1921

Draft
wants to merge 6 commits into
base: develop
Choose a base branch
from
Draft

Fix for #1904 autolifting of data fields #1921

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
9f2076b
Fix for #1904 autolifting of data fields
Fizzixnerd Jan 6, 2022
8aaceac
Add negative test for #1904
Fizzixnerd Jan 6, 2022
943cc45
More tests for #1904
Fizzixnerd Jan 6, 2022
d737a26
Simplify AutoliftedFields02.hs
Fizzixnerd Jan 6, 2022
3500cd9
working on fix for #1904 decls having wrong inferred LH type
Fizzixnerd Jan 17, 2022
8a84fd2
Remove bad test from other branch
Fizzixnerd Jan 17, 2022
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
6 changes: 3 additions & 3 deletions src/Language/Haskell/Liquid/Bare.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -266,7 +266,7 @@ makeGhcSpec0 cfg src lmap mspecsNoCls = do
, _gsLSpec = finalLiftedSpec
{ impSigs = makeImports mspecs
, expSigs = [ (F.symbol v, F.sr_sort $ Bare.varSortedReft embs v) | v <- gsReflects refl ]
, dataDecls = dataDecls mySpec2
, dataDecls = dataDecls mySpec2
, measures = Ms.measures mySpec
-- We want to export measures in a 'LiftedSpec', especially if they are
-- required to check termination of some 'liftedSigs' we export. Due to the fact
Expand Down Expand Up @@ -752,7 +752,7 @@ makeInlSigs env rtEnv

makeMsrSigs :: Bare.Env -> BareRTEnv -> [(ModName, Ms.BareSpec)] -> [(Ghc.Var, LocSpecType)]
makeMsrSigs env rtEnv
= makeLiftedSigs rtEnv (CoreToLogic.inlineSpecType (typeclass (getConfig env)))
= makeLiftedSigs rtEnv (CoreToLogic.measureSpecType (typeclass (getConfig env)))
. makeFromSet "hmeas" Ms.hmeas env

makeLiftedSigs :: BareRTEnv -> (Ghc.Var -> SpecType) -> [Ghc.Var] -> [(Ghc.Var, LocSpecType)]
Expand Down Expand Up @@ -1172,7 +1172,7 @@ makeLiftedSpec name src _env refl sData sig qual myRTE lSpec0 = lSpec0
, isLocInFile srcF t
]
, Ms.axeqs = gsMyAxioms refl
, Ms.aliases = F.notracepp "MY-ALIASES" $ M.elems . typeAliases $ myRTE
, Ms.aliases = F.tracepp "MY-ALIASES" $ M.elems . typeAliases $ myRTE
, Ms.ealiases = M.elems . exprAliases $ myRTE
, Ms.qualifiers = filter (isLocInFile srcF) (gsQualifiers qual)
}
Expand Down
14 changes: 9 additions & 5 deletions src/Language/Haskell/Liquid/Bare/DataType.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -73,11 +73,15 @@ makeDataConChecker = F.testSymbol . F.symbol
-- equivalent to `head` and `tail`.
--------------------------------------------------------------------------------
makeDataConSelector :: Maybe Bare.DataConMap -> Ghc.DataCon -> Int -> F.Symbol
makeDataConSelector dmMb d i = M.lookupDefault def (F.symbol d, i) dm
where
dm = Mb.fromMaybe M.empty dmMb
makeDataConSelector dmMb d i
| Just ithField <- ithFieldMb = F.symbol (Ghc.flSelector ithField)
| otherwise = M.lookupDefault def (F.symbol d, i) dm
where
fields = Ghc.dataConFieldLabels d
ithFieldMb = Misc.getNth (i - 1) fields
dm = Mb.fromMaybe M.empty dmMb
def = makeDataConSelector' d i


makeDataConSelector' :: Ghc.DataCon -> Int -> F.Symbol
makeDataConSelector' d i
Expand Down Expand Up @@ -336,7 +340,7 @@ fieldName d dp x

makeDataFields :: F.TCEmb Ghc.TyCon -> F.FTycon -> [RTyVar] -> [(F.LocSymbol, SpecType)]
-> [F.DataField]
makeDataFields tce _c as xts = [ F.DField x (fSort t) | (x, t) <- xts]
makeDataFields tce _c as xts = F.tracepp "dfields" [ F.DField x (fSort t) | (x, t) <- F.tracepp "xts" xts]
where
su = zip (F.symbol <$> as) [0..]
fSort = F.substVars su . F.mapFVar (+ (length as)) . RT.rTypeSort tce
Expand Down
2 changes: 1 addition & 1 deletion src/Language/Haskell/Liquid/Bare/Expand.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -327,7 +327,7 @@ instance Expand Body where
instance Expand DataCtor where
expand rtEnv l c = c
{ dcTheta = expand rtEnv l (dcTheta c)
, dcFields = [(x, expand rtEnv l t) | (x, t) <- dcFields c ]
, dcFields = F.tracepp "dcFields: postexpand" [(x, expand rtEnv l t) | (x, t) <- F.tracepp "dcFields: preexpand" $ dcFields c ]
, dcResult = expand rtEnv l (dcResult c)
}

Expand Down
14 changes: 14 additions & 0 deletions tests/datacon/neg/AutoliftedFields00.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
{-@ LIQUID "--exact-data-cons" @-}

-- data decl in LH is missing and uses a LH-refined type alias incorrectly

module AutoliftedFields00 where

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

data T = T { getT :: Nat }

{-@ f :: T -> { v : Int | v < 0 } @-}
f :: T -> Nat
f (T x) = x
Copy link
Collaborator

@facundominguez facundominguez Jan 10, 2022 •
edited
Loading

Choose a reason for hiding this comment

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

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

Copy link
Contributor Author

Choose a reason for hiding this comment

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

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.

Copy link
Collaborator

@facundominguez facundominguez Jan 11, 2022 •
edited
Loading

Choose a reason for hiding this comment

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

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).

Copy link
Contributor Author

Choose a reason for hiding this comment

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

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!

15 changes: 15 additions & 0 deletions tests/datacon/neg/AutoliftedFields01.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
{-@ LIQUID "--exact-data-cons" @-}

-- data decl in LH and Haskell do not match and the LH one is not a subtype

module AutoliftedFields01 where

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

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

{-@ f :: { t : T | getT t >= 1 } -> Nat @-}
f :: T -> Nat
f (T x) = x
14 changes: 14 additions & 0 deletions tests/datacon/pos/AutoliftedFields00.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
{-@ LIQUID "--exact-data-cons" @-}

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

module AutoliftedFields00 where

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

data T = T { getT :: Nat }

{-@ f :: T -> Nat @-}
f :: T -> Nat
f (T x) = x
16 changes: 16 additions & 0 deletions tests/datacon/pos/AutoliftedFields01.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
{-@ LIQUID "--exact-data-cons" @-}

-- data decl in LH and Haskell give different names to the fields, but use them
-- in valid ways.

module AutoliftedFields01 where

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

{-@ data T = T { getMyT :: Nat } @-}
data T = T { getT :: Nat }
Copy link
Collaborator

Choose a reason for hiding this comment

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

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


{-@ f :: { t : T | getT t == getMyT t } -> Nat @-}
f :: T -> Nat
f (T x) = x
15 changes: 15 additions & 0 deletions tests/datacon/pos/AutoliftedFields02.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
{-@ LIQUID "--exact-data-cons" @-}

-- data decl in LH and Haskell do not match but the LH is a subtype

module AutoliftedFields02 where

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

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

{-@ f :: T -> Nat @-}
f :: T -> Nat
f (T x) = x