Daniel Fischer
Well, the context is not redundant, that's the crux.
You can specify the type `Source v a` even when there is no `Variable v` instance [whether you use DatatypeContexts - which, again, are pretty useless because they don't do what one would expect - or GADTs]. And such a type is inhabited by bottom, you just can't create non-bottom values of such a type.
Hence the `Variable v` context gives additional information that is needed for the instance.
I'm not following - perhaps you could give a practical example? I'm trying to understand the flaw in this: 1) The compiler sees that a Source v a can only be created when v is a variable. 2) Whenever Source v a is used, the compiler should understand that v is a variable without me having to remind it.