blob: e806e2a6a2064f686c5317767569dc3ce7b2b755 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
{-# LANGUAGE PolyKinds, DataKinds, TypeFamilies, ScopedTypeVariables, GADTs, RankNTypes #-}
module T9574 where
data KProxy (t :: *) = KProxy
data Proxy p
class Funct f where
type Codomain f :: *
instance Funct ('KProxy :: KProxy o) where
type Codomain 'KProxy = NatTr (Proxy :: o -> *)
data NatTr (c :: o -> *) where
M :: (forall (a :: o). Proxy a) -> NatTr (c :: o -> *)
p :: forall (c :: o -> *). NatTr c
p = M t where
M t = undefined :: Codomain ('KProxy :: KProxy o)
|
