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