Generalize Exists to hold non-Type-kinded types

CHANGELOG.md

@@ -9,6 +9,7 @@ Breaking changes:
 
 New features:
 - Added roles declarations to allow safe coercions (#9) 
+- Generalized `Exists` to hold non-`Type`-kinded types (#14)
 
 Bugfixes:
 

src/Data/Exists.purs

@@ -2,7 +2,7 @@ module Data.Exists where
 
 import Unsafe.Coerce (unsafeCoerce)
 
--- | This type constructor can be used to existentially quantify over a type of kind `Type`.
+-- | This type constructor can be used to existentially quantify over a type.
 -- |
 -- | Specifically, the type `Exists f` is isomorphic to the existential type `exists a. f a`.
 -- |
@@ -24,7 +24,7 @@ import Unsafe.Coerce (unsafeCoerce)
 -- | ```purescript
 -- | type Stream a = Exists (StreamF a)
 -- | ```
-foreign import data Exists :: (Type -> Type) -> Type
+foreign import data Exists :: forall k. (k -> Type) -> Type
 
 type role Exists representational
 

test/Test/Main.purs

@@ -25,5 +25,24 @@ head = runExists head'
   head' :: forall s. StreamF a s -> a
   head' (StreamF s f) = snd (f s)
 
+data Maybe a = Nothing | Just a
+
+count :: forall a. Maybe a -> Int
+count Nothing = 0
+count _ = 1
+
+data FooF f = FooF (forall a. f a -> Int) (f String)
+
+type Foo = Exists FooF
+
+foo :: Foo
+foo = mkExists $ FooF count (Just "test")
+
+x :: Int
+x = runExists runFooF foo
+  where
+  runFooF :: forall f. FooF f -> Int
+  runFooF (FooF f fStr) = f fStr
+
 main :: Effect Unit
 main = logShow $ head nats