Performance of pattern checker on OptCoercions

[Simon Peyton Jones]

`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.

Simon

From: George Karachalias [mailto:george.karachalias at gmail.com]
Sent: 11 December 2015 11:27
To: Ben Gamari <ben at well-typed.com>
Cc: Simon Peyton Jones <simonpj at microsoft.com>; Richard Eisenberg <eir at cis.upenn.edu>; GHC developers <ghc-devs at haskell.org>
Subject: Re: Performance of pattern checker on OptCoercions

Hello Ben,

On Fri, Dec 11, 2015 at 11:58 AM, Ben Gamari <ben at well-typed.com<mailto:ben at well-typed.com>> wrote:

Hi George,

Richard has encountered a bit of a performance cliff when merging his
no-kinds work. In particular OptCoercions now results in multiple
gigabytes of memory consumption during compilation due to the pattern
checker. The problem seems to be the opt_trans_rule binding, which has
numerous equations, each of which has patterns of various complexities
and guards. Might this be another case where disabling the pattern
checker is unavoidable?

I am afraid so. I have just responded to the ticket about it. The essence is the
difference between `f` and `g` below:
f x = case x of
  []      -> ...
  (_:_) -> ...

g y | []      <- y = ...
      | (_:_) <- y = ...

`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. Since pattern guards can pattern match
against any variable whilst case expressions match a single expression (`x` above)
I can not make the check treat them the same.
From what I see, until now the pattern guards in opt_trans_co involved mostly
pattern matching with Maybe which has only two constructors. I can easily assume
that this is the reason we did not have such a problem until now. So many guards
are already a challenge for the pattern match checker but maybe changing this (by
this I mean to not use pattern guards on types with many constructors because this
is the most expensive thing for the whole check) is enough to make GHC bootstrap.

I hope this helps, I am really confident that this is the cause of the problem.
Nevertheless, I will look into it more to see if I can find another source.

George
--
things you own end up owning you
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20151211/a49f24a4/attachment.html>