- ghc-devs - Haskell.org

Impredicative types in 8.0, again
by Kosyrev Serge 04 Mar '16

04 Mar '16

Good day! I realise that ImpredicativeTypes is a problematic extension, but I have found something that looks like an outright bug -- no polymorphism involved: ,---- | {-# LANGUAGE ImpredicativeTypes #-} | | module Foo where | | foo :: IO (Maybe Int) | foo = do | pure $ case undefined :: Maybe String of | Nothing | -> Nothing | Just _ | -> (undefined :: Maybe Int) `---- produces the following errors: ,---- | foo.hs:7:3: error: | • Couldn't match type ‘forall a. Maybe a’ with ‘Maybe Int’ | Expected type: IO (Maybe Int) | Actual type: IO (forall a. Maybe a) | • In a stmt of a 'do' block: | pure | $ case undefined :: Maybe String of { | Nothing -> Nothing | Just _ -> (undefined :: Maybe Int) } | In the expression: | do { pure | $ case undefined :: Maybe String of { | Nothing -> Nothing | Just _ -> (undefined :: Maybe Int) } } | In an equation for ‘foo’: | foo | = do { pure | $ case undefined :: Maybe String of { | Nothing -> Nothing | Just _ -> (undefined :: Maybe Int) } } | | foo.hs:11:19: error: | • Couldn't match type ‘a’ with ‘Int’ | ‘a’ is a rigid type variable bound by | a type expected by the context: | forall a. Maybe a | at foo.hs:11:19 | Expected type: forall a. Maybe a | Actual type: Maybe Int | • In the expression: (undefined :: Maybe Int) | In a case alternative: Just _ -> (undefined :: Maybe Int) | In the second argument of ‘($)’, namely | ‘case undefined :: Maybe String of { | Nothing -> Nothing | Just _ -> (undefined :: Maybe Int) }’ `---- -- с уважениeм / respectfully, Косырев Сергей

3 2

isRecursiveTyCon
by José Manuel Calderón Trilla 04 Mar '16

04 Mar '16

Hello, I'm extending GHC's demand analysis to sum types, but _not_ recursive types. I was searching for a function that would tell me if a TyCon is recursive, so that I could analyse Maybes but avoid Lists. I found isRecursiveTyCon, but it's not actually for this purpose, there's actually a long note in typecheck/TcTyDecls.hs that explains why it's not fit for determining which type constructors are recursive in general. The key point from the note is "The "recursive" flag for algebraic data types is irrelevant (never consulted) for types with more than one constructor." It seems that because the strictness analyser never worked over sum types it never had to worry about recursive sum types and at some point the flag that says a data type is recursive broke for sum types without anyone knowing. For example the following mutually recursive data types have different return values from isRecursiveTyCon data OddNat = One | SuccO EvenNat data EvenNat = Zero | SuccE OddNat Does anyone know of the simplest way to test for this? Thanks for your time, Jose

2 1

Re: Questions concerning the LLVM backend - i.e. 'proc point splitting'
by David Spitzenberg 04 Mar '16

04 Mar '16

Simon > | Could you explain the need of further info-tables for 'inner' > | proc-points (those, which are not the entry-block of a function) to > | me, please? > > The main purpose of inner info tables is this. Given (case e of blah) we push a return address (for 'blah') on the stack and evaluate 'e'. During evaluation of 'e', garbage collection may take place. So the garbage collector needs to walk the stack to follow live pointers. Who knows what pointers are live? Answer: the code for 'blah' clearly knows what pointers are alive in the current stack frame, because it is going to access them. So the return address gets an info table that makes that implicit knowledge explicit, as a bitmap describing the liveness/pointer-hood of the stack frame. > > Addresses that are only jumped to don’t need info tables. > > It would be great if, as you learn about this stuff, you could add to the Commentary > https://ghc.haskell.org/trac/ghc/wiki/Commentary > to capture what you have learned. Thank you very much! In cases I find the current description imprecise or incomplete I can add what I've learned to the Commentary of course. > | The documentation states, that proc-point splitting is only required > | by the LLVM backend (see [2]). Does the cmm-pipeline perform proc- > | point splitting even when using the native code generator? > > I'm not certain, but I don't think so. > > | As stated above, the major problem of LLVM seems to be inferring > | control flow when it comes to call proc-points. As it's hard to avoid > | proc-point splitting, we leave the cmm-pipeline 'as-is'. We modify the > > I regard the whole proc-point thing as a major wart. I think we should work hard to eliminate it. So: another line of thought might be: how could we influence LLVM so that we didn't need proc-point splitting? I totally agree with you here. However, determining how LLVM needs to be influenced to eliminate proc-point splitting is a thing I won't be capable of doing mid term because of my current knowledge and lack of time. > | To make control flow more apparent to LLVM, they came up with the > | following idea. Remark before showing the idea: I know that it greatly > > I'm sorry to say that I didn't really understand the idea. Maybe someone else did? David Terei? My apologies for being imprecise. I hope to find the time to work out a little demonstration during the upcoming holidays. I'm currently fully occupied by university because of upcoming exams this week. > If you are seriously about investing effort in the back end, I'd be happy to help; in that case a Skype call is probably the best way. That is a great idea. Due to the above mentioned time constraints I propose that we follow up in January. Regards, David > Simon > > | interferes with CPS. It leaves parts of the continuation-handling to > | the implicit LLVM call-stack. Further, this does not solve the problem > | of proc-point splitting at all. It is more a workaround than a > | solution. > | But it would greatly increase LLVM's possibilities to optimize code > | later on. That's why I found this idea worth mentioning. Especially > | because after reading your answer, Ben, I'm somewhat convinced that > | solving the problem of proc-point splitting is nearly impossible with > | the capabilities of LLVM IR available at the moment. Now back to the > | idea. > | > | As stated above, the major problem of LLVM seems to be inferring > | control flow when it comes to call proc-points. As it's hard to avoid > | proc-point splitting, we leave the cmm-pipeline 'as-is'. We modify the > | code, llvmGen produces when it comes to call proc-points instead. All > | other types of proc-points remain unchanged. > | > | Initial situation in pseudo cmm: > | > | foo() { > | ... > | call bar() returns to cont // bar defined externally > | > | cont: > | ... > | } > | > | After proc-point splitting, this is converted into LLVM IR similar to > | the following: > | > | @foo() { > | ... > | store @cont(), %Sp ; push continuation on the stack tail call @bar() ; > | @bar defined externally } > | > | @cont() { > | ... > | } > | > | To fix the above issue, we introduce a method, which restores the > | pointers Sp, Hp and the register R1 (among everything else, what has > | to be restored) and 'fakes' the continuation. Note, that '@restore' > | returns without calling into the continuation. This way, the call into > | the continuation can be made direct. The above code would be > | transformed into something similar to the following: > | > | @foo() { > | ... > | store @restore(), %Sp ; 'fake' continuation call @bar() ; br label > | restore > | > | restore: > | %Sp = load (getelementptr @environment 0, 0) ; restore what has to be > | ... ; restored tail call @cont() } > | > | @cont() { > | ... > | } > | > | @restore(%Sp, %Hp, %R1, ...) { > | store %Sp, (getelementptr @environment 0, 0) ; store everything into > | ... ; global variable ret void } > | > | @environment ; structure of type similar to {i64*, i64*, i64*, i64, > | i64, ..} > | > | As an alternative, the above transformation could be done by a LLVM > | pass. llvmGen could then annotate the continuation of calls call cite. > | This would greatly simplify the detection of the correct continuation. > | > | What do you think about this idea? Especially when thinking about the > | interference with CPS? > | > | Regards, > | > | David > | > | > | > | > | [1] > | https://ghc.haskell.org/trac/ghc/wiki/Commentary/Compiler/GeneratedCod > | e#Importantconceptsinthemachine > | > | [2] > | https://ghc.haskell.org/trac/ghc/wiki/Commentary/Compiler/CodeGen#Seco > | ndstage:theCmmpipeline > | > | > | > | > | On 11/21/2015 12:00 AM, Ben Gamari wrote: > | > Simon Peyton Jones <simonpj(a)microsoft.com> writes: > | > > | >> David > | >> > | >> All this stuff is terribly paged-out for me. But I'd love someone > | to > | >> pay attention to some of this back-end stuff, so if you'd like to > | >> work there, I'd like to help you. > | >> > | >> David Terei was also thinking of getting rid of proc point > | splitting > | >> for LLVM (see attached email and the notes attached to it) > | >> > | >> Simon Marlow also was thinking about this; see his attached email. > | >> > | >> The main *reason* for establishing a proc-point is so that, when > | >> generating C code (which we don't do any more) you can take its > | >> address. E.g. > | >> > | >> foo() { ... Push &bar onto the stack (effectively a return address) > | >> Jump to thingumpy } > | >> > | >> bar() { ... } > | >> > | >> Really bar is part of foo, but we have make it a separate top level > | >> thing so that we can take the address of bar and push it on the > | stack. > | >> > | >> The trouble is that if there is a label inside bar that foo wants > | to > | >> jump to (i.e. without pushing &bar etc) then we have to make that > | >> label too into a proc-point, so that both foo and bar can see it. > | >> Urgh. > | >> > | >> In LLVM this probably is not true; presumably you can take the > | >> address of any label? > | >> > | > This is true. While labels themselves have function-local scope in > | > LLVM, there is an expression, `blockaddress`, which allows you to > | take > | > an address to a label in another function [1]. That being said, in > | > reading through the documentation it's not at all clear to me that > | it > | > would be safe to jump to such an address. In fact, given that the > | > instruction that this expression is supposed to be used with, > | > `indirectbr`, can only be used for local blocks, I suspect it is > | not. > | > More information about this feature can be found here [2]. > | > > | > The jump issue aside, I don't know how you would deal with > | > tables-next-to-code. The prefix data support that currently > | available > | > in LLVM is attached to functions and I unfortunately don't see that > | > changing any time soon. > | > > | > Ultimately it seems that trying to refer to labels defined in other > | > functions is using LLVM against the way it was intended. One > | > alternative would be to teach llvmGen to merge mutually recusive > | > top-level functions into a single LLVM function during code > | > generation. Otherwise I'm afraid you are stuck with either the > | status > | > quo or attempting to improve on LLVM's own cross-procedure > | optimization ability. > | > > | > That being said, it sounds as though eliminating proc-point > | splitting > | > would make for quite a nice project in the native code generator. > | > > | > Cheers, > | > > | > - Ben > | > > | > > | > [1] > | > > | https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fllvm.o > | > rg%2fdocs%2fLangRef.html%23addresses-of-basic- > | blocks&data=01%7c01%7csi > | > > | monpj%40064d.mgd.microsoft.com%7c7fdbfda0b4514a098c4d08d2f74448f1%7c72 > | > > | f988bf86f141af91ab2d7cd011db47%7c1&sdata=nKVLgmZezUdEYL%2fma1exMMPLbcT > | > RkaE1JrvVaR1EesY%3d [2] > | > > | https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fblog.l > | > lvm.org%2f2010%2f01%2faddress-of-label-and-indirect- > | branches.html&data > | > > | =01%7c01%7csimonpj%40064d.mgd.microsoft.com%7c7fdbfda0b4514a098c4d08d2 > | > > | f74448f1%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=BTMdZESwYS4tZa5W > | > sOAqyFutoI5xNNFDe0b%2bdKC3ODs%3d [3] > | > > | https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fllvm.o > | > rg%2fdocs%2fLangRef.html%23prefix- > | data&data=01%7c01%7csimonpj%40064d.m > | > > | gd.microsoft.com%7c7fdbfda0b4514a098c4d08d2f74448f1%7c72f988bf86f141af > | > > | 91ab2d7cd011db47%7c1&sdata=rdo4ZLjjE%2bWxNykVL%2bSuToWioY6nzQpflSk296E > | > 8W70%3d > | > >

3 4

Generalising the demand analysis to sum types
by José Manuel Calderón Trilla 04 Mar '16

04 Mar '16

Hello ghc-devs, Apologies for the longish email. I'm looking to generalise GHC's demand analysis to work on sum types. This is in connection with the work on unboxed sums. The idea is that if the strictness analysis tells us that a sum type is strict in all the fields of all of its constructors, it is safe to unbox that sum automatically. We hope for this to feed into a worker/wrapper like transformation for sum types. I am new to the GHC codebase and wanted to make sure that my plan of attack seemed sensible to you all. GHC's current type representing demand is StrDmd, which is defined as follows: data StrDmd = HyperStrict | SCall StrDmd | SProd [ArgStr] | HeadStr I believe that adding sum types will be as simple as adding a single new constructor for Sums: data StrDmd = HyperStrict | SCall StrDmd | SProd [ArgStr] | SSum [(Tag, StrDmd)] | HeadStr We need the constructor tag so that we can analyze each branch of a case expression independently before combining the results of each branch. Since we only care if all fields are strict for all constructors, we won't actually use the tag information except in the analysis itself. Projection-based strictness analysis on sum types is not new (though sum types + higher-order seems to be). That being said, all previous treatments of the subject that I'm aware of forbid polymorphic recursion. Luckily for us we aren't trying to unbox recursive types, so for now [1] we will not attempt to analyze recursive types, hence no SMu or SRec constructor above. With the analysis accepting sum types we will be able to analyze functions with sum types as parameters, as a trivial example: fromMaybe2 x y = case x of Just v -> v Nothing -> y You would get a demand signature like: Str=Dmdtype <S[("Just", <S,U>), ("Nothing", <>)],U><L,U> Which says that the function is strict in its first argument and that if the value is a 'Just' then its field is used strictly, if the value is a 'Nothing' then there is no further demand (a nullary product). For those with more experience in these matter, does this seem to be a sensible approach? Thanks in advance for any insight, Jose [1]: Those of you who saw my Haskell Symposium talk on implicit parallelism last year might remember that we will need the analysis to work on recursive types in order to automatically generate parallel strategies, but that's for later (I've spoken with Ilya Sergey about working on that).

4 8

RTS's (old?) invariant regarding OS blocking
by Dan Aloni 03 Mar '16

03 Mar '16

Hi, While trying to gain insights into the RTS, I've noticed the following in the Wiki page [1] on the topic of the scheduler: Invariant: a task that holds a capability is not blocked in the operating system. This makes some parts of the system simpler - for example, we can use spin locks that spin indefinitely, because we can ensure that the spin lock is only held by a currently executing CPU, and will therefore be released in a finite (and short) amount of time. Does it still apply to modern day GHC, or was it addressed by [2]? [1] https://ghc.haskell.org/trac/ghc/wiki/Commentary/Rts/Scheduler#Capabilities [2] https://ghc.haskell.org/trac/ghc/ticket/3553 -- Dan Aloni

2 2

Simple "Hello World" Warp-based web server crashes on Ubuntu x86_64
by Антон Десятов 02 Mar '16

02 Mar '16

Hello dear GHC developers, I have recently experienced what I believe to be a bug either in GHC or in Warp library (if it is indeed in Warp then sorry for posting to wrong mailing list). I've managed to shrink it to a few lines of code and publish on a GitHub. Here is the link: https://github.com/anton-dessiatov/warp-ghc-issue What I wanted to do is to establish network connection in my code and then at some point pass it to Warp for further processing. What I got is that after successfully processing first HTTP request my program consumes 100% CPU and eventually crashes with an error like this: *** Error in `/home/farnsworth/work/warp-ghc-issue/.stack-work/install/x86_64-linux/lts-5.5/7.10.3/bin/warp-ghc-issue': double free or corruption (!prev): 0x00000000016214b0 *** Aborted (core dumped) When compiled with -debug I see another message: repro: internal error: ASSERTION FAILED: file rts/Schedule.h, line 137 (GHC version 7.10.3 for x86_64_unknown_linux) Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug Aborted (core dumped) I tried to debug it by enabling -dcore-lint and -debug in my ~/.stack/config.yaml and what worries me is that in this case Warp itself doesn't compile (tried with 7.10.2 and 7.10.3) giving core lint failure in Network.Wai.Handler.Warp.HTTP2.Worker. Not sure if it is relevant, but looks suspicious. Could anybody please try building my code on x64 Linux, run it, open localhost:8080 in a web browser and confirm that there is indeed a bug? Regards, Anton.

4 8

Re: GADTs and functional dependencies?
by Iavor Diatchki 01 Mar '16

01 Mar '16

Hello Conal, the implementation of fun-deps in GHC is quite limited, and they don't do what you'd expect with existential types (like in your example), type-signatures, or GADTs. Basically, GHC only uses fun-deps to fill-in types for unification variables, but it won't use them to reason about quantified variables. Here is an example that shows the problem, just using type signatures: > class F a b | a -> b where > f :: a -> b -> () > > instance F Bool Char where > f _ _ = () > > test :: F Bool a => a -> Char > test a = a GHC rejects the declaration for `test` because there it needs to prove that `a ~ Char`. Using the theory of fun-deps, the equality follows because from the fun-dep we know that: forall x y z. (F x y, F x z) => (y ~ z) Now, if we instantiate this axiom with `Bool`, `Char`, and `a`, we can prove that `Char ~ a` by combining the instance and the local assumption from the signature. Unfortunately, this is exactly the kind of reasoning GHC does not do. I am not 100% sure on why not, but at present GHC will basically do all the work to ensure that the fun-dep axiom for each class is valid (that's all the checking that instances are consistent with their fun-deps), but then it won't use that invariant when solving equalities. I hope this helps! -Iavor On Tue, Mar 1, 2016 at 9:38 AM, Conal Elliott <conal(a)conal.net> wrote: > Do GADTs and functional dependencies get along? I'm wondering why the > following code doesn't type-check under GHC 7.10.3 and 8.1.20160224: > > > {-# OPTIONS_GHC -Wall #-} > > {-# LANGUAGE GADTs, KindSignatures, MultiParamTypeClasses, > FunctionalDependencies #-} > > > > module FundepGadt where > > > > class C a b | a -> b > > > > data G :: * -> * where > > -- ... > > GC :: C a b => G b -> G a > > > > instance Eq (G a) where > > -- ... > > GC b == GC b' = b == b' > > Error message: > > FundepGadt.hs:14:25: error: > • Couldn't match type 'b1’ with 'b’ > 'b1’ is a rigid type variable bound by > a pattern with constructor: GC :: forall a b. C a b => G b -> > G a, > in an equation for '==’ > at FundepGadt.hs:14:12 > 'b’ is a rigid type variable bound by > a pattern with constructor: GC :: forall a b. C a b => G b -> > G a, > in an equation for '==’ > at FundepGadt.hs:14:3 > Expected type: G b > Actual type: G b1 > • In the second argument of '(==)’, namely 'b'’ > In the expression: b == b' > In an equation for '==’: (GC b) == (GC b') = b == b' > • Relevant bindings include > b' :: G b1 (bound at FundepGadt.hs:14:15) > b :: G b (bound at FundepGadt.hs:14:6) > > I think the functional dependency does ensure that "b == b" is well-typed. > > In contrast, the following type-family version does type-check: > > > {-# OPTIONS_GHC -Wall #-} > > {-# LANGUAGE GADTs, KindSignatures, TypeFamilies #-} > > > > module TyfamGadt where > > > > class C a where > > type B a > > > > data G :: * -> * where > > -- ... > > GC :: C a => G (B a) -> G a > > > > instance Eq (G a) where > > -- ... > > GC b == GC b' = b == b' > > Thanks, - Conal > > _______________________________________________ > ghc-tickets mailing list > ghc-tickets(a)haskell.org > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets > >

2 2

Patches/proposals waiting for review
by Thomas Miedema 01 Mar '16

01 Mar '16

Hi Simon, the following issues are waiting for your review: * https://phabricator.haskell.org/D1762 "Fix #11348 handle instance dependencies" by Alexander Vieth * https://phabricator.haskell.org/D1896 "Improve printing of pattern synonym types" by Rik Steenkamp * https://ghc.haskell.org/trac/ghc/wiki/ShorterImportSyntax by Anthony Cowley Maybe others, they should show up under "Blocking Others" when you go to https://phabricator.haskell.org/ Thanks, Thomas

5 4

GHC 8.0.1 status
by Ben Gamari 01 Mar '16

01 Mar '16

tl;dr. Stabilizing the ghc-8.0 is taking a bit longer than was anticipated. The release schedule is being pushed back a bit. Hello everyone, As you likely know we are currently in the depths of the 8.0 release. In fact, under more ideal circumstances I would probably be cutting another release candidate right now instead of writing this email, in preparation for a final release next week or so. However, our world is far from ideal as evidenced by the number [1] of significant bugs present on the 8.0 branch. This isn't altogether unexpected; we knew we were taking a bit of a risk in merging so many high-impact patches in one release. However, we thought that given a longer-than-usual period between first-candidate and the final release, we'd have enough time to smooth out the wrinkles. Sadly, this has taken a bit longer than we anticipated. Of course, the last thing we want is to push a known buggy release out the door. Consequently, we won't be delivering the 8.0.1 release next week as originally planned. Instead, we'll be pushing the release back by about three weeks. This will give developers a bit more breathing room in which to work out the remaining issues. Hopefully in a few weeks the tree will be in such a state that we can push out yet another candidate which, with luck, will be the last before the release. If you'd like to expedite the process (and have fun in the process), you could do worse than to having a look at Trac [1], choosing a bug of your liking, and trying your hand at solving it. Thanks to everyone who has contributed to this effort thusfar. If you have any questions about the release process or how you can help, don't hesistate to ask. Cheers, - Ben [1] https://ghc.haskell.org/trac/ghc/wiki/Status/GHC-8.0.1

3 4

Change in demand analysis results between 7.10.2 and RC1 (not fixed in RC2 and HEAD)
by Ömer Sinan Ağacan 29 Feb '16

29 Feb '16

Hi all, While working on demand analyzer today we realized that there has been some changes in demand analysis results between GHC 7.10.2 and 8.0-rc2. Here's a minimal example: {-# LANGUAGE BangPatterns #-} module Main where data Prod a = Prod !a !a addProd :: Prod Int -> Prod Int -> Prod Int addProd (Prod i1 i2) (Prod i3 i4) = Prod i1 (i2 + i4) main = return () Compiled with 7.10.2: addProd :: Prod Int -> Prod Int -> Prod Int [GblId, Arity=2, Caf=NoCafRefs, Str=DmdType <S(SS),1*U(U,U(U))><S(SS),1*U(1*H,U(U))>m, ...}}}}] addProd = \ (ds_dzH :: Prod Int) (ds1_dzI :: Prod Int) -> case ds_dzH of _ [Occ=Dead] { Prod i1_an2 i2_an3 -> case i2_an3 of _ [Occ=Dead] { GHC.Types.I# x_s2B4 -> case ds1_dzI of _ [Occ=Dead] { Prod i3_an4 i4_an5 -> case i4_an5 of _ [Occ=Dead] { GHC.Types.I# y_s2B7 -> Main.Prod @ Int i1_an2 (GHC.Types.I# (GHC.Prim.+# x_s2B4 y_s2B7)) } } } } Compiled with 8.0-rc2: -- RHS size: {terms: 20, types: 17, coercions: 0} addProd :: Prod Int -> Prod Int -> Prod Int [GblId, Arity=2, Caf=NoCafRefs, Str=DmdType <S(SS),1*U(U,U(U))><S(LS),1*U(A,U(U))>m, ...}}}}] addProd = \ (ds_dQL :: Prod Int) (ds1_dQM :: Prod Int) -> case ds_dQL of _ [Occ=Dead] { Prod i1_avS i2_avT -> case i2_avT of _ [Occ=Dead] { GHC.Types.I# x_s1vO -> case ds1_dQM of _ [Occ=Dead] { Prod i3_avU i4_avV -> case i4_avV of _ [Occ=Dead] { GHC.Types.I# y_s1vR -> Main.Prod @ Int i1_avS (GHC.Types.I# (GHC.Prim.+# x_s1vO y_s1vR)) } } } } To highlight the difference, GHC 7.10.2: <S(SS),1*U(U,U(U))><S(SS),1*U(1*H,U(U))> GHC 8.0-rc2: <S(SS),1*U(U,U(U))><S(LS),1*U(A,U(U))> (NOTE: Also tried with HEAD and rc1 just now, the results are the same as rc2) The demand put on the second argument is more strict in GHC 7.10. Was that an intentional change? Any ideas on why this might be happening? In our case, we prefer the result in 7.10.2 of course, because that's a more precise demand and it gives us more opportunities for optimizations. But I guess this could potentially reveal itself in some other situations and make some programs slower? Any ideas? Thanks..

3 4