The World’s Largest Online Community for Developers

';
haskell - Coercible and existential - LavOzs.Com
haskell gadt coercion existential-type

```
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

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.

Related