[commit: testsuite] master: Test Trac #7786 (3a03187)

[Simon Peyton Jones]

Repository : ssh://darcs.haskell.org//srv/darcs/testsuite

On branch  : master

https://github.com/ghc/testsuite/commit/3a031876556cea3f52a6c8e41f0fb19c58f8c844

>---------------------------------------------------------------

commit 3a031876556cea3f52a6c8e41f0fb19c58f8c844
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Mon Apr 22 12:58:52 2013 +0100

    Test Trac #7786

>---------------------------------------------------------------

 tests/indexed-types/should_fail/T7786.hs     |   93 ++++++++++++++++++++++++++
 tests/indexed-types/should_fail/T7786.stderr |   24 +++++++
 tests/indexed-types/should_fail/all.T        |    1 +
 3 files changed, 118 insertions(+), 0 deletions(-)

diff --git a/tests/indexed-types/should_fail/T7786.hs b/tests/indexed-types/should_fail/T7786.hs
new file mode 100644
index 0000000..f2d119b
--- /dev/null
+++ b/tests/indexed-types/should_fail/T7786.hs
@@ -0,0 +1,93 @@
+{-# LANGUAGE GADTs, ConstraintKinds,
+             PolyKinds, KindSignatures, DataKinds, TypeOperators,
+             TypeFamilies, UndecidableInstances,
+             FlexibleContexts, ScopedTypeVariables #-}
+module T7786 where
+
+
+import GHC.TypeLits
+
+data Inventory a = Empty | More (Inventory a) a
+
+data instance Sing (l :: Inventory a) where
+  Nil :: Sing Empty
+  Snoc :: Sing bs -> Sing b -> Sing (More bs b)
+
+data KeySegment = Numic Nat | Symic Symbol
+
+data instance Sing (n :: KeySegment) where
+  Numic' :: Sing n -> Sing (Numic n)
+  Symic' :: Sing s -> Sing (Symic s)
+
+data instance Sing (k :: [KeySegment]) where
+  Root' :: Sing ('[] :: [KeySegment])
+  Symic'' :: Sing p -> Sing k -> Sing (Symic k ': p)
+  Numic'' :: Sing p -> Sing k -> Sing (Numic k ': p)
+
+type family Under (pre :: [KeySegment]) (post :: [KeySegment]) :: [KeySegment]
+type instance Under '[] post = post
+type instance Under (x ': xs) post = x ': xs `Under` post
+
+under :: Sing (pre :: [KeySegment]) -> Sing (post :: [KeySegment]) -> Sing (pre `Under` post)
+under Root' post = post
+under (Symic'' ks k) post = under ks post `Symic''` k
+under (Numic'' ks k) post = under ks post `Numic''` k
+
+data Database :: Inventory [KeySegment] -> * where
+  Clean :: Database Empty
+  Record :: (k `KeyNotIn` i) => Database i -> Sing k -> () -> Database (More i k)
+  Sub :: ((sub `UnderDisjoint` k) i) => Database i -> Sing k -> Database sub -> Database ((sub `BuriedUnder` k) i)
+
+dbKeys :: Database inv -> Sing inv
+dbKeys Clean = Nil
+dbKeys (Record db k _) = dbKeys db `Snoc` k
+dbKeys (Sub db k sub) = (dbKeys sub `buryUnder` k) (dbKeys db)
+
+buryUnder :: Sing sub -> Sing post -> Sing acc -> Sing ((sub `BuriedUnder` post) acc)
+buryUnder Nil _ acc = acc
+buryUnder (ps `Snoc` p) post acc = (ps `buryUnder` post) acc `Snoc` (p `under` post)
+
+type key `KeyNotIn` inv = Intersect (More Empty key) inv ~ Empty
+type (lhs `UnderDisjoint` post) rhs = Intersect ((lhs `BuriedUnder` post) Empty) rhs ~ Empty
+
+type family Intersect (l :: Inventory a) (r :: Inventory a) :: Inventory a
+type instance where
+  Intersect Empty r = Empty
+  Intersect l Empty = Empty
+  Intersect (More ls l) r = InterAppend (Intersect ls r) r l
+
+type family InterAppend (l :: Inventory a) 
+                        (r :: Inventory a) 
+                        (one :: a) 
+            :: Inventory a
+type instance where
+  InterAppend acc Empty one = acc
+  InterAppend acc (More rs one) one = More acc one
+  InterAppend acc (More rs r) one = InterAppend acc rs one
+
+type family BuriedUnder (sub :: Inventory [KeySegment]) 
+                        (post :: [KeySegment]) 
+                        (inv :: Inventory [KeySegment]) 
+            :: Inventory [KeySegment]
+type instance where
+  BuriedUnder Empty post inv = inv
+  BuriedUnder (More ps p) post inv = More ((ps `BuriedUnder` post) inv) (p `Under` post)
+
+
+intersectPaths :: Sing (lhs :: Inventory [KeySegment]) -> Sing (rhs :: Inventory [KeySegment]) -> Sing (lhs `Intersect` rhs)
+intersectPaths = undefined
+
+{- This foo is ambiguous
+foo :: Database inv
+    -> Sing post
+    -> Database sub
+    -> Sing (Intersect (BuriedUnder sub post 'Empty) rhs)
+foo db k sub = buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db
+-}
+
+addSub :: Database inv -> Sing k -> Database sub -> Maybe (Database ((sub `BuriedUnder` k) inv))
+addSub db k sub = do Nil :: Sing xxx <- return (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db)
+                     -- Nil :: Sing ((sub `BuriedUnder` k) Empty `Intersect` inv) <- return (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db)
+                     -- Nil :: Sing Empty <- return (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db)
+                     -- Nil <- return (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db)
+                     return $ Sub db k sub
diff --git a/tests/indexed-types/should_fail/T7786.stderr b/tests/indexed-types/should_fail/T7786.stderr
new file mode 100644
index 0000000..64febe6
--- /dev/null
+++ b/tests/indexed-types/should_fail/T7786.stderr
@@ -0,0 +1,24 @@
+
+T7786.hs:89:22:
+    Couldn't match type ‛Intersect
+                           [KeySegment] (BuriedUnder sub k ('Empty [KeySegment])) inv’
+                  with ‛'Empty [KeySegment]’
+    Inaccessible code in
+      a pattern with constructor
+        Nil :: forall (k :: BOX). Sing (Inventory k) ('Empty k),
+      in a pattern binding in
+           'do' block
+    Relevant bindings include
+      addSub :: Database inv
+                -> Sing [KeySegment] k
+                -> Database sub
+                -> Maybe (Database (BuriedUnder sub k inv))
+        (bound at T7786.hs:89:1)
+      db :: Database inv (bound at T7786.hs:89:8)
+      k :: Sing [KeySegment] k (bound at T7786.hs:89:11)
+      sub :: Database sub (bound at T7786.hs:89:13)
+    In the pattern: Nil
+    In the pattern: Nil :: Sing xxx
+    In a stmt of a 'do' block:
+      Nil :: Sing xxx <- return
+                           (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db)
diff --git a/tests/indexed-types/should_fail/all.T b/tests/indexed-types/should_fail/all.T
index 2b608f2..1ef4329 100644
--- a/tests/indexed-types/should_fail/all.T
+++ b/tests/indexed-types/should_fail/all.T
@@ -97,3 +97,4 @@ test('T7536', normal, compile_fail, [''])
 test('T7560', normal, compile_fail, [''])
 test('T7729', normal, compile_fail, [''])
 test('T7729a', normal, compile_fail, [''])
+test('T7786', normal, compile_fail, [''])