Consistent handling of dead code / absurd premises
Background
See https://gitlab.haskell.org/ghc/ghc/-/wikis/Dead-Code
Motivation
GHC does not currently have a very consistent policy.
-
As pointed out in the first part of !2080 (comment 235964), GHC sometimes makes code requiring absurd constraints an error, but this only is at the top level, and only happens if the absurd constraint involves an ambiguous type variable. Absurd constraints with ambiguous variables should not be treated differently than absurd constraints without them. This is because currently the ambiguity checker reports (as errors) conditions that are specifically suppressed during actual typechecking. If anything it should be the other way around!
-
As argued in #11066 (closed), and the second part of !2080 (comment 235964), dead code is better as a warning. Otherwise-valid substitutions (whether performed by the computer or humans) shouldn't cause errors one nothing would go wrong if those errors didn't exist. Also, metaprograms may have a harder time avoiding the absurd cases that humans can avoid by special-case. See 0e4e03a2 for the precedent of these being warnings not errors.
Proposal
-
Do not report dead code during ambiguity checking (formerly implemented in !2080 (closed)). Dead code should be reported elsewhere, if it is to be reported at all.
-
Top-level dead code should produce the same warning as inaccessible case branches (formerly explored in !3331 (closed)). This fixes the lack of warnings from examples 1 and 2, makes up for the removal of the error in example 3, and makes GHC treat all 3 the same as example 4.
-
Be sure dead code in derived instances is still not reported, preserving the behavior described in
Note [Avoid -Winaccessible-code when deriving]
inGHC.Tc.TyCl.Instance
.
Because the motivation of those is interrelated, we opted to make one combined PR instead for the entire issue: !3868.
Examples
-
This is accepted without warnings:
foo :: Int ~ Bool => () foo = ()
We think it ought to have a dead code warning, but agree it should not be an error.
-
This is accepted without warnings:
bar :: A a ~ B a => Proxy a -> () bar Proxy = ()
We think it ought to have a dead code warning, but agree it should not be an error.
-
This is an error, with or without
-XAllowAmbiguousTypes
:baz :: A a ~ B a => () baz = ()
We think 3 should be treated just as we want 1 and 2 to be treated: with dead code warnings, without errors. We think dead code errors/warnings should have nothing to do with the ambiguity check.
-
Meanwhile, this is accepted with dead code warnings:
data Bar a where MkBar :: Bar Int quop :: Bar Bool -> () quop MkBar = ()
We like this behavior, and want GHC to treat the other examples closer to how it treats this.
Analysis
In this 3rd case we end up with
[G] A a0 ~ B a0
[W] A a1 ~ B a1
Because the variables (skolems) are ambiguous, we did not get the substitutions that would allow the wanted constraint to be satisfied. Whereas in example 2, the variables weren't ambiguous so we did get the substitution, and in example 1 there were to variables we needed to substitute.
But why is this error emitted in the third case even with -XAllowAmbiguousTypes
? This is because the analysis is always run, and the errors are emitted unless allow_ambiguous && not (insolubleWC final_wc)
.
We think the && not (insolubleWC final_wc)
is bad idea:
-
As the first 2 examples show, this is clearly not sufficient for catching all top-level inaccessible code, so it only makes sense as part of a larger policy. But the current larger policy is that top-level inaccessible code is not an error.
-
With
-XAllowAmbiguousTypes
,baz
can unify with itself in real code: e.g.[baz @a @b, baz @a @b] :: forall a b. [A a ~ B a => ()]
. So even ignoring the question of whether to raise an error, @Ericson2314 thinks thetypeOfBaz <= typeOfBaz
subsumption check is a dubious thing to consult for any purpose with-XAllowAmbiguousTypes
.Put more simply, even if we were making dead code and error as before, under
-XAllowAmbiguousTypes
I think we should not distinguish 1, 2, and 3. While they would all have a dead code error, that error should be emitted for the same reasons and that reason should have nothing to do with the ambiguity check.
How we got here
The design history of this behavior is complicated and hard to follow. Nevertheless, it is instructive to go over it because it shows the multiple intents behind the current design, so we can be sure those needs are still met.
#8044 (closed)
This issue was fixed unintentionally/incidentally (see #8044 (comment 91823)), so I am not sure whether anything happened due to it that is relevant.
#12466 (closed)
This issue was fixed in 0e4e03a2. See that commit for details on the resolution.
Back then, dead code was never a warning, and always an error, if it was reported at all.
This led to issues where dead code was unavoidable, so the conditions under which the error was reported were made more complex and restrictive, as documented in the origin Note [Given errors]
.
#11066 (closed)
This issue was fixed in 08073e16. See that commit for details on the resolution.
This issue is about dead code making dead code a warning, which was done.
Crucially, while the issue is older than #12466 (closed), the resolution is newer. By making the error into a warning, the extra complexity from #12466 (closed)'s fix became obsolete: there is no presing need to "artificially" limit the situations the warning is emitted, since a warning, unlike an error, doesn't have prevent code from being written.
This issue
In both cases, it is our view that we are continuing the design agreed upon in #11066 (closed), which in our view was not fully implemented in 08073e16 when that issue was closed.
Proposal part 1
We continue in the spirit of #11066 (closed), removing the remaining dead code warning that happens to be emitted during the ambiguity check. That it is from the ambiguity check in particular we consider completely incidental: we don't see any sign that this was an intended part of ambiguity checking in particular. Rather, we think this was just a continue of a general preexisting policy towards inaccessible code up until #11066 (closed).
We consider our changes to the ambiguity checker just removing a relic that ought to have been changed when #11066 (closed) was fixed, and not novel design work.
Additionally, if the argument @Ericson2314 raises in part 2 of the "analysis of examples section" is accepted, the change to the ambiguity checker is good whether or not #11066 (closed) had been accepted/rejected (i.e. regardless of whether we want dead code to be an error or warning), because the ambiguity checker is never the right place to care about code that is dead due to impossible premises rather than ambiguity.
Proposal part 2
We now remove that complexity described in Note [Given errors]
from #12466 (closed), which is no longer needed after #11066m, but was never removed. The extra warnings this creates just so happen to compensate for the errors, removed with part 1's change, but we basically consider this a happy coincidence.
Open questions to follow up on later
TH
Should dead code warnings also be suppressed in TH splices, for much the same reason they are in derived instances? Is there already a way in TH to do this manually?
Positive vs negative position
It's possible that with !3868 we would over-report some Given constraints. Is that OK?
For example, consider the following two functions:
f :: (Int ~ Bool) => Int -> Int
g :: ((Int ~ Bool) => a -> a) -> Int
While f
cannot be called, and essentially must be dead code, the function g
could be used, as it only requires a function which demands an absurd premise. That is, f
requires something that is impossible, while g
merely requires something that is unnecessary. In fact, f
is just such a valid argument: g f :: Int
has no funny constraints and is perfectly fine.
However, according to other issues it's tricky to distinguish these two cases due to the way that the constraint solver is written. The circuitous discussion over the years is:
-
#12466 (closed), and #12466 (comment 123761) in particular, says we should silence errors because in part we cannot distinguish
f
andg
. - #11066 (closed) lowers the stakes making it a warning
- #17543 say we want some of those warnings back, but it is also saying that #12466 (closed) no longer applies since warnings to prevent writing programs. Implicit in that second part is it's not so bad to have false positive warnings, because we if found a way to make the errors exactly what we want, we might not even need to appear to #11066 (closed) making them warnings to justify our new approach.
But let's come to a final decision on this sort of thing explicitly.
Ideally, unusable arguments should not be reported as dead code -- it's a confusing message, the more so for being inaccurate, and there's no good way to fix the warning other than shutting it off for the whole module. However, currently nobody has a plan for how to distinguish these cases, and it has been indicated as being hard. @Ericson2314 and @cgibbard propose we indeed make them both warnings for now, and only later try to make just f
a warning.
In addition, @Ericson2314 hopes that there can be something like \case {}
bot for absurd constraints rather than absurd regular arguments. This would not have a a dead code warning, because the intent to be uncallable is explicit in the code. @Ericson2314 likes this example because he thinks it teases apart the guiding principle: it's not the definition or lambda abstract that gets the dead code warning dead code, but just the body of the abstraction that does. An explicit uncallable lambda like \case {}
or the proposed new syntax has no body, and that's precisely why it gets no warning. See https://gitlab.haskell.org/ghc/ghc/-/wikis/Dead-Code for more discussion of this.
Possible longer term resolution: With #19428 the pattern match checker would take over the job of the current inaccessible code linter. Because it works on Core, it can see dictionary passing and use that to distinguish between positive and negative position constraints. (See the conversation between @simonpj and @sgraf812 starting !3868 (comment 334206)). This is a great long-term plan that matches the principles outlined in ttps://gitlab.haskell.org/ghc/ghc/-/wikis/Dead-Code of always looking at terms not types.