LeibnizForGADT.hs

{-# LANGUAGE GADTs, TypeOperators, ScopedTypeVariables #-}
import Data.Eq.Type

data Expr e a where
    Sum :: Expr x Int -> Expr [x] Int

-- | This is almost ADT, x is existential.
data Expr' e a where
    Sum' :: [x] := e -> Int := a -> Expr' x a -> Expr' e a

fromExpr :: Expr e a -> Expr' e a
fromExpr (Sum e) = Sum' refl refl (fromExpr e)

toExpr :: forall e a. Expr' e a -> Expr e a
toExpr (Sum' proofE proofA e) = coerceBack $ Sum (coerceFwd $ toExpr e)
  where
    coerceBack = coerce (lift2' proofE proofA)
    coerceFwd  = coerce (lift2' refl (symm proofA))