blob: 915ad7e7dd0f44199c4441cc9f70eae31f3fff02 (
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
|
{-# Language RankNTypes, PatternSynonyms, TypeOperators, DataKinds, PolyKinds, KindSignatures, GADTs #-}
module T15694 where
import Data.Kind
import Data.Type.Equality
data Ctx :: Type -> Type where
E :: Ctx(Type)
(:&:) :: a -> Ctx(as) -> Ctx(a -> as)
data ApplyT(kind::Type) :: kind -> Ctx(kind) -> Type where
AO :: a -> ApplyT(Type) a E
AS :: ApplyT(ks) (f a) ctx
-> ApplyT(k -> ks) f (a:&:ctx)
pattern ASSO :: () => forall ks k (f :: k -> ks) (a1 :: k) (ctx :: Ctx ks)
(ks1 :: Type) k1 (a2 :: k1) (ctx1 :: Ctx ks1) a3.
(kind ~ (k -> ks), a ~~ f, b ~~ (a1 :&: ctx),
ks ~ (k1 -> ks1), ctx ~~ (a2 :&: E),
ks1 ~ Type, f a1 a2 ~~ a3)
=> a3 -> ApplyT kind a b
pattern ASSO a = AS (AS (AO a))
|
