Expanding a particular type family in type errors

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
6 messages Options
Reply | Threaded
Open this post in threaded view
|

Expanding a particular type family in type errors

Alexis King
Hi all,

As part of my ongoing rework of arrow notation, I have introduced two wired-in type families, which assist in the typechecking process. The details are not terribly important (you can read the proposal if you’d like for those), but the relevant detail is that equalities of the shape

    ArrowStackTup a ~ b

are produced by the typechecker in key places. ArrowStackTup is one of my wired-in type families, and it’s really an implementation detail. Unfortunately, I often end up with type errors that leak this detail, with expected/actual types like these ones:

    Expected type: ArrowStackTup '[Int] -> Bool
      Actual type: Int -> String

This is quite annoying, as it’s exceedingly rare that these type families actually get stuck, so they can almost always be expanded in type errors. As it happens, `ArrowStackTup '[a]` expands to simply `a`, so the type error I would like to report is this one:

    Expected type: Int -> Bool
      Actual type: Int -> String

Not technically challenging, but I find myself faced with the question of where this special expansion logic ought to go. It seems like it could go in any of several places:

  1. It could be hard-wired into pprType, and perhaps selectively disabled with an -fprint-* flag. This is nice in that it’s universal, but it’s almost certainly a step too far: the casts for ArrowStackTup still end up in Core, and expanding the type synonyms there would be quite confusing.

  2. The expansion could happen in tidyType, since it’s called before reporting an error. But this seems probably even worse than putting it in pprType, since it’s still used in too many places, and it isn’t supposed to actually change the type.

  3. It could be handled as an extra, ad-hoc preprocessing step in reportWanteds. This is much closer to reasonable, though it feels like quite a hack.

  4. A separate error Reporter could catch these errors before the other reporters do and perform the expansion there. But I don’t think this actually makes sense, as the above example demonstrates that ArrowStackTup might be buried inside another type and in fact might not actually be the source of the type error at all!

  5. It could be done last-minute in mkEqErr. But I don’t know if this is too late, and ArrowStackTup could leak into an error through some other code path.

Of those options, the best one I’ve come up with seems to be option 3, an ad-hoc preprocessing step in reportWanteds. Does that seem reasonable? Or is it too much of a kludge?

Thanks,
Alexis

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Expanding a particular type family in type errors

Alexis King
Answering my own question: it looks like cleaning this up in GHC.Tc.Errors is rather impractical—there are just too many types buried inside other datatypes that would have to be updated—so it has to be wired into pprType. Fortunately, I can branch on userStyle to decide whether or not to do the expansion. This still seems like a bit of a hack, but I can’t think of a better way. Do tell me if there’s a better approach!

On May 1, 2020, at 16:36, Alexis King <[hidden email]> wrote:

Hi all,

As part of my ongoing rework of arrow notation, I have introduced two wired-in type families, which assist in the typechecking process. The details are not terribly important (you can read the proposal if you’d like for those), but the relevant detail is that equalities of the shape

    ArrowStackTup a ~ b

are produced by the typechecker in key places. ArrowStackTup is one of my wired-in type families, and it’s really an implementation detail. Unfortunately, I often end up with type errors that leak this detail, with expected/actual types like these ones:

    Expected type: ArrowStackTup '[Int] -> Bool
      Actual type: Int -> String

This is quite annoying, as it’s exceedingly rare that these type families actually get stuck, so they can almost always be expanded in type errors. As it happens, `ArrowStackTup '[a]` expands to simply `a`, so the type error I would like to report is this one:

    Expected type: Int -> Bool
      Actual type: Int -> String

Not technically challenging, but I find myself faced with the question of where this special expansion logic ought to go. It seems like it could go in any of several places:

  1. It could be hard-wired into pprType, and perhaps selectively disabled with an -fprint-* flag. This is nice in that it’s universal, but it’s almost certainly a step too far: the casts for ArrowStackTup still end up in Core, and expanding the type synonyms there would be quite confusing.

  2. The expansion could happen in tidyType, since it’s called before reporting an error. But this seems probably even worse than putting it in pprType, since it’s still used in too many places, and it isn’t supposed to actually change the type.

  3. It could be handled as an extra, ad-hoc preprocessing step in reportWanteds. This is much closer to reasonable, though it feels like quite a hack.

  4. A separate error Reporter could catch these errors before the other reporters do and perform the expansion there. But I don’t think this actually makes sense, as the above example demonstrates that ArrowStackTup might be buried inside another type and in fact might not actually be the source of the type error at all!

  5. It could be done last-minute in mkEqErr. But I don’t know if this is too late, and ArrowStackTup could leak into an error through some other code path.

Of those options, the best one I’ve come up with seems to be option 3, an ad-hoc preprocessing step in reportWanteds. Does that seem reasonable? Or is it too much of a kludge?

Thanks,
Alexis


_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Expanding a particular type family in type errors

Richard Eisenberg-5
I'm afraid I like none of (1)-(5). Important background: if we have type family F a where F Int = Bool, then F Int and Bool are *not* equal in Core. We cannot just change one to the other. Instead, a coercion exists between them.

1. pprType seems a very challenging place to do this, given that pprType works on IfaceTypes, which are not amenable to much of any analysis. Maybe you could do the switcho-changeo before converting to IfaceType. Are your type families closed? Then it's just barely conceivable. If they're open, you won't have the instances available in pprType. Still, this seems like far too much processing to be done in pretty-printing.

2. tidyType really cannot change one type to another unequal one. Chaos will ensue.

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.

4-5. These seem the post plausible. Yes, it's true that calls to ArrowStackTup might leak through, but doing so wouldn't be strictly *wrong*, just suboptimal. So it might be that a best-effort here is good enough.

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.

If you haven't yet come across it, see the normaliseType function, which evaluates type families as much as possible.

I hope this helps!
Richard

On May 2, 2020, at 12:13 AM, Alexis King <[hidden email]> wrote:

Answering my own question: it looks like cleaning this up in GHC.Tc.Errors is rather impractical—there are just too many types buried inside other datatypes that would have to be updated—so it has to be wired into pprType. Fortunately, I can branch on userStyle to decide whether or not to do the expansion. This still seems like a bit of a hack, but I can’t think of a better way. Do tell me if there’s a better approach!

On May 1, 2020, at 16:36, Alexis King <[hidden email]> wrote:

Hi all,

As part of my ongoing rework of arrow notation, I have introduced two wired-in type families, which assist in the typechecking process. The details are not terribly important (you can read the proposal if you’d like for those), but the relevant detail is that equalities of the shape

    ArrowStackTup a ~ b

are produced by the typechecker in key places. ArrowStackTup is one of my wired-in type families, and it’s really an implementation detail. Unfortunately, I often end up with type errors that leak this detail, with expected/actual types like these ones:

    Expected type: ArrowStackTup '[Int] -> Bool
      Actual type: Int -> String

This is quite annoying, as it’s exceedingly rare that these type families actually get stuck, so they can almost always be expanded in type errors. As it happens, `ArrowStackTup '[a]` expands to simply `a`, so the type error I would like to report is this one:

    Expected type: Int -> Bool
      Actual type: Int -> String

Not technically challenging, but I find myself faced with the question of where this special expansion logic ought to go. It seems like it could go in any of several places:

  1. It could be hard-wired into pprType, and perhaps selectively disabled with an -fprint-* flag. This is nice in that it’s universal, but it’s almost certainly a step too far: the casts for ArrowStackTup still end up in Core, and expanding the type synonyms there would be quite confusing.

  2. The expansion could happen in tidyType, since it’s called before reporting an error. But this seems probably even worse than putting it in pprType, since it’s still used in too many places, and it isn’t supposed to actually change the type.

  3. It could be handled as an extra, ad-hoc preprocessing step in reportWanteds. This is much closer to reasonable, though it feels like quite a hack.

  4. A separate error Reporter could catch these errors before the other reporters do and perform the expansion there. But I don’t think this actually makes sense, as the above example demonstrates that ArrowStackTup might be buried inside another type and in fact might not actually be the source of the type error at all!

  5. It could be done last-minute in mkEqErr. But I don’t know if this is too late, and ArrowStackTup could leak into an error through some other code path.

Of those options, the best one I’ve come up with seems to be option 3, an ad-hoc preprocessing step in reportWanteds. Does that seem reasonable? Or is it too much of a kludge?

Thanks,
Alexis

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Expanding a particular type family in type errors

Alexis King
On May 4, 2020, at 04:25, Richard Eisenberg <[hidden email]> wrote:

1. pprType seems a very challenging place to do this, given that pprType works on IfaceTypes, which are not amenable to much of any analysis. Maybe you could do the switcho-changeo before converting to IfaceType. Are your type families closed? Then it's just barely conceivable. If they're open, you won't have the instances available in pprType. Still, this seems like far too much processing to be done in pretty-printing.

You are right—I discovered this after my previous email. But they are more than closed: they are BuiltInSynFams, so they can be expanded easily by isBuiltInSynFamTyCon_maybe + sfMatchFam.

2. tidyType really cannot change one type to another unequal one. Chaos will ensue.

Agreed.

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.

4-5. These seem the post plausible. Yes, it's true that calls to ArrowStackTup might leak through, but doing so wouldn't be strictly *wrong*, just suboptimal. So it might be that a best-effort here is good enough.

I think 4 makes sense for situations where the type family is stuck, since in that case we can’t just expand it away, and there is a more useful error message we can report. Maybe 5 makes more sense for the other cases, but I started down that path and it’s quite awkward.

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. If that weren’t true, I could drop them completely. (The proposal discusses that in a little more detail, as do some Notes in my WIP MR.)

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. It only becomes sketchy from the Core point of view, and I’m totally fine to not do any of this magic there!

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.

Alexis

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Expanding a particular type family in type errors

Richard Eisenberg-5


On May 4, 2020, at 8:17 PM, Alexis King <[hidden email]> 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


_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Expanding a particular type family in type errors

Alexis King
> On May 5, 2020, at 04:00, Richard Eisenberg <[hidden email]> wrote:
>
> reportWanteds reports errors, yes, but it also fills in deferred type errors. [snip] 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.

Yes, that does make sense; thank you for the explanation.

> 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.

You’re right that this might be feasible, but I think it would be awkward, and it probably would break down just often enough to be an unsatisfying solution.

> 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.

If you think this is a reasonable idea, I’m happy to give it a shot—it definitely seems like the nicest way to do it to me. I’ll try it out and report back if I run into any trouble. Thanks again!

Alexis
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs