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

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.