haskell - Conversion between different eDSLs (different type class constraints)

I'm trying to "compile" a simple eDSL to the Atom language. A problem that arises here is, that the type class constraints on my types/functions do not match those of the Atom language.

One eDSL which compiles to Atom is copilot, which also has this very same problem an solves it in a rather verbose way. What follows is a simplified version of the involved datatypes:

{-# LANGUAGE GADTs #-}
data Type a where
TFloat :: Type Float
data Op1 a b where
Neg :: Type a -> Op1 a a
class NumE a where
instance NumE Float
data Exp e where
ENeg :: NumE a => Exp a -> Exp a

Type and Op1 are part of the new eDSL, NumE and Exp belong to the compilation target. To convert between the eDSLs at some point I need a function op2exp with the following type:

op2exp :: Op1 a b -> Exp a -> Exp b

Now the way Atom handles this is rather verbose:

data NumEInst e = NumE e => NumEInst
numEInst :: Type a -> NumEInst a
numEInst TFloat = NumEInst
op2exp :: Op1 a b -> Exp a -> Exp b
op2exp op = case op of
Neg t -> case numEInst t of NumEInst -> ENeg

This works, but is quite cumbersome and full of repetition.

Question:

Is there a way, maybing using new language features, to write the op2exp function in an easier way? Ideally something along the lines of:

op2exp (Neg t) = ENeg

Ideally, I wouldn't even need the Type data type and have the compiler figure out that all the types match.