Implicitly bind kind variables in type family instance RHSes when it's sensible
ClosedPublic

Authored by RyanGlScott on Aug 19 2017, 9:27 PM.

Details

Summary

Before, there was a discrepancy in how GHC renamed type synonyms as
opposed to type family instances. That is, GHC would accept definitions like
this one:

type T = (Nothing :: Maybe a)

However, it would not accept a very similar type family instance:

type family   T :: Maybe a
type instance T = (Nothing :: Maybe a)

The primary goal of this patch is to bring the renaming of type family
instances up to par with that of type synonyms, causing the latter definition
to be accepted, and fixing Trac #14131.

In particular, we now allow kind variables on the right-hand sides of type
(and data) family instances to be implicitly bound by LHS type (or kind)
patterns (as opposed to type variables, which must always be explicitly
bound by LHS type patterns only). As a consequence, this allows programs
reported in Trac #7938 and Trac #9574 to typecheck, whereas before they would
have been rejected.

Implementation-wise, there isn't much trickery involved in making this happen.
We simply need to bind additional kind variables from the RHS of a type family
in the right place (in particular, see RnSource.rnFamInstEqn, which has
undergone a minor facelift).

While doing this has the upside of fixing Trac #14131, it also made it easier to
trigger Trac #13985, so I decided to fix that while I was in town. This was
accomplished by a careful blast of reportFloatingKvs in tcFamTyPats.

Test Plan

./validate

Diff Detail

Repository
rGHC Glasgow Haskell Compiler
Lint
Automatic diff as part of commit; lint not applicable.
Unit
Automatic diff as part of commit; unit tests not applicable.
RyanGlScott created this revision.Aug 19 2017, 9:27 PM
RyanGlScott edited the summary of this revision. (Show Details)Aug 19 2017, 9:38 PM

Ugh, I just realized that there's now a new way to trigger a GHC panic using these changes:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where

class C k where
  data CD :: k -> k -> *

instance C (Maybe a) where
  data CD :: (k -> *) -> (k -> *) -> *
$ ghc4/inplace/bin/ghc-stage2 Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )
ghc-stage2: panic! (the 'impossible' happened)
  (GHC version 8.3.20170818 for x86_64-unknown-linux):
        repSplitTyConApp_maybe
  k_aof[sk:1]
  *
  *
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/utils/Outputable.hs:1138:37 in ghc:Outputable
        pprPanic, called at compiler/types/Type.hs:1123:5 in ghc:Type

I'm not sure if this is a separate issue, or if this is an indication that I'm doing something horribly wrong.

RyanGlScott planned changes to this revision.Aug 21 2017, 8:23 AM

I'm putting this Diff on hold for the time being, since @simonpj suggested a variation on this patch in https://ghc.haskell.org/trac/ghc/ticket/14131#comment:9 that will require some degree of refactoring beforehand.

TODO: Don't use the phrasing "RHS type pattern". Use the phrase "invisible kind pattern" instead.

  • Revise documentation
  • Spruce up comments
RyanGlScott edited the summary of this revision. (Show Details)Aug 29 2017, 3:01 PM

This program:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where

class C k where
  data CD :: k -> k -> *

instance C (Maybe a) where
  data CD :: (k -> *) -> (k -> *) -> *

Now gives a different panic from before:

$ inplace/bin/ghc-stage2 --interactive ../Bug.hs
GHCi, version 8.3.20170818: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( ../Bug.hs, interpreted )
ghc-stage2: panic! (the 'impossible' happened)
  (GHC version 8.3.20170818 for x86_64-unknown-linux):
        getRuntimeRep
  k_a1tx[sk:1] :: k_a1tP[tau:1]
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/utils/Outputable.hs:1138:37 in ghc:Outputable
        pprPanic, called at compiler/types/Type.hs:1982:18 in ghc:Type

Might this possibly be related to Trac #13910? If so, this does make me feel a little better—perhaps this is the work of a separate bug that has been lurking in the shadows (and is now easier to trigger because of these changes).

compiler/typecheck/TcTyClsDecls.hs
1450–1500

@simonpj has expressed some doubts about this design. That is:

  1. In tc_fam_ty_pats, we bind all of the type variables mentioned in LHS type patterns. We return this as the first result in the triple.
  2. In tcFamTyPats, which calls tc_fam_ty_pats, we take all of the type variables mentioned in the type family instance equation (including the kind of the RHS) and compare them to those from the bound variables of the LHS type patterns. If there are any tyvars in the former that aren't in the latter, they should be reported as free-floating.

It's somewhat ugly, since we have to roundtrip through tc_fam_ty_pats to accomplish this. But to be honest, I can't see a better way. We can't do this in tc_fam_ty_pats, since it's parametric in the return type of the kind-checker. In tcFamTyPats, the kind checker returns extra types, which it makes use of to compute the tyvars mentioned in the family instance equation. So tcFamTyPats is the best fit that I can see for the moment.

RyanGlScott added a comment.EditedAug 29 2017, 7:55 PM

There's another awkward problem here. I needed to incorporate @goldfire's fix for Trac #13988 (from here) in order to make some of the tests pass with my changes (for instance, T13877 wouldn't work in the presence of my changes without that fix). But I've now discovered that that fix is also responsible for two other test regressions (causing the Harbormaster build to fail):

Unexpected failures:
   /tmp/ghctest-q8qizyma/test   spaces/./polykinds/T6021.run               T6021 [exit code 0] (normal)
   /tmp/ghctest-q8qizyma/test   spaces/./typecheck/should_fail/T11963.run  T11963 [stderr mismatch] (normal)

I don't quite know off the top of my head how to fix this.

simonpj edited edge metadata.Aug 30 2017, 3:10 AM

One remark; need to look more

compiler/rename/RnSource.hs
727–731

Rather than pass in a function extract_kind_vars_payload, I think it's probably better to compute the payload FreeKiTyVars in the caller and pass it in. That is what is done in (eg) bindHsQTyVars.

Can't do that for rn_payload because it's sensitive to its environment.

RyanGlScott marked an inline comment as done.
  • Compute the RHS kind vars outside of rnFamInstEqn
  • Some scratch work I didn't mean to check in

I now understand why I am experiencing the test failures that I reported in https://phabricator.haskell.org/D3872#109482. It's simply because the patch that I applied to fix Trac #13988 failed to account for recent changes made to rnImplicitBndrs in 0257dacf228024d0cc6ba247c707130637a25580—that is, rnImplicitBndrs now calls checkMixedVars, so it expects its FreeKiTyVars argument to not have its duplicates filtered out beforehand. Fixing this is straightforward enough, but it might be wise to have the fix for Trac #13988 plus my tweaks be its own Diff. I'll work on that.

Rebase on top of D3902

RyanGlScott edited the summary of this revision. (Show Details)Aug 30 2017, 2:54 PM
simonpj accepted this revision.Aug 31 2017, 4:09 AM

Great. I'd like some help with the free-floating kv stuff though

compiler/typecheck/TcTyClsDecls.hs
1488

Add a couple of examples (in a Note) of what will and will not trigger this error. The general note of free-floating variables isn't enough for family instances I think.

In the Note I think it's helpful to make explicit what the final kind/type parameters of the family are, and what the final kind/type patterns of the instance are. (I.e. don't leave the kind patterns implicit!)

This revision is now accepted and ready to land.Aug 31 2017, 4:09 AM

PS: in appropriate notes, refer to the Trac tickets mentioned in the summary. It's invaluable to from a Note to the discussion on a ticket. After all, since it's a ticket it's not that obvious!

Ugh, I just realized that there's now a new way to trigger a GHC panic using these changes:

Make a ticket for this when you commit. (What did it do before your changes?)

RyanGlScott marked an inline comment as done.
  • Expand Note

Ugh, I just realized that there's now a new way to trigger a GHC panic using these changes:

Make a ticket for this when you commit. (What did it do before your changes?)

Before this commit, it wasn't possible to even compile that code, since it would fail due to Trac #14131 itself:

../Foo.hs:11:15: error: Not in scope: type variable ‘k’
   |
11 |   data CD :: (k -> *) -> (k -> *) -> *
   |               ^

../Foo.hs:11:27: error: Not in scope: type variable ‘k’
   |
11 |   data CD :: (k -> *) -> (k -> *) -> *
   |                           ^

Hence why I think that these changes exposed a different bug, since it didn't seem possible to go down that code path before.

compiler/typecheck/TcTyClsDecls.hs
1488

I've added some more examples to Note [Free-floating kind vars] in TcHsType.

goldfire edited edge metadata.Sep 3 2017, 5:40 PM

Simon seems to taking charge on reviewing this. Shout if you want another set of eyes.

I'm a bit lost as to where we are on this one now.

I'm a bit lost as to where we are on this one now.

The only change since your last comment is that I've expanding Note [Free-floating kind vars] in TcHsType with more examples specific to type families. If you find the documentation there to be adequate, I'd say this is good to go.

As a side note, I've thought more about free-floating kind variable analysis in general, and there's something about it all that makes me it a bit uncomfortable—namely, that H98 datatypes and GADTs are treated inconsistently. In particular, this is rejected, since k is free-floating:

data Foo = MkFoo (forall (a :: k). Proxy a)

But this seemingly equivalent definition is accepted, as k is implicitly quantified as an existential type variable!

data Foo where MkFoo :: (forall (a :: k). Proxy a) -> Foo

Perhaps this is suited to its own ticket, though.

RyanGlScott updated the Trac tickets for this revision.Sep 5 2017, 8:24 AM
This revision was automatically updated to reflect the committed changes.

As a side note, I've thought more about free-floating kind variable analysis in general, and there's something about it all that makes me it a bit uncomfortable—namely, that H98 datatypes and GADTs are treated inconsistently. In particular, this is rejected, since k is free-floating:

data Foo = MkFoo (forall (a :: k). Proxy a)

But this seemingly equivalent definition is accepted, as k is implicitly quantified as an existential type variable!

data Foo where MkFoo :: (forall (a :: k). Proxy a) -> Foo

This is by design. Kind variables can be quantified only at a few places -- at a :: and in tycon declarations for example. H98 has no :: where the kind can be bound, whereas the GADT constructor does. Perhaps this design could be improved, but it's not an implementation bug.

This is by design. Kind variables can be quantified only at a few places -- at a :: and in tycon declarations for example. H98 has no :: where the kind can be bound, whereas the GADT constructor does. Perhaps this design could be improved, but it's not an implementation bug.

I suppose I should be more specific: H98 syntax can implicitly quantify kind variables if you don't spell them out. For instance:

{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}

import Data.Proxy

data Foo = MkFoo (forall a. Proxy a)

This implicitly quantifies the invisible kind of a (call it k) as an existential type variable. So we have a scenario where kinds get implicitly bound when left off, but not when written out!

In D3872#110044, @RyanGlScott wrote:

H98 syntax can implicitly quantify kind variables if you don't spell them out.

Yuck. I think that's a bug. @simonpj, what do you think of that example? (The kind is currently implicitly quantified as existential in the constructor: MkFoo :: forall k. (forall (a :: k). Proxy k a) -> Foo.)

It turns out that this example was reported as a Trac ticket once upon a time: Trac #7873. (The resolution was to keep the yucky behavior.)

It turns out that this example was reported as a Trac ticket once upon a time: Trac #7873. (The resolution was to keep the yucky behavior.)

However, kind quantification has been revised since that ticket, moving around where implicit kind quantification takes place.

Summarising:

data Foo = MkFoo (forall a. Proxy a)

is accepted with

MkFoo :: forall {k}. (forall (a :: k). Proxy k a) -> Foo

But

data Foo = MkFoo (forall (a :: k). Proxy a)

is rejected with

Foo.hs:7:1: error:
    * Kind variable `k' is implicitly bound in data type
      `Foo', but does not appear as the kind of any
      of its type variables. Perhaps you meant
      to bind it explicitly somewhere?
      Type variables with inferred kinds: (k :: *)
    * In the data declaration for `Foo'
  |
7 | data Foo = MkFoo (forall (a :: k). Proxy a)
  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

I agree this difference is bizarre. But the "accepted" version is also bonkers. The k is right at the top of the type, but doesn't appear in the result type, so it's an existential... it makes my head hurt. If it is to be accepted, surely it should be

MkFoo :: (forall {k} (a :: k). Proxy k a) -> Foo

My current thought: we should accept both or reject both; but if we accept both it'd better be with implcit kind quantification for each kind argument separately.

This is surprisingly tricky. I suggest opening a ticket.

This is surprisingly tricky. I suggest opening a ticket.

I've opened Trac #14198 for this.