A deliberately minimal, forward-safe TestEquality (and TestCoercion) synthesizer.

It handles exactly the unambiguous "finite singleton" GADT: a one-parameter type whose every constructor is nullary, has no existentials, and pins the parameter to a ground type:

data T a where { TInt :: T Int; TBool :: T Bool }

For these the lawful behaviour is forced: testEquality x y is Just Refl exactly when the type indices of x and y coincide (NOT when they are the same constructor: two constructors pinning the same type are equal), and Nothing otherwise. Because that is the only law-abiding implementation, it can never disagree with a future, more general design, so it commits us to nothing. Anything outside the subset is refused.