Implement the Unlifted Newtypes proposal
Needs ReviewPublic

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

Details

Summary

This is proposal 13 on the ghc-proposals repo and is fully described there.

Test Plan

Use the unit tests that are provided in this patch

There are a very large number of changes, so older changes are hidden. Show Older Changes
andrewthad updated this revision to Diff 19273.Jan 11 2019, 2:21 PM
  • add test for VTA on coerce

Let's take a step back:

The UnliftedNewtypesDifficultUnification test is meant not to be compiled, right? The idea is that this is an example of the case that's beyond GHC's ability to handle right now. This is to be caught in kcConDecl. And the trouble you're getting is from the call to unravelFamInstPats later in kcConDecl. (By the way, WARNings are printed out only in compilers built with DEBUG enabled, by choosing, e.g., the devel2 settings in your build.mk file.) There is an easy answer here: have decideNewtypeKind fail if the coercion returned from unifyKind is non-reflexive. failWithTc is a good way to do this. Then, we can be assured we never proceed in the troublesome case.

Does that make sense?

andrewthad marked 17 inline comments as done.Jan 11 2019, 3:24 PM

I've made coerce and coerce# the same function. All comments about documentation of coerce# and about the rewrite rules stuff are now moot, so I have marked them complete. All tests now pass. I still need to do a few documentation things. Could @goldfire or @simonpj confirm that what I have done in unravelFamInstPats is sound?

compiler/typecheck/TcInstDcls.hs
692

I realized that UnliftedNewtypesFamilyKindFail2 doesn't actually have a doubled error message. It has two error messages, and they are both meaningful. I think I was incorrect earlier when I said that there was another check that rejected Nat but accepted Constraint.

812–813

This is done now. And the example code you gave has been pulled into UnliftedNewtypesUnassociatedFamily, which passes.

testsuite/tests/typecheck/should_fail/UnliftedNewtypesInfinite.stderr
2

Surprisingly, this error message has become better, although it is somewhat by accident. I think became better as a result of two things:

  • Less omitted checks.
  • Not throwing away the coercion you were concerned about discarding.

I'm guessing that the kind ends up as something like TYPE (a0 |> co1), and the cast gets shot down immediately.

No, I don't think the new implementation of unravelFamInstPats is good: throwing away the cast might cause trouble later on. I still say we shouldn't ever see the case with the coercion, because kcConDecl won't let us. My guess is that you didn't see my earlier comment before posting yours.

andrewthad marked 2 inline comments as done.Jan 11 2019, 3:48 PM

Sorry, I just now saw your comment Richard. I had already made the appropriate change to kcConDecl, but that turned out to not be enough. To see why, consider the trace output I was looking at earlier:

tcDataFamHeader lhs_kind: TYPE (Interpret 'Red)
tcDataFamHeader res_kind: TYPE t_a10U[tau:1]

The lhs_kind and the res_kind as we are working our way through:

do { stupid_theta <- tcHsContext hs_ctxt                            
   ; (lhs_ty, lhs_kind) <- tcFamTyPats fam_tc mb_clsinfo hs_pats    
   ; res_kind <- tc_kind_sig m_ksig                                 
   ; mapM_ (wrapLocM_ (kcConDecl new_or_data res_kind)) hs_cons     
   ; lhs_ty <- checkExpectedKindX pp_lhs lhs_ty lhs_kind res_kind   
   ; return (stupid_theta, lhs_ty, res_kind) }

The weakness is that kcConDecl calls decideNewtypeKind, where unifyKind happily produces a reflexive coercion involving t_a10U[tau:1]. If we passed lhs_kind into kcConDecl instead of res_kind, this wouldn't happen. (That's the benefit of the "don't invent a fresh metavar" approach). So, I worked an extra case into unravelFamInstPats to make it accept a cast. What's strange about what I've done is that now GHC will actually accept the instance if you omit the kind signature, but it rejects it if you include the signature (using GADT syntax on the instance). I'm not sure if this is a bad thing. The only alternative I see to changing unravelFamInstPats is going back to threading lhs_kind through instead of inventing a metavar. That would lead to a failure regardless of whether or not a kind signature was provided.

As a minor aside, I feel that the fall-through case in unravelFamInstPats should be a panic and not a WARN. Returning an empty list as the arguments is almost certain to cause a panic elsewhere, and I think it's preferable to get the panic at the place something went wrong.

And I just missed that one as well. Sorry, my previous comment was in response to the one before your last one, not your last one.

simonpj added a comment.EditedJan 16 2019, 6:11 AM

I'm not sure how WARN gets handled by the compiler, but my suspicion is that the warning is silently discarded. So the question is, what's the right thing to do here?

I'm not following all the details here; but I'm pretty definite that this branch of unravelFamInstPats should fail completely, with some (probably hard to understand) error message.

See Trac Trac #15905 comment:11

libraries/ghc-prim/GHC/Types.hs
285

I agree with Richard: we should make the source code match the wired-in type. So yes, explicit kind variables.

andrewthad updated this revision to Diff 19282.Jan 19 2019, 5:32 PM
  • beef up the UnliftedNewtypesUnassociatedFamily test
  • cross-referencing in more notes about UnliftedNewtypes
  • improve kind unification for newtype instances a little bit, breaks different tests
andrewthad marked 6 inline comments as done.Jan 19 2019, 5:52 PM

@goldfire I've done what you suggested in decideNewtypeKind, and I've reverted the changes I made that let unravelFamInstPats accept casts. However, there's a problem. In tcDataFamHeader, we have two options for what to do when the user doesn't use GADT-style syntax to provide a type signature for a newtype instance. We've discussed these briefly in the comments already. We can invent a fresh metavar, or we can reuse the LHS result kind. Currently, I've reverted to using the LHS result kind, since the problems it has are less bad.

What goes wrong when we invent a fresh metavar? We feed this into kcConDecl and the isTcReflCo check in decideNewtypeKind fails to work because we call it on the wrong thing. By that, I mean that it always succeeds. The coercion is always reflexive since we have unified a fresh metavar with something. Consequently, unravelFamInstPats panics (I've converted the WARN to a panic at Simon's prompting) when we run UnliftedNewtypesDifficultUnification.

What about the other option? Reusing lhs_kind instead of inventing a metavar does work. We get the error we are looking for in UnliftedNewtypesDifficultUnification, but it makes UnliftedNewtypesUnassociatedFamily and several other tests fail. The problem is that this gets rejected:

data family DF :: TYPE (r :: RuntimeRep)
newtype instance DF = MkDF1 Int#
newtype instance DF = MkDF2 Word#

It's rejected with the same error from decideNewtypeKind. I'm not sure why. At the point in time at which we call kcConDecl, I would think we would have:

res_kind: TYPE a0
typeKind typ: TYPE 'IntRep

But clearly this isn't actually the case. I've poked around a little, and I suspect that there is a cast on the outside of res_kind, but I don't understand how and where casts end up in types. I'm stuck on this and would appreciate any insights.

compiler/typecheck/TcTyClsDecls.hs
3250

I've reworded this. All uses of levity polymorphism are allowed.

@goldfire, I believe this might be blocked on you.

For data family instances, there are potentially three kinds that all get unified:

data family DF a :: K1
newtype instance DF Int :: K2 where
  Mk :: (Ty :: K3) -> DF Int

The three are labeled K1, K2, and K3. decideNewtypeKind looks at K3 and K2. (If K2 is missing, I've suggested it should be a metavariable.) But I think we're in trouble also if K1 and K3 have a non-reflexive coercion between them. The non-reflexive coercion would be tacked onto lhs_ty by the call to checkExpectedKindX near the top of tcDataFamHeader. So, in addition to the check in decideNewtypeKind, we need an additional check in tcDataFamHeader, to make sure that (the final) lhs_ty is really a TyConApp. If it isn't, error out with a similar error that you have in decideNewtypeKind.

So, I think the check you have is correct, and it should snag weird non-data-family cases. But we need another check, too.

andrewthad updated this revision to Diff 19285.Jan 25 2019, 9:18 AM
  • add another check for reflexive coercions

That appears to do it. I've added the proposed additional check. It works, and all tests now pass. The error message on UnliftedNewtypesInfinite is better now as well.

One last suggestion below. Then I think we're ready to merge! :)

testsuite/tests/typecheck/should_fail/UnliftedNewtypesDifficultUnification.hs
21

Given the recent discover that this "difficult unification" problem manifests in different ways, I wonder if we can make sure to test all the different ways. To wit:

newtype Quux :: TYPE (Interpret Red) where
  MkQ :: Int# -> Quux
  -- this should test the check in decideNewtypeKind

newtype instance Foo 'Blue :: TYPE WordRep where
  MkFB :: Word# -> Foo 'Blue
  -- not sure, offhand, what will catch this one

type family Interpret2 (x :: Type) :: RuntimeRep where
  Interpret2 Int = IntRep
  Interpret2 Word = WordRep

data family Foo2 (x :: Color) :: TYPE (Interpret x)
newtype instance Foo2 'Red :: TYPE (Interpret2 Int) where
  MkF2R :: Int# -> Foo2 'Red
  -- Now, any two of the three kinds involved need a coercion to connect them

I think these should all work (as in, they are all rejected with a good error message that we're not clever enough to accept them), but it would be good to be sure.

andrewthad updated this revision to Diff 19286.Jan 25 2019, 1:19 PM
  • beef up difficult unification test

I've beefed up the UnliftedNewtypesDifficultUnification test with the examples that @goldfire provided. The errors appear to be as expected.

I've been trying out this patch recently, and one thing keeps nagging me at the back of my mind: should Coercible be heterogeneously kinded? The reason I ask is that the UnliftedNewtypes extension lets you define "kind-changing" newtypes like this one:

newtype T :: Type where
  MkT :: Int# -> T

It initially surprised me to discover that GHC accepts this, but after some thought, this makes sense, since unboxed equality is already heterogeneously kinded, so GHC has no trouble constructing a coercion from Int# :: TYPE IntRep to T :: TYPE LiftedRep in Core.

However, the definition of Coercible doesn't have as much expressive power. That's because this won't kind-check:

:kind Coercible Int# T

<interactive>:1:16: error:
    • Expecting an unlifted type, but ‘T’ is lifted
    • In the second argument of ‘Coercible’, namely ‘T’
      In the type ‘Coercible Int# T’

Oh dear. This happens because Coercible is homogeneously kinded:

λ> :kind Coercible
Coercible :: forall k. k -> k -> Constraint

It's not possible to talk about inter-Coercible things with different kinds, like Int# and T. Similarly, one can't coerce between them at the term level, so it is effectively impossible to derive anything for T using GeneralizedNewtypeDeriving.

But this restriction feels a little artificial, given that unboxed representational equality has the power to be heterogeneously kinded. (It's only boxed representational equality, a.k.a. Coercible, that has this limitation.) Perhaps this is a sign that we should expose something like these to the user?

  • HCoercible :: forall j k. j -> k -> Constraint
  • hcoerce :: forall {j :: RuntimeRep} {k :: RuntimeRep} (a :: TYPE j) (b :: TYPE k). HCoercible a b => a -> b

This is all technically orthogonal to the main patch, so I don't think this necessarily needs to be a blocker. But it is something worth thinking about.

RyanGlScott added a comment.EditedJan 25 2019, 9:01 PM

On second thought, I think my comments in https://phabricator.haskell.org/D4777#151665 might be null and void, since kind-changing newtypes actually appear to be quite bogus. At the very least, permitting them allows me to write the following program, which segfaults:

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE UnliftedNewtypes #-}
module Main (main) where

import Data.Kind
import GHC.Exts

newtype T :: Type where
  MkT :: Double# -> T
  deriving Show

f :: (T, T) -> T -> [T]
f (MkT x##, MkT y##) (MkT z##) =
  [ MkT (x## +## y## +## z##)
  , MkT (x## -## y## -## z##) ]
{-# NOINLINE f #-}

main :: IO ()
main = print $ f (MkT 3.0##, MkT 4.5##) (MkT 39.054325##)
$ ghc3/inplace/bin/ghc-stage2 -O0 Bug.hs
[1 of 1] Compiling Main             ( Bug.hs, Bug.o )
Linking Bug ...

$ ./Bug 
Segmentation fault (core dumped)

HCoercible might be independently desirable for things like coercing between unboxed tuples of different layouts, but kind-changing newtypes definitely aren't the killer app :)

This

newtype T :: Type where
  MkT :: Int# -> T

is an abomination. If this patch accepts it, then the patch is wrong. Which is a shame, because I was about to say that this is ready for merging. @andrewthad, can you check this? I don't have a build of this here.

I agree that T should be rejected. I am surprised that this wasn't caught by an existing test. I've added a test locally, and this patch does indeed currently accept T. I'm looking into this.

Oh, I see the problem. We only call kcLTyClDecl on no_cusk_decls. For cusk_decls, the path we follow never ends up calling unifyNewtypeKind. I think I know where to fix this.

  • start performing kcConDecl checks on the data constructors of types with cusks

I've done the simplest thing to make this work: running kcLTyClDecl on all the cusk_decls. This makes Ryan's data type fail to typecheck, but the error message is the impenetrable:

UnliftedNewtypesMismatchedKind.hs:12:3:
     Kind unification on the result kind a newtype is not yet
      sophisticated enough to handle non-reflexive coercions
      between a (possibly inferred) kind signature and a newtype
      field kind. If this is the result of using a type family in
      the kind, please open a bug report.
      Alternatively, this newtype may have been defined recursively
      in such a way that its inferred kind is infinite. Such
      newtypes are rejected since they are unrepresentable.
     In the definition of data constructor ‘MkT’
      In the newtype declaration for ‘T’

The user deserves a better error message here. I had thought that unifyKind would fail if you tried to unify TYPE 'LiftedRep and TYPE 'IntRep (with an error message along the lines on "Could not unify actual kind X with expected kind Y"). But this doesn't happen.

The naive solution I attempted actually makes a bunch of tests fail. I'm looking into other options.

andrewthad updated this revision to Diff 19288.Jan 26 2019, 2:48 PM
  • kind check the field in a newtype to ensure that it matches what the data type expects

I've nearly got this fixed. I've broken the following:

should_fail/UnliftedNewtypesLevityBinder.run          UnliftedNewtypesLevityBinder [stderr mismatch] (normal)
should_fail/UnliftedNewtypesDifficultUnification.run  UnliftedNewtypesDifficultUnification [stderr mismatch] (normal)
should_run/UnliftedNewtypesIdentityRun.run            UnliftedNewtypesIdentityRun [exit code non-0] (normal)

The first two are degraded error messages. The third is legitimately a problem. What I've done is threaded the result kind from the type constructor into tcConDecl, where I check that the field's type's kind matches it. This snags Ryan's T type but causes a few issues elsewhere.

  • correctly check that the field in an unlifted newtype matches the expected kind

The user deserves a better error message here. I had thought that unifyKind would fail if you tried to unify TYPE 'LiftedRep and TYPE 'IntRep (with an error message along the lines on "Could not unify actual kind X with expected kind Y"). But this doesn't happen.

The problem is that unifyKind returns a coercion if it can't unify the two kinds. Sometimes this coercion is insoluble (e.g., IntRep vs LiftedRep). Sometimes, it's soluble by a type family axiom (the "difficult unification" scenario). We *don't* want to fail eagerly for an insoluble coercion, as we'll fail later, anyway. But we do want to fail eagerly for a soluble coercion, because that coercion will get solved... but then has nowhere to go. The problem is that we can't tell the two apart at this stage.

What we really need to do is to delay looking at the coercion until after the enclosing call to solveEqualities. That sorts out soluble coercions from insoluble ones; it will print nice errors and fail in the monad if any coercions are insoluble. So, really, you want the "we're not clever enough" error to happen only if solveEqualities does not fail (and the coercion is not reflexive). It's not clear to me how much extra plumbing this will entail... but you may need to return the coercion back several functions past the enclosing call to solveEqualities. Conversely, you can just call solveEqualities $ unifyKind ..., as there's no real harm in nested calls to solveEqualities. It's just a bit gross. But then again, the only reason any of this code is getting added is that we don't want to refactor the whole data family mechanism to deal with these new coercions (even though, I'm nearly sure, we could do so if we wanted to).

I'm out of (good) ideas at the moment. This is a place where @simonpj may have some insight, as his code is inescapably elegant.

compiler/typecheck/TcTyClsDecls.hs
501

Remove before committing...

1162

?

So, the problem was that I didn't actually do checks in tcConDecl to make sure that the kind of the type of the field in a newtype matched what was expected. I've added this check for GADT-style declarations. All it requires is checking that the kind of the field matches the kind of res_ty. I've written a note in the code requesting a little feedback.

For non-GADT-style declarations, it's not actually necessary since they never have CUSKs when UnliftedNewtypes is on. This means that kcConDecl gets called on them while type constructors are being kind-checked, and the field's type gets kind-checked there. This is not intuitive, and I should add an explanation of this in a note.

compiler/typecheck/TcTyClsDecls.hs
2462

This is not the right way to do this. Using decideNewtypeKind means that we are doing unification, and we don't actually want unification. We want to say "if these two kinds don't match exactly, fail". What's the function for doing this? (Plus we can give a much better error message this way).

andrewthad updated this revision to Diff 19290.Jan 27 2019, 1:38 PM
  • Remove commented out garbage. Allow solving before checking coercion type in tcConDecl. Include original type in error message.
andrewthad marked 4 inline comments as done.Jan 27 2019, 1:43 PM

@goldfire I've implemented your suggestion. I picked the variant of it that didn't involve nesting solveEqualities. The error message we get for UnliftedNewtypesMismatchedKind is now excellent, especially because we can feed Just ... as the first argument to unifyKind. If @simonpj has a cleaner idea for how to accomplish this check in tcConDecl, I can switch to that. All tests are currently passing. I need to update some of the notes.

I have not been following the details here, since Richard has been On The Job. But it'd be good for me to do so before we finally pull the trigger.

Where can I find a Note that gives an overview of the moving parts?

Thanks

Simon

andrewthad updated this revision to Diff 19291.Jan 28 2019, 9:12 AM
  • improve notes, update notes, rename decideNewtypeKind to unifyNewtypeKind

@simonpj The note with a high-level overview is Implementation of UnliftedNewtypes, found in compiler/typecheck/TcTyClsDecls.hs. I've updated the note to be more accurate.

Also, I wanted to better explain why we cannot handle non-reflexive coercions, but I realized I don't actually understand why. It's something along the lines of "we don't have anywhere to put them", but I don't know where coercions would normally get stashed. If anyone could point me to some documentation that explains what we would normally do with coercions, I could improve the treatment of this subject in the notes.

This wasn't as bad as I was worried about, but I'm curious for Simon's thoughts on the design.

compiler/typecheck/TcTyClsDecls.hs
1096

Is this text still accurate? That is, is there no way now to separate these two possibilities?

2449

This mco should morally have type MCoercion. Not sure if it's worth adding the plumbing to make it so.

2463

This is suspicious. What about RecCon? More generally, I think matching on hs_args here is a bad idea. Is there another way?

andrewthad updated this revision to Diff 19293.Jan 29 2019, 7:33 AM
  • Handle all three types of data constructors when dealing with kind-checking the field of an unlifted newtype
andrewthad updated this revision to Diff 19294.Jan 29 2019, 8:18 AM
  • use MCoercion in tcConDecl with unlifted newtypes
andrewthad added inline comments.Jan 29 2019, 8:53 AM
compiler/typecheck/TcTyClsDecls.hs
1096

To my knowledge, it is still accurate. I don't think there is a good way to separate them. Here are some thoughts. The recursive-kind case happens if the user writes this:

data Foo = Foo (# Int#, Foo #)

It's more difficult to write something with a recursive kind while providing a kind signature. The only way to accomplish do this while providing a kind signature would be:

type KindOf (a :: TYPE k) = k
data Foo :: TYPE ('TupleRep [ 'IntRep, KindOf Foo])
  Foo :: (# Int#, Foo #) -> Foo

However, with or without a kind signature, it's easy to get the non-reflexive coercion case. Just involve a type family in the kind of the field's type. So, trying to use is-there-a-kind-signature vs is-there-not-a-kind-signature wouldn't work for trying to make this distinction.

Maybe there's a way to peek into the coercion and to check for infiniteness. GHC must have some facility for doing this since it can provide a "cannot construct the infinite type ..." error message.

2449

I've made this change. Let me know if the way I did it is what you had in mind. In order to do this, I had to add a panic, since we now no longer have anything to return if the newtype is malformed. However, I think all the right checks for that have happened by the time we get here.

2463

I've fixed this by adding a function in compiler/hsSyn/HsTypes.hs that gives a list of the types of all the fields.

andrewthad marked 6 inline comments as done.Feb 1 2019, 7:53 AM

Marking a few old comments as done.

andrewthad updated this revision to Diff 19295.Feb 2 2019, 6:42 AM
  • Improve outdated notes, cross reference more, quit using panic before validity check happens.
andrewthad marked 5 inline comments as done.Feb 2 2019, 6:48 AM

I fixed a panic that could be triggered by a multi-field type with a CUSK (added a test for this as well). I've added a note about what's going on in tcConDecl. I rewrote the bottom part of the note for kcConDecl since I realized that kcConDecl would never actually be called on the example I gave. I believe I've now cross-referenced all the notes in appropriate places, but let me know if I've missed any of them.

andrewthad added a comment.EditedFeb 6 2019, 8:37 AM

Does anyone have any more feedback on this? I'm not aware of any outstanding issues that need to be addressed.

Sorry, that was supposed to be *have*. Does anyone *have* any more feedback on this?

I certainly don't have any more feedback to give on the patch itself (@goldfire and @simonpj might).

I thought some more about the issue observed in https://phabricator.haskell.org/D4777#151223, and I believe this might be Trac #14331 manifesting in a strange way. Consider this stripped-down version of UnliftedNewtypesGnd:

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
module UnliftedNewtypesGnd where

import GHC.Exts

class LevityEq (a :: TYPE (r :: RuntimeRep))
type LE = LevityEq

Quick question: what is the kind of LE? It might not be what you expect:

$ /opt/ghc/8.6.3/bin/ghci UnliftedNewtypesGnd.hs -XPolyKinds -fprint-explicit-runtime-reps -fprint-explicit-foralls
GHCi, version 8.6.3: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling UnliftedNewtypesGnd ( UnliftedNewtypesGnd.hs, interpreted )
Ok, one module loaded.
λ> :kind LE
LE :: * -> Constraint

Even with -XPolyKinds -fprint-explicit-runtime-reps -fprint-explicit-foralls enabled, GHC treats LE as having kind * -> Constraint! This is because GHC deliberately defaults the RuntimeRep to LiftedRep, intending levity polymorphism to be opt-in. Similarly, if you define type Arr = (->), then GHC will give Arr kind * -> * -> *, not the full, levity polymorphic kind.

That's not to say that all uses of LevityEq will be defaulted like this. If you define this:

type LE2 = (LevityEq :: TYPE IntRep -> Constraint)

Then GHC's all-powerful bidirectional type inference engine will be able to determine that we shouldn't default the RuntimeRep to LiftedRep.

Back to the issue in https://phabricator.haskell.org/D4777#151223. Presumably, you're trying something like this:

class LevityEq (a :: TYPE r) where
  levityEq :: a -> a -> Bool

newtype Foo = Foo Int#
  deriving newtype (LevityEq)

One might think that GHC's bidirectional type inference could figure out that LevityEq should have kind TYPE IntRep -> Constraint here. But as Trac #14331 demonstrates, deriving clauses aren't really typechecked in a very sensible way. Each class in a deriving clause is kind-checked in isolation, and then the resulting kind is unified with the kind of the data type. When kind-checking LevityEq in isolation, GHC has no reason to believe that it should use a levity polymorphic kind, so it defaults it to Type -> Constraint. Later, when we try to unify Type with TYPE IntRep, GHC errors out.

My hunch is that fixing Trac #14331 would also nail this bug (see also Trac #15376, which is a very similarly flavored bug with DerivingVia). Regardless, it would be good to file a ticket about this after the patch has landed, since this provides an interesting test case.

Also, since it looks like most of the in-depth reviewing has quiesced, it would be worth migrating this patch over to GitLab, as it'll need to exist in MR format in order to be merged anyway.

Another ticket to file after this patch lands: it seems that the symptoms of Trac #15883 aren't completely cured by this patch. In particular, this still panics:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE UnliftedNewtypes #-}
module Bug where

import GHC.Exts

newtype Foo rep = MkFoo (forall (a :: TYPE rep). a)
-- Commenting out the instance below makes the panic go away
deriving stock instance Eq (Foo LiftedRep)
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )
ghc-stage2: panic! (the 'impossible' happened)
  (GHC version 8.7.20190208 for x86_64-unknown-linux):
        isUnliftedType
  forall (a :: TYPE rep_av3[sk:1]). a :: TYPE rep_av3[sk:1]
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/utils/Outputable.hs:1159:37 in ghc:Outputable
        pprPanic, called at compiler/types/Type.hs:2292:10 in ghc:Type

I'm not sure if this should count as a bug or not, but you also can't use record selectors with levity polymorphic fields:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE UnliftedNewtypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeInType #-}

module UnliftedNewtypesLevityBinder where

import GHC.Types (RuntimeRep,TYPE,Coercible)

newtype Ident :: forall (r :: RuntimeRep). TYPE r -> TYPE r where
  IdentC :: forall (r :: RuntimeRep) (a :: TYPE r).
            { unIdentC :: a } -> Ident a
$ ghc5/inplace/bin/ghc-stage2 Bug.hs
[1 of 1] Compiling UnliftedNewtypesLevityBinder ( Bug.hs, Bug.o )

Bug.hs:14:15: error:
    A levity-polymorphic type is not allowed here:
      Type: a
      Kind: TYPE r
    In the type of binder ‘unIdentC’
   |
14 |             { unIdentC :: a } -> Ident a
   |               ^^^^^^^^

UnliftedNewtypes have a mildly unpleasant interaction with Template Haskell reification:

λ> newtype Foo :: TYPE IntRep where MkFoo :: Int# -> Foo
λ> putStrLn $(reify ''Foo >>= stringE . show)
TyConI (NewtypeD [] Ghci8.Foo [] Nothing (GadtC [Ghci8.MkFoo] [(Bang NoSourceUnpackedness NoSourceStrictness,ConT GHC.Prim.Int#)] (ConT Ghci8.Foo)) [])

Ideally, the return kind of Foo (TYPE IntRep) would appear as within a Just in the fourth argument to NewtypeD. But instead, Nothing appears, leaving us no way to know what the return kind of the reified Foo type is (I suppose you could reverse engineer this from Int#, but it would be somewhat painful).

I think Template Haskell never bothers to fill in this fourth NewtypeD argument with anything besides Nothing since it is operating under the assumption that since all data types have return kind Type, there's no need to ever include this information. UnlifedNewtypes changes that assumption, so I wonder if we should change Template Haskell to fill in this information if the return kind is something other than Type. Or perhaps we should just always fill it in? It shouldn't hurt anyone to do so, at least.

This patch also exposes a dark corner in :info:

λ> newtype T = MkT Int#
λ> :i T
newtype T :: TYPE 'IntRep = MkT Int#
        -- Defined at <interactive>:5:1

This problem has existed before this patch, however, as the same issue can be observed with unboxed tuples:

λ> :i (##)
data (##) :: TYPE ('GHC.Types.TupleRep '[]) = (##)
        -- Defined in ‘GHC.Prim’

I've filed this as Trac #16299. I believe this can be fixed independently of this patch, so no need to worry about it on your end.

While I'm in the neighborhood, I decided to file Trac #16300 about https://phabricator.haskell.org/D4777#151772, since there is also a path forward to fixing that bug independently of this patch.

Some long overdue responses to Ryan's comments:

I've rebased on top of master and put this patch on gitlab at https://gitlab.haskell.org/ghc/ghc/merge_requests/364. The only regression after rebasing is that test T15801 now has the wrong output. The typechecker rejects the program, but the error message we get is:

Kind unification on the result kind a newtype is not yet
 sophisticated enough to handle non-reflexive coercions
 between a (possibly inferred) kind signature and a newtype
 field kind. If this is the result of using a type family in
 the kind, please open a bug report.
 Alternatively, this newtype may have been defined recursively
 in such a way that its inferred kind is infinite. Such
 newtypes are rejected since they are unrepresentable.
In the definition of data constructor ‘Y’
 In the newtype declaration for ‘Y’

Instead of:

Couldn't match representation of type ‘UnOp op_a -> UnOp b’
                          with that of ‘op_a --> b’
   arising from the superclasses of an instance declaration
In the instance declaration for ‘OpRíki (Op *)’

I'll work through this on gitlab.

Also, concerning the panicing example that Ryan gave:

newtype Foo rep = MkFoo (forall (a :: TYPE rep). a)
-- Commenting out the instance below makes the panic go away
deriving stock instance Eq (Foo LiftedRep)

The definition of Foo should never be accepted to begin with. GHC rejects newtypes with existentially quantified type variables. Consider that the following would be rejected:

newtype Bar = Bar (forall (a :: TYPE 'LiftedRep. a))

Foo should be no different, especially since Foo is just a generalization of Bar.

I had not considered that record selectors didn't work. Technically, it should be possible to make them work since they ultimately desugar to coercions. I'll open a trac ticket for this once unlifted newtypes lands.

Concerning the template haskell interaction, I don't even know to use template haskell, so I have no insight there. But thanks for opening up the ticket!

Also, concerning the panicing example that Ryan gave:

newtype Foo rep = MkFoo (forall (a :: TYPE rep). a)
-- Commenting out the instance below makes the panic go away
deriving stock instance Eq (Foo LiftedRep)

The definition of Foo should never be accepted to begin with. GHC rejects newtypes with existentially quantified type variables. Consider that the following would be rejected:

newtype Bar = Bar (forall (a :: TYPE 'LiftedRep). a)

Foo should be no different, especially since Foo is just a generalization of Bar.

Huh? There are no existentials to be seen here, only a rank-2 type. The argument to MkFoo is required to be polymorphic.

@dfeuer is correct. (You'll notice that if you comment out the deriving stock instance Eq (Foo LiftedRep) part of the program, then it compiles, as it should.)

@RyanGlScott, @simonpj, @goldfire, what should we do with this differential? It looks like there are valuable review comments here that would be good to preserve until the patch is landed but it's not clear to me how close we are to being able to do so.

@RyanGlScott, @simonpj, @goldfire, what should we do with this differential? It looks like there are valuable review comments here that would be good to preserve until the patch is landed but it's not clear to me how close we are to being able to do so.

I've lost track. The primary author is @andrewthad. If poss we should move to GitLab.

This has already been moved to gitlab.