#11341: Reifying a GADT doesn't tell you the correct return type -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Template Haskell | Version: 8.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect result | Unknown/Multiple at runtime | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * cc: goldfire (added) Comment: The bug might even be deeper than that. If I try using a more complex type synonym: {{{#!hs {-# LANGUAGE GADTs, TemplateHaskell #-} module Main (main) where import Language.Haskell.TH type S a = T data T a where MkT :: S Char Int $(return []) main :: IO () main = putStrLn $(reify ''T >>= stringE . pprint) }}} then it doesn't tell you that the type indices are both `Char` and `Int`: {{{ data Main.T (a_0 :: *) where Main.MkT :: Main.T GHC.Types.Int }}} The same thing is outputted even when the GADT return type appears as a "type index": {{{#!hs {-# LANGUAGE GADTs, TemplateHaskell #-} module Main (main) where import Language.Haskell.TH type Id a = a type S a = T data T a where MkT :: Id (S Char Int) $(return []) main :: IO () main = putStrLn $(reify ''T >>= stringE . pprint) }}} That brings up an interesting design question. Is the third field of `Gadt` (a `Name`) intended to be the outermost type application, and the fourth field (a `[Type]`) intended to be the types that to which the `Name` is applied? If so, then the "type index" returned in the above example is just `S Char Int`, so how should a Template Haskell programmer know that `a` is being refined to `Int`? Presumably, you'd have to do some tricky type arithmetic, which doesn't sit right to me. Perhaps it would be better to change `GadtC` to this: {{{#!hs data Con = ... | GadtC [Name] [BangType] Type [Type] }}} where the third field contains the return type as written in the source code (in the above example, `Id (S Char Int)`) and the fourth field contains the type indices after expanding type synonyms (in the above example, `Int`). Similarly for `RecGadtC`. Jan, Richard, what are your thoughts? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11341#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11341: Reifying a GADT doesn't tell you the correct return type -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Template Haskell | Version: 8.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect result | Unknown/Multiple at runtime | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Replying to [comment:2 jstolarek]:

In this setting I don't think it is a good idea to store indices inside `GadtC`. This would duplicate information already stored inside the constructor and make it possible to create inconsistent data constructors.

That's a good point I hadn't thought of. We definitely don't want users to be able to splice in type indices that don't match up with the actual return type. I suppose the real type indices can always be found out through something like `expand` in `th-desugar`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11341#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11341: Reifying a GADT doesn't tell you the correct return type -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Template Haskell | Version: 8.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect result | Unknown/Multiple at runtime | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Replying to [comment:4 jstolarek]:

I just fear that the check would not be trivial. I also think that in most cases GADT result type simply includes indexed type constructor and having to duplicate the indices will be painful.

I agree with you here fully. Also, I hope there's ''never'' a case where where a GADT result type isn't an instance of the parent type (modulo type synonyms)—that would be strange indeed!

In such corner cases that you've demonstrated indices might be very hard (impossible?) to recover. But I think that's acceptable.

Again, I wouldn't think there's ''any'' case in which you couldn't recover the type indices. The only case where `th-desugar`'s `expand` function [https://github.com/goldfirere/th- desugar/blob/60b78b2b423fcb6f8bcdd2f10fbe2ce79192982c/Language/Haskell/TH/Desugar/Expand.hs#L56 can choke] is with type families, but GHC doesn't attempt to expand type families in a GADT definition anyway, so there's nothing to worry about: {{{ $ ghci GHCi, version 7.10.3: http://www.haskell.org/ghc/ :? for help λ> :set -XTypeFamilies -XGADTs λ> type family Id a where Id a = a λ> data Wat a where Wat :: a -> Id (Wat a) <interactive>:4:18: Data constructor ‘Wat’ returns type ‘Id (Wat a)’ instead of an instance of its parent type ‘Wat a’ In the definition of data constructor ‘Wat’ In the data declaration for ‘Wat’ }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11341#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11341: Reifying a GADT doesn't tell you the correct return type -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: jstolarek Type: bug | Status: new Priority: normal | Milestone: Component: Template Haskell | Version: 8.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect result | Unknown/Multiple at runtime | Test Case: Blocked By: | Blocking: Related Tickets: #10828 | Differential Rev(s): Phab:D1738 Wiki Page: | -------------------------------------+------------------------------------- Changes (by jstolarek): * differential: => Phab:D1738 * related: => #10828 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11341#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11341: Reifying a GADT doesn't tell you the correct return type -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: jstolarek Type: bug | Status: merge Priority: normal | Milestone: Component: Template Haskell | Version: 8.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect result | Unknown/Multiple at runtime | Test Case: th/T11341 Blocked By: | Blocking: Related Tickets: #10828 | Differential Rev(s): Phab:D1738 Wiki Page: | -------------------------------------+------------------------------------- Changes (by jstolarek): * status: new => merge * testcase: => th/T11341 Comment: This is now fixed in HEAD. It would be really good to have this in GHC 8.0. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11341#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11341: Reifying a GADT doesn't tell you the correct return type -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: jstolarek Type: bug | Status: merge Priority: normal | Milestone: 8.0.1 Component: Template Haskell | Version: 7.11 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect result | Unknown/Multiple at runtime | Test Case: th/T11341 Blocked By: | Blocking: Related Tickets: #10828 #10719 | Differential Rev(s): Phab:D1738 Wiki Page: | -------------------------------------+------------------------------------- Changes (by heisenbug): * related: #10828 => #10828 #10719 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11341#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler