<html><head><meta http-equiv="Content-Type" content="text/html charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><div>Hi Conal,</div><div><br></div><div>In your case, the `_N` on the argument to NTCo:HasIf[0] is correct -- the `HasIf` class indeed has a nominal parameter. So, it seems that this part, at least, is OK.</div><div><br></div><div>What's the -ddump-tc on EP? Is EP's role nominal? (I think so, given what you're saying.) If that's the case, you won't be able to pass the result of NTCo:HasIf[0] to a coercion built from EP.</div><div><br></div><div>Popping up a level, what are you trying to do here? If EP's role is indeed nominal, then I don't believe there's a fix here, as the coercion it seems you're trying to build may be unsound. (It looks to me like you want something proving `EP (Bool -> Bool -> Bool -> Bool) ~R EP (HasIf Bool)`, but if EP's role is nominal, then this is indeed bogus.)</div><div><br></div><div>Richard</div><div><br></div><div><div>On Apr 14, 2014, at 2:23 PM, Conal Elliott <<a href="mailto:conal@conal.net">conal@conal.net</a>> wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><div dir="ltr"><div><blockquote>

</blockquote>Thanks for the pointers! I don't quite know how to get to the form you recommend from the existing coercion, which is `Simple.NTCo:HasIf[0] <GHC.Types.Bool>_N`. (Note the `_N`.) I got that coercion in GHC 7.8.2 from the following code:<br>

<br>> class HasIf a where<br>>   ifThenElse :: Bool -> a -> a -> a<br>><br>> instance HasIf Bool where<br>>   ifThenElse i t e = (i && t) || (not i && e)<br><br>With `--dump-tc`, I see<br>

<br>> TYPE SIGNATURES<br>> TYPE CONSTRUCTORS<br>>   HasIf :: * -> Constraint<br>>   class HasIf a<br>>     Roles: [nominal]<br>>     RecFlag NonRecursive<br>>     ifThenElse :: Bool -> a -> a -> a<br>

> COERCION AXIOMS<br>>   axiom Main.NTCo:HasIf :: HasIf a = Bool -> a -> a -> a<br>> INSTANCES<br>>   instance HasIf Bool -- Defined at ../test/HasIf.hs:4:10<br><br>Do I need to convert the nominal coercion I got from GHC (`Simple.NTCo:HasIf[0] <GHC.Types.Bool>_N` in this case) to a representational one? If so, how?<br>

My current formulation (tweaked to use `mkSubCo` and `mkAppCo`) is to apply `mkAppCo (mkSubCo (Refl Nominal ep))` to the given coercion, which then produces<br><br>> (LambdaCCC.Lambda.EP (Sym (Simple.NTCo:HasIf[0] <GHC.Types.Bool>_N)))_R<br>

<br>And still I get "Role incompatibility: expected nominal, got representational in `Sym (Simple.NTCo:HasIf[0] <GHC.Types.Bool>_N)`".<br><br>I also tried wrapping `mkSubCo` around the entire coercion (applying `mkSubCo . mkAppCo (Refl Nominal ep)`), and I see the same result:<br>

<br>> (LambdaCCC.Lambda.EP (Sym (Simple.NTCo:HasIf[0] <GHC.Types.Bool>_N)))_R<br><br></div>-- Conal<br><div><blockquote>

</blockquote></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Mon, Apr 14, 2014 at 4:39 AM, Richard Eisenberg <span dir="ltr"><<a href="mailto:eir@cis.upenn.edu" target="_blank">eir@cis.upenn.edu</a>></span> wrote:<br>

<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word"><div>I agree with Simon, but just `Sub` the `<LambdaCCC.Lambda.EP>_N`, not the whole coercion.</div>

<div><br></div><div>There are actually two problems here. The one Simon identified, and also the fact that Simple.NTCo:HasIf[0] produces a representational coercion. How do I know? Because of the `NT` -- it's a newtype axiom and must produce representational coercions. Furthermore, unless the newtype definition is inferred to require a nominal parameter, the newtype would expect a representational coercion, not the nominal one you are passing. Check the dump (using -ddump-tc) of the newtype axiom to be sure.</div>

<div><br></div><div>Though putting a `Sub` on `<EP>` and changing the Refl constructor on `<Bool>` would work, you would then be violating an invariant of GHC's Coercion type: that we prefer `TyConAppCo tc ...` over `AppCo (Refl (TyConApp tc [])) ...`.</div>

<div><br></div><div>In sum, here is the coercion I think you want:</div><div><br></div><div>(LambdaCCC.Lambda.EP (Sym (Simple.NTCo:HasIf[0] <GHC.Types.Bool>_R)))_R</div><div><br></div><div>This is one of the problems with roles -- they are *very* fiddly within GHC, and it's hard for a non-expert in roles to get them right.</div>

<div><br></div><div>Have you seen docs/core-spec/core-spec.pdf? That is updated w.r.t. roles and may be of help.</div><div><br></div><div>Let me know if I can help further!</div><div>Richard</div><br><div><div><div class="h5">

<div>On Apr 14, 2014, at 5:45 AM, Simon Peyton Jones <<a href="mailto:simonpj@microsoft.com" target="_blank">simonpj@microsoft.com</a>> wrote:</div><br></div></div><blockquote type="cite"><div link="#0563C1" vlink="#954F72" style="font-family:Helvetica;font-size:medium;font-style:normal;font-variant:normal;font-weight:normal;letter-spacing:normal;line-height:normal;text-align:-webkit-auto;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px" lang="EN-GB">

<div><div class="h5"><div style="margin:0cm 0cm 0.0001pt;font-size:12pt;font-family:'Times New Roman',serif"><span style="font-family:Calibri,sans-serif;color:rgb(31,73,125)">I think you need a ‘Sub’.<u></u><u></u></span></div>

<div style="margin:0cm 0cm 0.0001pt;font-size:12pt;font-family:'Times New Roman',serif"><span style="font-family:Calibri,sans-serif;color:rgb(31,73,125)"> </span></div><div style="margin:0cm 0cm 0.0001pt;font-size:12pt;font-family:'Times New Roman',serif">

<span style="font-family:Calibri,sans-serif;color:rgb(31,73,125)">A cast  (e `cast` g) requires a representational coercion.  I think you have given it a (stronger) nominal one.  Sub gets from one to t’other.<u></u><u></u></span></div>

<div style="margin:0cm 0cm 0.0001pt;font-size:12pt;font-family:'Times New Roman',serif"><span style="font-family:Calibri,sans-serif;color:rgb(31,73,125)"> </span></div><div style="margin:0cm 0cm 0.0001pt;font-size:12pt;font-family:'Times New Roman',serif">

<span style="font-family:Calibri,sans-serif;color:rgb(31,73,125)">Simon<u></u><u></u></span></div><div style="margin:0cm 0cm 0.0001pt;font-size:12pt;font-family:'Times New Roman',serif"><span style="font-family:Calibri,sans-serif;color:rgb(31,73,125)"> </span></div>

<div style="border-style:none none none solid;border-left-width:1.5pt;border-left-color:blue;padding:0cm 0cm 0cm 4pt"><div><div style="border-style:solid none none;border-top-width:1pt;border-top-color:rgb(225,225,225);padding:3pt 0cm 0cm">

<div style="margin:0cm 0cm 0.0001pt;font-size:12pt;font-family:'Times New Roman',serif"><b><span style="font-size:11pt;font-family:Calibri,sans-serif" lang="EN-US">From:</span></b><span style="font-size:11pt;font-family:Calibri,sans-serif" lang="EN-US"><span> </span>Glasgow-haskell-users [mailto:<a href="mailto:glasgow-" target="_blank">glasgow-</a><a href="mailto:haskell-users-bounces@haskell.org" target="_blank">haskell-users-bounces@haskell.org</a>]<span> </span><b>On Behalf Of<span> </span></b>Conal Elliott<br>

<b>Sent:</b><span> </span>14 April 2014 06:00<br><b>To:</b><span> </span><a href="mailto:ghc-devs@haskell.org" target="_blank">ghc-devs@haskell.org</a>; <a href="mailto:glasgow-haskell-users@haskell.org" target="_blank">glasgow-haskell-users@haskell.org</a><br>

<b>Subject:</b><span> </span>Help with coercion & roles?<u></u><u></u></span></div></div></div><div style="margin:0cm 0cm 0.0001pt;font-size:12pt;font-family:'Times New Roman',serif"><u></u> <u></u></div><div><p class="MsoNormal" style="margin:0cm 0cm 6pt;font-size:12pt;font-family:'Times New Roman',serif">I’m working on a GHC plugin (as part of my Haskell-to-hardware work) and running into trouble with coercions & roles. Error message from Core Lint:<u></u><u></u></p>

<pre style="margin:0cm 0cm 0.0001pt 30pt;font-size:10pt;font-family:'Courier New'"><code style="font-family:'Courier New'">Warning: In the expression:<u></u><u></u></code></pre><pre style="margin:0cm 0cm 0.0001pt 30pt;font-size:10pt;font-family:'Courier New'">
<code style="font-family:'Courier New'"> </code></pre><pre style="margin:0cm 0cm 0.0001pt 30pt;font-size:10pt;font-family:'Courier New'"><code style="font-family:'Courier New'">  LambdaCCC.Lambda.lamvP#<u></u><u></u></code></pre>

<pre style="margin:0cm 0cm 0.0001pt 30pt;font-size:10pt;font-family:'Courier New'"><code style="font-family:'Courier New'">    @ (GHC.Types.Bool → GHC.Types.Bool → GHC.Types.Bool → GHC.Types.Bool)<u></u><u></u></code></pre>

<pre style="margin:0cm 0cm 0.0001pt 30pt;font-size:10pt;font-family:'Courier New'"><code style="font-family:'Courier New'">    @ (Simple.HasIf GHC.Types.Bool)<u></u><u></u></code></pre><pre style="margin:0cm 0cm 0.0001pt 30pt;font-size:10pt;font-family:'Courier New'">
<code style="font-family:'Courier New'">    "tpl"#<u></u><u></u></code></pre><pre style="margin:0cm 0cm 0.0001pt 30pt;font-size:10pt;font-family:'Courier New'"><code style="font-family:'Courier New'">    ((LambdaCCC.Lambda.varP#<u></u><u></u></code></pre>

<pre style="margin:0cm 0cm 0.0001pt 30pt;font-size:10pt;font-family:'Courier New'"><code style="font-family:'Courier New'">        @ (GHC.Types.Bool → GHC.Types.Bool → GHC.Types.Bool → GHC.Types.Bool)<u></u><u></u></code></pre>

<pre style="margin:0cm 0cm 0.0001pt 30pt;font-size:10pt;font-family:'Courier New'"><code style="font-family:'Courier New'">        "tpl"#)<u></u><u></u></code></pre><pre style="margin:0cm 0cm 0.0001pt 30pt;font-size:10pt;font-family:'Courier New'">
<code style="font-family:'Courier New'">     `cast` (<LambdaCCC.Lambda.EP>_N (Sym (Simple.NTCo:HasIf[0] <GHC.Types.Bool>_N))<u></u><u></u></code></pre><pre style="margin:0cm 0cm 0.0001pt 30pt;font-size:10pt;font-family:'Courier New'">
<code style="font-family:'Courier New'">             </code><code style="font-family:'Courier New'"><span style="font-family:'Cambria Math',serif">∷</span> LambdaCCC.Lambda.EP<u></u><u></u></code></pre>

<pre style="margin:0cm 0cm 0.0001pt 30pt;font-size:10pt;font-family:'Courier New'"><code style="font-family:'Courier New'">                  (GHC.Types.Bool<u></u><u></u></code></pre><pre style="margin:0cm 0cm 0.0001pt 30pt;font-size:10pt;font-family:'Courier New'">
<code style="font-family:'Courier New'">                   → GHC.Types.Bool → GHC.Types.Bool → GHC.Types.Bool)<u></u><u></u></code></pre><pre style="margin:0cm 0cm 0.0001pt 30pt;font-size:10pt;font-family:'Courier New'">
<code style="font-family:'Courier New'">                  ~#<u></u><u></u></code></pre><pre style="margin:0cm 0cm 0.0001pt 30pt;font-size:10pt;font-family:'Courier New'"><code style="font-family:'Courier New'">                LambdaCCC.Lambda.EP (Simple.HasIf GHC.Types.Bool)))<u></u><u></u></code></pre>

<pre style="margin:0cm 0cm 0.0001pt 30pt;font-size:10pt;font-family:'Courier New'"><code style="font-family:'Courier New'"> <u></u><u></u></code></pre><pre style="margin:0cm 0cm 0.0001pt 30pt;font-size:10pt;font-family:'Courier New'">
<code style="font-family:'Courier New'">Role incompatibility: expected nominal, got representational<u></u><u></u></code></pre><pre style="margin:0cm 0cm 0.0001pt 30pt;font-size:10pt;font-family:'Courier New'">
<code style="font-family:'Courier New'">in <LambdaCCC.Lambda.EP>_N (Sym (Simple.NTCo:HasIf[0] <GHC.Types.Bool>_N))</code><u></u><u></u></pre><p style="margin-right:0cm;margin-left:0cm;font-size:12pt;font-family:'Times New Roman',serif">

Do you see anything inconsistent/incompatible in the coercions or roles above? I constructed the nominal<span> </span><code style="font-family:'Courier New'"><span style="font-size:10pt">EP</span></code><span> </span><code style="font-family:'Courier New'"><span style="font-size:10pt">Refl</span></code><span> </span>coercion, and applied it (<code style="font-family:'Courier New'"><span style="font-size:10pt">AppCo</span></code>) an existing coercion of a simpler type.<u></u><u></u></p><p style="margin-right:0cm;margin-left:0cm;font-size:12pt;font-family:'Times New Roman',serif">Thanks,<u></u><u></u></p><div style="margin:0cm 0cm 0.0001pt;font-size:12pt;font-family:'Times New Roman',serif">

-- Conal<u></u><u></u></div></div></div></div></div>_______________________________________________<br>Glasgow-haskell-users mailing list<br><a href="mailto:Glasgow-haskell-users@haskell.org" target="_blank">Glasgow-haskell-users@haskell.org</a><br>

<a href="http://www.haskell.org/mailman/listinfo/glasgow-haskell-users" target="_blank">http://www.haskell.org/mailman/listinfo/glasgow-haskell-users</a></div></blockquote></div><br></div></blockquote></div><br></div>
</blockquote></div><br></body></html>