<html><head><meta http-equiv="Content-Type" content="text/html charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class="">Hi Gabor,<div class=""><br class=""></div><div class="">Oleg is right that the re-use of type variables obscures the error, but it's not quite a scoping error under the hood. The problem is that GHC type-checks type signatures on patterns *before* type-checking the pattern itself. That means that when GHC checks your `Foo [a]` type signature, we haven't yet learned that `a1` (the type variable used in the type signature of foo) equals `[a]`. This makes it hard to bind a variable to `a`. Here's what I've done:</div><div class=""><br class=""></div><div class=""><div class=""></div></div><blockquote type="cite" class=""><div class=""><div class="">foo :: Foo a -> ()</div><div class="">foo b@Bar = case b of</div><div class=""> (_ :: Foo [c]) -> quux b</div><div class=""> where</div><div class=""> quux :: Foo [c] -> ()</div><div class=""> quux Bar = ()</div></div></blockquote><div class=""><br class=""></div><div class="">It's gross, but it works, and I don't think there's a better way at the moment. A collaborator of mine is working on a proposal (and implementation) of binding existentials in patterns (using similar syntax to visible type application), but that's still a few months off, at best.</div><div class=""><br class=""></div><div class="">Richard</div><div class=""><br class=""><div><blockquote type="cite" class=""><div class="">On Oct 29, 2017, at 1:42 PM, Gabor Greif <<a href="mailto:ggreif@gmail.com" class="">ggreif@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div dir="ltr" class=""><div class="">Hi Devs!</div><div class=""><br class=""></div>I encountered a curious restriction with type signatures (tyvar bindings) in GADT pattern matches.<div class=""><br class=""></div><div class="">GHC won't let me directly capture the refined type structure of GADT constructors like this:</div><div class=""><br class=""></div><div class=""><br class=""></div><div class=""><div class=""><font face="monospace, monospace" class="">{-# Language GADTs, ScopedTypeVariables #-}</font></div><div class=""><font face="monospace, monospace" class=""><br class=""></font></div><div class=""><font face="monospace, monospace" class="">data Foo a where</font></div><div class=""><font face="monospace, monospace" class=""> Bar :: Foo [a]</font></div><div class=""><font face="monospace, monospace" class=""><br class=""></font></div><div class=""><font face="monospace, monospace" class="">foo :: Foo a -> ()</font></div><div class=""><font face="monospace, monospace" class="">foo b@(Bar :: Foo [a]) = quux b</font></div><div class=""><font face="monospace, monospace" class=""> where quux :: Foo [b] -> ()</font></div><div class=""><font face="monospace, monospace" class=""> quux Bar = ()</font></div></div><div class=""><br class=""></div><div class=""><br class=""></div><div class="">I get:</div><div class=""><br class=""></div><div class=""><br class=""></div><div class=""><div style="margin: 0px; font-size: 15px; line-height: normal;" class=""><font face="arial, helvetica, sans-serif" class=""><span style="font-variant-ligatures:no-common-ligatures" class=""><b class="">test.hs:7:8: </b></span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(195,55,32)" class=""><b class="">error:</b></span></font></div><div style="margin: 0px; font-size: 15px; line-height: normal;" class=""><span style="font-variant-ligatures:no-common-ligatures" class=""><b class=""><font face="arial, helvetica, sans-serif" class=""> • Couldn't match type ‘a1’ with ‘[a]’</font></b></span></div><div style="margin: 0px; font-size: 15px; line-height: normal;" class=""><span style="font-variant-ligatures:no-common-ligatures" class=""><b class=""><font face="arial, helvetica, sans-serif" class=""> ‘a1’ is a rigid type variable bound by</font></b></span></div><div style="margin: 0px; font-size: 15px; line-height: normal;" class=""><span style="font-variant-ligatures:no-common-ligatures" class=""><b class=""><font face="arial, helvetica, sans-serif" class=""> the type signature for:</font></b></span></div><div style="margin: 0px; font-size: 15px; line-height: normal;" class=""><span style="font-variant-ligatures:no-common-ligatures" class=""><b class=""><font face="arial, helvetica, sans-serif" class=""> foo :: forall a1. Foo a1 -> ()</font></b></span></div><div style="margin: 0px; font-size: 15px; line-height: normal;" class=""><span style="font-variant-ligatures:no-common-ligatures" class=""><b class=""><font face="arial, helvetica, sans-serif" class=""> at test.hs:6:1-18</font></b></span></div><div style="margin: 0px; font-size: 15px; line-height: normal;" class=""><span style="font-variant-ligatures:no-common-ligatures" class=""><b class=""><font face="arial, helvetica, sans-serif" class=""> Expected type: Foo a1</font></b></span></div><div style="margin: 0px; font-size: 15px; line-height: normal;" class=""><span style="font-variant-ligatures:no-common-ligatures" class=""><b class=""><font face="arial, helvetica, sans-serif" class=""> Actual type: Foo [a]</font></b></span></div></div><div class=""><span style="font-variant-ligatures:no-common-ligatures" class=""><b class=""><br class=""></b></span></div><div class=""><br class=""></div>To me it appears that the type refinement established by the GADT pattern match is not accounted for.<div class=""><br class=""></div><div class="">Of course I can write:</div><div class=""><br class=""></div><div class=""><div class=""><font face="monospace, monospace" class="">foo :: Foo a -> ()</font></div><div class=""><font face="monospace, monospace" class="">foo b@Bar | (c :: Foo [a]) <- b = quux c</font></div><div class=""><font face="monospace, monospace" class=""> where quux :: Foo [b] -> ()</font></div><div class=""><font face="monospace, monospace" class=""> quux Bar = ()</font></div></div><div class=""><br class=""></div><div class="">but it feels like a complicated way to do it...</div><div class=""><br class=""></div><div class="">My question is whether this is generally seen as the way to go or whether <span style="font-family:monospace,monospace" class="">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 class=""><br class=""></div><div class="">Just wanted to feel the waters before writing a ticket about this.</div><div class=""><br class=""></div><div class="">Cheers and thanks,</div><div class=""><br class=""></div><div class=""> Gabor</div></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>