Opened 3 years ago

Closed 3 years ago

#12973 closed bug (fixed)

No levity-polymorphic arguments

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

Description

As discussed in our draft paper on levity polymorphism, you cannot have a levity-polymorphic argument. Here is an example:

{-# LANGUAGE RebindableSyntax, TypeInType, ExplicitForAll #-}

module Bug where

import qualified Prelude as P
import GHC.Exts

class Num (a :: TYPE r) where
  (+) :: a -> a -> a
  fromInteger :: P.Integer -> a

foo :: forall (a :: TYPE r). Num a => a
foo = 3 + 4

HEAD panics in kindPrimRep, but the code should be rejected.

Change History (5)

comment:1 Changed 3 years ago by goldfire

This is subtler than we realized in the paper. Consider

data (a :: k1) :~~: (b :: k2) where
  HRefl :: a :~~: a

bar :: forall (r :: RuntimeRep) (a :: TYPE r). a :~~: Int -> a
bar HRefl = 3 + 4

Well? What do we think? Is that good or bad? It depends on how GHC inserts the coercions. :(

In HEAD, this panics as written. But if I make the RHS to be 3 + 4 :: Int, then it compiles. The question is whether GHC chooses to desugar the RHS to

(+) @a (fromInteger @a 3) (fromInteger @a 4)

or to

(+) @Int (fromInteger @Int 3) (fromInteger @Int 4) |> co

where co can cast from Int to a. The former is much more obvious in this case, but there's nothing actually wrong about the latter. And I'm sure some scenarios won't be as easy to guess what might happen under the hood.

I think this question is more fundamental than just predictable type inference. For example, is this Core well typed: f (x |> co) What if the left-hand type of co is levity polymorphic? What if the right-hand type is? And what happens in the code generator when it sees such a construct? Presumably, it just ignores casts. This tells us that we care about co's left-hand type. But now what if we substitute x :-> y |> co'. If y looks levity-polymorphic while x does not, this substitution has brought us from a well typed program to an ill typed one. Disaster!

I thus go to sleep troubled. Hopefully wisdom strikes in the night, either in my sleep or on this ticket.

comment:2 Changed 3 years ago by goldfire

Something struck in the night. Time will tell if it was wisdom.

The idea is this: the representation choice of an argument is properly a property of the function, not the argument. So, in Core at least, when examining f (x |> co), we care about the argument type of f, not that of x or co. (Of course, if it's well typed, the right-hand type of co matches the argument type of f.) So the Core levity polymorphism check does not look under coercions. However, this means that the code generator must also not look under coercions when compiling arguments (that is, when converting to ANF). Does this already happen? Perhaps, as I look at CorePrep.

But then is this respected further on down the compilation chain? (That is, how are coerced arguments handled in STG and beyond?) I do see that we simply drop casts in CoreToStg; no surprise there. And I suppose that, at this point, we're already in ANF form, so any arguments are bound to ids that have the right type.... so maybe it's all OK. I'd love confirmation.

Even if this all works out at the Core level, we still have a type inference challenge. Maybe the solution is simply to punt, arguing that the user is playing with fire and so sometimes will get burnt. By "punt" here, I mean that GHC just has a little unpredictability in this area. (Indeed, this is already the case, as discussed in the paper around trouble generalizing levity variables.)

Maybe this is the real wisdom here: keep calm, carry on, and hope it all works.

comment:3 Changed 3 years ago by Iceland_jack

Cc: Iceland_jack added

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

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