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 <j...@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
_______________________________________________
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
