Re: [GHC] #14579: GeneralizedNewtypeDeriving produces ambiguously-kinded code

5 Jan 2019

      #14579: GeneralizedNewtypeDeriving produces ambiguously-kinded code
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.10.1
       Component:  Compiler (Type    |              Version:  8.2.2
  checker)                           |
      Resolution:                    |             Keywords:  deriving
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  GHC rejects       |            Test Case:
  valid program                      |  deriving/should_compile/T14579{a}
      Blocked By:  12045             |             Blocking:
 Related Tickets:                    |  Differential Rev(s):  Phab:D4264,
       Wiki Page:                    |  Phab:D5229
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 Cruelly enough, comment:20 means the the original program in this ticket
 must have an explicit kind signature anyway, since in the kind of
 `'Proxy`:

 {{{#!hs
 'Proxy :: forall {k} (a :: k). Proxy a
 }}}

 We have an inferred type variable binder! Argh.

 I wonder if we can be a bit smarter about where we put explicit kind
 signatures? This is the code that GHC 8.6.3 currently generates for the
 original program's `Eq (Glurp a)` instance:

 {{{
   instance GHC.Classes.Eq a => GHC.Classes.Eq (Bug.Glurp a) where
     (GHC.Classes.==)
       = GHC.Prim.coerce
           @((Bug.Wat (Data.Proxy.Proxy :: (Data.Proxy.Proxy a_a1Dx :: TYPE
 GHC.Types.LiftedRep)) :: TYPE GHC.Types.LiftedRep)
             -> (Bug.Wat (Data.Proxy.Proxy :: (Data.Proxy.Proxy a_a1Dx ::
 TYPE GHC.Types.LiftedRep)) :: TYPE GHC.Types.LiftedRep)
                -> GHC.Types.Bool)
           @(Bug.Glurp a_a1Dx -> Bug.Glurp a_a1Dx -> GHC.Types.Bool)
           (GHC.Classes.==) ::
           Bug.Glurp a_a1Dx -> Bug.Glurp a_a1Dx -> GHC.Types.Bool
     (GHC.Classes./=)
       = GHC.Prim.coerce
           @((Bug.Wat (Data.Proxy.Proxy :: (Data.Proxy.Proxy a_a1Dx :: TYPE
 GHC.Types.LiftedRep)) :: TYPE GHC.Types.LiftedRep)
             -> (Bug.Wat (Data.Proxy.Proxy :: (Data.Proxy.Proxy a_a1Dx ::
 TYPE GHC.Types.LiftedRep)) :: TYPE GHC.Types.LiftedRep)
                -> GHC.Types.Bool)
           @(Bug.Glurp a_a1Dx -> Bug.Glurp a_a1Dx -> GHC.Types.Bool)
           (GHC.Classes./=) ::
           Bug.Glurp a_a1Dx -> Bug.Glurp a_a1Dx -> GHC.Types.Bool
 }}}

 There are many explicit kind signatures here that are completely
 redundant—for instance, each `(_ :: TYPE GHC.Types.LiftedRep)` signature
 is redundant, since they're not needed to fix any type variables. The only
 signature that's strictly necessary is the `(Data.Proxy.Proxy ::
 (Data.Proxy.Proxy a_a1Dx :: ...))` one, since that fixes `a_a1Dx`.

 Perhaps we should adopt a more fine-grained heuristic (besides the mere
 presence of inferred type variable binders) to determine when to insert
 explicit kind signatures? For instance, the `reify_tc_app` function in
 `TcSplice` (which reifies applications of tycons) uses a more complicated
 heuristic: if the free variables of the tycon's kind are not a subset of
 the free variables of the arguments in injective positions, then it needs
 an explicit signature. (This is explained in
 [https://gitlab.haskell.org/ghc/ghc/blob/master/compiler/typecheck/TcSplice.h...
 this Note]).

 This heuristic could work well in this situation as well. We'd need to
 modify the definition of "injective positions" to include specified
 arguments (currently it only includes required ones), but if we did, then
 I believe we could drop all of the explicit signatures in the original
 program.

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