The World’s Largest Online Community for Developers
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
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
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.
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.