eliminators 0.4.1 → 0.5

raw patch · 14 files changed

+209/−160 lines, 14 filesdep ~basedep ~singleton-natsdep ~singletonsPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: base, singleton-nats, singletons, template-haskell, th-desugar

API changes (from Hackage documentation)

Files

• CHANGELOG.md +3/−0
• eliminators.cabal +14/−13
• src/Data/Eliminator.hs +4/−3
• src/Data/Eliminator/TH.hs +13/−11
• src/Data/Eliminator/TypeNats.hs +5/−4
• tests/DecideSpec.hs +2/−1
• tests/DecideTypes.hs +2/−1
• tests/EqualitySpec.hs +43/−115
• tests/EqualityTypes.hs +104/−0
• tests/GADTSpec.hs +2/−1
• tests/ListSpec.hs +4/−3
• tests/ListTypes.hs +2/−1
• tests/VecSpec.hs +8/−6
• tests/VecTypes.hs +3/−1

@@ -1,3 +1,6 @@+## 0.5 [2018.09.18]+* Require `singletons-2.5` and GHC 8.6.+ ### 0.4.1 [2018.02.13] * Add `elimVoid` to `Data.Eliminator`. 

@@ -1,5 +1,5 @@ name:                eliminators-version:             0.4.1+version:             0.5 synopsis:            Dependently typed elimination functions using singletons description:         This library provides eliminators for inductive data types,                      leveraging the power of the @singletons@ library to allow@@ -16,7 +16,7 @@ build-type:          Simple extra-source-files:  CHANGELOG.md, README.md cabal-version:       >=1.10-tested-with:         GHC == 8.4.1+tested-with:         GHC == 8.6.1  source-repository head   type:                git@@ -26,13 +26,13 @@   exposed-modules:     Data.Eliminator                        Data.Eliminator.TH                        Data.Eliminator.TypeNats-  build-depends:       base             >= 4.11    && < 4.12-                     , extra            >= 1.4.2   && < 1.7-                     , singletons       >= 2.4.1   && < 2.5-                     , singleton-nats   >= 0.4.0.4 && < 0.5-                     , template-haskell >= 2.13    && < 2.14-                     , th-abstraction   >= 0.2.3   && < 0.3-                     , th-desugar       >= 1.8     && < 1.9+  build-depends:       base             >= 4.12  && < 4.13+                     , extra            >= 1.4.2 && < 1.7+                     , singletons       >= 2.5   && < 2.6+                     , singleton-nats   >= 0.4.2 && < 0.5+                     , template-haskell >= 2.14  && < 2.15+                     , th-abstraction   >= 0.2.3 && < 0.3+                     , th-desugar       >= 1.9   && < 1.10   hs-source-dirs:      src   default-language:    Haskell2010   ghc-options:         -Wall -Wno-unticked-promoted-constructors@@ -43,16 +43,17 @@   other-modules:       DecideSpec                        DecideTypes                        EqualitySpec+                       EqualityTypes                        GADTSpec                        ListSpec                        ListTypes                        VecTypes                        VecSpec-  build-depends:       base           >= 4.11    && < 4.12+  build-depends:       base           >= 4.12  && < 4.13                      , eliminators-                     , hspec          >= 2       && < 3-                     , singletons     >= 2.4.1   && < 2.5-                     , singleton-nats >= 0.4.0.4 && < 0.5+                     , hspec          >= 2     && < 3+                     , singletons     >= 2.5   && < 2.6+                     , singleton-nats >= 0.4.2 && < 0.5   build-tool-depends:  hspec-discover:hspec-discover   hs-source-dirs:      tests   default-language:    Haskell2010

@@ -1,15 +1,16 @@ {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-} {-# LANGUAGE EmptyCase #-} {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE GADTs #-}+{-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE Trustworthy #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} {-| Module:      Data.Eliminator@@ -55,9 +56,9 @@ {- $eliminators  These eliminators are defined with propositions of kind @\<Datatype\> ~> 'Type'@-(that is, using the '(~>)' kind). These eliminators are designed for+(that is, using the @('~>')@ kind). These eliminators are designed for defunctionalized (i.e., \"partially applied\") types as predicates,-and as a result, the predicates must be applied manually with '(@@)'.+and as a result, the predicates must be applied manually with 'Apply'.  The naming conventions are: 

@@ -46,11 +46,11 @@ @ elimMyList :: forall (a :: 'Type') (p :: MyList a '~>' 'Type') (l :: MyList a).               'Sing' l-           -> p '@@' MyNil+           -> 'Apply' p MyNil            -> (forall (x :: a). 'Sing' x-                -> forall (xs :: MyList a). 'Sing' xs -> p '@@' xs-                -> p '@@' (MyCons x xs))-           -> p '@@' l+                -> forall (xs :: MyList a). 'Sing' xs -> 'Apply' p xs+                -> 'Apply' p (MyCons x xs))+           -> 'Apply' p l elimMyList SMyNil pMyNil _ = pMyNil elimMyList (SMyCons (x' :: 'Sing' x) (xs' :: 'Sing' xs)) pMyNil pMyCons   = pMyCons x' xs' (elimMyList \@a \@p \@xs pMyNil pMyCons)@@ -82,7 +82,7 @@        in a second.    The return type is the predicate type variable applied to the data type-  (@p '@@' (MyCons x xs)@, the above example).+  (@'Apply' p (MyCons x xs)@, the above example).    The type of each constructor argument also follows certain conventions: @@ -96,20 +96,24 @@        explained using the above example. In the @MyCons@ constructor, the second        field (of type @MyCons a@) is a recursive occurrence of @MyCons@, so        that corresponds to the type-       @forall (xs :: MyList a). 'Sing' xs -> p '@@' xs@, where @p '@@' xs@+       @forall (xs :: MyList a). 'Sing' xs -> 'Apply' p xs@, where @'Apply' p xs@        is only present due to the recursion.      3. Finally, the return type will be the predicate type variable applied        to a saturated occurrence of the data constructor-       (@p '@@' (MyCons x xs)@, in the above example).+       (@'Apply' p (MyCons x xs)@, in the above example).  * You'll need to enable lots of GHC extensions in order for the code generated   by 'deriveElim' to typecheck. You'll need at least the following:      * @AllowAmbiguousTypes@ +    * @DataKinds@+     * @GADTs@ +    * @PolyKinds@+     * @RankNTypes@      * @ScopedTypeVariables@@@ -118,8 +122,6 @@      * @TypeApplications@ -    * @TypeInType@- * 'deriveElim' doesn't support every possible data type at the moment.   It is known not to work for the following: @@ -263,9 +265,9 @@ singType :: Name -> Type singType x = ConT ''Sing `AppT` VarT x --- | Construct a type of the form @p '@@' ty@ given @p@ and @ty@.+-- | Construct a type of the form @'Apply' p ty@ given @p@ and @ty@. predType :: Name -> Type -> Type-predType p ty = InfixT (VarT p) ''(@@) ty+predType p ty = ConT ''Apply `AppT` VarT p `AppT` ty  -- | Generate a list of fresh names with a common prefix, and numbered suffixes. newNameList :: String -> Int -> Q [Name]

@@ -1,9 +1,10 @@ {-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE Trustworthy #-} {-# LANGUAGE TypeApplications #-}-{-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} {-| Module:      Data.Eliminator.TypeNats@@ -29,9 +30,9 @@ -- (crudely) pretend that it is using this eliminator. elimNat :: forall (p :: Nat ~> Type) (n :: Nat).            Sing n-        -> p @@ 0-        -> (forall (k :: Nat). Sing k -> p @@ k -> p @@ (k + 1))-        -> p @@ n+        -> Apply p 0+        -> (forall (k :: Nat). Sing k -> Apply p k -> Apply p (k + 1))+        -> Apply p n elimNat snat pZ pS =   case fromSing snat of     0        -> unsafeCoerce pZ

@@ -1,9 +1,10 @@+{-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-}+{-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} module DecideSpec where

@@ -1,12 +1,13 @@ {-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-}+{-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} module DecideTypes where

@@ -1,13 +1,13 @@ {-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-}+{-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-}-{-# OPTIONS_GHC -fno-warn-orphans #-} module EqualitySpec where  import           Data.Kind@@ -15,6 +15,8 @@ import qualified Data.Type.Equality as DTE import           Data.Type.Equality ((:~:)(..), (:~~:)(..)) +import           EqualityTypes+ import           Test.Hspec  main :: IO ()@@ -31,102 +33,57 @@  ----- -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-  fromSing SRefl = Refl-  toSing Refl    = SomeSing SRefl--instance SingI Refl where-  sing = SRefl--(~>:~:) :: forall (k :: Type) (a :: k) (b :: k)-                  (p :: forall (y :: k). a :~: y ~> Type)-                  (r :: a :~: b).-           Sing r-        -> p @@ Refl-        -> p @@ r-(~>:~:) SRefl pRefl = pRefl--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-  fromSing SHRefl = HRefl-  toSing HRefl    = SomeSing SHRefl--instance SingI HRefl where-  sing = SHRefl+j :: forall (k :: Type) (a :: k) (b :: k)+            (p :: forall (x :: k) (y :: k). x :~: y ~> Type)+            (r :: a :~: b).+     Sing r+  -> (forall (x :: k). p @@ (Refl :: x :~: x))+  -> p @@ r+j SRefl pRefl = pRefl @a -(~>:~~:) :: forall (j :: Type) (k :: Type) (a :: j) (b :: k)-                   (p :: forall (z :: Type) (y :: z). a :~~: y ~> Type)-                   (r :: a :~~: b).-            Sing r-         -> p @@ HRefl-         -> p @@ r-(~>:~~:) SHRefl pHRefl = pHRefl+hj :: forall (j :: Type) (k :: Type) (a :: j) (b :: k)+             (p :: forall (y :: Type) (z :: Type) (w :: y) (x :: z). w :~~: x ~> Type)+             (r :: a :~~: b).+      Sing r+   -> (forall (y :: Type) (w :: y). p @@ (HRefl :: w :~~: w))+   -> p @@ r+hj SHRefl pHRefl = pHRefl @k @a ------+k :: forall (k :: Type) (a :: k)+            (p :: a :~: a ~> Type)+            (r :: a :~: a).+     Sing r+  -> p @@ Refl+  -> p @@ r+k SRefl pRefl = pRefl -type WhySym (a :: t) (y :: t) (e :: a :~: y) = y :~: a-data WhySymSym (a :: t) :: forall (y :: t). a :~: y ~> Type-type instance Apply (WhySymSym a :: a :~: y ~> Type) x-  = WhySym a y x+hk :: forall (k :: Type) (a :: k)+             (p :: a :~~: a ~> Type)+             (r :: a :~~: a).+      Sing r+   -> p @@ HRefl+   -> p @@ r+hk SHRefl pHRefl = pHRefl  sym :: forall (t :: Type) (a :: t) (b :: t).        a :~: b -> b :~: a sym eq = withSomeSing eq $ \(singEq :: Sing r) ->-           (~>:~:) @t @a @b @(WhySymSym a) @r singEq Refl--type WhyHsym (a :: j) (y :: z) (e :: a :~~: y) = y :~~: a-data WhyHsymSym (a :: j) :: forall (z :: Type) (y :: z). a :~~: y ~> Type-type instance Apply (WhyHsymSym a :: a :~~: y ~> Type) x-  = WhyHsym a y x+           (~>:~:) @t @a @b @(WhySymSym1 a) @r singEq Refl  hsym :: forall (j :: Type) (k :: Type) (a :: j) (b :: k).         a :~~: b -> b :~~: a hsym eq = withSomeSing eq $ \(singEq :: Sing r) ->-            (~>:~~:) @j @k @a @b @(WhyHsymSym a) @r singEq HRefl--type family Symmetry (x :: (a :: k) :~: (b :: k)) :: b :~: a where-  Symmetry Refl = Refl--type WhySymIdempotent (a :: t) (z :: t) (r :: a :~: z)-  = Symmetry (Symmetry r) :~: r-data WhySymIdempotentSym (a :: t) :: forall (z :: t). a :~: z ~> Type-type instance Apply (WhySymIdempotentSym a :: a :~: z ~> Type) r-  = WhySymIdempotent a z r+            (~>:~~:) @j @k @a @b @(WhyHsymSym1 a) @r singEq HRefl  symIdempotent :: forall (t :: Type) (a :: t) (b :: t)                         (e :: a :~: b).                  Sing e -> Symmetry (Symmetry e) :~: e-symIdempotent se = (~>:~:) @t @a @b @(WhySymIdempotentSym a) @e se Refl--type family Hsymmetry (x :: (a :: j) :~~: (b :: k)) :: b :~~: a where-  Hsymmetry HRefl = HRefl--type WhyHsymIdempotent (a :: j) (y :: z) (r :: a :~~: y)-  = Hsymmetry (Hsymmetry r) :~: r-data WhyHsymIdempotentSym (a :: j) :: forall (z :: Type) (y :: z). a :~~: y ~> Type-type instance Apply (WhyHsymIdempotentSym a :: a :~~: y ~> Type) r-  = WhyHsymIdempotent a y r+symIdempotent se = (~>:~:) @t @a @b @(WhySymIdempotentSym1 a) @e se Refl  hsymIdempotent :: forall (j :: Type) (k :: Type) (a :: j) (b :: k)                          (e :: a :~~: b).                   Sing e -> Hsymmetry (Hsymmetry e) :~: e-hsymIdempotent se = (~>:~~:) @j @k @a @b @(WhyHsymIdempotentSym a) @e se Refl--type WhyReplace (from :: t) (p :: t ~> Type)-                (y :: t) (e :: from :~: y) = p @@ y-data WhyReplaceSym (from :: t) (p :: t ~> Type)-  :: forall (y :: t). from :~: y ~> Type-type instance Apply (WhyReplaceSym from p :: from :~: y ~> Type) x-  = WhyReplace from p y x+hsymIdempotent se = (~>:~~:) @j @k @a @b @(WhyHsymIdempotentSym1 a) @e se Refl  replace :: forall (t :: Type) (from :: t) (to :: t) (p :: t ~> Type).            p @@ from@@ -134,16 +91,10 @@         -> p @@ to replace from eq =   withSomeSing eq $ \(singEq :: Sing r) ->-    (~>:~:) @t @from @to @(WhyReplaceSym from p) @r singEq from+    (~>:~:) @t @from @to @(WhyReplaceSym2 from p) @r singEq from +-- Doesn't work due to https://ghc.haskell.org/trac/ghc/ticket/11719 {--type WhyHreplace (from :: j) (p :: forall (z :: Type). z ~> Type)-                 (y :: k) (e :: from :~~: y) = p @@ y-data WhyHreplaceSym (from :: j) (p :: forall (z :: Type). z ~> Type)-  :: forall (k :: Type) (y :: k). from :~~: y ~> Type-type instance Apply (WhyHreplaceSym from p :: from :~~: y ~> Type) x-  = WhyHreplace from p y x- hreplace :: forall (j :: Type) (k :: Type) (from :: j) (to :: k)                    (p :: forall (z :: Type). z ~> Type).             p @@ from@@ -151,27 +102,14 @@          -> p @@ to hreplace from heq =   withSomeSing eq $ \(singEq :: Sing r) ->-    (~>:~~:) @j @k @from @to @(WhyHreplaceSym from p) singEq from+    (@~>:~~:) @j @k @from @to @(WhyHreplaceSym2 from p) singEq from -} -type WhyLeibniz (f :: t ~> Type) (a :: t) (z :: t)-  = f @@ a -> f @@ z-data WhyLeibnizSym (f :: t ~> Type) (a :: t) :: t ~> Type-type instance Apply (WhyLeibnizSym f a) z = WhyLeibniz f a z- leibniz :: forall (t :: Type) (f :: t ~> Type) (a :: t) (b :: t).            a :~: b         -> f @@ a         -> f @@ b-leibniz = replace @t @a @b @(WhyLeibnizSym f a) id--type WhyCong (x :: Type) (y :: Type) (f :: x ~> y)-             (a :: x) (z :: x) (e :: a :~: z)-  = f @@ a :~: f @@ z-data WhyCongSym (x :: Type) (y :: Type) (f :: x ~> y)-                (a :: x) :: forall (z :: x). a :~: z ~> Type-type instance Apply (WhyCongSym x y f a :: a :~: z ~> Type) e-  = WhyCong x y f a z e+leibniz = replace @t @a @b @(WhyLeibnizSym2 f a) id  cong :: forall (x :: Type) (y :: Type) (f :: x ~> y)                (a :: x) (b :: x).@@ -179,22 +117,12 @@      -> f @@ a :~: f @@ b cong eq =   withSomeSing eq $ \(singEq :: Sing r) ->-    (~>:~:) @x @a @b @(WhyCongSym x y f a) @r singEq Refl--type WhyEqIsRefl (a :: k) (z :: k) (e :: a :~: z)-  = e :~~: (Refl :: a :~: a)-data WhyEqIsReflSym (a :: k) :: forall (z :: k). a :~: z ~> Type-type instance Apply (WhyEqIsReflSym a :: a :~: z ~> Type) e = WhyEqIsRefl a z e+    (~>:~:) @x @a @b @(WhyCongSym2 f a) @r singEq Refl  eqIsRefl :: forall (k :: Type) (a :: k) (b :: k) (e :: a :~: b).             Sing e -> e :~~: (Refl :: a :~: a)-eqIsRefl eq = (~>:~:) @k @a @b @(WhyEqIsReflSym a) @e eq HRefl--type WhyHEqIsHRefl (a :: j) (z :: k) (e :: a :~~: z)-  = e :~~: (HRefl :: a :~~: a)-data WhyHEqIsHReflSym (a :: j) :: forall (k :: Type) (z :: k). a :~~: z ~> Type-type instance Apply (WhyHEqIsHReflSym a :: a :~~: z ~> Type) e = WhyHEqIsHRefl a z e+eqIsRefl eq = (~>:~:) @k @a @b @(WhyEqIsReflSym1 a) @e eq HRefl  heqIsHRefl :: forall (j :: Type) (k :: Type) (a :: j) (b :: k) (e :: a :~~: b).               Sing e -> e :~~: (HRefl :: a :~~: a)-heqIsHRefl heq = (~>:~~:) @j @k @a @b @(WhyHEqIsHReflSym a) @e heq HRefl+heqIsHRefl heq = (~>:~~:) @j @k @a @b @(WhyHEqIsHReflSym1 a) @e heq HRefl

@@ -0,0 +1,104 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+module EqualityTypes where++import           Data.Kind+import           Data.Singletons.TH+import           Data.Type.Equality ((:~:)(..), (:~~:)(..))++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+  fromSing SRefl = Refl+  toSing Refl    = SomeSing SRefl++instance SingI Refl where+  sing = SRefl++-- | Christine Paulin-Mohring's version of the J rule.+(~>:~:) :: forall (k :: Type) (a :: k) (b :: k)+                  (p :: forall (y :: k). a :~: y ~> Type)+                  (r :: a :~: b).+           Sing r+        -> p @@ Refl+        -> p @@ r+(~>:~:) SRefl pRefl = pRefl++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+  fromSing SHRefl = HRefl+  toSing HRefl    = SomeSing SHRefl++instance SingI HRefl where+  sing = SHRefl++-- | Christine Paulin-Mohring's version of the J rule, but heterogeneously kinded.+(~>:~~:) :: forall (j :: Type) (k :: Type) (a :: j) (b :: k)+                   (p :: forall (z :: Type) (y :: z). a :~~: y ~> Type)+                   (r :: a :~~: b).+            Sing r+         -> p @@ HRefl+         -> p @@ r+(~>:~~:) SHRefl pHRefl = pHRefl++-----++$(singletons [d|+  type family WhySym (a :: t) (e :: a :~: (y :: t)) :: Type where+    WhySym a (_ :: a :~: y) = y :~: a++  type family WhyHsym (a :: j) (e :: a :~~: (y :: z)) :: Type where+    WhyHsym a (_ :: a :~~: y)  = y :~~: a++  type family Symmetry (x :: (a :: k) :~: (b :: k)) :: b :~: a where+    Symmetry Refl = Refl++  type family WhySymIdempotent (a :: t) (r :: a :~: (z :: t)) :: Type where+    WhySymIdempotent _ r = Symmetry (Symmetry r) :~: r++  type family Hsymmetry (x :: a :~~: b) :: b :~~: a where+    Hsymmetry HRefl = HRefl++  type family WhyHsymIdempotent (a :: j) (r :: a :~~: (y :: z)) :: Type where+    WhyHsymIdempotent _ r = Hsymmetry (Hsymmetry r) :~: r++  type family WhyReplace (from :: t) (p :: t ~> Type)+                         (e :: from :~: (y :: t)) :: Type where+    WhyReplace from p (_ :: from :~: y) = p @@ y++  -- Doesn't work due to https://ghc.haskell.org/trac/ghc/ticket/11719+  {-+  type family WhyHreplace (from :: j) (p :: forall (z :: Type). z ~> Type)+                          (e :: from :~~: (y :: k)) :: Type where+    WhyHreplace from p (_ :: from :~~: y) = p @@ y+  -}++  type family WhyLeibniz (f :: t ~> Type) (a :: t) (z :: t) :: Type where+    WhyLeibniz f a z = f @@ a -> f @@ z++  type family WhyCong (f :: x ~> y) (a :: x) (e :: a :~: (z :: x)) :: Type where+    WhyCong (f :: x ~> y) (a :: x) (e :: a :~: (z :: x)) = f @@ a :~: f @@ z++  type family WhyEqIsRefl (a :: k) (e :: a :~: (z :: k)) :: Type where+    WhyEqIsRefl a e = e :~~: (Refl :: a :~: a)++  type family WhyHEqIsHRefl (a :: j) (e :: a :~~: (z :: k)) :: Type where+    WhyHEqIsHRefl a e = e :~~: (HRefl :: a :~~: a)+  |])

@@ -1,10 +1,11 @@ {-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-}+{-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} module GADTSpec where 

@@ -1,10 +1,11 @@ {-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-}+{-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} module ListSpec where @@ -32,7 +33,7 @@                       SingI l                    => Length l :~: Length (Map f l) mapPreservesLength-  = elimList @x @(WhyMapPreservesLengthSym1 f) @l (sing @_ @l) base step+  = elimList @x @(WhyMapPreservesLengthSym1 f) @l (sing @l) base step   where     base :: WhyMapPreservesLength f '[]     base = Refl@@ -48,7 +49,7 @@                     SingI l                  => Map f (Map g l) :~: Map (f .@#@$$$ g) l mapFusion-  = elimList @x @(WhyMapFusionSym2 f g) @l (sing @_ @l) base step+  = elimList @x @(WhyMapFusionSym2 f g) @l (sing @l) base step   where     base :: WhyMapFusion f g '[]     base = Refl

@@ -1,7 +1,8 @@+{-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-}+{-# LANGUAGE PolyKinds #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} module ListTypes where

@@ -1,7 +1,9 @@+{-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-}+{-# LANGUAGE NoStarIsType #-}+{-# LANGUAGE PolyKinds #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-}-{-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} module VecSpec where @@ -77,7 +79,7 @@ mapVec :: forall (a :: Type) (b :: Type) (n :: Nat).           SingI n        => (a -> b) -> Vec a n -> Vec b n-mapVec f = elimNat @(WhyMapVecSym2 a b) @n (sing @_ @n) base step+mapVec f = elimNat @(WhyMapVecSym2 a b) @n (sing @n) base step   where     base :: WhyMapVec a b Z     base _ = VNil@@ -88,7 +90,7 @@ zipWithVec :: forall (a :: Type) (b :: Type) (c :: Type) (n :: Nat).               SingI n            => (a -> b -> c) -> Vec a n -> Vec b n -> Vec c n-zipWithVec f = elimNat @(WhyZipWithVecSym3 a b c) @n (sing @_ @n) base step+zipWithVec f = elimNat @(WhyZipWithVecSym3 a b c) @n (sing @n) base step   where     base :: WhyZipWithVec a b c Z     base _ _ = VNil@@ -103,7 +105,7 @@ appendVec :: forall (e :: Type) (n :: Nat) (m :: Nat).              SingI n           => Vec e n -> Vec e m -> Vec e (n + m)-appendVec = elimNat @(WhyAppendVecSym2 e m) @n (sing @_ @n) base step+appendVec = elimNat @(WhyAppendVecSym2 e m) @n (sing @n) base step   where     base :: WhyAppendVec e m Z     base _ = id@@ -117,10 +119,10 @@ transposeVec :: forall (e :: Type) (n :: Nat) (m :: Nat).                 (SingI n, SingI m)              => Vec (Vec e m) n -> Vec (Vec e n) m-transposeVec = elimNat @(WhyTransposeVecSym2 e m) @n (sing @_ @n) base step+transposeVec = elimNat @(WhyTransposeVecSym2 e m) @n (sing @n) base step   where     base :: WhyTransposeVec e m Z-    base _ = replicateVec (sing @_ @m) VNil+    base _ = replicateVec (sing @m) VNil      step :: forall (k :: Nat).             Sing k

@@ -1,12 +1,14 @@ {-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-}+{-# LANGUAGE NoStarIsType #-}+{-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} module VecTypes where