liquidhaskell 0.8.10.1 → 0.8.10.2
raw patch · 6 files changed
+192/−15 lines, 6 filesdep ~aesondep ~ghcdep ~hashable
Dependency ranges changed: aeson, ghc, hashable, optparse-applicative
Files
- liquidhaskell.cabal +5/−4
- src/Language/Haskell/Liquid/Constraint/Generate.hs +13/−10
- tests/pos/T1697.hs +58/−0
- tests/pos/T1697A.hs +60/−0
- tests/pos/T1697C.hs +54/−0
- tests/test.hs +2/−1
liquidhaskell.cabal view
@@ -1,6 +1,6 @@ cabal-version: 2.4 name: liquidhaskell-version: 0.8.10.1+version: 0.8.10.2 synopsis: Liquid Types for Haskell description: Liquid Types for Haskell. license: BSD-3-Clause@@ -224,9 +224,10 @@ , gitrev , hashable >= 1.3 , hscolour >= 1.22- , liquid-fixpoint >= 0.8.0.0+ , liquid-fixpoint >= 0.8.10.1 , mtl >= 2.1 , optics >= 0.2+ , optparse-applicative < 0.16.0.0 , optparse-simple , githash , parsec >= 3.1@@ -297,7 +298,7 @@ other-modules: Paths_liquidhaskell hs-source-dirs: tests build-depends: base >= 4.8.1.0 && < 5- , liquid-fixpoint >= 0.8.0.0+ , liquid-fixpoint >= 0.8.10.1 , liquidhaskell , parsec , syb@@ -313,7 +314,7 @@ other-modules: Paths_liquidhaskell hs-source-dirs: tests build-depends: base >= 4.8.1.0 && < 5- , liquid-fixpoint >= 0.8.0.0+ , liquid-fixpoint >= 0.8.10.1 , liquidhaskell , tasty >= 0.7 , tasty-hunit
src/Language/Haskell/Liquid/Constraint/Generate.hs view
@@ -437,14 +437,15 @@ consCB _ _ γ (NonRec x def) | Just (w, τ) <- grepDictionary def , Just d <- dlookup (denv γ) w- = do t <- trueTy τ- addW $ WfC γ t+ = do t <- mapM trueTy τ+ mapM addW (WfC γ <$> t) let xts = dmap (fmap (f t)) d let γ' = γ { denv = dinsert (denv γ) x xts } t <- trueTy (varType x) extender γ' (x, Assumed t) where- f t' (RAllT α te _) = subsTyVar_meet' (ty_var_value α, t') te+ f [t'] (RAllT α te _) = subsTyVar_meet' (ty_var_value α, t') te+ f (t':ts) (RAllT α te _) = f ts $ subsTyVar_meet' (ty_var_value α, t') te f _ _ = impossible Nothing "consCB on Dictionary: this should not happen" consCB _ _ γ (NonRec x e)@@ -452,10 +453,13 @@ to' <- consBind False γ (x, e, to) >>= (addPostTemplate γ) extender γ (x, makeSingleton γ (simplify e) <$> to') -grepDictionary :: CoreExpr -> Maybe (Var, Type)-grepDictionary (App (Var w) (Type t)) = Just (w, t)-grepDictionary (App e (Var _)) = grepDictionary e-grepDictionary _ = Nothing+grepDictionary :: CoreExpr -> Maybe (Var, [Type])+grepDictionary = go [] + where + go ts (App (Var w) (Type t)) = Just (w, reverse (t:ts))+ go ts (App e (Type t)) = go (t:ts) e+ go ts (App e (Var _)) = go ts e+ go _ _ = Nothing -------------------------------------------------------------------------------- consBind :: Bool -> CGEnv -> (Var, CoreExpr, Template SpecType) -> CG (Template SpecType)@@ -1448,14 +1452,13 @@ -- | @isGenericVar@ determines whether the @RTyVar@ has no class constraints isGenericVar :: RTyVar -> SpecType -> Bool-isGenericVar α t = all (\(c, α') -> (α'/=α) || isOrd c || isEq c ) (classConstrs t)+isGenericVar α t = all (\(c, α') -> (α'/=α) || isGenericClass c ) (classConstrs t) where classConstrs t = [(c, ty_var_value α') | (c, ts) <- tyClasses t , t' <- ts , α' <- freeTyVars t']- isOrd = (ordClassName ==) . className- isEq = (eqClassName ==) . className+ isGenericClass c = className c `elem` [ordClassName, eqClassName] -- , functorClassName, monadClassName] -- instance MonadFail CG where -- fail msg = panic Nothing msg
+ tests/pos/T1697.hs view
@@ -0,0 +1,58 @@+{-@ LIQUID "--no-pattern-inline" @-}++module B where++data User = U++{-@ measure currentUser :: User @-}++{-@ data TaggedT user m a <label :: user -> Bool, clear :: user -> Bool> = TaggedT _ @-}+data TaggedT user m a = TaggedT { unTag :: m a }+{-@ data variance TaggedT invariant invariant covariant contravariant covariant @-}++instance Functor m => Functor (TaggedT user m) where+ fmap f = TaggedT . fmap f . unTag++instance Applicative m => Applicative (TaggedT user m) where+ pure = TaggedT . pure+ f <*> x = TaggedT $ unTag f <*> unTag x++{-@+instance Monad m => Monad (TaggedT user m) where+ >>= :: forall < p :: user -> Bool+ , q :: user -> Bool+ , r :: user -> Bool+ , s :: user -> Bool+ , t :: user -> Bool+ , u :: user -> Bool+ , rx :: a -> Bool+ , rf :: a -> b -> Bool+ , ro :: b -> Bool+ >.+ {content :: a<rx> |- b<rf content> <: b<ro>}+ {content :: a<rx> |- b<ro> <: b<rf content>}+ {{v : (user<s>) | True} <: {v : (user<p>) | True}}+ {{v : (user<t>) | True} <: {v : (user<p>) | True}}+ {{v : (user<t>) | True} <: {v : (user<r>) | True}}+ {{v : (user<q>) | True} <: {v : (user<u>) | True}}+ {{v : (user<s>) | True} <: {v : (user<u>) | True}}+ x:TaggedT<p, q> user m (a<rx>)+ -> (y:a -> TaggedT<r, s> user m (b<rf y>))+ -> TaggedT<t, u> user m (b<ro>);++ return :: a -> TaggedT<{\_ -> True}, {\_ -> False}> user m a+@-}+instance Monad m => Monad (TaggedT user m) where+ x >>= f = TaggedT $ unTag x >>= \y -> unTag (f y)+ +-------------------------------------------------------------------------------------------+-- | Test+-------------------------------------------------------------------------------------------++{-@ assume respondT :: String -> TaggedT<{\_ -> True}, {\v -> v == currentUser}> User m () @-}+respondT :: String -> TaggedT User m ()+respondT = undefined++{-@ test :: TaggedT<{\_ -> True}, {\v -> v == currentUser}> User m () @-}+test :: Monad m => TaggedT User m ()+test = return "a" >>= respondT
+ tests/pos/T1697A.hs view
@@ -0,0 +1,60 @@+-------------------------------------------------------------------------------------------+-- | Fixed User (WORKING)+-------------------------------------------------------------------------------------------++module A where++data User = U++{-@ measure currentUser :: User @-}++{-@ data TaggedT m a <label :: User -> Bool, clear :: User -> Bool> = TaggedT _ @-}+data TaggedT m a = TaggedT { unTag :: m a }+{-@ data variance TaggedT invariant covariant contravariant covariant @-}++instance Functor m => Functor (TaggedT m) where+ fmap f = TaggedT . fmap f . unTag++instance Applicative m => Applicative (TaggedT m) where+ pure = TaggedT . pure+ f <*> x = TaggedT $ unTag f <*> unTag x++{-@+instance Monad m => Monad (TaggedT m) where+ >>= :: forall < p :: User -> Bool+ , q :: User -> Bool+ , r :: User -> Bool+ , s :: User -> Bool+ , t :: User -> Bool+ , u :: User -> Bool+ , rx :: a -> Bool+ , rf :: a -> b -> Bool+ , ro :: b -> Bool+ >.+ {content :: a<rx> |- b<rf content> <: b<ro>}+ {content :: a<rx> |- b<ro> <: b<rf content>}+ {{v : (User<s>) | True} <: {v : (User<p>) | True}}+ {{v : (User<t>) | True} <: {v : (User<p>) | True}}+ {{v : (User<t>) | True} <: {v : (User<r>) | True}}+ {{v : (User<q>) | True} <: {v : (User<u>) | True}}+ {{v : (User<s>) | True} <: {v : (User<u>) | True}}+ x:TaggedT<p, q> m (a<rx>)+ -> (y:a -> TaggedT<r, s> m (b<rf y>))+ -> TaggedT<t, u> m (b<ro>);++ return :: a -> TaggedT<{\_ -> True}, {\_ -> False}> m a+@-}+instance Monad m => Monad (TaggedT m) where+ x >>= f = TaggedT $ unTag x >>= \y -> unTag (f y)+ +-------------------------------------------------------------------------------------------+-- | Test+-------------------------------------------------------------------------------------------++{-@ assume respondT :: String -> TaggedT<{\_ -> True}, {\v -> v == currentUser}> m () @-}+respondT :: String -> TaggedT m ()+respondT = undefined++{-@ test :: TaggedT<{\_ -> True}, {\v -> v == currentUser}> m () @-}+test :: Monad m => TaggedT m ()+test = return "a" >>= respondT
+ tests/pos/T1697C.hs view
@@ -0,0 +1,54 @@+-------------------------------------------------------------------------------------------+-- | Polymorphic user but defining bind and return as normal functions (WORKING)+-------------------------------------------------------------------------------------------++module C where++data User = U++{-@ measure currentUser :: User @-}++{-@ data TaggedT user m a <label :: user -> Bool, clear :: user -> Bool> = TaggedT _ @-}+data TaggedT user m a = TaggedT { unTag :: m a }+{-@ data variance TaggedT invariant invariant covariant contravariant covariant @-}++{-@+assume bindT :: forall < p :: user -> Bool+ , q :: user -> Bool+ , r :: user -> Bool+ , s :: user -> Bool+ , t :: user -> Bool+ , u :: user -> Bool+ , rx :: a -> Bool+ , rf :: a -> b -> Bool+ , ro :: b -> Bool+ >.+ {content :: a<rx> |- b<rf content> <: b<ro>}+ {content :: a<rx> |- b<ro> <: b<rf content>}+ {{v : (user<s>) | True} <: {v : (user<p>) | True}}+ {{v : (user<t>) | True} <: {v : (user<p>) | True}}+ {{v : (user<t>) | True} <: {v : (user<r>) | True}}+ {{v : (user<q>) | True} <: {v : (user<u>) | True}}+ {{v : (user<s>) | True} <: {v : (user<u>) | True}}+ x:TaggedT<p, q> user m (a<rx>)+ -> (y:a -> TaggedT<r, s> user m (b<rf y>))+ -> TaggedT<t, u> user m (b<ro>)+@-}+bindT :: Monad m => TaggedT user m a -> (a -> TaggedT user m b) -> TaggedT user m b+bindT x f = TaggedT $ unTag x >>= \y -> unTag (f y)++{-@ assume returnT :: a -> TaggedT<{\_ -> True}, {\_ -> False}> user m a @-}+returnT :: Monad m => a -> TaggedT user m a+returnT x = TaggedT (return x)++-------------------------------------------------------------------------------------------+-- | Test+-------------------------------------------------------------------------------------------++{-@ assume respondT :: String -> TaggedT<{\_ -> True}, {\v -> v == currentUser}> User m () @-}+respondT :: String -> TaggedT User m ()+respondT = undefined++{-@ test :: TaggedT<{\_ -> True}, {\v -> v == currentUser}> User m () @-}+test :: Monad m => TaggedT User m ()+test = returnT "a" `bindT` respondT
tests/test.hs view
@@ -313,7 +313,8 @@ benchTests :: IO TestTree benchTests = group "Benchmarks"- [ testGroup "esop" <$> dirTests "benchmarks/esop2013-submission" esopIgnored ExitSuccess+ [ testGroup "cse230" <$> dirTests "benchmarks/cse230/src/Week10" [] ExitSuccess+ , testGroup "esop" <$> dirTests "benchmarks/esop2013-submission" esopIgnored ExitSuccess , testGroup "vect-algs" <$> odirTests "benchmarks/vector-algorithms-0.5.4.2" [] vectOrder ExitSuccess , testGroup "bytestring" <$> odirTests "benchmarks/bytestring-0.9.2.1" bsIgnored bsOrder ExitSuccess , testGroup "text" <$> odirTests "benchmarks/text-0.11.2.3" textIgnored textOrder ExitSuccess