<div dir="auto">Coincidentally, I've been thinking about (a small part of) this issue for a day or two. I think it would probably be pretty easy to add a language feature that basically brought what the compiler does up to the Haskell level. Imagine a sort of *generalized* as-pattern:<div dir="auto"><br></div><div dir="auto">f x@@(Right y) = ...</div><div dir="auto"><br></div><div dir="auto">`x` here is not bound to the actual argument; instead, it is bound to `Right y`. The type of `x` will either be inferred or given explicitly:</div><div dir="auto"><br></div><div dir="auto">f (x :: ...)@@(Right y) = ...</div><div dir="auto"><br></div><div dir="auto">How can this translate to Core? Roughly speaking, it would look like</div><div dir="auto"><br></div><div dir="auto">f _x = case _x of</div><div dir="auto">  Left p -> ...</div><div dir="auto">  Right y -></div><div dir="auto">    let x = unsafeCoerce _x</div><div dir="auto">    in ...</div><div dir="auto"><br></div><div dir="auto">But `x` would be given the unfolding `Right y`.</div><div dir="auto"><br></div><div dir="auto">For existentials and GADTs, the type checking and Core translation needs some extras. In particular, the dictionary arguments need to be included to ensure the coercion is valid. Just make sure they match. The special ~ and Coercible constraints don't need to be included in that check, but it must be possible to produce coercions with the appropriate types.</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, Dec 2, 2020, 11:32 AM Brent Walker <<a href="mailto:brenthwalker@gmail.com" target="_blank" rel="noreferrer">brenthwalker@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">My question was on how to use coerce -- not whether this is worth doing or not.  If we were discussing that, then I would say it's not 'just a leaf' -- it's ALL the leaves of the tree -- and for a tree of depth n, there are 2^n of them so depending on what 'n' is, it could potentially be something to worry about.<div><br></div><div><div><br></div></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, Dec 2, 2020 at 6:00 PM Henning Thielemann <<a href="mailto:lemming@henning-thielemann.de" rel="noreferrer noreferrer" target="_blank">lemming@henning-thielemann.de</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><br>
On Wed, 2 Dec 2020, Brent Walker wrote:<br>
<br>
> In the following code, function fmap does not compile because variable <br>
> 'y' on line marked <***> has type (Expr a) where an (Expr b) is <br>
> expected.  The code can be fixed simply by returning (Val x) on the rhs <br>
> of the function but then we are allocating a new object for something we <br>
> could potentially reuse since (Val n) has the same runtime <br>
> representation in (Expr a) and (Expr b) (it has no dependence on the <br>
> type variable).<br>
<br>
Is it worth the trouble? It is only a leaf of the tree.</blockquote></div>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
To (un)subscribe, modify options or view archives go to:<br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer noreferrer noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
Only members subscribed via the mailman list are allowed to post.</blockquote></div>