Remove the incredibly hairy splitTelescopeTvs.
[ghc.git] / testsuite / tests / polykinds / T11821.hs
1 {-# LANGUAGE RankNTypes, DataKinds, PolyKinds, GADTs, TypeFamilies, UndecidableInstances #-}
2 module NotInScope where
3
4 import Data.Proxy
5
6 type KindOf (a :: k) = ('KProxy :: KProxy k)
7 data TyFun :: * -> * -> *
8 type family Apply (f :: TyFun k1 k2 -> *) (x :: k1) :: k2
9
10 data Lgo2 l1
11 l2
12 l3
13 (l4 :: b)
14 (l5 :: TyFun [a] b)
15 = forall (arg :: [a]) . KindOf (Apply (Lgo2 l1 l2 l3 l4) arg) ~ KindOf (Lgo l1 l2 l3 l4 arg) =>
16 Lgo2KindInference
17
18 data Lgo1 l1
19 l2
20 l3
21 (l4 :: TyFun b (TyFun [a] b -> *))
22 = forall (arg :: b) . KindOf (Apply (Lgo1 l1 l2 l3) arg) ~ KindOf (Lgo2 l1 l2 l3 arg) =>
23 Lgo1KindInference
24
25 type family Lgo f
26 z0
27 xs0
28 (a1 :: b)
29 (a2 :: [a]) :: b where
30 Lgo f z0 xs0 z '[] = z
31 Lgo f z0 xs0 z ('(:) x xs) = Apply (Apply (Lgo1 f z0 xs0) (Apply (Apply f z) x)) xs