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

[Benjamin Redelings]

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