Nonrecursive variant fields that are not leftmost can result in an internal typechecking error

[jazullo]

(Tested on commit 2fc0301, examples do not execute correctly due to previous issue #194)
Consider these two programs:

data Tree = E | T Int Tree Tree

empty :: Tree -> Bool
empty t = case t of
  E -> True
  T x y z -> False

insert :: Tree -> Int -> Tree
insert t x = case t of
  E -> T x E E
  T v t1 t2 ->
    if v == x then t
    else if v < x then T v t1 (insert t2 x)
    else T v (insert t1 x) t2

gibbon_main = 
  let
    _ = printPacked (insert (insert E 1) 2)
  in ()

data Tree = E | T Tree Int Tree

empty :: Tree -> Bool
empty t = case t of
  E -> True
  T x y z -> False

insert :: Tree -> Int -> Tree
insert t x = case t of
  E -> T E x E
  T t1 v t2 ->
    if v == x then t
    else if v < x then T t1 v (insert t2 x)
    else T (insert t1 x) v t2

gibbon_main = 
  let
    _ = printPacked (insert (insert E 1) 2)
  in ()

The only difference between these two programs is that the second permutes the first two fields of the variant so that the integer is in the middle. The first program is able to compile without any type error. The second program results in the following error:

$ cabal v2-exec gibbon -- --packed --no-gc --to-exe ../test/bst.hs

gibbon: Var end_x_25_83_132 not found. Checking:
: VarE "end_x_25_83_132"
CallStack (from HasCallStack):
  error, called at src/Gibbon/L3/Typecheck.hs:824:21 in gibbon-0.2-inplace:Gibbon.L3.Typecheck

It appears that a necessary variable is missing from L3 when compiling the permuted program.

[vidsinghal]

Hi @jazullo, for now can you make the scalar Int a packed Integer

data Integer = I Int 

It is in-efficient but will at least ensure correct programs I think.

using scalars with packed types has bugs in gibbon. Especially if its after the packed fields.

could you try to check out to this branch and see if the programs compile after making it a packed integer and also check correctness?

[vidsinghal]

example modified code:

data Integer = I Int
data Tree = E | T Integer Tree Tree


empty :: Tree -> Bool
empty t = case t of
  E -> True
  T x y z -> False


getInteger :: Integer -> Int 
getInteger val = case val of 
      I v -> v

insert :: Tree -> Integer -> Tree
insert t x = case t of
    E -> T x E E
    T v t1 t2 -> let xx = getInteger x
                     vv = getInteger v
                   in if (vv == xx) then t
                      else if (vv < xx) then T v t1 (insert t2 x)
                      else T v (insert t1 x) t2