Re: [GHC] #4879: Deprecate exports
#4879: Deprecate exports -+-- Reporter: basvandijk|Owner: Type: feature request | Status: new Priority: normal|Milestone: 7.2.1 Component: Compiler | Version: 7.0.1 Keywords:| Testcase: Blockedby:| Difficulty: Os: Unknown/Multiple | Blocking: Architecture: Unknown/Multiple | Failure: None/Unknown -+-- Comment(by simonpj): Ah, now I see. It's a bit like deprecating the definition of `lines` in `Data.List`, where in this case the definition is the import from `Data.String`. But there are questions of course. What if I now say {{{ module Foo( lines ) where import Data.List( lines ) }}} Do I get a deprecation message from the mention of `lines` in the export list? What if there was no export list was `moudle Foo( module Data.List )`? What if something is in scope more than one way, one deprecated and one not: {{{ module Bar where import Data.List( lines ) import Data.String( lines ) f = lines }}} Do I get a deprecation warning? Or does the use pick the best import declaration? What if something is imported two ways, and ''both'' are separately deprectated. Does it accumulate two deprecation warnings? What if a moudule M imports `Data.List(lines)`, and re-exports `lines`? Is an import from M deprecated? That is, are deprecations transitive? Thinking about it, a possible view is this: * The existing deprecating mechanism attaches a deprecation to a ''definition'', and complains at a ''use'', but not at imports. * The new mechanism attaches a deprecation to an ''export'' (from module M, say), and complains at ''import'' (of module M only), but but not at uses. Under this interpretation it's not clear whether plain `import module M` should do. But regardless, there are lots of details to be worked out. Whether the pain is worth the gain is not clear to me. Simon -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4879#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4875: ghc misdiagnoses a compile time error concerning parameterized types
#4875: ghc misdiagnoses a compile time error concerning parameterized types -+-- Reporter: Stef Joosten |Owner: simonpj Type: bug | Status: new Priority: normal|Milestone: 7.2.1 Component: Compiler | Version: 6.12.3 Keywords:| Testcase: Blockedby:| Difficulty: Os: Windows | Blocking: Architecture: Unknown/Multiple | Failure: Other -+-- Comment(by simonpj): Yes, I was on a plane so I started working on this. Patch coming. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4875#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4856: Performance regression in the type checker regression for GADTs and type families
#4856: Performance regression in the type checker regression for GADTs and type families +--- Reporter: chak |Owner: Type: bug | Status: new Priority: high |Milestone: 7.0.3 Component: Compiler (Type checker) | Version: 7.0.1 Keywords: | Testcase: Blockedby: | Difficulty: Os: Unknown/Multiple | Blocking: Architecture: Unknown/Multiple | Failure: Compile-time performance bug +--- Comment(by simonpj): I'm working on it. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4856#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4370: Bring back monad comprehensions
#4370: Bring back monad comprehensions -+-- Reporter: simonpj |Owner: nsch Type: feature request | Status: new Priority: normal|Milestone: 7.2.1 Component: Compiler | Version: 6.12.3 Keywords:| Testcase: Blockedby:| Difficulty: Os: Unknown/Multiple | Blocking: Architecture: Unknown/Multiple | Failure: None/Unknown -+-- Comment(by simonpj): I didn't highlight enough above, but my suggestion is to add a new `Stmt` constructor, namely `ReturnStmt` to use as the last `Stmt` of a block. Rather than using `ExprStmt` which, as you say, isn't really right. Oh, if you prefer to call it `BodyStmt` that's fine too. Re second point, yes, the whole idea would be to remove the `body` argument from `tcExpr` and instead have it deal only with a `[Stmt]`. Make sense? -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4370#comment:26 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #3472: Porting through .hc files broken
#3472: Porting through .hc files broken -+-- Reporter: pumpkin | Type: bug Status: new | Priority: high Milestone: 7.2.1 |Component: Build System Version: 6.12.1 RC1| Resolution: Keywords:| Testcase: Blockedby:| Difficulty: Unknown Os: Unknown/Multiple | Blocking: Architecture: Unknown/Multiple | Failure: None/Unknown -+-- Changes (by simonmar): * milestone: 7.0.2 = 7.2.1 -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/3472#comment:29 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4163: Make cross-compilation work
#4163: Make cross-compilation work -+-- Reporter: simonmar |Owner: Type: task | Status: new Priority: high |Milestone: 7.2.1 Component: Build System | Version: 6.12.3 Keywords:| Testcase: Blockedby:| Difficulty: Difficult (2-5 days) Os: Unknown/Multiple | Blocking: Architecture: Unknown/Multiple | Failure: None/Unknown -+-- Changes (by simonmar): * milestone: 7.0.2 = 7.2.1 -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4163#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4839: RTS assertion failure when heap profiling threaded programs.
#4839: RTS assertion failure when heap profiling threaded programs. -+-- Reporter: benl |Owner: igloo Type: bug | Status: new Priority: high |Milestone: 7.0.3 Component: Runtime System| Version: 7.0.1 Keywords:| Testcase: Blockedby:| Difficulty: Os: MacOS X | Blocking: Architecture: Unknown/Multiple | Failure: Runtime crash -+-- Changes (by simonmar): * owner: simonmar = igloo Comment: Igloo is going to try reproducing it on OS X. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4839#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #2722: loop when compiling with -O option with ghc-6.10.0.20081019
#2722: loop when compiling with -O option with ghc-6.10.0.20081019 +--- Reporter: uwe| Owner: simonpj Type: bug| Status: new Priority: normal | Milestone: 7.0.3 Component: libraries (other) |Version: 7.0.1 Resolution: | Keywords: arrows Testcase: | Blockedby: Difficulty: Unknown| Os: Linux Blocking: | Architecture: x86_64 (amd64) Failure: Runtime crash | +--- Changes (by simonmar): * owner: = simonpj -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/2722#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4831: Infinite loop in SpecConstr
#4831: Infinite loop in SpecConstr -+-- Reporter: simonpj |Owner: simonpj Type: bug | Status: new Priority: normal|Milestone: 7.0.3 Component: Compiler | Version: 7.0.1 Keywords:| Testcase: Blockedby:| Difficulty: Os: Unknown/Multiple | Blocking: Architecture: Unknown/Multiple | Failure: None/Unknown -+-- Changes (by simonmar): * owner: = simonpj -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4831#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4849: object code size fairly large for ghc-7.0.1 with optimization
#4849: object code size fairly large for ghc-7.0.1 with optimization -+-- Reporter: maeder|Owner: igloo Type: bug | Status: new Priority: normal|Milestone: 7.0.3 Component: Compiler | Version: 7.0.1 Keywords:| Testcase: Blockedby:| Difficulty: Os: Unknown/Multiple | Blocking: Architecture: Unknown/Multiple | Failure: Compile-time performance bug -+-- Changes (by igloo): * owner: = igloo -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4849#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4874: Unnecessary reboxing when using INLINABLE
#4874: Unnecessary reboxing when using INLINABLE -+-- Reporter: tibbe |Owner: simonpj Type: bug | Status: new Priority: normal|Milestone: 7.0.3 Component: Compiler | Version: 7.0.1 Keywords:| Testcase: Blockedby:| Difficulty: Os: Unknown/Multiple | Blocking: Architecture: Unknown/Multiple | Failure: None/Unknown -+-- Changes (by simonmar): * owner: = simonpj -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4874#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4877: Template Haskell panic when splicing an infix expression with a non-variable middle bit
#4877: Template Haskell panic when splicing an infix expression with a non- variable middle bit -+-- Reporter: benmachine|Owner: simonpj Type: bug | Status: new Priority: normal|Milestone: 7.0.3 Component: Template Haskell | Version: 7.0.1 Keywords:| Testcase: Blockedby:| Difficulty: Os: Unknown/Multiple | Blocking: Architecture: Unknown/Multiple | Failure: Compile-time crash -+-- Changes (by simonmar): * owner: = simonpj -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4877#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4875: ghc misdiagnoses a compile time error concerning parameterized types
#4875: ghc misdiagnoses a compile time error concerning parameterized types --+- Reporter: Stef Joosten | Owner: simonpj Type: bug | Status: closed Priority: normal | Milestone: 7.2.1 Component: Compiler |Version: 6.12.3 Resolution: fixed| Keywords: Testcase: typecheck/should_fail/T4875 | Blockedby: Difficulty: | Os: Windows Blocking: | Architecture: Unknown/Multiple Failure: Other| --+- Changes (by simonpj): * status: new = closed * testcase: = typecheck/should_fail/T4875 * resolution: = fixed Comment: Fixed by {{{ }}} Try not to push this to the 7.0 branch because it'll (correctly) reject a few programs that 7.0 accepts. Simon -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4875#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4875: ghc misdiagnoses a compile time error concerning parameterized types
#4875: ghc misdiagnoses a compile time error concerning parameterized types --+- Reporter: Stef Joosten | Owner: simonpj Type: bug | Status: closed Priority: normal | Milestone: 7.2.1 Component: Compiler |Version: 6.12.3 Resolution: fixed| Keywords: Testcase: typecheck/should_fail/T4875 | Blockedby: Difficulty: | Os: Windows Blocking: | Architecture: Unknown/Multiple Failure: Other| --+- Comment(by simonpj): Oops I missed out the commit message: {{{ Mon Jan 10 11:03:51 GMT 2011 simo...@microsoft.com * Do dependency analysis when kind-checking type declarations This patch fixes Trac #4875. The main point is to do dependency analysis on type and class declarations, and kind-check them in dependency order, so as to improve error messages. This patch means that a few programs that would typecheck before won't typecheck any more; but before we were (naughtily) going beyond Haskell 98 without any language-extension flags, and Trac #4875 convinces me that doing so is a Bad Idea. Here's an example that won't typecheck any more data T a b = MkT (a b) type F k = T k Maybe If you look at T on its own you'd default 'a' to kind *-*; and then kind-checking would fail on F. But GHC currently accepts this program beause it looks at the *occurrences* of T. M ./compiler/deSugar/DsMeta.hs -1 +1 M ./compiler/hsSyn/HsDecls.lhs -2 +8 M ./compiler/hsSyn/HsUtils.lhs -3 +4 M ./compiler/rename/RnNames.lhs -1 +1 M ./compiler/rename/RnSource.lhs -11 +52 M ./compiler/typecheck/TcInstDcls.lhs -1 +1 M ./compiler/typecheck/TcRnDriver.lhs -5 +5 M ./compiler/typecheck/TcTyClsDecls.lhs -224 +139 M ./compiler/typecheck/TcTyDecls.lhs +37 M ./utils/ghctags/Main.hs -1 +1 }}} -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4875#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4870: Compiler panic with SPECIALIZE pragma on function from imported module
#4870: Compiler panic with SPECIALIZE pragma on function from imported module -+-- Reporter: dreixel |Owner: Type: bug | Status: merge Priority: high |Milestone: 7.0.3 Component: Compiler | Version: 7.0.1 Keywords:| Testcase: deSugar/should_compile/T4870 Blockedby:| Difficulty: Os: Unknown/Multiple | Blocking: Architecture: Unknown/Multiple | Failure: None/Unknown -+-- Changes (by simonpj): * status: new = merge * testcase: = deSugar/should_compile/T4870 Comment: Thanks for the example. Fixed by {{{ Wed Jan 5 00:27:12 GMT 2011 simo...@microsoft.com * Fix Trac #4870: get the inlining for an imported INLINABLE Id We need the unfolding even for a *recursive* function (indeed that's the point) and I was using the wrong function to get it (idUnfolding rather than realIdUnfolding). M ./compiler/deSugar/DsBinds.lhs -6 +7 }}} Please merge to 7.0 branch Simon -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4870#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4875: ghc misdiagnoses a compile time error concerning parameterized types
#4875: ghc misdiagnoses a compile time error concerning parameterized types --+- Reporter: Stef Joosten | Owner: simonpj Type: bug | Status: closed Priority: normal | Milestone: 7.2.1 Component: Compiler |Version: 6.12.3 Resolution: fixed| Keywords: Testcase: typecheck/should_fail/T4875 | Blockedby: Difficulty: | Os: Windows Blocking: | Architecture: Unknown/Multiple Failure: Other| --+- Comment(by Stef Joosten): Simon, thank you for this. Yours, Stef Joosten -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4875#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4884: registerPackage fails with multiple command line --package-conf= flags
#4884: registerPackage fails with multiple command line --package-conf= flags --+- Reporter: r6 | Owner: Type: bug | Status: closed Priority: normal | Milestone: 7.2.1 Component: ghc-pkg |Version: 6.12.3 Resolution: invalid | Keywords: Testcase: | Blockedby: Difficulty: | Os: Linux Blocking: | Architecture: x86 Failure: Incorrect result at runtime | --+- Changes (by simonmar): * status: new = closed * resolution: = invalid Comment: This is the documented behaviour of `ghc-pkg`. In the output of `ghc-pkg --help`: {{{ When asked to modify a database (register, unregister, update, hide, expose, and also check), ghc-pkg modifies the global database by default. Specifying --user causes it to act on the user database, or --package-conf can be used to act on another database entirely. When multiple of these options are given, the rightmost one is used as the database to act upon. }}} So in your command line: {{{ ghc-pkg --package-conf=myPkg1 --package-conf=myPkg2 --package-conf=myPkg3 --global --user update newPkg.conf }}} Since `--user` is the rightmost option, that is the DB to act on. The user DB can only depend on the global DB, so you get the stack `[user,global]`. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4884#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4385: Type-level natural numbers
#4385: Type-level natural numbers +--- Reporter: diatchki |Owner: diatchki Type: feature request | Status: new Priority: normal |Milestone: 7.2.1 Component: Compiler (Type checker) | Version: Keywords: | Testcase: Blockedby: | Difficulty: Os: Unknown/Multiple | Blocking: Architecture: Unknown/Multiple | Failure: None/Unknown +--- Comment(by simonpj): Iavor: what's your plan for this? I'd like to have it in the HEAD, but we need to resolve the design issues first. Also I'm unsure about whether you are actively developing or whether you've moved on to other things. Oh, one other thing that isn't clear to me is how all this fits in FC. If a Pressburger solver shows that (a*b = b*a), say how is that expressed as a FC proof term? Simon -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4385#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4884: registerPackage fails with multiple command line --package-conf= flags
#4884: registerPackage fails with multiple command line --package-conf= flags --+- Reporter: r6 | Owner: Type: bug | Status: closed Priority: normal | Milestone: 7.2.1 Component: ghc-pkg |Version: 6.12.3 Resolution: invalid | Keywords: Testcase: | Blockedby: Difficulty: | Os: Linux Blocking: | Architecture: x86 Failure: Incorrect result at runtime | --+- Comment(by r6): Where is it documented that user databases cannot depend on package-conf databases? Also, what is the motivation for such a restriction? -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4884#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4868: deepseq should not depend on containers
#4868: deepseq should not depend on containers --+- Reporter: tibbe |Owner: Type: proposal | Status: new Priority: normal |Milestone: Not GHC Component: libraries (other) | Version: 7.0.1 Keywords: | Testcase: Blockedby: | Difficulty: Os: Unknown/Multiple | Blocking: Architecture: Unknown/Multiple | Failure: None/Unknown --+- Comment(by tibbe): Supported by Henning Thielemann, Milan Straka, Malcolm Wallace, Iavor Diatchki, and Daniel Peebles. Christian Maeder suggested using packages containing only orphaned instances instead. Ian Lynagh raised some concerns about adding another boot package. Henning Thielemann pointed out that the array package should also be included in the proposal. Should you wish to see the whole thread, it begins with http://www.haskell.org/pipermail/libraries/2010-December/015421.html -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4868#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4868: deepseq should not depend on containers
#4868: deepseq should not depend on containers --+- Reporter: tibbe |Owner: Type: proposal | Status: new Priority: normal |Milestone: Not GHC Component: libraries (other) | Version: 7.0.1 Keywords: | Testcase: Blockedby: | Difficulty: Os: Unknown/Multiple | Blocking: Architecture: Unknown/Multiple | Failure: None/Unknown --+- Comment(by tibbe): Christian Maeder has clarified that he's neither for or against the proposal. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4868#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4868: deepseq should not depend on containers
#4868: deepseq should not depend on containers --+- Reporter: tibbe |Owner: Type: proposal | Status: new Priority: normal |Milestone: Not GHC Component: libraries (other) | Version: 7.0.1 Keywords: | Testcase: Blockedby: | Difficulty: Os: Unknown/Multiple | Blocking: Architecture: Unknown/Multiple | Failure: None/Unknown --+- Comment(by tibbe): Ian Lynagh has clarified that he's against the proposal. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4868#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4868: deepseq should not depend on containers
#4868: deepseq should not depend on containers +--- Reporter: tibbe | Owner: Type: proposal | Status: closed Priority: normal | Milestone: Not GHC Component: libraries (other) |Version: 7.0.1 Resolution: wontfix| Keywords: Testcase: | Blockedby: Difficulty: | Os: Unknown/Multiple Blocking: | Architecture: Unknown/Multiple Failure: None/Unknown | +--- Changes (by tibbe): * status: new = closed * resolution: = wontfix Comment: Since consensus wasn't reached and I don't have time to pursue it I'm closing this ticket. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4868#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4385: Type-level natural numbers
#4385: Type-level natural numbers +--- Reporter: diatchki |Owner: diatchki Type: feature request | Status: new Priority: normal |Milestone: 7.2.1 Component: Compiler (Type checker) | Version: Keywords: | Testcase: Blockedby: | Difficulty: Os: Unknown/Multiple | Blocking: Architecture: Unknown/Multiple | Failure: None/Unknown +--- Comment(by diatchki): Hello, I am certainly still working on it, and I think that it'd be great to merge it with HEAD. What would be the best way to work on the design issues---I feel that these ticket comments do not have enough space to discuss things properly. Perhaps I will make a page on the wiki where we (meaning whoever is interested in this feature) can list all the issues and see how to solve them best? I'll update the ticket when I get a chance to do this. Briefly, my current status is: - I've added the syntactic change to treat all symbols as type constructors, and the associated change to the module system. In the process I noticed that GHC does not really use the precedence machinery for infix predicates (classes, ~). Adding support for this is on my TODO list, so that we can write things like `(a + b ~ c)`, rather then `((a + b) ~ c)`. - I've implemented the numeric type literals, which are of a new kind (currently called) Nat. I've added a new form of type `LiteralTy TyLit`, where `TyLit` is a type for type-level literals. Currently, it has only numbers in it but later we could add other things too, if we deemed it useful. - I've added a set of operations on the type numbers, currently: comparison `(=)`, addition `(+)`, multiplication `(*)`, and exponentiation `(^)`. By using equality constraints, we also get their inverses: subtraction, division, logarithms, and roots. My solver is by no means complete although it seems to work for a number of practical examples. I am sure that we can continue to improve it for a long time though. The current implementation cheats on the proofs for the equalities and (=) because it uses unsafeCoercions. At first I had it generate proofs but then you mentioned that you were redoing the evidence mechanism based on Brent's work, and the proofs were getting quite large and difficult to read so I removed them. It would not be hard to re-add them but we should decide on the granularity of the primitive axioms (coercions) to use. The trade-off is basically RISC vs CISC, a smaller set of simpler axioms tends to result in larger proofs. There is also an issue about what evidence to pass for (=). (=) is similar to (~) (and any other class with no methods) in that it does not really need any runtime evidence. I could not see how to adopt the (~) mechanism to account for (=) so, currently, the evidence for (=) is basically a hack (the run-time evidence calls error if it is ever evaluated). It might be nice if we had a unified way to treat things without evidence (e.g., by having a special form of argument that does not emit any run-time code) but I have not looked into how hard would be to do this. Can anyone think of a better way to do this? - In the support library, I made the `DynNat` change that Simon described above. This worked out really nice because this type is basically the type of natural numbers at the value level, so I added all the usual instances for it and called it `Natural`, which mirrors `Integer`. I think that that's all. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4385#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs