<div dir="ltr"><div>Hi Devs!</div><div><br></div>I encountered a curious restriction with type signatures (tyvar bindings) in GADT pattern matches.<div><br></div><div>GHC won't let me directly capture the refined type structure of GADT constructors like this:</div><div><br></div><div><br></div><div><div><font face="monospace, monospace">{-# Language GADTs, ScopedTypeVariables #-}</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">data Foo a where</font></div><div><font face="monospace, monospace">  Bar :: Foo [a]</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">foo :: Foo a -> ()</font></div><div><font face="monospace, monospace">foo b@(Bar :: Foo [a]) = quux b</font></div><div><font face="monospace, monospace">  where quux :: Foo [b] -> ()</font></div><div><font face="monospace, monospace">        quux Bar = ()</font></div></div><div><br></div><div><br></div><div>I get:</div><div><br></div><div><br></div><div><p style="margin:0px;font-size:15px;line-height:normal"><font face="arial, helvetica, sans-serif"><span style="font-variant-ligatures:no-common-ligatures"><b>test.hs:7:8: </b></span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(195,55,32)"><b>error:</b></span></font></p>
<p style="margin:0px;font-size:15px;line-height:normal"><span style="font-variant-ligatures:no-common-ligatures"><b><font face="arial, helvetica, sans-serif">    • Couldn't match type ‘a1’ with ‘[a]’</font></b></span></p>
<p style="margin:0px;font-size:15px;line-height:normal"><span style="font-variant-ligatures:no-common-ligatures"><b><font face="arial, helvetica, sans-serif">      ‘a1’ is a rigid type variable bound by</font></b></span></p>
<p style="margin:0px;font-size:15px;line-height:normal"><span style="font-variant-ligatures:no-common-ligatures"><b><font face="arial, helvetica, sans-serif">        the type signature for:</font></b></span></p>
<p style="margin:0px;font-size:15px;line-height:normal"><span style="font-variant-ligatures:no-common-ligatures"><b><font face="arial, helvetica, sans-serif">          foo :: forall a1. Foo a1 -> ()</font></b></span></p>
<p style="margin:0px;font-size:15px;line-height:normal"><span style="font-variant-ligatures:no-common-ligatures"><b><font face="arial, helvetica, sans-serif">        at test.hs:6:1-18</font></b></span></p>
<p style="margin:0px;font-size:15px;line-height:normal"><span style="font-variant-ligatures:no-common-ligatures"><b><font face="arial, helvetica, sans-serif">      Expected type: Foo a1</font></b></span></p>
<p style="margin:0px;font-size:15px;line-height:normal"><span style="font-variant-ligatures:no-common-ligatures"><b><font face="arial, helvetica, sans-serif">        Actual type: Foo [a]</font></b></span></p></div><div><span style="font-variant-ligatures:no-common-ligatures"><b><br></b></span></div><div><br></div>To me it appears that the type refinement established by the GADT pattern match is not accounted for.<div><br></div><div>Of course I can write:</div><div><br></div><div><div><font face="monospace, monospace">foo :: Foo a -> ()</font></div><div><font face="monospace, monospace">foo b@Bar | (c :: Foo [a]) <- b = quux c</font></div><div><font face="monospace, monospace">  where quux :: Foo [b] -> ()</font></div><div><font face="monospace, monospace">        quux Bar = ()</font></div></div><div><br></div><div>but it feels like a complicated way to do it...</div><div><br></div><div>My question is whether this is generally seen as the way to go or whether <span style="font-family:monospace,monospace">ScopedTypeVariables</span> coming from a GADT pattern match should be able to capture the refined type. To me the latter seems more useful.</div><div><br></div><div>Just wanted to feel the waters before writing a ticket about this.</div><div><br></div><div>Cheers and thanks,</div><div><br></div><div>    Gabor</div></div>