Removing errors from the zonker

It seems to me that we don't want the zonker to add error messages. One motivation is that, when reporting an error, we rely on an action stored in

type ErrCtxt = (Bool, TidyEnv -> TcM (TidyEnv, SDoc))

In practice, these actions only do zonking and tidying; it seems the inner action should not be adding errors, while we are already reporting an error. If we remove the ability for the zonker to emit errors, then we avoid this problem.

Currently, the only error we throw in the zonker is when we can't default a concrete type variable. This comes from cases like

f1 :: forall r s (a :: TYPE (r s)). a -> ()
f1 = f1

g1 h = f1 (h ())

f2 :: forall r s t u (a :: TYPE (r s t u)). a -> ()
f2 = f1

g2 h = f2 (h ())

The issue is that we create concrete metavariables r[conc], s[conc], t[conc], u[conc], but because they don't have kind RuntimeRep we don't know how to default them.

However, I would want to say:

• for g1, we can default r[conc] s[conc] as a whole to BoxedRep Lifted (even though technically it could be something else, like r ~ VecRep Vec2, s ~ DoubleElemRep).
• for f2, there is no way to unify r s t u with a concrete RuntimeRep, so we should emit a kind error in f2 (before we even get to g2).

If we implement some logic like this, I imagine we could remove the error.