Here's a thought: is there a way you can tell when you're in a bad case? There's surely one easy way: just count how many times your algorithm goes around. But perhaps you can do better, by looking for lots of guards, etc. My idea would be to enable guard checking by default, but to bail when the going gets tough. Bailing could issue a warning that such-and-such a function/case/multi-way-if is too ornate to be checked performantly. The user could then specify `-fno-warn-incomplete-pattern-guards` to turn off pattern-guard checking, `-fno-warn-ornate-guards` simply to disable the warning in the too-tough-to-handle case (but still check other guards in the module), or `-fwarn-incomplete-pattern-guards-at-any-cost` to instruct the check simply to work harder. Thus, pattern-guard checking would be enabled by default, but we would be protected from requiring 10GB of memory to compile a module.

I was inspired by the fact that I would be tempted to enable pattern-guard checking by default in my own code, even if the check is non-performant. Then, in years' time, I would have a module that inexplicably takes forever to compile and forget to look here. The design above lets me have my cake and eat it too -- that is, to have my code checked but not worry about surprising compilation times.

What do you think?

Richard

On Dec 12, 2015, at 1:05 PM, George Karachalias <george.karachalias@gmail.com> wrote:



On Sat, Dec 12, 2015 at 12:01 AM, Simon Peyton Jones <simonpj@microsoft.com> wrote:

`f` will generate an empty uncovered set while g will generate:

uncovered =

  { x |> { x ~ [], x ~ (_:_) }

  , x |> { x ~ (_:_), x ~ [] } }

 

which is also semantically empty but this cannot be detected until we call the

term oracle on it to see the inconsistency.

 

So, why not call the term oracle more aggressively (at every node of the tree), to prune empty sets?  It should not be hard to spot common cases; in what you show above it’s very easy.


Yes, we've been tempted to do this before but it didn't work. Since the sets can be really
big, we have relied on laziness a lot to save space and time. By calling the oracle more
often we will evaluate more eagerly parts of the sets which may lead to more space leaks.

Additionally, in my reply for #11195 (https://ghc.haskell.org/trac/ghc/ticket/11195#comment:4)
you can find another example for which solving the constraints eagerly does not necessarily
improve the situation. Sometimes the sets are big and consistent. So checking eagerly does
not actually prune anything. I can see now that my `f` and `g` above were bad examples for this.

Last but not least, the term oracle is not the most performant part of the checker. I would
certainly avoid calling it more often than we already do.

Nevertheless, I do not want to drop the work we have done on pattern guards either so I
think that the flag solution is a very good and realistic option for now. If we really manage to
find a nice way to do better we can always update the code which will not be removed from
GHC. I will certainly keep thinking about it :)

George

--
things you own end up owning you