<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>