Reifying a GADT doesn't tell you the correct return type

changed weight to 5

added Tbug TemplateHaskell Trac import labels

The bug might even be deeper than that. If I try using a more complex type synonym:

{-# 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":

{-# 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:

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?

Currently reifying a GADT data constructor tells us "what the user meant", not "what the user wrote", ie. type synonyms are expanded.

I think the most important question is what should the GADT data constructor representation look like. I believe that TH should represent source code syntax. That said, your third example shows that the current representation is not sufficient. So I would propose to represent GADT data constructor as:

data Con = ...
         | GadtC [Name] [StrictType] Type

Where Type is the result type written by the user. In TcSplice.reifyDataCon we have access to dcOrigResTy field of a DataCon, which should allow us to reify original result type.

data T a where
  MkT :: a -> T a

Note that by result type of MkT I mean T a, not a -> T a. (I believe dcOrigResTy stores the latter).

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.

Replying to [ticket:11341#comment:112604 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.

Replying to [ticket:11341#comment:112607 RyanGlScott]:

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.

Just to be clear: TH syntax tree already allows to write all sorts of silliness that we have to catch later on in the pipeline. This would be another such thing. 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 suppose the real type indices can always be found out through something like expand in th-desugar.

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

Replying to [ticket:11341#comment:112608 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 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’

assigned to @trac-jstolarek

Trac metadata

Trac field	Value
Differential revisions	- → D1738
Related	- → #10828 (closed)

mentioned in commit cac0795a

This is now fixed in HEAD. It would be really good to have this in GHC 8.0.

Trac metadata

Trac field	Value
Test case	- → th/T11341

added 1 deleted label

changed milestone to %8.0.1

Trac metadata

Trac field	Value
Version	8.1 → 7.11

Trac metadata

Trac field	Value
Related	#10828 (closed) → #10719 (closed), #10828 (closed)

closed

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedFixed

removed 1 deleted label

added incorrect runtime result label

added Pnormal label

Reifying a GADT doesn't tell you the correct return type

Child items 0

Activity

Reifying a GADT doesn't tell you the correct return type

Relates to

Activity