diff options
| author | Simon Peyton Jones <simonpj@microsoft.com> | 2017-03-08 09:39:29 +0000 |
|---|---|---|
| committer | Simon Peyton Jones <simonpj@microsoft.com> | 2017-03-08 11:04:09 +0000 |
| commit | 8e053700f9357c1b9030c406130062795ae5015c (patch) | |
| tree | 9263690bcdfcef449acdccca0048743ec0d79631 /compiler/coreSyn/CoreSyn.hs | |
| parent | bd6681713a603bcdcf2fde9aab85b17183eefb0b (diff) | |
| download | haskell-8e053700f9357c1b9030c406130062795ae5015c.tar.gz | |
Join points can be levity-polymorphic
It's ok to have a levity-polymorphic join point, thus
let j :: r :: TYPE l = blah
in ...
Usually we don't allow levity-polymorphic binders, but join points
are different because they are not first class. I updated the
invariants in CoreSyn.
This commit fixes Trac #13394.
Diffstat (limited to 'compiler/coreSyn/CoreSyn.hs')
| -rw-r--r-- | compiler/coreSyn/CoreSyn.hs | 18 |
1 files changed, 17 insertions, 1 deletions
diff --git a/compiler/coreSyn/CoreSyn.hs b/compiler/coreSyn/CoreSyn.hs index 31fbd12979..385ea4ecd6 100644 --- a/compiler/coreSyn/CoreSyn.hs +++ b/compiler/coreSyn/CoreSyn.hs @@ -444,7 +444,10 @@ Note [Levity polymorphism invariants] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ The levity-polymorphism invariants are these: -* The type of a term-binder must not be levity-polymorphic +* The type of a term-binder must not be levity-polymorphic, + unless it is a let(rec)-bound join point + (see Note [Invariants on join points]) + * The type of the argument of an App must not be levity-polymorphic. A type (t::TYPE r) is "levity polymorphic" if 'r' has any free variables. @@ -570,12 +573,25 @@ Join points must follow these invariants: 1. All occurrences must be tail calls. Each of these tail calls must pass the same number of arguments, counting both types and values; we call this the "join arity" (to distinguish from regular arity, which only counts values). + 2. For join arity n, the right-hand side must begin with at least n lambdas. + 3. If the binding is recursive, then all other bindings in the recursive group must also be join points. + 4. The binding's type must not be polymorphic in its return type (as defined in Note [The polymorphism rule of join points]). +However, join points have simpler invariants in other ways + + 5. A join point can have an unboxed type without the RHS being + ok-for-speculation (i.e. drop the let/app invariant) + e.g. let j :: Int# = factorial x in ... + + 6. A join point can have a levity-polymorphic RHS + e.g. let j :: r :: TYPE l = fail void# in ... + This happened in an intermediate program Trac #13394 + Examples: join j1 x = 1 + x in jump j (jump j x) -- Fails 1: non-tail call |