Merge pull request #2433 from AlecsFerra/develop

Handle type alias + refinements

Author: facundominguez

liquidhaskell-boot/src/Language/Haskell/Liquid/Types/RefType.hs

@@ -712,6 +712,7 @@ strengthen (RVar a r)         r' = RVar a         (r `meet` r')
 strengthen (RFun b i t1 t2 r) r' = RFun b i t1 t2 (r `meet` r')
 strengthen (RAppTy t1 t2 r)   r' = RAppTy t1 t2   (r `meet` r')
 strengthen (RAllT a t r)      r' = RAllT a t      (r `meet` r')
+strengthen (RHole r)          r' = RHole          (r `meet` r')
 strengthen t                  _  = t
 
 quantifyRTy :: (Monoid r, Eq tv) => [RTVar tv (RType c tv ())] -> RType c tv r -> RType c tv r

tests/neg/RefinedProp.hs

@@ -0,0 +1,15 @@
+{-# Language GADTs #-}
+
+module RefinedProp where
+
+import Language.Haskell.Liquid.ProofCombinators
+
+data Id where
+{-@ MkId :: Prop (Id 12) @-}
+    MkId :: Id
+data ID = Id Int
+
+-- Should error as False is supposed to not be satisfied
+{-@ fail bad @-}
+{-@ bad :: { v:Prop (Id 12) | False } @-}
+bad = MkId

tests/tests.cabal

@@ -1294,6 +1294,7 @@ executable unit-neg
                     , Record0
                     , RecQSort
                     , RecSelector
+                    , RefinedProp
                     , Revshape
                     , ReWrite2
                     , ReWrite3