Opened 21 months ago

Closed 7 months ago

Last modified 7 months ago

#14579 closed bug (fixed)

GeneralizedNewtypeDeriving produces ambiguously-kinded code

Reported by: RyanGlScott Owned by:
Priority: normal Milestone: 8.10.1
Component: Compiler (Type checker) Version: 8.2.2
Keywords: deriving Cc: mnguyen
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case: deriving/should_compile/T14579{a,b}
Blocked By: Blocking:
Related Tickets: Differential Rev(s): Phab:D4264, Phab:D5229, https://gitlab.haskell.org/ghc/ghc/merge_requests/261
Wiki Page:

Description

This program should compile:

{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE TypeInType #-}
module Bug where

import Data.Kind
import Data.Proxy

newtype Wat (x :: Proxy (a :: Type)) = MkWat (Maybe a)
  deriving Eq

newtype Glurp a = MkGlurp (Wat ('Proxy :: Proxy a))
  deriving Eq

After all, it should produce this Eq (Glurp a) instance, which compiles without issue:

instance Eq a => Eq (Glurp a) where
  (==) = coerce @(Wat ('Proxy :: Proxy a) -> Wat ('Proxy :: Proxy a) -> Bool)
                @(Glurp a                 -> Glurp a                 -> Bool)
                (==)

But despite my wishful thinking, GHC does not actually do this. In fact, the code that GHC tries to generate for an Eq (Glurp a) instance is completely wrong:

$ /opt/ghc/8.2.2/bin/ghci -ddump-deriv Bug.hs
GHCi, version 8.2.2: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )

==================== Derived instances ====================
Derived class instances:
  instance forall a (x :: Data.Proxy.Proxy a).
           GHC.Classes.Eq a =>
           GHC.Classes.Eq (Bug.Wat x) where
    (GHC.Classes.==)
      = GHC.Prim.coerce
          @(GHC.Base.Maybe a_a2wE -> GHC.Base.Maybe a_a2wE -> GHC.Types.Bool)
          @(Bug.Wat x_a2wF -> Bug.Wat x_a2wF -> GHC.Types.Bool)
          (GHC.Classes.==)
    (GHC.Classes./=)
      = GHC.Prim.coerce
          @(GHC.Base.Maybe a_a2wE -> GHC.Base.Maybe a_a2wE -> GHC.Types.Bool)
          @(Bug.Wat x_a2wF -> Bug.Wat x_a2wF -> GHC.Types.Bool)
          (GHC.Classes./=)
  
  instance GHC.Classes.Eq a => GHC.Classes.Eq (Bug.Glurp a) where
    (GHC.Classes.==)
      = GHC.Prim.coerce
          @(Bug.Wat Data.Proxy.Proxy
            -> Bug.Wat Data.Proxy.Proxy -> GHC.Types.Bool)
          @(Bug.Glurp a_a1vT -> Bug.Glurp a_a1vT -> GHC.Types.Bool)
          (GHC.Classes.==)
    (GHC.Classes./=)
      = GHC.Prim.coerce
          @(Bug.Wat Data.Proxy.Proxy
            -> Bug.Wat Data.Proxy.Proxy -> GHC.Types.Bool)
          @(Bug.Glurp a_a1vT -> Bug.Glurp a_a1vT -> GHC.Types.Bool)
          (GHC.Classes./=)
  

Derived type family instances:



Bug.hs:12:12: error:
    • Couldn't match representation of type ‘a0’ with that of ‘a’
        arising from a use of ‘GHC.Prim.coerce’
      ‘a’ is a rigid type variable bound by
        the instance declaration at Bug.hs:12:12-13
    • In the expression:
        GHC.Prim.coerce
          @(Wat Proxy -> Wat Proxy -> Bool)
          @(Glurp a -> Glurp a -> Bool)
          (==)
      In an equation for ‘==’:
          (==)
            = GHC.Prim.coerce
                @(Wat Proxy -> Wat Proxy -> Bool)
                @(Glurp a -> Glurp a -> Bool)
                (==)
      When typechecking the code for ‘==’
        in a derived instance for ‘Eq (Glurp a)’:
        To see the code I am typechecking, use -ddump-deriv
      In the instance declaration for ‘Eq (Glurp a)’
    • Relevant bindings include
        (==) :: Glurp a -> Glurp a -> Bool (bound at Bug.hs:12:12)
   |
12 |   deriving Eq
   |            ^^

Bug.hs:12:12: error:
    • Could not deduce (Eq a0) arising from a use of ‘==’
      from the context: Eq a
        bound by the instance declaration at Bug.hs:12:12-13
      The type variable ‘a0’ is ambiguous
      These potential instances exist:
        instance forall k (s :: k). Eq (Proxy s) -- Defined in ‘Data.Proxy’
        instance Eq Ordering -- Defined in ‘GHC.Classes’
        instance Eq Integer
          -- Defined in ‘integer-gmp-1.0.1.0:GHC.Integer.Type’
        ...plus 25 others
        ...plus 9 instances involving out-of-scope types
        (use -fprint-potential-instances to see them all)
    • In the third argument of ‘GHC.Prim.coerce’, namely ‘(==)’
      In the expression:
        GHC.Prim.coerce
          @(Wat Proxy -> Wat Proxy -> Bool)
          @(Glurp a -> Glurp a -> Bool)
          (==)
      In an equation for ‘==’:
          (==)
            = GHC.Prim.coerce
                @(Wat Proxy -> Wat Proxy -> Bool)
                @(Glurp a -> Glurp a -> Bool)
                (==)
      When typechecking the code for ‘==’
        in a derived instance for ‘Eq (Glurp a)’:
        To see the code I am typechecking, use -ddump-deriv
   |
12 |   deriving Eq
   |            ^^

Bug.hs:12:12: error:
    • Couldn't match representation of type ‘a1’ with that of ‘a’
        arising from a use of ‘GHC.Prim.coerce’
      ‘a’ is a rigid type variable bound by
        the instance declaration at Bug.hs:12:12-13
    • In the expression:
        GHC.Prim.coerce
          @(Wat Proxy -> Wat Proxy -> Bool)
          @(Glurp a -> Glurp a -> Bool)
          (/=)
      In an equation for ‘/=’:
          (/=)
            = GHC.Prim.coerce
                @(Wat Proxy -> Wat Proxy -> Bool)
                @(Glurp a -> Glurp a -> Bool)
                (/=)
      When typechecking the code for ‘/=’
        in a derived instance for ‘Eq (Glurp a)’:
        To see the code I am typechecking, use -ddump-deriv
      In the instance declaration for ‘Eq (Glurp a)’
    • Relevant bindings include
        (/=) :: Glurp a -> Glurp a -> Bool (bound at Bug.hs:12:12)
   |
12 |   deriving Eq
   |            ^^

Bug.hs:12:12: error:
    • Could not deduce (Eq a1) arising from a use of ‘/=’
      from the context: Eq a
        bound by the instance declaration at Bug.hs:12:12-13
      The type variable ‘a1’ is ambiguous
      These potential instances exist:
        instance forall k (s :: k). Eq (Proxy s) -- Defined in ‘Data.Proxy’
        instance Eq Ordering -- Defined in ‘GHC.Classes’
        instance Eq Integer
          -- Defined in ‘integer-gmp-1.0.1.0:GHC.Integer.Type’
        ...plus 25 others
        ...plus 9 instances involving out-of-scope types
        (use -fprint-potential-instances to see them all)
    • In the third argument of ‘GHC.Prim.coerce’, namely ‘(/=)’
      In the expression:
        GHC.Prim.coerce
          @(Wat Proxy -> Wat Proxy -> Bool)
          @(Glurp a -> Glurp a -> Bool)
          (/=)
      In an equation for ‘/=’:
          (/=)
            = GHC.Prim.coerce
                @(Wat Proxy -> Wat Proxy -> Bool)
                @(Glurp a -> Glurp a -> Bool)
                (/=)
      When typechecking the code for ‘/=’
        in a derived instance for ‘Eq (Glurp a)’:
        To see the code I am typechecking, use -ddump-deriv
   |
12 |   deriving Eq
   |            ^^

Yikes. To see what went wrong, let's zoom in a particular part of the -ddump-deriv output (cleaned up a bit for presentation purposes):

  instance Eq a => Eq (Glurp a) where
    (==)
      = coerce
          @(Wat 'Proxy -> Wat 'Proxy -> Bool)
          @(Glurp a -> Glurp a -> Bool)
          (==)

Notice that it's Wat 'Proxy, and not Wat ('Proxy :: Proxy a)! And no, that's not just a result of GHC omitting the kind information—you will see the exact same thing if you compile with -fprint-explicit-kinds. What's going on here?

As it turns out, the types inside of those visible type applications aren't Types, but rather HsType GhcRns (i.e., source syntax). So what is happening is that GHC is literally producing @(Wat 'Proxy -> Wat 'Proxy -> Bool) as source syntax, not as a Type. This means that 'Proxy has an underspecified kind, resulting in the numerous The type variable ‘a0’ is ambiguous errors you see above.

Change History (28)

comment:1 Changed 21 months ago by simonpj

Hm... look at TcGenDeriv.nlHsAppType. Presumably you want to add the necessary kind signatures when doing typeToHsType.

comment:2 Changed 21 months ago by RyanGlScott

Differential Rev(s): Phab:D4264
Status: newpatch

comment:3 Changed 21 months ago by simonpj

What change to typeToHsType do we want? The problem is to specify the invisible kind arguments to occurrences of poly-kinded type-constructor applications. Eg

instance Eq a => Eq (Glurp a) where
    (==)
      = coerce
          @(Wat 'Proxy -> Wat 'Proxy -> Bool)
          @(Glurp a -> Glurp a -> Bool)
          (==)

The problem is the invisible kind arguments to the poly-kinded 'Proxy occurrences. If we had visible kind application we could use that, but we don't. Solution: add a kind signature, as in the Description:

instance Eq a => Eq (Glurp a) where
  (==) = coerce @(Wat ('Proxy :: Proxy a) -> Wat ('Proxy :: Proxy a) -> Bool)
                @(Glurp a                 -> Glurp a                 -> Bool)
                (==)

When do we need a kind signature?

  • (a) When we have an application of a type constructor with invisible arguments
  • (b) And the invisible arguments are not fixed by the kinds of the visible arguments.

Probably just using (a) is enough to reduce the noise of redundant kind signatures to reasonable levels.

comment:4 Changed 21 months ago by goldfire

Is there any reason we can't say

typeToLHsType = noLoc . HsCoreTy

? That certainly seems to save a lot of huffing and puffing.

comment:5 Changed 21 months ago by simonpj

Good thought. But these types have free type variables, bound by the instance decl. I'm far from sure they'd line up right.

comment:6 Changed 21 months ago by RyanGlScott

simonpj's hunch appears to be right—I just attempted to compile GHC with goldfire's suggested change, and wound up face-first in panictown:

libraries/base/GHC/Generics.hs:811:13: error:ghc-stage1: panic! (the 'impossible' happened)
  (GHC version 8.5.20171213 for x86_64-unknown-linux):
        No skolem info:
  [p3_a3Jl]
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/utils/Outputable.hs:1150:37 in ghc:Outputable
        pprPanic, called at compiler/typecheck/TcErrors.hs:2892:5 in ghc:TcErrors

I'll try simonpj's suggested refactoring in comment:3.

comment:7 Changed 21 months ago by goldfire

Ryan's visit to panictown notwithstanding, I'm still not convinced by comment:5. comment:5 seems to be suggesting that we need the generated code to pass through the renamer, so that the type variables can be captured. This is a reasonable guess. But typeToLHsType, as currently written (and working), uses Exact names, so the journey through the renamer doesn't capture anything. Perhaps the panic is actually caused by these lines in RnTypes:

rnHsTyKi _ (HsCoreTy ty)
  = return (HsCoreTy ty, emptyFVs)
    -- The emptyFVs probably isn't quite right
    -- but I don't think it matters

Maybe it matters. Or maybe I'm missing something more fundamental.

comment:8 Changed 21 months ago by RyanGlScott

I think it would be worthwhile to investigate this issue further (probably in another Trac ticket). My gut feeling is that Phab:D4264 is simple enough that we can adopt it without too much worry—worst comes to worst, we can scrap the current implementation of typeToLHsType in favor of something simpler later.

comment:9 Changed 21 months ago by Ryan Scott <ryan.gl.scott@…>

In 649e777/ghc:

Make typeToLHsType produce kind signatures for tycon applications

Summary:
`GeneralizedNewtypeDeriving` generates calls to `coerce`
which take visible type arguments. These types must be produced by
way of `typeToLHsType`, which converts a `Type` to an `LHsType`.
However, `typeToLHsType` was leaving off important kind information
when a `Type` contained a poly-kinded tycon application, leading to
incorrectly generated code in #14579.

This fixes the issue by tweaking `typeToLHsType` to generate
explicit kind signatures for tycon applications. This makes the
generated code noisier, but at least the program from #14579 now
works correctly.

Test Plan: make test TEST=T14579

Reviewers: simonpj, bgamari

Reviewed By: simonpj

Subscribers: rwbarton, thomie, carter

GHC Trac Issues: #14579

Differential Revision: https://phabricator.haskell.org/D4264

comment:10 Changed 21 months ago by RyanGlScott

Milestone: 8.4.1
Status: patchmerge
Test Case: deriving/should_compile/T14579

Could merge to 8.4.1 if convenient.

comment:11 Changed 20 months ago by bgamari

Resolution: fixed
Status: mergeclosed

Merged in ebf8e07629.

comment:12 Changed 11 months ago by RyanGlScott

Blocked By: 12045 added
Milestone: 8.4.18.8.1
Resolution: fixed
Status: closednew

I wonder if the hack we implemented to fix this issue originally could be made substantially simpler with visible kind applications (which should be available soon-ish). With VKAs, we could instead generate the following code:

{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE TypeInType #-}
module Bug where

import Data.Kind
import Data.Proxy

newtype Wat (x :: Proxy (a :: Type)) = MkWat (Maybe a)
  deriving Eq

newtype Glurp a = MkGlurp (Wat ('Proxy :: Proxy a))

instance Eq a => Eq (Glurp a) where
  (==) = coerce @(Wat ('Proxy @a) -> Wat ('Proxy @a) -> Bool)
                @(Glurp a         -> Glurp a         -> Bool)
                (==)

I'll reopen this ticket to keep track of this idea.

comment:13 Changed 11 months ago by simonpj

Yes indeed. comment:3 identifies VKA as the desired facility, with kind signatures as second best. Good idea to re-open

comment:14 Changed 11 months ago by goldfire

Cc: mynguyen added

Cc'ing the implementor of visible kind application.

comment:15 Changed 11 months ago by goldfire

Cc: mnguyen added; mynguyen removed

comment:16 in reply to:  12 Changed 10 months ago by mnguyen

{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE TypeInType #-}
module Bug where

import Data.Kind
import Data.Proxy

newtype Wat (x :: Proxy (a :: Type)) = MkWat (Maybe a)
  deriving Eq

newtype Glurp a = MkGlurp (Wat ('Proxy :: Proxy a))

instance Eq a => Eq (Glurp a) where
  (==) = coerce @(Wat ('Proxy @a) -> Wat ('Proxy @a) -> Bool)
                @(Glurp a         -> Glurp a         -> Bool)
                (==)

I try this with my current VKA and it fails

T14579a.hs:15:32: error: Not in scope: type variable a

T14579a.hs:15:51: error: Not in scope: type variable a

T14579a.hs:16:25: error: Not in scope: type variable a

T14579a.hs:16:44: error: Not in scope: type variable a

???

comment:17 Changed 10 months ago by RyanGlScott

I've responded to comment:16 at https://phabricator.haskell.org/D5229#inline-42631. (The code is very nearly correct; you just need some minor tweaks to make it compile).

Also, thanks for adding a test case for this! Once the VKA patch lands, I can look into tweaking GeneralizedNewtypeDeriving itself such that it generates code with visible kind applications.

comment:18 Changed 9 months ago by osa1

Milestone: 8.8.18.10.1

Bumping milestones of low-priority tickets.

comment:19 Changed 9 months ago by RyanGlScott

Differential Rev(s): Phab:D4264Phab:D4264, Phab:D5229
Test Case: deriving/should_compile/T14579deriving/should_compile/T14579{a}

A test case was added in 17bd163566153babbf51adaff8397f948ae363ca:

Author: mynguyen <mnguyen1@brynmawr.edu>
Date:   Tue Dec 18 11:52:26 2018 -0500

    Visible kind application
    
    Summary:
    This patch implements visible kind application (GHC Proposal 15/#12045), as well as #15360 and #15362.
    It also refactors unnamed wildcard handling, and requires that type equations in type families in Template Haskell be
    written with full type on lhs. PartialTypeSignatures are on and warnings are off automatically with visible kind
    application, just like in term-level.
    
    There are a few remaining issues with this patch, as documented in
    ticket #16082.
    
    Includes a submodule update for Haddock.
    
    Test Plan: Tests T12045a/b/c/TH1/TH2, T15362, T15592a
    
    Reviewers: simonpj, goldfire, bgamari, alanz, RyanGlScott, Iceland_jack
    
    Subscribers: ningning, Iceland_jack, RyanGlScott, int-index, rwbarton, mpickering, carter
    
    GHC Trac Issues: `#12045`, `#15362`, `#15592`, `#15788`, `#15793`, `#15795`, `#15797`, `#15799`, `#15801`, `#15807`, `#15816`
    
    Differential Revision: https://phabricator.haskell.org/D5229

To ensure that the code in comment:12 actually typechecks. However, the task of making GeneralizedNewtypeDeriving actually generate this code remains to be done.

comment:20 Changed 9 months ago by RyanGlScott

When writing comment:12, I was originally hopeful that we could scrap all of commit 649e777211fe08432900093002547d7358f92d82—that is, that we could avoid generating any explicit kind signatures and exclusively use visible kind application. Alas, this is not the case. Consider this tortuous example:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE PolyKinds #-}
module Bug where

import Data.Kind
import Data.Proxy

-- type P :: forall {k} {t :: k}. Proxy t
type P = 'Proxy

-- type Wat :: forall a. Proxy a -> *
newtype Wat (x :: Proxy (a :: Type)) = MkWat (Maybe a)
  deriving Eq

-- type Wat2 :: forall {a}. Proxy a -> *
type Wat2 = Wat

-- type Glurp :: * -> *
newtype Glurp a = MkGlurp (Wat2 (P :: Proxy a))
  deriving Eq

This compiles with GHC 8.6.3. However, if I try to switch GeneralizedNewtypeDeriving over to using exclusively visible kind applications, then the code that it generates no longer compiles:

$ ghc/inplace/bin/ghc-stage2 Bug.hs -ddump-deriv
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

==================== Derived instances ====================
Derived class instances:
  instance forall a (x :: Data.Proxy.Proxy a).
           GHC.Classes.Eq a =>
           GHC.Classes.Eq (Bug.Wat x) where
    (GHC.Classes.==)
      = GHC.Prim.coerce
          @(GHC.Maybe.Maybe a_a1wk
            -> GHC.Maybe.Maybe a_a1wk -> GHC.Types.Bool)
          @(Bug.Wat @a_a1wk x_a210
            -> Bug.Wat @a_a1wk x_a210 -> GHC.Types.Bool)
          ((GHC.Classes.==) @(GHC.Maybe.Maybe a_a1wk)) ::
          Bug.Wat @a_a1wk x_a210 -> Bug.Wat @a_a1wk x_a210 -> GHC.Types.Bool
    (GHC.Classes./=)
      = GHC.Prim.coerce
          @(GHC.Maybe.Maybe a_a1wk
            -> GHC.Maybe.Maybe a_a1wk -> GHC.Types.Bool)
          @(Bug.Wat @a_a1wk x_a210
            -> Bug.Wat @a_a1wk x_a210 -> GHC.Types.Bool)
          ((GHC.Classes./=) @(GHC.Maybe.Maybe a_a1wk)) ::
          Bug.Wat @a_a1wk x_a210 -> Bug.Wat @a_a1wk x_a210 -> GHC.Types.Bool
  
  instance GHC.Classes.Eq a => GHC.Classes.Eq (Bug.Glurp a) where
    (GHC.Classes.==)
      = GHC.Prim.coerce
          @(Bug.Wat2 Bug.P -> Bug.Wat2 Bug.P -> GHC.Types.Bool)
          @(Bug.Glurp a_avE -> Bug.Glurp a_avE -> GHC.Types.Bool)
          ((GHC.Classes.==) @(Bug.Wat2 Bug.P)) ::
          Bug.Glurp a_avE -> Bug.Glurp a_avE -> GHC.Types.Bool
    (GHC.Classes./=)
      = GHC.Prim.coerce
          @(Bug.Wat2 Bug.P -> Bug.Wat2 Bug.P -> GHC.Types.Bool)
          @(Bug.Glurp a_avE -> Bug.Glurp a_avE -> GHC.Types.Bool)
          ((GHC.Classes./=) @(Bug.Wat2 Bug.P)) ::
          Bug.Glurp a_avE -> Bug.Glurp a_avE -> GHC.Types.Bool
  

Derived type family instances:



Bug.hs:21:12: error:
    • Couldn't match representation of type ‘a0’ with that of ‘a’
        arising from a use of ‘GHC.Prim.coerce’
      ‘a’ is a rigid type variable bound by
        the instance declaration
        at Bug.hs:21:12-13
    • In the expression:
          GHC.Prim.coerce
            @(Wat2 P -> Wat2 P -> Bool)
            @(Glurp a -> Glurp a -> Bool)
            ((==) @(Wat2 P)) ::
            Glurp a -> Glurp a -> Bool
      In an equation for ‘==’:
          (==)
            = GHC.Prim.coerce
                @(Wat2 P -> Wat2 P -> Bool)
                @(Glurp a -> Glurp a -> Bool)
                ((==) @(Wat2 P)) ::
                Glurp a -> Glurp a -> Bool
      When typechecking the code for ‘==’
        in a derived instance for ‘Eq (Glurp a)’:
        To see the code I am typechecking, use -ddump-deriv
      In the instance declaration for ‘Eq (Glurp a)’
    • Relevant bindings include
        (==) :: Glurp a -> Glurp a -> Bool (bound at Bug.hs:21:12)
   |
21 |   deriving Eq
   |            ^^

Bug.hs:21:12: error:
    • Couldn't match representation of type ‘a1’ with that of ‘a’
        arising from a use of ‘GHC.Prim.coerce’
      ‘a’ is a rigid type variable bound by
        the instance declaration
        at Bug.hs:21:12-13
    • In the expression:
          GHC.Prim.coerce
            @(Wat2 P -> Wat2 P -> Bool)
            @(Glurp a -> Glurp a -> Bool)
            ((/=) @(Wat2 P)) ::
            Glurp a -> Glurp a -> Bool
      In an equation for ‘/=’:
          (/=)
            = GHC.Prim.coerce
                @(Wat2 P -> Wat2 P -> Bool)
                @(Glurp a -> Glurp a -> Bool)
                ((/=) @(Wat2 P)) ::
                Glurp a -> Glurp a -> Bool
      When typechecking the code for ‘/=’
        in a derived instance for ‘Eq (Glurp a)’:
        To see the code I am typechecking, use -ddump-deriv
      In the instance declaration for ‘Eq (Glurp a)’
    • Relevant bindings include
        (/=) :: Glurp a -> Glurp a -> Bool (bound at Bug.hs:21:12)
   |
21 |   deriving Eq
   |            ^^

Ambiguity once again rears its ugly head. You might be tempted to think that we could sprinkle @a somewhere in Wat2 P to resolve the ambiguity, but this is impossible, as all of the type variable binders in Wat2 and P are inferred, making them unavailable for visible kind application. The only way out of this mess is to surround P with an explicit kind signature (i.e., (P :: Proxy a)).

That being said, visible kind application will help us quite a bit, as we can avoid generating explicit kind signatures whenever a tycon only has specified or required type variable binders in its kind. But we'll still need to keep around the hack in commit 649e777211fe08432900093002547d7358f92d82 in the event that there are any inferred type variables.

comment:21 Changed 9 months ago 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:

'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 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.

Last edited 8 months ago by RyanGlScott (previous) (diff)

comment:22 Changed 8 months ago by simonpj

I was originally hopeful that we could avoid generating any explicit kind signatures and exclusively use visible kind application.

Yes I agree with your analysis. Visible kind application (VKA) can only be used for Specified arguments, and user-defined types can have Inferred arguments. So yes, if there are no Inferred ones (a common case) you can use VKA; but not if not. Annoying!

comment:23 Changed 8 months ago by RyanGlScott

Blocked By: 12045 removed

To recap, there are two distinct-but-related tasks here:

  1. Make GND-generated code use VKA to instantiate arguments in specified positions.
  2. Minimize the number of explicit kind signatures generated by GND code by using the approach discussed in comment:21.

Althought (1) and (2) can technically be done independently, it's only the combination of the two that will make it so that the original program in this ticket generate code with no explicit kind signatures adorning its 'Proxy types. I'll look into this approach.

comment:24 Changed 8 months ago by RyanGlScott

Differential Rev(s): Phab:D4264, Phab:D5229Phab:D4264, Phab:D5229, https://gitlab.haskell.org/ghc/ghc/merge_requests/261
Status: newpatch

comment:25 Changed 8 months ago by simonpj

To be clear

So the only remaining issue is MR 261 "Fix #14579 by defining tyConAppNeedsKindSig, and using it"

comment:26 Changed 8 months ago by simonpj

I've read the patch, but I'm commenting here because Trac has greater longevity than code reviews.

You have written a commendably detailed Note -- thank you. Still, it took me a solid hour of head-scratching to really understand it. Here are some thoughts that may (or may not) help to make it clearer.

First, it took me ages reslise that tyConAppNeedsKindSig can be done without knowing the actual arguments to T. Only once I'd realised that did I discover that, sure enough, it doesn't rely on args, only on length args! So I strongly suggest

tyConAppNeedsKindSig
  :: Bool -- ^ Should specified binders count towards injective positions in
          --   the kind of the TyCon?
  -> TyCon
  -> Int    -- Number of args
  -> Bool   -- Does (T t1 .. tn) need a signature
tyConAppNeedsKindSig spec_inj_pos tc n_args = ...

That is, pass the number of args, not the actual args.

That makes it clear that the function could, in principle, live in TyCon. It could even be cached in the TyCon, as a list of Bools or, because of the Inferred/Specified thing, two lists of Bools. But the caching is probably not worth it.

Ok then, my thought process went like this. Given a application T t1 .. tn, does it need a kind signature? Why might it need a kind signature? So that we can fill in any of T's omitted arguments. By an "omitted argument" I mean one that we do not reify expicitly in the HsType. Sometimes the omitted ones are Inferred ones (in typeToHsType); sometimes both Inferred and Specified (in TcSplice); but the key thing is that they don't appear in the HsType.

What do we mean by "fill in"? Suppose

T :: forall {k}. Type -> (k->*) -> k

and we have the application T {j} Int aty. When we convert to HsType we are going to omit the inferred arg {j}. Is it fixed by the other non-inferred args? Yes: if we know the kind of aty :: blah, we'll generate an equality constraint (kappa->*) ~ blah and, assuming we can solve it, that will fix kappa. (Here kappa is the unification variable that we instantiate k with.)

So the question becomes this.

  • Consider the first n args of T: do the kinds of the non-omitted arguments determine the omitted arguments?

We'll only handle the case were the omitted arguments are NamedTCB, so we need to determine a variable. When does a kind "determine" a variable? This is what injectiveVarsOfType computes.

-- (See @Note [Kind annotations on TyConApps]@ in "TcSplice" for an explanation
-- of what an injective position is.)
injectiveVarsOfType :: Type -> FV

Rather than speak of "injective positions" I think of it like this: if a is in injectiveVarsOfType ty then knowing ty fixes, or determines, a. More formally:

  If a is in (injectiveVarsOfType ty)
  and S1(ty) ~ S2(ty)
  then S1(a) ~ S2(a)
  where S1 and S2 are arbitrary substitutions

For example, if F is a non-injective type family, then

  injectiveTyVarsOf( Either c (Maybe (a, F b c)) )  =  {a,c}

(This part about injectiveVarsOfType is not new -- but I'd suggest adding it as comments to the function.)

So we can refine the question:

  • Consider the first n args of T, and each omitted argument i <= n: is argument i a NamedTCB binder b, and does b appear in injectiveVarsOfTtype (k(i+1) .. k(n))? Where kj is the kind of the j'th argument of T.

Much of this is as you have it, except that I'm not lookin at result_kind (in your tyConAppNeedsKindSig. If I can't fill in all omitted arguments, I'll add a kind signature. So for a silly thing like

  T :: forall k. Type -> Type

and the type (T {j} Int), I'll add a kind signature, which actually does no good since k is unused. But it's a silly example. And you'll add one for a different silly example.

  T :: forall k. Type -> F k

which equally does no good.

Nothing here is radically different from what you have. But I find the chain of thought here easier to follow.

comment:27 Changed 7 months ago by RyanGlScott

Resolution: fixed
Status: patchclosed
Test Case: deriving/should_compile/T14579{a}deriving/should_compile/T14579{a,b}

This was finally fixed in e88e083d62389d5c8d082a25395a3d933ab2f03b.

comment:28 Changed 7 months ago by Ryan Scott <ryan.gl.scott@…>

In e88e083/ghc:

Fix #14579 by defining tyConAppNeedsKindSig, and using it
Note: See TracTickets for help on using tickets.