[Haskell-cafe] Explicit type signatures and wrappers / impedance-matching

[Benjamin Redelings]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20220131/f11edd59/attachment.html>