eliminators 0.5 → 0.5.1

raw patch · 13 files changed

+221/−152 lines, 13 filesdep ~th-abstractionPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: th-abstraction

API changes (from Hackage documentation)

Files

• CHANGELOG.md +3/−0
• eliminators.cabal +12/−11
• src/Data/Eliminator/TH.hs +11/−7
• tests/DecideSpec.hs +9/−9
• tests/DecideTypes.hs +28/−33
• tests/EqualitySpec.hs +44/−29
• tests/EqualityTypes.hs +26/−8
• tests/GADTSpec.hs +40/−14
• tests/Internal.hs +5/−0
• tests/ListSpec.hs +2/−3
• tests/ListTypes.hs +6/−6
• tests/VecSpec.hs +10/−11
• tests/VecTypes.hs +25/−21

@@ -1,3 +1,6 @@+### 0.5.1 [2019.04.26]+* Support `th-abstraction-0.3.0.0` or later.+ ## 0.5 [2018.09.18] * Require `singletons-2.5` and GHC 8.6. 

@@ -1,5 +1,5 @@ name:                eliminators-version:             0.5+version:             0.5.1 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.6.1+tested-with:         GHC == 8.6.4  source-repository head   type:                git@@ -26,16 +26,16 @@   exposed-modules:     Data.Eliminator                        Data.Eliminator.TH                        Data.Eliminator.TypeNats-  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+  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.11 && < 0.4+                     , th-desugar       >= 1.9    && < 1.10   hs-source-dirs:      src   default-language:    Haskell2010-  ghc-options:         -Wall -Wno-unticked-promoted-constructors+  ghc-options:         -Wall -Wcompat -Wno-unticked-promoted-constructors  test-suite spec   type:                exitcode-stdio-1.0@@ -45,6 +45,7 @@                        EqualitySpec                        EqualityTypes                        GADTSpec+                       Internal                        ListSpec                        ListTypes                        VecTypes@@ -57,4 +58,4 @@   build-tool-depends:  hspec-discover:hspec-discover   hs-source-dirs:      tests   default-language:    Haskell2010-  ghc-options:         -Wall -Wno-unticked-promoted-constructors -threaded -rtsopts+  ghc-options:         -Wall -Wcompat -Wno-unticked-promoted-constructors -threaded -rtsopts

@@ -1,3 +1,4 @@+{-# LANGUAGE CPP #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE Unsafe #-} {-|@@ -29,7 +30,7 @@  import           Language.Haskell.TH import           Language.Haskell.TH.Datatype-import           Language.Haskell.TH.Desugar (tupleNameDegree_maybe, unboxedTupleNameDegree_maybe)+import           Language.Haskell.TH.Desugar hiding (NewOrData(..))  {- $conventions 'deriveElim' and 'deriveElimNamed' provide a way to automate the creation of@@ -149,7 +150,12 @@ -- function named @funName@ for the datatype @dataName@. deriveElimNamed :: String -> Name -> Q [Dec] deriveElimNamed funName dataName = do-  info@(DatatypeInfo { datatypeVars    = vars+  info@(DatatypeInfo { datatypeVars    =+#if MIN_VERSION_th_abstraction(0,3,0)+                                         dataVarBndrs+#else+                                         dataVars+#endif                      , datatypeVariant = variant                      , datatypeCons    = cons                      }) <- reifyDatatype dataName@@ -163,7 +169,9 @@   predVar <- newName "p"   singVar <- newName "s"   let elimN = mkName funName-      dataVarBndrs = catMaybes $ map typeToTyVarBndr vars+#if !(MIN_VERSION_th_abstraction(0,3,0))+      dataVarBndrs = freeVariablesWellScoped dataVars+#endif       promDataKind = datatypeType info       predVarBndr = KindedTV predVar (InfixT promDataKind ''(~>) (ConT ''Kind.Type))       singVarBndr = KindedTV singVar promDataKind@@ -283,10 +291,6 @@   = "~>" ++ nStr   where     nStr = nameBase n--typeToTyVarBndr :: Type -> Maybe TyVarBndr-typeToTyVarBndr (SigT (VarT n) k) = Just $ KindedTV n k-typeToTyVarBndr _                 = Nothing  -- Reconstruct and arrow type from the list of types ravel :: [Type] -> Type -> Type

@@ -114,7 +114,7 @@                  -> Decision (S k :~: S m)         stepStep sm _ = decCongS sk (runWhyDecEqNat swhyK sm) -listEqConsequencesSame :: forall (es :: [e]). Sing es -> ListEqConsequences es es+listEqConsequencesSame :: forall e (es :: [e]). Sing es -> ListEqConsequences es es listEqConsequencesSame sl = elimList @e @WhyListEqConsequencesSameSym0 @es sl base step   where     base :: ListEqConsequences '[] '[]@@ -126,24 +126,24 @@          -> ListEqConsequences (x:xs) (x:xs)     step _ _ _ = (Refl, Refl) -useListEq :: forall (xs :: [e]) (ys :: [e]).+useListEq :: forall e (xs :: [e]) (ys :: [e]).              Sing xs -> xs :~: ys -> ListEqConsequences xs ys useListEq sxs xsEqYs = replace @[e] @xs @ys @(ListEqConsequencesSym1 xs)                                (listEqConsequencesSame @e @xs sxs) xsEqYs -nilNotCons :: forall (x :: e) (xs :: [e]). '[] :~: (x:xs) -> Void+nilNotCons :: forall e (x :: e) (xs :: [e]). '[] :~: (x:xs) -> Void nilNotCons = useListEq @e @'[] @(x:xs) SNil -consNotNil :: forall (x :: e) (xs :: [e]). (x:xs) :~: '[] -> Void+consNotNil :: forall e (x :: e) (xs :: [e]). (x:xs) :~: '[] -> Void consNotNil eq = nilNotCons @e @x @xs (sym eq) -consInjective :: forall (x :: e) (xs :: [e]) (y :: e) (ys :: [e]).+consInjective :: forall e (x :: e) (xs :: [e]) (y :: e) (ys :: [e]).                  Sing x -> Sing xs               -> (x:xs) :~: (y:ys)               -> (x :~: y, xs :~: ys) consInjective sx sxs = useListEq @e @(x:xs) @(y:ys) (SCons sx sxs) -decEqNil :: forall (es :: [e]). Sing es -> Decision ('[] :~: es)+decEqNil :: forall e (es :: [e]). Sing es -> Decision ('[] :~: es) decEqNil ses = elimList @e @WhyDecEqNilSym0 @es ses base step   where     base :: Decision ('[] :~: '[])@@ -155,7 +155,7 @@          -> Decision ('[] :~: (x:xs))     step _ _ _ = Disproved (nilNotCons @e @x @xs) -intermixListEqs :: forall (x :: e) (xs :: [e]) (y :: e) (ys :: [e]).+intermixListEqs :: forall e (x :: e) (xs :: [e]) (y :: e) (ys :: [e]).                    x :~: y -> xs :~: ys                 -> (x:xs) :~: (y:ys) intermixListEqs xEqY xsEqYs =@@ -163,7 +163,7 @@           (replace @[e] @xs @ys @(WhyIntermixListEqs2Sym2 x xs) Refl xsEqYs)           xEqY -decCongCons :: forall (x :: e) (xs :: [e]) (y :: e) (ys :: [e]).+decCongCons :: forall e (x :: e) (xs :: [e]) (y :: e) (ys :: [e]).                Sing x -> Sing xs             -> Decision (x :~: y) -> Decision (xs :~: ys)             -> Decision ((x:xs) :~: (y:ys))@@ -193,7 +193,7 @@     injective :: (x:xs) :~: (y:ys) -> (x :~: y, xs :~: ys)     injective = consInjective @e @x @xs @y @ys sx sxs -decEqList :: forall (es1 :: [e]) (es2 :: [e]).+decEqList :: forall e (es1 :: [e]) (es2 :: [e]).              (forall (e1 :: e) (e2 :: e).                      Sing e1 -> Sing e2 -> Decision (e1 :~: e2))           -> Sing es1 -> Sing es2 -> Decision (es1 :~: es2)

@@ -23,10 +23,10 @@   = Proved a   | Disproved (p @@ a @@ Void) -elimDecision :: forall (a :: Type) (p :: PDecision a ~> Type) (d :: PDecision a).+elimDecision :: forall a (p :: PDecision a ~> Type) (d :: PDecision a).                 Sing d-             -> (forall (yes :: a). Sing yes -> p @@ (Proved yes))-             -> (forall (no :: a ~> Void). Sing no -> p @@ (Disproved no))+             -> (forall (yes :: a). Sing yes -> p @@ Proved yes)+             -> (forall (no :: a ~> Void). Sing no -> p @@ Disproved no)              -> p @@ d elimDecision (SProved yes)   pProved _          = pProved yes elimDecision (SDisproved no) _       pDisproved = pDisproved no@@ -40,12 +40,12 @@ type Decision  = Decision' (TyCon (->)) type PDecision = Decision' (~>@#@$) -data instance Sing (z :: PDecision a) where+data instance Sing :: forall a. PDecision a -> Type where   -- It would be lovely to not have to write those (:: PDecision a) kind   -- ascriptions in the return types of each constructor.   -- See https://ghc.haskell.org/trac/ghc/ticket/14111.-  SProved    :: forall (x :: a).         Sing x -> Sing (Proved x    :: PDecision a)-  SDisproved :: forall (r :: a ~> Void). Sing r -> Sing (Disproved r :: PDecision a)+  SProved    :: forall a (x :: a).         Sing x -> Sing (Proved x    :: PDecision a)+  SDisproved :: forall a (r :: a ~> Void). Sing r -> Sing (Disproved r :: PDecision a)  instance SingKind a => SingKind (PDecision a) where   type Demote (PDecision a) = Decision (Demote a)@@ -54,46 +54,41 @@   toSing (Proved x)    = withSomeSing x $ SomeSing . SProved   toSing (Disproved r) = withSomeSing r $ SomeSing . SDisproved -type family NatEqConsequences (a :: Nat) (b :: Nat) :: Type where-  NatEqConsequences Z      Z      = ()-  NatEqConsequences Z      (S _)  = Void-  NatEqConsequences (S _)  Z      = Void-  NatEqConsequences (S k1) (S k2) = k1 :~: k2-$(genDefunSymbols [''NatEqConsequences])+$(singletons [d|+  type family NatEqConsequences (a :: Nat) (b :: Nat) :: Type where+    NatEqConsequences Z      Z      = ()+    NatEqConsequences Z      (S _)  = Void+    NatEqConsequences (S _)  Z      = Void+    NatEqConsequences (S k1) (S k2) = k1 :~: k2 -type WhyNatEqConsequencesSame (a :: Nat) = NatEqConsequences a a-$(genDefunSymbols [''WhyNatEqConsequencesSame])+  type WhyNatEqConsequencesSame (a :: Nat) = NatEqConsequences a a -type WhyDecEqZ (k :: Nat) = Decision (Z :~: k)-$(genDefunSymbols [''WhyDecEqZ])+  type WhyDecEqZ (k :: Nat) = Decision (Z :~: k) -type WhyDecEqS (n :: Nat) (k :: Nat) = Decision (S n :~: k)-$(genDefunSymbols [''WhyDecEqS])+  type WhyDecEqS (n :: Nat) (k :: Nat) = Decision (S n :~: k)+  |])  -- The newtype wrapper is needed to work around -- https://github.com/goldfirere/singletons/issues/198 newtype WhyDecEqNat (k :: Nat) = WhyDecEqNat   { runWhyDecEqNat :: forall (j :: Nat). Sing j -> Decision (k :~: j) } -type family ListEqConsequences (xxs :: [e]) (yys :: [e]) :: Type where-  ListEqConsequences '[]    '[]    = ()-  ListEqConsequences '[]    (_:_)  = Void-  ListEqConsequences (_:_)  '[]    = Void-  ListEqConsequences (x:xs) (y:ys) = (x :~: y, xs :~: ys)-$(genDefunSymbols [''ListEqConsequences])+$(singletons [d|+  type family ListEqConsequences (xxs :: [e]) (yys :: [e]) :: Type where+    ListEqConsequences '[]    '[]    = ()+    ListEqConsequences '[]    (_:_)  = Void+    ListEqConsequences (_:_)  '[]    = Void+    ListEqConsequences (x:xs) (y:ys) = (x :~: y, xs :~: ys) -type WhyListEqConsequencesSame (es :: [e]) = ListEqConsequences es es-$(genDefunSymbols [''WhyListEqConsequencesSame])+  type WhyListEqConsequencesSame (es :: [e]) = ListEqConsequences es es -type WhyDecEqNil (es :: [e]) = Decision ('[] :~: es)-$(genDefunSymbols [''WhyDecEqNil])+  type WhyDecEqNil (es :: [e]) = Decision ('[] :~: es) -type WhyDecEqCons (x :: e) (xs :: [e]) (es :: [e]) = Decision ((x:xs) :~: es)-$(genDefunSymbols [''WhyDecEqCons])+  type WhyDecEqCons (x :: e) (xs :: [e]) (es :: [e]) = Decision ((x:xs) :~: es) -type WhyIntermixListEqs1 (x :: e) (xs :: [e]) (ys :: [e]) (k :: e) = (x:xs) :~: (k:ys)-type WhyIntermixListEqs2 (x :: e) (xs :: [e]) (k :: [e])           = (x:xs) :~: (x:k)-$(genDefunSymbols [''WhyIntermixListEqs1, ''WhyIntermixListEqs2])+  type WhyIntermixListEqs1 (x :: e) (xs :: [e]) (ys :: [e]) (k :: e) = (x:xs) :~: (k:ys)+  type WhyIntermixListEqs2 (x :: e) (xs :: [e]) (k :: [e])           = (x:xs) :~: (x:k)+  |])  -- The newtype wrapper is needed to work around -- https://github.com/goldfirere/singletons/issues/198

@@ -16,6 +16,7 @@ import           Data.Type.Equality ((:~:)(..), (:~~:)(..))  import           EqualityTypes+import           Internal  import           Test.Hspec @@ -33,23 +34,37 @@  ----- -j :: forall (k :: Type) (a :: k) (b :: k)-            (p :: forall (x :: k) (y :: k). x :~: y ~> Type)+j :: forall k (p :: forall (x :: k) (y :: k). x :~: y ~> Type)+            (a :: k) (b :: k)             (r :: a :~: b).      Sing r   -> (forall (x :: k). p @@ (Refl :: x :~: x))   -> p @@ r j SRefl pRefl = pRefl @a -hj :: forall (j :: Type) (k :: Type) (a :: j) (b :: k)-             (p :: forall (y :: Type) (z :: Type) (w :: y) (x :: z). w :~~: x ~> Type)+jProp :: forall k (p :: k ~> k ~> Prop)+                (a :: k) (b :: k).+         a :~: b+      -> (forall (x :: k). p @@ x @@ x)+      -> p @@ a @@ b+jProp Refl pRefl = pRefl @a++hj :: forall (p :: forall y z (w :: y) (x :: z). w :~~: x ~> Type)+             j k (a :: j) (b :: k)              (r :: a :~~: b).       Sing r-   -> (forall (y :: Type) (w :: y). p @@ (HRefl :: w :~~: w))+   -> (forall y (w :: y). p @@ (HRefl :: w :~~: w))    -> p @@ r-hj SHRefl pHRefl = pHRefl @k @a+hj SHRefl pHRefl = pHRefl @j @a -k :: forall (k :: Type) (a :: k)+hjProp :: forall (p :: forall y z. y ~> z ~> Prop)+                 j k (a :: j) (b :: k).+          a :~~: b+       -> (forall y (w :: y). p @@ w @@ w)+       -> p @@ a @@ b+hjProp HRefl pHRefl = pHRefl @j @a++k :: forall k (a :: k)             (p :: a :~: a ~> Type)             (r :: a :~: a).      Sing r@@ -57,7 +72,7 @@   -> p @@ r k SRefl pRefl = pRefl -hk :: forall (k :: Type) (a :: k)+hk :: forall k (a :: k)              (p :: a :~~: a ~> Type)              (r :: a :~~: a).       Sing r@@ -65,64 +80,64 @@    -> p @@ r hk SHRefl pHRefl = pHRefl -sym :: forall (t :: Type) (a :: t) (b :: t).+sym :: forall t (a :: t) (b :: t).        a :~: b -> b :~: a sym eq = withSomeSing eq $ \(singEq :: Sing r) ->-           (~>:~:) @t @a @b @(WhySymSym1 a) @r singEq Refl+           (~>:~:) @t @a @(WhySymSym1 a) @b @r singEq Refl -hsym :: forall (j :: Type) (k :: Type) (a :: j) (b :: k).+hsym :: forall j k (a :: j) (b :: k).         a :~~: b -> b :~~: a hsym eq = withSomeSing eq $ \(singEq :: Sing r) ->-            (~>:~~:) @j @k @a @b @(WhyHsymSym1 a) @r singEq HRefl+            (~>:~~:) @j @a @(WhyHsymSym1 a) @k @b @r singEq HRefl -symIdempotent :: forall (t :: Type) (a :: t) (b :: t)+symIdempotent :: forall t (a :: t) (b :: t)                         (e :: a :~: b).                  Sing e -> Symmetry (Symmetry e) :~: e-symIdempotent se = (~>:~:) @t @a @b @(WhySymIdempotentSym1 a) @e se Refl+symIdempotent se = (~>:~:) @t @a @(WhySymIdempotentSym1 a) @b @e se Refl -hsymIdempotent :: forall (j :: Type) (k :: Type) (a :: j) (b :: k)+hsymIdempotent :: forall j k (a :: j) (b :: k)                          (e :: a :~~: b).                   Sing e -> Hsymmetry (Hsymmetry e) :~: e-hsymIdempotent se = (~>:~~:) @j @k @a @b @(WhyHsymIdempotentSym1 a) @e se Refl+hsymIdempotent se = (~>:~~:) @j @a @(WhyHsymIdempotentSym1 a) @k @b @e se Refl -replace :: forall (t :: Type) (from :: t) (to :: t) (p :: t ~> Type).+replace :: forall t (from :: t) (to :: t) (p :: t ~> Type).            p @@ from         -> from :~: to         -> p @@ to replace from eq =   withSomeSing eq $ \(singEq :: Sing r) ->-    (~>:~:) @t @from @to @(WhyReplaceSym2 from p) @r singEq from+    (~>:~:) @t @from @(WhyReplaceSym2 from p) @to @r singEq from  -- Doesn't work due to https://ghc.haskell.org/trac/ghc/ticket/11719 {--hreplace :: forall (j :: Type) (k :: Type) (from :: j) (to :: k)-                   (p :: forall (z :: Type). z ~> Type).+hreplace :: forall j k (from :: j) (to :: k)+                   (p :: forall z. z ~> Type).             p @@ from          -> from :~~: to          -> p @@ to hreplace from heq =-  withSomeSing eq $ \(singEq :: Sing r) ->-    (@~>:~~:) @j @k @from @to @(WhyHreplaceSym2 from p) singEq from+  withSomeSing heq $ \(singEq :: Sing r) ->+    (~>:~~:) @j @from @(WhyHreplaceSym2 from p) @k @to @r singEq from -} -leibniz :: forall (t :: Type) (f :: t ~> Type) (a :: t) (b :: t).+leibniz :: forall t (f :: t ~> Type) (a :: t) (b :: t).            a :~: b         -> f @@ a         -> f @@ b leibniz = replace @t @a @b @(WhyLeibnizSym2 f a) id -cong :: forall (x :: Type) (y :: Type) (f :: x ~> y)+cong :: forall x y (f :: x ~> y)                (a :: x) (b :: x).         a :~: b      -> f @@ a :~: f @@ b cong eq =   withSomeSing eq $ \(singEq :: Sing r) ->-    (~>:~:) @x @a @b @(WhyCongSym2 f a) @r singEq Refl+    (~>:~:) @x @a @(WhyCongSym2 f a) @b @r singEq Refl -eqIsRefl :: forall (k :: Type) (a :: k) (b :: k) (e :: a :~: b).+eqIsRefl :: forall k (a :: k) (b :: k) (e :: a :~: b).             Sing e -> e :~~: (Refl :: a :~: a)-eqIsRefl eq = (~>:~:) @k @a @b @(WhyEqIsReflSym1 a) @e eq HRefl+eqIsRefl eq = (~>:~:) @k @a @(WhyEqIsReflSym1 a) @b @e eq HRefl -heqIsHRefl :: forall (j :: Type) (k :: Type) (a :: j) (b :: k) (e :: a :~~: b).+heqIsHRefl :: forall j k (a :: j) (b :: k) (e :: a :~~: b).               Sing e -> e :~~: (HRefl :: a :~~: a)-heqIsHRefl heq = (~>:~~:) @j @k @a @b @(WhyHEqIsHReflSym1 a) @e heq HRefl+heqIsHRefl heq = (~>:~~:) @j @a @(WhyHEqIsHReflSym1 a) @k @b @e heq HRefl

@@ -16,7 +16,9 @@ import           Data.Singletons.TH import           Data.Type.Equality ((:~:)(..), (:~~:)(..)) -data instance Sing (z :: a :~: b) where+import           Internal++data instance Sing :: forall k (a :: k) (b :: k). a :~: b -> Type where   SRefl :: Sing Refl type (%:~:) = (Sing :: (a :: k) :~: (b :: k) -> Type) @@ -29,15 +31,23 @@   sing = SRefl  -- | Christine Paulin-Mohring's version of the J rule.-(~>:~:) :: forall (k :: Type) (a :: k) (b :: k)+(~>:~:) :: forall k (a :: k)                   (p :: forall (y :: k). a :~: y ~> Type)-                  (r :: a :~: b).+                  (b :: k) (r :: a :~: b).            Sing r         -> p @@ Refl         -> p @@ r (~>:~:) SRefl pRefl = pRefl -data instance Sing (z :: a :~~: b) where+(~>!:~:) :: forall k (a :: k)+                   (p :: k ~> Prop)+                   (b :: k).+            a :~: b+         -> p @@ a+         -> p @@ b+(~>!:~:) Refl pRefl = pRefl++data instance Sing :: forall j k (a :: j) (b :: k). a :~~: b -> Type where   SHRefl :: Sing HRefl type (%:~~:) = (Sing :: (a :: j) :~~: (b :: k) -> Type) @@ -50,14 +60,22 @@   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).+(~>:~~:) :: forall j (a :: j)+                   (p :: forall z (y :: z). a :~~: y ~> Type)+                   k (b :: k) (r :: a :~~: b).             Sing r          -> p @@ HRefl          -> p @@ r (~>:~~:) SHRefl pHRefl = pHRefl +(~>!:~~:) :: forall j (a :: j)+                    (p :: forall z. z ~> Prop)+                    k (b :: k).+             a :~~: b+          -> p @@ a+          -> p @@ b+(~>!:~~:) HRefl pHRefl = pHRefl+ -----  $(singletons [d|@@ -85,7 +103,7 @@    -- Doesn't work due to https://ghc.haskell.org/trac/ghc/ticket/11719   {--  type family WhyHreplace (from :: j) (p :: forall (z :: Type). z ~> Type)+  type family WhyHreplace (from :: j) (p :: forall z. z ~> Type)                           (e :: from :~~: (y :: k)) :: Type where     WhyHreplace from p (_ :: from :~~: y) = p @@ y   -}

@@ -12,6 +12,8 @@ import Data.Kind import Data.Singletons +import Internal+ import Test.Hspec  main :: IO ()@@ -25,31 +27,37 @@ data So :: Bool -> Type where   Oh :: So True -data instance Sing (z :: So what) where+data instance Sing :: forall (what :: Bool). So what -> Type 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).+elimSo :: forall (p :: forall (long_sucker :: Bool). So long_sucker ~> Type)+                 (what :: Bool) (s :: So what).           Sing s        -> p @@ Oh        -> p @@ s elimSo SOh pOh = pOh -data Flarble (a :: Type) (b :: Type) where+elimPropSo :: forall (p :: Bool ~> Prop) (what :: Bool).+              So what+           -> p @@ True+           -> p @@ what+elimPropSo Oh pOh = pOh++data Flarble :: Type -> Type -> Type where   MkFlarble1 :: a -> Flarble a b   MkFlarble2 :: a ~ Bool => Flarble a (Maybe b) -data instance Sing (z :: Flarble a b) where+data instance Sing :: forall a b. Flarble a b -> Type 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)-                      (f :: Flarble a b).+elimFlarble :: forall (p :: forall x y. Flarble x y ~> Type)+                      a b (f :: Flarble a b).                Sing f-            -> (forall (a' :: Type) (b' :: Type) (x :: a'). Sing x -> p @@ (MkFlarble1 x :: Flarble a' b'))-            -> (forall (b' :: Type). p @@ (MkFlarble2 :: Flarble Bool (Maybe b')))+            -> (forall a' b' (x :: a'). Sing x -> p @@ (MkFlarble1 x :: Flarble a' b'))+            -> (forall b'. p @@ (MkFlarble2 :: Flarble Bool (Maybe b')))             -> p @@ f elimFlarble s@(SMkFlarble1 sx) pMkFlarble1 _ =   case s of@@ -58,15 +66,33 @@   case s of     (_ :: Sing (MkFlarble2 :: Flarble Bool (Maybe b'))) -> pMkFlarble2 @b' +elimPropFlarble :: forall (p :: Type ~> Type ~> Prop) a b.+                   Flarble a b+                -> (forall a' b'. a -> p @@ a' @@ b')+                -> (forall b'. p @@ Bool @@ Maybe b')+                -> p @@ a @@ b+elimPropFlarble f@(MkFlarble1 x) pMkFlarble1 _ =+  case f of+    (_ :: Flarble a' b') -> pMkFlarble1 @a' @b' x+elimPropFlarble f@MkFlarble2 _ pMkFlarble2 =+  case f of+    (_ :: Flarble Bool (Maybe b')) -> pMkFlarble2 @b'+ data Obj :: Type where   MkObj :: o -> Obj -data instance Sing (z :: Obj) where-  SMkObj :: forall (obj :: obiwan). Sing obj -> Sing (MkObj obj)+data instance Sing :: Obj -> Type where+  SMkObj :: forall obiwan (obj :: obiwan). Sing obj -> Sing (MkObj obj) type SObj = (Sing :: Obj -> Type) -elimObj :: forall (o :: Obj) (p :: Obj ~> Type).+elimObj :: forall (p :: Obj ~> Type) (o :: Obj).            Sing o-        -> (forall (obj :: Type) (x :: obj). Sing x -> p @@ (MkObj x))+        -> (forall obj (x :: obj). Sing x -> p @@ MkObj x)         -> p @@ o-elimObj (SMkObj (x :: Sing (obj :: obiwan))) pMkObj = pMkObj @obiwan @obj x+elimObj (SMkObj (sx :: Sing (x :: obj))) pMkObj = pMkObj @obj @x sx++elimPropObj :: forall (p :: Prop).+               Obj+            -> (forall obj. obj -> p)+            -> p+elimPropObj (MkObj o) pMkObj = pMkObj o

@@ -0,0 +1,5 @@+module Internal where++import Data.Kind++type Prop = Type

@@ -10,7 +10,6 @@ module ListSpec where  import Data.Eliminator-import Data.Kind import Data.Singletons.Prelude import Data.Singletons.Prelude.List import Data.Type.Equality@@ -29,7 +28,7 @@  ----- -mapPreservesLength :: forall (x :: Type) (y :: Type) (f :: x ~> y) (l :: [x]).+mapPreservesLength :: forall x y (f :: x ~> y) (l :: [x]).                       SingI l                    => Length l :~: Length (Map f l) mapPreservesLength@@ -44,7 +43,7 @@          -> WhyMapPreservesLength f (s:ss)     step _ _ = cong @_ @_ @((+@#@$$) 1) -mapFusion :: forall (x :: Type) (y :: Type) (z :: Type)+mapFusion :: forall x y z                     (f :: y ~> z) (g :: x ~> y) (l :: [x]).                     SingI l                  => Map f (Map g l) :~: Map (f .@#@$$$ g) l

@@ -11,10 +11,10 @@ import Data.Singletons.Prelude.List import Data.Singletons.TH -type WhyMapPreservesLength (f :: x ~> y) (l :: [x])-  = Length l :~: Length (Map f l)-$(genDefunSymbols [''WhyMapPreservesLength])+$(singletons [d|+  type WhyMapPreservesLength (f :: x ~> y) (l :: [x])+    = Length l :~: Length (Map f l) -type WhyMapFusion (f :: y ~> z) (g :: x ~> y) (l :: [x])-  = Map f (Map g l) :~: Map (f .@#@$$$ g) l-$(genDefunSymbols [''WhyMapFusion])+  type WhyMapFusion (f :: y ~> z) (g :: x ~> y) (l :: [x])+    = Map f (Map g l) :~: Map (f .@#@$$$ g) l+  |])

@@ -8,7 +8,6 @@ module VecSpec where  import Data.Eliminator-import Data.Kind (Type) import Data.Nat import Data.Singletons import Data.Singletons.Prelude.Num@@ -69,14 +68,14 @@  ----- -replicateVec :: forall (e :: Type) (howMany :: Nat).+replicateVec :: forall e (howMany :: Nat).                 Sing howMany -> e -> Vec e howMany replicateVec s e = elimNat @(TyCon (Vec e)) @howMany s VNil step   where     step :: forall (k :: Nat). Sing k -> Vec e k -> Vec e (S k)     step _ = (e :#) -mapVec :: forall (a :: Type) (b :: Type) (n :: Nat).+mapVec :: forall a b (n :: Nat).           SingI n        => (a -> b) -> Vec a n -> Vec b n mapVec f = elimNat @(WhyMapVecSym2 a b) @n (sing @n) base step@@ -87,7 +86,7 @@     step :: forall (k :: Nat). Sing k -> WhyMapVec a b k -> WhyMapVec a b (S k)     step _ mapK vK = f (vhead vK) :# mapK (vtail vK) -zipWithVec :: forall (a :: Type) (b :: Type) (c :: Type) (n :: Nat).+zipWithVec :: forall a b c (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@@ -102,7 +101,7 @@     step _ zwK vaK vbK = f   (vhead vaK) (vhead vbK)                       :# zwK (vtail vaK) (vtail vbK) -appendVec :: forall (e :: Type) (n :: Nat) (m :: Nat).+appendVec :: forall e (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@@ -116,7 +115,7 @@          -> WhyAppendVec e m (S k)     step _ avK vK1 vK2 = vhead vK1 :# avK (vtail vK1) vK2 -transposeVec :: forall (e :: Type) (n :: Nat) (m :: Nat).+transposeVec :: forall e (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@@ -130,17 +129,17 @@          -> WhyTransposeVec e m (S k)     step _ transK vK = zipWithVec (:#) (vhead vK) (transK (vtail vK)) -concatVec :: forall (e :: Type) (n :: Nat) (j :: Nat).+concatVec :: forall e (n :: Nat) (j :: Nat).              (SingKind e, SingI j, e ~ Demote e)           => Vec (Vec e j) n -> Vec e (n * j) concatVec l = withSomeSing l $ \(singL :: Sing l) ->-                elimVec @(Vec e j) @n @(WhyConcatVecSym e j) @l singL base step+                elimVec @(Vec e j) @(WhyConcatVecSym2 e j) @n @l singL base step   where-    base :: WhyConcatVec e j Z VNil+    base :: WhyConcatVec e j VNil     base = VNil      step :: forall (k :: Nat) (x :: Vec e j) (xs :: Vec (Vec e j) k).                    Sing x -> Sing xs-                -> WhyConcatVec e j k     xs-                -> WhyConcatVec e j (S k) (x :# xs)+                -> WhyConcatVec e j xs+                -> WhyConcatVec e j (x :# xs)     step h _ vKJ = appendVec (fromSing h) vKJ

@@ -17,6 +17,7 @@ import Data.Nat import Data.Singletons.Prelude.Num import Data.Singletons.TH+import Internal  data Vec :: Type -> Nat -> Type where   VNil :: Vec a Z@@ -26,7 +27,7 @@ deriving instance Ord a  => Ord (Vec a n) deriving instance Show a => Show (Vec a n) -data instance Sing (z :: Vec a n) where+data instance Sing :: forall a (n :: Nat). Vec a n -> Type where   SVNil :: Sing VNil   (:%#) :: { sVhead :: Sing x, sVtail :: Sing xs } -> Sing (x :# xs) type SVec = (Sing :: Vec a n -> Type)@@ -48,8 +49,8 @@ instance (SingI x, SingI xs) => SingI (x :# xs) where   sing = sing :%# sing -elimVec :: forall (a :: Type) (n :: Nat)-                  (p :: forall (k :: Nat). Vec a k ~> Type) (v :: Vec a n).+elimVec :: forall a (p :: forall (k :: Nat). Vec a k ~> Type)+                  (n :: Nat) (v :: Vec a n).            Sing v         -> p @@ VNil         -> (forall (k :: Nat) (x :: a) (xs :: Vec a k).@@ -57,26 +58,29 @@         -> p @@ v elimVec SVNil pVNil _ = pVNil elimVec (sx :%# (sxs :: Sing (xs :: Vec a k))) pVNil pVCons =-  pVCons sx sxs (elimVec @a @k @p @xs sxs pVNil pVCons)+  pVCons sx sxs (elimVec @a @p @k @xs sxs pVNil pVCons) -type WhyMapVec (a :: Type) (b :: Type) (n :: Nat) = Vec a n -> Vec b n-$(genDefunSymbols [''WhyMapVec])+elimPropVec :: forall a (p :: Nat ~> Prop) (n :: Nat).+               Vec a n+            -> p @@ Z+            -> (forall (k :: Nat). a -> Vec a k -> p @@ k -> p @@ S k)+            -> p @@ n+elimPropVec VNil pZ _ = pZ+elimPropVec (x :# (xs :: Vec a k)) pZ pS =+  pS x xs (elimPropVec @a @p @k xs pZ pS) -type WhyZipWithVec (a :: Type) (b :: Type) (c :: Type) (n :: Nat)-  = Vec a n -> Vec b n -> Vec c n-$(genDefunSymbols [''WhyZipWithVec])+$(singletons [d|+  type WhyMapVec a b (n :: Nat) = Vec a n -> Vec b n -type WhyAppendVec (e :: Type) (m :: Nat) (n :: Nat)-  = Vec e n -> Vec e m -> Vec e (n + m)-$(genDefunSymbols [''WhyAppendVec])+  type WhyZipWithVec a b c (n :: Nat)+    = Vec a n -> Vec b n -> Vec c n -type WhyTransposeVec (e :: Type) (m :: Nat) (n :: Nat)-  = Vec (Vec e m) n -> Vec (Vec e n) m-$(genDefunSymbols [''WhyTransposeVec])+  type WhyAppendVec e (m :: Nat) (n :: Nat)+    = Vec e n -> Vec e m -> Vec e (n + m) -type WhyConcatVec (e :: Type) (j :: Nat) (n :: Nat) (l :: Vec (Vec e j) n)-  = Vec e (n * j)-data WhyConcatVecSym (e :: Type) (j :: Nat)-  :: forall (n :: Nat). Vec (Vec e j) n ~> Type-type instance Apply (WhyConcatVecSym e j :: Vec (Vec e j) n ~> Type) l-  = WhyConcatVec e j n l+  type WhyTransposeVec e (m :: Nat) (n :: Nat)+    = Vec (Vec e m) n -> Vec (Vec e n) m++  type family WhyConcatVec e (j :: Nat) (l :: Vec (Vec e j) n) :: Type where+    WhyConcatVec e j (l :: Vec (Vec e j) n) = Vec e (n * j)+  |])