Performance of pattern checker on OptCoercions

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

Re: -XStrict: Why some binders are not made strict?

I believe Scala has optional lazy values, but you could also consider in strict languages if you do manual thunking. If we force strictness all the way down it's not really call-by-value either, because the caller doesn't know what to evaluate (I think). In addition, making pattern matching

Re: -XStrict: Why some binders are not made strict?

On 12/11/2015 02:21 PM, Johan Tibell wrote: > If we force strictness all the way down it's not really call-by-value > either, because the caller doesn't know what to evaluate (I think). Not sure what you mean here. > In addition, making pattern matching strict in this way makes it hard to > mix

Re: Performance of pattern checker on OptCoercions

If I understand correctly, you're saying that the problem is due to my use of guards, not anything with fancy types. If that's correct, then this sort of thing might be a trap anyone could stumble into. (The code in OptCoercion is fairly routine for Haskell.) It seems like disabling checking

Re: type operators and colon in GHC

This behavior changed in 7.6 I believe. It used to be that type operators needed to start with a colon, but that restriction was dropped. The documentation is out of date. Ticket #11046 is about updating Template Haskell to match the new behavior, but it doesn't affect the core story of type

Re: Unused type variables with non-linear patterns

I agree with Michael. This should not emit a warning. While you're in this area, make sure that > type instance F _ _ = Int indeed matches `F Char Bool`. It's easy to imagine both underscores being treated as the same variable, which is not what the user intends. Thanks, Richard On Dec 10,

kind inference (#11203)

Hi Simon and other devs, I struggled a bit today with some issues around kind inference that I wanted to write down. Here are some illuminating test cases, explained below: -- useful definition: data SameKind :: k -> k -> * 1. data T (a :: k1) x = MkT (S a ()) data S (b :: k2) y = MkS (T b

RE: Performance of pattern checker on OptCoercions

Yes; but we should jolly well figure out a way to do better for guards. These guards are no more than patterns really! Simon From: Richard Eisenberg [mailto:e...@cis.upenn.edu] Sent: 11 December 2015 15:59 To: George Karachalias Cc: Ben Gamari

Re: A comment on Introspective-Haskell

Spot on.. I really want "Template Core," independent of TH. To be honest, "GHC Plugins" already provides "Template Core" in this sense; but would be nicer if one can get his hands on the Core in the regular Haskell context, not just in a plugin context. So, perhaps "Template Core" is not the

RE: Performance of pattern checker on OptCoercions

`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

Re: A comment on Introspective-Haskell

My "hidden agenda" is to liberate the SBV library to work on Haskell programs directly. (http://hackage.haskell.org/package/sbv) SBV allows programming with symbolic values, allowing a certain class of "proofs" to be done. It uses SMT solvers to do the actual "solving." It's limited in what it

Re: -XStrict: Why some binders are not made strict?

Thanks Simon, this is an interesting and compelling interpretation. But I'm wondering whether it is enough to specify the dynamic semantics unambiguously. Two examples: 1. let _ = undefined in () Intuitively, since we are talking about /strictness/, this should evaluate to bottom. However,

Re: A comment on Introspective-Haskell

I'm seeing several different directions here, and it may be helpful to clarify what's going on: * My original proposal was about changing the implementation of Template Haskell in a way that casual TH users wouldn't notice (by going through the compatibility shim). Once this is done, it may be

RE: -XStrict: Why some binders are not made strict?

| As I said, I prefer this semantics mainly because it's easier to | explain: all variables (and underscores) bound in a strict module refer | to WHNF values. Do you have a similarly simple explanation for the | semantics you're suggesting? Here's one, which is roughly what the current

Re: -XStrict: Why some binders are not made strict?

I agree with Roman here. Probably another reason for making every binding strict is this: (sorry if this is mentioned) Suppose I imported `data D = D ...` from another library and I'm in -XStrict. In this code: case ... of D b1 b2 ... -> I should be able to assume that b1, b2 ...

RE: -XStrict: Why some binders are not made strict?

In addition, making pattern matching strict in this way makes it hard to mix and match strict and lazy data types (e.g. Maybe), because using a lazy data type from another module will make it appear strict in your code (hurting modularity). I didn’t understand that. Simon From: ghc-devs

Re: A comment on Introspective-Haskell

On Fri, Dec 11, 2015, at 14:54, Levent Erkok wrote: > Spot on.. I really want "Template Core," independent of TH. > > To be honest, "GHC Plugins" already provides "Template Core" in this > sense; > but would be nicer if one can get his hands on the Core in the regular > Haskell context, not just

Re: A comment on Introspective-Haskell

On Fri, Dec 11, 2015, at 15:28, Levent Erkok wrote: > My "hidden agenda" is to liberate the SBV library to work on Haskell > programs directly. (http://hackage.haskell.org/package/sbv) > So the idea is to translate a Haskell expression to an SBV symbolic expression, which you can then ship off

Re: A comment on Introspective-Haskell

Precisely.. If all goes well, one will be able to say: import Data.SBV.Plugin {-# ANN f theorem #-}f :: Double -> Double -> Double -> Boolf x y z = x + (y + z) == (x + y) + z And have that theorem proven at "compile" time. (Of course, the above is actually not true, so the user will get a

Re: kind inference (#11203)

Actually, I think I know how to fix the problem with (3) and (4), by unifying the kinds in any KindedTyVars in the tycon's LHsQTyVars with the tyvar kinds in the tycon's kind. I have some preliminary code toward this, and should return to the problem early next week. (2), on the other hand, is

Re: [ANNOUNCE] Glasgow Haskell Compiler version 7.10.3

Tuncer Ayaz writes: > On 9 December 2015 at 13:17, Ben Gamari wrote: > >> Unfortunately, due to some oversights in the release process there are >> two source tarballs for this release. The first, >> ghc-7.10.3-src.tar.{bz2,xz}, does not include the