Opened 3 years ago

Closed 3 years ago

Last modified 3 years ago

#12809 closed bug (fixed)

TYPE 'UnboxedTupleRep is still a lie

Reported by: goldfire Owned by: goldfire
Priority: normal Milestone:
Component: Compiler Version: 8.0.1
Keywords: LevityPolymorphism Cc: RyanGlScott, Iceland_jack
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: typecheck/should_run/T12809
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

The new scheme for describing kinds of types with values with TYPE :: RuntimeRep -> Type is a large improvement on the old way of using kind # for all unlifted types. In particular, the new scheme differentiates between the kind of Int# and Float#, for example, because these have different calling conventions. This is Good.

But there is still a lie left in the whole scheme: UnboxedTupleRep, which covers all unboxed tuples. Of course, unboxed tuples of different arities and contents have different calling conventions, so these should be distinguished at the kind level.

Simon and I have cooked up a new scheme to handle this, summarized in these definitions:

TYPE :: RuntimeRep -> Type    -- highly magical, just as before
type RuntimeRep = [UnaryRep]  -- this bit is the new part
data UnaryRep = PtrRepLifted  -- like the old RuntimeRep type
              | PtrRepUnlifted
              | IntRep
              | ...
type Lifted = '[PtrRepLifted]  -- a very common case
type Type = TYPE Lifted        -- good old Type

The UnaryRep type is the big sum of all possible representations, just like the RuntimeRep of today. It drops VoidRep and UnboxedTupleRep, however.

The interpretation of this is that the kinds now include a list of unary representation forms. A "unary representation" corresponds to what we might expect to store in one machine register at runtime. Unboxed tuples naturally have a variable number of associated unary reps: this is precisely what an unboxed tuple means. It also baldly states that the unary unboxed tuple is identical (at runtime) to the thing in the tuple (which is correct) and also allows us to remove the runtime distinction between (# #) and Void#, which now both have kind TYPE '[]. (Indeed, perhaps we should just say type Void# = (# #).)

This will not be backward compatible with GHC 8.0. But I'm OK with this, as any user access to these features requires importing internal modules, and it seems quite painful to try to come up with a migration story here for an experimental feature.

Patch will be written this weekend, with any luck.

Change History (8)

comment:1 Changed 3 years ago by RyanGlScott

Cc: RyanGlScott added

If this is implemented, will it obviate the error-checks needed to fix things like #11723, #11724, #11509, etc.?

comment:2 Changed 3 years ago by monoidal

Out of curiosity, what about unboxed sums? Is the TYPE 'UnboxedSumRep also a lie?

comment:3 Changed 3 years ago by Iceland_jack

Cc: Iceland_jack added

comment:5 Changed 3 years ago by simonpj

Keywords: LevityPolymorphism added

comment:6 Changed 3 years ago by Richard Eisenberg <rae@…>

In e7985ed2/ghc:

Update levity polymorphism

This commit implements the proposal in
https://github.com/ghc-proposals/ghc-proposals/pull/29 and
https://github.com/ghc-proposals/ghc-proposals/pull/35.

Here are some of the pieces of that proposal:

* Some of RuntimeRep's constructors have been shortened.

* TupleRep and SumRep are now parameterized over a list of RuntimeReps.
* This
means that two types with the same kind surely have the same
representation.
Previously, all unboxed tuples had the same kind, and thus the fact
above was
false.

* RepType.typePrimRep and friends now return a *list* of PrimReps. These
functions can now work successfully on unboxed tuples. This change is
necessary because we allow abstraction over unboxed tuple types and so
cannot
always handle unboxed tuples specially as we did before.

* We sometimes have to create an Id from a PrimRep. I thus split PtrRep
* into
LiftedRep and UnliftedRep, so that the created Ids have the right
strictness.

* The RepType.RepType type was removed, as it didn't seem to help with
* much.

* The RepType.repType function is also removed, in favor of typePrimRep.

* I have waffled a good deal on whether or not to keep VoidRep in
TyCon.PrimRep. In the end, I decided to keep it there. PrimRep is *not*
represented in RuntimeRep, and typePrimRep will never return a list
including
VoidRep. But it's handy to have in, e.g., ByteCodeGen and friends. I can
imagine another design choice where we have a PrimRepV type that is
PrimRep
with an extra constructor. That seemed to be a heavier design, though,
and I'm
not sure what the benefit would be.

* The last, unused vestiges of # (unliftedTypeKind) have been removed.

* There were several pretty-printing bugs that this change exposed;
* these are fixed.

* We previously checked for levity polymorphism in the types of binders.
* But we
also must exclude levity polymorphism in function arguments. This is
hard to check
for, requiring a good deal of care in the desugarer. See Note [Levity
polymorphism
checking] in DsMonad.

* In order to efficiently check for levity polymorphism in functions, it
* was necessary
to add a new bit of IdInfo. See Note [Levity info] in IdInfo.

* It is now safe for unlifted types to be unsaturated in Core. Core Lint
* is updated
accordingly.

* We can only know strictness after zonking, so several checks around
* strictness
in the type-checker (checkStrictBinds, the check for unlifted variables
under a ~
pattern) have been moved to the desugarer.

* Along the way, I improved the treatment of unlifted vs. banged
* bindings. See
Note [Strict binds checks] in DsBinds and #13075.

* Now that we print type-checked source, we must be careful to print
* ConLikes correctly.
This is facilitated by a new HsConLikeOut constructor to HsExpr.
Particularly troublesome
are unlifted pattern synonyms that get an extra void# argument.

* Includes a submodule update for haddock, getting rid of #.

* New testcases:
  typecheck/should_fail/StrictBinds
  typecheck/should_fail/T12973
  typecheck/should_run/StrictPats
  typecheck/should_run/T12809
  typecheck/should_fail/T13105
  patsyn/should_fail/UnliftedPSBind
  typecheck/should_fail/LevPolyBounded
  typecheck/should_compile/T12987
  typecheck/should_compile/T11736

* Fixed tickets:
  #12809
  #12973
  #11736
  #13075
  #12987

* This also adds a test case for #13105. This test case is
* "compile_fail" and
succeeds, because I want the testsuite to monitor the error message.
When #13105 is fixed, the test case will compile cleanly.

comment:7 Changed 3 years ago by goldfire

Resolution: fixed
Status: newclosed
Test Case: typecheck/should_run/T12809

No more lies! Only truthiness from now on.

comment:8 Changed 3 years ago by RyanGlScott

Thanks, goldfire!

I'll try to revisit the fixes for #11723, #11724, and #11509 at some point. I believe they all put in checks that forbade the use of UnboxedTupleRep and UnboxedSumRep in deriving because it was assuming the inadequacies of the old system for levity polymorphism, but now that's it's overhauls, I don't believe those checks are required anymore.

Note: See TracTickets for help on using tickets.