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 <[email protected]>wrote: > 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 <[email protected]> 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 <[email protected]>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 <[email protected]> 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 <[email protected]>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 <[email protected]> >>> 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- >>> [email protected]] *On Behalf Of *Conal Elliott >>> *Sent:* 14 April 2014 06:00 >>> *To:* [email protected]; [email protected] >>> *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 >>> [email protected] >>> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users >>> >>> >>> >> >> > >
_______________________________________________ Glasgow-haskell-users mailing list [email protected] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
