diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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. diff --git a/eliminators.cabal b/eliminators.cabal --- a/eliminators.cabal +++ b/eliminators.cabal @@ -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 diff --git a/src/Data/Eliminator.hs b/src/Data/Eliminator.hs --- a/src/Data/Eliminator.hs +++ b/src/Data/Eliminator.hs @@ -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) 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 @@ -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 diff --git a/tests/DecideSpec.hs b/tests/DecideSpec.hs --- a/tests/DecideSpec.hs +++ b/tests/DecideSpec.hs @@ -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 diff --git a/tests/DecideTypes.hs b/tests/DecideTypes.hs --- a/tests/DecideTypes.hs +++ b/tests/DecideTypes.hs @@ -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) } diff --git a/tests/EqualitySpec.hs b/tests/EqualitySpec.hs --- a/tests/EqualitySpec.hs +++ b/tests/EqualitySpec.hs @@ -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)) +-} diff --git a/tests/EqualityTypes.hs b/tests/EqualityTypes.hs --- a/tests/EqualityTypes.hs +++ b/tests/EqualityTypes.hs @@ -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 |]) diff --git a/tests/GADTSpec.hs b/tests/GADTSpec.hs --- a/tests/GADTSpec.hs +++ b/tests/GADTSpec.hs @@ -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 diff --git a/tests/VecTypes.hs b/tests/VecTypes.hs --- a/tests/VecTypes.hs +++ b/tests/VecTypes.hs @@ -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 |])