Generated Haskell code has redundant matches triggering GHC warnings

[andreasabel]

Generated Haskell code produces tons of overlapping-patterns warning because we have a catch-all in every alternative:

warning: [-Woverlapping-patterns]
    Pattern match is redundant
    In a case alternative: _ -> ...
      |
12242 |       _ -> MAlonzo.RTE.mazUnreachableError
      |       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Suggested fix: Put

{-# OPTIONS_GHC -Wno-overlapping-patterns -#}

into the generated Haskell files.

[andreasabel]

Currently, the no-overlapping-patterns option is passed in from inside Agda when calling GHC:

agda/src/full/Agda/Compiler/MAlonzo/Compiler.hs

Lines 1284 to 1292 in 798be60

	otherArgs =
	[ "-i" ++ mdir] ++
	(if isMain then ["-main-is", hsmod] else []) ++
	[ fp
	, "--make"
	, "-fwarn-incomplete-patterns"
	, "-fno-warn-overlapping-patterns"
	]
	args = overridableArgs ++ ghcopts ++ otherArgs

However, we might process the generated .hs files from outside after --dont-call-ghc, e.g. with cabal or stack. So I think it is better the option is written to each file (just like the LANGUAGE options are).

[nad]

If you include -Wno-warn-overlapping-patterns in the files, why not also -Wwarn-incomplete-patterns?

[andreasabel]

Good question. I want users to be able to switch on -Werror=overlapping-patterns without failing at the Agda-generated code which they cannot influence. We know that the overlaps introduced by Agda do not point to potential logical errors in the code and are all harmless.

What would be the motivation to force -Wincomplete-patterns in the Agda-generated files? Say Agda knows that a match is complete where GHC fails to see it (due to the loss of type information in the compilation). Why would we then force onto every user to see a pointless warning (and they cannot even switch it off from the outside)?

Of course, the current MAlonzo always puts out a catch-all (1), so it will never produce an incomplete match. So atm, we could add this warning without harm. Under the optimistic assumption of the truth of (1), there would also be no use of adding this warning.

So, to answer your question:

1. There is definitively use in inlining -Wno-overlapping-patterns.
2. Inlining -Wincomplete-patterns has only potential use of alerting the user of a bug in MAlonzo.

TL;DR I wanted to silence this pointless warning.

[UlfNorell]

Note that we do rely on the -Wincomplete-patterns for checking that Agda data types bound to Haskell types are not leaving out any constructors:

data Bool : Set where
  true : Bool

{-# COMPILE GHC Bool = data Bool (True) #-}

fails with

MAlonzo/Code/Foo.hs:21:5: error: [-Wincomplete-patterns, -Werror=incomplete-patterns]
    Pattern match(es) are non-exhaustive
    In a case alternative: Patterns of type ‘Bool’ not matched: False
   |
21 |   = case x of
   |     ^^^^^^^^^...

[andreasabel]

Note that we do rely on the -Wincomplete-patterns for checking that Agda data types bound to Haskell types are not leaving out any constructors:

Ok, this could be a reason to write it to the files as well. Do you suggest this?
I am still not sure this is good practice. Note that this cannot be overwritten from the outside then, can it?

[andreasabel]

I merged #5759 now, fixing the OP.
Welcome to do something about -Wincomplete-patterns if you will.