October 2014 - ghc-tickets

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

Re: [GHC] #5462: Deriving clause for arbitrary classes
by GHC 14 Oct '14

14 Oct '14

#5462: Deriving clause for arbitrary classes -------------------------------------+------------------------------------- Reporter: simonpj | Owner: dreixel Type: feature | Status: new request | Milestone: 7.10.1 Priority: normal | Version: 7.2.1 Component: Compiler | Keywords: Generics Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: | Related Tickets: #7346 None/Unknown | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by dreixel): No, not yet, I'm afraid. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/5462#comment:38> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

Re: [GHC] #5462: Deriving clause for arbitrary classes
by GHC 14 Oct '14

14 Oct '14

#5462: Deriving clause for arbitrary classes -------------------------------------+------------------------------------- Reporter: simonpj | Owner: dreixel Type: feature | Status: new request | Milestone: 7.10.1 Priority: normal | Version: 7.2.1 Component: Compiler | Keywords: Generics Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: | Related Tickets: #7346 None/Unknown | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by hvr): @dreixel, is your code ready for code revision via as a Phab:differential ? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/5462#comment:37> 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): 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". Anyway, I believe that my thinking is correct and in my algorithm I have addressed problems that you raised. It looks that I need help with sorting out the terminology so things are clear. Now, looking at your examples: {{{#!hs type family E1 a = r | r -> a where E1 Int = Int -- 1 E1 a = a -- 2 }}} When my algorithm reaches (2) it will attempt to unify `a` with RHS of equation (1). It will succeed with substitution `[ a -> Int ]`. It will apply that substitution to the LHS of (2) and proceed with checking whether after substitution this equation is subsumed (?) by any of the earlier ones. Clearly, it is by the first equation and since this is the last equation we declare `E1` to be injective. In other words I know that (2) will never produce an `Int` since this will equation will never be reached for `a` equal to `Int`. 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. > In `IdNat` and `NatToMaybe`, unification fails before seeing the recursive use of the type family. Right. I assumed that noticing that allows us to conlcude that equations of `IdNat` and `NatToMaybe` produce distinct types and thus these type families are injective. Your reasoning in that whole paragraph completely agrees with mine. > But I'd want a proof first. Agreed. As I said, I've been unable to produce a counter-example but that doesn't meant that one does not exist. 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. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6018#comment:84> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

[GHC] #9690: in GHCi map `:editNNN` to $EDITOR +NNN
by GHC 14 Oct '14

14 Oct '14

#9690: in GHCi map `:editNNN` to $EDITOR +NNN -------------------------------------+------------------------------------- Reporter: heisenbug | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: GHCi | Version: 7.8.3 Keywords: | Operating System: Architecture: Unknown/Multiple | Unknown/Multiple Difficulty: Unknown | Type of failure: Blocked By: | None/Unknown Related Tickets: | Test Case: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- I suggest to treat GHCi REPL commands `:editNNN` (as well as equivalent abbreviations, like `:eNNN` ) where `NNN` is a natural number, as invocations of the text editor with a `+NNN` option. Rationale: When I see a type error in line 42 then I'd like to visit this line directly with `:e42`. Optionally one could implement `:eNNN:CCC` to also target the column `CCC` in that line. `emacs`, `vi` and `pico` all implement the option `+NNN` to land in the line `NNN`. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9690> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 1

Re: [GHC] #7942: aarch64 support in ghc
by GHC 14 Oct '14

14 Oct '14

#7942: aarch64 support in ghc -------------------------------------+------------------------------------- Reporter: jcapik | Owner: Type: feature | Status: closed request | Milestone: 7.10.1 Priority: normal | Version: Component: Compiler | Keywords: Resolution: fixed | Architecture: arm Operating System: Linux | Difficulty: Unknown Type of failure: GHC | Blocked By: doesn't work at all | Related Tickets: 7623, 8664 Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by lukexi): I sent a mail out to the list a bit ago but should have added a comment here: I've completed the work to add the GHC ARM64 calling convention to LLVM [1], and finished up the support in GHC itself [2]. I'm in the process of tidying up the patches for submission. I'm going to try to backport them to 7.8 as well. [1] https://github.com/lukexi/llvm [2] https://github.com/lukexi/ghc -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/7942#comment:46> 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:82 jstolarek]: > Right. Still, I wondering how this works. I mean there are probably no special cases in the typechecker that try to guess whether a type family is an identity function? Of course, you're right -- GHC doesn't have a special case there. What it does do is so-called ''compatibility'' checking. Two equations of a type family (open or closed) are ''compatible'' if, whenever the LHSs unify with substitution ''s'', applying ''s'' to the RHSs makes them the same. Two equations for an open type family do not have a malignant overlap if they are compatible. And, more relevant here, GHC does the apartness check in closed type families only among incompatible equations. In `F` as originally given, all the equations are compatible with one another, and so GHC always skips the apartness check. Thus, when it sees `F a`, the last equation triggers and reduces `F a` to `a`. This is all described in the closed type families paper, and in the manual. > > We have to be careful with the word overlap here. I think we want "overlaps" to be "is subsumed by". > > I don't see the difference between "overlaps" and "is subsumed by". :-( I would say these equations overlap: > type instance G a Int = a > type instance G Int a = a but neither equation subsumes the other. On the other hand, > type instance H a a = a -- 1 > type instance H Int Int = Int -- 2 equation 1 subsumes equation 2, because anything that matches 2 will also surely match 1. > > Now, in 4c I wrote: > > > if unification [of the RHSs] succeeds and there are type variables involved we substitute unified type variables on the LHS and check whether this LHS overlaps with any of the previous equations. If it does we proceed to the next equation > > You replied with this: > > > you want to know of the equation at hand is reachable, given the LHS substitution. Even if it is reachable, the (substituted) LHS may coincide with the LHS of the earlier equation whose RHS unified with the current RHS. > > I don't see the difference between your version and mine. See new example `E1` on the wiki page. > > > Even subtler, it's possible that certain values for type variables are excluded if the current LHS is reachable (for example, some variable a couldn't be Int, because if a were Int, then a previous equation would have triggered). Perhaps these exclusions can also be taken into account. > > Hm... can you give an example where this would be useful? See new example `E2` on the wiki page. > > > '''RAE:''' But it seems that, under this treatment, any self-recursion would automatically lead to a conclusion of "not injective", just like any other use of a type family. For example: > > > > {{{#!hs > > type family IdNat n where > > IdNat Z = Z > > IdNat (S n) = S (IdNat n) > > }}} > > > > `IdNat` is injective. But, following the algorithm above, GHC would see the recursive use of `IdNat`, not know whether `IdNat` is injective, and then give up, concluding "not injective". Is there a case where the special treatment of self-recursion leads to a conclusion of "injective"? '''End RAE''' > > This example is just like my `NatToMaybe`. My idea here was that RHSs of these two equations won't unify - first returns `Z`, second returns `S something`. These are distinct constructors that have no chance of being unified. (I assumed that we are able to detect that.) There are no calls to type families other than self-recursion and so we can declare `IdNat` to be injective. I admit I am not 100% certain that allowing self- recursion is safe. It's just that I was unable to come up with an example that would show that my algorithm: a:) declares injective function to be non-injective; b) declares a non-injective function to be injective. > What are the steps your algorithm is taking? I don't see how `IdNat` can be considered injective while `Ban` is considered non-injective. A critical step in banning `Ban` is noting that we don't yet know that `Ban` is injective when checking it, so we conclude "not injective". Maybe it's because `Ban`'s recursion is at the top-level? In `IdNat` and `NatToMaybe`, unification fails before seeing the recursive use of the type family. Hmm... maybe. There seems to be something going on here that, if unification succeeds up until it sees the recursive use of the type family, then the family either must be non-injective or non-terminating... because this situation can only arise when the function "collapses" two inputs into the same output through recursion. But I'd want a proof first. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6018#comment:83> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

Re: [GHC] #1476: Template Haskell: splicing types and patterns
by GHC 14 Oct '14

14 Oct '14

#1476: Template Haskell: splicing types and patterns -------------------------------------+------------------------------------- Reporter: igloo | Owner: Type: bug | Status: new Priority: low | Milestone: ⊥ Component: Template | Version: 6.6.1 Haskell | 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 liyang): * cc: ghc.haskell.org@… (added) -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/1476#comment:11> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0