blob: ae724dcd7b9b63fea1094e0c07d583db1ed9a3f0 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
{-# LANGUAGE TypeFamilies, DataKinds, KindSignatures, TypeOperators #-}
module T10776 where
import GHC.TypeLits (Nat, Natural, Symbol, KnownNat)
import Data.Type.Equality ((:~:)(..))
import Data.Proxy
nat_is_natural :: Nat :~: Natural
nat_is_natural = Refl
data NatPair = TN Natural Natural
type X = TN 1 101
type family SecondNat (a :: NatPair) :: Nat where
SecondNat ('TN _ a) = a
|
