RE: Help with coercion roles?
I think you need a ‘Sub’. 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. Simon From: Glasgow-haskell-users [mailto:glasgow-haskell-users-boun...@haskell.org] On Behalf Of Conal Elliott Sent: 14 April 2014 06:00 To: ghc-d...@haskell.org; glasgow-haskell-users@haskell.org Subject: Help with coercion roles? 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: Warning: In the expression: LambdaCCC.Lambda.lamvP# @ (GHC.Types.Bool → GHC.Types.Bool → GHC.Types.Bool → GHC.Types.Bool) @ (Simple.HasIf GHC.Types.Bool) tpl# ((LambdaCCC.Lambda.varP# @ (GHC.Types.Bool → GHC.Types.Bool → GHC.Types.Bool → GHC.Types.Bool) tpl#) `cast` (LambdaCCC.Lambda.EP_N (Sym (Simple.NTCo:HasIf[0] GHC.Types.Bool_N)) ∷ LambdaCCC.Lambda.EP (GHC.Types.Bool → GHC.Types.Bool → GHC.Types.Bool → GHC.Types.Bool) ~# LambdaCCC.Lambda.EP (Simple.HasIf GHC.Types.Bool))) Role incompatibility: expected nominal, got representational in LambdaCCC.Lambda.EP_N (Sym (Simple.NTCo:HasIf[0] GHC.Types.Bool_N)) Do you see anything inconsistent/incompatible in the coercions or roles above? I constructed the nominal EP Refl coercion, and applied it (AppCo) an existing coercion of a simpler type. Thanks, -- Conal ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Help with coercion roles?
I agree with Simon, but just `Sub` the `LambdaCCC.Lambda.EP_N`, not the whole coercion. 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. 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 [])) ...`. In sum, here is the coercion I think you want: (LambdaCCC.Lambda.EP (Sym (Simple.NTCo:HasIf[0] GHC.Types.Bool_R)))_R 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. Have you seen docs/core-spec/core-spec.pdf? That is updated w.r.t. roles and may be of help. Let me know if I can help further! Richard On Apr 14, 2014, at 5:45 AM, Simon Peyton Jones simo...@microsoft.com wrote: I think you need a ‘Sub’. 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. Simon From: Glasgow-haskell-users [mailto:glasgow-haskell-users-boun...@haskell.org] On Behalf Of Conal Elliott Sent: 14 April 2014 06:00 To: ghc-d...@haskell.org; glasgow-haskell-users@haskell.org Subject: Help with coercion roles? 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: Warning: In the expression: LambdaCCC.Lambda.lamvP# @ (GHC.Types.Bool → GHC.Types.Bool → GHC.Types.Bool → GHC.Types.Bool) @ (Simple.HasIf GHC.Types.Bool) tpl# ((LambdaCCC.Lambda.varP# @ (GHC.Types.Bool → GHC.Types.Bool → GHC.Types.Bool → GHC.Types.Bool) tpl#) `cast` (LambdaCCC.Lambda.EP_N (Sym (Simple.NTCo:HasIf[0] GHC.Types.Bool_N)) ∷ LambdaCCC.Lambda.EP (GHC.Types.Bool → GHC.Types.Bool → GHC.Types.Bool → GHC.Types.Bool) ~# LambdaCCC.Lambda.EP (Simple.HasIf GHC.Types.Bool))) Role incompatibility: expected nominal, got representational in LambdaCCC.Lambda.EP_N (Sym (Simple.NTCo:HasIf[0] GHC.Types.Bool_N)) Do you see anything inconsistent/incompatible in the coercions or roles above? I constructed the nominal EP Refl coercion, and applied it (AppCo) an existing coercion of a simpler type. Thanks, -- Conal ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Using Cabal to install terminfo-0.4.0.0 breaks GHC on Debian x86_64
I am using Debian, not Mac. It is possible the problem may be with the binary release for Debian x86_64, or it could just be my Cabal config file. When I install the binary distribution onto Debian, I simply run make install in the ghc-7.8.2 directory. I don't know how this install process the creates the GHC package registry, but after a fresh install, the output of the ghc-pkg list command shows that terminfo-0.4.0.0 is NOT installed even though there the /usr/local/lib/ghc-7.8.2/terminfo-0.4.0.0 directory clearly exists and is populated with the correct library files. But since it is not registered Cabal tries to re-build it and overwrites the existing terminfo-0.4.0.0 package. After a fresh install on Mac or Fedora, I wonder if terminfo-0.4.0.0 shows up in the GHC package registry? It could be the package registry for the Debian binary distribution missed that detail. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Using Cabal to install terminfo-0.4.0.0 breaks GHC on Debian x86_64
Hi Ramin,
Can I ask if you're installing packages into the global user database?
If so, that's definitely the way for this to happen - otherwise, Cabal
should never overwrite *anything* in the 'global' package directory
(in your case, under /usr/local/lib/ghc-7.8.2...) This is the only way
I can see this happening. In particular, installing 'terminfo' into my
local package database ('cabal install terminfo') works fine...
Carefully review your cabal configuration if you don't mind. You can
also always force the installation using '--user' when running cabal.
However, thank you very much for bringing this to my attention. What
you have discovered is a real brainfart I don't think we had
considered! The problem is that now that GHC is dynamically linked, we
*cannot* get away with lying about whether those packages are
installed - because they must install shared objects for GHC itself to
work. That means overwriting them by accident (because we don't think
they're installed) is a real possibility.
Relatedly, the NixOS Haskell users are suffering from the same problem
with 7.8.2 - http://lists.science.uu.nl/pipermail/nix-dev/2014-April/012992.html
- same problem, slightly different symptoms.
See https://ghc.haskell.org/trac/ghc/ticket/8919 for the ticket.
So this is definitely a real problem. I think scheduling the change
for 7.8.3 is correct.
My intuition tells me the fix might actually be quite simple - don't
lie about xhtml and terminfo being installed, and just be honest. Is
there any particular downside to doing this? I don't think so, *other*
than the fact it does mean terminfo has to come along when it's not
part of the Haskell Platform!
On Mon, Apr 14, 2014 at 7:08 AM, Ramin Honary ramin.hon...@gmail.com wrote:
I am using Debian, not Mac. It is possible the problem may be with the
binary release for Debian x86_64, or it could just be my Cabal config file.
When I install the binary distribution onto Debian, I simply run make
install in the ghc-7.8.2 directory. I don't know how this install process
the creates the GHC package registry, but after a fresh install, the output
of the ghc-pkg list command shows that terminfo-0.4.0.0 is NOT installed
even though there the /usr/local/lib/ghc-7.8.2/terminfo-0.4.0.0 directory
clearly exists and is populated with the correct library files. But since it
is not registered Cabal tries to re-build it and overwrites the existing
terminfo-0.4.0.0 package.
After a fresh install on Mac or Fedora, I wonder if terminfo-0.4.0.0 shows
up in the GHC package registry? It could be the package registry for the
Debian binary distribution missed that detail.
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
--
Regards,
Austin Seipp, Haskell Consultant
Well-Typed LLP, http://www.well-typed.com/
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: -optl behavior in ghc-7.8.1
On 10/04/2014 18:11, Yuras Shumovich wrote: On Thu, 2014-04-10 at 18:49 +0200, Karel Gardas wrote: On 04/10/14 06:39 PM, Yuras Shumovich wrote: ...and other linker options must come after, like in my case. So what? Are there any ticket where people complain about the old behavior? I'm not advocating any specific behavior, I'm just asking why it was changed. Hmm, I'm not sure if I'm the patch provider, but at least I provided patch which was merged into HEAD (don't have 7.8 branch here so check yourself) which fixes linking of binaries failure on Solaris. Please see b9b94ec82d9125da47c619c69e626120b3e60457 The core of the change is: -else package_hs_libs ++ extra_libs ++ other_flags +else other_flags ++ package_hs_libs ++ extra_libs Thank you for pointing to the commit. I hoped it was incidental change, but now I see the reason. Actually this was me: https://ghc.haskell.org/trac/ghc/changeset/1e2b3780ebc40d28cd0f029b90df102df09e6827/ghc The problem I was fixing was that we weren't always passing the -optl options. Now when we invoke a program the -optXXX options always come first - I think before it was kind of random and different for each of the phases. Cheers, Simon Thanks, Yuras the patch contains full explanation in comment so see it for more information. If this is not what bugs you, then please ignore me. Thanks, Karel ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users a ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: -optl behavior in ghc-7.8.1
On Mon, Apr 14, 2014 at 10:42 AM, Simon Marlow marlo...@gmail.com wrote: The problem I was fixing was that we weren't always passing the -optl options. Now when we invoke a program the -optXXX options always come first - I think before it was kind of random and different for each of the phases. Some things do need to come first, like that; but apparently we need either after-options or a more flexible library syntax. (Or an other-objects?) -- brandon s allbery kf8nh sine nomine associates allber...@gmail.com ballb...@sinenomine.net unix, openafs, kerberos, infrastructure, xmonadhttp://sinenomine.net ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Fwd: Using Cabal to install terminfo-0.4.0.0 breaks GHC on Debian x86_64
Hi, thanks for your reply.
Yes, I know for a fact I was installing to the global registry. All of my
Haskell projects depend on a few important packages, and I always install
these globally. For stuff I just want to play around with, I just install
into the user registry. Actually terminfo-0.4.0.0 is not something any of
my projects depend on, but I had installed it globally anyway and then this
problem occurred.
Also, the behavior Cabal installing Crypto-4.2.5.1 was odd. As I explained
in my first e-mail, some of the shared modules were being built with file
extensions of .hi instead of .dyn_hi, but the copy phase of the Cabal
installation was searching for files with .dyn_hi extensions and was
failing. And not all modules were being built incorrectly, some modules had
the correct .dyn_hi, others had just .hi. This may be a problem with
the Crypto.cabal file, however.
But anyway, the transition to using shared libraries by default has (in my
experience) caused just these two hiccups. I'm glad I was able to expose
this problem.
-- Ramin Honary
On Mon, Apr 14, 2014 at 10:07 PM, Austin Seipp aus...@well-typed.comwrote:
Hi Ramin,
Can I ask if you're installing packages into the global user database?
If so, that's definitely the way for this to happen - otherwise, Cabal
should never overwrite *anything* in the 'global' package directory
(in your case, under /usr/local/lib/ghc-7.8.2...) This is the only way
I can see this happening. In particular, installing 'terminfo' into my
local package database ('cabal install terminfo') works fine...
Carefully review your cabal configuration if you don't mind. You can
also always force the installation using '--user' when running cabal.
However, thank you very much for bringing this to my attention. What
you have discovered is a real brainfart I don't think we had
considered! The problem is that now that GHC is dynamically linked, we
*cannot* get away with lying about whether those packages are
installed - because they must install shared objects for GHC itself to
work. That means overwriting them by accident (because we don't think
they're installed) is a real possibility.
Relatedly, the NixOS Haskell users are suffering from the same problem
with 7.8.2 -
http://lists.science.uu.nl/pipermail/nix-dev/2014-April/012992.html
- same problem, slightly different symptoms.
See https://ghc.haskell.org/trac/ghc/ticket/8919 for the ticket.
So this is definitely a real problem. I think scheduling the change
for 7.8.3 is correct.
My intuition tells me the fix might actually be quite simple - don't
lie about xhtml and terminfo being installed, and just be honest. Is
there any particular downside to doing this? I don't think so, *other*
than the fact it does mean terminfo has to come along when it's not
part of the Haskell Platform!
On Mon, Apr 14, 2014 at 7:08 AM, Ramin Honary ramin.hon...@gmail.com
wrote:
I am using Debian, not Mac. It is possible the problem may be with the
binary release for Debian x86_64, or it could just be my Cabal config
file.
When I install the binary distribution onto Debian, I simply run make
install in the ghc-7.8.2 directory. I don't know how this install
process
the creates the GHC package registry, but after a fresh install, the
output
of the ghc-pkg list command shows that terminfo-0.4.0.0 is NOT
installed
even though there the /usr/local/lib/ghc-7.8.2/terminfo-0.4.0.0 directory
clearly exists and is populated with the correct library files. But
since it
is not registered Cabal tries to re-build it and overwrites the existing
terminfo-0.4.0.0 package.
After a fresh install on Mac or Fedora, I wonder if terminfo-0.4.0.0
shows
up in the GHC package registry? It could be the package registry for the
Debian binary distribution missed that detail.
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
--
Regards,
Austin Seipp, Haskell Consultant
Well-Typed LLP, http://www.well-typed.com/
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Help with coercion roles?
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: class HasIf a where ifThenElse :: Bool - a - a - a instance HasIf Bool where ifThenElse i t e = (i t) || (not i e) With `--dump-tc`, I see TYPE SIGNATURES TYPE CONSTRUCTORS HasIf :: * - Constraint class HasIf a Roles: [nominal] RecFlag NonRecursive ifThenElse :: Bool - a - a - a COERCION AXIOMS axiom Main.NTCo:HasIf :: HasIf a = Bool - a - a - a INSTANCES instance HasIf Bool -- Defined at ../test/HasIf.hs:4:10 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? My current formulation (tweaked to use `mkSubCo` and `mkAppCo`) is to apply `mkAppCo (mkSubCo (Refl Nominal ep))` to the given coercion, which then produces (LambdaCCC.Lambda.EP (Sym (Simple.NTCo:HasIf[0] GHC.Types.Bool_N)))_R And still I get Role incompatibility: expected nominal, got representational in `Sym (Simple.NTCo:HasIf[0] GHC.Types.Bool_N)`. I also tried wrapping `mkSubCo` around the entire coercion (applying `mkSubCo . mkAppCo (Refl Nominal ep)`), and I see the same result: (LambdaCCC.Lambda.EP (Sym (Simple.NTCo:HasIf[0] GHC.Types.Bool_N)))_R -- Conal On Mon, Apr 14, 2014 at 4:39 AM, Richard Eisenberg e...@cis.upenn.eduwrote: I agree with Simon, but just `Sub` the `LambdaCCC.Lambda.EP_N`, not the whole coercion. 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. 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 [])) ...`. In sum, here is the coercion I think you want: (LambdaCCC.Lambda.EP (Sym (Simple.NTCo:HasIf[0] GHC.Types.Bool_R)))_R 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. Have you seen docs/core-spec/core-spec.pdf? That is updated w.r.t. roles and may be of help. Let me know if I can help further! Richard On Apr 14, 2014, at 5:45 AM, Simon Peyton Jones simo...@microsoft.com wrote: I think you need a ‘Sub’. 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. Simon *From:* Glasgow-haskell-users [mailto:glasgow- haskell-users-boun...@haskell.org] *On Behalf Of *Conal Elliott *Sent:* 14 April 2014 06:00 *To:* ghc-d...@haskell.org; glasgow-haskell-users@haskell.org *Subject:* Help with coercion roles? 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: Warning: In the expression: LambdaCCC.Lambda.lamvP# @ (GHC.Types.Bool → GHC.Types.Bool → GHC.Types.Bool → GHC.Types.Bool) @ (Simple.HasIf GHC.Types.Bool) tpl# ((LambdaCCC.Lambda.varP# @ (GHC.Types.Bool → GHC.Types.Bool → GHC.Types.Bool → GHC.Types.Bool) tpl#) `cast` (LambdaCCC.Lambda.EP_N (Sym (Simple.NTCo:HasIf[0] GHC.Types.Bool_N)) ∷ LambdaCCC.Lambda.EP (GHC.Types.Bool → GHC.Types.Bool → GHC.Types.Bool → GHC.Types.Bool) ~# LambdaCCC.Lambda.EP (Simple.HasIf GHC.Types.Bool))) Role incompatibility: expected nominal, got representational in LambdaCCC.Lambda.EP_N (Sym (Simple.NTCo:HasIf[0] GHC.Types.Bool_N)) Do you see anything inconsistent/incompatible in the coercions or roles above? I constructed the nominal EP Refl coercion, and applied it (AppCo) an existing coercion of a simpler type. Thanks, -- Conal ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Help with coercion roles?
Hi Conal, 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. 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. 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.) Richard On Apr 14, 2014, at 2:23 PM, Conal Elliott co...@conal.net wrote: 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: class HasIf a where ifThenElse :: Bool - a - a - a instance HasIf Bool where ifThenElse i t e = (i t) || (not i e) With `--dump-tc`, I see TYPE SIGNATURES TYPE CONSTRUCTORS HasIf :: * - Constraint class HasIf a Roles: [nominal] RecFlag NonRecursive ifThenElse :: Bool - a - a - a COERCION AXIOMS axiom Main.NTCo:HasIf :: HasIf a = Bool - a - a - a INSTANCES instance HasIf Bool -- Defined at ../test/HasIf.hs:4:10 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? My current formulation (tweaked to use `mkSubCo` and `mkAppCo`) is to apply `mkAppCo (mkSubCo (Refl Nominal ep))` to the given coercion, which then produces (LambdaCCC.Lambda.EP (Sym (Simple.NTCo:HasIf[0] GHC.Types.Bool_N)))_R And still I get Role incompatibility: expected nominal, got representational in `Sym (Simple.NTCo:HasIf[0] GHC.Types.Bool_N)`. I also tried wrapping `mkSubCo` around the entire coercion (applying `mkSubCo . mkAppCo (Refl Nominal ep)`), and I see the same result: (LambdaCCC.Lambda.EP (Sym (Simple.NTCo:HasIf[0] GHC.Types.Bool_N)))_R -- Conal On Mon, Apr 14, 2014 at 4:39 AM, Richard Eisenberg e...@cis.upenn.edu wrote: I agree with Simon, but just `Sub` the `LambdaCCC.Lambda.EP_N`, not the whole coercion. 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. 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 [])) ...`. In sum, here is the coercion I think you want: (LambdaCCC.Lambda.EP (Sym (Simple.NTCo:HasIf[0] GHC.Types.Bool_R)))_R 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. Have you seen docs/core-spec/core-spec.pdf? That is updated w.r.t. roles and may be of help. Let me know if I can help further! Richard On Apr 14, 2014, at 5:45 AM, Simon Peyton Jones simo...@microsoft.com wrote: I think you need a ‘Sub’. 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. Simon From: Glasgow-haskell-users [mailto:glasgow-haskell-users-boun...@haskell.org] On Behalf Of Conal Elliott Sent: 14 April 2014 06:00 To: ghc-d...@haskell.org; glasgow-haskell-users@haskell.org Subject: Help with coercion roles? 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: Warning: In the expression: LambdaCCC.Lambda.lamvP# @ (GHC.Types.Bool → GHC.Types.Bool → GHC.Types.Bool → GHC.Types.Bool) @ (Simple.HasIf GHC.Types.Bool) tpl# ((LambdaCCC.Lambda.varP# @ (GHC.Types.Bool → GHC.Types.Bool → GHC.Types.Bool → GHC.Types.Bool) tpl#) `cast` (LambdaCCC.Lambda.EP_N (Sym (Simple.NTCo:HasIf[0] GHC.Types.Bool_N)) ∷ LambdaCCC.Lambda.EP (GHC.Types.Bool → GHC.Types.Bool → GHC.Types.Bool → GHC.Types.Bool) ~# LambdaCCC.Lambda.EP (Simple.HasIf GHC.Types.Bool))) Role incompatibility: expected nominal, got representational in LambdaCCC.Lambda.EP_N
Re: Help with coercion roles?
Hi Richard, I'm working on compiling Haskell to hardware, as outlined at https://github.com/conal/lambda-ccc/blob/master/doc/notes.md (with links to a few recent blog posts). The first step is to convert Core into other Core that evaluates to a reified form, represented as a type-parametrized GADT. This GADT (in `LambdaCCC.Lambda`): data E :: (* - *) - (* - *) where ... The parameter is also type-parametrized, and is for the primitives. I have such a type designed for hardware generation (in `LambdaCCC.Prim`) data Prim :: * - * where ... and then the combination of the two: type EP = E Prim So that's what `EP` is. With `-ddump-tc`, I get TYPE CONSTRUCTORS ... E :: (* - *) - * - * data E ($a::* - *) $b No C type associated Roles: [representational, nominal] RecFlag NonRecursive, Not promotable = ... EP :: * - * type EP = E Prim The use of `EP` rather than the more general `E` is only temporary, while I'm learning more details of Core (and of HERMIT which I'm using to manipulate Core). I'm now working on reification in the presence of casts. The rule I'm trying to implement is evalEP e | co -- evalEP (e | co'). Here, `evalEP :: EP a - a` and `co :: a ~ b`, so `co' :: EP a ~ EP b`. I'm trying to build `co'` from `co`, which led to these questions. So what do you think? Is there a sound coercion I can build for `co'`? -- Conal On Mon, Apr 14, 2014 at 11:54 AM, Richard Eisenberg e...@cis.upenn.eduwrote: Hi Conal, 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. 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. 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.) Richard On Apr 14, 2014, at 2:23 PM, Conal Elliott co...@conal.net wrote: 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: class HasIf a where ifThenElse :: Bool - a - a - a instance HasIf Bool where ifThenElse i t e = (i t) || (not i e) With `--dump-tc`, I see TYPE SIGNATURES TYPE CONSTRUCTORS HasIf :: * - Constraint class HasIf a Roles: [nominal] RecFlag NonRecursive ifThenElse :: Bool - a - a - a COERCION AXIOMS axiom Main.NTCo:HasIf :: HasIf a = Bool - a - a - a INSTANCES instance HasIf Bool -- Defined at ../test/HasIf.hs:4:10 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? My current formulation (tweaked to use `mkSubCo` and `mkAppCo`) is to apply `mkAppCo (mkSubCo (Refl Nominal ep))` to the given coercion, which then produces (LambdaCCC.Lambda.EP (Sym (Simple.NTCo:HasIf[0] GHC.Types.Bool_N)))_R And still I get Role incompatibility: expected nominal, got representational in `Sym (Simple.NTCo:HasIf[0] GHC.Types.Bool_N)`. I also tried wrapping `mkSubCo` around the entire coercion (applying `mkSubCo . mkAppCo (Refl Nominal ep)`), and I see the same result: (LambdaCCC.Lambda.EP (Sym (Simple.NTCo:HasIf[0] GHC.Types.Bool_N)))_R -- Conal On Mon, Apr 14, 2014 at 4:39 AM, Richard Eisenberg e...@cis.upenn.eduwrote: I agree with Simon, but just `Sub` the `LambdaCCC.Lambda.EP_N`, not the whole coercion. 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. 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 [])) ...`. In sum, here is the coercion I think you want: (LambdaCCC.Lambda.EP (Sym (Simple.NTCo:HasIf[0] GHC.Types.Bool_R)))_R 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. Have you seen docs/core-spec/core-spec.pdf? That is updated w.r.t. roles and may
Re: Help with coercion roles?
So what do you think? Is there a sound coercion I can build for `co'`? In a word, no. The problem is that E, as you describe, is a GADT. Therefore, it cares exactly which types it is parameterized by. We can see this in evidence in the dump, which labels E's second parameter as nominal. To draw out the problem, let's look at a simpler example: newtype Age = MkAge Int data G a where MkGInt :: G Int MkGAge :: G Age Here, `G` would similarly get a nominal role, because we can't lift representational coercions (such as NTCo:Age :: Age ~R Int) through the `G` type constructor. If we could, we could then have (MkGAge | ...) :: G Int, which goes against our definition of G -- the only value inhabitant of G Int should be MkGInt. The best you can do here is to try to raise the inner coercion to be nominal, by unSubCo_maybe. If that fails, I think you've gone beyond the ability of GHC's type system. Of course, I would like to help you with a way forward -- let me know if there's a way I can. Richard On Apr 14, 2014, at 4:12 PM, Conal Elliott co...@conal.net wrote: Hi Richard, I'm working on compiling Haskell to hardware, as outlined at https://github.com/conal/lambda-ccc/blob/master/doc/notes.md (with links to a few recent blog posts). The first step is to convert Core into other Core that evaluates to a reified form, represented as a type-parametrized GADT. This GADT (in `LambdaCCC.Lambda`): data E :: (* - *) - (* - *) where ... The parameter is also type-parametrized, and is for the primitives. I have such a type designed for hardware generation (in `LambdaCCC.Prim`) data Prim :: * - * where ... and then the combination of the two: type EP = E Prim So that's what `EP` is. With `-ddump-tc`, I get TYPE CONSTRUCTORS ... E :: (* - *) - * - * data E ($a::* - *) $b No C type associated Roles: [representational, nominal] RecFlag NonRecursive, Not promotable = ... EP :: * - * type EP = E Prim The use of `EP` rather than the more general `E` is only temporary, while I'm learning more details of Core (and of HERMIT which I'm using to manipulate Core). I'm now working on reification in the presence of casts. The rule I'm trying to implement is evalEP e | co -- evalEP (e | co'). Here, `evalEP :: EP a - a` and `co :: a ~ b`, so `co' :: EP a ~ EP b`. I'm trying to build `co'` from `co`, which led to these questions. So what do you think? Is there a sound coercion I can build for `co'`? -- Conal On Mon, Apr 14, 2014 at 11:54 AM, Richard Eisenberg e...@cis.upenn.edu wrote: Hi Conal, 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. 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. 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.) Richard On Apr 14, 2014, at 2:23 PM, Conal Elliott co...@conal.net wrote: 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: class HasIf a where ifThenElse :: Bool - a - a - a instance HasIf Bool where ifThenElse i t e = (i t) || (not i e) With `--dump-tc`, I see TYPE SIGNATURES TYPE CONSTRUCTORS HasIf :: * - Constraint class HasIf a Roles: [nominal] RecFlag NonRecursive ifThenElse :: Bool - a - a - a COERCION AXIOMS axiom Main.NTCo:HasIf :: HasIf a = Bool - a - a - a INSTANCES instance HasIf Bool -- Defined at ../test/HasIf.hs:4:10 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? My current formulation (tweaked to use `mkSubCo` and `mkAppCo`) is to apply `mkAppCo (mkSubCo (Refl Nominal ep))` to the given coercion, which then produces (LambdaCCC.Lambda.EP (Sym (Simple.NTCo:HasIf[0] GHC.Types.Bool_N)))_R And still I get Role incompatibility: expected nominal, got representational in `Sym (Simple.NTCo:HasIf[0] GHC.Types.Bool_N)`. I also tried wrapping `mkSubCo` around the entire coercion (applying `mkSubCo . mkAppCo (Refl Nominal ep)`), and I see the same result: (LambdaCCC.Lambda.EP (Sym (Simple.NTCo:HasIf[0] GHC.Types.Bool_N)))_R -- Conal On Mon, Apr 14, 2014 at 4:39 AM, Richard Eisenberg
Re: Help with coercion roles?
This explanation-with-example is very helpful. Thanks, Richard! I'll noodle some more. A fairly simple robust solution may be to add `Cast` to my expression GADT. -- Conal On Mon, Apr 14, 2014 at 2:02 PM, Richard Eisenberg e...@cis.upenn.eduwrote: So what do you think? Is there a sound coercion I can build for `co'`? In a word, no. The problem is that E, as you describe, is a GADT. Therefore, it cares exactly which types it is parameterized by. We can see this in evidence in the dump, which labels E's second parameter as nominal. To draw out the problem, let's look at a simpler example: newtype Age = MkAge Int data G a where MkGInt :: G Int MkGAge :: G Age Here, `G` would similarly get a nominal role, because we can't lift representational coercions (such as NTCo:Age :: Age ~R Int) through the `G` type constructor. If we could, we could then have (MkGAge | ...) :: G Int, which goes against our definition of G -- the only value inhabitant of G Int should be MkGInt. The best you can do here is to try to raise the inner coercion to be nominal, by unSubCo_maybe. If that fails, I think you've gone beyond the ability of GHC's type system. Of course, I would like to help you with a way forward -- let me know if there's a way I can. Richard On Apr 14, 2014, at 4:12 PM, Conal Elliott co...@conal.net wrote: Hi Richard, I'm working on compiling Haskell to hardware, as outlined at https://github.com/conal/lambda-ccc/blob/master/doc/notes.md (with links to a few recent blog posts). The first step is to convert Core into other Core that evaluates to a reified form, represented as a type-parametrized GADT. This GADT (in `LambdaCCC.Lambda`): data E :: (* - *) - (* - *) where ... The parameter is also type-parametrized, and is for the primitives. I have such a type designed for hardware generation (in `LambdaCCC.Prim`) data Prim :: * - * where ... and then the combination of the two: type EP = E Prim So that's what `EP` is. With `-ddump-tc`, I get TYPE CONSTRUCTORS ... E :: (* - *) - * - * data E ($a::* - *) $b No C type associated Roles: [representational, nominal] RecFlag NonRecursive, Not promotable = ... EP :: * - * type EP = E Prim The use of `EP` rather than the more general `E` is only temporary, while I'm learning more details of Core (and of HERMIT which I'm using to manipulate Core). I'm now working on reification in the presence of casts. The rule I'm trying to implement is evalEP e | co -- evalEP (e | co'). Here, `evalEP :: EP a - a` and `co :: a ~ b`, so `co' :: EP a ~ EP b`. I'm trying to build `co'` from `co`, which led to these questions. So what do you think? Is there a sound coercion I can build for `co'`? -- Conal On Mon, Apr 14, 2014 at 11:54 AM, Richard Eisenberg e...@cis.upenn.eduwrote: Hi Conal, 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. 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. 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.) Richard On Apr 14, 2014, at 2:23 PM, Conal Elliott co...@conal.net wrote: 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: class HasIf a where ifThenElse :: Bool - a - a - a instance HasIf Bool where ifThenElse i t e = (i t) || (not i e) With `--dump-tc`, I see TYPE SIGNATURES TYPE CONSTRUCTORS HasIf :: * - Constraint class HasIf a Roles: [nominal] RecFlag NonRecursive ifThenElse :: Bool - a - a - a COERCION AXIOMS axiom Main.NTCo:HasIf :: HasIf a = Bool - a - a - a INSTANCES instance HasIf Bool -- Defined at ../test/HasIf.hs:4:10 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? My current formulation (tweaked to use `mkSubCo` and `mkAppCo`) is to apply `mkAppCo (mkSubCo (Refl Nominal ep))` to the given coercion, which then produces (LambdaCCC.Lambda.EP (Sym (Simple.NTCo:HasIf[0] GHC.Types.Bool_N)))_R And still I get Role incompatibility: expected nominal, got representational in `Sym (Simple.NTCo:HasIf[0] GHC.Types.Bool_N)`. I also tried wrapping `mkSubCo` around the entire coercion (applying
