November 2017 - ghc-devs

GHC on Ubuntu
by Simon Peyton Jones 16 Nov '17

16 Nov '17

The GHC distribution for Ubuntu appears to be 7.10, very old. Do we (or they) bring on new versions? https://packages.ubuntu.com/search?keywords=ghc Here we use the LTS versions of Ubuntu, which seems stuck on 7.10. Simon

2 1

Reasoning backwards with type families
by David Feuer 16 Nov '17

16 Nov '17

Sometimes it woulld be useful to be able to reason backwards about type families. For example, we have type family a && b where 'False && b = 'False 'True && b = b a && 'False = 'False a && 'True = a a && a = a If we know something about either of the arguments, we can choose an equation and learn something about the result. But if we know something about the *result*, GHC doesn't give us any way to learn anything about the arguments. For (&&), the obvious things you'd want are prj1 :: (a && b) ~ 'True => a :~: 'True prj2 :: (a && b) ~ 'True => b :~: 'True flop :: (a && b) ~ 'False => (Not a || Not B) :~: 'True There's nothing inherently impossible about this sort of reasoning. In order for the constraint (a && b) ~ 'True to hold, the type family application *must have reduced* using one of its equations. The only possibilities are 'True && b = b a && 'True = a a && a = a Substituting 'True for each RHS gives 'True && 'True = 'True 'True && 'True = 'True 'True && 'True = 'True So in each case, the first argument is forced to 'True. Similarly, if (a && b) ~ 'False, we look at all the possibilities: 'False && a = 'False 'True && a = a a && 'False = 'False a && 'True = a a && a = a Substituting 'False for each RHS, 'False && a = 'False 'True && 'False = 'False a && 'False = 'False 'False && 'True = 'False 'False && 'False = 'False and we can calculate (Not a || Not b) as 'True for each of these LHSes. Now consider (==), which is recursive: type family (a :: k) == (b :: k) :: Bool where f a == g b = f == g && a == b a == a = 'True _ == _ = 'False We'd really like to know that eqEqual :: (a == b) ~ 'True => a :~: b :: For eqEqual, we can reason thus: if (a == b) ~ 'True, then we obtained that result from one of the equations f a == g b = f == g && a == b a == a = 'True In the base case, a ~ a on the LHS. In the recursive case, the RHS being 'True tells us (using the reasoning for (&&)) that (f == g) ~ True and that (a == b) ~ True. Inductively, we conclude that f :~: g and a :~: b. Shifting to the LHS, we conclude that f a ~ g b. I wouldn't necessarily expect GHC to be able to work something like this out on its own. But it seems like there should be some way to allow the user to guide it to a proof. A tantalizing feature is that we're essentially reasoning about execution traces, which are necessarily finite. It at least *seems* that this should mean that the induction is well-founded. Now why should anyone care about this sort of business? Because the runtime representation of, say, (a == b && c /= d) :~: 'True is smaller than the runtime representation of (a :~: b, c :~: d -> Void). So it would be nice to be able to recover the latter from the former. Can we do it? David

1 0

[ANNOUNCE] Hadrian update
by Andrey Mokhov 16 Nov '17

16 Nov '17

Dear GHC developers, As some of you might have already noticed, Hadrian has finally been merged into the GHC tree. However it's not yet time to celebrate - there are still many issues that need to be addressed before the Make-based build system may retire. Have a look at the README if you'd like a quick try: https://github.com/ghc/ghc/tree/master/hadrian. Here is a quick update on the on-going development: 1) Hadrian can build GHC and can already be used as part of the CI infrastructure. However, the resulting binary does not pass the validation. Zhen Zhang is looking into this, but more help is needed. See https://github.com/snowleopard/hadrian/issues/299. 2) A major refactoring by Moritz Angermann is on the way. Moritz is primarily interested in cross compilation, but to make it work he had to get rid of the ghc-cabal utility, reorganise the build tree, and make numerous other improvements to Hadrian. See https://github.com/snowleopard/hadrian/pull/445. 3) There is currently no support for binary distribution. Ben Gamari is looking into this issue: https://github.com/snowleopard/hadrian/issues/219. 4) Dynamic linking on Windows is not implemented. Tamar Christina has kindly offered help with this: https://github.com/snowleopard/hadrian/issues/343. 5) Hadrian source code is still not fully documented and tested, and generally requires some polishing. I am currently taking care of this when not distracted by urgent bug fixes and will appreciate your help in making Hadrian easier to understand and use. I can't believe that we seem to approach the finish line! It's been a long, tedious but also interesting project. Thank you all for helping us get this far, and I hope we'll celebrate the switch from Make to Hadrian soon. Cheers, Andrey

2 1

New core profiling mode
by Douglas Wilson 15 Nov '17

15 Nov '17

Hi ghc-devs, I've been working on a new mode of adding cost-centres to programs and I'd like to ask some questions and solicit some feedback. The code is here [fn:1], it works, provided one enables -fprof-core on all modules. I've recently been trying to pick some low hanging fruit from ghc compilation performance. A common frustration was in the difference between profiled and non-profiled builds. Often I thought had I found a problem in the profiled build, only to find it was optimized away in the non-profiled build. Several times an issue was tail-calls not happening in profiled builds. To solve this problem I've been working on a new way of inserting cost-centres: adding them to core after simplification (currently at the end of corePrepPgm) rather than adding them to HsSyn before simplification. This makes it harder to map cost-centres into source code (You have to -ddump-prep currently), but in exchange you are profiling the same core program as the non-profilied build. I intend to investigate whether I can use SourceNotes to create SrcSpans for the generated cost-centres to somewhat alleviate the need to inspect dumped core. There are several new flags: -fprof-core: Enables the aforementioned mode. This is mutually exclusive with -fprof-auto etc. -fprof-core-drop-ticks: Non-user ticks are dropped from unfoldings(though I don't know how to do this yet). -fprof-core-tick-binds: ticks are inserted around the RHS of bindings (except top-level unlifted bindings). -fprof-core-tick-cases: ticks are inserted around the scrutinees of cases. -fprof-core-tick-alts: ticks are inserted around Alt expressions (unless there is only one). Some questions: I need to strip (probably only non-user) ticks out of unfoldings before they are substituted into a module that uses -fprof-core. Where is the right place to do this? I need inlining to proceed exactly as if the ticks were not present, however I don't want to strip ticks when the unfoldings are created as other modules may still need them. Is the end of corePrepPgm the right place to insert the cost-centres? I chose it because it can't affect any core optimizations if it's last, but perhaps it could be earlier, or perhaps it needs to act on Stg? Do you have any examples of programs for which existing profiling tools are inadequate due to how cost-centres affect simplification? There is an example in #12893 but something self-contained would be great! Regards, Doug Wilson

3 2

RE: Trees that Grow and constraints
by Simon Peyton Jones 13 Nov '17

13 Nov '17

Alan (adding Shayan and ghc-devs) OK. It’s hard to keep this straight in email. Take a look at https://ghc.haskell.org/trac/ghc/wiki/ImplementingTreesThatGrow/Instances Please edit and improve it. Simon From: Alan & Kim Zimmerman [mailto:alan.zimm@gmail.com] Sent: 13 November 2017 13:30 To: Simon Peyton Jones <simonpj(a)microsoft.com> Subject: Re: Trees that Grow and constraints At the moment, in GHC master, we have data HsOverLit p = OverLit { ol_ext :: (XOverLit p), ol_val :: OverLitVal, ol_witness :: HsExpr p} -- Note [Overloaded literal witnesses] | XOverLit (XXOverLit p) deriving instance (DataIdLR p p) => Data (HsOverLit p) And in HsExtension.hs we have an ever-growing constraint type defining DataIdLR I am trying to remove the need for that. In the Experiment.hs file, I found that using data Experiment p = Experiment { e_ext :: (XEOverLit p), e_val :: Int } | XExperiment (XXOverLit p) deriving instance Data (GhcPass 'Parsed ) => Data (Experiment (GhcPass 'Parsed )) deriving instance Data (GhcPass 'Renamed ) => Data (Experiment (GhcPass 'Renamed )) deriving instance Data (GhcPass 'Typechecked) => Data (Experiment (GhcPass 'Typechecked)) will compile using GHC 8.2.1, but not with GHC 8.0.2 Alan On 13 November 2017 at 15:13, Simon Peyton Jones <simonpj(a)microsoft.com<mailto:simonpj@microsoft.com>> wrote: And it looks like it could work, when bootstrapping from GHC 8.2.1, but this is still a long time away. I’m sorry, I still don’t know what “it” is that “could work”. Can you be more precise. I think you must be suggesting some alternative to my code below? Simon From: Alan & Kim Zimmerman [mailto:alan.zimm@gmail.com<mailto:alan.zimm@gmail.com>] Sent: 13 November 2017 13:09 To: Simon Peyton Jones <simonpj(a)microsoft.com<mailto:simonpj@microsoft.com>> Subject: Re: Trees that Grow and constraints Yes. If we can solve this, it means we can get rid of the DataId and ForallXXX constraints defined in hsSyn/HsExtension.hs And also move the type family definitions to the files where they are used. I suspect that typechecking those constraint sets is adding to the GHC compilation time, significantly And it looks like it could work, when bootstrapping from GHC 8.2.1, but this is still a long time away. Alan On 13 November 2017 at 15:05, Simon Peyton Jones <simonpj(a)microsoft.com<mailto:simonpj@microsoft.com>> wrote: That’s not a problem you are trying to solve – it’s just some code 😊. Let me hazard a guess. You want a derived instance for Data (OverLit (GhcPass p)) But to do that of course we’ll need Data (XEOverLit (GhcPass p)). We can’t possibly have that at the time of writing the instance declaration, because p is universally quantified. So we are stuck with instance (Data (XEOverLit (GhcPass p))) => Data (OverLit (GhcPass p)) where… and the context gets a constraint for every extension field in OverLit, which is painful. So we have a solution bit contexts, but it’s painful. Is that the problem you are trying to solve? Simon From: Alan & Kim Zimmerman [mailto:alan.zimm@gmail.com<mailto:alan.zimm@gmail.com>] Sent: 13 November 2017 13:01 To: Simon Peyton Jones <simonpj(a)microsoft.com<mailto:simonpj@microsoft.com>> Subject: Re: Trees that Grow and constraints Sorry, I simplified the problem. The actual one I am trying to solve will be the general case, so e.g. type instance XEOverLit (GhcPass 'Parsed ) = RdrName type instance XEOverLit (GhcPass 'Renamed ) = Name type instance XEOverLit (GhcPass 'Typechecked) = Id or more likely, modelling the existing PostTc and PostRn usages. And I suppose looking into using them in a single definition might work Alan On 13 November 2017 at 14:55, Simon Peyton Jones <simonpj(a)microsoft.com<mailto:simonpj@microsoft.com>> wrote: Or do I misunderstand your advice? Well, you said Where specifying the type instance with a wild card keeps GHC happy (the XXOverLit case), but specifying for each of the three constructors for pass does not (the XEOverLit case) My question is: why not just use the wildcard, in that case? Do you want to re-state the problem you are trying to solve? Simon From: Alan & Kim Zimmerman [mailto:alan.zimm@gmail.com<mailto:alan.zimm@gmail.com>] Sent: 13 November 2017 12:49 To: Simon Peyton Jones <simonpj(a)microsoft.com<mailto:simonpj@microsoft.com>> Cc: ghc-devs(a)haskell.org<mailto:ghc-devs@haskell.org> Subject: Re: Trees that Grow and constraints So why not use one? Simon If I do instance (Data p) => Data (Experiment p) then GHC does not know that the type instances for type instance XEOverLit (GhcPass 'Parsed ) = PlaceHolder type instance XEOverLit (GhcPass 'Renamed ) = PlaceHolder type instance XEOverLit (GhcPass 'Typechecked) = PlaceHolder apply. Or do I misunderstand your advice? Alan

2 2

Trees that Grow and constraints
by Alan & Kim Zimmerman 13 Nov '17

13 Nov '17

At the moment the Trees that Grow implementation in GHC master makes use of massive constraint types to provide Data instances for the hsSyn AST. I am trying to remove the need for this, and have hit a problem. The example I have reduced it to is here [1] The essence of the problem is ------------------- data Experiment p = Experiment { e_ext :: (XEOverLit p), e_val :: Int } | XExperiment (XXOverLit p) deriving instance (Data (GhcPass p)) => Data (Experiment (GhcPass p)) type family XEOverLit x type family XXOverLit x -- The following line works -- type instance XEOverLit (GhcPass _) = PlaceHolder -- The following 3 lines do noe type instance XEOverLit (GhcPass 'Parsed ) = PlaceHolder type instance XEOverLit (GhcPass 'Renamed ) = PlaceHolder type instance XEOverLit (GhcPass 'Typechecked) = PlaceHolder type instance XXOverLit (GhcPass _) = PlaceHolder ------------------- Where specifying the type instance with a wild card keeps GHC happy (the XXOverLit case), but specifying for each of the three constructors for pass does not (the XEOverLit case) The exact error message is ------------------------------ Experiment.hs:34:1: error: • Could not deduce (Data (XEOverLit (GhcPass p))) arising from a use of ‘k’ from the context: Data (GhcPass p) bound by the instance declaration at Experiment.hs:34:1-69 • In the first argument of ‘k’, namely ‘(z Experiment `k` a1)’ In the expression: ((z Experiment `k` a1) `k` a2) In an equation for ‘gfoldl’: gfoldl k z Experiment a1 a2 = ((z Experiment `k` a1) `k` a2) When typechecking the code for ‘gfoldl’ in a derived instance for ‘Data (Experiment (GhcPass p))’: To see the code I am typechecking, use -ddump-deriv | 34 | deriving instance (Data (GhcPass p)) => Data (Experiment (GhcPass p)) | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ ------------------------------ Alan [1] http://lpaste.net/360017

3 5

Dynamically choosing the main function
by Harendra Kumar 13 Nov '17

13 Nov '17

Hi, GHC allows choosing a main function at link time using the "-main-is" option. I was wondering if there is a possibility to choose the main function at runtime. Or even better, if something equivalent to "ghc -e" is somehow possible in a linked binary executable. If not, are there any plans to achieve something like that in future? Are there any theoretical, practical obstacles to that? Thanks, Harendra

5 10

Re: [commit: ghc] master: WIP on combined Step 1 and 3 for Trees That Grow, HsExpr (e3ec2e7)
by Joachim Breitner 13 Nov '17

13 Nov '17

Hi Alan, the combined effect of commit e3ec2e7ae94524ebd111963faf34b84d942265b4 WIP on combined Step 1 and 3 for Trees That Grow, HsExpr and commit 438dd1cbba13d35f3452b4dcef3f94ce9a216905 WIP on Doing a combined Step 1 and 3 for Trees That Grow causes a 15% regression in the time it takes to build GHC, according to https://perf.haskell.org/ghc/#compare/fe6848f544c2a14086bcef388c46f4070c22d… Is that a known, expected and accepted regression? Joachim -- Joachim Breitner mail(a)joachim-breitner.de http://www.joachim-breitner.de/

3 4

Asserting vars with different Uniques represent the same Object
by Andreas Klebinger 11 Nov '17

11 Nov '17

My core questions are: * Should variables representing the same thing always have the same unique? * If not how can one assert they actually represent the same thing? Working on the pattern matching code I came across this assertion: > ASSERT(tvs1 `equalLength` ex_tvs ) http://git.haskell.org/ghc.git/blob/HEAD:/compiler/deSugar/MatchCon.hs#l125 tvs1 and ex_tvs are both the existentially quantified type variables of a pattern. One gained by taking apart the pattern itself and one by taking apart the ConLike in the pattern. While as far as I can tell they always represent the same Types they don't always compare as equal. Is there any other stable way to compare them? (By name? Something else?). Or is them not being equal a bug to begin with. Follow up question: The whole assert is essentially a unit test as ex_tvs isn't used outside of the assert. Is there a solution to check these invariants in tests instead of the source code?

2 1

merge issues with new field for FamEqn
by John Leo 11 Nov '17

11 Nov '17

Hi everyone, Today I'm trying to merge the latest HEAD into my work on the explicit forall proposal, and I'm running into a problem I'd like help with. The changes that are affecting me seem to come from the latest Trees that Grow checkins. I had added a field to FamEqn, namely feqn_bndrs: data FamEqn pass pats rhs = FamEqn { feqn_tycon :: Located (IdP pass) , feqn_bndrs :: Maybe [LHsTyVarBndr pass] -- ^ Explicit user-provided binders , feqn_pats :: pats , feqn_fixity :: LexicalFixity -- ^ Fixity used in the declaration , feqn_rhs :: rhs } -- ^ -- - 'ApiAnnotation.AnnKeywordId' : 'ApiAnnotation.AnnEqual', -- 'ApiAnnotation.AnnForall','ApiAnnotation.AnnDot' -- For details on above see note [Api annotations] in ApiAnnotation deriving instance (DataId pass, Data pats, Data rhs) => Data (FamEqn pass pats rhs) When I try to compile now, I get the following errors that I cannot understand. I assume I need to do something else, but I'm not sure what it is, so I'd appreciate any guidance. compiler/hsSyn/HsDecls.hs:1441:1: error: • Could not deduce (Data (XValBinds pass pass), Data (XXValBindsLR pass pass)) arising from a use of ‘k’ from the context: (DataId pass, Data pats, Data rhs) bound by the instance declaration at compiler/hsSyn/HsDecls.hs:(1441,1)-(1442,46) • In the first argument of ‘k’, namely ‘((z FamEqn `k` a1) `k` a2)’ In the first argument of ‘k’, namely ‘(((z FamEqn `k` a1) `k` a2) `k` a3)’ In the first argument of ‘k’, namely ‘((((z FamEqn `k` a1) `k` a2) `k` a3) `k` a4)’ When typechecking the code for ‘gfoldl’ in a derived instance for ‘Data (FamEqn pass pats rhs)’: To see the code I am typechecking, use -ddump-deriv | 1441 | deriving instance (DataId pass, Data pats, Data rhs) | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^... compiler/hsSyn/HsDecls.hs:1441:1: error: • Could not deduce (Data (XValBinds pass pass), Data (XXValBindsLR pass pass)) arising from a use of ‘k’ from the context: (DataId pass, Data pats, Data rhs) bound by the instance declaration at compiler/hsSyn/HsDecls.hs:(1441,1)-(1442,46) • In the first argument of ‘k’, namely ‘(k (k (z FamEqn)))’ In the first argument of ‘k’, namely ‘(k (k (k (z FamEqn))))’ In the first argument of ‘k’, namely ‘(k (k (k (k (z FamEqn)))))’ When typechecking the code for ‘gunfold’ in a derived instance for ‘Data (FamEqn pass pats rhs)’: To see the code I am typechecking, use -ddump-deriv | 1441 | deriving instance (DataId pass, Data pats, Data rhs) | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ John

2 1