Sorts Main.Either and Main.Either are incompatible

[atondwal]

We should file the rel fixpoint bug after we find it

#!/usr/bin/env stack
-- stack --resolver lts-9.2 exec liquid --package process --install-ghc

{-@ LIQUID "--higherorder"       @-}
{-@ LIQUID "--exact-data-cons"   @-}
{-@ LIQUID "--automatic-instances=liquidinstances" @-}
{-# LANGUAGE GADTs               #-}

import Prelude hiding (Maybe (..), Either (..))

data Either a b = Left a | Right b
data Maybe a = Just a | Nothing
type Heap = Map Int (Maybe Double)
--
-- Maps
---------

{-@ data Map [mlen] k v = Empty | Record {mKey :: k, mVal :: v, mRest :: Map k v} @-}
data Map k v = Empty
         | Record k v (Map k v)

{-@ measure mlen @-}
{-@ mlen :: Map k v -> Nat @-}
mlen :: Map k v-> Int
mlen Empty          = 0
mlen (Record k v r) = 1 + mlen r

{-@ reflect update @-}
update :: Map k v -> k -> v -> Map k v
update m k v = Record k v m

{-@ reflect find @-}
find :: Eq k => k -> Map k v -> Maybe v
find key  Empty          = Nothing
find key (Record k v r)
  | k == key            = Just v
  | otherwise           = find key r

{-@ reflect delete @-}
delete :: Eq k => k -> Map k v -> Map k v
delete key Empty          = Empty
delete key (Record k v r)
  | k == key            = delete key r
  | otherwise           = Record k v (delete key r)

{-@ reflect insertWith @-}
insertWith :: Eq k => (v -> v -> v) -> k -> v -> Map k v -> Map k v
insertWith _ _ _ Empty  = Empty
insertWith f key val (Record k v r)
  | k == key            = Record k (f v val) r
  | otherwise           = Record k v (insertWith f key val r)

-- List
--------

{-@ reflect app @-}
app :: [a] -> [a] -> [a]
app (x:xs) ys = x:(app xs ys)
app [] ys     = ys

{-@ reflect fmapList @-}
fmapList :: (a -> b) -> [a] -> [b]
fmapList f (x:xs) = f x : fmapList f xs
fmapList _ [] = []

-- Heap Parital Order:
--------------------------------------------------------------------------------
data HeapLteProp where
  HeapLte :: Heap -> Heap -> HeapLteProp

data HeapLte where
  HeapRefl :: Heap -> HeapLte
  HeapTrans :: Heap -> Heap -> Heap
            -> HeapLte -> HeapLte
            -> HeapLte
  HeapAdd :: Heap -> Int -> Maybe Double
          -> HeapLte
{-@ data HeapLte where
    HeapRefl  :: h:Heap -> Prop (HeapLte h h)
  | HeapTrans :: h1:Heap -> h2:Heap -> h3:Heap
              -> Prop (HeapLte h1 h2)
              -> Prop (HeapLte h2 h3)
              -> Prop (HeapLte h1 h3)
  | HeapAdd   :: h:Heap -> k:Int -> val:(Maybe Double)
              -> Prop (HeapLte h (Record k val h))
@-}

{-@ measure prop :: a -> b           @-}
{-@ type Prop E = {v:_ | prop v = E} @-}

-- step
--------------------------------------------------------------------------------
data IVar a = IVar Int

data Trace = Get (IVar Double) (Double -> Trace)
           | Put (IVar Double) Double Trace
           | New (IVar Double -> Trace)
           | Fork Trace Trace
           | Done

data Exn = MultiplePut Double Int Double
         | Deadlock (Map Int [Double -> Trace])
         | HeapExn

instance Eq Exn where
  MultiplePut _ _ _ == MultiplePut _ _ _ = True
  Deadlock _ == Deadlock _ = True
  HeapExn == HeapExn = True
  _ == _ = False

{-@ measure brop :: a -> Bool           @-}
{-@
step :: a:(Trace,[Trace]) -> b:( Map Int [Double -> Trace]) -> c:Int -> h:Heap
     -> { v:_ | (isRight v => brop (HeapLte h (select4of4 (selectRight v)))) }
@-}
step :: (Trace, [Trace]) -> Map Int [Double -> Trace] -> Int -> Heap
     -> Either Exn ([Trace], Map Int [Double -> Trace], Int, Heap)
step (trc, others) blkd cntr heap =
  case trc of
    Done -> Right (others, blkd, cntr, heap)
    Fork t1 t2 -> Right (t1 : t2 : others, blkd, cntr, heap)
    New k -> Right (k (IVar cntr) : others, blkd, cntr + 1, Record cntr Nothing heap)
    Get (IVar ix) k ->
      case join (find ix heap) of
        Nothing -> Right (others, insertWith app ix [k] blkd, cntr, heap)
        Just v  -> Right (k v : others, blkd, cntr, heap)
    Put (IVar ix) v t2 ->
      let heap' = Record ix (Just v) heap
      in case join (find ix heap) of
        Nothing ->
          case find ix blkd of
            Nothing -> Right (t2 : others, blkd, cntr, heap')
            Just ls -> Right (t2 : app ( fmapList ($$v) ls ) others
                             , delete ix blkd, cntr, heap')
        Just v0 -> Left (MultiplePut v ix v0)

-- Misc
--------
{-@ reflect $$ @-}
f $$ x = f x

{-@ reflect join @-}
join (Just (Just x)) = Just x
join _               = Nothing

{-@ reflect isRight @-}
isRight (Right _) = True
isRight (Left _) = False

{-@ reflect select4of4 @-}
select4of4 (_,_,_,h) = h

{-@ reflect selectRight @-}
selectRight (Right h) = h

results in:

**** RESULT: ERROR *************************************************************

:1:1-1:1: Error
  crash: SMTLIB2 respSat = Error "line 1780 column 16495: Sorts Main.Either and Main.Either are incompatible"

[ranjitjhala]

Well that's a new one. Am busy for the next few days; @atondwal can you take a look?

[ranjitjhala]

@atondwal the problem here is that Z3 doesn't have any type inference so it thinks that

x = Right y

is ill-typed when

x :: Either Exn Int 
y :: Int

here is a minimal Z3/.smt file that demonstrates the problem:

(set-option :auto-config false)
(set-option :model true)
(set-option :model.partial false)
(set-option :smt.mbqi false)

(declare-datatypes (T0 T1) ((Main.Either (Main.Right (selectRight T1)) (Main.Left (selectLeft T0)))))

(declare-fun junk () (Main.Either Int  Int))
(declare-fun punk () (Main.Either Bool Int))
(declare-fun escobar () Int)

(push 1)
(assert (= punk (Main.Right escobar)))
(assert (= junk (Main.Right escobar)))
(pop 1)

The solution is to put explicit annotations around the constructor applications, just with the output type:

(set-option :auto-config false)
(set-option :model true)
(set-option :model.partial false)

(set-option :smt.mbqi false)

(declare-datatypes (T0 T1) ((Main.Either (Main.Right (selectRight T1)) (Main.Left (selectLeft T0)))))

(declare-fun junk () (Main.Either Int  Int))
(declare-fun punk () (Main.Either Bool Int))
(declare-fun escobar () Int)

(push 1)

;; BAD 
;; (assert (= punk (Main.Right escobar)))
;; (assert (= junk (Main.Right escobar)))

;; GOOD
(assert (= punk ((as Main.Right (Main.Either Bool Int)) escobar)))
(assert (= junk ((as Main.Right (Main.Either Int  Int)) escobar)))

(pop 1)

For example, see tests/pos/adt_list_2.fq which generates the SMT query (in .liquid/tests/pos/adt_list_2.fq.smt2`.

(assert (not (= (as emp (LL Int)) (ite (< 1 2) (as emp (LL Int)) (con 1 (as emp (LL Int)))))))

which gives the explicit sort annotation as emp (LL Int).

SO can you:

1. Create a minimal .fq file test that demonstrates the above problem? (It should basically be a backwards transliteration of the .smt2 file

2. Then see how the as annotations are currently generated to extend them as above

• The identifier is its a data-constructor (see SymEnv) and
• Then use the type of the result.

[atondwal]

I added tests/todo/1090.fq to LF. We should move this issue to that repo.

[atondwal]

Unfortunately, there's a bug-within-a-bug. Old version of z3 don't suffer from this monomorphization problem(???) so we can see that under that crash is another similar one.

**** RESULT: ERROR *************************************************************

:1:1-1:1: Error
  elaborate makeKnowledge failed on:
      lq_anf$##7205759403792801278##d1ZQ == lam lam_arg##1 : (function real Main.Trace) . Main.$$ (lam_arg##1 : func(0, [real;

                  Main.Trace])) v##a1u1
  with error
      Cannot unify func(0, [real; Main.Trace]) with (function real Main.Trace) in expression: lam_arg##1
  because
Cannot cast lam_arg##1 of sort (function real Main.Trace) to incompatible sort func(0, [real; Main.Trace])
  in environment
      Main.$$ := func(2, [func(0, [@(1); @(0)]); @(1); @(0)])

      v##a1u1 := real

      lq_anf$##7205759403792801278##d1ZQ := func(0, [func(0, [real;
                                                              Main.Trace]);
                                                     Main.Trace])

[ranjitjhala]

What is this function real Main.Trace?

On Tue, Sep 19, 2017 at 1:11 PM, Anish Tondwalkar notifications@github.com wrote:

Unfortunately, there's a bug-within-a-bug. Old version of z3 don't suffer from this monomorphization problem(???) so we can see that under that crash is another

** RESULT: ERROR ***

:1:1-1:1: Error elaborate makeKnowledge failed on: lq_anf$##7205759403792801278##d1ZQ == lam lam_arg##1 : (function real Main.Trace) . Main.$$ (lam_arg##1 : func(0, [real;

              Main.Trace])) v##a1u1

with error Cannot unify func(0, [real; Main.Trace]) with (function real Main.Trace) in expression: lam_arg##1 because Cannot cast lam_arg##1 of sort (function real Main.Trace) to incompatible sort func(0, [real; Main.Trace]) in environment Main.$$ := func(2, [func(0, [@(1); @(0)]); @(1); @(0)])

  v##a1u1 := real

  lq_anf$##7205759403792801278##d1ZQ := func(0, [func(0, [real;
                                                          Main.Trace]);
                                                 Main.Trace])

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/1090#issuecomment-330659126, or mute the thread https://github.com/notifications/unsubscribe-auth/ABkuOHZTsZ0Chk_5r_iVG9mxqy-rPKJLks5skB_ogaJpZM4PZ28r .

[ranjitjhala]

Anyways, this "inner" bug seems easy to fix -- figure out where this weird (function real Main.Trace) is being generated, and replace it with the actual sort which should be func(0, [real; Main.Trace])?

On Tue, Sep 19, 2017 at 2:36 PM, Ranjit Jhala jhala@cs.ucsd.edu wrote:

What is this function real Main.Trace?

On Tue, Sep 19, 2017 at 1:11 PM, Anish Tondwalkar < notifications@github.com> wrote:

Unfortunately, there's a bug-within-a-bug. Old version of z3 don't suffer from this monomorphization problem(???) so we can see that under that crash is another

** RESULT: ERROR ***

:1:1-1:1: Error elaborate makeKnowledge failed on: lq_anf$##7205759403792801278##d1ZQ == lam lam_arg##1 : (function real Main.Trace) . Main.$$ (lam_arg##1 : func(0, [real;

              Main.Trace])) v##a1u1

with error Cannot unify func(0, [real; Main.Trace]) with (function real Main.Trace) in expression: lam_arg##1 because Cannot cast lam_arg##1 of sort (function real Main.Trace) to incompatible sort func(0, [real; Main.Trace]) in environment Main.$$ := func(2, [func(0, [@(1); @(0)]); @(1); @(0)])

  v##a1u1 := real

  lq_anf$##7205759403792801278##d1ZQ := func(0, [func(0, [real;
                                                          Main.Trace]);
                                                 Main.Trace])

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/1090#issuecomment-330659126, or mute the thread https://github.com/notifications/unsubscribe-auth/ABkuOHZTsZ0Chk_5r_iVG9mxqy-rPKJLks5skB_ogaJpZM4PZ28r .

[atondwal]

Yeah, it shouldn't be too bad. I'll tackle both after my talk tomorrow

On Tue, Sep 19, 2017 at 2:38 PM, Ranjit Jhala notifications@github.com wrote:

Anyways, this "inner" bug seems easy to fix -- figure out where this weird (function real Main.Trace) is being generated, and replace it with the actual sort which should be func(0, [real; Main.Trace])?

On Tue, Sep 19, 2017 at 2:36 PM, Ranjit Jhala jhala@cs.ucsd.edu wrote:

What is this function real Main.Trace?

On Tue, Sep 19, 2017 at 1:11 PM, Anish Tondwalkar < notifications@github.com> wrote:

Unfortunately, there's a bug-within-a-bug. Old version of z3 don't suffer from this monomorphization problem(???) so we can see that under that crash is another

RESULT: ERROR **

---

:1:1-1:1: Error elaborate makeKnowledge failed on: lq_anf$##7205759403792801278##d1ZQ == lam lam_arg##1 : (function real Main.Trace) . Main.$$ (lam_arg##1 : func(0, [real;

Main.Trace])) v##a1u1 with error Cannot unify func(0, [real; Main.Trace]) with (function real Main.Trace) in expression: lam_arg##1 because Cannot cast lam_arg##1 of sort (function real Main.Trace) to incompatible sort func(0, [real; Main.Trace]) in environment Main.$$ := func(2, [func(0, [@(1); @(0)]); @(1); @(0)])

v##a1u1 := real

lq_anf$##7205759403792801278##d1ZQ := func(0, [func(0, [real; Main.Trace]); Main.Trace])

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/ 1090#issuecomment-330659126, or mute the thread https://github.com/notifications/unsubscribe-auth/ABkuOHZTsZ0Chk_5r_ iVG9mxqy-rPKJLks5skB_ogaJpZM4PZ28r .

— You are receiving this because you modified the open/close state. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/1090#issuecomment-330681303, or mute the thread https://github.com/notifications/unsubscribe-auth/AAU8CL-qyC7tFw-LpYhOmF8tTFgWg6Tqks5skDRWgaJpZM4PZ28r .

-- Anish

Q: Why is this email two sentences or less? A: http://two.sentenc.es

[ranjitjhala]

why is this closed? i dont think its fixed?

[ranjitjhala]

Ah right you moved it to FP; still let's keep it open till the other one is fixed...

[ranjitjhala]

I've fixed the first bug (the Either ~~~ Either) business in liquid-fixpoint

https://github.com/ucsd-progsys/liquid-fixpoint/issues/332

via

https://github.com/ucsd-progsys/liquid-fixpoint/pull/333

but the second issue re: makeKnowledge remains, so keeping this open.

[atondwal]

So we're not generating any new exprs in instantiate, so this is being caused by something else altogether:

Knowledge : Foo.Done ~> Foo.Done
Rewrite -is$Foo.Done : is$Foo.Done Foo.Done ~> true
Knowledge : Foo.Done ~> Foo.Done
Rewrite -is$Foo.Fork : is$Foo.Fork Foo.Done ~> false
Knowledge : Foo.Done ~> Foo.Done
Rewrite -is$Foo.New : is$Foo.New Foo.Done ~> false
Knowledge : Foo.Done ~> Foo.Done
Rewrite -is$Foo.Put : is$Foo.Put Foo.Done ~> false
Knowledge : Foo.Done ~> Foo.Done
Rewrite -is$Foo.Get : is$Foo.Get Foo.Done ~> false
Knowledge : Foo.HeapExn ~> Foo.HeapExn
Rewrite -is$Foo.HeapExn : is$Foo.HeapExn Foo.HeapExn ~> true
Knowledge : Foo.HeapExn ~> Foo.HeapExn
Rewrite -is$Foo.Deadlock : is$Foo.Deadlock Foo.HeapExn ~> false
Knowledge : Foo.HeapExn ~> Foo.HeapExn
Rewrite -is$Foo.MultiplePut : is$Foo.MultiplePut Foo.HeapExn ~> false
Knowledge : Foo.Done ~> Foo.Done
Rewrite -is$Foo.Done : is$Foo.Done Foo.Done ~> true
Knowledge : Foo.Done ~> Foo.Done
Rewrite -is$Foo.Fork : is$Foo.Fork Foo.Done ~> false
Knowledge : Foo.Done ~> Foo.Done
Rewrite -is$Foo.New : is$Foo.New Foo.Done ~> false
Knowledge : Foo.Done ~> Foo.Done
Rewrite -is$Foo.Put : is$Foo.Put Foo.Done ~> false
Knowledge : Foo.Done ~> Foo.Done
Rewrite -is$Foo.Get : is$Foo.Get Foo.Done ~> false
Knowledge : Foo.HeapExn ~> Foo.HeapExn
Rewrite -is$Foo.HeapExn : is$Foo.HeapExn Foo.HeapExn ~> true
Knowledge : Foo.HeapExn ~> Foo.HeapExn
Rewrite -is$Foo.Deadlock : is$Foo.Deadlock Foo.HeapExn ~> false
Knowledge : Foo.HeapExn ~> Foo.HeapExn
Rewrite -is$Foo.MultiplePut : is$Foo.MultiplePut Foo.HeapExn ~> false
Knowledge : Foo.Done ~> Foo.Done
Rewrite -is$Foo.Done : is$Foo.Done Foo.Done ~> true
Knowledge : Foo.Done ~> Foo.Done
Rewrite -is$Foo.Fork : is$Foo.Fork Foo.Done ~> false
Knowledge : Foo.Done ~> Foo.Done
Rewrite -is$Foo.New : is$Foo.New Foo.Done ~> false
Knowledge : Foo.Done ~> Foo.Done
Rewrite -is$Foo.Put : is$Foo.Put Foo.Done ~> false
Knowledge : Foo.Done ~> Foo.Done
Rewrite -is$Foo.Get : is$Foo.Get Foo.Done ~> false
Knowledge : Foo.HeapExn ~> Foo.HeapExn
Rewrite -is$Foo.HeapExn : is$Foo.HeapExn Foo.HeapExn ~> true
Knowledge : Foo.HeapExn ~> Foo.HeapExn
Rewrite -is$Foo.Deadlock : is$Foo.Deadlock Foo.HeapExn ~> false
Knowledge : Foo.HeapExn ~> Foo.HeapExn
Rewrite -is$Foo.MultiplePut : is$Foo.MultiplePut Foo.HeapExn ~> false
Knowledge : Foo.Done ~> Foo.Done
Rewrite -is$Foo.Done : is$Foo.Done Foo.Done ~> true
Knowledge : Foo.Done ~> Foo.Done
Rewrite -is$Foo.Fork : is$Foo.Fork Foo.Done ~> false
Knowledge : Foo.Done ~> Foo.Done
Rewrite -is$Foo.New : is$Foo.New Foo.Done ~> false
Knowledge : Foo.Done ~> Foo.Done
Rewrite -is$Foo.Put : is$Foo.Put Foo.Done ~> false
Knowledge : Foo.Done ~> Foo.Done
Rewrite -is$Foo.Get : is$Foo.Get Foo.Done ~> false
Knowledge : Foo.HeapExn ~> Foo.HeapExn
Rewrite -is$Foo.HeapExn : is$Foo.HeapExn Foo.HeapExn ~> true
Knowledge : Foo.HeapExn ~> Foo.HeapExn
Rewrite -is$Foo.Deadlock : is$Foo.Deadlock Foo.HeapExn ~> false
Knowledge : Foo.HeapExn ~> Foo.HeapExn
Rewrite -is$Foo.MultiplePut : is$Foo.MultiplePut Foo.HeapExn ~> false
Knowledge : Foo.Done ~> Foo.Done
Rewrite -is$Foo.Done : is$Foo.Done Foo.Done ~> true
Knowledge : Foo.Done ~> Foo.Done
Rewrite -is$Foo.Fork : is$Foo.Fork Foo.Done ~> false
Knowledge : Foo.Done ~> Foo.Done
Rewrite -is$Foo.New : is$Foo.New Foo.Done ~> false
Knowledge : Foo.Done ~> Foo.Done
Rewrite -is$Foo.Put : is$Foo.Put Foo.Done ~> false
Knowledge : Foo.Done ~> Foo.Done
Rewrite -is$Foo.Get : is$Foo.Get Foo.Done ~> false