blob: d79e66b93685c9ee15f5a11b8487d365c06f081d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
|
{-# LANGUAGE GADTs, DataKinds, KindSignatures, StandaloneDeriving, TypeOperators #-}
module T10348 where
import GHC.TypeLits
import Data.Typeable
import Data.Proxy
data Foo (n :: Nat) where
Hey :: KnownNat n => Foo n
deriving instance Show (Foo n)
data T t where
T :: (Show t, Typeable t) => t -> T t
deriving instance Show (T n)
hey :: KnownNat n => T (Foo n)
hey = T Hey
ho :: T (Foo 42)
ho = T Hey
f1 :: KnownNat a => Proxy a -> TypeRep
f1 = typeRep
g2 :: KnownSymbol a => Proxy a -> TypeRep
g2 = typeRep
pEqT :: (KnownSymbol a, KnownSymbol b) => Proxy a -> Proxy b -> Maybe (a :~: b)
pEqT Proxy Proxy = eqT
|
