Re: How do Coercions work

Hi Ben, thanks, that *does* make clear what TransCo does, I did not know how the transitivity was meant to act. This also hints that my code there is utter garbage, as I already suspected. So I guess my actual question is: What does the coercion returned by normalize_type represent? Same with flatten_one in TcFlatten.hs. I have problems visualizing what is going on there and what is expected of me to do with the returned coercion from a recursive call. Cheers, Jan Am 22.07.19 um 15:58 schrieb Ben Gamari:

Jan van Brügge 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