- ghc-tickets - Haskell.org

[GHC] #9670: Make Data.List.tails a good producer for list fusion
by GHC 16 Oct '14

16 Oct '14

#9670: Make Data.List.tails a good producer for list fusion -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: ekmett Type: task | Status: new Priority: normal | Milestone: 7.10.1 Component: Core Libraries | Version: 7.8.3 Keywords: fusion | Operating System: Architecture: Unknown/Multiple | Unknown/Multiple Difficulty: Unknown | Type of failure: Blocked By: | None/Unknown Related Tickets: | Test Case: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Its structure is trivially an unfold, so it should work well as a producer. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9670> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 3

Re: [GHC] #6018: Injective type families
by GHC 15 Oct '14

15 Oct '14

#6018: Injective type families -------------------------------------+------------------------------------- Reporter: lunaris | Owner: jstolarek Type: feature | Status: new request | Milestone: 7.10.1 Priority: normal | Version: 7.4.1 Component: Compiler | Keywords: TypeFamilies, Resolution: | Injective Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: #4259 Test Case: | Blocking: | Differential Revisions: Phab:D202 | -------------------------------------+------------------------------------- Comment (by jstolarek): Simon, I'm trying to understand your [comment:76 earlier comment]: > * We are not (at least for now) changing System FC. So the only effect of injectivity is to add extra "Derived" unification constraints, very much like functional dependencies. If we see > {{{ > [W] F t ~ F s > }}} > then we don't decopose it. Instead we add > {{{ > [D] t ~ s > }}} > That guides inference, but does not produce proof terms. So, no, nothing to do with `isDecomposableTyCon`. Much more like the `try_improvement` code in `TcInteract.doTopReactFunEq`. First of all, do we ever get a chance of actually seeing `F t ~ F s`? I think this is not canonical and if such constraint ever appears it would be turned into `F t ~ a, F s ~ a`. I'm not sure which of the canonicalization rules in Fig. 21 in OutsideIn paper would be responsible for that conversion because I don't know the meaning of these stylized D, F and T used in the mentioned figure. My guess would be FFLAT[W/G]R rules. Anyway, once we have `F t ~ a, F s ~ a` we could apply my suggested INJFEQFEQ interaction rule to generate `[D] s ~ t`. If my thinking here is right then shouldn't the implementation go into `TcInteract.interactFunEq` (guessing from its name)? I also wonder whether `[W]` is important in your `[W] F t ~ F s` example? I believe this rule is valid for both given and wanted constraints. I don't understand what you mean by "we don't decopose it". What is this "decomposition" that you mention? I believe that the only moment when injectivity interacts with top-level axioms is when we're deducing LHS from RHS. I suspect this might require a new reaction rule, separate from FINST. Are my ideas here correct? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6018#comment:90> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

Re: [GHC] #6018: Injective type families
by GHC 15 Oct '14

15 Oct '14

#6018: Injective type families -------------------------------------+------------------------------------- Reporter: lunaris | Owner: jstolarek Type: feature | Status: new request | Milestone: 7.10.1 Priority: normal | Version: 7.4.1 Component: Compiler | Keywords: TypeFamilies, Resolution: | Injective Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: #4259 Test Case: | Blocking: | Differential Revisions: Phab:D202 | -------------------------------------+------------------------------------- Comment (by jstolarek): I've read section 7.4 of OutsideIn(X) paper. Code makes more sense now but still I have some questions. Most importantly I'm trying to understand FINST top-level reaction rule (OutsideIn paper, fig. 24 page 65), which according to my understanding is implemented by `doTopReactFunEq`. Since I don't have LaTeX in the wiki I'll be using following notation: \Q - set of top-level axiom schemes \g - little gamma \d - little delta \th - little theta \t - little tau \e - little epsilon _0 - 0 in a subscript \vec{...} - a vector of values, in paper denoted using overline \in - set membership realtion Now the rule: {{{ forall \vec{a}. F \vec{Xi_0} ~ Xi_0 \in \Q -- (1) \vec{b} = ftv(\vec{Xi_0}) -- (2) \vec{c} = \vec{a} - \vec{b} -- (3) \g fresh -- (4) \th = [\vec{b |-> \t_a},\vec{c |-> \g}] -- (5) \th \vec{Xi_0} = \vec{Xi} -- (6) if (l = w) then \vec{\d} = \vec{\g} else \vec{\d} = \e -- (7) ------------------------------------------------------------- topreact[l](\Q, F \vec{Xi}~Xi) = {\d, \th Xi_0 ~ Xi} -- (8) }}} Here's how I understand (or misunderstand that rule): Premise (1) represents a type family equation written by the user (either from a closed or open type family). `\vec{Xi_0}` represents the LHS of `F` ie. patterns in that equation. So for example if the equation is `F [b] Bool c` then `\vec{Xi_0}` is `([b],Bool, c)`. I'm not sure about `[b]` - I think that's not canonical? Are axioms canonicalized? I'm also not sure about the meaning of `\vec{a}` in (1)'s forall. My intuition would be that these are type variables in the LHS (`b` and `c` in above example). But then I don't know how to understand premise (2). If `\vec{b}` represents free variables if `\vec{Xi_0}` then wouldn't this be identical to `\vec{a}`? This does not make sense because in that situation `\vec{c}` in premise (3) would always be empty. Premise (5) is a substitution used in premise (6) to turn the LHS of the original axiom into LHS of a constraint we are trying to solve. But what does `\t_a` represent? Instantiation of variables in the original axiom to some particular values present in `\vec{Xi}`? Premise (7) says that if a constraint is wanted then we introduce new variables. I'm not sure why. Maybe this will become clear once I understand the rest. I'm not sure if I understand the conclusion (8). Reading the rule I see that if we have `F \vec{Xi} ~ Xi` constraint we use it to figure out the `\th` substitution and then use that substitution to create a new constraint that tries to equate the RHS of our current constraint with the RHS of original axiom. But why do we want this? I could use an example with more comments than in the paper (and the example could be more complicated too). Before proceeding with the implementation I'd like to understand how injectivity affects FINST rule. What is not clear to me is whether the new constraint we are producing is wanted or given? My guess is that we produce a given if the original constraint was given and wanted if the original was wanted. I also wonder whether injectivity gives us a new interaction rule: {{{ INJFEQFEQ interact[l] (F \vec{Xi_1} ~ Xi, F \vec{Xi_2} ~ Xi) = (F \vec{Xi_1} ~ Xi, \vec{ Xi_1 ~ Xi_2 }) }}} where `\vec{ Xi_1 ~ Xi_2 }` represents vector of pairwise constraints. A few more questions unrelated to the paper: 1. Are axioms for associated types treated differently than for open type families? 2. What does `BuiltInSynFamTyCon` constructor represent? 3. `Note [Basic Simplifier Plan]` in `TcInteract` mentions "inert reactions" and "spontaneous reactions". What's the difference between the two? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6018#comment:89> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

Re: [GHC] #7828: RebindableSyntax and Arrow
by GHC 15 Oct '14

15 Oct '14

#7828: RebindableSyntax and Arrow -------------------------------------+------------------------------------- Reporter: | Owner: AlessandroVermeulen | Status: new Type: bug | Milestone: 7.10.1 Priority: normal | Version: 7.6.2 Component: Compiler | Keywords: (Type checker) | Architecture: Unknown/Multiple Resolution: | Difficulty: Unknown Operating System: | Blocked By: Unknown/Multiple | Related Tickets: #1537, #3613 Type of failure: GHC | rejects valid program | Test Case: | Blocking: | Differential Revisions: Phab:D72 | -------------------------------------+------------------------------------- Comment (by simonpj): See also [http://www.haskell.org/pipermail/glasgow-haskell- users/2014-October/025298.html this ghc-users thread]. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/7828#comment:51> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

Re: [GHC] #3242: ghci: can't load .so/.DLL for: m (addDLL: could not load DLL)
by GHC 15 Oct '14

15 Oct '14

#3242: ghci: can't load .so/.DLL for: m (addDLL: could not load DLL) ---------------------------------------+--------------------------- Reporter: jeffz1 | Owner: Type: bug | Status: new Priority: normal | Milestone: 7.10.1 Component: GHCi | Version: 7.4.1 Resolution: | Keywords: Operating System: Windows | Architecture: x86 Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: 3658 Blocking: | Related Tickets: #7097 Differential Revisions: | ---------------------------------------+--------------------------- Comment (by dreixel): I hit this problem too with `criterion` on Windows. `criterion` depends on `hastache`, which depends on `ieee754` without any version bounds. `ieee754-0.7.4` is good, `ieee754-0.7.3` isn't. So I fixed it with the following sequence of commands: {{{ ghc-pkg unregister criterion-1.0.1.0 ghc-pkg unregister hastache-0.6.0 ghc-pkg unregister ieee754-0.7.3 cabal install criterion --constraint="ieee754-0.7.4" }}} Hopefully others can do something similar to this. Also, package authors should update their packages to require `ieee754 >= 0.7.4`. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/3242#comment:31> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

Re: [GHC] #7495: generalizing overloaded list syntax to Sized Lists, HLists, HRecords, etc (was: Rebindable list syntax?)
by GHC 15 Oct '14

15 Oct '14

#7495: generalizing overloaded list syntax to Sized Lists, HLists, HRecords, etc -------------------------------------+------------------------------------- Reporter: nwf | Owner: carter Type: feature | Status: new request | Milestone: 7.10.1 Priority: normal | Version: 7.6.1 Component: Compiler | Keywords: Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: | Related Tickets: None/Unknown | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Changes (by carter): * owner: => carter Comment: I've been working on designing a set of classes that subsumes this proposal. the work in progress in the class design can be found https://github.com/cartazio/HetList/blob/master/HetList.hs It doesn't yet have the analogues machinery to support the older `fromList` style instances, but thats easy to add. As part of the dev I'm making sure I can write useful instances for the fancy HList libs that are in the while, like `HList` and `Vinyl` after another week or two of polish, I hope to have a candidate patch with the right desugaring (plus some extra work to support current style instances if possible) -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/7495#comment:7> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

Re: [GHC] #6018: Injective type families
by GHC 14 Oct '14

14 Oct '14

#6018: Injective type families -------------------------------------+------------------------------------- Reporter: lunaris | Owner: jstolarek Type: feature | Status: new request | Milestone: 7.10.1 Priority: normal | Version: 7.4.1 Component: Compiler | Keywords: TypeFamilies, Resolution: | Injective Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: #4259 Test Case: | Blocking: | Differential Revisions: Phab:D202 | -------------------------------------+------------------------------------- Comment (by jstolarek): > I don't know how to do this either. Luckily, we can reject E2 on a first pass. Yes, I believe that's what we should do. If we ever have analysis of unreachable equations for type families then we can use it to deal with `E2` but until then we should simply reject it. As for answers to 1-5 I'll read some more and get back if that doesn't help. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6018#comment:88> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

Re: [GHC] #6018: Injective type families
by GHC 14 Oct '14

14 Oct '14

#6018: Injective type families -------------------------------------+------------------------------------- Reporter: lunaris | Owner: jstolarek Type: feature | Status: new request | Milestone: 7.10.1 Priority: normal | Version: 7.4.1 Component: Compiler | Keywords: TypeFamilies, Resolution: | Injective Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: #4259 Test Case: | Blocking: | Differential Revisions: Phab:D202 | -------------------------------------+------------------------------------- Comment (by goldfire): Replying to [comment:86 jstolarek]: > I don't yet see how to deal with your `E2` example. It looks like we would need to have pattern-exhaustiveness checking for type families. And this would only be possible for closed kinds I think. Well, for open kinds type family would simply be non-injective. I don't know how to do this either. Luckily, we can reject `E2` on a first pass. It's possible that the only examples like this are silly in the same way that `E2` is silly, in that the last equation is utterly unreachable. > > I have a few more questions about implementation. These most likely go to Simon. I've been trying to wrap my head around implementation of `doTopReactFunEq` and I have these questions: > > 1. What does the term "react" mean? As in the name `doTopReact` and the comment below its type signature: "The work item does not react with the inert set..." (TcInteract, L1412). > > 2. What is "interaction"? As in the module name `TcInteract` or the comment mentioned above: "... so try interaction with top-level instances". Simon may be able to answer better than I, but I believe these refer to the actions taken in section 7 of the !OutsideIn paper. > > 3. What does `EvTerm` data type represent? These are values of constraint types, including class dictionaries, type equalities, and implicit parameters. `EvTerm`s are desugared in !DsBinds. Write back if that's not enough of an explanation. > > 4. What are branches in axioms? A closed type family with multiple equations leads to a so-called branched axiom. The way overlap works in a closed type family means that we can't have separate axioms for each equation. So, a branched axiom contains potentially many branches; each branch asserts an equality, but later branches can be used only when no previous branch supersedes. Does that help? It's all in the closed type families paper. > > 5. I don't understand how canonicalization works. Is there an overview somewhere? Other than `Note [Canonicalization]`, which unfortunately is too vague for me :-( I think this is also in !OutsideIn. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6018#comment:87> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

Re: [GHC] #6018: Injective type families
by GHC 14 Oct '14

14 Oct '14

#6018: Injective type families -------------------------------------+------------------------------------- Reporter: lunaris | Owner: jstolarek Type: feature | Status: new request | Milestone: 7.10.1 Priority: normal | Version: 7.4.1 Component: Compiler | Keywords: TypeFamilies, Resolution: | Injective Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: #4259 Test Case: | Blocking: | Differential Revisions: Phab:D202 | -------------------------------------+------------------------------------- Comment (by jstolarek): > Does that clarify? Yes. I don't yet see how to deal with your `E2` example. It looks like we would need to have pattern-exhaustiveness checking for type families. And this would only be possible for closed kinds I think. Well, for open kinds type family would simply be non-injective. I have a few more questions about implementation. These most likely go to Simon. I've been trying to wrap my head around implementation of `doTopReactFunEq` and I have these questions: 1. What does the term "react" mean? As in the name `doTopReact` and the comment below its type signature: "The work item does not react with the inert set..." (TcInteract, L1412). 2. What is "interaction"? As in the module name `TcInteract` or the comment mentioned above: "... so try interaction with top-level instances". 3. What does `EvTerm` data type represent? 4. What are branches in axioms? 5. I don't understand how canonicalization works. Is there an overview somewhere? Other than `Note [Canonicalization]`, which unfortunately is too vague for me :-( -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6018#comment:86> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

Re: [GHC] #6018: Injective type families
by GHC 14 Oct '14

14 Oct '14

#6018: Injective type families -------------------------------------+------------------------------------- Reporter: lunaris | Owner: jstolarek Type: feature | Status: new request | Milestone: 7.10.1 Priority: normal | Version: 7.4.1 Component: Compiler | Keywords: TypeFamilies, Resolution: | Injective Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: #4259 Test Case: | Blocking: | Differential Revisions: Phab:D202 | -------------------------------------+------------------------------------- Comment (by goldfire): Replying to [comment:84 jstolarek]: > Richard, either I'm not getting the subtleties of your arguments or you're misunderstanding what I meant to say on the wiki page. Or both :-) > > I now see the theoretical difference between "overlaps" and "subsumes" but I don't yet see how that is important in my algorithm outline. I re- read parts of the closed type families paper and now I'm not even sure whether I meant "overlaps" or "unifies". To be clear, I am considering the expressions "two types overlap" and "two types unify" to be synonymous. Subsumption is a finer, directed relation between types than overlap/unify. > {{{#!hs > type family E1 a = r | r -> a where ... > }}} Yes yes yes. You're right here. I was wrong. The wiki page is updated. > > Now `E2`: > > {{{#!hs > type family E2 (a:: Bool) = r | r -> a where > E2 False = True > E2 True = False > E2 a = False > }}} > I consider almost identical example on the wiki: > {{{#!hs > type family Bak a = r | r -> a where > Bak Int = Char > Bak Char = Int > Bak a = a > }}} > The difference is the RHS of the last equation: a concrete type in your example, a type variable in mine. Yet I believe that both examples are intended to demonstrate the same problem - see discussion below that example. I think these cases are different. In yours, the RHS unification (`a` unifies with `Char`) refines the LHS (`a |-> Char`) so that it is subsumed by an earlier equation. This action does not happen in my example, and different reasoning (noting that `False` and `True` are both impossible) is required. > I have a question about closed type families paper. Paragraph just after Candidate Rule 2 (section 3.2, page 3) says: "As a notational convention, apart(ρ, τ) considers the lists ρ and τ as tuples of types; the apartness check does ''not'' go element-by-element.", where "not" is emphasized. Why is this important? Seems like the choice of representing patterns and types as tuples or lists is just an implementation detail. Agreed that choosing a list vs. a tuple is irrelevant, but choosing element-by-element vs. as-a-whole is quite important. For example `(a, a)` is quite apart from `(Int, Bool)`, when considered as a whole, even though `a` is neither apart from `Int` nor `Bool` looking at individual elements. Does that clarify? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6018#comment:85> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0