blob: 02de90ae1259c594dd0e90ac1d7b8e118147168e (
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
|
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds, PolyKinds #-}
{-# LANGUAGE TypeOperators #-}
module T15170 where
import Data.Kind
import Data.Proxy
data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
type f @@ x = Apply f x
infixl 9 @@
wat :: forall (a :: Type)
(b :: a ~> Type)
(c :: forall (x :: a). Proxy x ~> b @@ x ~> Type)
(f :: forall (x :: a) (y :: b @@ x). Proxy x ~> Proxy y ~> c @@ ('Proxy :: Proxy x) @@ y)
(x :: a).
(forall (xx :: a) (yy :: b @@ xx). Proxy (f @@ ('Proxy :: Proxy xx) @@ ('Proxy :: Proxy yy)))
-> ()
wat _ = ()
|
