<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="">Yes, in support. Thanks for the nice summary.<div class=""><br class=""></div><div class="">Richard<br class=""><div><br class=""><blockquote type="cite" class=""><div class="">On Aug 29, 2023, at 4:40 AM, Moritz Angermann <<a href="mailto:moritz.angermann@gmail.com" class="">moritz.angermann@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div dir="auto" class="">Looks like an overall improvement to me. I’m in support. </div><div class=""><br class=""><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, 29 Aug 2023 at 2:48 PM, Vladislav <<a href="mailto:vlad.z.4096@gmail.com" class="">vlad.z.4096@gmail.com</a>> wrote:<br class=""></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-style:solid;padding-left:1ex;border-left-color:rgb(204,204,204)"><div id="m_-225181298943727227geary-body" dir="auto" class=""><div class="">Dear Committee,</div><div class=""><br class=""></div><div class="">Jakob Brünker has proposed #607, an amendment to proposals #281 (visible forall) and #378 (Design of DH). </div><div class="">See the diff here: <a href="https://github.com/ghc-proposals/ghc-proposals/pull/607/files" target="_blank" class="">https://github.com/ghc-proposals/ghc-proposals/pull/607/files</a></div><div class=""><br class=""></div><div class="">The amendment concerns type checking of term-level variables appearing in types, for example:</div><div class=""><br class=""></div><div class=""> f :: forall (a :: Bool) -> ... -- visible forall, `f` expects a type-level Bool</div><div class=""> g :: Bool -> ... -- ordinary arrow, `g` expects a term-level Bool</div><div class=""> g x = f x</div><div class=""><br class=""></div><div class="">What should happen to `x`, bound as a term variable but used as a type? #378 "Design for Dependent Types" already has an answer to this question: treat `x` as a skolem. But there are two problems</div><div class=""><br class=""></div><div class="">1. #378 does not explain this design decision in sufficient detail. This led Simon to question its inclusion: "Does it have any value, really? Why not just reject?"</div><div class="">2. #281 follows this design in one section, saying "treated as a fresh skolem constant"; and rejects it in another section, saying "any uses of terms in types are ill-typed". There is a contradiction.</div><div class=""><br class=""></div><div class="">The amendment addresses both issues as follows:</div><div class=""><br class=""></div><div class="">1. A new example is added to #378, explaining how treating `x` as a skolem is useful, but only if `foreach` is available (a retained quantifier that allows dependent pattern matching)</div><div class="">2. Contradiction in #281 is resolved in favor of rejecting any uses of terms in types as ill-typed, saving this feature for a future proposal.</div><div class=""><br class=""></div><div class="">I recommend to accept. Please share your thoughts either here or directly on GitHub.</div><div class=""><br class=""></div><div class="">Vlad</div></div>_______________________________________________<br class="">
ghc-steering-committee mailing list<br class="">
<a href="mailto:ghc-steering-committee@haskell.org" target="_blank" class="">ghc-steering-committee@haskell.org</a><br class="">
<a href="https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee" rel="noreferrer" target="_blank" class="">https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee</a><br class="">
</blockquote></div></div>
_______________________________________________<br class="">ghc-steering-committee mailing list<br class=""><a href="mailto:ghc-steering-committee@haskell.org" class="">ghc-steering-committee@haskell.org</a><br class="">https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee<br class=""></div></blockquote></div><br class=""></div></body></html>