Add a flag to allow unsafe ctor refinement

ucsd-progsys · Jan 14, 2025 · df43885 · df43885
1 parent 4d69733
commit df43885
Show file tree

Hide file tree

Showing 4 changed files with 24 additions and 1 deletion.
diff --git 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
@@ -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
@@ -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
@@ -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