Commit 0bfd104f authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Test Trac #7786

parent 0edc55b7
{-# 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
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)
......@@ -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, [''])
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment