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

3 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:                    |
-------------------------------------+-------------------------------------

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