How do Coercions work

[Ben Gamari]

Jan van Brügge <jan at vanbruegge.de> writes:

> Hi,
>
> currently I have some problems understanding how the coercions are
> threaded through the compiler. In particular the function
> `normalise_type`. With guessing and looking at the other cases, I came
> to this solution, but I have no idea if I am on the right track:
>
> normalise_type ty
>   = go ty
>   where
>     go (RowTy k v flds)
>       = do { (co_k, nty_k) <- go k
>            ; (co_v, nty_v) <- go v
>            ; let (a, b) = unzip flds
>            ; (co_a, ntys_a) <- foldM foldCo (co_k, []) a
>            ; (co_b, ntys_b) <- foldM foldCo (co_v, []) b
>            ; return (co_a `mkTransCo` co_b, mkRowTy nty_k nty_v $ zip
> ntys_a ntys_b) }
>         where
>             foldCo (co, tys) t = go t >>= \(c, nt) -> return (co
> `mkTransCo` c, nt:tys)
>
>
> RowTy has type Type -> Type -> [(Type, Type)]
>
> What I am not sure at all is how to treat the coecions. From looking at
> the go_app_tys code I guessed that I can just combine them like that,
> but what does that mean from a semantic standpoint? The core spec was
> not that helpful either in that regard.
>
Perhaps others are quicker than me but I'll admit I'm having a hard time
following this. What is the specification for normalise_type's desired
behavior? What equality is the coercion you are trying to build supposed
to witness?

In short, TransCo (short for "transitivity") represents a "chain" of
coercions. That is, if I have,

    co1 :: a ~ b
    co2 :: b ~ c

then I can construct

    co3 :: a ~ c
    co3 = TransCo co1 co2

Does this help?

Cheers,

- Ben
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 487 bytes
Desc: not available
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20190722/8f465f67/attachment.sig>