Coercible and existential

Question

data T t where
  A :: Show (t a) => t a -> T t
  B :: Coercible Int (t a) => t a -> T t

f :: T t -> String
f (A t) = show t

g :: T t -> Int
g (B t) = coerce t

Why does f compile but g generate an error like follows? I'm using GHC 8.4.

• Couldn't match representation of type ‘Int’ with that of ‘t a’
  Inaccessible code in
    a pattern with constructor:
      B :: forall k (t :: k -> *) (a :: k).
           Coercible Int (t a) =>
           t a -> T t,
    in an equation for ‘g’
• In the pattern: B t
  In an equation for ‘g’: g (B t) = coerce t

Also, are Coercible constraints zero-cost even when they are embedded in GADTs?

UPD: Compiler bug: https://ghc.haskell.org/trac/ghc/ticket/15431

Newsome

The issue is that GHC doesn't know what how to use a Coercible Int (t a). The error message becomes a tiny bit clearer if you swap out Coercible Int (t a) for Int ~ t a. OTOH, something like Coercible [Int] (t a) is fine, since you are coercing from from type constructor to type constructor. – Deteriorate

g (B t) = 42 already triggers the error. It seems the issue lies in pattern matching, not in the use of coerce. Maybe, for some reason, the constraint is required in the pattern matching, instead of provided (as one would expect with GADTs)? – Spalding

@Spalding It’s not required, not directly. The compiler believes that the constraint is impossible and is saying that the entire equation is therefore unreachable. I think Alec is on to something: however GHC is checking the constraint may have confused representational equality with propositional equality (a bug). That is my hypothesis. – Imaginary

@Imaginary It is quite weird. Using Int triggers "Inaccessible code". Using Identity Int does that as well. Using [Int] instead is OK. Maybe GHC needs to know that t is representational, but there's no way to specify that. – Spalding

Answer 1

As a workaround, you may replace the constraint (which is not free in the first place) with a Data.Type.Coercion.Coercion (which adds an extra data wrapper around the dictionary).

data T t where
  A :: Show (t a) => t a -> T t
  B :: !(Coercion Int (t a)) -> t a -> T t
    -- ! for correctness: you can’t have wishy-washy values like B _|_ (I "a")
    -- Such values decay to _|_
f :: T t -> String
f (A x) = show x
f (B c x) = show (coerceWith (sym c) x)

newtype I a = I a
main = putStrLn $ f $ B Coercion $ I (5 :: Int)

GHC 8.6 will improve this situation in two ways:

• Your original code will work, as the underlying bug was fixed.

• The Coercion can be unpacked to a Coercible constraint, and this will happen automatically, due to -funbox-small-strict-fields. Thus, this T will get performance characteristics equivalent to your original for free.

Imaginary

I'd try to UNPACK that, hoping that it becomes free. I'm unsure about what would happen, though. – Spalding

@Spalding There is currently no way whatsoever to unpack a Coercible constraint. I opened a GHC proposal about that, but it's dormant. The Coercion itself will be unpacked by the default -funbox-small-strict-fields when compiling with optimization. – Barimah

@Barimah I don't think Coercion is unpacked. At least, an explicit {-# UNPACK #-} emits a "this does nothing" warning, so I can't see why -funbox-small-strict-fields would work. – Imaginary

@HTNW, Coercion should unpack to Coercible, which is not itself unpacked. The best way to check is to use -ddump-simpl and look at the code for the constructor wrapper. I'm pretty surprised by that warning. What version are you using? – Barimah

@Barimah 8.4.3, -O2. -Wall tells me the UNPACK is unusable. -ddump-simpl shows that the constructor wrapper takes a full Coercion, evaluates it, and stores it wholesale. EDIT: It works on HEAD. – Imaginary

Oh yes, I missed the fact that the former inability of GADTs to unpack (ever) affected Coercion too. There's still a restriction on existentials, but I think that can usually be worked around. – Barimah