eliminators 0.7 → 0.8

raw patch · 15 files changed

+130/−143 lines, 15 filesdep +singletons-basedep −singletonsdep ~basedep ~template-haskelldep ~th-abstractionPVP ok

version bump matches the API change (PVP)

Dependencies added: singletons-base

Dependencies removed: singletons

Dependency ranges changed: base, template-haskell, th-abstraction, th-desugar

API changes (from Hackage documentation)

Files

• CHANGELOG.md +5/−0
• README.md +1/−1
• eliminators.cabal +11/−11
• src/Data/Eliminator.hs +9/−11
• src/Data/Eliminator/TH.hs +28/−25
• src/Data/Eliminator/TypeNats.hs +1/−1
• tests/DecideSpec.hs +15/−13
• tests/DecideTypes.hs +2/−1
• tests/EqualityTypes.hs +8/−20
• tests/GADTSpec.hs +23/−27
• tests/ListSpec.hs +7/−7
• tests/ListTypes.hs +2/−2
• tests/MatchabilizeSpec.hs +2/−2
• tests/VecSpec.hs +2/−2
• tests/VecTypes.hs +14/−20

@@ -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

@@ -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

@@ -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

@@ -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 @\<Datatype\> ~> 'Type'@@@ -145,7 +144,6 @@              , ''Min              , ''Nat              , ''NonEmpty-             , ''Option              , ''Ordering              , ''Product              , ''Sum

@@ -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

@@ -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)

@@ -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

@@ -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

@@ -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)

@@ -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

@@ -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)))

@@ -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

@@ -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 

@@ -9,8 +9,8 @@  import Data.Eliminator import Data.Nat-import Data.Singletons-import Data.Singletons.Prelude.Num++import Prelude.Singletons  import VecTypes 

@@ -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).