eliminators 0.5.1 → 0.6

raw patch · 10 files changed

+304/−133 lines, 10 filesdep ~basedep ~extradep ~singletonsPVP ok

version bump matches the API change (PVP)

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

API changes (from Hackage documentation)

Files

• CHANGELOG.md +3/−0
• eliminators.cabal +11/−11
• src/Data/Eliminator.hs +1/−1
• src/Data/Eliminator/TH.hs +2/−32
• tests/DecideSpec.hs +2/−2
• tests/DecideTypes.hs +13/−18
• tests/EqualitySpec.hs +138/−12
• tests/EqualityTypes.hs +110/−34
• tests/GADTSpec.hs +10/−10
• tests/VecTypes.hs +14/−13

@@ -1,3 +1,6 @@+## 0.6 [2019.08.27]+* Require `singletons-2.6` and GHC 8.8.+ ### 0.5.1 [2019.04.26] * Support `th-abstraction-0.3.0.0` or later. 

@@ -1,5 +1,5 @@ name:                eliminators-version:             0.5.1+version:             0.6 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.4+tested-with:         GHC == 8.8.1  source-repository head   type:                git@@ -26,13 +26,13 @@   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.11 && < 0.4-                     , th-desugar       >= 1.9    && < 1.10+  build-depends:       base             >= 4.13  && < 4.14+                     , extra            >= 1.4.2 && < 1.7+                     , singletons       >= 2.6   && < 2.7+                     , singleton-nats   >= 0.4.2 && < 0.5+                     , template-haskell >= 2.15  && < 2.16+                     , th-abstraction   >= 0.3   && < 0.4+                     , th-desugar       >= 1.10  && < 1.11   hs-source-dirs:      src   default-language:    Haskell2010   ghc-options:         -Wall -Wcompat -Wno-unticked-promoted-constructors@@ -50,10 +50,10 @@                        ListTypes                        VecTypes                        VecSpec-  build-depends:       base           >= 4.12  && < 4.13+  build-depends:       base           >= 4.13  && < 4.14                      , eliminators                      , hspec          >= 2     && < 3-                     , singletons     >= 2.5   && < 2.6+                     , singletons     >= 2.6   && < 2.7                      , singleton-nats >= 0.4.2 && < 0.5   build-tool-depends:  hspec-discover:hspec-discover   hs-source-dirs:      tests

@@ -48,7 +48,7 @@ import Data.List.NonEmpty (NonEmpty(..)) import Data.Nat import Data.Singletons.Prelude-import Data.Singletons.Prelude.List.NonEmpty (Sing(..))+import Data.Singletons.Prelude.List.NonEmpty (SNonEmpty(..)) import Data.Void (Void)  import Language.Haskell.TH.Desugar (tupleNameDegree_maybe)

@@ -1,4 +1,3 @@-{-# LANGUAGE CPP #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE Unsafe #-} {-|@@ -24,7 +23,6 @@ import           Data.Char (isUpper) import           Data.Foldable import qualified Data.Kind as Kind (Type)-import           Data.List.NonEmpty (NonEmpty(..)) import           Data.Maybe import           Data.Singletons.Prelude @@ -150,12 +148,7 @@ -- function named @funName@ for the datatype @dataName@. deriveElimNamed :: String -> Name -> Q [Dec] deriveElimNamed funName dataName = do-  info@(DatatypeInfo { datatypeVars    =-#if MIN_VERSION_th_abstraction(0,3,0)-                                         dataVarBndrs-#else-                                         dataVars-#endif+  info@(DatatypeInfo { datatypeVars    = dataVarBndrs                      , datatypeVariant = variant                      , datatypeCons    = cons                      }) <- reifyDatatype dataName@@ -169,9 +162,6 @@   predVar <- newName "p"   singVar <- newName "s"   let elimN = mkName funName-#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@@ -256,7 +246,7 @@ mbInductiveCase :: Name -> Type -> a -> Maybe a mbInductiveCase dataName varType inductiveArg   = case unfoldType varType of-      headTy :| _+      (headTy, _)           -- Annoying special case for lists         | ListT <- headTy         , dataName == ''[]@@ -304,26 +294,6 @@ -- apply an expression to a list of types foldAppType :: Exp -> [Type] -> Exp foldAppType = foldl' AppTypeE---- | Decompose an applied type into its individual components. For example, this:------ @--- Either Int Char--- @------ would be unfolded to this:------ @--- Either :| [Int, Char]--- @-unfoldType :: Type -> NonEmpty Type-unfoldType = go []-  where-    go :: [Type] -> Type -> NonEmpty Type-    go acc (AppT t1 t2)    = go (t2:acc) t1-    go acc (SigT t _)      = go acc t-    go acc (ForallT _ _ t) = go acc t-    go acc t               = t :| acc  tyVarBndrName :: TyVarBndr -> Name tyVarBndrName (PlainTV  n)   = n

@@ -93,7 +93,7 @@     right no = Disproved $ fromSing no . sInjective @n @j sn  decEqNat :: forall (n :: Nat) (j :: Nat). Sing n -> Sing j -> Decision (n :~: j)-decEqNat sn = runWhyDecEqNat (elimNat @(TyCon WhyDecEqNat) @n sn base step)+decEqNat sn = runWhyDecEqNat $ elimNat @(TyCon WhyDecEqNat) @n sn base step   where     base :: WhyDecEqNat Z     base = WhyDecEqNat decEqZ@@ -197,7 +197,7 @@              (forall (e1 :: e) (e2 :: e).                      Sing e1 -> Sing e2 -> Decision (e1 :~: e2))           -> Sing es1 -> Sing es2 -> Decision (es1 :~: es2)-decEqList f ses1 = runWhyDecEqList (elimList @e @(TyCon1 WhyDecEqList) @es1 ses1 base step)+decEqList f ses1 = runWhyDecEqList $ elimList @e @(TyCon1 WhyDecEqList) @es1 ses1 base step   where     base :: WhyDecEqList '[]     base = WhyDecEqList decEqNil

@@ -40,12 +40,10 @@ type Decision  = Decision' (TyCon (->)) type PDecision = Decision' (~>@#@$) -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 a (x :: a).         Sing x -> Sing (Proved x    :: PDecision a)-  SDisproved :: forall a (r :: a ~> Void). Sing r -> Sing (Disproved r :: PDecision a)+data SDecision :: forall a. PDecision a -> Type where+  SProved    :: forall a (x :: a).         Sing x -> SDecision (Proved x)+  SDisproved :: forall a (r :: a ~> Void). Sing r -> SDecision (Disproved r)+type instance Sing = SDecision  instance SingKind a => SingKind (PDecision a) where   type Demote (PDecision a) = Decision (Demote a)@@ -54,6 +52,15 @@   toSing (Proved x)    = withSomeSing x $ SomeSing . SProved   toSing (Disproved r) = withSomeSing r $ SomeSing . SDisproved +-----++-- These newtype wrappers are needed to work around+-- https://gitlab.haskell.org/ghc/ghc/issues/9269+newtype WhyDecEqNat (k :: Nat) = WhyDecEqNat+  { runWhyDecEqNat :: forall (j :: Nat). Sing j -> Decision (k :~: j) }+newtype WhyDecEqList (l1 :: [e]) = WhyDecEqList+  { runWhyDecEqList :: forall (l2 :: [e]). Sing l2 -> Decision (l1 :~: l2) }+ $(singletons [d|   type family NatEqConsequences (a :: Nat) (b :: Nat) :: Type where     NatEqConsequences Z      Z      = ()@@ -66,14 +73,7 @@   type WhyDecEqZ (k :: Nat) = Decision (Z :~: k)    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) }--$(singletons [d|   type family ListEqConsequences (xxs :: [e]) (yys :: [e]) :: Type where     ListEqConsequences '[]    '[]    = ()     ListEqConsequences '[]    (_:_)  = Void@@ -89,8 +89,3 @@   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-newtype WhyDecEqList (l1 :: [e]) = WhyDecEqList-  { runWhyDecEqList :: forall (l2 :: [e]). Sing l2 -> Decision (l1 :~: l2) }

@@ -25,12 +25,15 @@  spec :: Spec spec = parallel $ do-  describe "sym" $+  describe "sym" $ do+    let boolEq :: Bool :~: Bool+        boolEq = Refl     it "behaves like the one from Data.Type.Equality" $ do-      let boolEq :: Bool :~: Bool-          boolEq = Refl       sym boolEq       `shouldBe` DTE.sym boolEq       sym (sym boolEq) `shouldBe` DTE.sym (DTE.sym boolEq)+    it "behaves like the one from Data.Type.Equality" $ do+      trans boolEq boolEq       `shouldBe` DTE.trans boolEq boolEq+      trans boolEq (sym boolEq) `shouldBe` Refl  ----- @@ -38,7 +41,7 @@             (a :: k) (b :: k)             (r :: a :~: b).      Sing r-  -> (forall (x :: k). p @@ (Refl :: x :~: x))+  -> (forall (x :: k). p @@ (Refl @x))   -> p @@ r j SRefl pRefl = pRefl @a @@ -53,7 +56,7 @@              j k (a :: j) (b :: k)              (r :: a :~~: b).       Sing r-   -> (forall y (w :: y). p @@ (HRefl :: w :~~: w))+   -> (forall y (w :: y). p @@ (HRefl @w))    -> p @@ r hj SHRefl pHRefl = pHRefl @j @a @@ -85,11 +88,19 @@ sym eq = withSomeSing eq $ \(singEq :: Sing r) ->            (~>:~:) @t @a @(WhySymSym1 a) @b @r singEq Refl +sSym :: forall t (a :: t) (b :: t) (e :: a :~: b).+        Sing e -> Sing (Symmetry e)+sSym se = (~>:~:) @t @a @(WhySSymSym1 a) @b @e se SRefl+ hsym :: forall j k (a :: j) (b :: k).         a :~~: b -> b :~~: a hsym eq = withSomeSing eq $ \(singEq :: Sing r) ->-            (~>:~~:) @j @a @(WhyHsymSym1 a) @k @b @r singEq HRefl+            (~>:~~:) @j @a @(WhyHSymSym1 a) @k @b @r singEq HRefl +sHSym :: forall j k (a :: j) (b :: k) (e :: a :~~: b).+         Sing e -> Sing (HSymmetry e)+sHSym se = (~>:~~:) @j @a @(WhySHSymSym1 a) @k @b @e se SHRefl+ symIdempotent :: forall t (a :: t) (b :: t)                         (e :: a :~: b).                  Sing e -> Symmetry (Symmetry e) :~: e@@ -97,9 +108,21 @@  hsymIdempotent :: forall j k (a :: j) (b :: k)                          (e :: a :~~: b).-                  Sing e -> Hsymmetry (Hsymmetry e) :~: e-hsymIdempotent se = (~>:~~:) @j @a @(WhyHsymIdempotentSym1 a) @k @b @e se Refl+                  Sing e -> HSymmetry (HSymmetry e) :~: e+hsymIdempotent se = (~>:~~:) @j @a @(WhyHSymIdempotentSym1 a) @k @b @e se Refl +trans :: forall t (a :: t) (b :: t) (c :: t).+                a :~: b -> b :~: c -> a :~: c+trans eq1 eq2 = withSomeSing eq1 $ \(singEq1 :: Sing r) ->+                  unwrapTrans ((~>:~:) @t @a @(WhyTransSym1 a) @b @r+                                       singEq1 (WrapTrans id)) eq2++htrans :: forall j k l (a :: j) (b :: k) (c :: l).+                 a :~~: b -> b :~~: c -> a :~~: c+htrans eq1 eq2 = withSomeSing eq1 $ \(singEq1 :: Sing r) ->+                   unwrapHTrans ((~>:~~:) @j @a @(WhyHTransSym1 a) @k @b @r+                                          singEq1 (WrapHTrans id)) eq2+ replace :: forall t (from :: t) (to :: t) (p :: t ~> Type).            p @@ from         -> from :~: to@@ -108,8 +131,6 @@   withSomeSing eq $ \(singEq :: Sing r) ->     (~>:~:) @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 k (from :: j) (to :: k)                    (p :: forall z. z ~> Type).             p @@ from@@ -117,8 +138,7 @@          -> p @@ to hreplace from heq =   withSomeSing heq $ \(singEq :: Sing r) ->-    (~>:~~:) @j @from @(WhyHreplaceSym2 from p) @k @to @r singEq from--}+    (~>:~~:) @j @from @(WhyHReplaceSym2 from (WrapPred p)) @k @to @r singEq from  leibniz :: forall t (f :: t ~> Type) (a :: t) (b :: t).            a :~: b@@ -126,6 +146,12 @@         -> f @@ b leibniz = replace @t @a @b @(WhyLeibnizSym2 f a) id +hleibniz :: forall (f :: forall t. t ~> Type) j k (a :: j) (b :: k).+            a :~~: b+         -> f @@ a+         -> f @@ b+hleibniz = hreplace @j @k @a @b @(WhyHLeibnizSym2 (WrapPred f) a) id+ cong :: forall x y (f :: x ~> y)                (a :: x) (b :: x).         a :~: b@@ -141,3 +167,103 @@ heqIsHRefl :: forall j k (a :: j) (b :: k) (e :: a :~~: b).               Sing e -> e :~~: (HRefl :: a :~~: a) heqIsHRefl heq = (~>:~~:) @j @a @(WhyHEqIsHReflSym1 a) @k @b @e heq HRefl++transLeft :: forall j (a :: j) (b :: j) (e :: a :~: b).+             Sing e -> Trans e Refl :~: e+transLeft se = leibniz @(a :~: b) @(WhyTransLeftSym1 a)+                       @(Symmetry (Symmetry e)) @e+                       (symIdempotent se) transLeftHelper+  where+    transLeftHelper :: Trans (Symmetry (Symmetry e)) Refl+                   :~: Symmetry (Symmetry e)+    transLeftHelper = (~>:~:) @j @b @(WhyTransLeftHelperSym1 b) @a @(Symmetry e)+                              (sSym se) Refl++htransLeft :: forall j k (a :: j) (b :: k) (e :: a :~~: b).+              Sing e -> HTrans e HRefl :~: e+htransLeft se = leibniz @(a :~~: b) @(WhyHTransLeftSym1 a)+                        @(HSymmetry (HSymmetry e)) @e+                        (hsymIdempotent se) htransLeftHelper+  where+    htransLeftHelper :: HTrans (HSymmetry (HSymmetry e)) HRefl+                    :~: HSymmetry (HSymmetry e)+    htransLeftHelper = (~>:~~:) @k @b @(WhyHTransLeftHelperSym1 b) @j @a @(HSymmetry e)+                                (sHSym se) Refl++transRight :: forall j (a :: j) (b :: j) (e :: a :~: b).+              Sing e -> Trans Refl e :~: e+transRight se = (~>:~:) @j @a @(WhyTransRightSym1 a) @b @e se Refl++htransRight :: forall j k (a :: j) (b :: k) (e :: a :~~: b).+               Sing e -> HTrans HRefl e :~: e+htransRight se = (~>:~~:) @j @a @(WhyHTransRightSym1 a) @k @b @e se Refl++-- Commented out for now, since these take ages to compile :(+-- Perhaps https://gitlab.haskell.org/ghc/ghc/merge_requests/611 will make+-- things tolerable.+{-+sTrans :: forall t (a :: t) (b :: t) (c :: t)+                   (e1 :: a :~: b) (e2 :: b :~: c).+          Sing e1 -> Sing e2 -> Sing (Trans e1 e2)+sTrans se1 = unwrapSTrans $ (~>:~:) @t @a @(WhySTransSym1 a) @b @e1+                                    se1 (WrapSTrans sTransHelper)+  where+    sTransHelper :: forall (z :: t) (e' :: a :~: z).+                    Sing e' -> Sing (Trans Refl e')+    sTransHelper se' = leibniz @(a :~: z) @(TyCon1 Sing) @e' @(Trans Refl e')+                               (sym (transRight se')) se'++sHTrans :: forall j k l (a :: j) (b :: k) (c :: l)+                  (e1 :: a :~~: b) (e2 :: b :~~: c).+           Sing e1 -> Sing e2 -> Sing (HTrans e1 e2)+sHTrans se1 = unwrapSHTrans $ (~>:~~:) @j @a @(WhySHTransSym1 a) @k @b @e1+                                       se1 (WrapSHTrans sHTransHelper)+  where+    sHTransHelper :: forall m (z :: m) (e' :: a :~~: z).+                     Sing e' -> Sing (HTrans HRefl e')+    sHTransHelper se' = leibniz @(a :~~: z) @(TyCon1 Sing) @e' @(HTrans HRefl e')+                                (sym (htransRight se')) se'++rebalance :: forall j (x1 :: j) (x2 :: j) (x3 :: j) (x4 :: j)+                    (a :: x1 :~: x2) (b :: x2 :~: x3) (c :: x3 :~: x4).+             Sing a -> Sing b -> Sing c+          -> Trans a (Trans b c) :~: Trans (Trans a b) c+rebalance sa sb sc = leibniz @(x1 :~: x2) @(WhyRebalanceSym2 b c)+                             @(Symmetry (Symmetry a)) @a+                             (symIdempotent sa) rebalanceHelper+  where+    rebalanceHelper :: Trans (Symmetry (Symmetry a)) (Trans b c)+                   :~: Trans (Trans (Symmetry (Symmetry a)) b) c+    rebalanceHelper = (~>:~:) @j @x2 @(WhyRebalanceHelperSym2 b c) @x1 @(Symmetry a)+                              (sSym sa) rebalanceBC++    rebalanceBC :: Trans Refl (Trans b c) :~: Trans (Trans Refl b) c+    rebalanceBC = trans (transRight (sTrans sb sc)) transRightBC++    transRightBC :: Trans b c :~: Trans (Trans Refl b) c+    transRightBC = cong @(x2 :~: x3) @(x2 :~: x4) @(FlipSym2 TransSym0 c)+                        @b @(Trans Refl b)+                        (sym (transRight sb))++hrebalance :: forall k1 k2 k3 k4 (x1 :: k1) (x2 :: k2) (x3 :: k3) (x4 :: k4)+                     (a :: x1 :~~: x2) (b :: x2 :~~: x3) (c :: x3 :~~: x4).+              Sing a -> Sing b -> Sing c+           -> HTrans a (HTrans b c) :~: HTrans (HTrans a b) c+hrebalance sa sb sc = leibniz @(x1 :~~: x2) @(WhyHRebalanceSym2 b c)+                              @(HSymmetry (HSymmetry a)) @a+                              (hsymIdempotent sa) hrebalanceHelper+  where+    hrebalanceHelper :: HTrans (HSymmetry (HSymmetry a)) (HTrans b c)+                    :~: HTrans (HTrans (HSymmetry (HSymmetry a)) b) c+    hrebalanceHelper = (~>:~~:) @k2 @x2 @(WhyHRebalanceHelperSym2 b c)+                                @k1 @x1 @(HSymmetry a)+                                (sHSym sa) hrebalanceBC++    hrebalanceBC :: HTrans HRefl (HTrans b c) :~: HTrans (HTrans HRefl b) c+    hrebalanceBC = trans (htransRight (sHTrans sb sc)) htransRightBC++    htransRightBC :: HTrans b c :~: HTrans (HTrans HRefl b) c+    htransRightBC = cong @(x2 :~~: x3) @(x2 :~~: x4) @(FlipSym2 HTransSym0 c)+                         @b @(HTrans HRefl b)+                         (sym (htransRight sb))+-}

@@ -14,13 +14,13 @@  import           Data.Kind import           Data.Singletons.TH-import           Data.Type.Equality ((:~:)(..), (:~~:)(..))+import           Data.Type.Equality ((:~~:)(..))  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)+data (%:~:) :: forall k (a :: k) (b :: k). a :~: b -> Type where+  SRefl :: (%:~:) Refl+type instance Sing = (%:~:)  instance SingKind (a :~: b) where   type Demote (a :~: b) = a :~: b@@ -47,9 +47,9 @@          -> 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)+data (%:~~:) :: forall j k (a :: j) (b :: k). a :~~: b -> Type where+  SHRefl :: (%:~~:) HRefl+type instance Sing = (%:~~:)  instance SingKind (a :~~: b) where   type Demote (a :~~: b) = a :~~: b@@ -78,45 +78,121 @@  ----- +-- These newtype wrappers are needed to work around+-- https://gitlab.haskell.org/ghc/ghc/issues/9269+newtype WrappedTrans (x :: k) (e :: x :~: y) =+  WrapTrans { unwrapTrans :: forall (z :: k). y :~: z -> x :~: z }+newtype WrappedHTrans (x :: j) (e :: x :~~: (y :: k)) =+  WrapHTrans { unwrapHTrans :: forall l (z :: l). y :~~: z -> x :~~: z }++-- This is all needed to avoid impredicativity in the defunctionalization+-- symbols for WhyHReplace and WhyHLeibniz.+newtype WrappedPred = WrapPred { unwrapPred :: forall z. z ~> Type }+type family UnwrapPred (wp :: WrappedPred) :: forall z. z ~> Type where+  forall (uwp :: forall z. z ~> Type). UnwrapPred (WrapPred uwp) = uwp+ $(singletons [d|-  type family WhySym (a :: t) (e :: a :~: (y :: t)) :: Type where-    WhySym a (_ :: a :~: y) = y :~: a+  type WhySym (a :: t) (e :: a :~: (y :: t)) =+    y :~: a :: Type -  type family WhyHsym (a :: j) (e :: a :~~: (y :: z)) :: Type where-    WhyHsym a (_ :: a :~~: y)  = y :~~: a+  type WhySSym (a :: t) (e :: a :~: (y :: t)) =+    Sing (Symmetry e) :: Type +  type WhyHSym (a :: j) (e :: a :~~: (y :: z)) =+    y :~~: a :: Type++  type WhySHSym (a :: j) (e :: a :~~: (y :: z)) =+    Sing (HSymmetry e) :: Type+   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 WhySymIdempotent (a :: t) (r :: a :~: (z :: t)) =+    Symmetry (Symmetry r) :~: r :: Type -  type family Hsymmetry (x :: a :~~: b) :: b :~~: a where-    Hsymmetry HRefl = HRefl+  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 WhyHSymIdempotent (a :: j) (r :: a :~~: (y :: z)) =+    HSymmetry (HSymmetry r) :~: r :: Type -  type family WhyReplace (from :: t) (p :: t ~> Type)-                         (e :: from :~: (y :: t)) :: Type where-    WhyReplace from p (_ :: from :~: y) = p @@ y+  type WhyTrans (x :: k) (e :: x :~: (y :: k)) =+    WrappedTrans x e :: Type -  -- Doesn't work due to https://ghc.haskell.org/trac/ghc/ticket/11719-  {--  type family WhyHreplace (from :: j) (p :: forall z. z ~> Type)-                          (e :: from :~~: (y :: k)) :: Type where-    WhyHreplace from p (_ :: from :~~: y) = p @@ y-  -}+  type WhyHTrans (x :: j) (e :: x :~~: (y :: k)) =+    WrappedHTrans x e :: Type -  type family WhyLeibniz (f :: t ~> Type) (a :: t) (z :: t) :: Type where-    WhyLeibniz f a z = f @@ a -> f @@ z+  type family Trans (x :: a :~: b) (y :: b :~: c) :: a :~: c where+    Trans Refl Refl = Refl -  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 HTrans (x :: a :~~: b) (y :: b :~~: c) :: a :~~: c where+    HTrans HRefl HRefl = HRefl -  type family WhyEqIsRefl (a :: k) (e :: a :~: (z :: k)) :: Type where-    WhyEqIsRefl a e = e :~~: (Refl :: a :~: a)+  type WhyReplace (from :: t) (p :: t ~> Type) (e :: from :~: (y :: t)) =+    p @@ y :: Type -  type family WhyHEqIsHRefl (a :: j) (e :: a :~~: (z :: k)) :: Type where-    WhyHEqIsHRefl a e = e :~~: (HRefl :: a :~~: a)+  type WhyHReplace (from :: j) (p :: WrappedPred) (e :: from :~~: (y :: k)) =+    UnwrapPred p @@ y :: Type++  type WhyLeibniz (f :: t ~> Type) (a :: t) (z :: t) =+    f @@ a -> f @@ z :: Type++  type WhyHLeibniz (f :: WrappedPred) (a :: j) (b :: k) =+    UnwrapPred f @@ a -> UnwrapPred f @@ b :: Type++  type WhyCong (f :: x ~> y) (a :: x) (e :: a :~: (z :: x)) =+    f @@ a :~: f @@ z :: Type++  type WhyEqIsRefl (a :: k) (e :: a :~: (z :: k)) =+    e :~~: (Refl :: a :~: a) :: Type++  type WhyHEqIsHRefl (a :: j) (e :: a :~~: (z :: k)) =+    e :~~: (HRefl :: a :~~: a) :: Type++  type WhyTransLeft (a :: k) (e :: a :~: (z :: k)) =+    Trans e Refl :~: e :: Type++  type WhyTransLeftHelper (b :: k) (e :: b :~: (z :: k)) =+    Trans (Symmetry e) Refl :~: Symmetry e :: Type++  type WhyHTransLeft (a :: j) (e :: a :~~: (z :: k)) =+    HTrans e HRefl :~: e :: Type++  type WhyHTransLeftHelper (b :: k) (e :: b :~~: (z :: j)) =+    HTrans (HSymmetry e) HRefl :~: HSymmetry e :: Type++  type WhyTransRight (a :: k) (e :: a :~: (z :: k)) =+    Trans Refl e :~: e :: Type++  type WhyHTransRight (a :: j) (e :: a :~~: (z :: k)) =+    HTrans HRefl e :~: e :: Type++  type WhyRebalance (b :: x2 :~: x3) (c :: x3 :~: x4) (a :: x1 :~: x2) =+    Trans a (Trans b c) :~: Trans (Trans a b) c :: Type++  type WhyRebalanceHelper (b :: x2 :~: x3) (c :: x3 :~: x4) (a :: x2 :~: x1) =+    Trans (Symmetry a) (Trans b c) :~: Trans (Trans (Symmetry a) b) c :: Type++  type WhyHRebalance (b :: x2 :~~: x3) (c :: x3 :~~: x4) (a :: x1 :~~: x2) =+    HTrans a (HTrans b c) :~: HTrans (HTrans a b) c :: Type++  type WhyHRebalanceHelper (b :: x2 :~~: x3) (c :: x3 :~~: x4) (a :: x2 :~~: (x1 :: k1)) =+    HTrans (HSymmetry a) (HTrans b c) :~: HTrans (HTrans (HSymmetry a) b) c :: Type+  |])++-- These newtype wrappers are needed to work around+-- https://gitlab.haskell.org/ghc/ghc/issues/9269+newtype WrappedSTrans (x :: k) (e1 :: x :~: y) =+  WrapSTrans { unwrapSTrans :: forall (z :: k) (e2 :: y :~: z).+                               Sing e2 -> Sing (Trans e1 e2) }+newtype WrappedSHTrans (x :: j) (e1 :: x :~~: (y :: k)) =+  WrapSHTrans { unwrapSHTrans :: forall l (z :: l) (e2 :: y :~~: z).+                                 Sing e2 -> Sing (HTrans e1 e2) }++$(singletons [d|+  type WhySTrans (x :: k) (e :: x :~: (y :: k)) =+    WrappedSTrans x e :: Type++  type WhySHTrans (x :: j) (e :: x :~~: (y :: k)) =+    WrappedSHTrans x e :: Type   |])

@@ -27,9 +27,9 @@ data So :: Bool -> Type where   Oh :: So True -data instance Sing :: forall (what :: Bool). So what -> Type where-  SOh :: Sing Oh-type SSo = (Sing :: So what -> Type)+data SSo :: forall (what :: Bool). So what -> Type where+  SOh :: SSo Oh+type instance Sing = SSo  elimSo :: forall (p :: forall (long_sucker :: Bool). So long_sucker ~> Type)                  (what :: Bool) (s :: So what).@@ -48,10 +48,10 @@   MkFlarble1 :: a -> Flarble a b   MkFlarble2 :: a ~ Bool => Flarble a (Maybe b) -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)+data SFlarble :: forall a b. Flarble a b -> Type where+  SMkFlarble1 :: Sing x -> SFlarble (MkFlarble1 x)+  SMkFlarble2 :: SFlarble MkFlarble2+type instance Sing = SFlarble  elimFlarble :: forall (p :: forall x y. Flarble x y ~> Type)                       a b (f :: Flarble a b).@@ -81,9 +81,9 @@ data Obj :: Type where   MkObj :: o -> Obj -data instance Sing :: Obj -> Type where-  SMkObj :: forall obiwan (obj :: obiwan). Sing obj -> Sing (MkObj obj)-type SObj = (Sing :: Obj -> Type)+data SObj :: Obj -> Type where+  SMkObj :: forall obiwan (obj :: obiwan). Sing obj -> SObj (MkObj obj)+type instance Sing = SObj  elimObj :: forall (p :: Obj ~> Type) (o :: Obj).            Sing o

@@ -27,10 +27,10 @@ deriving instance Ord a  => Ord (Vec a n) deriving instance Show a => Show (Vec a n) -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)+data SVec :: forall a (n :: Nat). Vec a n -> Type 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@@ -70,17 +70,18 @@   pS x xs (elimPropVec @a @p @k xs pZ pS)  $(singletons [d|-  type WhyMapVec a b (n :: Nat) = Vec a n -> Vec b n+  type WhyMapVec a b (n :: Nat) =+    Vec a n -> Vec b n -  type WhyZipWithVec a b c (n :: Nat)-    = Vec a n -> Vec b n -> Vec c n+  type WhyZipWithVec a b c (n :: Nat) =+    Vec a n -> Vec b n -> Vec c n -  type WhyAppendVec e (m :: Nat) (n :: Nat)-    = Vec e n -> Vec e m -> Vec e (n + m)+  type WhyAppendVec e (m :: Nat) (n :: Nat) =+    Vec e n -> Vec e m -> Vec e (n + m) -  type WhyTransposeVec e (m :: Nat) (n :: Nat)-    = Vec (Vec e m) n -> Vec (Vec e n) m+  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)+  type WhyConcatVec e (j :: Nat) (l :: Vec (Vec e j) n) =+    Vec e (n * j) :: Type   |])