<html><head><meta http-equiv="Content-Type" content="text/html; charset=us-ascii"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">Some time has passed. Have you made forward progress?<div class=""><br class=""></div><div class="">The truth is that the particular case you describe would make me, too, stare hard at the code. (This is why I have been slow to respond!)</div><div class=""><br class=""></div><div class="">One thing I can say is that I do not think HsWrappers are much implicated. They are involved with instantiation of type variables and of dictionaries (among other fun things). Instead, look for a construct called AbsBinds, which is heavily implicated here.</div><div class=""><br class=""></div><div class="">You seem to be doing interesting work -- please don't let yourself get stuck. Keeping asking for answers if you need them! :)</div><div class=""><br class=""></div><div class="">Richard<br class=""><div><br class=""><blockquote type="cite" class=""><div class="">On Feb 7, 2022, at 8:21 PM, Benjamin Redelings <<a href="mailto:benjamin.redelings@gmail.com" class="">benjamin.redelings@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class="">
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8" class="">
<div class=""><p class="">So... I suspect that the best way forwards is just to read
GHC/TC/Gen/Bind.hs and make notes on all the functions. That is
what I am doing.<br class="">
</p><p class="">-BenRI<br class="">
</p>
<div class="moz-cite-prefix">On 1/31/22 2:50 PM, Benjamin Redelings
wrote:<br class="">
</div>
<blockquote type="cite" cite="mid:69bf561f-2fea-d1dd-4485-75e7dcbe28de@gmail.com" class="">
<meta http-equiv="content-type" content="text/html; charset=UTF-8" class=""><p class="">Hi,</p><p class="">I am trying to understand (and implement) how Haskell handles
explicit type signatures. Specifically, I'm trying to
understand how explicit type signatures interact with wrappers.
<br class="">
</p><p class="">1. Is there any paper or documentation that explains wrappers
and/or explicit type signatures in detail? There are some
non-obvious details regarding wrappers, such as using
eliminating type arguments by supplying the Any type as an
argument...<br class="">
</p><p class="">2. Do explicit type signatures impose any unification
constraints, or can they be thought of entirely in terms of
wrappers?</p><p class="">For example, if we have <br class="">
</p>
<pre class="">g :: Int -> Int
(f,g) = (\x ->x, f)
</pre><p class="">then the signature for g is added to the environment when
typing the right-hand-side.</p><p class="">One way that this could be handled is:</p><p class="">(i) typecheck rhs -> rhs_type<br class="">
</p><p class="">(ii) generate type of lhs with fresh variables for every binder
-> lhs_type = (a,b)<br class="">
</p><p class="">(iii) unify(lhs_type, rhs_type)</p><p class="">(iv) do one-way unification: match(inferred-type-of-g,
explicit-type-for-g)</p><p class="">Is this correct? Step (iv), the way that I have written it,
would impose unification constraints.</p><p class="">Without considering the type signature, we would have</p><p class="">{ f_mono :: a -> a, g_mono :: a -> a}</p><p class="">If we just use wrappers to impose the explict type, it seems
like we would get something like<br class="">
</p>
<pre class="">let tup = /\a.let {(f:a,g:a) = (\x:a -> x:a, f::a->a)
f = /\a.case tup a of (f,g) -> f
g = case tup @Int of (f,g) -> g
</pre><p class="">where f :: forall a.a ->a and g :: Int -> Int.</p><p class="">THIH seems to imply that type signatures are merely checked: no
unification constraints are imposed (I think). However, ghc
reports f :: Int -> Int.</p><p class="">I apologize if this is a dumb question. I have found the
definition of HsWrapper in
ghc/compiler/GHC/Tc/Types/Evidence.hs, but I am still struggling
a bit.</p><p class="">thanks!<br class="">
</p><p class="">-BenRI<br class="">
</p>
</blockquote>
</div>
_______________________________________________<br class="">Haskell-Cafe mailing list<br class="">To (un)subscribe, modify options or view archives go to:<br class=""><a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" class="">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br class="">Only members subscribed via the mailman list are allowed to post.</div></blockquote></div><br class=""></div></body></html>