Why is the undefined function levity-polymorphic when using it with unboxed types? : <p>I just got finished reading the paper <a href="https://cs.brynmawr.edu/~rae/papers/2017/levity/levity-extended.pdf" rel="noreferrer">Levity Polymorphism</a>.</p>

<p>I had a question about why <a href="https://hackage.haskell.org/package/base-4.11.1.0/docs/Prelude.html#v:undefined" rel="noreferrer"><code>undefined</code></a> can be levity-polymorphic when used as an unboxed type.</p>

<p>First, let's start with some definitions of boxity from the paper:</p>

<ul>
<li><p><strong>boxed</strong>:</p>

<ul>
<li><p>A <strong>boxed</strong> value is represented by a pointer into the heap.</p></li>
<li><p><code>Int</code> and <code>Bool</code> are examples of types that have <strong>boxed</strong> values.</p></li>
</ul></li>
<li><p><strong>unboxed</strong>:</p>

<ul>
<li><p>An <strong>unboxed</strong> value is represented by the value itself (<em>not</em> a pointer to the heap).</p></li>
<li><p><a href="https://hackage.haskell.org/package/ghc-prim-0.5.2.0/docs/GHC-Prim.html#g:3" rel="noreferrer"><code>Int#</code></a> and <a href="https://hackage.haskell.org/package/ghc-prim-0.5.2.0/docs/GHC-Prim.html#g:2" rel="noreferrer"><code>Char#</code></a> from the <a href="https://hackage.haskell.org/package/ghc-prim-0.5.2.0/docs/GHC-Prim.html" rel="noreferrer"><code>GHC.Prim</code></a> module are examples of types with <strong>unboxed</strong> values.</p></li>
<li><p>An <strong>unboxed</strong> value cannot be a thunk.  Function arguments of unboxed types must be passed by value.</p></li>
</ul></li>
</ul>

<p>The paper follows with some definitions of levity:</p>

<ul>
<li><p><strong>lifted</strong>:</p>

<ul>
<li><p>A <strong>lifted</strong> type is one that is lazy.</p></li>
<li><p>A <strong>lifted</strong> type has on extra element beyond the normal ones, representing a non-terminating computation.</p></li>
<li><p>For example, the type <code>Bool</code> is <strong>lifted</strong>, meaning that there are three different values for <code>Bool</code>: <code>True</code>, <code>False</code>, and <code>⊥</code> (bottom).</p></li>
<li><p>All <strong>lifted</strong> types MUST be <strong>boxed</strong>.</p></li>
</ul></li>
<li><p><strong>unlifted</strong></p>

<ul>
<li><p>An <strong>unlifted</strong> type is one that is strict.</p></li>
<li><p>The element <code>⊥</code> does not exist in an <strong>unlifted</strong> type.</p></li>
<li><p><code>Int#</code> and <code>Char#</code> are examples of <strong>unlifted</strong> types.</p></li>
</ul></li>
</ul>

<p>The paper goes on to explain how GHC 8 provides functionality allowing type variables to have polymorphic levity.</p>

<p>This allows you to write a levity-polymorphic <a href="https://hackage.haskell.org/package/base-4.11.1.0/docs/Prelude.html#v:undefined" rel="noreferrer"><code>undefined</code></a> with the following type:</p>

<pre><code>undefined :: forall (r :: RuntimeRep). forall (a :: TYPE r). a
</code></pre>

<p>This says that <code>undefined</code> should work for <em>any</em> <code>RuntimeRep</code>, even unlifted types.</p>

<p>Here is an example of using <code>undefined</code> as an unboxed, unlifted <code>Int#</code> in GHCi:</p>

<pre><code>&gt; :set -XMagicHash
&gt; import GHC.Prim
&gt; import GHC.Exts
&gt; I# (undefined :: Int#)
*** Exception: Prelude.undefined
</code></pre>

<hr>

<p>I've always thought of <code>undefined</code> as being the same as <code>⊥</code> (bottom).  However, the paper says, "The element <code>⊥</code> does not exist in an unlifted type."</p>

<p>What is going on here? Is <code>undefined</code> not actually <code>⊥</code> when used as an unlifted type?  Am I misunderstanding something about the paper (or boxity or levity)?</p>
