test.djinn

-- Use "uninterpreted" types to disallow pattern matching on constructors
type Seq :: * -> * -> *
type Tup :: * -> * -> *

-- This also doesn't work -- djinn treats them as Void
-- data Seq a b
-- data Tup a b

iden :: Seq a a
comp :: Seq a b -> Seq b c -> Seq a c
unit :: Seq a ()
injl :: Seq a b -> Seq a (Either b c)
injr :: Seq a c -> Seq a (Either b c)
case :: Seq (Tup a c) d -> Seq (Tup b c) d -> Seq (Tup (Either a b) c) d
pair :: Seq a b -> Seq a c -> Seq a (Tup b c)
take :: Seq a c -> Seq (Tup a b) c
drop :: Seq b c -> Seq (Tup a b) c

-- I'm trying to implement things like this
f ? Seq (Tup a c0) (Tup b c0) -> Seq (Tup a c1) (Tup c c1) -> Seq (Tup a (Tup c0 c1)) (Tup (Tup b c) (Tup c0 c1))
comp1 ? Seq (Tup a c0) (Tup b c0) -> Seq (Tup b c1) (Tup c c1) -> Seq (Tup a (Tup c0 c1)) (Tup c (Tup c0 c1))

-- djinn reports that iden' has a realizer, but iden'' does not
iden' ? Seq a a
iden'' ? Seq b b