<html>
<head>
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
</head>
<body>
<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>
</body>
</html>