Assert that a data constructor is injective

Question

I have the following datatype:

{-# 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 .... -}

Then I have a Num instance:

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

Of course this doesn't work. The type a is hidden by the constructor, because the type of Var is forall (i :: Nat) a. Num a => a -> Var i. Also note, the Var constructor isn't intended to be used directly; Vars are created by a smart constructor that guarantees Var i0 ~ Var i1 => a0 ~ a1. The type of the Var can't be Var i a; the point is to hide the type from the user.

How can I tell the type system, what I've 'proven' to be true, namely that Var i0 ~ Var i1 => a0 ~ a1. Currently I'm using unsafeCoerce:

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

I realize that unsafeCoerce is in an assertion that two types are equal, but I would like to try and make this assertion on the type level, so that exporting the constructor isn't unsafe. By unsafe I mean the following is possible:

>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

Answer 1

A possible way you can convince the typesystem is by providing the mapping function Of :: i -> a at type level. This trivially satisfies that if i ~ i' => Of i ~ Of i'. Here is the modified version of your program

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

import GHC.TypeLits
import Unsafe.Coerce

type family Of :: Nat -> *

data Var (i :: Nat) where
    Var :: (Num (Of i), Integral (Of i)) => (Of i) -> Var i

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

The drawback of this is you have to provide the explicit mapping. There might be more elegant way of capturing your constraint at type level and I am waiting to see more enlightened people giving insight into that.