Is it possible to store a GADT inside a State monad transformer?

Question

Say that I have got a GADT like this:

data Term a where
  Lit    :: a -> Term a
  Succ   :: Term Int -> Term Int
  IsZero :: Term Int -> Term Bool
  If     :: Term Bool -> Term a -> Term a -> Term a

Is it possible to store Succ (Lit 2) and IsZero (Succ (Lit 2)) inside the State monad transformer, as a value of the internal state?

The issue here being those two are of different types, and I don't know how the s of StateT s m a should be typed.

Edit: ATerm solved the initial question of how to store different GADT in the state, the issue now is since the type is lost it seemed impossible to compare the old and new state.

Edit: Final answer.

After going back and forth with @luqui, here's the full code snippet that answers this question.

Feel free to fork this repl and have a try.

{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}

import Data.Typeable

data Term a where
  Lit    :: a -> Term a
  Succ   :: Term Int -> Term Int
  IsZero :: Term Int -> Term Bool
  If     :: Term Bool -> Term a -> Term a -> Term a

deriving instance (Eq a) => Eq (Term a)

data ATerm where
  ATerm :: (Typeable a, Eq a) => Term a -> ATerm

instance Eq ATerm where
    ATerm t == ATerm u
        | Just t' <- cast t = t' == u
        | otherwise = False

main :: IO ()
main = return ()

Answer 1

Yes, you can use an existential

data ATerm where
   ATerm :: Term a -> ATerm

which is a monotype that stores "a Term of any type".

However you should be aware that you will lose the type information, which I have a hunch will not cause a problem in your case. If you do need to recover it, you will need to add some Typeable constraints or some other trick—hard to say without more context on what you are doing.

EDIT

To get the type information back, you will need to include it in ATerm

data ATerm where
    ATerm :: (Typeable a, Eq a) => Term a -> ATerm

Sadly, this change might cause the Typeable constraint to infect a fair amount of your code. That's just how it goes. We also include Eq a, since if we are comparing ATerms and do find that their types are the same, we will need to compare on that type.

Then to compare two ATerms, you first need to compare their types, then their values. This can be done with the Typeable library.

instance Eq ATerm where
    ATerm t == ATerm u
        | Just t' <- cast t = t' == u
        | otherwise = False

Luckily, your Term GADT doesn't hide any types. If you had a case like, for example

data Term a where
    ...
    Apply :: Func a b -> Term a -> Term b

you would need to add Typeable also to any hidden variables (variables that don't appear in the result type)

    Apply :: (Typeable a) => Func a b -> Term a -> Term b

Roughly, if you want to compare types, you need to have a Typeable constraint on them somewhere.