<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<title></title>
</head>
<body>
<div name="messageBodySection" style="font-size: 14px; font-family: -apple-system, BlinkMacSystemFont, sans-serif;">Right, but I think Gabor's suggestion here is for type checking of the pattern to be done first, and then capturing the coercions
<div>that were brought into scope by the pattern match.</div>
<div><br /></div>
<div>
<p style="margin: 0px; font-stretch: normal; line-height: normal; font-family: "Helvetica Neue"; color: rgb(51, 51, 51);">data Foo a where</p>
<p style="margin: 0px; font-stretch: normal; line-height: normal; font-family: "Helvetica Neue"; color: rgb(51, 51, 51);"> Bar :: Foo [a]</p>
<p style="margin: 0px; font-stretch: normal; line-height: normal; font-family: "Helvetica Neue"; color: rgb(51, 51, 51); min-height: 16px;"><br /></p>
<p style="margin: 0px; font-stretch: normal; line-height: normal; font-family: "Helvetica Neue"; color: rgb(51, 51, 51);">foo :: Foo a -> ()</p>
<p style="margin: 0px; font-stretch: normal; line-height: normal; font-family: "Helvetica Neue"; color: rgb(51, 51, 51);">foo Bar = <body> -- we know (a ~ [b]) here, for some b</p>
<p style="margin: 0px; font-stretch: normal; line-height: normal; font-family: "Helvetica Neue"; color: rgb(51, 51, 51);"><br /></p>
<p style="margin: 0px; font-stretch: normal; line-height: normal; font-family: "Helvetica Neue"; color: rgb(51, 51, 51);">The pattern match on Bar in foo gives us the equality assumption on the right hand side, but</p>
<p style="margin: 0px; font-stretch: normal; line-height: normal; font-family: "Helvetica Neue"; color: rgb(51, 51, 51);">we don't have an easy way of capturing 'b' - which we might want to do for, say, visible type application inside <body>.</p>
<p style="margin: 0px; font-stretch: normal; line-height: normal; font-family: "Helvetica Neue"; color: rgb(51, 51, 51);"><br /></p>
<p style="margin: 0px; font-stretch: normal; line-height: normal; font-family: "Helvetica Neue"; color: rgb(51, 51, 51);">foo' :: Foo a -> ()</p>
<p style="margin: 0px; font-stretch: normal; line-height: normal; font-family: "Helvetica Neue"; color: rgb(51, 51, 51);">foo' (Bar :: Foo a) = <body></p>
<p style="margin: 0px; font-stretch: normal; line-height: normal; font-family: "Helvetica Neue"; color: rgb(51, 51, 51);"><br /></p>
<p style="margin: 0px; font-stretch: normal; line-height: normal; font-family: "Helvetica Neue"; color: rgb(51, 51, 51);">of course works, but it only gives us access to 'a' in <body>.</p>
<p style="margin: 0px; font-stretch: normal; line-height: normal; font-family: "Helvetica Neue"; color: rgb(51, 51, 51);"><br /></p>
<p style="margin: 0px; font-stretch: normal; line-height: normal; font-family: "Helvetica Neue"; color: rgb(51, 51, 51);">foo'' :: Foo a -> ()</p>
<p style="margin: 0px; font-stretch: normal; line-height: normal; font-family: "Helvetica Neue"; color: rgb(51, 51, 51);">foo'' (Bar :: Foo [c]) = <body></p>
<p style="margin: 0px; font-stretch: normal; line-height: normal; font-family: "Helvetica Neue"; color: rgb(51, 51, 51);"><br /></p>
<p style="margin: 0px; font-stretch: normal; line-height: normal; font-family: "Helvetica Neue"; color: rgb(51, 51, 51);">This would mean that in addition to (a ~ [b]), for some b, we would get (a ~ [c]), for our new c. This then gives (b ~ c),</p>
<p style="margin: 0px; font-stretch: normal; line-height: normal; font-family: "Helvetica Neue"; color: rgb(51, 51, 51);">essentially giving us access to the existential b. Of course we would need to check that our scoped type signature</p>
<p style="margin: 0px; font-stretch: normal; line-height: normal; font-family: "Helvetica Neue"; color: rgb(51, 51, 51);">doesn't introduce bogus coercions, like</p>
<p style="margin: 0px; font-stretch: normal; line-height: normal; font-family: "Helvetica Neue"; color: rgb(51, 51, 51);"><br /></p>
<p style="margin: 0px; font-stretch: normal; line-height: normal; font-family: "Helvetica Neue"; color: rgb(51, 51, 51);">foo''' :: Foo a -> ()</p>
<p style="margin: 0px; font-stretch: normal; line-height: normal; font-family: "Helvetica Neue"; color: rgb(51, 51, 51);">foo''' (Bar :: Foo [[c]]) = <body></p>
<p style="margin: 0px; font-stretch: normal; line-height: normal; font-family: "Helvetica Neue"; color: rgb(51, 51, 51);"><br /></p>
<p style="margin: 0px; font-stretch: normal; line-height: normal; font-family: "Helvetica Neue"; color: rgb(51, 51, 51);">is clearly invalid, because (a ~ [b]) and (a ~ [[c]]) would need (b ~ [c]), which we can't prove from the given assumptions.</p>
<p style="margin: 0px; font-stretch: normal; line-height: normal; font-family: "Helvetica Neue"; color: rgb(51, 51, 51);"><br /></p>
</div>
</div>
<div name="messageSignatureSection" style="font-size: 14px; font-family: -apple-system, BlinkMacSystemFont, sans-serif;"><br />
Cheers,
<div>Csongor</div>
</div>
<div name="messageReplySection" style="font-size: 14px; font-family: -apple-system, BlinkMacSystemFont, sans-serif;"><br />
On 30 Oct 2017, 12:13 +0000, Brandon Allbery <allbery.b@gmail.com>, wrote:<br />
<blockquote type="cite" style="margin: 5px 5px; padding-left: 10px; border-left: thin solid #1abc9c;">
<div dir="ltr">
<div class="gmail_extra">
<div class="gmail_quote">On Mon, Oct 30, 2017 at 5:14 AM, Gabor Greif <span dir="ltr"><<a href="mailto:ggreif@gmail.com" target="_blank">ggreif@gmail.com</a>></span> wrote:<br />
<blockquote class="gmail_quote" style="margin: 5px 5px; padding-left: 10px; border-left: thin solid #e67e22;">My original question, though, is not answered yet, namely why not to<br />
detect that we are about to pattern match on a GADT constructor and<br />
allow the programmer to capture the *refined* type with her type<br />
annotation. Sure this would necessitate a change to the type checker,<br />
but would also increase the expressive power a bit.<br />
<br />
Is there some fundamental problem with this? Or simply nobody wanted<br />
to do this yet? Would it be hard to implement type checking *after*<br />
refinement on GADT(-like) patterns?<br /></blockquote>
</div>
<div><br /></div>
<div>I wouldn't be surprised if type checking is precisely what enables refinement, making this a bit chicken-and-egg.</div>
<div><br /></div>
--<br />
<div class="gmail_signature" data-smartmail="gmail_signature">
<div dir="ltr">
<div>brandon s allbery kf8nh sine nomine associates</div>
<div><a href="mailto:allbery.b@gmail.com" target="_blank">allbery.b@gmail.com</a> <a href="mailto:ballbery@sinenomine.net" target="_blank">ballbery@sinenomine.net</a></div>
<div>unix, openafs, kerberos, infrastructure, xmonad <a href="http://sinenomine.net" target="_blank">http://sinenomine.net</a></div>
</div>
</div>
</div>
</div>
_______________________________________________<br />
ghc-devs mailing list<br />
ghc-devs@haskell.org<br />
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs<br /></blockquote>
<div></div>
</div>
</body>
</html>