Wibbles

tests/EqualitySpec.hs

@@ -33,6 +33,7 @@ spec = parallel $ do
 
 data instance Sing (z :: a :~: b) where
   SRefl :: Sing Refl
+type (%:~:) = (Sing :: (a :: k) :~: (b :: k) -> Type)
 
 instance SingKind (a :~: b) where
   type Demote (a :~: b) = a :~: b
@@ -50,6 +51,7 @@ instance SingI Refl where
 
 data instance Sing (z :: a :~~: b) where
   SHRefl :: Sing HRefl
+type (%:~~:) = (Sing :: (a :: j) :~~: (b :: k) -> Type)
 
 instance SingKind (a :~~: b) where
   type Demote (a :~~: b) = a :~~: b

tests/GADTSpec.hs

@@ -26,6 +26,7 @@ data So :: Bool -> Type where
 
 data instance Sing (z :: So what) where
   SOh :: Sing Oh
+type SSo = (Sing :: So what -> Type)
 
 elimSo :: forall (what :: Bool) (s :: So what) (p :: forall (long_sucker :: Bool). So long_sucker ~> Type).
           Sing s
@@ -40,6 +41,7 @@ data Flarble (a :: Type) (b :: Type) where
 data instance Sing (z :: Flarble a b) where
   SMkFlarble1 :: Sing x -> Sing (MkFlarble1 x)
   SMkFlarble2 :: Sing MkFlarble2
+type SFlarble = (Sing :: Flarble a b -> Type)
 
 elimFlarble :: forall (a :: Type) (b :: Type)
                       (p :: forall (x :: Type) (y :: Type). Flarble x y ~> Type)
@@ -60,6 +62,7 @@ data Obj :: Type where
 
 data instance Sing (z :: Obj) where
   SMkObj :: forall (obj :: obiwan). Sing obj -> Sing (MkObj obj)
+type SObj = (Sing :: Obj -> Type)
 
 elimObj :: forall (o :: Obj) (p :: Obj ~> Type).
            Sing o

tests/PeanoSpec.hs

@@ -1,6 +1,7 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
 module PeanoSpec where
 
 import Data.Kind
@@ -89,7 +90,7 @@ zipWithVec f = elimPeano @n @(WhyZipWithVecSym3 a b c) (sing @_ @n) base step
 
 appendVec :: forall (e :: Type) (n :: Peano) (m :: Peano).
              SingI n
-          => Vec e n -> Vec e m -> Vec e (Plus n m)
+          => Vec e n -> Vec e m -> Vec e (n `Plus` m)
 appendVec = elimPeano @n @(WhyAppendVecSym2 e m) (sing @_ @n) base step
   where
     base :: WhyAppendVec e m Z

tests/PeanoTypes.hs

@@ -17,10 +17,12 @@ import Data.Singletons.TH
 $(singletons [d|
   data Peano = Z | S Peano
 
+  infixl 6 `plus`
   plus :: Peano -> Peano -> Peano
   plus Z     m = m
   plus (S k) m = S (plus k m)
 
+  infixl 7 `times`
   times :: Peano -> Peano -> Peano
   times Z     _ = Z
   times (S k) m = plus m (times k m)
@@ -45,6 +47,7 @@ deriving instance Show a => Show (Vec a n)
 data instance Sing (z :: Vec a n) where
   SVNil :: Sing VNil
   (:%#) :: { sVhead :: Sing x, sVtail :: Sing xs } -> Sing (x :# xs)
+type SVec = (Sing :: Vec a n -> Type)
 infixr 5 :%#
 
 instance SingKind a => SingKind (Vec a n) where
@@ -82,15 +85,15 @@ type WhyZipWithVec (a :: Type) (b :: Type) (c :: Type) (n :: Peano)
 $(genDefunSymbols [''WhyZipWithVec])
 
 type WhyAppendVec (e :: Type) (m :: Peano) (n :: Peano)
-  = Vec e n -> Vec e m -> Vec e (Plus n m)
+  = Vec e n -> Vec e m -> Vec e (n `Plus` m)
 $(genDefunSymbols [''WhyAppendVec])
 
 type WhyTransposeVec (e :: Type) (m :: Peano) (n :: Peano)
   = Vec (Vec e m) n -> Vec (Vec e n) m
 $(genDefunSymbols [''WhyTransposeVec])
 
 type WhyConcatVec (e :: Type) (j :: Peano) (n :: Peano) (l :: Vec (Vec e j) n)
-  = Vec e (Times n j)
+  = Vec e (n `Times` j)
 data WhyConcatVecSym (e :: Type) (j :: Peano)
   :: forall (n :: Peano). Vec (Vec e j) n ~> Type
 type instance Apply (WhyConcatVecSym e j :: Vec (Vec e j) n ~> Type) l

tests/VecSpec.hs

@@ -30,7 +30,7 @@ spec = parallel $ do
 
 concatVec :: forall (e :: Type) (n :: Peano) (j :: Peano).
              (SingKind e, SingI j, e ~ Demote e)
-          => Vec (Vec e j) n -> Vec e (Times n j)
+          => Vec (Vec e j) n -> Vec e (n `Times` j)
 concatVec l = withSomeSing l $ \(singL :: Sing l) ->
                 elimVec @(Vec e j) @n @(WhyConcatVecSym e j) @l singL base step
   where