Strange behavior with monadic bind

[ranjitjhala]

Via @nilehmann

https://gist.github.com/nilehmann/8ace3dd793dc78bf0af04f8ee3585b84

• A.hs the code is safe using a monad where User is hardwired
• B.hs the code is unsafe using a monad where user is a parameter
• C.hs the code is safe where we use a plain bindT and returnT

Some mysterious goings on.

1. Why is LH not failing on A.hs, B.hs demanding that --no-pattern-inline? Both use refined monads?
2. Also, when run in the latest LH, A is safe with 1 checked constraint while C has 28 checked constraints?
3. Why does C.hs need the assume statements but A and B do not? (are instance signatures "assumed" by default??)

@nikivazou -- I think you will need definitely need to take a look at this, it touches two things that I'm unfamiliar
with (the instances and bounds) but I'm guessing that won't happen until the after your deadline next week?

[ranjitjhala]

@nilehmann -- this almost surely has to do with some strange interaction of
the gnarly code that links signatures and class-instances. The only good news
here is that C.hs seems to be doing the right thing. Consequently, for the short
term i.e. till @nikivazou can figure this out, can you try to make progress with
RebindableSyntax e.g. module D.hs below (which works?)

(Basically means you cannot overload >>= in a module, i.e. use a different
monad instance than TaggedT / Controller in the same file as where you
are doing stuff with TaggedT / Controller which obviously sucks, and must
be fixed ASAP, but maybe you can make some progress with it? LMK!)

{-# LANGUAGE RebindableSyntax #-}

module D where

import Prelude hiding ((>>=), return)

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 >>= :: 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>)
@-}
(>>=) :: Monad m => TaggedT user m a -> (a -> TaggedT user m b) -> TaggedT user m b
(>>=) x f = undefined -- TaggedT $ unTag x >>= \y -> unTag (f y)

{-@ assume return :: a -> TaggedT<{\_ -> True}, {\_ -> False}> user m a @-}
return :: Monad m => a -> TaggedT user m a
return x = undefined -- 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 = do
  z <- return "a"
  respondT z

[nilehmann]

@ranjitjhala, thanks for the suggestion. I think it will be enough to have a proof of concept of the library-ification. So, I should be good for now.

[nikivazou]

The solution to make B.hs safe is this: #1621 where both functor and monads are generic classes. i.e.,

https://github.com/ucsd-progsys/liquidhaskell/pull/1621/files#diff-69cb9308eaa64a31f444271f0cf99568R1467

should get

    isGenericClass c = className c `elem` [ordClassName, eqClassName, functorClassName, monadClassName]

In other words, all the refinements are lost on the constraints >>=.

[nilehmann]

I don't quite understand the solution, but why is there a difference between refining TaggedT m a (A.hs) and TaggedT user m a (B.hs)?

Also, is this related to instantiating mapM :: (a -> TaggedT<true, true> m b) -> t a -> TaggedT<true, true> (t b) instead of mapM :: (a -> TaggedT<p, q> m b) -> t a -> TaggedT<p q> (t b) as we would want?

[ranjitjhala]

@nilehmann i don’t follow your mapM remark, aren’t you missing some m in the signature?

[nilehmann]

@ranjitjhala, yeah I missed some m's. Right now I think mapM is instantiated with:

mapM :: (a -> TaggedT<{\_ -> True}, {\_ -> True}> m b) -> t a -> TaggedT<{\_ -> True}, {\_ -> True}> m (t b)

but we'd like it to be more like

mapM :: (a -> TaggedT<p, q> m b) -> t a -> TaggedT<p, q> m (t b)

[ranjitjhala]

Can you add this as a concrete code snippet to this issue? Eg we want X.hs to be safe (if mapM is instantiated correctly?) as I understand it Niki’s suggestion may/should Address this too so I can see if the edit she suggests helps

…

On Thu, Jul 23, 2020 at 11:17 AM Nico Lehmann ***@***.***> wrote: @ranjitjhala <https://urldefense.com/v3/__https://github.com/ranjitjhala__;!!Mih3wA!ViXO-Q2HZINM-UPZL2TY6EwMPsOKsYATyuleK0cYy10zmmxtmz73Kd5UGT9zNmCZ$>, yeah I missed some m's. Right now I think mapM is instantiated with: mapM :: (a -> TaggedT<{\_ -> True}, {\_ -> True}> m b) -> t a -> TaggedT<{\_ -> True}, {\_ -> True}> m (t b) but we'd like it to be more like mapM :: (a -> TaggedT<p, q> m b) -> t a -> TaggedT<p, q> m (t b) — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquidhaskell/issues/1697*issuecomment-663157865__;Iw!!Mih3wA!ViXO-Q2HZINM-UPZL2TY6EwMPsOKsYATyuleK0cYy10zmmxtmz73Kd5UGS2Pw9Ou$>, or unsubscribe <https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OA5M535ACR7DNPIINDR5B5CVANCNFSM4OPOM72A__;!!Mih3wA!ViXO-Q2HZINM-UPZL2TY6EwMPsOKsYATyuleK0cYy10zmmxtmz73Kd5UGQ1qGi9F$> .

[ranjitjhala]

Thinking some more the isGeneric should be necessary to get the mapM working properly but may not be sufficient...

…

On Thu, Jul 23, 2020 at 11:20 AM Ranjit Jhala ***@***.***> wrote: Can you add this as a concrete code snippet to this issue? Eg we want X.hs to be safe (if mapM is instantiated correctly?) as I understand it Niki’s suggestion may/should Address this too so I can see if the edit she suggests helps On Thu, Jul 23, 2020 at 11:17 AM Nico Lehmann ***@***.***> wrote: > @ranjitjhala > <https://urldefense.com/v3/__https://github.com/ranjitjhala__;!!Mih3wA!ViXO-Q2HZINM-UPZL2TY6EwMPsOKsYATyuleK0cYy10zmmxtmz73Kd5UGT9zNmCZ$>, > yeah I missed some m's. Right now I think mapM is instantiated with: > > mapM :: (a -> TaggedT<{\_ -> True}, {\_ -> True}> m b) -> t a -> TaggedT<{\_ -> True}, {\_ -> True}> m (t b) > > but we'd like it to be more like > > mapM :: (a -> TaggedT<p, q> m b) -> t a -> TaggedT<p, q> m (t b) > > — > You are receiving this because you were mentioned. > Reply to this email directly, view it on GitHub > <https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquidhaskell/issues/1697*issuecomment-663157865__;Iw!!Mih3wA!ViXO-Q2HZINM-UPZL2TY6EwMPsOKsYATyuleK0cYy10zmmxtmz73Kd5UGS2Pw9Ou$>, > or unsubscribe > <https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OA5M535ACR7DNPIINDR5B5CVANCNFSM4OPOM72A__;!!Mih3wA!ViXO-Q2HZINM-UPZL2TY6EwMPsOKsYATyuleK0cYy10zmmxtmz73Kd5UGQ1qGi9F$> > . >

[ranjitjhala]

@nikivazou your solution doesn't work. When I make Monad generic, the tests/neg/monad4.hs verifies which is unsound. The test looks like this:

module Foo () where

import Language.Haskell.Liquid.Prelude

gpp :: Monad m => m Int -> m Int
gpp z = do x <- z
           return $ liquidAssert (x > 0) (x - 10)

{-@ xs :: Maybe {v:Int | v > 0} @-}
xs :: Maybe Int
xs = Just 9

ys :: Maybe Int
ys = gpp xs

The reason this gets verified is that LH synthesizes the type

gpp :: (Monad m) => m Pos -> {v:m | false} Int

and hence that

ys :: {v: Maybe Int | false}

after which it is all game over...

Now, I don't know why making Monad generic should gpp this odd type (with the {m | false}).

The code is something like:

gpp z = z >>= \x -> return (...)

Now, I can see that the

return :: a -> m a

so return ... can yield an {m | false} ... (because there is no constraint on the m in the return).

but I'm puzzled by the >>= because

>>= :: m a -> (a -> m b) -> m b

so if we have an instance:

{m | km} ka -> (ka -> {m | k} kb) -> {m| k} kb

where km, ka and kb are the refinement variables for m, a and b respectively.

then, as the type of z :: {m | true} Pos we should get the subtyping constraints:

g |- {m | true} Pos <: {m | km} ka                  ... 1
g |- x:tx -> {m|false} Int <: ka -> {m|km} kb    ... 2

due to the two arguments to >>= which should produce a

g |- true <:  km

UNLESS in the constraint splitting for Higher Kinded types like this m Int, we silently ignore subtyping on the m ? However, that's not what the code seems to be doing:

splitC (SubC γ t1@(RAppTy r1 r1' _) t2@(RAppTy r2 r2' _))
  =  do cs    <- bsplitC γ t1 t2
        cs'   <- splitC  (SubC γ r1 r2)
        cs''  <- splitC  (SubC γ r1' r2')
        cs''' <- splitC  (SubC γ r2' r1')
        return $ cs ++ cs' ++ cs'' ++ cs'''

I am confused why is there BOTH r1' <: r2' AND r2' <: r1' btw?

Anyway -- long story short, just marking Monad as generic is currently unsound. So either we need to make it sound (by figuring out why the {m | false} is showing up?) or find another route.

[ranjitjhala]

Btw, @nikivazou here's a stripped down version that is unsoundly marked "safe" with "generic" monad

module Foo () where

gpp :: Monad m => m Int -> m Int
gpp z = do
  x <- z
  return x

{-@ ys :: {v: Maybe Int | false } @-}
ys :: Maybe Int
ys = gpp (Just 0)

[ranjitjhala]

Further simplification yields this:

module Foo () where

rebindMonad :: Monad m => m Int -> m Int
rebindMonad z = do
  x <- z
  return x

{-@ rebindMaybe :: {v:_ | true} -> {v:_| false} @-}
rebindMaybe :: Maybe Int -> Maybe Int
rebindMaybe = rebindMonad

I think the problem is this: LH infers

rebindMonad :: Monad m => m Int -> {v:m | false}  Int

but then when we do the actual specialization to the Maybe monad it somehow converts:

INSTANTIATE({v:m | false} Int, m, Maybe) ===>  {v:Maybe Int | false} 

So maybe it has to do with how we're dealing with application/substitution of HKT?

Also, its odd that we should attach a refinement with the m in {v: m | false} -- I mean m is not of kind * and we should only have refinements attached to things of kind * (much like we don't associate refinements with functions.

[nikivazou]

@ranjitjhala it seems that all the "unsound" examples you have are soundly unsafe with the "--no-pattern-inline" flag.
With respect to whether or not the Monad is actually generic, since return can return ANY monad, I do not have yet a concrete answer.

Here is exactly why we need a fresh k var for B.hs to type check. We need to check

(>>=) (@ TaggedT User m') d (return "a") respondT :: TaggedT<{\_ -> True}, {\v -> v == currentUser}> User m' ()

with

(>>=) :: Monad m => m a -> (a -> m b) -> m  b  

Currently, the only way to unify bind's result m b with TaggedT<{\_ -> True}, {\v -> v == currentUser}> User m' () is if the type generated at the type instantiation of the bind is fresh and the fresh k var gets eventually instantiated with the <{\_ -> True}, {\v -> v == currentUser}> refinements.
A (drastic) alternative approach would be not to rely on inference, but to type check application using checking of our bidirectional rules (cconsE) and syntactically unify bind's result with the desired type.