Testsuite error message changes
[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 GHC.TypeLits(Symbol,Nat)
8 data family Sing (a :: k)
9
10 data Inventory a = Empty | More (Inventory a) a
11
12 data instance Sing (l :: Inventory a) where
13 Nil :: Sing Empty
14 Snoc :: Sing bs -> Sing b -> Sing (More bs b)
15
16 data KeySegment = Numic Nat | Symic Symbol
17
18 data instance Sing (n :: KeySegment) where
19 Numic' :: Sing n -> Sing (Numic n)
20 Symic' :: Sing ss -> Sing (Symic ss)
21
22 data instance Sing (k :: [KeySegment]) where
23 Root' :: Sing ('[] :: [KeySegment])
24 Symic'' :: Sing p -> Sing k -> Sing (Symic k ': p)
25 Numic'' :: Sing p -> Sing k -> Sing (Numic k ': p)
26
27 type family Under (pre :: [KeySegment]) (post :: [KeySegment]) :: [KeySegment]
28 type instance Under '[] post = post
29 type instance Under (x ': xs) post = x ': xs `Under` post
30
31 under :: Sing (pre :: [KeySegment]) -> Sing (post :: [KeySegment]) -> Sing (pre `Under` post)
32 under Root' post = post
33 under (Symic'' ks k) post = under ks post `Symic''` k
34 under (Numic'' ks k) post = under ks post `Numic''` k
35
36 data Database :: Inventory [KeySegment] -> * where
37 Clean :: Database Empty
38 Record :: (k `KeyNotIn` i) => Database i -> Sing k -> () -> Database (More i k)
39 Sub :: ((sub `UnderDisjoint` k) i) => Database i -> Sing k -> Database sub -> Database ((sub `BuriedUnder` k) i)
40
41 dbKeys :: Database inv -> Sing inv
42 dbKeys Clean = Nil
43 dbKeys (Record db k _) = dbKeys db `Snoc` k
44 dbKeys (Sub db k sub) = (dbKeys sub `buryUnder` k) (dbKeys db)
45
46 buryUnder :: Sing sub -> Sing post -> Sing acc -> Sing ((sub `BuriedUnder` post) acc)
47 buryUnder Nil _ acc = acc
48 buryUnder (ps `Snoc` p) post acc = (ps `buryUnder` post) acc `Snoc` (p `under` post)
49
50 type key `KeyNotIn` inv = Intersect (More Empty key) inv ~ Empty
51 type (lhs `UnderDisjoint` post) rhs = Intersect ((lhs `BuriedUnder` post) Empty) rhs ~ Empty
52
53 type family Intersect (l :: Inventory a) (r :: Inventory a) :: Inventory a where
54 Intersect Empty r = Empty
55 Intersect l Empty = Empty
56 Intersect (More ls l) r = InterAppend (Intersect ls r) r l
57
58 type family InterAppend (l :: Inventory a)
59 (r :: Inventory a)
60 (one :: a)
61 :: Inventory a where
62 InterAppend acc Empty one = acc
63 InterAppend acc (More rs one) one = More acc one
64 InterAppend acc (More rs r) one = InterAppend acc rs one
65
66 type family BuriedUnder (sub :: Inventory [KeySegment])
67 (post :: [KeySegment])
68 (inv :: Inventory [KeySegment])
69 :: Inventory [KeySegment] where
70 BuriedUnder Empty post inv = inv
71 BuriedUnder (More ps p) post inv = More ((ps `BuriedUnder` post) inv) (p `Under` post)
72
73
74 intersectPaths :: Sing (lhs :: Inventory [KeySegment]) -> Sing (rhs :: Inventory [KeySegment]) -> Sing (lhs `Intersect` rhs)
75 intersectPaths = undefined
76
77 {- This foo is ambiguous
78 foo :: Database inv
79 -> Sing post
80 -> Database sub
81 -> Sing (Intersect (BuriedUnder sub post 'Empty) rhs)
82 foo db k sub = buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db
83 -}
84
85 addSub :: Database inv -> Sing k -> Database sub -> Maybe (Database ((sub `BuriedUnder` k) inv))
86 addSub db k sub = do Nil :: Sing xxx <- return (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db)
87 -- Nil :: Sing ((sub `BuriedUnder` k) Empty `Intersect` inv) <- return (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db)
88 -- Nil :: Sing Empty <- return (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db)
89 -- Nil <- return (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db)
90 return $ Sub db k sub