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.

5 files changed, 51 insertions, 14 deletions

diff --git a/compiler/coreSyn/CoreLint.hs b/compiler/coreSyn/CoreLint.hs
index aed938220c..93fcbe4b3f 100644
--- a/compiler/coreSyn/CoreLint.hs
+++ b/compiler/coreSyn/CoreLint.hs
@@ -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
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
diff --git a/compiler/coreSyn/CoreUnfold.hs b/compiler/coreSyn/CoreUnfold.hs
index 3a46d58089..0e3efbf5de 100644
--- a/compiler/coreSyn/CoreUnfold.hs
+++ b/compiler/coreSyn/CoreUnfold.hs
@@ -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
diff --git a/testsuite/tests/polykinds/T13394.hs b/testsuite/tests/polykinds/T13394.hs
new file mode 100644
index 0000000000..88c482a4e9
--- /dev/null
+++ b/testsuite/tests/polykinds/T13394.hs
@@ -0,0 +1,15 @@
+{-# 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"]
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index 270aea3287..8dd27b0377 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -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, [''])