I ran a program that fiddles with bits, which went hilariously wrong. The behaviour I expected for "true" happened for "false", and vice versa. I was using

    data Two : Set where tt ff : Two
    {-# BUILTIN BOOL Two #-}
    {-# BUILTIN FALSE ff #-}
    {-# BUILTIN TRUE tt #-}

I got the correct behaviour by doing this instead:

    data Two : Set where tt ff : Two
    {-# COMPILE GHC Two = data Bool (True | False) #-}

I also got the correct behaviour by reordering the constructors:

    data Two : Set where ff tt : Two
    {-# BUILTIN BOOL Two #-}
    {-# BUILTIN FALSE ff #-}
    {-# BUILTIN TRUE tt #-}

The order of BUILTIN FALSE and BUILTIN TRUE seems not to matter, but the order of ff and tt seems to be the key.

On the face of it, there would seem to be something a little astray.