Panic with ADTs

[atondwal]

:1:1-1:1: Error
  PANIC: Please file an issue at https://github.com/ucsd-progsys/liquid-fixpoint
Unknown func-sort: (Main.Map Int (Main.Maybe Real)) : (Main.Maybe (Main.Maybe Real)) for (apply : func(0, [(Main.Map int (Main.Maybe real));
                  (Main.Maybe (Main.Maybe real))])) ((apply : func(0, [int;
                                                                       (Main.Map int @(44));
                                                                       (Main.Maybe @(44))])) (Main.find : func(0, [int;
                                                                                                                   (Main.Map int @(44));
                                                                                                                   (Main.Maybe @(44))])) ((lqdc##select##IVar#
#1 : func(0, [(Main.IVar real);

              int])) ((lqdc##select##Get##1 : func(0, [Main.Trace;

                                                       (Main.IVar real)])) (((apply : func(0, [(Tuple Main.Trace [Main.Trace]);

                                                                                               Main.Trace])) (lqdc##select##(,)##1 : func(0, [(Tuple Main.Trac
e [Main.Trace]);

                                                                                                                                              Main.Trace])) (x
##a1yh : (Tuple Main.Trace [Main.Trace])) : Main.Trace) : Main.Trace) : (Main.IVar real)) : int) : func(0, [(Main.Map int @(44));

                                                                                                            (Main.Maybe @(44))])) (lq_tmp$x##8270 : (Main.Map
int (Main.Maybe real)))

using LH on file:

#!/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 (..))
import System.Process
type Heap = Map Int (Maybe Double)

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

-- | Partial ordering on the `Heap`. Read as "definedness"
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} @-}

-- Maybe
--------
data Either a b = Left a | Right b
data Maybe a = Just a | Nothing

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

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

-- 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 _ [] = []

-- 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

{-@ reflect step @-}
step :: (Trace, [Trace]) -> Map Int [Double -> Trace] -> Int ->  Map Int (Maybe Double)
     -> Either Exn ([Trace], Map Int [Double -> Trace], Int,  Map Int (Maybe Double))
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)

-- Theorems
-------------

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

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

{-@
 theoremMonotonic :: a:(Trace,[Trace]) -> b:( Map Int [Double -> Trace]) -> c:Int -> h:Heap
                  -> h':{v:Heap | v = select4of4 (selectRight (step a b c h))}
                  -> Prop ( HeapLte h h' )
@-}
theoremMonotonic :: (Trace, [Trace]) ->  Map Int [Double -> Trace] -> Int -> Heap -> Heap -> ()
theoremMonotonic x y = undefined

[ranjitjhala]

Same issue as https://github.com/ucsd-progsys/liquidhaskell/issues/1086 i.e. lack of alias expansion and happily fixed by https://github.com/ucsd-progsys/liquidhaskell/pull/1087

[atondwal]

This isn't actually completely fixed; it goes away after we turn off instantiation, but the file above, as written, (with instantiation on) still exposes the bug

[ranjitjhala]

Ok I think it's a good idea for you to try to fix this one yourself (to familiarize yourself with the code). The issue is that we need to know all the monomorphic sorts at which polymorphic functions are instantiate she. look for the function called apply sorts in fixed point and then follow the links forwards and backwards from there. Let me know if you get stuck?

On Sat, Sep 16, 2017 at 9:23 AM Anish Tondwalkar notifications@github.com wrote:

Reopened #326 https://github.com/ucsd-progsys/liquid-fixpoint/issues/326 .

— 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/liquid-fixpoint/issues/326#event-1252207992, or mute the thread https://github.com/notifications/unsubscribe-auth/ABkuOJFMdCHivmntC98TUXsjLueLEw9hks5si_WEgaJpZM4PX8Yh .

[ranjitjhala]

Wondering if this was related to #335? @atondwal Can you check if it has been fixed by recent changes?

[atondwal]

Hmm... seems that this is hitting something else now.

LiquidHaskell Copyright 2013-17 Regents of the University of California. All Rights Reserved.

**** DONE:  A-Normalization ****************************************************

**** DONE:  annotate ***********************************************************

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

 <no source information>:0:0: Error: Bad Data Specification
 GHC.Types.[] :: Mismatch in number of type variables