diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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`. diff --git a/eliminators.cabal b/eliminators.cabal --- a/eliminators.cabal +++ b/eliminators.cabal @@ -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 diff --git a/src/Data/Eliminator.hs b/src/Data/Eliminator.hs --- a/src/Data/Eliminator.hs +++ b/src/Data/Eliminator.hs @@ -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 @\ ~> '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: diff --git a/src/Data/Eliminator/TH.hs b/src/Data/Eliminator/TH.hs --- a/src/Data/Eliminator/TH.hs +++ b/src/Data/Eliminator/TH.hs @@ -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] diff --git a/src/Data/Eliminator/TypeNats.hs b/src/Data/Eliminator/TypeNats.hs --- a/src/Data/Eliminator/TypeNats.hs +++ b/src/Data/Eliminator/TypeNats.hs @@ -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 diff --git a/tests/DecideSpec.hs b/tests/DecideSpec.hs --- a/tests/DecideSpec.hs +++ b/tests/DecideSpec.hs @@ -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 diff --git a/tests/DecideTypes.hs b/tests/DecideTypes.hs --- a/tests/DecideTypes.hs +++ b/tests/DecideTypes.hs @@ -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 diff --git a/tests/EqualitySpec.hs b/tests/EqualitySpec.hs --- a/tests/EqualitySpec.hs +++ b/tests/EqualitySpec.hs @@ -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 diff --git a/tests/EqualityTypes.hs b/tests/EqualityTypes.hs new file mode 100644 --- /dev/null +++ b/tests/EqualityTypes.hs @@ -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) + |]) diff --git a/tests/GADTSpec.hs b/tests/GADTSpec.hs --- a/tests/GADTSpec.hs +++ b/tests/GADTSpec.hs @@ -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 diff --git a/tests/ListSpec.hs b/tests/ListSpec.hs --- a/tests/ListSpec.hs +++ b/tests/ListSpec.hs @@ -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 diff --git a/tests/ListTypes.hs b/tests/ListTypes.hs --- a/tests/ListTypes.hs +++ b/tests/ListTypes.hs @@ -1,7 +1,8 @@ +{-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} +{-# LANGUAGE PolyKinds #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} module ListTypes where diff --git a/tests/VecSpec.hs b/tests/VecSpec.hs --- a/tests/VecSpec.hs +++ b/tests/VecSpec.hs @@ -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 diff --git a/tests/VecTypes.hs b/tests/VecTypes.hs --- a/tests/VecTypes.hs +++ b/tests/VecTypes.hs @@ -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