<div dir="ltr"><p>Hello,</p>
<p>As I mentioned in <a href="https://mail.haskell.org/pipermail/ghc-devs/2021-October/020223.html">a previous email</a>,
 GHC seems currently somewhat uncertain about whether or not matching on
 GADTs is permitted in arrow notation. Sam Derbyshire suggested <a href="https://twitter.com/samderbyshire/status/1444705156583641099">on Twitter</a> that we probably do, ideally speaking, want to support them. Unfortunately, I am confident that the existing implementation is <em>not</em> up to this task, as I have now demonstrated in issues <a href="https://gitlab.haskell.org/ghc/ghc/-/issues/20469">#20469</a> and <a href="https://gitlab.haskell.org/ghc/ghc/-/issues/20470">#20470</a>.</p>
<p>The latter of those two issues is particularly challenging to solve, 
as it highlights the sorts of tricky interactions that can arise when 
arrow notation is mixed with existential quantification. To give an 
example, suppose we have the following datatypes:</p>
<pre><code>    data A where
      A :: a -> B a -> A
    data B a where
      B :: B ()</code></pre>
<p>And suppose we have the following <code>proc</code> expression:</p>
<pre><code>    proc a -> case a of
      A x B -> id -< x</code></pre>
<p>The match on the <code>A</code> constructor introduces a locally-scoped skolem, and even though the use of <code>id</code> appears on the RHS, it is <em>not</em> actually within the match’s scope—rather, its scope is that of the overall <code>proc</code> expression.</p>
<p>This makes it tricky to maintain typechecker invariants, as 
introduced metavariables must not accidentally leak into the outer scope
 via these strangely-scoped expressions. For example, when typechecking 
the above expression, we’ll increment <code>tcl_tclevel</code> before typechecking the <code>id -< x</code> command, and we may introduce fresh metavariables while doing so. This means we may end up with an expected type for <code>id</code> that looks like this:</p>
<pre><code>    a1[tau:1] -> a2[tau:1]</code></pre>
<p>However, when we actually check <code>id</code> against that type, we must do so in a context where <code>tcl_tclevel</code> is <code>0</code>, not <code>1</code>.
 This violates WantedInv from Note [TcLevel invariants] in 
GHC.Tc.Utils.TcType. This means we need to do a three-step process to 
properly check <code>id</code>’s type:</p>
<ol type="1"><li><p>Synthesize a new metavariable <code>a3[tau:0]</code>.</p></li><li><p>Emit <code>[W] a3[tau:0] ~ (a1[tau:1] -> a2[tau:1])</code> within the arrow scope, i.e. where <code>tcl_tclevel = 1</code>.</p></li><li><p>Check <code>id</code> against <code>a3[tau:0]</code>.</p></li></ol>
<p>Discerning readers may note that this looks <em>awfully</em> similar to the process by which we promote a type via <code>promoteTcType</code>,
 as described in Note [Promoting a type] in GHC.Tc.Utils.TcMType. 
However, in this case, we aren’t really promoting a type, but <em>demoting</em>
 it—we ultimately want to decrease its level, not increase it. However, it
 seems to me that the process of doing this demotion is in fact handled 
perfectly fine by <code>promoteTcType</code>. So my question is twofold:</p>
<ol type="1"><li><p>Is my reasoning about what to do here correct?</p></li><li><p>Is there any harm in using <code>promoteTcType</code> to do this demotion?</p></li></ol>
<p>Thanks,<br>
Alexis</p></div>