Re: Help with cast error

24 Apr 2014


      Thanks for the summary and paper pointer! I'll study up.  -- Conal


On Thu, Apr 24, 2014 at 12:58 AM, Simon Peyton Jones
wrote:
...
(a ~ b)  is a *boxed*, *nominal* equality.
(a ~R# b)  is an *unboxed, representational* equality
So it is rightly rejected.
For the boxed/unboxed thing, the paper “practical aspects…” gives more
detail.
http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/
I think you already know about the nominal/representational distinction.
Simon
*From:* Glasgow-haskell-users [mailto:
glasgow-haskell-users-bounces@haskell.org] *On Behalf Of *Conal Elliott
*Sent:* 24 April 2014 01:29
*To:* glasgow-haskell-users@haskell.org; ghc-devs@haskell.org; Richard
Eisenberg; Simon Peyton Jones
*Subject:* Help with cast error
I'd appreciate help with a cast-related Core Lint error I'm getting with a
GHC plugin I'm working on:
Argument value doesn't match argument type:
    Fun type:
        Enc (Vec ('S 'Z) Bool) ~ (Bool, ()) =>
        EP (Enc (Vec ('S 'Z) Bool)) -> EP (Bool, ())
    Arg type:
        ~R# (Enc (Vec ('S 'Z) Bool)) (Bool, ())
    Arg:
        CO Sub (TFCo:R:EncVec[0] <'Z>_N <Bool>_N)
           ; (Sub TFCo:R:EncBool[0], Sub (TFCo:R:EncVec0[0] <Bool>_N))_R
(I omitted the module prefixes for brevity.) Do I have a role wrong here,
or maybe something more fundamental?
I can easily supply more info if it'd help.
Thanks, -- Conal