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 defaultr[conc] s[conc]
as a whole toBoxedRep Lifted
(even though technically it could be something else, liker ~ VecRep Vec2
,s ~ DoubleElemRep
). - for
f2
, there is no way to unifyr s t u
with a concreteRuntimeRep
, so we should emit a kind error inf2
(before we even get tog2
).
If we implement some logic like this, I imagine we could remove the error.