Exhaustiveness checking for non-arithmetic patterns

[LeitMoth]

Implements the Lower Your Guards algorithm for coverage checking.
Makes significant progress on #32 (but does not complete it, as we don't handle arithmetic patterns).
To avoid false positives, we simply treat every arithmetic pattern as if it has the same coverage as a wildcard. I do not believe we can achieve a better result until a rework of arithmetic patterns is merged.

While I have not encountered a problem, I am marking this as a draft, as there are a few things that I would like to have reviewed:

These TODOs have to do with resolveAlias and should be read as a group. It seems to work with recursive type aliases, but I would like to be absolutely sure before merging:

src/Disco/Exhaustiveness/Constraint.hs:66:17:      -- 10c -- TODO(colin): Still need to add type constraints!
src/Disco/Exhaustiveness/Constraint.hs:132:6:--   TODO(colin): we may eventually have type constraints
src/Disco/Exhaustiveness/TypeInfo.hs:112:4:-- TODO(colin): ask yorgey, make sure I've done this correctly

These TODOs have to do with tyDataConsHelper and should be read as a group. This function assumes that aliases have been resolved, and converts Disco types to lists of my custom data constructor type, which I needed to make for the LYG algorithm. I would like to be sure that I am not losing any important information in this conversion:

src/Disco/Exhaustiveness/TypeInfo.hs:128:4:-- TODO(colin): ask yorgey to see if I've handled all the thing
src/Disco/Exhaustiveness/TypeInfo.hs:143:4:-- TODO(colin): We could do all valid ASCII, but this is most likely good enough
src/Disco/Exhaustiveness/TypeInfo.hs:153:4:-- TODO(colin): confim below:

These two are about comments / comment style:

src/Disco/Exhaustiveness.hs:42:4:-- TODO(colin): should I explain that this comes from the LYG paper
src/Disco/Exhaustiveness/TypeInfo.hs:72:4:-- TODO(colin): should I quote 'Infinite' with single quotes in the above doc comment?

And the surrounding comment around this one has details about the unhanded arithmetic stuff and asks if it is okay to leave it at what I have:

src/Disco/Exhaustiveness.hs:126:6:--   TODO(colin):

Of course, if I need to change/add any comments or code outside of these TODOs, let me know about that too.

Once all these and possibly a few new TODOs have been handled, I am excited to finally merge this.

[LeitMoth]

Also, when running the tests, this is printed out (from when example/lists.disco is checked):

Warning: You haven't covered these cases:
indexP 1 [] = ...
indexP 2 [] = ...
indexP 3 [] = ...

The coverage checker is working correctly here, but I'm not sure if having a warning like this is the test output is an okay thing.

All the tests still succeed, but it looks like the output from the disco-examples and the disco-test test suites overlap, like both are being run at the same time. This is not really a problem, but is worth noting. I am running cabal test if that matters.

(Also, when checking the log files for both test suites after this happens, the above coverage warning isn't in either of those. Maybe this is because the warning is printed on standard error? Also probably fine, but worth noting)

[byorgey]

Also, when running the tests, this is printed out (from when example/lists.disco is checked):

Ah, indeed, the coverage checker is working correctly there, and it uncovered another problem: we should actually delete example/lists.disco, because it doesn't work any more! A long time ago it used to generate an infinite (lazy) list of Fibonacci pairs with iterateP, and then index into it, but Disco is strict now, so in fact it just hangs in an infinite loop.

(Also, when checking the log files for both test suites after this happens, the above coverage warning isn't in either of those. Maybe this is because the warning is printed on standard error? Also probably fine, but worth noting)

Hmm, not sure, I'll look into this.

[LeitMoth]

Also, when running the tests, this is printed out (from when example/lists.disco is checked):

Ah, indeed, the coverage checker is working correctly there, and it uncovered another problem: we should actually delete example/lists.disco, because it doesn't work any more! A long time ago it used to generate an infinite (lazy) list of Fibonacci pairs with iterateP, and then index into it, but Disco is strict now, so in fact it just hangs in an infinite loop.

(Also, when checking the log files for both test suites after this happens, the above coverage warning isn't in either of those. Maybe this is because the warning is printed on standard error? Also probably fine, but worth noting)

Hmm, not sure, I'll look into this.

Then I will delete example/lists.disco as part of this PR.

[LeitMoth]

Another thought: the way you have written this, it applies to functions defined by clauses, but not to case expressions. For example,

f : N -> N
f(2) = 7   -- this generates a warning

g : N -> N
g(n) = {? 7 if n is 2 ?}  -- this does not

It's not a huge deal right now since students will mostly be using the first form. But I'm curious what would be needed to get it to analyze case expressions as well. If it's easy, we could do it right now, or we can just file an issue for later.

I originally did not consider case expressions, as I imagined students would only reach for case expressions when they had to check some boolean condition, which is not something the coverage checker can help with.

Also I think that having the coverage checker work for some case expressions, but drop out the moment a boolean condition is introduced, might give students the wrong idea that adding the boolean condition covered all the cases (When in fact we just can't check it so we can't report any warnings).

If we did add this, I am not sure the effort it would take, but it is definitely more work than I can do before the semester starts. I think we should just file an issue and come back to it later.

[byorgey]

Also I think that having the coverage checker work for some case expressions, but drop out the moment a boolean condition is introduced, might give students the wrong idea that adding the boolean condition covered all the cases (When in fact we just can't check it so we can't report any warnings).

Right, the way GHC handles this is to yield a warning every time there are Boolean guards with no catch-all case. So as long as you have a series of guards with an otherwise at the end it will not yield any warnings; but with no otherwise it will give a warning. We could do something similar. However, I 100% agree that we should just file an issue and leave it for later.

[LeitMoth]

I am am now converting to disco patterns and using the pretty printer.
I think everything is in order, and all tests pass. I believe everything is now formatting correctly, but I haven't done extensive testing.

There are two small things of note:

1. I am re-sugaring lists of chars to string patterns. (Let me know if this is a misstep.) However, an empty list pattern does not have the necessary type information for me to be able to report it. So I cannot resugar an empty list of chars as "". I see no way around this without significant changes to how I store dataconstructors.
   For example:

Disco> f : List(Char) -> Unit
Disco> f "hello" = unit
Warning: the function f is undefined for some inputs. For example:
f([]) = ...
f("a") = ...
f("aa") = ...

2. I have the full list of unicode working, but the prettyprinter doesn't seem to want to print any of it.
   For example, code 161 is the upside-down exclamation mark:

ghci> putChar (toEnum 161) >> putChar '\n'
¡

asdf.disco is a file where ever ascii char except ~ is matched on. And for it, the prettyprinter says \161

$ cabal run disco -- --check /tmp/asdf.disco
Loading asdf.disco...
Warning: the function f is undefined for some inputs. For example:
f('~') = ...
f('\161') = ...
f('\162') = ...
Loaded.

Both of these are technically correct behavior, so I am not too worried, and I think I am finally ready to merge.

[byorgey]

1. I cannot resugar an empty list of chars as ""

That's fine, that would make a nice improvement but not critical. Let's just make it into an issue for now.

the prettyprinter says \161

Yeah, I think the default is to use escape sequences for any non-ASCII characters, since it's hard to know what kind of guarantees there are in terms of what font is being used, which characters it has glyphs for, etc. so it's safest to just use escape sequences for everything. This is perfectly fine and expected. Writing f('\161') is in fact legal Disco code.

[byorgey]

This looks great! We don't need to worry about the failing doc build, since it looks like it is failing just because of missing configuration on this branch. As for the Restyled issue, I went ahead and merged the style fixes. Once the CI finishes running again I think this should be good to go.

[byorgey]

@LeitMoth go ahead and apply the merge me label to this PR whenever you're ready!

[byorgey]

🎉