[GHC] #10828: TH can't represent all GADTs in its AST
#10828: TH can't represent all GADTs in its AST -------------------------------------+------------------------------------- Reporter: spinda | Owner: Type: feature | Status: new request | Priority: normal | Milestone: Component: Template | Version: 7.10.2 Haskell | Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Revisions: | -------------------------------------+------------------------------------- For example, it's impossible to add a kind signature on a data type with `DataD`. In {{{Con}}} I believe it's possible to encode GADT constructor signatures using {{{NormalC}}} (haven't tried this yet), but ideally there would be another constructor specific to GADTs to go along with {{{RecC}}}, {{{InfixC}}}, and {{{ForallC}}}. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10828 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10828: TH can't represent all GADTs in its AST -------------------------------------+------------------------------------- Reporter: spinda | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Template Haskell | Version: 7.10.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by goldfire): I believe the TH AST is fully expressive here (with one tiny caveat). It's just clunky. Take {{{ data T :: k -> * -> * where MkT :: T x Int }}} To encode into TH, you transform the definition to this: {{{ data T (a1 :: k) (a2 :: *) = forall . a2 ~ Int => MkT }}} which has a direct translation. The one tiny caveat is the new feature for deriving `Foldable` for GADTs, which distinguishes among the two forms above. (I can't find a reference to this change. Can you? It was described at Haskell Implementors' Workshop a few days ago. You, the reader, if you know the reference, please add it!) Is it worth refactoring the TH types to handle GADTs more directly? Perhaps. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10828#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10828: TH can't represent all GADTs in its AST -------------------------------------+------------------------------------- Reporter: spinda | Owner: Type: feature request | Status: new Priority: normal | Milestone: 7.12.1 Component: Template Haskell | Version: 7.10.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by goldfire): * milestone: => 7.12.1 Comment: In any case, let's decide what to do and do it by the next release. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10828#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10828: TH can't represent all GADTs in its AST -------------------------------------+------------------------------------- Reporter: spinda | Owner: Type: feature request | Status: new Priority: normal | Milestone: 7.12.1 Component: Template Haskell | Version: 7.10.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by spinda): re: kind signatures -- ah, you're right. It is a bit clunky, but perhaps not worth a breaking change to the structure of {{{DataD}}} improve. Although, if #10819 makes it in, then it could be worth slipping this in at the same time. I hadn't heard about the new {{{Foldable}}} deriving feature. Any reference to that would be helpful. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10828#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10828: TH could do a better job of representing GADTs -------------------------------------+------------------------------------- Reporter: spinda | Owner: Type: feature request | Status: new Priority: normal | Milestone: 7.12.1 Component: Template Haskell | Version: 7.10.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10828#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
The one tiny caveat is the new feature for deriving Foldable for GADTs, which distinguishes among the two forms above. (I can't find a reference to this change. Can you? It was described at Haskell Implementors' Workshop a few days ago. You, the reader, if you know the reference,
#10828: TH could do a better job of representing GADTs -------------------------------------+------------------------------------- Reporter: spinda | Owner: Type: feature request | Status: new Priority: normal | Milestone: 7.12.1 Component: Template Haskell | Version: 7.10.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by simonpj): please add it!) See [wiki:Commentary/Compiler/DeriveFunctor] and #10447. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10828#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10828: TH could do a better job of representing GADTs -------------------------------------+------------------------------------- Reporter: spinda | Owner: Type: feature request | Status: new Priority: normal | Milestone: 8.0.1 Component: Template Haskell | Version: 7.10.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I think, in light of comment:5, we should add proper GADT support in TH. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10828#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10828: TH could do a better job of representing GADTs -------------------------------------+------------------------------------- Reporter: spinda | Owner: jstolarek Type: feature request | Status: new Priority: normal | Milestone: 8.0.1 Component: Template Haskell | Version: 7.10.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by jstolarek): * owner: => jstolarek Comment: I can work on implementing that, but I have one question:
I think, in light of comment:5, we should add proper GADT support in TH. Why "in light of comment:5"? I read through #10447 and I saw this example by Simon:
{{{#!hs data T1 a where MkT1 :: (a~Int) => a -> T1 a data T2 a where MkT2 :: Int -> T2 Int data T3 a where MkT3 :: (a~Int) => a -> T3 Int }}} All these declarations can be represented in TH: {{{#!hs data T1 a = a ~ Int => MkT1 a data T2 a = a ~ Int => MkT2 Int data T3 a = forall b. (a ~ Int, b ~ Int) => MkT3 b }}} It is possible to automatically derive `Foldable` for all three declarations `T1`, `T2` and `T3`, both in GADT form as well as in the standard form given above, so `DerivingFoldable` makes no distinction between these three declarations. Are there other declarations where `Foldable` distinguishes the two forms? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10828#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10828: TH could do a better job of representing GADTs -------------------------------------+------------------------------------- Reporter: spinda | Owner: jstolarek Type: feature request | Status: new Priority: normal | Milestone: 8.0.1 Component: Template Haskell | Version: 7.10.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by jstolarek): My proposal would be to add the following constructor to `Con` data type: {{{#!hs | GadtC Name [StrictType] [Type] }}} where the last field stores list of constructor indices. Once we have this new constructor I would modify `DsMera` and `Convert` accordingly. Most importantly, GADT declarations would be now translated to use this new constructor instead of encoding that uses `ForallC` and `NormalC`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10828#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10828: TH could do a better job of representing GADTs -------------------------------------+------------------------------------- Reporter: spinda | Owner: jstolarek Type: feature request | Status: new Priority: normal | Milestone: 8.0.1 Component: Template Haskell | Version: 7.10.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Replying to [comment:8 jstolarek]:
It is possible to automatically derive `Foldable` for all three declarations `T1`, `T2` and `T3`, both in GADT form as well as in the standard form given above, so `DerivingFoldable` makes no distinction between these three declarations.
I agree that deriving `Foldable` works for all of them, but does it do the same thing? I would expect not, from the commentary on #10447. Your `GadtC` is missing a place for a `[TyVarBndr]` (to store the quantified type variables, both universals and existentials) and a `Cxt` to store any extra constraints. It also forbids record syntax, but maybe we can live without GADT record syntax. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10828#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
Your `GadtC` is missing a place for a `[TyVarBndr]` (to store the quantified type variables, both universals and existentials) and a `Cxt` to store any extra constraints. My intention was to nest `GadtC` inside `ForallC`. Is there any reason why
#10828: TH could do a better job of representing GADTs -------------------------------------+------------------------------------- Reporter: spinda | Owner: jstolarek Type: feature request | Status: new Priority: normal | Milestone: 8.0.1 Component: Template Haskell | Version: 7.10.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by jstolarek): this wouldn't work?
It also forbids record syntax, but maybe we can live without GADT record syntax. Ok, I haven't thought about that one. TBH I think I have never used (or seen) GADTs with record syntax.
-- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10828#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10828: TH could do a better job of representing GADTs -------------------------------------+------------------------------------- Reporter: spinda | Owner: jstolarek Type: feature request | Status: new Priority: normal | Milestone: 8.0.1 Component: Template Haskell | Version: 7.10.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Replying to [comment:11 jstolarek]:
My intention was to nest `GadtC` inside `ForallC`. Is there any reason why this wouldn't work? Good point. That would work well.
The documentation should make clear that, unlike other constructor forms, GADT constructors do ''not'' have the type variables from the declaration head in scope. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10828#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
The documentation should make clear that, unlike other constructor
#10828: TH could do a better job of representing GADTs -------------------------------------+------------------------------------- Reporter: spinda | Owner: jstolarek Type: feature request | Status: new Priority: normal | Milestone: 8.0.1 Component: Template Haskell | Version: 7.10.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by jstolarek): Replying to [comment:12 goldfire]: forms, GADT constructors do ''not'' have the type variables from the declaration head in scope. Does that make a difference for TH representation (ie. `GadtC` data type)? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10828#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10828: TH could do a better job of representing GADTs -------------------------------------+------------------------------------- Reporter: spinda | Owner: jstolarek Type: feature request | Status: new Priority: normal | Milestone: 8.0.1 Component: Template Haskell | Version: 7.10.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): No. But it does affect the code in Convert and !DsMeta. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10828#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10828: TH could do a better job of representing GADTs -------------------------------------+------------------------------------- Reporter: spinda | Owner: jstolarek Type: feature request | Status: new Priority: normal | Milestone: 8.0.1 Component: Template Haskell | Version: 7.10.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by jstolarek): These are `Foldable` instances derived automatically for data types in comment:8 {{{#!hs instance Foldable T1 where foldr f z (MkT1 a1) = f a1 z foldMap f (MkT1 a1) = f a1 instance Foldable T1' where foldr f z (MkT1' a1) = f a1 z foldMap f (MkT1' a1) = f a1 instance Foldable T2 where foldr f z (MkT2 a1) = (\ b1 b2 -> b2) a1 z foldMap f (MkT2 a1) = (\ b1 -> mempty) a1 instance Foldable T2' where foldr f z (MkT2' a1) = (\ b1 b2 -> b2) a1 z foldMap f (MkT2' a1) = (\ b1 -> mempty) a1 instance Foldable T3 where foldr f z (MkT3 a1) = (\ b1 b2 -> b2) a1 z foldMap f (MkT3 a1) = (\ b1 -> mempty) a1 instance Foldable T3' where foldr f z (MkT3' a1) = (\ b1 b2 -> b2) a1 z foldMap f (MkT3' a1) = (\ b1 -> mempty) a1 }}} So `DerivingFoldable` does not distinguish between GADT and normal declarations - respective pairs of instances are identical. At least in this case. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10828#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10828: TH could do a better job of representing GADTs -------------------------------------+------------------------------------- Reporter: spinda | Owner: jstolarek Type: feature request | Status: new Priority: normal | Milestone: 8.0.1 Component: Template Haskell | Version: 7.10.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Good. I understood you to mean previously that the three forms had the same `Foldable` instance -- not that primed forms matched the unprimed forms, as you've clarified here. So fixing this is a bit less compelling. But I still think it would be nice, given that TH is meant to reflect Haskell syntax, and it fails miserably in this corner. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10828#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10828: TH could do a better job of representing GADTs -------------------------------------+------------------------------------- Reporter: spinda | Owner: jstolarek Type: feature request | Status: new Priority: normal | Milestone: 8.0.1 Component: Template Haskell | Version: 7.10.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D1465 Wiki Page: | -------------------------------------+------------------------------------- Changes (by jstolarek): * differential: => Phab:D1465 Comment: I'll continue the discussion on Phab. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10828#comment:17 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10828: TH could do a better job of representing GADTs -------------------------------------+------------------------------------- Reporter: spinda | Owner: jstolarek Type: feature request | Status: new Priority: normal | Milestone: 8.0.1 Component: Template Haskell | Version: 7.10.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #4188 | Differential Rev(s): Phab:D1465 Wiki Page: | -------------------------------------+------------------------------------- Changes (by jstolarek): * related: => #4188 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10828#comment:18 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10828: TH could do a better job of representing GADTs -------------------------------------+------------------------------------- Reporter: spinda | Owner: jstolarek Type: feature request | Status: new Priority: normal | Milestone: 8.0.1 Component: Template Haskell | Version: 7.10.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #4188, #5217 | Differential Rev(s): Phab:D1465 Wiki Page: | -------------------------------------+------------------------------------- Changes (by jstolarek): * related: #4188 => #4188, #5217 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10828#comment:19 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10828: TH could do a better job of representing GADTs
-------------------------------------+-------------------------------------
Reporter: spinda | Owner: jstolarek
Type: feature request | Status: new
Priority: normal | Milestone: 8.0.1
Component: Template Haskell | Version: 7.10.2
Resolution: | Keywords:
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: None/Unknown | Test Case:
Blocked By: | Blocking:
Related Tickets: #4188, #5217 | Differential Rev(s): Phab:D1465
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Jan Stolarek
#10828: TH could do a better job of representing GADTs -------------------------------------+------------------------------------- Reporter: spinda | Owner: jstolarek Type: feature request | Status: closed Priority: normal | Milestone: 8.0.1 Component: Template Haskell | Version: 7.10.2 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: th/T10828, | th/T10828a, th/T10828b Blocked By: | Blocking: Related Tickets: #4188, #5217 | Differential Rev(s): Phab:D1465 Wiki Page: | -------------------------------------+------------------------------------- Changes (by jstolarek): * status: new => closed * testcase: => th/T10828, th/T10828a, th/T10828b * resolution: => fixed -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10828#comment:21 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC