{-# LINE 1 "src/Netw/Internal/Ancillary.hsc" #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE AllowAmbiguousTypes #-} module Netw.Internal.Ancillary where import GHC.TypeLits import Data.Proxy type UNIX_CONTROL_MESSAGE_RIGHTS = '(1, 1) {-# LINE 9 "src/Netw/Internal/Ancillary.hsc" #-} class KnownNatPair (p :: (Nat, Nat)) where {-# MINIMAL fstNatVal, sndNatVal | natPairVal #-} natPairVal :: (Integer, Integer) natPairVal = (forall (p :: (Nat, Nat)). KnownNatPair p => Integer fstNatVal @p, forall (p :: (Nat, Nat)). KnownNatPair p => Integer sndNatVal @p) fstNatVal :: Integer fstNatVal = (Integer, Integer) -> Integer forall a b. (a, b) -> a fst (forall (p :: (Nat, Nat)). KnownNatPair p => (Integer, Integer) natPairVal @p) sndNatVal :: Integer sndNatVal = (Integer, Integer) -> Integer forall a b. (a, b) -> b snd (forall (p :: (Nat, Nat)). KnownNatPair p => (Integer, Integer) natPairVal @p) instance (KnownNat a, KnownNat b) => KnownNatPair '(a, b) where fstNatVal :: Integer fstNatVal = forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Integer natVal @a Proxy a forall {k} (t :: k). Proxy t Proxy sndNatVal :: Integer sndNatVal = forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Integer natVal @b Proxy b forall {k} (t :: k). Proxy t Proxy