Heapster programs <<loop>> when SAW is built with GHC 9.0+ (but not with GHC 8.10)

[RyanGlScott]

After the goal sequents patch (#1689), the following simple Heapster program loops instead of terminating:

// column.c
typedef enum {
    ColumnA = 0,
    ColumnB,
} Column;

int is_column_a(Column c) {
  return c == ColumnA;
}

// column.saw

// bug.saw
enable_experimental;

env <- heapster_init_env "column" "column.bc";

heapster_define_perm env "int32" " " "llvmptr 32" "exists x:bv 32.eq(llvmword(x))";

heapster_define_perm env "Column" ""
    "llvmptr 32"
    "eq(llvmword(0)) or eq(llvmword(1))";

heapster_typecheck_fun env "is_column_a"
    "().arg0:Column<> -o ret:int32<>";

First, compile column.c:

$ clang-10 -emit-llvm -c column.c -o column.bc

Prior to the goal sequents patch, this would terminate:

$ saw bug.saw



[16:20:56.714] Loading file "/home/rscott/Documents/Hacking/Haskell/sandbox/saw-script/bug.saw"

After the goal sequents patch, however, this happens:

$ saw bug.saw



[16:21:19.728] Loading file "/home/rscott/Documents/Hacking/Haskell/sandbox/saw-script/bug.saw"
[16:21:20.388] <<loop>>

[RyanGlScott]

Upon further investigation, this has nothing to do with the goal sequents patch (#1742) at all. Rather, it is due to my GHC version: I was using GHC 9.0 to compile SAW. It turns out that the example above will <<loop>> when SAW is compiled with GHC 9.0 or 9.2 (using the experimental #1717 PR), but it will not loop when compiled with GHC 8.10.7. Moreover, I have confirmed this to be the case when building SAW before and after #1742. Our CI only tests using GHC 8.10.7, which is why we never noticed this in the heapster-tests test suite before.

I suppose we should report this to the GHC issue tracker, although the thought of minimizing the code in SAW makes me a little squeamish. At the very least, I'll update the title of this issue accordingly.

[RyanGlScott]

I have filed GHC#22492 for this issue upstream.

[RyanGlScott]

With Matthew Pickering's invaluable help on GHC#22492, I have determined that this is not a bug in GHC, but rather a series of unfortunate (but expected) behaviors in the hobbits library. I'll recap this comment which gets to the heart of the issue, discussing the interaction between TemplateHaskell and INCOHERENT instances in hobbits. Here is a minimized example that doesn't assume any prior knowledge of hobbits:

{-# LANGUAGE Haskell2010 #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE UndecidableInstances #-}
module Main (main) where

data P a = MkP
instance Show (P a) where
  show MkP = "MkP"

class C a where
  m :: P a

class C1 a where
  m1 :: P a

instance {-# INCOHERENT #-} C1 a => C a where
  m = m1

instance C1 Int where
  m1 = m

$(return [])

instance C Int where
  m = MkP

main :: IO ()
main = print $ m1 @Int

Somewhat surprisingly, this program will terminate on GHC 8.10:

$ ghc-8.10 AllInOneModule.hs -fforce-recomp && ./AllInOneModule
[1 of 1] Compiling Main             ( AllInOneModule.hs, AllInOneModule.o, AllInOneModule.dyn_o )
Linking AllInOneModule ...
MkP

But not on GHC 9.0 or later:

$ ghc-9.0 AllInOneModule.hs -fforce-recomp && ./AllInOneModule
[1 of 1] Compiling Main             ( AllInOneModule.hs, AllInOneModule.o, AllInOneModule.dyn_o )
Linking AllInOneModule ...
AllInOneModule: <<loop>>

The root cause of this difference is that GHC 9.0 changed the behavior of Template Haskell declaration splices such that any declarations before a splice (such as $(return []) above) cannot see any declarations after the splice. Usually, this only affects whether programs compile or not, but in this particular case, the presence of $(return []) actually affects the runtime behavior:

1. The C1 Int instance defines m1 = m, so this requires a C Int instance to typecheck.

2. Which C Int should be used? There are two possible options: the incoherent C a instance, as well as the non-incoherent C Int instance.

   Prior to GHC 9.0, GHC would see both instances, and it would end up picking the non-incoherent C Int instance, which simply returns MkP. On GHC 9.0 or later, however, GHC will only see the incoherent C a instance! This is because the non-incoherent C Int instance is separated by the $(return []) splice, so GHC cannot see this instance when typechecking the C1 Int instance. As a result, GHC picks the incoherent C a instance, which creates a cyclic definition that loops at runtime.

In the actual hobbits library, C is named NuMatching, and C1 is named NuMatchingAny1. To fix the issue, we will need to change the hobbits library in some way or another:

1. One way is to move the instances around such that instances like C Int are always put in the same declaration group as C1 Int (or in a declaration group that precedes C1 Int). This is somewhat tedious, and moreover, you have to be careful to ensure that you do not accidentally "cut off" any instances like in the program above, as GHC will not warn you about this.
2. Matthew Pickering suggests an alternative patch to hobbits here that removes the INCOHERENT instance entirely. Instead, he defines NuMatchingAny1 (i.e., C1) to have a quantified superclass involving NuMatching (i.e., C), which makes it simple to define NuMatchingAny1 instances in terms of NuMatching instances. This requires a fair bit of code churn, but it avoids the possibility of accidentally introducing an infinite loop at runtime, which is a nice benefit.

Of the two possible ways to fix this issue, I like (2) the best. Does this sound agreeable, @eddywestbrook?

[eddywestbrook]

@RyanGlScott I think you're right, that choice 2 sounds like the right approach. NuMatchingAny1 f is really meant to capture the idea that there is a NuMatching (f a) instance for every type a, so it makes sense to use quantification over a in some fashion.