[GHC] #12432: TypeInType: open type family application as type family return kind fails to compile
#12432: TypeInType: open type family application as type family return kind fails to compile -------------------------------------+------------------------------------- Reporter: j6carey | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 (Type checker) | Keywords: | Operating System: Linux Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- With TypeInType enabled, I can use a closed type family to compute the return kind of a type family from its arguments. But an equivalent open type family used in the same way triggers a compilation failure, as if the relevant instance of that open type family were not considered. (Of course, there may be some subtle prohibition of which I am not aware at the present time.) I will attach a test case. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12432 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12432: TypeInType: open type family application as type family return kind fails to compile -------------------------------------+------------------------------------- Reporter: j6carey | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: Operating System: Linux | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by j6carey): * Attachment "test.hs" added. Test case that does not compile with GHC 8.0.1 due to use of an open type family to supply the return kind of another type family -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12432 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12432: TypeInType: open type family application as type family return kind fails to compile -------------------------------------+------------------------------------- Reporter: j6carey | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: duplicate | Keywords: Operating System: Linux | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * status: new => closed * resolution: => duplicate Comment: This is due to the fact that GHC processes instances after other type declarations. Fixed in HEAD by @alexvieth. Workaround: use multiple modules or use an empty top-level declaration splice `$(return [])` to force GHC to compile the instances earlier. Thanks for reporting! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12432#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12432: TypeInType: open type family application as type family return kind fails to compile -------------------------------------+------------------------------------- Reporter: j6carey | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: duplicate | Keywords: Operating System: Linux | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by j6carey): Thanks! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12432#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12432: TypeInType: open type family application as type family return kind fails to compile -------------------------------------+------------------------------------- Reporter: j6carey | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: duplicate | Keywords: Operating System: Linux | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by j6carey): * Attachment "Test3.hs" added. One more thing: does the same fix help with class instance contexts as well? Please see the new attachment Test3.hs. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12432 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12432: TypeInType: open type family application as type family return kind fails to compile -------------------------------------+------------------------------------- Reporter: j6carey | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: duplicate | Keywords: Operating System: Linux | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): That last test case is an unrelated issue, not yet fixed. The problem is that `-XTypeInType` can't use a kind equality "right away". Equality constraints in Haskell are ''lifted'', meaning that we must make sure they are not bottom before using them to cast anything. Normally, this is all optimized away. But it does mean that we can't immediately use a kind equality in a type unless there is a place to put a check for bottom. Your code has no such place. This is all a bit of a dark corner, and I'm afraid you shouldn't hold your breath for a solution. On the flip side, it would be very enlightening if you have a realistic scenario where this limitation bites. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12432#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12432: TypeInType: open type family application as type family return kind fails to compile -------------------------------------+------------------------------------- Reporter: j6carey | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: duplicate | Keywords: Operating System: Linux | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by j6carey): * Attachment "Test4.hs" added. An application of an associated type family with the kind problem mentioned. Also includes a workaround. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12432 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12432: TypeInType: open type family application as type family return kind fails to compile -------------------------------------+------------------------------------- Reporter: j6carey | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: duplicate | Keywords: Operating System: Linux | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by j6carey): Because of a workaround (as mentioned below), I don't have a compelling use case at present. The application I had in mind is illustrated by the recently-added attachment, "Test4.hs". The idea is that you have types that express formulas for values, and these can be evaluated in the context of various run-time parameters, though for brevity I have omitted the type expressions whose values actually depend on run-time parameters. Because some of these expressions will determine the sizes of certain objects in memory, I would like optimize length checks by computing static bounds on the range of sizes that a given type expression might specify. In particular, the expression might be a constant of kind "Nat". The associated type family exhibiting the problem is the one that computes the static bounds for the values associated with type expressions. The straightforward instance definition for constants of kind 'Nat' triggers the problem. On the other hand, I have managed to work around the issue by using a helper type family; please see the comment about 'EvalSingleton'. (Minor detail: this excerpt is missing certain features such as checking that the 'Nat' is in bounds, and recovering in some fashion, such as forcing it into the bounds or triggering a compilation error. This is still just a toy example, though hopefully more illustrative of the intended use case.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12432#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12432: TypeInType: open type family application as type family return kind fails to compile -------------------------------------+------------------------------------- Reporter: j6carey | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: duplicate | Keywords: Operating System: Linux | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): This example also has another problem: forgetting about lifted equality and such, an associated type cannot assume any context of an instance. This is because an associated type instance is effectively floated out of the class and behaves identically to a standalone type instance. Associated types just give you some nice syntax -- and that's it.... but maybe we need to revisit all of this, and perhaps allow type instances to specify a context. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12432#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12432: TypeInType: open type family application as type family return kind fails to compile -------------------------------------+------------------------------------- Reporter: j6carey | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: Operating System: Linux | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * status: closed => new * resolution: duplicate => Comment: This ticket is closed as a duplicate. But a duplicate of ''what''? The discussion doesn't look like duplication. I'll re-open for now. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12432#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12432: Use kind equality in instance context in type family instance -------------------------------------+------------------------------------- Reporter: j6carey | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: Operating System: Linux | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by goldfire: @@ -7,0 +7,4 @@ + + EDIT: This ticket got repurposed at comment:3 and below. The original + problem described above is fixed, but the commentary is useful to keep + around and on this ticket. New description: With TypeInType enabled, I can use a closed type family to compute the return kind of a type family from its arguments. But an equivalent open type family used in the same way triggers a compilation failure, as if the relevant instance of that open type family were not considered. (Of course, there may be some subtle prohibition of which I am not aware at the present time.) I will attach a test case. EDIT: This ticket got repurposed at comment:3 and below. The original problem described above is fixed, but the commentary is useful to keep around and on this ticket. -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12432#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12432: Use kind equality in instance context in type family instance -------------------------------------+------------------------------------- Reporter: j6carey | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: Operating System: Linux | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): I'm sorry; I'm still lost. Are you saying that there is a still-open bug, described in comment:3, and that's what the ticket is now about? If so let's either change the Description, or open a new ticket that actually describes the bug. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12432#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12432: Use kind equality in instance context in type family instance -------------------------------------+------------------------------------- Reporter: j6carey | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: Operating System: Linux | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by kosmikus): Haven't checked the attached test cases in detail, but from the description and discussion it sounds as if the original issue is #12381, which is fixed in HEAD. And the subsequent issue seems to be #12384, which is not fixed and seems to be difficult to fix. I ran into both of those issues when I tried to write a type-level translation of the new type-level generic metadata that GHC 8 provides into a different representation of type-level metadata that would be useful for generics-sop (and makes use of a type-level GADT and therefore TypeInType). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12432#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12432: Use kind equality in instance context in type family instance -------------------------------------+------------------------------------- Reporter: j6carey | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: Operating System: Linux | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by kosmikus): * cc: kosmikus (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12432#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12432: Use kind equality in instance context in type family instance -------------------------------------+------------------------------------- Reporter: j6carey | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: duplicate | Keywords: Operating System: Linux | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * status: new => closed * resolution: => duplicate Comment: I concur with comment:9 that this has become #12384. Closing as a duplicate. Please reopen if you want to, as per comment:3:ticket:12384. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12432#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC