(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