Switch to visible type applications

.github/workflows/ci.yml

@@ -13,6 +13,8 @@ jobs:
       - uses: actions/checkout@v2
 
       - uses: purescript-contrib/setup-purescript@main
+        with:
+          purescript: "unstable"
 
       - uses: actions/setup-node@v2
         with:

src/Data/FastVect/Common.purs

@@ -2,30 +2,40 @@ module Data.FastVect.Common
   ( Append
   , Cons
   , Drop
+  , DropP
   , Empty
   , Generate
+  , GenerateP
   , Head
   , HeadM
-  , Last
   , Index
   , IndexM
+  , IndexMP
   , IndexModulo
   , IndexModuloM
+  , IndexP
+  , Last
   , MapWithTerm
   , Modify
+  , ModifyP
   , NegOne
   , One
   , Replicate
+  , ReplicateP
   , Set
+  , SetP
   , Singleton
   , Snoc
   , Sparse
   , SplitAt
+  , SplitAtP
   , Take
+  , TakeP
   , Zero
   , class IsVect
   , term
   , toInt
+  , toIntP
   ) where
 
 import Data.Maybe (Maybe)
@@ -46,8 +56,11 @@ term :: forall (i :: Int). Proxy i
 term = Proxy
 
 -- | Convert a term to an Int
-toInt :: forall (len :: Int). Reflectable len Int => Proxy len -> Int
-toInt = reflectType
+toIntP :: forall (len :: Int). Reflectable len Int => Proxy len -> Int
+toIntP = reflectType
+
+toInt :: forall (@len :: Int). Reflectable len Int => Int
+toInt = reflectType (Proxy :: Proxy len)
 
 -- | Create a `Vect` by replicating `len` times the given element
 -- |
@@ -56,6 +69,12 @@ toInt = reflectType
 -- | vect = replicate (term :: _ 300) "a"
 -- | ```
 type Replicate vect len elem =
+  Compare len NegOne GT
+  => Reflectable len Int
+  => elem
+  -> vect len elem
+
+type ReplicateP vect len elem =
   Compare len NegOne GT
   => Reflectable len Int
   => Proxy len
@@ -122,6 +141,15 @@ type Append vect m n m_plus_n elem =
 -- | ```
 type Drop :: forall k. (Int -> k -> Type) -> Int -> Int -> Int -> k -> Type
 type Drop vect m n m_plus_n elem =
+  Add m n m_plus_n
+  => Reflectable m Int
+  => Compare m NegOne GT
+  => Compare n NegOne GT
+  => vect m_plus_n elem
+  -> vect n elem
+
+type DropP :: forall k. (Int -> k -> Type) -> Int -> Int -> Int -> k -> Type
+type DropP vect m n m_plus_n elem =
   Add m n m_plus_n
   => Reflectable m Int
   => Compare m NegOne GT
@@ -142,6 +170,15 @@ type Drop vect m n m_plus_n elem =
 -- | ```
 type Take :: forall k. (Int -> k -> Type) -> Int -> Int -> Int -> k -> Type
 type Take vect m n m_plus_n elem =
+  Add m n m_plus_n
+  => Reflectable m Int
+  => Compare m NegOne GT
+  => Compare n NegOne GT
+  => vect m_plus_n elem
+  -> vect m elem
+
+type TakeP :: forall k. (Int -> k -> Type) -> Int -> Int -> Int -> k -> Type
+type TakeP vect m n m_plus_n elem =
   Add m n m_plus_n
   => Reflectable m Int
   => Compare m NegOne GT
@@ -160,6 +197,15 @@ type Take vect m n m_plus_n elem =
 -- | newVect = modify (term :: _ 100) (append "b") vect
 -- | ```
 type Modify vect m n elem =
+  Reflectable m Int
+  => Compare m NegOne GT
+  => Compare n NegOne GT
+  => Compare m n LT
+  => (elem -> elem)
+  -> vect n elem
+  -> vect n elem
+
+type ModifyP vect m n elem =
   Reflectable m Int
   => Compare m NegOne GT
   => Compare n NegOne GT
@@ -179,6 +225,15 @@ type Modify vect m n elem =
 -- | newVect = modify (term :: _ 100) "b" vect
 -- | `
 type Set vect m n elem =
+  Reflectable m Int
+  => Compare m NegOne GT
+  => Compare n NegOne GT
+  => Compare m n LT
+  => elem
+  -> vect n elem
+  -> vect n elem
+
+type SetP vect m n elem =
   Reflectable m Int
   => Compare m NegOne GT
   => Compare n NegOne GT
@@ -202,6 +257,15 @@ type Set vect m n elem =
 -- | ```
 type SplitAt :: forall k. (Int -> k -> Type) -> Int -> Int -> Int -> k -> Type
 type SplitAt vect m n m_plus_n elem =
+  Add m n m_plus_n
+  => Reflectable m Int
+  => Compare m NegOne GT
+  => Compare n NegOne GT
+  => vect m_plus_n elem
+  -> { before :: vect m elem, after :: vect n elem }
+
+type SplitAtP :: forall k. (Int -> k -> Type) -> Int -> Int -> Int -> k -> Type
+type SplitAtP vect m n m_plus_n elem =
   Add m n m_plus_n
   => Reflectable m Int
   => Compare m NegOne GT
@@ -243,6 +307,14 @@ type IndexModuloM vect m elem =
 -- | elem = index (term :: _ 299) vect
 -- | ```
 type Index vect m n elem =
+  Reflectable m Int
+  => Compare m NegOne GT
+  => Compare n NegOne GT
+  => Compare m n LT
+  => vect n elem
+  -> elem
+
+type IndexP vect m n elem =
   Reflectable m Int
   => Compare m NegOne GT
   => Compare n NegOne GT
@@ -252,6 +324,14 @@ type Index vect m n elem =
   -> elem
 
 type IndexM vect m n elem =
+  Reflectable m Int
+  => Compare m NegOne GT
+  => Compare n NegOne GT
+  => Compare m n LT
+  => vect n elem
+  -> Maybe elem
+
+type IndexMP vect m n elem =
   Reflectable m Int
   => Compare m NegOne GT
   => Compare n NegOne GT
@@ -312,6 +392,18 @@ type Snoc vect len len_plus_1 elem =
   -> vect len_plus_1 elem
 
 type Generate vect m elem =
+  Reflectable m Int
+  => Compare m NegOne GT
+  => ( forall i
+        . Compare i NegOne GT
+       => Compare i m LT
+       => Reflectable i Int
+       => Proxy i
+       -> elem
+     )
+  -> vect m elem
+
+type GenerateP vect m elem =
   Reflectable m Int
   => Compare m NegOne GT
   => Proxy m