Index a type with two nats using existential constraints/proxy args

TwoNatsExistential.hs

{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs, DataKinds #-}
module Foo where

import GHC.TypeLits
import Data.Type.Equality
import Data.Proxy

data Foo (a :: Nat) (b :: Nat) :: * where
     Foo :: (KnownNat a,KnownNat b) => Proxy a -> Proxy b -> Foo a b


instance Show (Foo a b) where
    show (Foo p1 p2) = "Foo (Proxy :: Proxy " ++ show (natVal p1) ++
                       ") (Proxy :: Proxy " ++ show (natVal p2) ++ ")"

bar :: Foo 1 2
bar = Foo Proxy Proxy


-- runtime type equality proof
castFoo :: Foo a b -> Foo c d -> Maybe (a :~: c , b :~: d)
castFoo (Foo pa pb) (Foo pc pd) = do
  pfac <- sameNat pa pc
  pfbd <- sameNat pb pd
  return (pfac,pfbd)


{-

λ> bar
Foo (Proxy :: Proxy 1) (Proxy :: Proxy 2)
λ> :set -XDataKinds
λ> Foo (Proxy :: Proxy 1) (Proxy :: Proxy 2)
Foo (Proxy :: Proxy 1) (Proxy :: Proxy 2)
 
-}