Embrace -XTypeInType, add -XStarIsType
[ghc.git] / testsuite / tests / indexed-types / should_fail / T7786.hs
1 {-# LANGUAGE GADTs, ConstraintKinds,
2 PolyKinds, KindSignatures, DataKinds, TypeOperators,
3 TypeFamilies, UndecidableInstances,
4 FlexibleContexts, ScopedTypeVariables #-}
5 module T7786 where
6
7 import Data.Kind (Type)
8 import GHC.TypeLits(Symbol,Nat)
9
10 data family Sing (a :: k)
11
12 data Inventory a = Empty | More (Inventory a) a
13
14 data instance Sing (l :: Inventory a) where
15 Nil :: Sing Empty
16 Snoc :: Sing bs -> Sing b -> Sing (More bs b)
17
18 data KeySegment = Numic Nat | Symic Symbol
19
20 data instance Sing (n :: KeySegment) where
21 Numic' :: Sing n -> Sing (Numic n)
22 Symic' :: Sing ss -> Sing (Symic ss)
23
24 data instance Sing (k :: [KeySegment]) where
25 Root' :: Sing ('[] :: [KeySegment])
26 Symic'' :: Sing p -> Sing k -> Sing (Symic k ': p)
27 Numic'' :: Sing p -> Sing k -> Sing (Numic k ': p)
28
29 type family Under (pre :: [KeySegment]) (post :: [KeySegment]) :: [KeySegment]
30 type instance Under '[] post = post
31 type instance Under (x ': xs) post = x ': xs `Under` post
32
33 under :: Sing (pre :: [KeySegment]) -> Sing (post :: [KeySegment]) -> Sing (pre `Under` post)
34 under Root' post = post
35 under (Symic'' ks k) post = under ks post `Symic''` k
36 under (Numic'' ks k) post = under ks post `Numic''` k
37
38 data Database :: Inventory [KeySegment] -> Type where
39 Clean :: Database Empty
40 Record :: (k `KeyNotIn` i) => Database i -> Sing k -> () -> Database (More i k)
41 Sub :: ((sub `UnderDisjoint` k) i) => Database i -> Sing k -> Database sub -> Database ((sub `BuriedUnder` k) i)
42
43 dbKeys :: Database inv -> Sing inv
44 dbKeys Clean = Nil
45 dbKeys (Record db k _) = dbKeys db `Snoc` k
46 dbKeys (Sub db k sub) = (dbKeys sub `buryUnder` k) (dbKeys db)
47
48 buryUnder :: Sing sub -> Sing post -> Sing acc -> Sing ((sub `BuriedUnder` post) acc)
49 buryUnder Nil _ acc = acc
50 buryUnder (ps `Snoc` p) post acc = (ps `buryUnder` post) acc `Snoc` (p `under` post)
51
52 type key `KeyNotIn` inv = Intersect (More Empty key) inv ~ Empty
53 type (lhs `UnderDisjoint` post) rhs = Intersect ((lhs `BuriedUnder` post) Empty) rhs ~ Empty
54
55 type family Intersect (l :: Inventory a) (r :: Inventory a) :: Inventory a where
56 Intersect Empty r = Empty
57 Intersect l Empty = Empty
58 Intersect (More ls l) r = InterAppend (Intersect ls r) r l
59
60 type family InterAppend (l :: Inventory a)
61 (r :: Inventory a)
62 (one :: a)
63 :: Inventory a where
64 InterAppend acc Empty one = acc
65 InterAppend acc (More rs one) one = More acc one
66 InterAppend acc (More rs r) one = InterAppend acc rs one
67
68 type family BuriedUnder (sub :: Inventory [KeySegment])
69 (post :: [KeySegment])
70 (inv :: Inventory [KeySegment])
71 :: Inventory [KeySegment] where
72 BuriedUnder Empty post inv = inv
73 BuriedUnder (More ps p) post inv = More ((ps `BuriedUnder` post) inv) (p `Under` post)
74
75
76 intersectPaths :: Sing (lhs :: Inventory [KeySegment]) -> Sing (rhs :: Inventory [KeySegment]) -> Sing (lhs `Intersect` rhs)
77 intersectPaths = undefined
78
79 {- This foo is ambiguous
80 foo :: Database inv
81 -> Sing post
82 -> Database sub
83 -> Sing (Intersect (BuriedUnder sub post 'Empty) rhs)
84 foo db k sub = buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db
85 -}
86
87 foogle :: Database inv
88 -> Sing post
89 -> Database sub
90 -> Maybe (Sing (Intersect (BuriedUnder sub post 'Empty) inv))
91
92 foogle db k sub = return (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db)
93
94
95 addSub :: Database inv -> Sing k -> Database sub -> Maybe (Database ((sub `BuriedUnder` k) inv))
96 addSub db k sub = do Nil :: Sing xxx <- foogle db k sub
97 return $ Sub db k sub
98
99 {-
100 addSub :: Database inv -> Sing k -> Database sub -> Maybe (Database ((sub `BuriedUnder` k) inv))
101 addSub db k sub = do Nil :: Sing xxx <- foogle db sub k
102 -- Nil :: Sing ((sub `BuriedUnder` k) Empty `Intersect` inv) <- return (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db)
103 -- Nil :: Sing Empty <- return (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db)
104 -- Nil <- return (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db)
105 return $ Sub db k sub
106 -}