Summary: Implement the Unlifted Newtypes proposal. This is proposal 13 on the ghc-proposals repo and is fully described there.
Needs ReviewPublic

Authored by andrewthad on Jun 3 2018, 8:01 AM.

Details

Reviewers
goldfire
bgamari
simonpj
Trac Issues
#15219
#1311
Test Plan

Use the unit tests that are provided in this patch

Diff Detail

andrewthad created this revision.Jun 3 2018, 8:01 AM
andrewthad updated this revision to Diff 16679.Jun 3 2018, 8:03 AM

Diff against the correct commit.

All I've done so far is allow newtypes (vanilla or GADT-style) over types that are not kinded TYPE 'LiftedRep. Things from the proposal that I still need to implement and test are:

  • unlifted data families
  • newtype over a levity-polymorphic type variable
  • make sure there's a good error message for types that would have an infinite kind
  • make sure coerce works with these
andrewthad updated this revision to Diff 16680.Jun 3 2018, 9:31 AM
  • improve test for UnliftedNewtypes
  • add test for gadt without kind sig
andrewthad updated this revision to Diff 16693.Jun 4 2018, 6:50 AM
  • generate fresh kind variable for newtypes

I'd like some confirmation that I'm on the right path. This code doesn't currently work for anything except GADTs with a kind signature, and even for those I think it accepts bad programs. I'm trying to support kind inference when the user writes something like:

newtype Foo = Foo Int#

In getInitialKind, I've made it so that newtypes don't get kinded TYPE LiftedRep. Instead, they get a fresh kind variable. The steps of kcTyClGroup are:

  • generate kind variables with getInitialKinds
  • call solveEqualities
  • generalize for poly kinds

I'm thinking that I should be able to tweak solveEqualities to unify the fresh kind variable on the newtype with the kind of the type inside of it. Does this seem like it will work?

Maybe I just need to modify kcTyClDecl. One thing that isn't clear to me is how to tell GHC that I want to attempt to unify two kinds. I think that should be all I need to add to kcTyClDecl.

andrewthad updated this revision to Diff 16694.Jun 4 2018, 9:31 AM
  • tried to get the fresh kind variable to unify with the kind of the type inside the newtype. it did not work correctly.

I've added a function decideNewtypeKinds. I thought it would eliminate the kind variables introduced by newMetaKindVar (by unifying it with the kind of the type inside of the newtype), but it does not work as I expected.

goldfire requested changes to this revision.Jun 5 2018, 3:28 PM
goldfire added a reviewer: simonpj.

Looking good! There is one real bug, but I like what I see here. Thanks.

compiler/typecheck/TcTyClsDecls.hs
487

This won't work. These initial_tcs haven't done any processing of datacons yet, so you won't be able to look them up. That's OK, though -- just have the initial kind for a newtype end with a kind variable instead of liftedTypeKind, and we can sort it out later.

Where later is in kcConDecl. Have that take the name of the datatype. It can retrieve the tycon via kcLookupTcTyCon. Then, you can check whether it's a newtype. If it is, then unify the kind with that of the representation type.

628

I think newOpenTypeKind would be more accurate here, though I doubt it will make a difference.

1960–1963

I think it would be OK to use tcHsOpenType here even for non-newtypes. I can't think of anything that would go wrong. (But maybe the testsuite has a different opinion.)

2780–2784

Perhaps change this output to suggest UnliftedNewtypes.

testsuite/tests/typecheck/should_fail/UnliftedNewtypesFail.hs
7

Good test!

testsuite/tests/typecheck/should_run/UnliftedNewtypesRun.hs
2

What about a levity-polymorphic newtype? Were those in the proposal?

This revision now requires changes to proceed.Jun 5 2018, 3:28 PM
andrewthad updated this revision to Diff 17087.Mon, Jun 25, 9:43 AM
  • try unifying newtype kinds differently
andrewthad marked 4 inline comments as done.Mon, Jun 25, 9:56 AM

I'm now getting the following error in stage2:

compiler/hsSyn/HsTypes.hs:413:1: error:
    You have written a *complete user-suppled kind signature*,
    but the following variable is undetermined: k0 :: *
    Perhaps add a kind signature.
    Inferred kinds of user-written variables:
    |
413 | newtype HsIPName = HsIPName FastString
    | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...

I think this is because kcLHsQTyVars gets called before the kind variable has a chance to unify with the kind of the type in the data constructor. I'm not sure what to do about this.

compiler/typecheck/TcTyClsDecls.hs
487

I'm now doing this, but I'm running into a different problem that I describe in a comment in the main thread.

testsuite/tests/typecheck/should_run/UnliftedNewtypesRun.hs
2

Yes, I still need to do those. They seem trickier, so I'm trying to get this working in the monomorphic setting first.

andrewthad marked an inline comment as done.Mon, Jun 25, 9:57 AM
andrewthad updated this revision to Diff 17187.Wed, Jul 4, 8:46 AM
  • suppress undetermined-type-variable when UnliftedNewtypes is on. still not working, but closer

I've made some more changes. There was a check for undetermined type variables that I had to disable to get past the error I mentioned previously. However, now, when the test suite is run, GHC think that Foo, Darth, and Pat have kind TYPE 'LiftedRep. So, somewhere in the typechecker, those kind variables are getting unified with TYPE 'LiftedRep before I get a chance to unify them with the kind of the underlying type. Alternatively, it's possible that my attempt to unify them with the kind of the underlying type doesn't actually work and they get unified with TYPE 'LiftedRep at some point after this.

I've made a suggestion in the line comment below -- let's try that before getting too deep into debugging these problems, as it might fix them all. I hate CUSKs.

compiler/typecheck/TcHsType.hs
1603 ↗(On Diff #17187)

Just looking for the extension is the wrong check, because someone might enable the extension but then trigger this in unrelated work. Regardless, this has been updated in master since you've started, so you may want to rebase before worrying too much more about this.

As I think about this more, you'll just run into other problems. Really, what I think you need is to change the definition of CUSK. A CUSK should mean that GHC can look only at the type declaration head (not the body) and find its kind. Without -XUnliftedNewtypes, data and newtypes have CUSKs when all their type variables have kind annotations -- there is no need for a return kind signature (because the return kind is always Type). But once we have -XUnliftedNewtypes, then we do need a return kind for newtypes.

Thus, I think the answer is: When -XUnliftedNewtypes is enabled, newtypes need a return kind annotation to have a CUSK. Then, I think all these problems will melt away. See HsDecls.hsDeclHasCusk, which will now need access to whether -XUnliftedNewtypes is enabled.

A CUSK should mean that GHC can look only at the type declaration head (not the body) and find its kind.

I strongly agree with this principle.

Thus, I think the answer is: When -XUnliftedNewtypes is enabled, newtypes need a return kind annotation to have a CUSK.

That looks right to me.

andrewthad added inline comments.Wed, Jul 4, 12:17 PM
compiler/typecheck/TcHsType.hs
1603 ↗(On Diff #17187)

I figured that I would have to do more than just a check for the extension, But I was trying to see if I could just get the tests working at all first. I thought it was weird that these types were being counted as having cusks, but your comments explains what’s going on. I’ll change the cusk check as you’ve suggested.

andrewthad added inline comments.Thu, Jul 5, 8:03 AM
compiler/typecheck/TcHsType.hs
1603 ↗(On Diff #17187)

This is now mostly completed.

andrewthad updated this revision to Diff 17199.Thu, Jul 5, 8:09 AM

Rebase and stop inferring cusk when unlifted newtypes are used without a kind signature

andrewthad added inline comments.Thu, Jul 5, 8:13 AM
compiler/typecheck/TcTyClsDecls.hs
773

I think this might be causing a panic. I'm now getting:

ghc-stage1: panic! (the 'impossible' happened)
  (GHC version 8.7.20180705 for x86_64-unknown-linux):
        kcLookupTcTyCon
  Type constructor ‘URec’
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/utils/Outputable.hs:1164:37 in ghc:Outputable
        pprPanic, called at compiler/typecheck/TcHsType.hs:2102:27 in ghc:TcHsType
simonpj updated the Trac tickets for this revision.Mon, Jul 9, 3:07 AM

There should also be tests with data/newtype instances.

This is moving along nicely! Thanks for doing it.

compiler/rename/RnSource.hs
1515

Make sure to update this note with the new details.

1517

Style: instead of caseing here, just bind these variables in the function declaration, above.

1519

Style: This is more intricate than it needs to be. Might I suggest

unlifted_newtypes <- xoptM LangExt.UnliftedNewtypes
let non_cusk_newtype
      | NewType <- new_or_data = unlifted_newtypes && isNothing kind_sig
      | otherwise = False
compiler/typecheck/TcTyClsDecls.hs
585

You don't want tyConKind here -- you want tyConResKind. The former includes the parameter kinds, while the latter is just the result kind.

628

I had a hard time parsing this for a moment with the nested cases. Might I suggest

case m_sig of
  Just ksig -> ...
  Nothing
    |  NewType <- new_or_data
    ,  unlifted_newtypes
    -> newOpenTypeKind

    |  otherwise
    -> new liftedTypeKind
773

It would be helpful to know the input code that triggered the panic. My guess is that URec is a data family, and this panic happens on an instance: kcConDecl is called when inferring the kind of a data/newtype instance (as well as for normal datatypes). But kcLookupTcTyCon doesn't work for data/newtype instances. And indeed it shouldn't -- the behavior here would be wrong in these cases.

I think kcConDecl should return a TcM TcKind, which, if we have -XUnliftedNewtypes and the definition is for a newtype, can then be unified with the return kind of the newtype. Doing this unification is easy enough in kcTyClDecl, but is awkward in kcDataDefn. I'm not sure what the best design here would be, actually. Perhaps return the constructor kind in the Nothing case for mb_kind and unify the typechecked signature with the constructor kind in the Just case. But I'm not quite sure where to stash the coercion that comes from unification...

775–776

Why doesn't this also look for newtype constructor kinds? Newtypes can be written in GADT syntax.

1189

The NewOrData type derives Eq. Just use ==.

1967

You've checked "Done" here, but I don't see that change reflected in the code.

andrewthad added inline comments.Wed, Jul 11, 7:32 AM
compiler/typecheck/TcTyClsDecls.hs
1488

This addition is what caused the panic I mentioned in another comment. I don't think I should have even added this.

I've realized that I must horribly misunderstand what exactly isNewTyCon does. Either that, or I've messed up something else pretty badly. In the test suite, recall that I have a newtype named Darth:

newtype Darth = DarthC Int#

Locally, I've rigged decideNewtypeKind to give me some debug information:

decideNewtypeKind :: [TcType] -> TcTyCon -> TcM ()

decideNewtypeKind data_con_ty_args tc

| True = panic ("not reached at all " 
    ++ getOccString (tyConName tc) ++ " " ++ show (isNewTyCon tc) ++ " "
    ++ show (isDataTyCon tc) ++ " " 
    ++ show (isUnliftedTyCon tc) ++ " "                             
    ++ show (isPrimTyCon tc) ++ " "
    ++ show (isVanillaAlgTyCon tc) ++ " "                           
    ++ show (isFunTyCon tc) ++ " " 
    ++ show (isProductTyCon tc) ++ " "
    ++ show (isAbstractTyCon tc) ++ " "                             
    ++ show (isFamilyTyCon tc) ++ " " 
    ++ show (isOpenFamilyTyCon tc) ++ " "                           
    ++ show (isTypeFamilyTyCon tc) ++ " " 
    ++ show (isOpenTypeFamilyTyCon tc) ++ " "                       
    ++ show (isDataFamilyTyCon tc) ++ " "                           
    ++ show (isTcTyCon tc) ++ " "
    ++ show (isImplicitTyCon tc) ++ " "                             
    ++ show (isTcLevPoly tc) ++ " "
    ++ show (isPromotedDataCon tc) ++ " "                           
    ++ show (isKindTyCon tc) ++ " "
    ++ show (isBoxedTupleTyCon tc) ++ " "                           
    ++ show (length data_con_ty_args))

This is what get when I run the test suite:

ghc-stage2: panic! (the 'impossible' happened)
  (GHC version 8.7.20180705 for x86_64-unknown-linux):
        not reached at all Darth False False False False False False False False False False False False False True False False False False False 1

There's only on True in there, and GHC doesn't think that Darth is a newtype constructor. Is this expected?

Yes. The TcTyCons used during kind-checking don't carry all the information about a declaration. In particular, they don't store newtype-ness. They could, if it's necessary, but I'm not yet convinced it is.

Good to know. Locally, I've changed decideNewtypeKind to not use isNewTyCon, and this looks like its working now. I've still got a ways to go, but at least vanilla newtypes look like they are behaving correctly.

andrewthad added inline comments.Thu, Jul 12, 6:59 AM
compiler/rename/RnSource.hs
1517

This leads to a non-exhaustive pattern match, since there are data constructors other than HsDataDefn. Is it alright to just panic if we get a different data constructor?

andrewthad updated this revision to Diff 17279.Thu, Jul 12, 7:16 AM
  • UnliftedNewtypes works on vanilla newtypes and GADT-style newtypes
andrewthad marked 4 inline comments as done.Thu, Jul 12, 7:19 AM
andrewthad added inline comments.
compiler/typecheck/TcTyClsDecls.hs
773

I have fixed the panic by removing code that I mistakenly added elsewhere. However, I still need to address the issue of returning the kind so that the unification can be done elsewhere. I have no idea how coercions are stored. Can you point me to a note that explains that?

1967

Sorry. I misread this and had only done half of it.

andrewthad marked an inline comment as done.Thu, Jul 12, 7:20 AM

The tests are now passing. I still need to deal with type families, data families, and levity-polymorphic newtypes.

I've not done a full pass. Let me know when this is ready for a more thorough read-through. Thanks!

compiler/rename/RnSource.hs
1517

Yes. The extra constructor is an unused extension.

compiler/typecheck/TcTyClsDecls.hs
773

This will be hard, I fear, but the missing case will be very obscure, triggered only when a data family return kind uses a type family and someone is trying to build a newtype instance.

Here's what to do: the call to unifyType returns a coercion. Check whether that coercion is reflexive (use isTcReflCo), and if it is, discard it. If it's not, issue an error saying that the feature isn't yet implemented.