Use the unit tests that are provided in this patch
- rGHC Glasgow Haskell Compiler
Lint Warnings Excuse: fix later
No Unit Test Coverage
- Build Status
Buildable 21724 Build 49703: [GHC] Linux/amd64: Continuous Integration Build 49702: [GHC] OSX/amd64: Continuous Integration Build 49701: [GHC] Windows/amd64: Continuous Integration Build 49700: arc lint + arc unit
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
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.
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.
Looking good! There is one real bug, but I like what I see here. Thanks.
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.
I think newOpenTypeKind would be more accurate here, though I doubt it will make a difference.
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.)
Perhaps change this output to suggest UnliftedNewtypes.
What about a levity-polymorphic newtype? Were those in the proposal?
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.
I'm now doing this, but I'm running into a different problem that I describe in a comment in the main thread.
Yes, I still need to do those. They seem trickier, so I'm trying to get this working in the monomorphic setting first.
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.
|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.
|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.
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
There should also be tests with data/newtype instances.
This is moving along nicely! Thanks for doing it.
Make sure to update this note with the new details.
Style: instead of caseing here, just bind these variables in the function declaration, above.
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
You don't want tyConKind here -- you want tyConResKind. The former includes the parameter kinds, while the latter is just the result kind.
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
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...
Why doesn't this also look for newtype constructor kinds? Newtypes can be written in GADT syntax.
The NewOrData type derives Eq. Just use ==.
You've checked "Done" here, but I don't see that change reflected in the code.
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.
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?
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?
Sorry. I misread this and had only done half of it.
I've not done a full pass. Let me know when this is ready for a more thorough read-through. Thanks!
Yes. The extra constructor is an unused extension.
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.