Re: [GHC] #11341: Reifying a GADT doesn't tell you the correct return type

2 Jan 2016

      #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