Nullary operations on GADT with constraints

I am trying to define something similar to Data.Monoid.Ap but as GADT with constraints on the constructors: import Data.Monoid (Ap(..)) -- instance (Monoid a, Applicative f) => Monoid (Ap f a) data Lifted f a where Lift :: (Monoid a, Applicative f) => Ap f a -> Lifted f a One can have a Semigroup instance wherein the constraints are hidden: instance Semigroup (Lifted f a) where (Lift a) <> (Lift b) = Lift (a <> b) This works because by matching on the Lift constructor, the constraint...