eliminators 0.6 → 0.7

raw patch · 14 files changed

+1002/−227 lines, 14 filesdep ~basedep ~singletonsdep ~template-haskellPVP ok

version bump matches the API change (PVP)

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

API changes (from Hackage documentation)

Files

• CHANGELOG.md +8/−0
• eliminators.cabal +11/−9
• src/Data/Eliminator.hs +94/−6
• src/Data/Eliminator/TH.hs +355/−73
• tests/DecideTypes.hs +88/−20
• tests/EqualitySpec.hs +19/−19
• tests/EqualityTypes.hs +220/−74
• tests/GADTSpec.hs +87/−7
• tests/Internal.hs +2/−0
• tests/ListTypes.hs +6/−4
• tests/MatchabilizeSpec.hs +34/−0
• tests/MatchabilizeTypes.hs +18/−0
• tests/VecSpec.hs +4/−4
• tests/VecTypes.hs +56/−11

@@ -1,3 +1,11 @@+## 0.7 [2020.03.25]+* Require `singletons-2.7` and GHC 8.10.+* Add experimental support for generating type-level eliminators through the+  `deriveTypeElim` and `deriveTypeElimNamed` functions.+* Add eliminators for `All`, `Any`, `Arg`, `Const`, `Down`, `Dual`, `First`,+  `Identity`, `Last`, `Max`, `Min`, `Option`, `Product`, `Sum`,+  and `WrappedMonoid`.+ ## 0.6 [2019.08.27] * Require `singletons-2.6` and GHC 8.8. 

@@ -1,5 +1,5 @@ name:                eliminators-version:             0.6+version:             0.7 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.8.1+tested-with:         GHC == 8.10.1  source-repository head   type:                git@@ -26,13 +26,13 @@   exposed-modules:     Data.Eliminator                        Data.Eliminator.TH                        Data.Eliminator.TypeNats-  build-depends:       base             >= 4.13  && < 4.14-                     , extra            >= 1.4.2 && < 1.7-                     , singletons       >= 2.6   && < 2.7+  build-depends:       base             >= 4.14  && < 4.15+                     , extra            >= 1.4.2 && < 1.8+                     , singletons       >= 2.7   && < 2.8                      , singleton-nats   >= 0.4.2 && < 0.5-                     , template-haskell >= 2.15  && < 2.16+                     , template-haskell >= 2.16  && < 2.17                      , th-abstraction   >= 0.3   && < 0.4-                     , th-desugar       >= 1.10  && < 1.11+                     , th-desugar       >= 1.11  && < 1.12   hs-source-dirs:      src   default-language:    Haskell2010   ghc-options:         -Wall -Wcompat -Wno-unticked-promoted-constructors@@ -46,14 +46,16 @@                        EqualityTypes                        GADTSpec                        Internal+                       MatchabilizeSpec+                       MatchabilizeTypes                        ListSpec                        ListTypes                        VecTypes                        VecSpec-  build-depends:       base           >= 4.13  && < 4.14+  build-depends:       base           >= 4.14  && < 4.15                      , eliminators                      , hspec          >= 2     && < 3-                     , singletons     >= 2.6   && < 2.7+                     , singletons     >= 2.7   && < 2.8                      , singleton-nats >= 0.4.2 && < 0.5   build-tool-depends:  hspec-discover:hspec-discover   hs-source-dirs:      tests

@@ -7,11 +7,13 @@ {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE Trustworthy #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-} {-| Module:      Data.Eliminator Copyright:   (C) 2017 Ryan Scott@@ -25,32 +27,89 @@ module Data.Eliminator (     -- * Eliminator functions     -- $eliminators-    elimBool+    elimAll+  , ElimAll+  , elimAny+  , ElimAny+  , elimArg+  , ElimArg+  , elimBool+  , ElimBool+  , elimConst+  , ElimConst+  , elimDown+  , ElimDown+  , elimDual+  , ElimDual   , elimEither+  , ElimEither+  , elimFirst+  , ElimFirst+  , elimIdentity+  , ElimIdentity+  , elimLast+  , ElimLast   , elimList+  , ElimList+  , elimMax+  , ElimMax   , elimMaybe+  , ElimMaybe+  , elimMin+  , ElimMin   , elimNat+  , ElimNat   , elimNonEmpty+  , ElimNonEmpty+  , elimOption+  , ElimOption   , elimOrdering+  , ElimOrdering+  , elimProduct+  , ElimProduct+  , elimSum+  , ElimSum   , elimTuple0+  , ElimTuple0   , elimTuple2+  , ElimTuple2   , elimTuple3+  , ElimTuple3   , elimTuple4+  , ElimTuple4   , elimTuple5+  , ElimTuple5   , elimTuple6+  , ElimTuple6   , elimTuple7+  , ElimTuple7   , elimVoid+  , ElimVoid+  , elimWrappedMonoid+  , ElimWrappedMonoid   ) where  import Control.Monad.Extra  import Data.Eliminator.TH+import Data.Functor.Const (Const(..))+import Data.Functor.Identity (Identity(..)) import Data.List.NonEmpty (NonEmpty(..))+import Data.Monoid hiding (First, Last) import Data.Nat-import Data.Singletons.Prelude+import Data.Ord (Down(..))+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.Void (Void) +import Language.Haskell.TH (nameBase) import Language.Haskell.TH.Desugar (tupleNameDegree_maybe)  {- $eliminators@@ -69,8 +128,37 @@   with @~>@ prepended. -} -$(concatMapM deriveElim [''Bool, ''Either, ''Maybe, ''Nat, ''NonEmpty, ''Ordering, ''Void])-$(deriveElimNamed "elimList" ''[])-$(concatMapM (\n -> let Just deg = tupleNameDegree_maybe n-                    in deriveElimNamed ("elimTuple" ++ show deg) n)+$(concatMapM (\n -> (++) <$> deriveElim n <*> deriveTypeElim n)+             [ ''All+             , ''Any+             , ''Arg+             , ''Bool+             , ''Const+             , ''Down+             , ''Dual+             , ''Either+             , ''First+             , ''Identity+             , ''Last+             , ''Max+             , ''Maybe+             , ''Min+             , ''Nat+             , ''NonEmpty+             , ''Option+             , ''Ordering+             , ''Product+             , ''Sum+             , ''Void+             , ''WrappedMonoid+             ])+$(deriveElimNamed     "elimList" ''[])+$(deriveTypeElimNamed "ElimList" ''[])+$(concatMapM (\n -> do deg <- fromMaybeM (fail $ "Internal error: "+                                              ++ nameBase n+                                              ++ " is not the name of a tuple")+                                         (pure $ tupleNameDegree_maybe n)+                       terms <- deriveElimNamed     ("elimTuple" ++ show deg) n+                       types <- deriveTypeElimNamed ("ElimTuple" ++ show deg) n+                       pure $ terms ++ types)              [''(), ''(,), ''(,,), ''(,,,), ''(,,,,), ''(,,,,,), ''(,,,,,,)])

@@ -1,4 +1,7 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE KindSignatures #-} {-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeApplications #-} {-# LANGUAGE Unsafe #-} {-| Module:      Data.Eliminator.TH@@ -12,25 +15,32 @@ -} module Data.Eliminator.TH (     -- * Eliminator generation-    -- $conventions+    -- ** Term-level eliminators+    -- $term-conventions     deriveElim   , deriveElimNamed+    -- ** Type-level eliminators+    -- $type-conventions+  , deriveTypeElim+  , deriveTypeElimNamed   ) where  import           Control.Applicative import           Control.Monad -import           Data.Char (isUpper)+import           Data.Char (isLetter, isUpper, toUpper) import           Data.Foldable 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.Desugar hiding (NewOrData(..)) -{- $conventions+{- $term-conventions 'deriveElim' and 'deriveElimNamed' provide a way to automate the creation of eliminator functions, which are mostly boilerplate. Here is a complete example showing how one might use 'deriveElim':@@ -134,7 +144,6 @@  -- | @'deriveElim' dataName@ generates a top-level elimination function for the -- datatype @dataName@. The eliminator will follow these naming conventions:--- The naming conventions are: -- -- * If the datatype has an alphanumeric name, its eliminator will have that name --   with @elim@ prepended.@@ -147,7 +156,123 @@ -- | @'deriveElimNamed' funName dataName@ generates a top-level elimination -- function named @funName@ for the datatype @dataName@. deriveElimNamed :: String -> Name -> Q [Dec]-deriveElimNamed funName dataName = do+deriveElimNamed = deriveElimNamed' (Proxy @IsTerm)++{- $type-conventions+'deriveTypeElim' and 'deriveTypeElimNamed' are like 'deriveElim' and+'deriveElimNamed' except that they create /type/-level eliminators instead of+term-level ones. Here is an example showing how one might use+'deriveTypeElim':++@+data MyList a = MyNil | MyCons a (MyList a)+$('deriveTypeElim' ''MyList)+@++This will produce an eliminator function that looks roughly like the following:++@+type ElimMyList :: forall (a :: 'Type').+                   forall (p :: MyList a '~>' 'Type') (l :: MyList a)+                -> 'Apply' p MyNil+                -> (forall (x :: a) (xs :: MyList a)+                     -> 'Apply' p xs '~>' 'Apply' p (MyCons x xs))+                -> 'Apply' p l+type family ElimMyList p l pMyNil pMyCons where+  forall (a :: 'Type')+         (p :: MyList a ~> 'Type')+         (pMyNil :: 'Apply' p MyNil)+         (pMyCons :: forall (x :: a) (xs :: MyList a)+                      -> 'Apply' p xs '~>' 'Apply' p (MyCons x xs)).+    ElimMyList @a p MyNil pMyNil pMyCons =+      pMyNil+  forall (a :: 'Type')+         (p :: MyList a ~> 'Type')+         (_pMyNil :: 'Apply' p MyNil)+         (pMyCons :: forall (x :: a) (xs :: MyList a)+                      -> 'Apply' p xs '~>' 'Apply' p (MyCons x xs))+         x' xs'.+    ElimMyList @a p (MyCons x' xs') pMyNil pMyCons =+      'Apply' (pMyCons x' xs') (ElimMyList @a p xs' pMyNil pMyCons)+@++Note the following differences from a term-level eliminator that 'deriveElim'+would generate:++* Type-level eliminators do not use 'Sing'. Instead, they use visible dependent+  quantification. That is, instead of generating+  @forall (x :: a). Sing x -> ...@ (as a term-level eliminator would do), a+  type-level eliminator would use @forall (x :: a) -> ...@.++* Term-level eliminators quantify @p@ with an invisible @forall@, whereas+  type-level eliminators quantify @p@ with a visible @forall@. (Really, @p@+  ought to be quantified visibly in both forms of eliminator, but GHC does not+  yet support visible dependent quantification at the term level.)++* Type-level eliminators use ('~>') in certain places where (@->@) would appear+  in term-level eliminators. For instance, note the use of+  @'Apply' p xs '~>' 'Apply' p (MyCons x xs)@ in @ElimMyList@ above. This is+  done to make it easier to use type-level eliminators with defunctionalization+  symbols (which aren't necessary for term-level eliminators).++  This comes with a notable drawback: type-level eliminators cannot support+  data constructors where recursive occurrences of the data type appear in a+  position other than the last field of a constructor. In other words,+  'deriveTypeElim' works on the @MyList@ example above, but not this variant:++  @+  data SnocList a = SnocNil | SnocCons (SnocList a) a+  @++  This is because @$('deriveTypeElim' ''SnocList)@ would generate an eliminator+  with the following kind:++  @+  type ElimSnocList :: forall (a :: 'Type').+                       forall (p :: SnocList a '~>' 'Type') (l :: SnocList a)+                    -> 'Apply' p SnocNil+                    -> (forall (xs :: SnocList a) -> 'Apply' p xs+                          '~>' (forall (x :: a) -> 'Apply' p (SnocCons x xs)))+                    -> 'Apply' p l+  @++  Unfortunately, the kind+  @'Apply' p xs '~>' (forall (x :: a) -> 'Apply' p (SnocCons x xs))@ is+  impredicative.++* In addition to the language extensions that 'deriveElim' requires, you'll need+  to enable these extensions in order to use 'deriveTypeElim':++    * @StandaloneKindSignatures@++    * @UndecidableInstances@+-}++-- | @'deriveTypeElim' dataName@ generates a type-level eliminator for the+-- datatype @dataName@. The eliminator will follow these naming conventions:+--+-- * If the datatype has an alphanumeric name, its eliminator will have that name+--   with @Elim@ prepended.+--+-- * If the datatype has a symbolic name, its eliminator will have that name+--   with @~>@ prepended.+deriveTypeElim :: Name -> Q [Dec]+deriveTypeElim dataName = deriveTypeElimNamed (upcase (eliminatorName dataName)) dataName++-- | @'deriveTypeElimNamed' funName dataName@ generates a type-level eliminator+-- named @funName@ for the datatype @dataName@.+deriveTypeElimNamed :: String -> Name -> Q [Dec]+deriveTypeElimNamed = deriveElimNamed' (Proxy @IsType)++-- The workhorse for deriveElim(Named). This generates either a term- or+-- type-level eliminator, depending on which Eliminator instance is used.+deriveElimNamed' ::+     Eliminator t+  => proxy t+  -> String  -- The name of the eliminator function+  -> Name    -- The name of the data type+  -> Q [Dec] -- The eliminator's type signature and body+deriveElimNamed' prox funName dataName = do   info@(DatatypeInfo { datatypeVars    = dataVarBndrs                      , datatypeVariant = variant                      , datatypeCons    = cons@@ -161,32 +286,29 @@     Newtype         -> pure ()   predVar <- newName "p"   singVar <- newName "s"-  let elimN = mkName funName+  let elimName = mkName funName       promDataKind = datatypeType info       predVarBndr = KindedTV predVar (InfixT promDataKind ''(~>) (ConT ''Kind.Type))       singVarBndr = KindedTV singVar promDataKind-  caseTypes <- traverse (caseType dataName predVar) cons+  caseTypes <- traverse (caseType prox dataName predVar) cons   let returnType  = predType predVar (VarT singVar)-      bndrsPrefix = dataVarBndrs ++ [predVarBndr]-      allBndrs    = bndrsPrefix ++ [singVarBndr]-      elimType = ForallT allBndrs []-                   (ravel (singType singVar:caseTypes) returnType)-      qelimDef-        | null cons-        = do singVal <- newName "singVal"-             pure $ FunD elimN [Clause [VarP singVal] (NormalB (CaseE (VarE singVal) [])) []]--        | otherwise-        = do caseClauses-               <- itraverse (\i -> caseClause dataName elimN-                                              (map tyVarBndrName bndrsPrefix)-                                              i (length cons)) cons-             pure $ FunD elimN caseClauses-  elimDef <- qelimDef-  pure [SigD elimN elimType, elimDef]+      elimType    = elimTypeSig prox dataVarBndrs predVarBndr singVarBndr+                                caseTypes returnType+  elimEqns <- qElimEqns prox (mkName funName) dataName+                        dataVarBndrs predVarBndr singVarBndr+                        caseTypes cons+  pure [elimSigD prox elimName elimType, elimEqns] -caseType :: Name -> Name -> ConstructorInfo -> Q Type-caseType dataName predVar+-- Generate the type for a "case alternative" in an eliminator function's type+-- signature, which is done on a constructor-by-constructor basis.+caseType ::+     Eliminator t+  => proxy t+  -> Name            -- The name of the data type+  -> Name            -- The predicate type variable+  -> ConstructorInfo -- The data constructor+  -> Q Type          -- The full case type+caseType prox dataName predVar          (ConstructorInfo { constructorName    = conName                           , constructorVars    = conVars                           , constructorContext = conContext@@ -199,19 +321,22 @@        vars <- newNameList "f" $ length fieldTypes        let returnType = predType predVar                                  (foldl' AppT (ConT conName) (map VarT vars))-           mbInductiveType var varType =-             let inductiveArg = predType predVar (VarT var)-             in mbInductiveCase dataName varType inductiveArg        pure $ foldr' (\(var, varType) t ->-                        ForallT [KindedTV var varType]-                                []-                                (ravel (singType var:maybeToList (mbInductiveType var varType)) t))+                        prependElimCaseTypeVar prox dataName predVar var varType t)                      returnType                      (zip vars fieldTypes) -caseClause :: Name -> Name -> [Name] -> Int -> Int-           -> ConstructorInfo -> Q Clause-caseClause dataName elimN bndrNamesPrefix conIndex numCons+-- Generate a single clause for a term-level eliminator.+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+  -> Int             -- The index of this constructor (0-indexed)+  -> Int             -- The total number of data constructors+  -> ConstructorInfo -- The data constructor+  -> Q Clause        -- The generated function clause+caseClause elimName dataName dataVarBndrs predVarBndr conIndex numCons     (ConstructorInfo { constructorName   = conName                      , constructorFields = fieldTypes })   = do let numFields = length fieldTypes@@ -222,26 +347,170 @@                         if i == conIndex                         then pure usedCaseVar                         else newName ("_p" ++ show i)-       let singConName = singDataConName conName+       let singConName = singledDataConName defaultOptions conName            mkSingVarPat var varSig = SigP (VarP var) (singType varSig)            singVarPats = zipWith mkSingVarPat singVars singVarSigs             mbInductiveArg singVar singVarSig varType =-             let prefix = foldAppType (VarE elimN)-                             $ map VarT bndrNamesPrefix-                            ++ [VarT singVarSig]-                 inductiveArg = foldExp prefix+             let prefix = foldAppTypeE (VarE elimName)+                             $ map (VarT . tvName) dataVarBndrs+                            ++ [VarT (tvName predVarBndr), VarT singVarSig]+                 inductiveArg = foldAppE prefix                                   $ VarE singVar:map VarE caseVars              in mbInductiveCase dataName varType inductiveArg            mkArg f (singVar, singVarSig, varType) =-             foldExp f $ VarE singVar-                       : maybeToList (mbInductiveArg singVar singVarSig varType)+             foldAppE f $ VarE singVar+                        : maybeToList (mbInductiveArg singVar singVarSig varType)            rhs = foldl' mkArg (VarE usedCaseVar) $                         zip3 singVars singVarSigs fieldTypes        pure $ Clause (ConP singConName singVarPats : map VarP caseVars)                      (NormalB rhs)                      [] +-- Generate a single equation for a type-level eliminator.+--+-- This code is fairly similar in structure to caseClause, but different+-- enough in subtle ways that I did not attempt to de-duplicate this code as+-- a method of the Eliminator class.+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+  -> Int             -- The index of this constructor (0-indexed)+  -> [Type]          -- The types of each "case alternative" in the eliminator+                     -- function's type signature+  -> ConstructorInfo -- The data constructor+  -> Q TySynEqn      -- The generated type family equation+caseTySynEqn elimName dataName dataVarBndrs predVarBndr conIndex caseTypes+    (ConstructorInfo { constructorName   = conName+                     , constructorFields = fieldTypes })+  = do let dataVarNames = map tvName dataVarBndrs+           predVarName  = tvName predVarBndr+           numFields    = length fieldTypes+       singVars     <- newNameList "s" numFields+       usedCaseVar  <- newName "useThis"+       caseVarBndrs <- flip itraverse caseTypes $ \i caseTy ->+                         let mkVarName+                               | i == conIndex = pure usedCaseVar+                               | otherwise     = newName ("_p" ++ show i)+                         in liftA2 KindedTV mkVarName (pure caseTy)+       let caseVarNames = map tvName caseVarBndrs+           prefix       = foldAppKindT (ConT elimName) $ map VarT dataVarNames+           mbInductiveArg singVar varType =+             let inductiveArg = foldAppT prefix $ VarT predVarName+                                                : VarT singVar+                                                : map VarT caseVarNames+             in mbInductiveCase dataName varType inductiveArg+           mkArg f (singVar, varType) =+             foldAppDefunT (f `AppT` VarT singVar)+                         $ maybeToList (mbInductiveArg singVar varType)+           bndrs = dataVarBndrs ++ predVarBndr : caseVarBndrs ++ map PlainTV singVars+           lhs   = foldAppT prefix $ VarT predVarName+                                   : foldAppT (ConT conName) (map VarT singVars)+                                   : map VarT caseVarNames+           rhs   = foldl' mkArg (VarT usedCaseVar) $ zip singVars fieldTypes+       pure $ TySynEqn (Just bndrs) lhs rhs++-- Are we dealing with a term or a type?+data TermOrType+  = IsTerm+  | IsType++-- A class that abstracts out certain common operations that one must perform+-- for both term- and type-level eliminators.+class Eliminator (t :: TermOrType) where+  -- Create the Dec for an eliminator function's type signature.+  elimSigD ::+       proxy t+    -> Name -- The name of the eliminator function+    -> Type -- The type of the eliminator function+    -> Dec  -- The type signature Dec (SigD or KiSigD)++  -- 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++  -- Take a data constructor's field type and prepend it to a "case+  -- alternative" in an eliminator function's type signature.+  prependElimCaseTypeVar ::+       proxy t+    -> Name -- The name of the data type+    -> Name -- The predicate type variable+    -> Name -- A fresh type variable name+    -> Kind -- The field type+    -> Type -- The rest of the "case alternative" type+    -> Type -- The "case alternative" type after prepending++  -- Generate the clauses/equations for the body of the eliminator function.+  qElimEqns ::+       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+    -> [Type]            -- The types of each "case alternative" in the eliminator+                         -- function's type signature+    -> [ConstructorInfo] -- The data constructors+    -> Q Dec             -- The Dec containing the clauses/equations++instance Eliminator IsTerm where+  elimSigD _ = SigD++  elimTypeSig _ dataVarBndrs predVarBndr singVarBndr caseTypes returnType =+    ForallT (dataVarBndrs ++ [predVarBndr, singVarBndr]) [] $+    ravel (singType (tvName singVarBndr):caseTypes) returnType++  prependElimCaseTypeVar _ dataName predVar var varType t =+    ForallT [KindedTV var varType] [] $+    ravel (singType var:maybeToList (mbInductiveType dataName predVar var varType)) t++  qElimEqns _ elimName dataName dataVarBndrs predVarBndr _singVarBndr _caseTypes cons+    | null cons+    = do singVal <- newName "singVal"+         pure $ FunD elimName [Clause [VarP singVal]+                               (NormalB (CaseE (VarE singVal) [])) []]+    | otherwise+    = do caseClauses+           <- itraverse (\i -> caseClause elimName dataName+                               dataVarBndrs predVarBndr i (length cons)) cons+         pure $ FunD elimName caseClauses++instance Eliminator IsType where+  elimSigD _ = KiSigD++  elimTypeSig _ dataVarBndrs predVarBndr singVarBndr caseTypes returnType =+    ForallT dataVarBndrs [] $+    ForallVisT [predVarBndr, singVarBndr] $+    ravel caseTypes returnType++  prependElimCaseTypeVar _ dataName predVar var varType t =+    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")+    let predVar   = tvName predVarBndr+        singVar   = tvName singVarBndr+        tyFamHead = TypeFamilyHead elimName+                      (PlainTV predVar:PlainTV singVar:caseVarBndrs)+                      NoSig Nothing+    caseEqns <- itraverse (\i -> caseTySynEqn elimName dataName+                                 dataVarBndrs predVarBndr i caseTypes) cons+    pure $ ClosedTypeFamilyD tyFamHead caseEqns++mbInductiveType :: Name -> Name -> Name -> Kind -> Maybe Type+mbInductiveType dataName predVar var varType =+  mbInductiveCase dataName varType $ predType predVar $ VarT var+ -- TODO: Rule out polymorphic recursion mbInductiveCase :: Name -> Type -> a -> Maybe a mbInductiveCase dataName varType inductiveArg@@ -271,6 +540,7 @@ newNameList :: String -> Int -> Q [Name] newNameList prefix n = ireplicateA n $ newName . (prefix ++) . show +-- Compute an eliminator function's name from the data type name. eliminatorName :: Name -> String eliminatorName n   | first:_ <- nStr@@ -282,23 +552,41 @@   where     nStr = nameBase n --- Reconstruct and arrow type from the list of types+-- Construct a function type, separating the arguments with -> ravel :: [Type] -> Type -> Type-ravel []    res = res-ravel (h:t) res = AppT (AppT ArrowT h) (ravel t res)+ravel args res = go args+  where+    go []    = res+    go (h:t) = AppT (AppT ArrowT h) (go t) --- apply an expression to a list of expressions-foldExp :: Exp -> [Exp] -> Exp-foldExp = foldl' AppE+-- Construct a function type, separating the arguments with ~>+ravelDefun :: [Type] -> Type -> Type+ravelDefun args res = go args+  where+    go []    = res+    go (h:t) = AppT (AppT (ConT ''(~>)) h) (go t) --- apply an expression to a list of types-foldAppType :: Exp -> [Type] -> Exp-foldAppType = foldl' AppTypeE+-- Apply an expression to a list of expressions using ordinary function applications.+foldAppE :: Exp -> [Exp] -> Exp+foldAppE = foldl' AppE -tyVarBndrName :: TyVarBndr -> Name-tyVarBndrName (PlainTV  n)   = n-tyVarBndrName (KindedTV n _) = n+-- Apply an expression to a list of types using visible type applications.+foldAppTypeE :: Exp -> [Type] -> Exp+foldAppTypeE = foldl' AppTypeE +-- Apply a type to a list of types using ordinary function applications.+foldAppT :: Type -> [Type] -> Type+foldAppT = foldl' AppT++-- Apply a type to a list of types using defunctionalized applications+-- (i.e., using Apply from singletons).+foldAppDefunT :: Type -> [Type] -> Type+foldAppDefunT = foldl' (\x y -> ConT ''Apply `AppT` x `AppT` y)++-- Apply a type to a list of types using visible kind applications.+foldAppKindT :: Type -> [Type] -> Type+foldAppKindT = foldl' AppKindT+ itraverse :: Applicative f => (Int -> a -> f b) -> [a] -> f [b] itraverse f xs0 = go xs0 0 where   go [] _ = pure []@@ -316,24 +604,18 @@ -- Taken directly from singletons ----- -singDataConName :: Name -> Name-singDataConName nm-  | nm == '[]                                      = 'SNil-  | nm == '(:)                                     = 'SCons-  | Just degree <- tupleNameDegree_maybe nm        = mkTupleDataName degree-  | Just degree <- unboxedTupleNameDegree_maybe nm = mkTupleDataName degree-  | otherwise                                      = prefixConName "S" "%" nm+-- Make an identifier uppercase. If the identifier is infix, this acts as the+-- identity function.+upcase :: String -> String+upcase str+  | isHsLetter first+  = toUpper first : tail str -mkTupleDataName :: Int -> Name-mkTupleDataName n = mkName $ "STuple" ++ (show n)+  | otherwise+  = str+  where+    first = head str --- Put an uppercase prefix on a constructor name. Takes two prefixes:--- one for identifiers and one for symbols.------ This is different from 'prefixName' in that infix constructor names always--- start with a colon, so we must insert the prefix after the colon in order--- for the new name to be syntactically valid.-prefixConName :: String -> String -> Name -> Name-prefixConName pre tyPre n = case (nameBase n) of-    (':' : rest) -> mkName (':' : tyPre ++ rest)-    alpha -> mkName (pre ++ alpha)+-- is it a letter or underscore?+isHsLetter :: Char -> Bool+isHsLetter c = isLetter c || c == '_'

@@ -5,6 +5,7 @@ {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-}@@ -12,13 +13,16 @@ {-# LANGUAGE UndecidableInstances #-} module DecideTypes where +import Data.Eliminator import Data.Kind import Data.Nat+import Data.Singletons.Prelude import Data.Singletons.TH hiding (Decision(..))  -- Due to https://github.com/goldfirere/singletons/issues/82, promoting the -- Decision data type from Data.Singletons.Decide is a tad awkward. To work -- around these, we define a more general Decision' data type here.+type Decision' :: (Type ~> Type ~> Type) -> Type -> Type data Decision' p a   = Proved a   | Disproved (p @@ a @@ Void)@@ -31,16 +35,36 @@ elimDecision (SProved yes)   pProved _          = pProved yes elimDecision (SDisproved no) _       pDisproved = pDisproved no +type ElimDecision :: forall a.+                     forall (p :: PDecision a ~> Type)+                            (d :: PDecision a) ->+                     (forall (yes :: a) -> p @@ Proved yes)+                  -> (forall (no :: a ~> Void) -> p @@ Disproved no)+                  -> p @@ d+type family ElimDecision p d pProved pDisproved where+  forall a (p :: PDecision a ~> Type)+         (pProved    :: forall (yes :: a) -> p @@ Proved yes)+         (pDisproved :: forall (no :: a ~> Void) -> p @@ Disproved no) yes.+    ElimDecision p (Proved yes) pProved pDisproved = pProved yes+  forall a (p :: PDecision a ~> Type)+         (pProved    :: forall (yes :: a) -> p @@ Proved yes)+         (pDisproved :: forall (no :: a ~> Void) -> p @@ Disproved no) no.+    ElimDecision p (Disproved no) pProved pDisproved = pDisproved no+ instance Show a => Show (Decision' p a) where   showsPrec p (Proved a) =     showParen (p > 10) $ showString "Proved " . showsPrec 11 a   showsPrec p (Disproved _) =     showParen (p > 10) $ showString "Disproved <void>" +type Decision :: Type -> Type type Decision  = Decision' (TyCon (->))++type PDecision :: Type -> Type type PDecision = Decision' (~>@#@$) -data SDecision :: forall a. PDecision a -> Type where+type SDecision :: PDecision a -> Type+data SDecision d 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@@ -56,36 +80,80 @@  -- These newtype wrappers are needed to work around -- https://gitlab.haskell.org/ghc/ghc/issues/9269-newtype WhyDecEqNat (k :: Nat) = WhyDecEqNat+type WhyDecEqNat :: Nat -> Type+newtype WhyDecEqNat k = WhyDecEqNat   { runWhyDecEqNat :: forall (j :: Nat). Sing j -> Decision (k :~: j) }++type WhyDecEqList :: [e] -> Type 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      = ()-    NatEqConsequences Z      (S _)  = Void-    NatEqConsequences (S _)  Z      = Void-    NatEqConsequences (S k1) (S k2) = k1 :~: k2+  type ConstVoidNat :: forall (m :: Nat) -> Const Type m -> Const Type (S m)+  type ConstVoidNat m r = Void -  type WhyNatEqConsequencesSame (a :: Nat) = NatEqConsequences a a+  type EqSameNat :: Nat -> forall (m :: Nat) -> Const Type m -> Const Type (S m)+  type EqSameNat n m r = n :~: m -  type WhyDecEqZ (k :: Nat) = Decision (Z :~: k)+  type ConstVoidList :: forall e. forall (y :: e) (ys :: [e])+                     -> Const Type ys -> Const Type (y:ys)+  type ConstVoidList y ys r = Void -  type WhyDecEqS (n :: Nat) (k :: Nat) = Decision (S n :~: k)+  type EqSameList :: forall e. e -> [e] -> forall (y :: e) (ys :: [e])+                  -> Const Type ys -> Const Type (y:ys)+  type EqSameList x xs y ys r = (x :~: y, xs :~: ys)+  |]) -  type family ListEqConsequences (xxs :: [e]) (yys :: [e]) :: Type where-    ListEqConsequences '[]    '[]    = ()-    ListEqConsequences '[]    (_:_)  = Void-    ListEqConsequences (_:_)  '[]    = Void-    ListEqConsequences (x:xs) (y:ys) = (x :~: y, xs :~: ys)+$(singletons [d|+  type NatEqConsequencesBase :: Nat -> Type+  type NatEqConsequencesBase m = ElimNat (ConstSym1 Type) m () ConstVoidNatSym1 -  type WhyListEqConsequencesSame (es :: [e]) = ListEqConsequences es es+  type NatEqConsequencesStep :: forall (m :: Nat) -> Const (Nat ~> Type) m+                             -> Nat -> Const Type (S m)+  type NatEqConsequencesStep m r n = ElimNat (ConstSym1 Type) n Void (EqSameNatSym2 m) -  type WhyDecEqNil (es :: [e]) = Decision ('[] :~: es)+  type ListEqConsequencesBase :: [e] -> Type+  type ListEqConsequencesBase ys = ElimList (ConstSym1 Type) ys () ConstVoidListSym2 -  type WhyDecEqCons (x :: e) (xs :: [e]) (es :: [e]) = Decision ((x:xs) :~: es)+  type ListEqConsequencesStep :: forall e. forall (x :: e) (xs :: [e])+                              -> Const ([e] ~> Type) xs -> [e] -> Const Type (x:xs)+  type ListEqConsequencesStep x xs r ys = ElimList (ConstSym1 Type) ys Void (EqSameListSym4 x xs)+  |]) -  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)+$(singletons [d|+  type NatEqConsequences :: Nat -> Nat -> Type+  type NatEqConsequences n m =+    ElimNat (ConstSym1 (Nat ~> Type)) n+            NatEqConsequencesBaseSym0+            NatEqConsequencesStepSym1 @@ m++  type WhyNatEqConsequencesSame :: Nat -> Type+  type WhyNatEqConsequencesSame a = NatEqConsequences a a++  type WhyDecEqZ :: Nat -> Type+  type WhyDecEqZ k = Decision (Z :~: k)++  type WhyDecEqS :: Nat -> Nat -> Type+  type WhyDecEqS n k = Decision (S n :~: k)++  type ListEqConsequences :: [e] -> [e] -> Type+  type ListEqConsequences (xs :: [e]) (ys :: [e]) =+    ElimList (ConstSym1 ([e] ~> Type)) xs+             ListEqConsequencesBaseSym0+             ListEqConsequencesStepSym2 @@ ys++  type WhyListEqConsequencesSame :: [e] -> Type+  type WhyListEqConsequencesSame es = ListEqConsequences es es++  type WhyDecEqNil :: [e] -> Type+  type WhyDecEqNil es = Decision ('[] :~: es)++  type WhyDecEqCons :: e -> [e] -> [e] -> Type+  type WhyDecEqCons x xs es = Decision ((x:xs) :~: es)++  type WhyIntermixListEqs1 :: e -> [e] -> [e] -> e -> Type+  type WhyIntermixListEqs1 x xs ys k = (x:xs) :~: (k:ys)++  type WhyIntermixListEqs2 :: e -> [e] -> [e] -> Type+  type WhyIntermixListEqs2 x xs k = (x:xs) :~: (x:k)   |])

@@ -86,41 +86,41 @@ sym :: forall t (a :: t) (b :: t).        a :~: b -> b :~: a sym eq = withSomeSing eq $ \(singEq :: Sing r) ->-           (~>:~:) @t @a @(WhySymSym1 a) @b @r singEq Refl+           (~>:~:) @t @a @WhySymSym0 @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+sSym se = (~>:~:) @t @a @WhySSymSym0 @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 @WhyHSymSym0 @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+sHSym se = (~>:~~:) @j @a @WhySHSymSym0 @k @b @e se SHRefl  symIdempotent :: forall t (a :: t) (b :: t)                         (e :: a :~: b).                  Sing e -> Symmetry (Symmetry e) :~: e-symIdempotent se = (~>:~:) @t @a @(WhySymIdempotentSym1 a) @b @e se Refl+symIdempotent se = (~>:~:) @t @a @WhySymIdempotentSym0 @b @e se Refl  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+hsymIdempotent se = (~>:~~:) @j @a @WhyHSymIdempotentSym0 @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+                  unwrapTrans ((~>:~:) @t @a @WrappedTransSym0 @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+                   unwrapHTrans ((~>:~~:) @j @a @WrappedHTransSym0 @k @b @r                                           singEq1 (WrapHTrans id)) eq2  replace :: forall t (from :: t) (to :: t) (p :: t ~> Type).@@ -158,45 +158,45 @@      -> f @@ a :~: f @@ b cong eq =   withSomeSing eq $ \(singEq :: Sing r) ->-    (~>:~:) @x @a @(WhyCongSym2 f a) @b @r singEq Refl+    (~>:~:) @x @a @(WhyCongSym1 f) @b @r singEq Refl  eqIsRefl :: forall k (a :: k) (b :: k) (e :: a :~: b).             Sing e -> e :~~: (Refl :: a :~: a)-eqIsRefl eq = (~>:~:) @k @a @(WhyEqIsReflSym1 a) @b @e eq HRefl+eqIsRefl eq = (~>:~:) @k @a @WhyEqIsReflSym0 @b @e eq HRefl  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+heqIsHRefl heq = (~>:~~:) @j @a @WhyHEqIsHReflSym0 @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)+transLeft se = leibniz @(a :~: b) @WhyTransLeftSym0                        @(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)+    transLeftHelper = (~>:~:) @j @b @WhyTransLeftHelperSym0 @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)+htransLeft se = leibniz @(a :~~: b) @WhyHTransLeftSym0                         @(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)+    htransLeftHelper = (~>:~~:) @k @b @WhyHTransLeftHelperSym0 @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+transRight se = (~>:~:) @j @a @WhyTransRightSym0 @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+htransRight se = (~>:~~:) @j @a @WhyHTransRightSym0 @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@@ -205,7 +205,7 @@ 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+sTrans se1 = unwrapSTrans $ (~>:~:) @t @a @WhySTransSym0 @b @e1                                     se1 (WrapSTrans sTransHelper)   where     sTransHelper :: forall (z :: t) (e' :: a :~: z).@@ -216,7 +216,7 @@ 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+sHTrans se1 = unwrapSHTrans $ (~>:~~:) @j @a @WhySHTransSym0 @k @b @e1                                        se1 (WrapSHTrans sHTransHelper)   where     sHTransHelper :: forall m (z :: m) (e' :: a :~~: z).

@@ -4,6 +4,7 @@ {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-}@@ -18,7 +19,8 @@  import           Internal -data (%:~:) :: forall k (a :: k) (b :: k). a :~: b -> Type where+type (%:~:) :: a :~: b -> Type+data (%:~:) e where   SRefl :: (%:~:) Refl type instance Sing = (%:~:) @@ -39,6 +41,18 @@         -> p @@ r (~>:~:) SRefl pRefl = pRefl +type (~>:~:) :: forall k (a :: k).+                forall (p :: forall (y :: k). a :~: y ~> Type)+             -> forall (b :: k).+                forall (r :: a :~: b)+             -> p @@ Refl+             -> p @@ r+type family (~>:~:) p r pRefl where+  forall k (a :: k)+         (p :: forall (y :: k). a :~: y ~> Type)+         (pRefl :: p @@ Refl).+    (~>:~:) p Refl pRefl = pRefl+ (~>!:~:) :: forall k (a :: k)                    (p :: k ~> Prop)                    (b :: k).@@ -47,7 +61,17 @@          -> p @@ b (~>!:~:) Refl pRefl = pRefl -data (%:~~:) :: forall j k (a :: j) (b :: k). a :~~: b -> Type where+type (~>!:~:) :: forall k (a :: k).+                 forall (p :: k ~> Prop)+              -> forall (b :: k).+                 a :~: b+              -> p @@ a+              -> 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 = (%:~~:) @@ -68,6 +92,18 @@          -> p @@ r (~>:~~:) SHRefl pHRefl = pHRefl +type (~>:~~:) :: forall j (a :: j).+                 forall (p :: forall z (y :: z). a :~~: y ~> Type)+              -> forall k (b :: k).+                 forall (r :: a :~~: b)+              -> p @@ HRefl+              -> p @@ r+type family (~>:~~:) p r pHRefl where+  forall j (a :: j)+         (p :: forall z (y :: z). a :~~: y ~> Type)+         (pHRefl :: p @@ HRefl).+    (~>:~~:) p HRefl pHRefl = pHRefl+ (~>!:~~:) :: forall j (a :: j)                     (p :: forall z. z ~> Prop)                     k (b :: k).@@ -76,123 +112,233 @@           -> p @@ b (~>!:~~:) HRefl pHRefl = pHRefl +type (~>!:~~:) :: forall j (a :: j).+                  forall (p :: forall z. z ~> Prop)+               -> forall k (b :: k).+                  a :~~: b+               -> p @@ a+               -> p @@ b+type family (~>!:~~:) p r pHRefl where+  forall j (a :: j)+         (p :: forall z. z ~> Prop)+         (pHRefl :: p @@ a).+    (~>!:~~:) p (HRefl :: a :~~: a) pHRefl = pHRefl+ -----  -- 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 }+type WrappedTrans' ::+  (Type ~> Type ~> Type) -> forall k (x :: k) (y :: k). x :~: y -> Type+newtype WrappedTrans' p (e :: (x :: k) :~: y) =+  WrapTrans (forall (z :: k). p @@ (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+type WrappedHTrans' ::+  (Type ~> Type ~> Type) -> forall j (x :: j) k (y :: k). x :~~: y -> Type+newtype WrappedHTrans' p (e :: x :~~: y) =+  WrapHTrans (forall l (z :: l). p @@ (y :~~: z) @@ (x :~~: z))  $(singletons [d|-  type WhySym (a :: t) (e :: a :~: (y :: t)) =-    y :~: a :: Type+  type WrappedTrans :: forall k (x :: k) (y :: k). x :~: y -> Type+  type WrappedTrans = WrappedTrans' (TyCon2 (->)) -  type WhySSym (a :: t) (e :: a :~: (y :: t)) =-    Sing (Symmetry e) :: Type+  type PWrappedTrans :: forall k (x :: k) (y :: k). x :~: y -> Type+  type PWrappedTrans = WrappedTrans' (~>@#@$) -  type WhyHSym (a :: j) (e :: a :~~: (y :: z)) =-    y :~~: a :: Type+  type WrappedHTrans :: forall j (x :: j) k (y :: k). x :~~: y -> Type+  type WrappedHTrans = WrappedHTrans' (TyCon2 (->)) -  type WhySHSym (a :: j) (e :: a :~~: (y :: z)) =-    Sing (HSymmetry e) :: Type+  type PWrappedHTrans :: forall j (x :: j) k (y :: k). x :~~: y -> Type+  type PWrappedHTrans = WrappedHTrans' (~>@#@$)+  |]) -  type family Symmetry (x :: (a :: k) :~: (b :: k)) :: b :~: a where-    Symmetry Refl = Refl+unwrapTrans :: WrappedTrans (e :: (x :: k) :~: y)+            -> forall (z :: k). y :~: z -> x :~: z+unwrapTrans (WrapTrans f) = f -  type WhySymIdempotent (a :: t) (r :: a :~: (z :: t)) =-    Symmetry (Symmetry r) :~: r :: Type+type UnwrapTrans ::+  forall k (x :: k) (y :: k) (e :: x :~: y).+  PWrappedTrans e -> forall (z :: k). y :~: z ~> x :~: z+type family UnwrapTrans wt :: forall z. y :~: z ~> x :~: z where+  forall k (x :: k) (y :: k) (uwt :: forall (z :: k). y :~: z ~> x :~: z).+    UnwrapTrans (WrapTrans uwt) = uwt -  type family HSymmetry (x :: a :~~: b) :: b :~~: a where-    HSymmetry HRefl = HRefl+unwrapHTrans :: WrappedHTrans (e :: x :~~: y)+             -> forall l (z :: l). y :~~: z -> x :~~: z+unwrapHTrans (WrapHTrans f) = f -  type WhyHSymIdempotent (a :: j) (r :: a :~~: (y :: z)) =-    HSymmetry (HSymmetry r) :~: r :: Type+type UnwrapHTrans ::+  forall j (x :: j) k (y :: k) (e :: x :~~: y).+  PWrappedHTrans e -> forall l (z :: l). y :~~: z ~> x :~~: z+type family UnwrapHTrans wht :: forall l (z :: l). y :~~: z ~> x :~~: z where+  forall j (x :: j) k (y :: k) (uwht :: forall l (z :: l). y :~~: z ~> x :~~: z).+    UnwrapHTrans (WrapHTrans uwht) = uwht -  type WhyTrans (x :: k) (e :: x :~: (y :: k)) =-    WrappedTrans x e :: Type+-- This is all needed to avoid impredicativity in the defunctionalization+-- symbols for WhyHReplace and WhyHLeibniz.+type WrappedPred :: Type+newtype WrappedPred = WrapPred { unwrapPred :: forall z. z ~> Type } -  type WhyHTrans (x :: j) (e :: x :~~: (y :: k)) =-    WrappedHTrans x e :: Type+type UnwrapPred :: WrappedPred -> forall z. z ~> Type+type family UnwrapPred wp :: forall z. z ~> Type where+  forall (uwp :: forall z. z ~> Type). UnwrapPred (WrapPred uwp) = uwp -  type family Trans (x :: a :~: b) (y :: b :~: c) :: a :~: c where+$(singletons [d|+  type WhySym :: forall t (a :: t) (y :: t). a :~: y -> Type+  type WhySym (e :: a :~: y) = y :~: a++  type WhyHSym :: forall j (a :: j) t (y :: t). a :~~: y -> Type+  type WhyHSym (e :: a :~~: y) = y :~~: a++  type TransStep :: forall k (x :: k) (z :: k). x :~: z -> x :~: z+  type TransStep e = e++  type HTransStep :: forall j (x :: j) k (z :: k). x :~~: z -> x :~~: z+  type HTransStep e = e+  |])++$(singletons [d|+  -- These use eliminators, but th-desugar takes a while to expand them.+  -- TODO RGS: Investigate why.+  {-+  type Trans :: a :~: b -> b :~: c -> a :~: c+  type Trans x y =+    UnwrapTrans ((~>:~:) PWrappedTransSym0 x (WrapTrans TransStepSym0)) @@ y++  type HTrans :: a :~~: b -> b :~~: c -> a :~~: c+  type HTrans x y =+    UnwrapHTrans ((~>:~~:) PWrappedHTransSym0 x (WrapHTrans HTransStepSym0)) @@ y+  -}++  type Trans :: a :~: b -> b :~: c -> a :~: c+  type family Trans x y where     Trans Refl Refl = Refl -  type family HTrans (x :: a :~~: b) (y :: b :~~: c) :: a :~~: c where+  type HTrans :: a :~~: b -> b :~~: c -> a :~~: c+  type family HTrans x y where     HTrans HRefl HRefl = HRefl+  |]) -  type WhyReplace (from :: t) (p :: t ~> Type) (e :: from :~: (y :: t)) =-    p @@ y :: Type+type WhyReplace :: forall t. forall (from :: t)+                -> (t ~> Type)+                -> forall (y :: t). from :~: y+                -> Type+type WhyReplace from p (e :: from :~: y) = p @@ y+data WhyReplaceSym2 :: forall t. forall (from :: t)+                    -> (t ~> Type)+                    -> forall (y :: t). from :~: y+                    ~> Type+type instance Apply (WhyReplaceSym2 x y) z = WhyReplace x y z -  type WhyHReplace (from :: j) (p :: WrappedPred) (e :: from :~~: (y :: k)) =-    UnwrapPred p @@ y :: Type+type WhyHReplace :: forall j. forall (from :: j)+                 -> WrappedPred+                 -> forall k (y :: k). from :~~: y+                 -> Type+type WhyHReplace from p (e :: from :~~: y) = UnwrapPred p @@ y+data WhyHReplaceSym2 :: forall j. forall (from :: j)+                     -> WrappedPred+                     -> forall k (y :: k). from :~~: y ~> Type+type instance Apply (WhyHReplaceSym2 x y) z = WhyHReplace x y z +$(singletons [d|   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 WhyHLeibniz :: WrappedPred+                 -> forall j. j+                 -> forall k. k+                 -> Type+type WhyHLeibniz f a b = UnwrapPred f @@ a -> UnwrapPred f @@ b+data WhyHLeibnizSym2 :: WrappedPred+                     -> forall j. j+                     -> forall k. k+                     ~> Type+type instance Apply (WhyHLeibnizSym2 x y) z = WhyHLeibniz x y z -  type WhyHEqIsHRefl (a :: j) (e :: a :~~: (z :: k)) =-    e :~~: (HRefl :: a :~~: a) :: Type+type WhyCong :: (x ~> y) -> forall (a :: x) (z :: x). a :~: z -> Type+type WhyCong f (e :: a :~: z) = f @@ a :~: f @@ z+data WhyCongSym1 :: (x ~> y) -> forall (a :: x) (z :: x). a :~: z ~> Type+type instance Apply (WhyCongSym1 x) y = WhyCong x y -  type WhyTransLeft (a :: k) (e :: a :~: (z :: k)) =-    Trans e Refl :~: e :: Type+$(singletons [d|+  type WhyEqIsRefl :: forall k (a :: k) (z :: k). a :~: z -> Type+  type WhyEqIsRefl (e :: a :~: z) = e :~~: (Refl :: a :~: a) -  type WhyTransLeftHelper (b :: k) (e :: b :~: (z :: k)) =-    Trans (Symmetry e) Refl :~: Symmetry e :: Type+  type WhyHEqIsHRefl :: forall j (a :: j) k (z :: k). a :~~: z -> Type+  type WhyHEqIsHRefl (e :: a :~~: z) = e :~~: (HRefl :: a :~~: a) -  type WhyHTransLeft (a :: j) (e :: a :~~: (z :: k)) =-    HTrans e HRefl :~: e :: Type+  type WhyTransLeft :: forall k (a :: k) (z :: k). a :~: z -> Type+  type WhyTransLeft e = Trans e Refl :~: e -  type WhyHTransLeftHelper (b :: k) (e :: b :~~: (z :: j)) =-    HTrans (HSymmetry e) HRefl :~: HSymmetry e :: Type+  type WhyHTransLeft :: forall j (a :: j) k (z :: k). a :~~: z -> Type+  type WhyHTransLeft e = HTrans e HRefl :~: e -  type WhyTransRight (a :: k) (e :: a :~: (z :: k)) =-    Trans Refl e :~: e :: Type+  type WhyTransRight :: forall k (a :: k) (z :: k). a :~: z -> Type+  type WhyTransRight e = Trans Refl e :~: e -  type WhyHTransRight (a :: j) (e :: a :~~: (z :: k)) =-    HTrans HRefl e :~: e :: Type+  type WhyHTransRight :: forall j (a :: j) k (z :: k). a :~~: z -> Type+  type WhyHTransRight e = HTrans HRefl e :~: e -  type WhyRebalance (b :: x2 :~: x3) (c :: x3 :~: x4) (a :: x1 :~: x2) =-    Trans a (Trans b c) :~: Trans (Trans a b) c :: Type+  type WhyRebalance :: x2 :~: x3 -> x3 :~: x4 -> x1 :~: x2 -> Type+  type WhyRebalance b c a = Trans a (Trans b c) :~: Trans (Trans a b) c -  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 :: x2 :~~: x3 -> x3 :~~: x4 -> x1 :~~: x2 -> Type+  type WhyHRebalance b c a = HTrans a (HTrans b c) :~: HTrans (HTrans a b) c+  |]) -  type WhyHRebalance (b :: x2 :~~: x3) (c :: x3 :~~: x4) (a :: x1 :~~: x2) =-    HTrans a (HTrans b c) :~: HTrans (HTrans a b) c :: Type+type Symmetry :: a :~: b -> b :~: a+type Symmetry  (r :: a :~: b) = (~>:~:) WhySymSym0 r Refl -  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-  |])+type HSymmetry :: a :~~: b -> b :~~: a+type HSymmetry (r :: a :~~: b) = (~>:~~:) WhyHSymSym0 r HRefl  -- These newtype wrappers are needed to work around -- https://gitlab.haskell.org/ghc/ghc/issues/9269-newtype WrappedSTrans (x :: k) (e1 :: x :~: y) =+type WrappedSTrans :: forall k (x :: k) (y :: k). x :~: y -> Type+newtype WrappedSTrans (e1 :: (x :: k) :~: y) =   WrapSTrans { unwrapSTrans :: forall (z :: k) (e2 :: y :~: z).                                Sing e2 -> Sing (Trans e1 e2) }-newtype WrappedSHTrans (x :: j) (e1 :: x :~~: (y :: k)) =++type WrappedSHTrans :: forall j (x :: j) k (y :: k). x :~~: y -> Type+newtype WrappedSHTrans (e1 :: x :~~: y) =   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 WhySSym :: forall t (a :: t) (y :: t). a :~: y -> Type+  type WhySSym e = Sing (Symmetry e) -  type WhySHTrans (x :: j) (e :: x :~~: (y :: k)) =-    WrappedSHTrans x e :: Type+  type WhySymIdempotent :: forall t (a :: t) (z :: t). a :~: z -> Type+  type WhySymIdempotent r = Symmetry (Symmetry r) :~: r++  type WhySHSym :: forall j (a :: j) z (y :: z). a :~~: y -> Type+  type WhySHSym e = Sing (HSymmetry e)++  type WhyHSymIdempotent :: forall j (a :: j) z (y :: z). a :~~: y -> Type+  type WhyHSymIdempotent r = HSymmetry (HSymmetry r) :~: r++  type WhyTransLeftHelper :: forall k (b :: k) (z :: k). b :~: z -> Type+  type WhyTransLeftHelper e = Trans (Symmetry e) Refl :~: Symmetry e++  type WhyHTransLeftHelper :: forall k. forall (b :: k) j (z :: j). b :~~: z -> Type+  type WhyHTransLeftHelper e = HTrans (HSymmetry e) HRefl :~: HSymmetry e++  type WhySTrans :: forall k (x :: k) (y :: k). x :~: y -> Type+  type WhySTrans e = WrappedSTrans e++  type WhySHTrans :: forall j (x :: j) k (y :: k). x :~~: y -> Type+  type WhySHTrans e = WrappedSHTrans e   |])++type WhyRebalanceHelper :: x2 :~: x3 -> x3 :~: x4 -> forall x1. x2 :~: x1 -> Type+type WhyRebalanceHelper b c a =+  Trans (Symmetry a) (Trans b c) :~: Trans (Trans (Symmetry a) b) c+data WhyRebalanceHelperSym2 :: x2 :~: x3 -> x3 :~: x4 -> forall x1. x2 :~: x1 ~> Type+type instance Apply (WhyRebalanceHelperSym2 x y) z = WhyRebalanceHelper x y z++type WhyHRebalanceHelper :: x2 :~~: x3 -> x3 :~~: x4 -> forall k1 (x1 :: k1). x2 :~~: x1 -> Type+type WhyHRebalanceHelper b c a =+  HTrans (HSymmetry a) (HTrans b c) :~: HTrans (HTrans (HSymmetry a) b) c+data WhyHRebalanceHelperSym2 :: x2 :~~: x3 -> x3 :~~: x4 -> forall k1 (x1 :: k1). x2 :~~: x1 ~> Type+type instance Apply (WhyHRebalanceHelperSym2 x y) z = WhyHRebalanceHelper x y z

@@ -4,9 +4,11 @@ {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-} module GADTSpec where  import Data.Kind@@ -24,10 +26,12 @@  ----- -data So :: Bool -> Type where+type So :: Bool -> Type+data So b where   Oh :: So True -data SSo :: forall (what :: Bool). So what -> Type where+type SSo :: So what -> Type+data SSo s where   SOh :: SSo Oh type instance Sing = SSo @@ -38,17 +42,38 @@        -> p @@ s elimSo SOh pOh = pOh +type ElimSo :: forall (p :: forall (long_sucker :: Bool). So long_sucker ~> Type)+            -> forall (what :: Bool).+               forall (s :: So what)+            -> p @@ Oh+            -> p @@ s+type family ElimSo p s pOh where+  forall (p :: forall (long_sucker :: Bool). So long_sucker ~> Type)+         (pOh :: p @@ Oh).+    ElimSo p Oh pOh = pOh+ elimPropSo :: forall (p :: Bool ~> Prop) (what :: Bool).               So what            -> p @@ True            -> p @@ what elimPropSo Oh pOh = pOh -data Flarble :: Type -> Type -> Type where+type ElimPropSo :: forall (p :: Bool ~> Prop)+                -> forall (what :: Bool).+                   So what+                -> p @@ True+                -> p @@ what+type family ElimPropSo p s pOh where+  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) -data SFlarble :: forall a b. Flarble a b -> Type where+type SFlarble :: Flarble a b -> Type+data SFlarble f where   SMkFlarble1 :: Sing x -> SFlarble (MkFlarble1 x)   SMkFlarble2 :: SFlarble MkFlarble2 type instance Sing = SFlarble@@ -66,9 +91,28 @@   case s of     (_ :: Sing (MkFlarble2 :: Flarble Bool (Maybe b'))) -> pMkFlarble2 @b' +type ElimFlarble ::+     forall (p :: forall x y. Flarble x y ~> Type)+  -> forall a b.+     forall (f :: Flarble a b)+  -> (forall a' b'. forall (x :: a') -> p @@ (MkFlarble1 x :: Flarble a' b'))+  -> (forall b'. p @@ (MkFlarble2 :: Flarble Bool (Maybe b')))+  -> p @@ f+type family ElimFlarble p f pMkFlarble1 pMkFlarble2 where+  forall (p :: forall x y. Flarble x y ~> Type) a b+         (pMkFlarble1 :: forall a' b'. forall (x :: a') -> p @@ (MkFlarble1 x :: Flarble a' b'))+         (pMkFlarble2 :: forall b'. p @@ (MkFlarble2 :: Flarble Bool (Maybe b'))) x.+    ElimFlarble p (MkFlarble1 x :: Flarble a b) pMkFlarble1 pMkFlarble2 =+      pMkFlarble1 @a @b x+  forall (p :: forall x y. Flarble x y ~> Type)+         (pMkFlarble1 :: forall a' b'. forall (x :: a') -> p @@ (MkFlarble1 x :: Flarble a' b'))+         (pMkFlarble2 :: forall b'. p @@ (MkFlarble2 :: Flarble Bool (Maybe b'))) b'.+    ElimFlarble p (MkFlarble2 :: Flarble Bool (Maybe b')) pMkFlarble1 pMkFlarble2 =+      pMkFlarble2 @b'+ elimPropFlarble :: forall (p :: Type ~> Type ~> Prop) a b.                    Flarble a b-                -> (forall a' b'. a -> p @@ a' @@ b')+                -> (forall a' b'. a' -> p @@ a' @@ b')                 -> (forall b'. p @@ Bool @@ Maybe b')                 -> p @@ a @@ b elimPropFlarble f@(MkFlarble1 x) pMkFlarble1 _ =@@ -78,10 +122,31 @@   case f of     (_ :: Flarble Bool (Maybe b')) -> pMkFlarble2 @b' -data Obj :: Type where+type ElimPropFlarble ::+     forall (p :: Type ~> Type ~> Prop)+  -> forall a b.+     Flarble a b+  -> (forall a' b'. a' ~> p @@ a' @@ b')+  -> (forall b'. p @@ Bool @@ Maybe b')+  -> p @@ a @@ b+type family ElimPropFlarble p f pMkFlarble1 pMkFlarble2 where+  forall (p :: Type ~> Type ~> Prop) a b+         (pMkFlarble1 :: forall a' b'. a' ~> p @@ a' @@ b')+         (pMkFlarble2 :: forall b'. p @@ Bool @@ Maybe b') x.+    ElimPropFlarble p (MkFlarble1 x :: Flarble a b) pMkFlarble1 pMkFlarble2 =+      pMkFlarble1 @a @b @@ x+  forall (p :: Type ~> Type ~> Prop)+         (pMkFlarble1 :: forall a' b'. a' ~> p @@ a' @@ b')+         (pMkFlarble2 :: forall b'. p @@ Bool @@ Maybe b') b'.+    ElimPropFlarble p (MkFlarble2 :: Flarble Bool (Maybe b')) pMkFlarble1 pMkFlarble2 =+      pMkFlarble2 @b'++type Obj :: Type+data Obj where   MkObj :: o -> Obj -data SObj :: Obj -> Type where+type SObj :: Obj -> Type+data SObj o where   SMkObj :: forall obiwan (obj :: obiwan). Sing obj -> SObj (MkObj obj) type instance Sing = SObj @@ -91,8 +156,23 @@         -> p @@ o elimObj (SMkObj (sx :: Sing (x :: obj))) pMkObj = pMkObj @obj @x sx +type ElimObj :: forall (p :: Obj ~> Type)+                       (o :: Obj)+             -> (forall obj. forall (x :: obj) -> p @@ MkObj x)+             -> p @@ o+type family ElimObj p o pMkObj where+  forall (p :: Obj ~> Type)+         (pMkObj :: forall obj. forall (x :: obj) -> p @@ MkObj x)+         obj (x :: obj).+    ElimObj p (MkObj (x :: obj)) pMkObj = pMkObj @obj x+ elimPropObj :: forall (p :: Prop).                Obj             -> (forall obj. obj -> p)             -> p elimPropObj (MkObj o) pMkObj = pMkObj o++type ElimPropObj :: forall (p :: Prop) -> Obj -> (forall obj. obj ~> p) -> p+type family ElimPropObj p o pMkObj where+  forall (p :: Prop) (pMkObj :: forall obj. obj ~> p) o.+    ElimPropObj p (MkObj o) pMkObj = pMkObj @@ o

@@ -1,5 +1,7 @@+{-# LANGUAGE StandaloneKindSignatures #-} module Internal where  import Data.Kind +type Prop :: Type type Prop = Type

@@ -1,20 +1,22 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE PolyKinds #-}+{-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} module ListTypes where +import Data.Kind import Data.Singletons.Prelude import Data.Singletons.Prelude.List import Data.Singletons.TH  $(singletons [d|-  type WhyMapPreservesLength (f :: x ~> y) (l :: [x])-    = Length l :~: Length (Map f l)+  type WhyMapPreservesLength :: (x ~> y) -> [x] -> Type+  type WhyMapPreservesLength f l = 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+  type WhyMapFusion :: (y ~> z) -> (x ~> y) -> [x] -> Type+  type WhyMapFusion f g l = Map f (Map g l) :~: Map (f .@#@$$$ g) l   |])

@@ -0,0 +1,34 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE StandaloneKindSignatures #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+module MatchabilizeSpec where++import Data.Eliminator+import Data.Singletons+import Data.Singletons.Prelude+import Data.Type.Equality++import MatchabilizeTypes++import Test.Hspec++main :: IO ()+main = hspec spec++spec :: Spec+spec = pure ()++-----++type ElimMaybeSimple :: b -> (a ~> b) -> Maybe a -> b+type ElimMaybeSimple (n :: b) j m =+    UnMatchabilize (ElimMaybe (ConstSym1 b) m n (Matchabilize j))++test1 :: ElimMaybeSimple "a" IdSym0 Nothing :~: "a"+test1 = Refl++test2 :: ElimMaybeSimple "a" IdSym0 (Just "b") :~: "b"+test2 = Refl

@@ -0,0 +1,18 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE StandaloneKindSignatures #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# OPTIONS_GHC -Wno-unused-foralls #-}+module MatchabilizeTypes where++import Data.Singletons++type Matchabilize :: (a ~> b) -> forall (x :: a) -> b+data family Matchabilize++type UnMatchabilize :: k -> k+type family UnMatchabilize a where+  UnMatchabilize (Matchabilize f a) = f @@ a+  UnMatchabilize x                  = x

@@ -133,13 +133,13 @@              (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) @(WhyConcatVecSym2 e j) @n @l singL base step+                elimVec @(Vec e j) @WhyConcatVecSym0 @n @l singL base step   where-    base :: WhyConcatVec e j VNil+    base :: WhyConcatVec VNil     base = VNil      step :: forall (k :: Nat) (x :: Vec e j) (xs :: Vec (Vec e j) k).                    Sing x -> Sing xs-                -> WhyConcatVec e j xs-                -> WhyConcatVec e j (x :# xs)+                -> WhyConcatVec xs+                -> WhyConcatVec (x :# xs)     step h _ vKJ = appendVec (fromSing h) vKJ

@@ -6,6 +6,7 @@ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-}@@ -19,6 +20,7 @@ import Data.Singletons.TH 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)@@ -27,7 +29,8 @@ deriving instance Ord a  => Ord (Vec a n) deriving instance Show a => Show (Vec a n) -data SVec :: forall a (n :: Nat). Vec a n -> Type where+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@@ -60,6 +63,30 @@ elimVec (sx :%# (sxs :: Sing (xs :: Vec a k))) pVNil pVCons =   pVCons sx sxs (elimVec @a @p @k @xs sxs pVNil pVCons) +type ElimVec :: forall a.+                forall (p :: forall (k :: Nat). Vec a k ~> Type)+             -> forall (n :: Nat).+                forall (v :: Vec a n)+             -> p @@ VNil+             -> (forall (k :: Nat).+                 forall (x :: a) (xs :: Vec a k) ->+                 p @@ xs ~> p @@ (x :# xs))+             -> p @@ v+type family ElimVec p v pVNil pVCons where+  forall a (p :: forall (k :: Nat). Vec a k ~> Type)+         (pVNil :: p @@ VNil)+         (pVCons :: forall (k :: Nat).+                    forall (x :: a) (xs :: Vec a k) ->+                    p @@ xs ~> p @@ (x :# xs)).+    ElimVec p VNil pVNil pVCons = pVNil+  forall a (p :: forall (k :: Nat). Vec a k ~> Type)+         (pVNil :: p @@ VNil)+         (pVCons :: forall (k :: Nat).+                    forall (x :: a) (xs :: Vec a k) ->+                    p @@ xs ~> p @@ (x :# xs)) k x xs.+    ElimVec p (x :# (xs :: Vec a k)) pVNil pVCons =+      pVCons x xs @@ ElimVec @a p @k xs pVNil pVCons+ elimPropVec :: forall a (p :: Nat ~> Prop) (n :: Nat).                Vec a n             -> p @@ Z@@ -69,19 +96,37 @@ elimPropVec (x :# (xs :: Vec a k)) pZ pS =   pS x xs (elimPropVec @a @p @k xs pZ pS) +type ElimPropVec :: forall a.+                    forall (p :: Nat ~> Prop)+                 -> forall (n :: Nat).+                    Vec a n+                 -> p @@ Z+                 -> (forall (k :: Nat). a ~> Vec a k ~> p @@ k ~> p @@ S k)+                 -> p @@ n+type family ElimPropVec p v pZ pS where+  forall a (p :: Nat ~> Prop)+         (pZ :: p @@ Z)+         (pS :: forall (k :: Nat). a ~> Vec a k ~> p @@ k ~> p @@ S k).+    ElimPropVec p VNil pZ pS = pZ+  forall a (p :: Nat ~> Prop)+         (pZ :: p @@ Z)+         (pS :: forall (k :: Nat). a ~> Vec a k ~> p @@ k ~> p @@ S k) k x xs.+    ElimPropVec p (x :# (xs :: Vec a k)) pZ pS =+      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 :: Type -> Type -> Nat -> Type+  type WhyMapVec a b n = Vec a n -> Vec b n -  type WhyZipWithVec a b c (n :: Nat) =-    Vec a n -> Vec b n -> Vec c n+  type WhyZipWithVec :: Type -> Type -> Type -> Nat -> Type+  type WhyZipWithVec a b c n = 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 :: Type -> Nat -> Nat -> Type+  type WhyAppendVec e m n = 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 :: Type -> Nat -> Nat -> Type+  type WhyTransposeVec e m n = Vec (Vec e m) n -> Vec (Vec e n) m -  type WhyConcatVec e (j :: Nat) (l :: Vec (Vec e j) n) =-    Vec e (n * j) :: Type+  type WhyConcatVec :: Vec (Vec e j) n -> Type+  type WhyConcatVec (l :: Vec (Vec e j) n) = Vec e (n * j)   |])