From 24b415d4a42de42f40fa10fbdbd83d7d443eb07f Mon Sep 17 00:00:00 2001 From: Alessio Ferrarini Date: Fri, 10 Jan 2025 11:15:37 +0100 Subject: [PATCH 1/8] Allow only safe refinements of data constructors --- .../Haskell/Liquid/ProofCombinators.hs | 4 ++- .../src/Language/Haskell/Liquid/Bare/Check.hs | 27 +++++++++++++++++++ .../Language/Haskell/Liquid/Types/Errors.hs | 10 +++++++ .../cse230/src/Week10/ProofCombinators.hs | 4 ++- tests/neg/RefCtor.hs | 14 ++++++++++ tests/pos/CountMonad.hs | 2 -- tests/tests.cabal | 1 + 7 files changed, 58 insertions(+), 4 deletions(-) create mode 100644 tests/neg/RefCtor.hs diff --git a/liquid-prelude/src/Language/Haskell/Liquid/ProofCombinators.hs b/liquid-prelude/src/Language/Haskell/Liquid/ProofCombinators.hs index 9faf8d6147..a3e0b9edd5 100644 --- a/liquid-prelude/src/Language/Haskell/Liquid/ProofCombinators.hs +++ b/liquid-prelude/src/Language/Haskell/Liquid/ProofCombinators.hs @@ -76,7 +76,9 @@ _ *** _ = () data QED = Admit | QED {-@ measure isAdmit :: QED -> Bool @-} -{-@ Admit :: {v:QED | isAdmit v } @-} +isAdmit :: QED -> Bool +isAdmit Admit = True +isAdmit QED = False ------------------------------------------------------------------------------- diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Check.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Check.hs index 93e80a3a0d..b319a5992a 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Check.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Check.hs @@ -173,6 +173,7 @@ checkTargetSpec specs src env cbs tsp <> checkSizeFun emb env (gsTconsP (gsName tsp)) <> checkPlugged (catMaybes [ fmap (F.dropSym 2 $ GM.simplesymbol x,) (getMethodType t) | (x, t) <- gsMethods (gsSig tsp) ]) <> checkRewrites tsp + <> checkConstructorRefinement (gsTySigs $ gsSig tsp) _rClasses = concatMap Ms.classes specs _rInsts = concatMap Ms.rinstance specs @@ -193,6 +194,32 @@ checkTargetSpec specs src env cbs tsp +checkConstructorRefinement :: [(Var, LocSpecType)] -> Diagnostics +checkConstructorRefinement = mconcat . map checkOne + where + checkOne (s, ty) | isCtorName s + , not $ validRef $ getRetTyRef $ val ty + = mkDiagnostics mempty [ ErrCtorRefinement (GM.sourcePosSrcSpan $ loc ty) (pprint s) ] + checkOne _ = mempty + + getRetTyRef (RFun _ _ _ t _) = getRetTyRef t + getRetTyRef (RAllT _ t _) = getRetTyRef t + getRetTyRef t = ur_reft $ rt_reft t + + -- True refinement + validRef (F.Reft (_, F.PTrue)) + = True + -- Prop foo from ProofCombinators + validRef (F.Reft (v, F.PAtom F.Eq (F.EApp (F.EVar n) (F.EVar v')) _)) + | n == "Language.Haskell.Liquid.ProofCombinators.prop" + , v == v' + = True + validRef _ = False + + isCtorName x = case idDetails x of + DataConWorkId _ -> True + DataConWrapId _ -> True + _ -> False checkPlugged :: PPrint v => [(v, LocSpecType)] -> Diagnostics diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Errors.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Errors.hs index edba616324..b20000ec0f 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Errors.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Errors.hs @@ -483,6 +483,11 @@ data TError t = , dc :: !Doc } + | ErrCtorRefinement { pos :: !SrcSpan + , ctorName :: !Doc + } -- ^ The refinement of a doesn't admit + -- a refinement on the return type that + -- isn't deemd safe | ErrOther { pos :: SrcSpan , msg :: !Doc @@ -1061,6 +1066,11 @@ ppError' _ dCtx (ErrPosTyCon _ tc dc) , nest 2 "https://ucsd-progsys.github.io/liquidhaskell/options/#positivity-check" ] +ppError' _ dCtx (ErrCtorRefinement _ ctorName) + = text "Refinement of the constructor" <+> ctorName <+> "doesn't admit an arbitrary refinements on the return type" + $+$ dCtx + $+$ nest 4 (text "Were you trying to use `Prop` from `Language.Haskell.Liquid.ProofCombinators`?") + ppError' _ dCtx (ErrParseAnn _ msg) = text "Malformed annotation" $+$ dCtx diff --git a/tests/benchmarks/cse230/src/Week10/ProofCombinators.hs b/tests/benchmarks/cse230/src/Week10/ProofCombinators.hs index e458c8939e..91d741bf9a 100644 --- a/tests/benchmarks/cse230/src/Week10/ProofCombinators.hs +++ b/tests/benchmarks/cse230/src/Week10/ProofCombinators.hs @@ -73,7 +73,9 @@ _ *** _ = () data QED = Admit | QED {-@ measure isAdmit :: QED -> Bool @-} -{-@ Admit :: {v:QED | isAdmit v } @-} +isAdmit :: QED -> Bool +isAdmit Admit = True +isAdmit QED = False ------------------------------------------------------------------------------- diff --git a/tests/neg/RefCtor.hs b/tests/neg/RefCtor.hs new file mode 100644 index 0000000000..6422c05b81 --- /dev/null +++ b/tests/neg/RefCtor.hs @@ -0,0 +1,14 @@ +{-# LANGUAGE GADTs #-} +{-@ LIQUID "--expect-any-error" @-} +module RefCtor where + +import Language.Haskell.Liquid.ProofCombinators + +{-@ type K X Y = { _:F | X = Y } @-} + +data F where +{-@ MkF :: x:Int -> y:Int -> K x y @-} + MkF :: Int -> Int -> F + +{-@ falseProof :: { false } @-} +falseProof = () ? MkF 0 2 \ No newline at end of file diff --git a/tests/pos/CountMonad.hs b/tests/pos/CountMonad.hs index df5468fb76..6e3d6b6065 100644 --- a/tests/pos/CountMonad.hs +++ b/tests/pos/CountMonad.hs @@ -4,7 +4,6 @@ module CountMonad () where {-@ measure count :: Count a -> Int @-} -{-@ Count :: x:a -> {v:Count a | v == Count x } @-} data Count a = Count a instance Functor Count where @@ -36,7 +35,6 @@ assertCount _ x = x getCount :: Count a -> Int getCount _ = 0 -{-@ makeCount :: x:a -> {v:Count a | v == Count x} @-} makeCount = Count {-@ assume incr :: a -> {v:Count a | count v == 1 } @-} diff --git a/tests/tests.cabal b/tests/tests.cabal index 9e15d4ada3..1576866b53 100644 --- a/tests/tests.cabal +++ b/tests/tests.cabal @@ -1295,6 +1295,7 @@ executable unit-neg , Record0 , RecQSort , RecSelector + , RefCtor , RefinedProp , Revshape , ReWrite2 From d461ed38903a8a9db68063b14ef4860af5478a1f Mon Sep 17 00:00:00 2001 From: Alessio <35380179+AlecsFerra@users.noreply.github.com> Date: Sat, 11 Jan 2025 00:02:25 +0100 Subject: [PATCH 2/8] Apply suggestions from code review MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Facundo Domínguez --- .../src/Language/Haskell/Liquid/Bare/Check.hs | 7 +++++++ .../src/Language/Haskell/Liquid/Types/Errors.hs | 4 ++-- tests/neg/RefCtor.hs | 2 ++ 3 files changed, 11 insertions(+), 2 deletions(-) diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Check.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Check.hs index 9f91c83da7..6ecbef1cf7 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Check.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Check.hs @@ -194,6 +194,13 @@ checkTargetSpec specs src env cbs tsp +-- | Tests that the returned refinement type of data constructors has predicate @True@ or @prop v == e@. +-- +-- > data T = T Int +-- > {-@ T :: x:Int -> { v:T | v = T x } @-} -- Should be rejected +-- > {-@ T :: x:Int -> { v:T | True } @-} -- Should be fine +-- > {-@ T :: x:Int -> { v:T | prop v = True } @-} -- Should be fine +-- checkConstructorRefinement :: [(Var, LocSpecType)] -> Diagnostics checkConstructorRefinement = mconcat . map checkOne where diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Errors.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Errors.hs index b20000ec0f..8dcba4cbdf 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Errors.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Errors.hs @@ -485,7 +485,7 @@ data TError t = | ErrCtorRefinement { pos :: !SrcSpan , ctorName :: !Doc - } -- ^ The refinement of a doesn't admit + } -- ^ The refinement of a data constructor doesn't admit -- a refinement on the return type that -- isn't deemd safe @@ -1067,7 +1067,7 @@ ppError' _ dCtx (ErrPosTyCon _ tc dc) ] ppError' _ dCtx (ErrCtorRefinement _ ctorName) - = text "Refinement of the constructor" <+> ctorName <+> "doesn't admit an arbitrary refinements on the return type" + = text "Refinement of the data constructor" <+> ctorName <+> "doesn't admit an arbitrary refinements on the return type" $+$ dCtx $+$ nest 4 (text "Were you trying to use `Prop` from `Language.Haskell.Liquid.ProofCombinators`?") diff --git a/tests/neg/RefCtor.hs b/tests/neg/RefCtor.hs index 6422c05b81..87615c6e80 100644 --- a/tests/neg/RefCtor.hs +++ b/tests/neg/RefCtor.hs @@ -1,5 +1,7 @@ {-# LANGUAGE GADTs #-} {-@ LIQUID "--expect-any-error" @-} +-- | Tests that the returned refinement type of data constructors +-- is not allowed to be other than @True@. module RefCtor where import Language.Haskell.Liquid.ProofCombinators From 4d69733c1c34dab3af74a75adcff525131068cf6 Mon Sep 17 00:00:00 2001 From: Alessio Ferrarini Date: Sat, 11 Jan 2025 00:12:22 +0100 Subject: [PATCH 3/8] Make error in negative test explicit --- tests/neg/RefCtor.hs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/tests/neg/RefCtor.hs b/tests/neg/RefCtor.hs index 87615c6e80..a6a0f31948 100644 --- a/tests/neg/RefCtor.hs +++ b/tests/neg/RefCtor.hs @@ -1,5 +1,5 @@ {-# LANGUAGE GADTs #-} -{-@ LIQUID "--expect-any-error" @-} + -- | Tests that the returned refinement type of data constructors -- is not allowed to be other than @True@. module RefCtor where @@ -9,6 +9,7 @@ import Language.Haskell.Liquid.ProofCombinators {-@ type K X Y = { _:F | X = Y } @-} data F where +{-@ LIQUID "--expect-error-containing=Refinement of the data constructor RefCtor.MkF doesn't admit an arbitrary refinements on the return type" @-} {-@ MkF :: x:Int -> y:Int -> K x y @-} MkF :: Int -> Int -> F From df4388542cd8f7b46a2489bc3d118d176033ebca Mon Sep 17 00:00:00 2001 From: Alessio Ferrarini Date: Tue, 14 Jan 2025 14:46:33 +0100 Subject: [PATCH 4/8] Add a flag to allow unsafe ctor refinement --- .../src/Language/Haskell/Liquid/Bare/Check.hs | 4 +++- .../src/Language/Haskell/Liquid/UX/CmdLine.hs | 5 +++++ .../src/Language/Haskell/Liquid/UX/Config.hs | 1 + tests/pos/AllowUnsafeCtor.hs | 15 +++++++++++++++ 4 files changed, 24 insertions(+), 1 deletion(-) create mode 100644 tests/pos/AllowUnsafeCtor.hs diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Check.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Check.hs index 6ecbef1cf7..944e647191 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Check.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Check.hs @@ -173,7 +173,9 @@ checkTargetSpec specs src env cbs tsp <> checkSizeFun emb env (gsTconsP (gsName tsp)) <> checkPlugged (catMaybes [ fmap (F.dropSym 2 $ GM.simplesymbol x,) (getMethodType t) | (x, t) <- gsMethods (gsSig tsp) ]) <> checkRewrites tsp - <> checkConstructorRefinement (gsTySigs $ gsSig tsp) + <> if allowUnsafeConstructors $ getConfig tsp + then mempty + else checkConstructorRefinement (gsTySigs $ gsSig tsp) _rClasses = concatMap Ms.classes specs _rInsts = concatMap Ms.rinstance specs diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/UX/CmdLine.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/UX/CmdLine.hs index 2abf1590ea..aad60b65e3 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/UX/CmdLine.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/UX/CmdLine.hs @@ -484,6 +484,10 @@ config = cmdArgsMode $ Config { = def &= help "Dump pre-normalized core (before a-normalization)" &= name "dump-pre-normalized-core" &= explicit + , allowUnsafeConstructors + = def &= help "Allow refining constructors with unsafe refinements" + &= name "allow-unsafe-constructors" + &= explicit } &= program "liquid" &= help "Refinement Types for Haskell" &= summary copyright @@ -748,6 +752,7 @@ defConfig = Config , excludeAutomaticAssumptionsFor = [] , dumpOpaqueReflections = False , dumpPreNormalizedCore = False + , allowUnsafeConstructors = False } -- | Write the annotations (i.e. the files in the \".liquid\" hidden folder) and diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/UX/Config.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/UX/Config.hs index 10593091cc..1aaf6fd0e8 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/UX/Config.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/UX/Config.hs @@ -126,6 +126,7 @@ data Config = Config , excludeAutomaticAssumptionsFor :: [String] , dumpOpaqueReflections :: Bool -- Dumps all opaque reflections to the stdout , dumpPreNormalizedCore :: Bool -- Dumps the prenormalized core (before a-normalization) + , allowUnsafeConstructors :: Bool -- ^ Allow refining constructors with unsafe refinements } deriving (Generic, Data, Typeable, Show, Eq) allowPLE :: Config -> Bool diff --git a/tests/pos/AllowUnsafeCtor.hs b/tests/pos/AllowUnsafeCtor.hs new file mode 100644 index 0000000000..55f1f12a58 --- /dev/null +++ b/tests/pos/AllowUnsafeCtor.hs @@ -0,0 +1,15 @@ +{-# LANGUAGE GADTs #-} + +module AllowUnsafeCtor where + +import Language.Haskell.Liquid.ProofCombinators + +{-@ type K X Y = { _:F | X = Y } @-} + +{-@ LIQUID "--allow-unsafe-constructors" @-} +data F where +{-@ MkF :: x:Int -> y:Int -> K x y @-} + MkF :: Int -> Int -> F + +{-@ falseProof :: { false } @-} +falseProof = () ? MkF 0 2 \ No newline at end of file From 13fa4215ab3a0c7532512b820008b76d45e67b2b Mon Sep 17 00:00:00 2001 From: Alessio Ferrarini Date: Tue, 14 Jan 2025 14:56:36 +0100 Subject: [PATCH 5/8] Add documentation for allow-unsafe-constructors --- docs/mkDocs/docs/options.md | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/docs/mkDocs/docs/options.md b/docs/mkDocs/docs/options.md index f4d06a87be..84848478f9 100644 --- a/docs/mkDocs/docs/options.md +++ b/docs/mkDocs/docs/options.md @@ -500,6 +500,23 @@ worse = bad (Very bad) Note that all positive occurrences are permited, unlike Coq that only allows the strictly positive ones (see: https://vilhelms.github.io/posts/why-must-inductive-types-be-strictly-positive/) +## Refined construcotr + +**Options:** `allow-unsafe-constructors` +By **default** only safe constructor refinements are allowed. + +Allows the user to refine the return type of a data constructor with arbitrary refinements, also unsafe ones. + +```haskell +data F where + {-@ MkF :: { _:F | false } @-} + MkF :: F + +{-@ bad :: { false } @-} +bad :: F +bad = () ? MkF +``` + ## Total Haskell **Options:** `total-Haskell` From 3b6ee5384b75cf5172033ac255119228d496fd33 Mon Sep 17 00:00:00 2001 From: Alessio Ferrarini Date: Tue, 14 Jan 2025 14:56:57 +0100 Subject: [PATCH 6/8] typo --- docs/mkDocs/docs/options.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/mkDocs/docs/options.md b/docs/mkDocs/docs/options.md index 84848478f9..904396bd22 100644 --- a/docs/mkDocs/docs/options.md +++ b/docs/mkDocs/docs/options.md @@ -500,7 +500,7 @@ worse = bad (Very bad) Note that all positive occurrences are permited, unlike Coq that only allows the strictly positive ones (see: https://vilhelms.github.io/posts/why-must-inductive-types-be-strictly-positive/) -## Refined construcotr +## Refined construcotrs **Options:** `allow-unsafe-constructors` By **default** only safe constructor refinements are allowed. From 4d70d120cd67922cdd9bc0ea5c41993e489adb4e Mon Sep 17 00:00:00 2001 From: Alessio Ferrarini Date: Tue, 14 Jan 2025 16:44:51 +0100 Subject: [PATCH 7/8] Mention --allow-unsafe-constructors in the error message for usafe constructors --- liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Errors.hs | 1 + 1 file changed, 1 insertion(+) diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Errors.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Errors.hs index 8dcba4cbdf..7d74dc9b81 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Errors.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Errors.hs @@ -1070,6 +1070,7 @@ ppError' _ dCtx (ErrCtorRefinement _ ctorName) = text "Refinement of the data constructor" <+> ctorName <+> "doesn't admit an arbitrary refinements on the return type" $+$ dCtx $+$ nest 4 (text "Were you trying to use `Prop` from `Language.Haskell.Liquid.ProofCombinators`?") + $+$ nest 4 (text "You can disable this error by enabling the flag `--allow-unsafe-constructors`") ppError' _ dCtx (ErrParseAnn _ msg) = text "Malformed annotation" From d61e399637ce3290c9c0502e7e027bdddecfb919 Mon Sep 17 00:00:00 2001 From: Alessio <35380179+AlecsFerra@users.noreply.github.com> Date: Tue, 14 Jan 2025 18:15:00 +0100 Subject: [PATCH 8/8] Apply suggestions from code review MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Facundo Domínguez --- docs/mkDocs/docs/options.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/mkDocs/docs/options.md b/docs/mkDocs/docs/options.md index 904396bd22..593bcf2133 100644 --- a/docs/mkDocs/docs/options.md +++ b/docs/mkDocs/docs/options.md @@ -500,10 +500,10 @@ worse = bad (Very bad) Note that all positive occurrences are permited, unlike Coq that only allows the strictly positive ones (see: https://vilhelms.github.io/posts/why-must-inductive-types-be-strictly-positive/) -## Refined construcotrs +## Refined data constructors **Options:** `allow-unsafe-constructors` -By **default** only safe constructor refinements are allowed. +By **default** only safe data constructor refinements are allowed. Allows the user to refine the return type of a data constructor with arbitrary refinements, also unsafe ones.