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

Some time has passed. Have you made forward progress? The truth is that the particular case you describe would make me, too, stare hard at the code. (This is why I have been slow to respond!) One thing I can say is that I do not think HsWrappers are much implicated. They are involved with instantiation of type variables and of dictionaries (among other fun things). Instead, look for a construct called AbsBinds, which is heavily implicated here. You seem to be doing interesting work -- please don't let yourself get stuck. Keeping asking for answers if you need them! :) Richard

On Feb 7, 2022, at 8:21 PM, Benjamin Redelings wrote:

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.

-BenRI

On 1/31/22 2:50 PM, Benjamin Redelings wrote:

...

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

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.