haskell - データ コンストラクターが単射であることをアサートする

Question

次のデータ型があります。

{-# LANGUAGE GADTs, KindSignatures, ScopedTypeVariables, DataKinds #-}

import GHC.TypeLits
import Unsafe.Coerce

data Var (i :: Nat) where
    Var :: (Num a, Integral a) => a -> Var i
    {- other constructors .... -}

次に、Numインスタンスがあります。

instance Num (Var i) where
    (Var a) + (Var b) = Var (a + b)

もちろん、これはうまくいきません。の型は であるため、型はaコンストラクターによって隠されています。また、コンストラクターは直接使用することを意図していないことに注意してください。s は、 を保証するスマート コンストラクターによって作成されます。Var の型を にすることはできません。ポイントは、タイプをユーザーから隠すことです。Varforall (i :: Nat) a. Num a => a -> Var iVarVarVar i0 ~ Var i1 => a0 ~ a1Var i a

型システムに、私が真であると「証明」したこと、つまりそれをどのように伝えることができますかVar i0 ~ Var i1 => a0 ~ a1。現在私は使用していunsafeCoerceます：

(Var (a :: n)) + (Var b) = Var (a + (unsafeCoerce b :: n))

unsafeCoerce2 つの型が等しいというアサーションであることは理解していますが、コンストラクターのエクスポートが危険にならないように、このアサーションを型レベルで試してみたいと思います。安全でないということは、次のことが可能であることを意味します。

>instance Show (Var i) where {show (Var a) = "Var " ++ show a}
>import Data.Word
>Var (1000 :: Word16) + Var (255 :: Word8)
Var 1255
>Var (255 :: Word8) + Var (1000 :: Word16)
Var 231