Re: [GHC] #16300: Make TH always reify data types with explicit return kinds

11 Feb 2019

      #16300: Make TH always reify data types with explicit return kinds
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Template Haskell  |              Version:  8.6.3
      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 RyanGlScott):

 Ah, but the program in comment:2 is accepted for different reasons than
 what I expected. It's not being accepted due to the fact that `Just StarT`
 is ignored. In fact, GHC //is// checking the explicit return kind! This is
 demonstrated by this program, which tries to sneak in something bogus:

 {{{#!hs
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE TemplateHaskell #-}
 module Bug where

 import Language.Haskell.TH

 $(pure [NewtypeD [] (mkName "D") [] (Just (ArrowT `AppT` ConT ''Maybe
 `AppT` StarT))
                  (NormalC (mkName "MkD")
                           [(Bang NoSourceUnpackedness NoSourceStrictness,
 ConT ''Int)])
                  []])
 }}}
 {{{
 GHCi, version 8.6.3: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 [1 of 1] Compiling Bug              ( Bug.hs, interpreted )

 Bug.hs:8:3: error:
     • Expecting one more argument to ‘Maybe’
       Expected a type, but ‘Maybe’ has kind ‘* -> *’
     • In the kind ‘Maybe -> GHC.Types.Type’
   |
 8 | $(pure [NewtypeD [] (mkName "D") [] (Just (ArrowT `AppT` ConT ''Maybe
 `AppT` StarT))
   |
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
 }}}

 I suppose this reveals another viable alternative. We could just treat the
 program in comment:1 as though we were trying to splice in a GADT (i.e.,
 `newtype D :: Type where MkD :: D`). Granted, we'd then be splicing in a
 GADT using `NormalC` instead of the usual `GadtC`, but there's no reason
 why we couldn't reinterpret `NormalC` as though it were specifying a GADT
 constructor.

 ...except there's another weird thing that `Convert` does in which it
 rejects mixed uses of `NormalC` and `GadtC`:

 {{{#!hs
         ; unless (isGadtDecl || isH98Decl)
                  (failWith (text "Cannot mix GADT constructors with
 Haskell 98"
                         <+> text "constructors"))
 }}}

 This suggests that if we want to pursue this direction, then we should
 further lift this mixed constructors restriction. Hm...

 I'm not sure which route to go down. Do others have any thoughts?

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16300#comment:3
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler