强制和存在主义

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

为什么f编译但g生成如下错误？我正在使用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即使将它们嵌入GADT中,约束也是零成本吗？

UPD:编译器错误:https://ghc.haskell.org/trac/ghc/ticket/15431

Answer 1

作为解决方法，您可以用 a （在字典周围Data.Type.Coercion.Coercion添加一个额外的包装器）替换约束（这首先不是免费的） 。data

\n\n

data T t where\n  A :: Show (t a) => t a -> T t\n  B :: !(Coercion Int (t a)) -> t a -> T t\n    -- ! for correctness: you can\xe2\x80\x99t have wishy-washy values like B _|_ (I "a")\n    -- Such values decay to _|_\nf :: T t -> String\nf (A x) = show x\nf (B c x) = show (coerceWith (sym c) x)\n\nnewtype I a = I a\nmain = putStrLn $ f $ B Coercion $ I (5 :: Int)\n

\n\n

GHC 8.6 将从两个方面改善这种情况：

\n\n

\n

• 您的原始代码将可以工作，因为潜在的错误已得到修复。

\n

• Coercion可以将其解压缩到Coercible约束，并且由于 ，这将自动发生-funbox-small-strict-fields。因此，这个T将免费获得与原始版本相同的性能特征。

\n

\n