Opened 4 years ago

Closed 3 years ago

#11736 closed feature request (fixed)

Allow unsaturated uses of unlifted types in Core

Reported by: bgamari Owned by: goldfire
Priority: normal Milestone: 8.2.1
Component: Compiler Version: 8.1
Keywords: Typeable, LevityPolymorphism Cc: goldfire, simonpj, sweirich@…, dimitris
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case: typecheck/should_compile/T11736
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

Currently Core Lint checks for unsaturated uses of unlifted types in . These are easily produced in the new type-indexed Typeable scheme. For instance, consider solving for Typeable # (Array# Int):

  • We decompose the application into wanteds Typeable (* -> #) Array# and Typeable * Int
  • We construct dictionaries for both, giving us a term typeRepArray# :: TypeRep (* -> #) Array#

While nothing seems to blow up with this patch,

  • compiler/coreSyn/CoreLint.hs

    diff --git a/compiler/coreSyn/CoreLint.hs b/compiler/coreSyn/CoreLint.hs
    index 99625c9..2c401de 100644
    a b lintType ty@(TyConApp tc tys) 
    10401040  = lintType ty'   -- Expand type synonyms, so that we do not bogusly complain
    10411041                   --  about un-saturated type synonyms
    10421042
    1043   | isUnliftedTyCon tc || isTypeSynonymTyCon tc || isTypeFamilyTyCon tc
     1043  | isTypeSynonymTyCon tc || isTypeFamilyTyCon tc
    10441044       -- Also type synonyms and type families
    10451045  , length tys < tyConArity tc
    10461046  = failWithL (hang (text "Un-saturated type application") 2 (ppr ty))

I otherwise have no reason to believe that this is safe.

Change History (12)

comment:1 Changed 4 years ago by goldfire

I believe this is OK. But we're beyond the scope of any proof I'm aware of for safety -- none have considered unlifted types, to my knowledge.

Simon?

comment:2 Changed 3 years ago by simonpj

Cc: sweirich@… dimitris added

The issue with un-saturated type function is to do with abstraction. What if you had

(/\(a:: * -> *).  blah)  F

where F is a type function. Well bad things, if you can decompose applications of a in blah.

I think that's the only thing that can go wrong with un-saturated unlifted type constructors. What if we said

(/\(a :: * -> *). blah)  Array#

Would that be OK? Well, no: Array# Int is an unlifted type, not *. So it's ill-kinded. But I think this would be fine

(/\(a :: TYPE 'PtrRepLifted -> TYPE 'PtrRepUnlifted). blah)  Array#

Inside blah a variable x :: a Int would be an unlifted type, evaluated call-by-value, just as it should.

Moreover stranger things like

(/\(a :: Type 'PtrRepLifted -> TYPE 'VoidRep). blah) State#

Now inside blah a variable x :: a Int would be an unboxed zero-width void thing. Just right.

In short I think this is absolutely fine. We don't even need to do anything! (I vote for the above patch.)

All we need is someone to come up with a proper account of runtime-rep polymorphism. Kenny?

comment:3 Changed 3 years ago by simonpj

See also #11722

comment:4 Changed 3 years ago by goldfire

What about unboxed tuples? Right now, we have, e.g., (# , #) :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep). TYPE r1 -> TYPE r2 -> TYPE 'UnboxedTupleRep. Of course, UnboxedTupleRep is a lie, because unboxed tuples have all sorts of representations. There is an explicit check for this along with the check for runtime representation polymorphism. With those checks in place, what can go wrong even if we unsaturate unboxed tuples? I think it's OK.

comment:5 Changed 3 years ago by simonpj

Oh bother, yes, you are right about unboxed tuples. What do you mean about "there is an explicit check for this"? You mean: we allow unrestricted un-saturated primitive type constructors, but enforce some other invariant?

There really is a paper here somewhere.

comment:6 Changed 3 years ago by goldfire

See Note [Unboxed tuples in representation polymorphism check] in TcHsSyn.

comment:7 Changed 3 years ago by simonpj

Keywords: Typeable added

comment:8 Changed 3 years ago by simonpj

Keywords: LevityPolymorphism added

comment:9 Changed 3 years ago by bgamari

Owner: set to goldfire

Richard, what is the current status of this?

comment:10 Changed 3 years ago by goldfire

Phab:D2842 will make this possible.

comment:11 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:12 Changed 3 years ago by goldfire

Resolution: fixed
Status: newclosed
Test Case: typecheck/should_compile/T11736
Note: See TracTickets for help on using tickets.