Re: Expanding a particular type family in type errors

On May 4, 2020, at 8:17 PM, Alexis King wrote:

...

3. reportWanteds will have a similar problem: if we have -fdefer-type-errors, then reportWanteds may actually happen before desugaring and execution, and we can't have a type magically changed in the process. Doing so will lead to a core-lint error.

I don’t totally understand this point—I thought reportWanteds just printed things! It sounds like you’re saying it does something more, but I don’t immediately see what.

reportWanteds reports errors, yes, but it also fills in deferred type errors. By the time reportWanteds sees an error, that error takes the form of an unsolved Wanted constraint. Every unsolved Wanted corresponds to an evidence Id (that is, variable) in the desugared program that should contain the evidence. (For example, we might have $dEq which should eventually have a dictionary for Eq Int.) If a Wanted is unsolved by the time it gets to reportWanteds, it will never be solved. Instead, if we are deferring errors, we must let-bind the Id to *something* to produce Core. So we bind it to a call to `error` (roughly) with the same error message that would have been printed if we weren't deferring errors. It's a bit awkward that a function called reportWanteds does this, but it actually makes good sense, because reportWanteds knows the text that should be in the runtime error call.

...

Another possibility: when these ArrowStackTup calls are born, do you already sometimes know the arguments? That is, there must be some code that produces the ArrowStackTup '[a] call -- could it just special-case an '[a] argument and produce `a` instead? Then, the ArrowStackTup family is used only when you have an abstract argument, which might be considerably rarer.

I’m afraid not. The entire reason I have the type families in the first place is that the arguments are not, in general, fully known when the equality constraint is emitted.

You say that they're not, in general, fully known. But are they often known in practice? My suggestion here isn't to remove the type families entirely, but maybe to short-circuit around them. If that's often possible, it takes some pressure off fixing the pretty-printing.

It’s all a bit frustrating, because it’s really not like printing things this way is “cheating” or somehow morally wrong—these types are nominally equal, so from the user’s point of view they are completely interchangeable.

This is a good point -- I don't think I quite absorbed it last time around. I had considered the change-before-printing quite strange. But you're right in that you're interchanging two nominally-equal types, and that's just fine.

Really, I think this morally belongs in the printer. This is just a display thing, nothing more. I want to be able to say “these type families are not something the user is likely to understand, so when printing error messages, expand them if at all possible.” But it’s very difficult to do that currently given the way pprType goes through IfaceType, since you’ve lost the necessary information by that point.

I wonder if we should have a preprocessTypeForPrinting :: DynFlags -> Type -> Type function. This could be run *before* the conversion to IfaceType. It could handle both your new idea and the existing idea for -f(no-)print-explicit-runtime-reps. The supplied DynFlags could be gotten from sdocWithDynFlags, I think. I bet that once we have this facility working, we'll find more uses for it. I'm now considerably happier than I was about doing this in the printing pipeline, if you think you see how it could be done. Richard

Alexis