invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
this resulted in a subtle soundness bug in Sledgehammer -- introduced by the transition to FOF
{-# OPTIONS_GHC -fglasgow-exts #-}
module Example where {
data Queue a = AQueue [a] [a];
empty :: forall a. Queue a;
empty = AQueue [] [];
dequeue :: forall a. Queue a -> (Maybe a, Queue a);
dequeue (AQueue [] []) = (Nothing, AQueue [] []);
dequeue (AQueue xs (y : ys)) = (Just y, AQueue xs ys);
dequeue (AQueue (v : va) []) =
let {
(y : ys) = reverse (v : va);
} in (Just y, AQueue [] ys);
enqueue :: forall a. a -> Queue a -> Queue a;
enqueue x (AQueue xs ys) = AQueue (x : xs) ys;
}