Hello Ben,

On Fri, Dec 11, 2015 at 11:58 AM, Ben Gamari <ben@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