Wouldn't that make `F` a constant type family, and so one could just skip the `a` parameter?   Anyway, if there was a way to assert something like that about a type-function, than there would be no problem.   When something like that happens (i.e., GHC figures out that it does not know how to instantiate a type variable, but it is sure that the actual instantiation does not matter), GHC instantiates the variable a special type called `Any`, which has a very polymorphic kind.

By the way, Simon recently reworked the ambiguity checker in GHC, and now HEAD correctly rejects `foo` as being ambiguous (the new ambiguity check uses exactly what's in your example: a value `f :: S` is ambiguous, if `g :: S; g = f` results in an error).

-Iavor