<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">I think the real difference is whether new type variables are brought into scope. It seems that GHC can't deal with a proc-pattern-match that introduces type variables, but it *can* deal with introduced constraints. I have no idea *why* this is the case, but it seems a plausible (if accidental) resting place for the implementation.<div class=""><br class=""></div><div class="">Richard<br class=""><div><br class=""><blockquote type="cite" class=""><div class="">On Oct 3, 2021, at 12:19 PM, Alexis King <<a href="mailto:lexi.lambda@gmail.com" class="">lexi.lambda@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div dir="ltr" class=""><p class="">Hi,</p><p class="">I’ve been working on bringing my reimplementation of arrow notation
back up to date, and I’ve run into some confusion about the extent to
which arrow notation is “supposed” to support matching on GADT
constructors. <code class="">Note [Arrows and patterns]</code> in <code class="">GHC.Tc.Gen.Pat</code> suggests they aren’t supposed to be supported at all, which is what I would essentially expect. But issues <a href="https://gitlab.haskell.org/ghc/ghc/-/issues/17423" class="">#17423</a> and <a href="https://gitlab.haskell.org/ghc/ghc/-/issues/18950" class="">#18950</a> provide examples of using GADT constructors in arrow notation, and there seems to be some expectation that in fact they <em class="">ought</em> to be supported, and some recently-added test cases verify that’s the case.</p><p class="">But this is quite odd, because it means the arrows test suite now includes test cases that verify both that this is supported <em class="">and</em> that it isn’t… and all of them pass! Here’s my understanding of the status quo:</p>
<ul class=""><li class=""><p class="">Matching on constructors that bind bona fide existential variables is not allowed, and this is verified by the <code class="">arrowfail004</code> test case, which involves the following program:</p>
<pre class=""><code class="">data T = forall a. T a
panic :: (Arrow arrow) => arrow T T
panic = proc (T x) -> do returnA -< T x</code></pre><p class="">This program is rejected with the following error message:</p>
<pre class=""><code class="">arrowfail004.hs:12:15:
Proc patterns cannot use existential or GADT data constructors
In the pattern: T x</code></pre></li><li class=""><p class="">Despite the previous point, matching on constructors that bind evidence is allowed. This is enshrined in test cases <code class="">T15175</code>, <code class="">T17423</code>, and <code class="">T18950</code>, which match on constructors like these:</p>
<pre class=""><code class="">data DecoType a where
DecoBool :: Maybe (String, String) -> Maybe (Int, Int) -> DecoType Bool
data Point a where
Point :: RealFloat a => a -> Point a</code></pre></li></ul><p class="">This seems rather contradictory to me. I don’t think there’s much of a
meaningful distinction between these types of matches, as they create
precisely the same set of challenges from the Core point of view… right?
And even if I’m wrong, the error message in <code class="">arrowfail004</code> seems rather misleading, since I would definitely call <code class="">DecoBool</code> and <code class="">Point</code> above “GADT data constructors”.</p><p class="">So what’s the intended story here? Is matching on GADT constructors
in arrow notation supposed to be allowed or not? (I suspect this is
really just yet another case of “nobody really knows what’s ‘supposed’
to happen with arrow notation,” but I figured I might as well ask out of
hopefulness that someone has some idea.)</p><p class="">Thanks,<br class="">
Alexis</p></div>
_______________________________________________<br class="">ghc-devs mailing list<br class=""><a href="mailto:ghc-devs@haskell.org" class="">ghc-devs@haskell.org</a><br class="">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs<br class=""></div></blockquote></div><br class=""></div></body></html>