- ghc-tickets - Haskell.org

[GHC] #10325: Clearify status of ImpredicativeTypes Extension
by GHC 22 Apr '15

22 Apr '15

#10325: Clearify status of ImpredicativeTypes Extension -------------------------------------+------------------------------------- Reporter: | Owner: j80JjBjVNRMajmA | Status: new Type: bug | Milestone: Priority: normal | Version: 7.10.1 Component: | Operating System: Unknown/Multiple Documentation | Type of failure: None/Unknown Keywords: | Blocked By: Architecture: | Related Tickets: Unknown/Multiple | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- There seem to be many statements about this extension and its problems floating around in the internet. But a user of GHC will first fall into a possibly large number of traps and problems before he finds them. I think it would help, if the GHC manual [https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/other- type-extensions.html#impredicative-polymorphism] and the compiler warned about this extension (instead of suggesting it!). -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/10325> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 3

[GHC] #10281: Type error with Rank-n-types
by GHC 22 Apr '15

22 Apr '15

#10281: Type error with Rank-n-types -------------------------------------+------------------------------------- Reporter: rhjl | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.4 (Type checker) | Operating System: Unknown/Multiple Keywords: | Type of failure: GHC rejects Architecture: | valid program Unknown/Multiple | Blocked By: Test Case: | Related Tickets: Peirce_eq_LEM.hs | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- GHC rejects the following program (which is also attached); it accepts it if the product type is replaced by tuples and the ImpredicativeTypes option is added. I am not sure if this is a bug or an expected consequence of the typing rules, which I do not know very well. In the latter case a better error message would be helpful. The error message is: {{{ 54:17: Couldn't match type ‘(Not 𝑎0 -> 𝑐0) -> (𝑎0 -> 𝑐0) -> 𝑐0’ with ‘LEM’ Expected type: (((Peirce -> LEM) -> 𝑐) ⨿ ((LEM -> Peirce) -> 𝑐)) -> 𝑐 Actual type: (((Peirce -> (Not 𝑎0 -> 𝑐0) -> (𝑎0 -> 𝑐0) -> 𝑐0) -> 𝑐) ⨿ ((LEM -> ((𝑎1 -> 𝑏0) -> 𝑎1) -> 𝑎1) -> 𝑐)) -> 𝑐 In the expression: peirce_implies_lem `and` lem_implies_peirce In an equation for ‘peirce_eq_lem’: peirce_eq_lem = peirce_implies_lem `and` lem_implies_peirce }}} This is the code: {{{#!hs {-# LANGUAGE NoImplicitPrelude #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UnicodeSyntax #-} -- truth type True = ∀ 𝑎. 𝑎 → 𝑎 type False = ∀ 𝑎. 𝑎 id ∷ True id 𝑥 = 𝑥 (∘) ∷ ∀ 𝑎 𝑏 𝑐. (𝑏 → 𝑐) → (𝑎 → 𝑏) → 𝑎 → 𝑐 𝑓 ∘ 𝑔 = \𝑥 → 𝑓 (𝑔 𝑥) -- negation type Not 𝑎 = 𝑎 → False -- disjunction / coproduct type 𝑎 ⨿ 𝑏 = ∀ 𝑐. (𝑎 → 𝑐) → (𝑏 → 𝑐) → 𝑐 𝜄₀ ∷ ∀ 𝑎 𝑏. 𝑎 → 𝑎 ⨿ 𝑏 𝜄₀ 𝑥 = \𝑙 _ → 𝑙 𝑥 𝜄₁ ∷ ∀ 𝑎 𝑏. 𝑏 → 𝑎 ⨿ 𝑏 𝜄₁ 𝑥 = \_ 𝑟 → 𝑟 𝑥 -- conjunction / product type 𝑎 × 𝑏 = ∀ 𝑐. (𝑎 → 𝑐) ⨿ (𝑏 → 𝑐) → 𝑐 𝜋₀ ∷ ∀ 𝑎 𝑏. 𝑎 × 𝑏 → 𝑎 𝜋₀ 𝑝 = 𝑝 (𝜄₀ id) 𝜋₁ ∷ ∀ 𝑎 𝑏. 𝑎 × 𝑏 → 𝑏 𝜋₁ 𝑝 = 𝑝 (𝜄₁ id) and ∷ ∀ 𝑎 𝑏. 𝑎 → 𝑏 → 𝑎 × 𝑏 𝑥 `and` 𝑦 = \𝑐 → 𝑐 (\𝑙 → 𝑙 𝑥) (\𝑟 → 𝑟 𝑦) -- equivalence type 𝑎 ↔ 𝑏 = (𝑎 → 𝑏) × (𝑏 → 𝑎) -- peirce ↔ lem type Peirce = ∀ 𝑎 𝑏. ((𝑎 → 𝑏) → 𝑎) → 𝑎 type LEM = ∀ 𝑎. (Not 𝑎) ⨿ 𝑎 peirce_eq_lem ∷ Peirce ↔ LEM peirce_eq_lem = peirce_implies_lem `and` lem_implies_peirce peirce_implies_lem ∷ Peirce → LEM peirce_implies_lem peirce = peirce (\𝑘 → 𝜄₀ (𝑘 ∘ 𝜄₁)) lem_implies_peirce ∷ LEM → Peirce lem_implies_peirce lem = \𝑓 → lem (\𝑥 → 𝑓 𝑥) id }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/10281> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 10

[GHC] #10182: lookupIfaceGlobal crash with SOURCE import
by GHC 22 Apr '15

22 Apr '15

#10182: lookupIfaceGlobal crash with SOURCE import -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: 7.12.1 Component: Compiler | Version: 7.8.4 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Blocked By: Test Case: | Related Tickets: Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Try this (in `testsuite/tests/stranal/should_compile`) {{{ bash$ ghc -c T8743.hs-boot bash$ ghc -c T8743.hs ghc: panic! (the 'impossible' happened) (GHC version 7.8.2 for x86_64-unknown-linux): tcIfaceGlobal (local): not found: main:T8743.$fxToRowMaybe{v r2J} [(r2L, Class ‘main:T8743.ToRow{tc r2L}’), (r2M, Data constructor ‘main:T8743.D:ToRow{d r2M}’), (r2P, Identifier ‘main:T8743.D:ToRow{v r2P}’), (roB, Identifier ‘main:T8743.toRow{v roB}’), (rqT, Coercion axiom ‘main:T8743.NTCo:ToRow{tc rqT}’)] }}} Something clearly wrong here. It think this happens with prettty much any version of GHC. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/10182> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 14

[GHC] #10341: hs-boot files can have bogus declarations if they're not exported
by GHC 22 Apr '15

22 Apr '15

#10341: hs-boot files can have bogus declarations if they're not exported -------------------------------------+------------------------------------- Reporter: ezyang | Owner: Type: bug | Status: new Priority: low | Milestone: Component: Compiler | Version: 7.11 (Type checker) | Operating System: Unknown/Multiple Keywords: | Type of failure: GHC accepts Architecture: | invalid program Unknown/Multiple | Blocked By: Test Case: | Related Tickets: Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Consider: {{{ -- A.hs-boot module A(foo) where data A = AC { bar :: Int } | CC -- B.hs module B where import {-# SOURCE #-} A -- A.hs module A(foo) where import B data A = AC { foo :: Int } | BC }}} GHC won't complain that `A` is incompatibly defined, since it's not exported. Seems relatively harmless though. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/10341> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 1

[GHC] #8743: The impossible happened : Prelude.(!!): index too large
by GHC 22 Apr '15

22 Apr '15

#8743: The impossible happened : Prelude.(!!): index too large ----------------------------------+--------------------------------------- Reporter: erikd | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.1-rc1 Keywords: | Operating System: Unknown/Multiple Architecture: x86_64 (amd64) | Type of failure: Compile-time crash Difficulty: Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | ----------------------------------+--------------------------------------- Running ghc git HEAD (reports it's version as 7.9.20140206) and when cabal installing postgresql-simple I get: {{{ ghc: panic! (the 'impossible' happened) (GHC version 7.9.20140206 for x86_64-unknown-linux): Prelude.(!!): index too large Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug cabal: Error: some packages failed to install: postgresql-simple-0.4.0.2 failed during the building phase. The exception was: }}} postgresql-simple-0.4.0.2 installs fine with 7.6.3. I'm going to compile 7.8-rc1 and see if the same problem exists there. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8743> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 15

Re: [GHC] #3919: Or-patterns as GHC extension
by GHC 22 Apr '15

22 Apr '15

#3919: Or-patterns as GHC extension -------------------------------------+------------------------------------- Reporter: BjornEdstrom | Owner: Type: feature request | Status: new Priority: normal | Milestone: ⊥ Component: Compiler | Version: Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by sergv): * cc: sergv (added) -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/3919#comment:8> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

Re: [GHC] #7672: boot file entities are sometimes invisible and are not (semantically) unified with corresponding entities in implementing module
by GHC 21 Apr '15

21 Apr '15

#7672: boot file entities are sometimes invisible and are not (semantically) unified with corresponding entities in implementing module -------------------------------------+------------------------------------- Reporter: skilpat | Owner: ezyang Type: bug | Status: new Priority: normal | Milestone: 7.12.1 Component: Compiler (Type | Version: 7.4.2 checker) | Keywords: backpack Resolution: | Architecture: x86_64 Operating System: Linux | (amd64) Type of failure: GHC rejects | Test Case: valid program | Blocking: Blocked By: | Differential Revisions: Related Tickets: | -------------------------------------+------------------------------------- Changes (by simonpj): * owner: => ezyang Comment: I agree. Just remove it and see. It looks outright wrong to me. Simon -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/7672#comment:9> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

Re: [GHC] #7672: boot file entities are sometimes invisible and are not (semantically) unified with corresponding entities in implementing module
by GHC 21 Apr '15

21 Apr '15

#7672: boot file entities are sometimes invisible and are not (semantically) unified with corresponding entities in implementing module -------------------------------------+------------------------------------- Reporter: skilpat | Owner: Type: bug | Status: new Priority: normal | Milestone: 7.12.1 Component: Compiler (Type | Version: 7.4.2 checker) | Keywords: backpack Resolution: | Architecture: x86_64 Operating System: Linux | (amd64) Type of failure: GHC rejects | Test Case: valid program | Blocking: Blocked By: | Differential Revisions: Related Tickets: | -------------------------------------+------------------------------------- Comment (by ezyang): The reason this occurs is when we process imports in `rnImportDecl`, we filter out any identifiers which come from a self-boot: {{{ let gbl_env = mkGlobalRdrEnv (filterOut from_this_mod gres) }}} So these identifiers never get added to the GlobalRdrEnv, and thus aren't brought into scope. I don't know what happens if you remove that `filterOut`. It comes from some very old code. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/7672#comment:8> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

[GHC] #10331: Accept HsSyn in splices and generate it in quotes (ghc-api)
by GHC 21 Apr '15

21 Apr '15

#10331: Accept HsSyn in splices and generate it in quotes (ghc-api) -------------------------------------+------------------------------------- Reporter: ezyang | Owner: Type: feature | Status: new request | Milestone: Priority: low | Version: 7.11 Component: Template | Operating System: Unknown/Multiple Haskell | Type of failure: None/Unknown Keywords: | Blocked By: Architecture: | Related Tickets: Unknown/Multiple | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- I propose a language pragma `GhcTemplateHaskell`, which, when enabled, causes Template Haskell splices to accept `HsSyn` return values, and causes TH quotes to return `HsSyn` trees. Users of `GhcTemplateHaskell` would stop using the `template-haskell` library and just directly manipulate the frontend ASTs using the `ghc-api`. Given our ghc-api track record, you would probably not be able to write code using this without having it break every GHC release. However, clients who are willing to track GHC development would reap the following benefits: 1. All syntax in Haskell would be supported in quotes; the AST would never lag behind. Additionally, you could use the ghc-api parser to parse Haskell code to be returned in a splice. (#2041) 2. Locations from quoting would be preserved. (Problem 2 of #10330) I don't think this would be difficult to implement, but it definitely could be a ball of wax. I broke this proposal off from #2041. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/10331> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 3

[GHC] #10327: Devise workaround for how infinite types prevent closed type family reduction
by GHC 21 Apr '15

21 Apr '15

#10327: Devise workaround for how infinite types prevent closed type family reduction -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: feature | Status: new request | Milestone: Priority: normal | Version: 7.10.1 Component: Compiler | Operating System: Unknown/Multiple Keywords: | Type of failure: None/Unknown Architecture: | Blocked By: Unknown/Multiple | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Suppose we have {{{ data a :+: b type family Inj x y where Inj a a = True Inj b (b :+: c) = False }}} When we try to reduce `Inj f (f :+: g)`, it looks like we should just use the second equation. Instead, we fail to reduce. This is because GHC is worried about the possibility of the first equation firing, in the event that `f ~ (f :+: g)`. This fact can happen only if `f` is infinitely large. On the surface, this seems impossible, but shenanigans in this area can cause `unsafeCoerce`. See #8162. I don't see an easy way to fix this, but the fact that GHC can't cope (well) with this example tells me something is wrong. Here is one idea of how to proceed: If we somehow ensure at reduction time that `f` is finite, we're OK. If we need finiteness in terms, we use `deepseq`. Can we do this in types? I tentatively say "yes". Imagine the following type family: {{{ type family Seq (x :: a) (y :: b) :: b type instance Seq True y = y type instance Seq False y = y }}} To reduce, say, {{{b `Seq` 5}}}, we'd need to know concretely what `b` is. We can then build `Deepseq` similarly to how `deepseq` at the term level works. The closed type family mechanism could then detect cases like `Inj`, where the whole infinite-type thing is causing trouble. (I conjecture that detecting this is not hard, as there's a specific line in the `Unify` module that triggers in the worry-about-infinite-types case.) In the case of `Inj`, something like `Inj f (f :+: g)` would reduce to {{{f `Deepseq` False}}}. Note that the call to `Seq` wouldn't be written in the closed type family definition, but would be inserted during reduction as appropriate. This solution is ugly. And it requires magic to define `Seq` in types (we need an instance for every type!) and weird magic in closed type family reduction. The definition of `Deepseq` might also benefit from being magical. It would be annoying to explain to users, but no more so than the current crazy story. In general, I don't like this idea much, but I do think it would work. In any case, this ticket is mainly to serve as a placeholder for any future thoughts in this direction. It's quite annoying to have the specter of infinite types cripple otherwise-sensible closed type families. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/10327> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 3