September 2014 - ghc-tickets

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

09 Sep '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: | -------------------------------------+------------------------------------- Comment (by jstolarek): Richard, I don't understand your terminology here (though I do understand the `F` example): > The equations defining a head-injective function all have RHSs with different heads. What appears below the heads does not matter. Could you explain what you mean by `RHSs with different heads` and `below the heads`? Up till now I thought that the term "head" refers to `type family F a` part of the declaration. I also don't understand why `G` is not head-injective, but perhaps this will become clear to me once earlier questions are answered. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6018#comment:50> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

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

09 Sep '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: | -------------------------------------+------------------------------------- Comment (by jstolarek): I think the bulk of the work with injectivity will be done under the hood. Changing the syntax later on will not be difficult and I don't want to be blocked by bikeshedding. Inferring injectivity for closed type families is something that indeed requires more discussion. But again, I feel I can make at least some progress without any binding decissions on this matter being made. I don't like any of Richard's proposals: - if we introduced `Result` this would be the first capitalized keyword (reserved word?) in Haskell. I don't like such inconsistency. Notice also that `result` might conflict with type variable names in type family head but that is a local conflict that restricts only the names possible to use for type variables. On the other hand `Result` might conflict with a name of a type (or type family), which is more of a global thing. - if we use syntax that uses type family name then we will get something like `type family F a b c | F b -> a c` and `F b` looks strange given that `F`'s arity is 3. It looks as if `F` could be partially applied. I don't think that restricting the use of `result` word in type family head is a big problem - we've already done that with `role`. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6018#comment:49> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

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

09 Sep '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: | -------------------------------------+------------------------------------- Comment (by goldfire): A conversation with Ulf Norell (the first implementor of Agda) led to this interesting thought: We may not want injectivity -- we may want a weaker property, which I'll term "head-injectivity". The equations defining a head-injective function all have RHSs with different heads. What appears below the heads does not matter. Here is an example: {{{#!hs type family F a where F (Just x) = True F Nothing = False }}} This function is ''not'' injective: `F (Just 1) ~ F (Just 2)`. Yet, it is head-injective. If the type-inferencer knows that `F x ~ True`, it can then refine `x ~ Just y` for some fresh unification variable `y`. This improvement may be enough to make further progress. Of course, injectivity does not imply head-injectivity. Consider {{{#!hs type family G a where G True = Just 1 G False = Just 2 }}} This function is injective but not head-injective. So, implementing only head-injectivity will miss this case. But, perhaps we can refine the notion of head-injectivity simply to mean that the RHSs don't unify. The reason I'm bringing this up is that head-injectivity is, as I understand it, implemented in Agda and used during type inference. It intrigues me to think that we can make progress in the case of `F`, a non- injective function. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6018#comment:48> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

Re: [GHC] #6086: Cross compilation fails using system linker for other architecture binaries
by GHC 09 Sep '14

09 Sep '14

#6086: Cross compilation fails using system linker for other architecture binaries ----------------------------------------------+--------------------------- Reporter: mtjm | Owner: Type: bug | Status: new Priority: high | Milestone: 7.8.4 Component: Build System | Version: 7.8.3 Resolution: | Keywords: Operating System: Linux | Architecture: arm Type of failure: Building GHC failed | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: Differential Revisions: | ----------------------------------------------+--------------------------- Comment (by rwbarton): Try adding `--with-gcc=[whatever the path to the C cross-compiler is]` to the configure command line. I've found that I need to do this when cross- compiling. I think that configure detecting the C cross-compiler worked in 7.8.2 and broke in 7.8.3 but I'm not 100% sure. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6086#comment:8> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

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

09 Sep '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: | -------------------------------------+------------------------------------- Comment (by rwbarton): We could also reuse an existing keyword, e.g., `type family F a :: * | type -> a`. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6018#comment:47> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

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

09 Sep '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: | -------------------------------------+------------------------------------- Comment (by goldfire): That syntax precludes the possibility of `result` being the name of an argument to the function. Using `Result` avoids this problem, but that would be a capitalized keyword, which is strange. The other possibility that avoids stealing the name `result` is to use the type family itself to represent the result: `type family F a | F -> a`, but that's a little strange. I guess I favor the last syntax the most. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6018#comment:46> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

Re: [GHC] #6086: Cross compilation fails using system linker for other architecture binaries
by GHC 09 Sep '14

09 Sep '14

#6086: Cross compilation fails using system linker for other architecture binaries ----------------------------------------------+--------------------------- Reporter: mtjm | Owner: Type: bug | Status: new Priority: high | Milestone: 7.8.4 Component: Build System | Version: 7.8.3 Resolution: | Keywords: Operating System: Linux | Architecture: arm Type of failure: Building GHC failed | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: Differential Revisions: | ----------------------------------------------+--------------------------- Comment (by cetu86): I have to confirm having exactly the same problem. build command line is {{{ ./configure --target=arm-unknown-linux-gnueabi --enable-unregisterised --with-nm=/usr/bin/nm --prefix=$HOME/haskell/ghc-build && make quick- cross }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6086#comment:7> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

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

09 Sep '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: | -------------------------------------+------------------------------------- Comment (by simonpj): Before embarking on the implementation, is everyone convinced that the proposed syntax {{{ type family F a :: * | result -> a }}} is the best one? I understand the desire to support injectivity in some parameters but not others. For ''closed'' type classes, can't we infer injectivity, rather than having to declare it? (Although I suppose that the ability to declare is always a Good Thing.) Simon -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6018#comment:45> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

[GHC] #9558: "Illegal equational constraint" that might not be the users fault
by GHC 09 Sep '14

09 Sep '14

#9558: "Illegal equational constraint" that might not be the users fault -------------------------------------+------------------------------------- Reporter: rrnewton | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.9 Keywords: | Operating System: Architecture: Unknown/Multiple | Unknown/Multiple Difficulty: Unknown | Type of failure: Blocked By: | None/Unknown Related Tickets: | Test Case: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- If you try the latest cabal head and GHC together as of 2014.09.04, and then you try to install statistics, you'll see an error like the following, which does not occur in GHC 7.8.3: {{{ cabal-1.21 install -w ghc-7.9.20140904 Resolving dependencies... Configuring statistics-0.13.2.1... Building statistics-0.13.2.1... Preprocessing library statistics-0.13.2.1... [ 1 of 46] Compiling Statistics.Test.Internal ( Statistics/Test/Internal.hs, dist/build/Statistics/Test/Internal.o ) [ 2 of 46] Compiling Statistics.Test.Types ( Statistics/Test/Types.hs, dist/build/Statistics/Test/Types.o ) [ 3 of 46] Compiling Statistics.Internal ( Statistics/Internal.hs, dist/build/Statistics/Internal.o ) [ 4 of 46] Compiling Statistics.Transform ( Statistics/Transform.hs, dist/build/Statistics/Transform.o ) Statistics/Transform.hs:113:3: Illegal equational constraint Control.Monad.Primitive.PrimState m ~ s (Use GADTs or TypeFamilies to permit this) When checking that ‘bitReverse’ has the inferred type bitReverse :: forall (m :: * -> *) b. (Control.Monad.Primitive.PrimMonad m, Control.Monad.Primitive.PrimState m ~ s) => Int -> Int -> m b In an equation for ‘mfft’: }}} (Indeed, adding the GADTs language pragma makes the type checker happy, as in the commit here: https://github.com/rrnewton/criterion/commit/3a2487176e92b6972560ab1abdfa09… ) Hmm, well, the source code in this case did not explicitly add the "~ s" constraint, the inference cooked it up. Is this a GHC bug in 7.9 or in 7.8? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9558> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 3

Re: [GHC] #5395: Context reduction stack overflow without undecidable instances
by GHC 09 Sep '14

09 Sep '14

#5395: Context reduction stack overflow without undecidable instances -------------------------------------+------------------------------------- Reporter: guest | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.0.4 Resolution: | Keywords: type family, Operating System: | termination Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: GHC | Difficulty: Unknown rejects valid program | Blocked By: Test Case: | Related Tickets: Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by nomeata): > I suspect that when splitting the two we put the type-class one back to 20. Correct. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/5395#comment:9> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0