January 2013 - ghc-tickets

Re: [GHC] #4259: Relax restrictions on type family instance overlap
by GHC 10 Jan '13

10 Jan '13

#4259: Relax restrictions on type family instance overlap ----------------------------------------+----------------------------------- Reporter: lilac | Owner: Type: feature request | Status: new Priority: normal | Milestone: 7.8.1 Component: Compiler (Type checker) | Version: 6.12.1 Keywords: | Os: Unknown/Multiple Architecture: Unknown/Multiple | Failure: None/Unknown Difficulty: Unknown | Testcase: Blockedby: | Blocking: Related: | ----------------------------------------+----------------------------------- Comment(by carter): well said, I have some thoughts on this. or at least my naive interpretation of a possible unifying point in the design space. I'll add a note on it to this ticket once i've thought about it a bit more -- Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/4259#comment:28> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

Re: [GHC] #6018: Injective type families
by GHC 10 Jan '13

10 Jan '13

#6018: Injective type families ----------------------------------------+----------------------------------- Reporter: lunaris | Owner: simonpj Type: feature request | Status: new Priority: normal | Milestone: 7.8.1 Component: Compiler | Version: 7.4.1 Keywords: TypeFamilies, Injective | Os: Unknown/Multiple Architecture: Unknown/Multiple | Failure: None/Unknown Difficulty: Unknown | Testcase: Blockedby: | Blocking: Related: #4259 | ----------------------------------------+----------------------------------- Changes (by goldfire): * related: => #4259 Comment: Also see the discussion in #4259, which is about strengthening type families along a different dimension. The two tickets are related. -- Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/6018#comment:11> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

Re: [GHC] #4259: Relax restrictions on type family instance overlap
by GHC 10 Jan '13

10 Jan '13

#4259: Relax restrictions on type family instance overlap ----------------------------------------+----------------------------------- Reporter: lilac | Owner: Type: feature request | Status: new Priority: normal | Milestone: 7.8.1 Component: Compiler (Type checker) | Version: 6.12.1 Keywords: | Os: Unknown/Multiple Architecture: Unknown/Multiple | Failure: None/Unknown Difficulty: Unknown | Testcase: Blockedby: | Blocking: Related: | ----------------------------------------+----------------------------------- Comment(by goldfire): Yes. The desire for injective type families (#6018) and this report seem something like treating symptoms instead of the disease. (Don't take that simile too far -- I'm not suggesting GHC's current treatment is somehow diseased, just not as powerful as some want.) What we all seem to want (even if we don't know it) is the ability to define an arbitrary rewrite system over types and for GHC to somehow, magically check that our rewrite system is consistent and then to apply it. I'm pretty sure that goal is impossible. But, we can certainly make inroads in that direction. Relaxing restrictions on instance overlap as described here is one way, and injective type families is another. My current thought on all of this is that we should consider some unified approach with a unified goal, instead of attacking this problem piecemeal. This unified approach may end up devolving into solving these two problems separately, but there should be an articulated reason why these two problems (this ticket and injectivity) are the two problems to solve. -- Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/4259#comment:27> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

Re: [GHC] #5777: core lint error with arrow notation and GADTs
by GHC 10 Jan '13

10 Jan '13

#5777: core lint error with arrow notation and GADTs ---------------------------------+------------------------------------------ Reporter: benmos | Owner: ross Type: bug | Status: new Priority: normal | Milestone: 7.6.2 Component: Compiler | Version: 7.4.2 Keywords: arrows, GADTs | Os: MacOS X Architecture: Unknown/Multiple | Failure: Compile-time crash Difficulty: Unknown | Testcase: Blockedby: | Blocking: Related: | ---------------------------------+------------------------------------------ Changes (by ross): * owner: => ross Comment: I'll put it on my list, but first priority is ArrForm (#5267/#5609), followed by infixr (#5333), with this and #344 as the lowest. -- Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/5777#comment:9> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

Re: [GHC] #7554: Define __SSE__ when compiling with -msse
by GHC 10 Jan '13

10 Jan '13

#7554: Define __SSE__ when compiling with -msse -----------------------------+---------------------------------------------- Reporter: tibbe | Owner: simonmar Type: feature request | Status: patch Priority: normal | Component: Compiler Version: 7.6.1 | Keywords: Os: Unknown/Multiple | Architecture: Unknown/Multiple Failure: None/Unknown | Blockedby: Blocking: | Related: -----------------------------+---------------------------------------------- Changes (by tibbe): * status: new => patch Comment: Simon M, as I removed a 'panic' you added to the code, could you please review? My rationale for removing it is that if the X86 codegen is run and the architecture is not X86, we have bigger problems and we should check that elsewhere (if at all). -- Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/7554#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

Re: [GHC] #7554: Define __SSE__ when compiling with -msse
by GHC 10 Jan '13

10 Jan '13

#7554: Define __SSE__ when compiling with -msse -----------------------------+---------------------------------------------- Reporter: tibbe | Owner: simonmar Type: feature request | Status: new Priority: normal | Component: Compiler Version: 7.6.1 | Keywords: Os: Unknown/Multiple | Architecture: Unknown/Multiple Failure: None/Unknown | Blockedby: Blocking: | Related: -----------------------------+---------------------------------------------- Changes (by tibbe): * owner: => simonmar -- Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/7554#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

Re: [GHC] #5777: core lint error with arrow notation and GADTs
by GHC 10 Jan '13

10 Jan '13

#5777: core lint error with arrow notation and GADTs ---------------------------------+------------------------------------------ Reporter: benmos | Owner: Type: bug | Status: new Priority: normal | Milestone: 7.6.2 Component: Compiler | Version: 7.4.2 Keywords: arrows, GADTs | Os: MacOS X Architecture: Unknown/Multiple | Failure: Compile-time crash Difficulty: Unknown | Testcase: Blockedby: | Blocking: Related: | ---------------------------------+------------------------------------------ Changes (by simonpj): * cc: ross (added) Comment: Ross, do you feel able to help with this. I have no clue. -- Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/5777#comment:8> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

Re: [GHC] #7436: Derived Foldable and Traversable instances become extremely inefficient due to eta-expansion
by GHC 10 Jan '13

10 Jan '13

#7436: Derived Foldable and Traversable instances become extremely inefficient due to eta-expansion --------------------------------------+------------------------------------- Reporter: shachaf | Owner: Type: bug | Status: merge Priority: normal | Milestone: Component: Compiler | Version: 7.6.1 Resolution: fixed | Keywords: Os: Unknown/Multiple | Architecture: Unknown/Multiple Failure: Runtime performance bug | Difficulty: Unknown Testcase: perf/should_runt/T7436 | Blockedby: Blocking: | Related: --------------------------------------+------------------------------------- Changes (by simonpj): * status: closed => merge Comment: I'd be happy to see this in 7.6.2 if there is still time to merge it, Ian. -- Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/7436#comment:19> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

Re: [GHC] #4259: Relax restrictions on type family instance overlap
by GHC 10 Jan '13

10 Jan '13

#4259: Relax restrictions on type family instance overlap ----------------------------------------+----------------------------------- Reporter: lilac | Owner: Type: feature request | Status: new Priority: normal | Milestone: 7.8.1 Component: Compiler (Type checker) | Version: 6.12.1 Keywords: | Os: Unknown/Multiple Architecture: Unknown/Multiple | Failure: None/Unknown Difficulty: Unknown | Testcase: Blockedby: | Blocking: Related: | ----------------------------------------+----------------------------------- Comment(by carter): Replying to [comment:23 goldfire]: > It has also become clear that the ideas leading to this thread have a more general setting than just allowing for relaxed overlap restrictions. For example, given a type family for {{{And}}}, we may want GHC to be able to simplify {{{And x y ~ True}}} to {{{(x ~ True, y ~ True)}}}... but this is certainly not straightforward type family simplification. I'm still not quite sure what the solution is, but my thought is that simply relaxed restrictions on overlap will be 1) hard to do right and 2) not quite enough power anyway. being able to "prove" (And x y) ~ True ---> (x~ True,y~True), and other things like it, that seems like it'd be a generalization of whats needed for Injective type families, right? -- Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/4259#comment:26> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

Re: Fundeps and type equality
by Richard Eisenberg 10 Jan '13

10 Jan '13

For better or worse, the new overlapping type family instances use a different overlapping mechanism than functional dependencies do. Class instances that overlap are chosen among by order of specificity; overlapping instances can be declared in separate modules. Overlapping family instances must be given an explicit order, and those that overlap must all be in the same module. The decision to make these different was to avoid type soundness issues that would arise with overlapping type family instances declared in separate modules. (Ordering a set of family instance equations by specificity, on the other hand, could easily be done within GHC.) So, as yet, we can't fully encode functional dependencies with type families, I don't think. Richard On Jan 2, 2013, at 4:01 PM, Martin Sulzmann <martin.sulzmann.haskell(a)googlemail.com> wrote: > > I agree with Iavor that it is fairly straight-forward to extend FC to support FD-style type improvement. In fact, I've formalized such a proof language in a PPDP'06 paper: > "Extracting programs from type class proofs" > (type improvement comes only at the end) > > Similar to FC, coercions (proof terms) are used to represent type equations (improvement). > > Why extend FC? > Why not simply use type families to encode FDs (and thus keep FC simple and small). > > It's been a while, but as far as I remember, the encoding is only problematic in case of the combination of FDs and overlapping instances. Shouldn't this now be fixable given > that type family instances can be overlapping? > Maybe I'm missing something, guess it's also time to dig out some old notes ... > > -Martin > > On Wed, Jan 2, 2013 at 10:04 AM, Simon Peyton-Jones <simonpj(a)microsoft.com> wrote: > As far as I understand, the reason that GHC does not construct such proofs is that it can't express them in its internal proof language (System FC). > > > > Iavor is quite right > > > > It seems to me that it should be fairly straight-forward to extend FC to support this sort of proof, but I have not been able to convince folks that this is the case. I could elaborate, if there's interest. > > > > Iavor: I don’t think it’s straightforward, but I’m willing to be educated. By all means start a wiki page to explain how, if you think it is. > > > > I do agree that injective type families would be a good thing, and would deal with the main reason that fundeps are sometimes better than type families. A good start would be to begin a wiki page to flesh out the design issues, perhaps linked from http://hackage.haskell.org/trac/ghc/wiki/TypeFunctions > > > > The main issues are, I think: > > · How to express functional dependencies like “fixing the result type and the first argument will fix the second argument” > > · How to express that idea in the proof language > > > > Simon > > > > From: glasgow-haskell-bugs-bounces(a)haskell.org [mailto:glasgow-haskell-bugs-bounces@haskell.org] On Behalf Of Iavor Diatchki > Sent: 26 December 2012 02:48 > To: Conal Elliott > Cc: glasgow-haskell-bugs(a)haskell.org; GHC Users Mailing List > Subject: Re: Fundeps and type equality > > > > Hello Conal, > > > > GHC implementation of functional dependencies is incomplete: it will use functional dependencies during type inference (i.e., to determine the values of free type variables), but it will not use them in proofs, which is what is needed in examples like the one you posted. The reason some proving is needed is that the compiler needs to figure out that for each instantiation of the type `ta` and `tb` will be the same (which, of course, follows directly from the FD on the class). > > > > As far as I understand, the reason that GHC does not construct such proofs is that it can't express them in its internal proof language (System FC). It seems to me that it should be fairly straight-forward to extend FC to support this sort of proof, but I have not been able to convince folks that this is the case. I could elaborate, if there's interest. > > > > In the mean time, the way forward would probably be to express the dependency using type families, which I find tends to be more verbose but, at present, is better supported in GHC. > > > > Cheers, > > -Iavor > > PS: cc-ing the GHC users' list, as there was some talk of closing the ghc-bugs list, but I am not sure if the transition happened yet. > > > > > > > > > > On Tue, Dec 25, 2012 at 6:15 PM, Conal Elliott <conal(a)conal.net> wrote: > > I ran into a simple falure with functional dependencies (in GHC 7.4.1): > > > class Foo a ta | a -> ta > > > > foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool > > foo = (==) > > I expected that the `a -> ta` functional dependency would suffice to prove that `ta ~ tb`, but > > Pixie/Bug1.hs:9:7: > Could not deduce (ta ~ tb) > from the context (Foo a ta, Foo a tb, Eq ta) > bound by the type signature for > foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool > at Pixie/Bug1.hs:9:1-10 > `ta' is a rigid type variable bound by > the type signature for > foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool > at Pixie/Bug1.hs:9:1 > `tb' is a rigid type variable bound by > the type signature for > foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool > at Pixie/Bug1.hs:9:1 > Expected type: ta -> tb -> Bool > Actual type: ta -> ta -> Bool > In the expression: (==) > In an equation for `foo': foo = (==) > Failed, modules loaded: none. > > Any insights about what's going wrong here? > > -- Conal > > > _______________________________________________ > Glasgow-haskell-bugs mailing list > Glasgow-haskell-bugs(a)haskell.org > http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs > > > > > _______________________________________________ > Glasgow-haskell-users mailing list > Glasgow-haskell-users(a)haskell.org > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users > > > _______________________________________________ > Glasgow-haskell-users mailing list > Glasgow-haskell-users(a)haskell.org > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

1 0