Note [Coverage condition for injective type families]

The Injective Type Families paper describes how we can tell whether
or not a type family equation upholds the injectivity condition.
Briefly, consider the following:

  type family F a b = r | r -> a      -- NB: b is not injective

  type instance F ty1 ty2 = ty3

We need to make sure that all variables mentioned in ty1 are mentioned in ty3
that's how we know that knowing ty3 determines ty1. But they can't be
mentioned just anywhere in ty3: they must be in *injective* positions in ty3.
For example:

  type instance F a Int = Maybe (G a)

This is no good, if G is not injective. However, if G is indeed injective,
then this would appear to meet our needs. There is a trap here, though: while
knowing G a does indeed determine a, trying to compute a from G a might not
terminate. This is precisely the same problem that we have with functional
dependencies and their liberal coverage condition. Here is the test case:

  type family G a = r | r -> a
  type instance G [a] = [G a]
  [W] G alpha ~ [alpha]

We see that the equation given applies, because G alpha equals a list. So we
learn that alpha must be [beta] for some beta. We then have

  [W] G [beta] ~ [[beta]]

This can reduce to

  [W] [G beta] ~ [[beta]]

which then decomposes to

  [W] G beta ~ [beta]

right where we started. The equation G [a] = [G a] thus is dangerous: while
it does not violate the injectivity assumption, it might throw us into a loop,
with a particularly dastardly Wanted.

We thus do what functional dependencies do: require -XUndecidableInstances to
accept this.

Checking the coverage condition is not terribly hard, but we also want to produce
a nice error message. A nice error message has at least two properties:

1. If any of the variables involved are invisible or are used in an invisible context,
we want to print invisible arguments (as -fprint-explicit-kinds does).

2. If we fail to accept the equation because we're worried about non-termination,
we want to suggest UndecidableInstances.

To gather the right information, we can talk about the *usage* of a variable. Every
variable is used either visibly or invisibly, and it is either not used at all,
in a context where acceptance requires UndecidableInstances, or in a context that
does not require UndecidableInstances. If a variable is used both visibly and
invisibly, then we want to remember the fact that it was used invisibly: printing
out invisibles will be helpful for the user to understand what is going on.
If a variable is used where we need -XUndecidableInstances and where we don't,
we can similarly just remember the latter.

We thus define Visibility and NeedsUndecInstFlag below. These enumerations are
*ordered*, and we used their Ord instances. We then define VarUsage, which is just a pair
of a Visibility and a NeedsUndecInstFlag. (The visibility is irrelevant when a
variable is NotPresent, but this extra slack in the representation causes no
harm.) We finally define VarUsages as a mapping from variables to VarUsage.
Its Monoid instance combines two maps, using the Semigroup instance of VarUsage
to combine elements that are represented in both maps. In this way, we can
compositionally analyze types (and portions thereof).

To do the injectivity check:

1. We build VarUsages that represent the LHS (rather, the portion of the LHS
that is flagged as injective); each usage on the LHS is NotPresent, because we
have not yet looked at the RHS.

2. We also build a VarUsage for the RHS, done by injTyVarUsages.

3. We then combine these maps. Now, every variable in the injective components of the LHS
will be mapped to its correct usage (either NotPresent or perhaps needing
-XUndecidableInstances in order to be seen as injective).

4. We look up each var used in an injective argument on the LHS in
the map, making a list of tvs that should be determined by the RHS
but aren't.

5. We then return the set of bad variables, whether any of the bad
ones were used invisibly, and whether any bad ones need -XUndecidableInstances.
If -XUndecidableInstances is enabled, than a var that needs the flag
won't be bad, so it won't appear in this list.

6. We use all this information to produce a nice error message, (a) switching
on -fprint-explicit-kinds if appropriate and (b) telling the user about
-XUndecidableInstances if appropriate.