Index a type with two Nats with "restricted proxy"

TwoNatsPseudoProxy.hs

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

import GHC.TypeLits
import Data.Proxy

data Foo (a :: Nat) (b :: Nat) :: * where Foo :: Foo a b

instance (KnownNat a, KnownNat b) => Show (Foo a b) where
    show Foo = "Foo :: Foo " ++ show (natVal (Proxy :: Proxy a)) ++ " " ++
               show (natVal (Proxy :: Proxy a))


bar :: Foo 1 2
bar = Foo

{-

λ> bar
Foo :: Foo 1 1
λ> :set -XDataKinds
λ> Foo :: Foo 1 1
Foo :: Foo 1 1

-}