Commit 8e053700 authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

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.
parent bd668171
......@@ -506,13 +506,20 @@ lintSingleBinding top_lvl_flag rec_flag (binder,rhs)
; binder_ty <- applySubstTy (idType binder)
; ensureEqTys binder_ty ty (mkRhsMsg binder (text "RHS") ty)
-- Check that it's not levity-polymorphic
-- Do this first, because otherwise isUnliftedType panics
-- Annoyingly, this duplicates the test in lintIdBdr,
-- because for non-rec lets we call lintSingleBinding first
; checkL (isJoinId binder || not (isTypeLevPoly binder_ty))
(badBndrTyMsg binder (text "levity-polymorphic"))
-- Check the let/app invariant
-- See Note [CoreSyn let/app invariant] in CoreSyn
; checkL (not (isUnliftedType binder_ty)
|| isJoinId binder
|| (isNonRec rec_flag && exprOkForSpeculation rhs)
|| exprIsLiteralString rhs)
(mkRhsPrimMsg binder rhs)
; checkL ( isJoinId binder
|| not (isUnliftedType binder_ty)
|| (isNonRec rec_flag && exprOkForSpeculation rhs)
|| exprIsLiteralString rhs)
(badBndrTyMsg binder (text "unlifted"))
-- Check that if the binder is top-level or recursive, it's not
-- demanded. Primitive string literals are exempt as there is no
......@@ -1208,7 +1215,7 @@ lintIdBndr top_lvl bind_site id linterF
; (ty, k) <- lintInTy (idType id)
-- See Note [Levity polymorphism invariants] in CoreSyn
; lintL (not (isKindLevPoly k))
; lintL (isJoinId id || not (isKindLevPoly k))
(text "Levity-polymorphic binder:" <+>
(ppr id <+> dcolon <+> parens (ppr ty <+> dcolon <+> ppr k)))
......@@ -2263,12 +2270,10 @@ mkLetAppMsg e
= hang (text "This argument does not satisfy the let/app invariant:")
2 (ppr e)
mkRhsPrimMsg :: Id -> CoreExpr -> MsgDoc
mkRhsPrimMsg binder _rhs
= vcat [hsep [text "The type of this binder is primitive:",
ppr binder],
hsep [text "Binder's type:", ppr (idType binder)]
]
badBndrTyMsg :: Id -> SDoc -> MsgDoc
badBndrTyMsg binder what
= vcat [ text "The type of this binder is" <+> what <> colon <+> ppr binder
, text "Binder's type:" <+> ppr (idType binder) ]
mkStrictMsg :: Id -> MsgDoc
mkStrictMsg binder
......
......@@ -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
......
......@@ -657,8 +657,8 @@ sizeExpr dflags bOMB_OUT_SIZE top_args expr
-- Cost to allocate binding with given binder
size_up_alloc bndr
| isTyVar bndr -- Doesn't exist at runtime
|| isUnliftedType (idType bndr) -- Doesn't live in heap
|| isJoinId bndr -- Not allocated at all
|| isUnliftedType (idType bndr) -- Doesn't live in heap
= 0
| otherwise
= 10
......
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
module T13394 where
import Data.ByteString
newtype ProperName =
ProperName { runProperName :: ByteString
-- purescript actually uses the Text type, but this works
-- just as well for the purposes of illustrating the bug
}
newtype ModuleName = ModuleName [ProperName]
pattern TypeDataSymbol :: ModuleName
pattern TypeDataSymbol = ModuleName [ProperName "Type"]
......@@ -155,3 +155,4 @@ test('T12718', normal, compile, [''])
test('T12444', normal, compile_fail, [''])
test('T12885', normal, compile, [''])
test('T13267', normal, compile_fail, [''])
test('T13394', normal, compile, [''])
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment