Hi,

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. 

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

2. Do explicit type signatures impose any unification constraints, or can they be thought of entirely in terms of wrappers?

For example, if we have

g :: Int -> Int
(f,g) = (\x ->x, f)

then the signature for g is added to the environment when typing the right-hand-side.

One way that this could be handled is:

(i) typecheck rhs -> rhs_type

(ii) generate type of lhs with fresh variables for every binder -> lhs_type = (a,b)

(iii) unify(lhs_type, rhs_type)

(iv) do one-way unification: match(inferred-type-of-g, explicit-type-for-g)

Is this correct?  Step (iv), the way that I have written it, would impose unification constraints.

Without considering the type signature, we would have

{ f_mono :: a -> a, g_mono :: a -> a}

If we just use wrappers to impose the explict type, it seems like we would get something like

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

where f :: forall a.a ->a and g :: Int -> Int.

THIH seems to imply that type signatures are merely checked: no unification constraints are imposed (I think).  However, ghc reports f :: Int -> Int.

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.

thanks!

-BenRI