{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

module QLinear.Index where

import Data.Proxy
import qualified GHC.Natural as Natural
import GHC.TypeNats

-- | Typesafe index. To construct it use TypeApplications
--
-- >>> Index @1 @3
-- Index 1 3
-- >>> :t Index @1 @3
-- Index @1 @3 :: Index 1 3
data Index (i :: Nat) (j :: Nat) = Index

instance forall i j. (KnownNat i, KnownNat j) => Show (Index i j) where
  show :: Index i j -> String
show _ = "Index " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Natural -> String
forall a. Show a => a -> String
show Natural
i String -> ShowS
forall a. Semigroup a => a -> a -> a
<> " " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Natural -> String
forall a. Show a => a -> String
show Natural
j
    where
      i :: Natural
i = Proxy i -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal (Proxy i
forall k (t :: k). Proxy t
Proxy @i)
      j :: Natural
j = Proxy j -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal (Proxy j
forall k (t :: k). Proxy t
Proxy @j)