Polymorph currying in class constraint or using forall quantification in class constraints

The following code does not work because a is not used. But there is an instance that works for any a.

module test

:: T a = T a

class c a v :: a -> v Int
instance c a T where c a = T 42

fun :: v Int | c a v
fun = c True

Start :: T Int
Start = fun

However, it works if I change the definition to, but now the function is not as general anymore, I might want to reuse it.

fun :: v Int | c Bool v

Moreover, say I want to make a function that can do this for a class constraint (hypothetical syntax)

instance c a T where c a = T 42

fun :: v Int | c (a | zero a) v
fun = c zero

What are the possibilities to possibly allow these constructions in the future.