Merge pull request #2470 from AlecsFerra/develop

Fix unsafe data constructor refinements

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 data constructors
+
+**Options:** `allow-unsafe-constructors`
+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.
+
+```haskell
+data F where
+  {-@ MkF :: { _:F | false } @-}
+  MkF :: F
+
+{-@ bad :: { false } @-}
+bad :: F
+bad = () ? MkF
+```
+
 ## Total Haskell
 
 **Options:** `total-Haskell`

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

liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Check.hs

@@ -173,6 +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
+                     <> if allowUnsafeConstructors $ getConfig tsp 
+                          then mempty 
+                          else checkConstructorRefinement (gsTySigs $ gsSig tsp) 
 
     _rClasses         = concatMap Ms.classes specs
     _rInsts           = concatMap Ms.rinstance specs
@@ -193,6 +196,39 @@ 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
+    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

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 data constructor doesn't admit
+                        -- a refinement on the return type that
+                        -- isn't deemd safe
 
   | ErrOther    { pos   :: SrcSpan
                 , msg   :: !Doc
@@ -1061,6 +1066,12 @@ ppError' _ dCtx (ErrPosTyCon _ tc dc)
              , nest 2 "https://ucsd-progsys.github.io/liquidhaskell/options/#positivity-check"
             ]
 
+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"
         $+$ dCtx

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

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

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

tests/neg/RefCtor.hs

@@ -0,0 +1,17 @@
+{-# LANGUAGE GADTs #-}
+
+-- | 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
+
+{-@ 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
+
+{-@ falseProof :: { false } @-}
+falseProof = () ? MkF 0 2

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

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 } @-}

tests/tests.cabal

@@ -1297,6 +1297,7 @@ executable unit-neg
                     , Record0
                     , RecQSort
                     , RecSelector
+                    , RefCtor
                     , RefinedProp
                     , Revshape
                     , ReWrite2