- ghc-devs - Haskell.org

Fwd: [GHC] #11683: compiled files don't load in ghci
by George Colpitts 06 Mar '16

06 Mar '16

---------- Forwarded message --------- From: GHC <ghc-devs(a)haskell.org> Date: Sun, Mar 6, 2016 at 1:23 PM Subject: [GHC] #11683: compiled files don't load in ghci To: Cc: <ghc-tickets(a)haskell.org> #11683: compiled files don't load in ghci -------------------------------------+------------------------------------- Reporter: George | Owner: Type: bug | Status: new Priority: high | Milestone: Component: Compiler | Version: 8.0.1-rc2 Keywords: | Operating System: MacOS X Architecture: | Type of failure: Incorrect result Unknown/Multiple | at runtime Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- compiled files don't load in ghci {{{ ghc -DYNAMIC bug.hs [1 of 1] Compiling Main ( bug.hs, bug.o ) Linking bug ... bash-3.2$ ghci -ignore-dot-ghci GHCi, version 8.0.0.20160204: http://www.haskell.org/ghc/ :? for help Prelude> Prelude> :load bug [1 of 1] Compiling Main ( bug.hs, interpreted ) Ok, modules loaded: Main. *Main> :show modules Main ( bug.hs, interpreted ) *Main> }}} According to the doc, file:///usr/local/share/doc/ghc-8.0.0.20160204/html/users_guide/ghci.html #loading-compiled-code, this should work: {{{ Note the -dynamic flag to GHC: GHCi uses dynamically-linked object code (if you are on a platform that supports it), and so in order to use compiled code with GHCi it must be compiled for dynamic linking. }}} Similarly https://ghc.haskell.org/trac/ghc/ticket/8736#comment:4 says the same thing: {{{ if you say :load Foo in GHCi Foo was compiled with -dynamic: loads Foo.o }}} Interestingly -fobject-code does work: {{{ ghci -ignore-dot-ghci -fobject-code GHCi, version 8.0.0.20160204: http://www.haskell.org/ghc/ :? for help Prelude> :load bug [1 of 1] Compiling Main ( bug.hs, bug.o ) Ok, modules loaded: Main. Prelude Main> }}} Unfortunately when I do {{{ ghci -v -ignore-dot-ghci -fobject-code }}} I don't see why it works. It doesn't seem to use just ghc to compile , it also uses gcc, see attached file. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11683> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

'lub' and 'both' on strictness - what does it mean for products to have different arity?
by Ömer Sinan Ağacan 04 Mar '16

04 Mar '16

I was looking at implementations of LUB and AND on demand signatures and I found this interesting case: lubStr (SProd s1) (SProd s2) | length s1 == length s2 = mkSProd (zipWith lubArgStr s1 s2) | otherwise = HeadStr The "otherwise" case is interesting, I'd expect that to be an error. I'm trying to come up with an example, let's say I have a case expression: case x of P1 -> RHS1 P2 -> RHS2 and y is used in RHS1 with S(SS) and in RHS2 with S(SSS). This seems to me like a type error leaked into the demand analysis. Same thing applies to `bothDmd` too. Funnily, it has this extra comment on this same code: bothStr (SProd s1) (SProd s2) | length s1 == length s2 = mkSProd (zipWith bothArgStr s1 s2) | otherwise = HyperStr -- Weird Does "Weird" here means "type error and/or bug" ? Should I try replacing these cases with panics and try to validate?

3 7

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