diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,8 @@ +## 0.8 [2021.03.12] +* Require `singletons-base-3.0` and GHC 9.0. +* Remove eliminators for `Data.Semigroup.Option`, which is deprecated as of + `base-4.15.0.0`. + ## 0.7 [2020.03.25] * Require `singletons-2.7` and GHC 8.10. * Add experimental support for generating type-level eliminators through the diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -3,7 +3,7 @@ [![Hackage Dependencies](https://img.shields.io/hackage-deps/v/eliminators.svg)](http://packdeps.haskellers.com/reverse/eliminators) [![Haskell Programming Language](https://img.shields.io/badge/language-Haskell-blue.svg)][Haskell.org] [![BSD3 License](http://img.shields.io/badge/license-BSD3-brightgreen.svg)][tl;dr Legal: BSD3] -[![Build](https://img.shields.io/travis/RyanGlScott/eliminators.svg)](https://travis-ci.org/RyanGlScott/eliminators) +[![Build Status](https://github.com/RyanGlScott/eliminators/workflows/Haskell-CI/badge.svg)](https://github.com/RyanGlScott/eliminators/actions?query=workflow%3AHaskell-CI) [Hackage: eliminators]: http://hackage.haskell.org/package/eliminators diff --git a/eliminators.cabal b/eliminators.cabal --- a/eliminators.cabal +++ b/eliminators.cabal @@ -1,5 +1,5 @@ name: eliminators -version: 0.7 +version: 0.8 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.10.1 +tested-with: GHC == 9.0.1 source-repository head type: git @@ -26,13 +26,13 @@ exposed-modules: Data.Eliminator Data.Eliminator.TH Data.Eliminator.TypeNats - build-depends: base >= 4.14 && < 4.15 + build-depends: base >= 4.15 && < 4.16 , extra >= 1.4.2 && < 1.8 - , singletons >= 2.7 && < 2.8 + , singletons-base >= 3.0 && < 3.1 , singleton-nats >= 0.4.2 && < 0.5 - , template-haskell >= 2.16 && < 2.17 - , th-abstraction >= 0.3 && < 0.4 - , th-desugar >= 1.11 && < 1.12 + , template-haskell >= 2.17 && < 2.18 + , th-abstraction >= 0.4 && < 0.5 + , th-desugar >= 1.12 && < 1.13 hs-source-dirs: src default-language: Haskell2010 ghc-options: -Wall -Wcompat -Wno-unticked-promoted-constructors @@ -52,11 +52,11 @@ ListTypes VecTypes VecSpec - build-depends: base >= 4.14 && < 4.15 + build-depends: base >= 4.15 && < 4.16 , eliminators - , hspec >= 2 && < 3 - , singletons >= 2.7 && < 2.8 - , singleton-nats >= 0.4.2 && < 0.5 + , hspec >= 2 && < 3 + , singletons-base >= 3.0 && < 3.1 + , 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 @@ -61,8 +61,6 @@ , ElimNat , elimNonEmpty , ElimNonEmpty - , elimOption - , ElimOption , elimOrdering , ElimOrdering , elimProduct @@ -93,25 +91,26 @@ import Data.Eliminator.TH import Data.Functor.Const (Const(..)) +import Data.Functor.Const.Singletons (SConst(..)) import Data.Functor.Identity (Identity(..)) +import Data.Functor.Identity.Singletons (SIdentity(..)) import Data.List.NonEmpty (NonEmpty(..)) +import Data.List.NonEmpty.Singletons (SNonEmpty(..)) import Data.Monoid hiding (First, Last) +import Data.Monoid.Singletons hiding (SFirst, SLast) import Data.Nat import Data.Ord (Down(..)) +import Data.Ord.Singletons (SDown(..)) import Data.Semigroup -import Data.Singletons.Prelude hiding - (All, Any, Const, Last, Min, Max, Product, Sum) -import Data.Singletons.Prelude.Const (SConst(..)) -import Data.Singletons.Prelude.Identity (SIdentity(..)) -import Data.Singletons.Prelude.List.NonEmpty (SNonEmpty(..)) -import Data.Singletons.Prelude.Monoid hiding (SFirst, SLast) -import Data.Singletons.Prelude.Ord (SDown(..)) -import Data.Singletons.Prelude.Semigroup +import Data.Semigroup.Singletons import Data.Void (Void) import Language.Haskell.TH (nameBase) import Language.Haskell.TH.Desugar (tupleNameDegree_maybe) +import Prelude.Singletons hiding + (All, Any, Const, Last, Min, Max, Product, Sum) + {- $eliminators These eliminators are defined with propositions of kind @\ ~> 'Type'@ @@ -145,7 +144,6 @@ , ''Min , ''Nat , ''NonEmpty - , ''Option , ''Ordering , ''Product , ''Sum 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 @@ -33,13 +33,15 @@ import qualified Data.Kind as Kind (Type) import Data.Maybe import Data.Proxy -import Data.Singletons.Prelude import Data.Singletons.TH.Options import Language.Haskell.TH import Language.Haskell.TH.Datatype +import Language.Haskell.TH.Datatype.TyVarBndr import Language.Haskell.TH.Desugar hiding (NewOrData(..)) +import Prelude.Singletons + {- $term-conventions 'deriveElim' and 'deriveElimNamed' provide a way to automate the creation of eliminator functions, which are mostly boilerplate. Here is a complete example @@ -288,8 +290,8 @@ singVar <- newName "s" let elimName = mkName funName promDataKind = datatypeType info - predVarBndr = KindedTV predVar (InfixT promDataKind ''(~>) (ConT ''Kind.Type)) - singVarBndr = KindedTV singVar promDataKind + predVarBndr = kindedTV predVar (InfixT promDataKind ''(~>) (ConT ''Kind.Type)) + singVarBndr = kindedTV singVar promDataKind caseTypes <- traverse (caseType prox dataName predVar) cons let returnType = predType predVar (VarT singVar) elimType = elimTypeSig prox dataVarBndrs predVarBndr singVarBndr @@ -330,8 +332,8 @@ caseClause :: Name -- The name of the eliminator function -> Name -- The name of the data type - -> [TyVarBndr] -- The type variables bound by the data type - -> TyVarBndr -- The predicate type variable + -> [TyVarBndrUnit] -- The type variables bound by the data type + -> TyVarBndrUnit -- The predicate type variable -> Int -- The index of this constructor (0-indexed) -> Int -- The total number of data constructors -> ConstructorInfo -- The data constructor @@ -375,8 +377,8 @@ caseTySynEqn :: Name -- The name of the eliminator function -> Name -- The name of the data type - -> [TyVarBndr] -- The type variables bound by the data type - -> TyVarBndr -- The predicate type variable + -> [TyVarBndrUnit] -- The type variables bound by the data type + -> TyVarBndrUnit -- The predicate type variable -> Int -- The index of this constructor (0-indexed) -> [Type] -- The types of each "case alternative" in the eliminator -- function's type signature @@ -394,7 +396,7 @@ let mkVarName | i == conIndex = pure usedCaseVar | otherwise = newName ("_p" ++ show i) - in liftA2 KindedTV mkVarName (pure caseTy) + in liftA2 kindedTV mkVarName (pure caseTy) let caseVarNames = map tvName caseVarBndrs prefix = foldAppKindT (ConT elimName) $ map VarT dataVarNames mbInductiveArg singVar varType = @@ -405,7 +407,7 @@ mkArg f (singVar, varType) = foldAppDefunT (f `AppT` VarT singVar) $ maybeToList (mbInductiveArg singVar varType) - bndrs = dataVarBndrs ++ predVarBndr : caseVarBndrs ++ map PlainTV singVars + bndrs = dataVarBndrs ++ predVarBndr : caseVarBndrs ++ map plainTV singVars lhs = foldAppT prefix $ VarT predVarName : foldAppT (ConT conName) (map VarT singVars) : map VarT caseVarNames @@ -430,13 +432,13 @@ -- Create an eliminator function's type. elimTypeSig :: proxy t - -> [TyVarBndr] -- The type variables bound by the data type - -> TyVarBndr -- The predicate type variable - -> TyVarBndr -- The type variable whose kind is that of the data type itself - -> [Type] -- The types of each "case alternative" in the eliminator - -- function's type signature - -> Type -- The eliminator function's return type - -> Type -- The full type + -> [TyVarBndrUnit] -- The type variables bound by the data type + -> TyVarBndrUnit -- The predicate type variable + -> TyVarBndrUnit -- The type variable whose kind is that of the data type itself + -> [Type] -- The types of each "case alternative" in the eliminator + -- function's type signature + -> Type -- The eliminator function's return type + -> Type -- The full type -- Take a data constructor's field type and prepend it to a "case -- alternative" in an eliminator function's type signature. @@ -454,9 +456,9 @@ proxy t -> Name -- The name of the eliminator function -> Name -- The name of the data type - -> [TyVarBndr] -- The type variables bound by the data type - -> TyVarBndr -- The predicate type variable - -> TyVarBndr -- The type variable whose kind is that of the data type itself + -> [TyVarBndrUnit] -- The type variables bound by the data type + -> TyVarBndrUnit -- The predicate type variable + -> TyVarBndrUnit -- The type variable whose kind is that of the data type itself -> [Type] -- The types of each "case alternative" in the eliminator -- function's type signature -> [ConstructorInfo] -- The data constructors @@ -466,11 +468,12 @@ elimSigD _ = SigD elimTypeSig _ dataVarBndrs predVarBndr singVarBndr caseTypes returnType = - ForallT (dataVarBndrs ++ [predVarBndr, singVarBndr]) [] $ + ForallT (changeTVFlags SpecifiedSpec $ + dataVarBndrs ++ [predVarBndr, singVarBndr]) [] $ ravel (singType (tvName singVarBndr):caseTypes) returnType prependElimCaseTypeVar _ dataName predVar var varType t = - ForallT [KindedTV var varType] [] $ + ForallT [kindedTVSpecified var varType] [] $ ravel (singType var:maybeToList (mbInductiveType dataName predVar var varType)) t qElimEqns _ elimName dataName dataVarBndrs predVarBndr _singVarBndr _caseTypes cons @@ -488,20 +491,20 @@ elimSigD _ = KiSigD elimTypeSig _ dataVarBndrs predVarBndr singVarBndr caseTypes returnType = - ForallT dataVarBndrs [] $ + ForallT (changeTVFlags SpecifiedSpec dataVarBndrs) [] $ ForallVisT [predVarBndr, singVarBndr] $ ravel caseTypes returnType prependElimCaseTypeVar _ dataName predVar var varType t = - ForallVisT [KindedTV var varType] $ + ForallVisT [kindedTV var varType] $ ravelDefun (maybeToList (mbInductiveType dataName predVar var varType)) t qElimEqns _ elimName dataName dataVarBndrs predVarBndr singVarBndr caseTypes cons = do - caseVarBndrs <- replicateM (length caseTypes) (PlainTV <$> newName "p") + caseVarBndrs <- replicateM (length caseTypes) (plainTV <$> newName "p") let predVar = tvName predVarBndr singVar = tvName singVarBndr tyFamHead = TypeFamilyHead elimName - (PlainTV predVar:PlainTV singVar:caseVarBndrs) + (plainTV predVar:plainTV singVar:caseVarBndrs) NoSig Nothing caseEqns <- itraverse (\i -> caseTySynEqn elimName dataName dataVarBndrs predVarBndr i caseTypes) cons 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 @@ -20,8 +20,8 @@ import Data.Kind (Type) import Data.Singletons -import Data.Singletons.TypeLits +import GHC.TypeLits.Singletons import GHC.TypeNats import Unsafe.Coerce (unsafeCoerce) diff --git a/tests/DecideSpec.hs b/tests/DecideSpec.hs --- a/tests/DecideSpec.hs +++ b/tests/DecideSpec.hs @@ -11,13 +11,14 @@ import Data.Eliminator import Data.Nat -import Data.Singletons.Prelude import Data.Singletons.TH hiding (Decision(..)) import Data.Type.Equality import EqualitySpec (cong, replace) import DecideTypes +import Prelude.Singletons + import Test.Hspec main :: IO () @@ -120,8 +121,8 @@ base :: ListEqConsequences '[] '[] base = () - step :: forall (x :: e) (xs :: [e]). - Sing x -> Sing xs + step :: forall (x :: e). Sing x + -> forall (xs :: [e]). Sing xs -> ListEqConsequences xs xs -> ListEqConsequences (x:xs) (x:xs) step _ _ _ = (Refl, Refl) @@ -149,11 +150,11 @@ base :: Decision ('[] :~: '[]) base = Proved Refl - step :: forall (x :: e) (xs :: [e]). - Sing x -> Sing xs + step :: forall (x :: e). Sing x + -> forall (xs :: [e]). Sing xs -> Decision ('[] :~: xs) -> Decision ('[] :~: (x:xs)) - step _ _ _ = Disproved (nilNotCons @e @x @xs) + step _ (_ :: Sing xs) _ = Disproved (nilNotCons @e @x @xs) intermixListEqs :: forall e (x :: e) (xs :: [e]) (y :: e) (ys :: [e]). x :~: y -> xs :~: ys @@ -202,19 +203,20 @@ base :: WhyDecEqList '[] base = WhyDecEqList decEqNil - step :: forall (x :: e) (xs :: [e]). - Sing x -> Sing xs + step :: forall (x :: e). Sing x + -> forall (xs :: [e]). Sing xs -> WhyDecEqList xs -> WhyDecEqList (x:xs) - step sx sxs swhyXs = WhyDecEqList $ \(sl :: Sing l) -> - elimList @e @(WhyDecEqConsSym2 x xs) @l sl - stepBase stepStep + step sx (sxs :: Sing xs) swhyXs = + WhyDecEqList $ \(sl :: Sing l) -> + elimList @e @(WhyDecEqConsSym2 x xs) @l sl + stepBase stepStep where stepBase :: Decision ((x:xs) :~: '[]) stepBase = Disproved $ consNotNil @e @x @xs - stepStep :: forall (y :: e) (ys :: [e]). - Sing y -> Sing ys + stepStep :: forall (y :: e). Sing y + -> forall (ys :: [e]). Sing ys -> Decision ((x:xs) :~: ys) -> Decision ((x:xs) :~: (y:ys)) stepStep sy sys _ = decCongCons sx sxs diff --git a/tests/DecideTypes.hs b/tests/DecideTypes.hs --- a/tests/DecideTypes.hs +++ b/tests/DecideTypes.hs @@ -16,8 +16,9 @@ import Data.Eliminator import Data.Kind import Data.Nat -import Data.Singletons.Prelude import Data.Singletons.TH hiding (Decision(..)) + +import Prelude.Singletons -- Due to https://github.com/goldfirere/singletons/issues/82, promoting the -- Decision data type from Data.Singletons.Decide is a tad awkward. To work diff --git a/tests/EqualityTypes.hs b/tests/EqualityTypes.hs --- a/tests/EqualityTypes.hs +++ b/tests/EqualityTypes.hs @@ -10,27 +10,28 @@ {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} -{-# OPTIONS_GHC -fno-warn-orphans #-} +{-# OPTIONS_GHC -Wno-orphans #-} module EqualityTypes where import Data.Kind import Data.Singletons.TH +import Data.Singletons.TH.Options import Data.Type.Equality ((:~~:)(..)) import Internal -type (%:~:) :: a :~: b -> Type -data (%:~:) e where - SRefl :: (%:~:) Refl -type instance Sing = (%:~:) +$(withOptions defaultOptions{genSingKindInsts = False} $ + genSingletons [''(:~:), ''(:~~:)]) instance SingKind (a :~: b) where type Demote (a :~: b) = a :~: b fromSing SRefl = Refl toSing Refl = SomeSing SRefl -instance SingI Refl where - sing = SRefl +instance SingKind (a :~~: b) where + type Demote (a :~~: b) = a :~~: b + fromSing SHRefl = HRefl + toSing HRefl = SomeSing SHRefl -- | Christine Paulin-Mohring's version of the J rule. (~>:~:) :: forall k (a :: k) @@ -69,19 +70,6 @@ -> p @@ b type family (~>!:~:) p r pRefl where (~>!:~:) _ Refl pRefl = pRefl - -type (%:~~:) :: forall j k (a :: j) (b :: k). a :~~: b -> Type -data (%:~~:) e where - SHRefl :: (%:~~:) HRefl -type instance Sing = (%:~~:) - -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 (a :: j) diff --git a/tests/GADTSpec.hs b/tests/GADTSpec.hs --- a/tests/GADTSpec.hs +++ b/tests/GADTSpec.hs @@ -5,6 +5,7 @@ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneKindSignatures #-} +{-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} @@ -12,7 +13,8 @@ module GADTSpec where import Data.Kind -import Data.Singletons +import Data.Singletons.TH +import Data.Singletons.TH.Options import Internal @@ -26,14 +28,12 @@ ----- -type So :: Bool -> Type -data So b where - Oh :: So True - -type SSo :: So what -> Type -data SSo s where - SOh :: SSo Oh -type instance Sing = SSo +$(withOptions defaultOptions{genSingKindInsts = False} $ + singletons [d| + type So :: Bool -> Type + data So b where + Oh :: So True + |]) elimSo :: forall (p :: forall (long_sucker :: Bool). So long_sucker ~> Type) (what :: Bool) (s :: So what). @@ -67,16 +67,14 @@ forall (p :: Bool ~> Prop) (pOh :: p @@ True). ElimPropSo p Oh pOh = pOh -type Flarble :: Type -> Type -> Type -data Flarble a b where - MkFlarble1 :: a -> Flarble a b - MkFlarble2 :: a ~ Bool => Flarble a (Maybe b) - -type SFlarble :: Flarble a b -> Type -data SFlarble f where - SMkFlarble1 :: Sing x -> SFlarble (MkFlarble1 x) - SMkFlarble2 :: SFlarble MkFlarble2 -type instance Sing = SFlarble +$(withOptions defaultOptions{genSingKindInsts = False} $ + singletons [d| + type Flarble :: Type -> Type -> Type + data Flarble a b where + MkFlarble1 :: a -> Flarble a b + -- MkFlarble2 :: a ~ Bool => Flarble a (Maybe b) + MkFlarble2 :: Flarble Bool (Maybe b) + |]) elimFlarble :: forall (p :: forall x y. Flarble x y ~> Type) a b (f :: Flarble a b). @@ -141,14 +139,12 @@ ElimPropFlarble p (MkFlarble2 :: Flarble Bool (Maybe b')) pMkFlarble1 pMkFlarble2 = pMkFlarble2 @b' -type Obj :: Type -data Obj where - MkObj :: o -> Obj - -type SObj :: Obj -> Type -data SObj o where - SMkObj :: forall obiwan (obj :: obiwan). Sing obj -> SObj (MkObj obj) -type instance Sing = SObj +$(withOptions defaultOptions{genSingKindInsts = False} $ + singletons [d| + type Obj :: Type + data Obj where + MkObj :: o -> Obj + |]) elimObj :: forall (p :: Obj ~> Type) (o :: Obj). Sing o diff --git a/tests/ListSpec.hs b/tests/ListSpec.hs --- a/tests/ListSpec.hs +++ b/tests/ListSpec.hs @@ -10,14 +10,14 @@ module ListSpec where import Data.Eliminator -import Data.Singletons.Prelude -import Data.Singletons.Prelude.List +import Data.List.Singletons import Data.Type.Equality import EqualitySpec (cong) - import ListTypes +import Prelude.Singletons + import Test.Hspec main :: IO () @@ -37,8 +37,8 @@ base :: WhyMapPreservesLength f '[] base = Refl - step :: forall (s :: x) (ss :: [x]). - Sing s -> Sing ss + step :: forall (s :: x). Sing s + -> forall (ss :: [x]). Sing ss -> WhyMapPreservesLength f ss -> WhyMapPreservesLength f (s:ss) step _ _ = cong @_ @_ @((+@#@$$) 1) @@ -53,8 +53,8 @@ base :: WhyMapFusion f g '[] base = Refl - step :: forall (s :: x) (ss :: [x]). - Sing s -> Sing ss + step :: forall (s :: x). Sing s + -> forall (ss :: [x]). Sing ss -> WhyMapFusion f g ss -> WhyMapFusion f g (s:ss) step _ _ = cong @_ @_ @((:@#@$$) (f @@ (g @@ s))) diff --git a/tests/ListTypes.hs b/tests/ListTypes.hs --- a/tests/ListTypes.hs +++ b/tests/ListTypes.hs @@ -9,9 +9,9 @@ module ListTypes where import Data.Kind -import Data.Singletons.Prelude -import Data.Singletons.Prelude.List +import Data.List.Singletons import Data.Singletons.TH +import Prelude.Singletons $(singletons [d| type WhyMapPreservesLength :: (x ~> y) -> [x] -> Type diff --git a/tests/MatchabilizeSpec.hs b/tests/MatchabilizeSpec.hs --- a/tests/MatchabilizeSpec.hs +++ b/tests/MatchabilizeSpec.hs @@ -7,11 +7,11 @@ module MatchabilizeSpec where import Data.Eliminator -import Data.Singletons -import Data.Singletons.Prelude import Data.Type.Equality import MatchabilizeTypes + +import Prelude.Singletons import Test.Hspec diff --git a/tests/VecSpec.hs b/tests/VecSpec.hs --- a/tests/VecSpec.hs +++ b/tests/VecSpec.hs @@ -9,8 +9,8 @@ import Data.Eliminator import Data.Nat -import Data.Singletons -import Data.Singletons.Prelude.Num + +import Prelude.Singletons import VecTypes diff --git a/tests/VecTypes.hs b/tests/VecTypes.hs --- a/tests/VecTypes.hs +++ b/tests/VecTypes.hs @@ -1,5 +1,6 @@ {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE DataKinds #-} +{-# LANGUAGE EmptyCase #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE NoStarIsType #-} {-# LANGUAGE PolyKinds #-} @@ -16,26 +17,25 @@ import Data.Kind (Type) import Data.Nat -import Data.Singletons.Prelude.Num -import Data.Singletons.TH +import Data.Singletons.Base.TH +import Data.Singletons.TH.Options + import Internal -type Vec :: Type -> Nat -> Type -data Vec :: Type -> Nat -> Type where - VNil :: Vec a Z - (:#) :: { vhead :: a, vtail :: Vec a n } -> Vec a (S n) -infixr 5 :# +import Prelude.Singletons + +$(withOptions defaultOptions{genSingKindInsts = False} $ + singletons [d| + type Vec :: Type -> Nat -> Type + data Vec a n where + VNil :: Vec a Z + (:#) :: { vhead :: a, vtail :: Vec a n } -> Vec a (S n) + infixr 5 :# + |]) deriving instance Eq a => Eq (Vec a n) deriving instance Ord a => Ord (Vec a n) deriving instance Show a => Show (Vec a n) -type SVec :: Vec a n -> Type -data SVec v where - SVNil :: SVec VNil - (:%#) :: { sVhead :: Sing x, sVtail :: Sing xs } -> SVec (x :# xs) -type instance Sing = SVec -infixr 5 :%# - instance SingKind a => SingKind (Vec a n) where type Demote (Vec a n) = Vec (Demote a) n fromSing SVNil = VNil @@ -45,12 +45,6 @@ withSomeSing x $ \sx -> withSomeSing xs $ \sxs -> SomeSing $ sx :%# sxs - -instance SingI VNil where - sing = SVNil - -instance (SingI x, SingI xs) => SingI (x :# xs) where - sing = sing :%# sing elimVec :: forall a (p :: forall (k :: Nat). Vec a k ~> Type) (n :: Nat) (v :: Vec a n).