<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
<p>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>
</p>
<p>-BenRI<br>
</p>
<div class="moz-cite-prefix">On 1/31/22 2:50 PM, Benjamin Redelings
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:69bf561f-2fea-d1dd-4485-75e7dcbe28de@gmail.com">
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
<p>Hi,</p>
<p>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>
</p>
<p>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>
</p>
<p>2. Do explicit type signatures impose any unification
constraints, or can they be thought of entirely in terms of
wrappers?</p>
<p>For example, if we have <br>
</p>
<pre>g :: Int -> Int
(f,g) = (\x ->x, f)
</pre>
<p>then the signature for g is added to the environment when
typing the right-hand-side.</p>
<p>One way that this could be handled is:</p>
<p>(i) typecheck rhs -> rhs_type<br>
</p>
<p>(ii) generate type of lhs with fresh variables for every binder
-> lhs_type = (a,b)<br>
</p>
<p>(iii) unify(lhs_type, rhs_type)</p>
<p>(iv) do one-way unification: match(inferred-type-of-g,
explicit-type-for-g)</p>
<p>Is this correct? Step (iv), the way that I have written it,
would impose unification constraints.</p>
<p>Without considering the type signature, we would have</p>
<p>{ f_mono :: a -> a, g_mono :: a -> a}</p>
<p>If we just use wrappers to impose the explict type, it seems
like we would get something like<br>
</p>
<pre>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>where f :: forall a.a ->a and g :: Int -> Int.</p>
<p>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>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>thanks!<br>
</p>
<p>-BenRI<br>
</p>
</blockquote>
</body>
</html>