f :: forall t. Foo (t -> Bar Integer) => t -> Integer
g :: forall t. Foo (t -> Bar ()) => t -> Integer
and their definitions use TypeApplications and ScopedTypeVariables to declare the Foo instance to use, since it’s ambiguous. I cannot write a type synonym Fubar…
type Fubar i = forall t. Foo (t -> Bar i) => t -> Integer
…since this will no longer bind t in the type declarations.
Can I somehow extract or bubble up the t variable? Could a type synonym have an additional output channel that can be bound?
I don’t know because I don’t really understand why you are trying to do this. Could you elaborate a little, perhaps pasting a complete example of what you really want to achieve?
I’ve also tried to figure this out for some time. My motivation was the use in backpack signatures where it is even more important to be able to do this. For example take the signature which is like the Semigroup class:
type A
append :: A -> A -> A
This signature cannot be instantiated by polymorphic lists because you would need to write:
type A = [a] -- where is 'a' bound?
append = (++)
But that fails to compile.
The only workaround I could come up with is using type classes with equality constraints as superclasses. Here’s what I mean:
class A a where
append :: a -> a -> a
Which can be instantiated by the module:
class A a where
append :: a -> a -> a
instance a ~ [b] => A a where
append = (++)
You might ask why even use backpack modules at all at this point, because the existing Semigroup class is already very similar. The advantage of this approach is that the A constraint is guaranteed to be resolved at compile time, so it will never be translated to dictionary passing. The disadvantage is that it now is specialized to a single type (the type of lists).
So, I would really also like a nicer way to float out type variables.