Better error messages by adding impossible instances

[tomjaguarpaw]

It was raised on Reddit that the error for 1 + [2, 3] is inscrutable:

Prelude> 1+[2,3]

<interactive>:1:1: error:
    • Non type-variable argument in the constraint: Num [a]
      (Use FlexibleContexts to permit this)
    • When checking the inferred type
        it :: forall a. (Num a, Num [a]) => [a]

I think the ultimate problem is, rather than any particular processing that the compiler does of error messages, that instance Num [a] should be explicitly forbidden rather the left unspecified. That is, the following seems to read much better

> 1 + [2,3]
<interactive>:7:1: error:
    • [a] is not an instance of Num
    • When checking the inferred type
        it :: forall a. ((TypeError ...), Num a) => [a]

which I achieve with

> :set -XUndecidableInstances -XTypeFamilies -XDataKinds -XTypeOperators
> import GHC.TypeLits
> import Data.Kind
> type family E t :: Constraint
> type instance E [a] = TypeError (ShowType [a] :<>: Text " is not an instance of Num")
> instance E [a] => Num [a] where
<interactive>:6:10: warning: [-Wmissing-methods]
...

Ultimately this would need to go through the CLC process, but I'm presenting it to the error-messages first to receive their expert opinion on whether this change would be worthwhile.

[MorrowM]

The error message is different in GHC 9.2.1 because of GHC2021, which I think is something to note:

$ ghci-9.2 -ignore-dot-ghci
GHCi, version 9.2.1: https://www.haskell.org/ghc/  :? for help
ghci> 1+[2,3]

<interactive>:1:1: error:
    • No instance for (Num [Integer]) arising from a use of ‘it’
    • In the first argument of ‘print’, namely ‘it’
      In a stmt of an interactive GHCi command: print it

[tomjaguarpaw]

Yes, because FlexibleContexts is part of GHC2021. That said, I didn't know that GHC2021 was enabled by default in 9.2. Dubious choice!

[goldfirere]

I'm not really excited about declaring impossible instances. What if someone wants one? Maybe I want "one" + "two" == "three"? I suppose even with your illegal instance, I could do this via an overlapping instance.

Instead, I would be happier with adding custom logic somewhere to produce good error messages in common cases. That is, instead of solving this problem by adding custom logic in a library (where "custom logic" is the code you pasted above), we add custom logic to an error-reporter (today: GHC; maybe tomorrow: HLS). I think that we have been too hesitant to add specialized logic to GHC around common error cases, like those arising from overloaded numbers.

[MorrowM]

In this particular case, I don't think we even need a special case. I think the error that GHC gives when FlexibleContexts is turned on is serviceable (and can be improved by the more general #5 perhaps). Could this not be fixed by making GHC complain about FlexibleContexts only when it can satisfy the constraint?

[tomjaguarpaw]

Certainly I think there's room for GHC to actually try a suggestion it is considering showing to the user and see if it really improves things, before actually showing it.

[MorrowM]

I think something similar to #5 would work better here than making it impossible. Something like:

Main.hs:6:5: error:
    • Expected a number, but got a list instead.
    • No instance for (Num [a0]) arising from a use of ‘+’
    • This would be accepted if there were an `instance Num [a0]',
      but you probably do not want to make this orphan instance for a type
      you did not define
    • In the expression: 1 + [2, 3]
      In an equation for ‘x’: x = 1 + [2, 3]

It is a bit trickier here as we don't have a concrete type for the list.

[noughtmare]

@goldfirere

I'm not really excited about declaring impossible instances. What if someone wants one? Maybe I want "one" + "two" == "three"? I suppose even with your illegal instance, I could do this via an overlapping instance.

I think there are some cases where you can prove that no lawful instance exists for a certain type. I think it is fine to make unlawful instances illegal. Your example is probably also unlawful, so I see no issues with making it impossible or very hard to define.

The problem I see with this approach is that you might end up having to write a huge amount of these impossible instances. Maybe we can just do this on a by-need basis, where we only add such instances if many people are running into problems.

[goldfirere]

I'm also OK with making provably unlawful instances impossible. But I'd be quite surprised if my "one" + "two" == "three" instance cannot be made lawful. I'm just using an unusual representation for numbers.

And, yes, I agree that we need do this only for cases that actually arise.

But, most of all, I agree with @MorrowM's suggestion, above.

[MorrowM]

Just a motivating example of a lawful num instance, [()] is a way of doing Peano numbers that works surprisingly well. Its Ord instance is actually very nice for this, working lazily. + is ++, and * is liftA2 (\_ _ -> ()). Converting back to an Int is simply length. negate is an issue, but it's similar to Natural in that respect.

[tomjaguarpaw]

It's possible I wasn't clear enough originally. I don't doubt that there are useful ways that a type isomorphic to [a] can be given a Num instance. What I doubt is that it is sensible to allow Haskell users to give a Num instance to literally [a] (even for a concrete choice of a). Such an instance would necessarily be an orphan and it is likely to call all sorts of confusion, if not chaos. I'm very happy for users to newtype [a] and give instances to their hearts' content.

[gbaz]

I think that enumerating "bad" instances and adding impossible instances for them on a case-by-case basis is a losing game. There are too many possible bad instances (and clever arguments for each one about why maaaaybe someone might want them).

The overall approach should be driven by heuristics that improve error messages uniformly. (Or in special cases, perhaps, the compiler itself just being smart enough to write a very specific message tailored to a common bad error).

For example, it would improve a ton of error messages (not just Num/List ones) if MorrowM's suggestion is implemented for "making GHC complain about FlexibleContexts only when it can satisfy the constraint"

[MorrowM]

It's possible I wasn't clear enough originally. I don't doubt that there are useful ways that a type isomorphic to [a] can be given a Num instance. What I doubt is that it is sensible to allow Haskell users to give a Num instance to literally [a] (even for a concrete choice of a). Such an instance would necessarily be an orphan and it is likely to call all sorts of confusion, if not chaos. I'm very happy for users to newtype [a] and give instances to their hearts' content.

I still don't see the argument for making these instances forbidden as opposed to simply not providing them. What's the advantage to making them forbidden over improving the error message for not finding an instance?

[tomjaguarpaw]

I still don't see the argument for making these instances forbidden as opposed to simply not providing them. What's the advantage to making them forbidden over improving the error message for not finding an instance?

Well, I assumed that it would make the error messages better! But I haven't thought very hard about it so if people here are not saying "yes, you're obviously right" then I suspect I was mistaken. @gbaz's point as a good one too: enumerating every possible bad instance seems like more trouble than it's worth.

[Bodigrim]

FWIW there is a lawful instance (Eq a, Num a) => Num [a], implementing polynomial arithmetic.

[tomjaguarpaw]

Seems like this particular proposal is a dead end. I'm happy to close this issue but I will leave it up to the error-messages team to decide whether they close this issue or not. I'm not sure that the policy is.