packages feed

eliminators 0.8 → 0.9

raw patch · 12 files changed

+575/−128 lines, 12 filesdep ~basedep ~singletons-basedep ~template-haskell

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

Files

CHANGELOG.md view
@@ -1,3 +1,19 @@+## 0.9 [2021.10.31]+* Require `singletons-base-3.1` and GHC 9.2.+* Add `{e,E}limProxy` to `Data.Eliminator`.+* `Data.Eliminator` no longer exports `{e,E}limFirst` and `{e,E}limLast`+  eliminators. If you wish to use eliminators that work over `First`/`Last`+  from `Data.Monoid`, you must import them `Data.Eliminator.Monoid`. If you+  wish to use eliminators that over `First`/`Last` from `Data.Semigroup`, you+  must import them from the new `Data.Eliminator.Semigroup` module.+* `Data.Eliminator` no longer exports `{e,E}limProduct` and `{e,E}limSum`+  eliminators. If you wish to use eliminators that work over `Product`/`Sum`+  from `Data.Monoid` or `Data.Semigroup`, you must import them+  `Data.Eliminator.Monoid` or `Data.Eliminator.Semigroup`. If you wish to use+  eliminators that over `Product`/`Sum` from+  `Data.Functor.Product`/`Data.Functor.Sum`, you must import them from the new+  `Data.Eliminator.Functor` module.+ ## 0.8 [2021.03.12] * Require `singletons-base-3.0` and GHC 9.0. * Remove eliminators for `Data.Semigroup.Option`, which is deprecated as of
eliminators.cabal view
@@ -1,5 +1,5 @@ name:                eliminators-version:             0.8+version:             0.9 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 == 9.0.1+tested-with:         GHC == 9.2.1  source-repository head   type:                git@@ -24,15 +24,18 @@  library   exposed-modules:     Data.Eliminator+                       Data.Eliminator.Functor+                       Data.Eliminator.Monoid+                       Data.Eliminator.Semigroup                        Data.Eliminator.TH                        Data.Eliminator.TypeNats-  build-depends:       base             >= 4.15  && < 4.16+  build-depends:       base             >= 4.16  && < 4.17                      , extra            >= 1.4.2 && < 1.8-                     , singletons-base  >= 3.0   && < 3.1+                     , singletons-base  >= 3.1   && < 3.2                      , singleton-nats   >= 0.4.2 && < 0.5-                     , template-haskell >= 2.17  && < 2.18+                     , template-haskell >= 2.18  && < 2.19                      , th-abstraction   >= 0.4   && < 0.5-                     , th-desugar       >= 1.12  && < 1.13+                     , th-desugar       >= 1.13  && < 1.14   hs-source-dirs:      src   default-language:    Haskell2010   ghc-options:         -Wall -Wcompat -Wno-unticked-promoted-constructors@@ -50,12 +53,13 @@                        MatchabilizeTypes                        ListSpec                        ListTypes+                       PolyRecTypes                        VecTypes                        VecSpec-  build-depends:       base            >= 4.15  && < 4.16+  build-depends:       base            >= 4.16  && < 4.17                      , eliminators                      , hspec           >= 2     && < 3-                     , singletons-base >= 3.0   && < 3.1+                     , singletons-base >= 3.1   && < 3.2                      , singleton-nats  >= 0.4.2 && < 0.5   build-tool-depends:  hspec-discover:hspec-discover   hs-source-dirs:      tests
src/Data/Eliminator.hs view
@@ -23,6 +23,29 @@ Portability: GHC  Dependently typed elimination functions using @singletons@.++This module exports a combination of eliminators whose names are known not to+clash with each other. Potential name conflicts have been resolved by putting+the conflicting names in separate modules:++* "Data.Eliminator" defines 'elimNat', which works over the 'Nat' data type+  from "Data.Nat". For an eliminator that works over 'Nat' from "GHC.TypeNats",+  see "Data.Eliminator.TypeNats".++* "Data.Eliminator" avoids exporting eliminators for @First@ and @Last@ data+  types, as there are multiple data types with these names. If you want+  eliminators for the 'First' and 'Last' data types from "Data.Monoid", import+  them from "Data.Eliminator.Monoid". If you want eliminators for the 'First'+  and 'Last' data types from "Data.Semigroup", import them from+  "Data.Eliminator.Semigroup".++* "Data.Eliminator" avoids exporting eliminators for @Product@ and @Sum@ data+  types, as there are multiple data types with these names. If you want+  eliminators for the 'Product' and 'Sum' data types from "Data.Monoid" or+  "Data.Semigroup", import them from "Data.Eliminator.Monoid" or+  "Data.Eliminator.Semigroup". If you want eliminators for the 'Product' and+  'Sum' data types from "Data.Functor.Product" and "Data.Functor.Sum",+  respectively, import them from "Data.Eliminator.Functor". -} module Data.Eliminator (     -- * Eliminator functions@@ -43,12 +66,8 @@   , ElimDual   , elimEither   , ElimEither-  , elimFirst-  , ElimFirst   , elimIdentity   , ElimIdentity-  , elimLast-  , ElimLast   , elimList   , ElimList   , elimMax@@ -63,10 +82,8 @@   , ElimNonEmpty   , elimOrdering   , ElimOrdering-  , elimProduct-  , ElimProduct-  , elimSum-  , ElimSum+  , elimProxy+  , ElimProxy   , elimTuple0   , ElimTuple0   , elimTuple2@@ -89,27 +106,22 @@  import Control.Monad.Extra +import Data.Eliminator.Functor+import Data.Eliminator.Monoid+import Data.Eliminator.Semigroup import Data.Eliminator.TH-import Data.Functor.Const (Const(..))-import Data.Functor.Const.Singletons (SConst(..))-import Data.Functor.Identity (Identity(..))-import Data.Functor.Identity.Singletons (SIdentity(..)) import Data.List.NonEmpty (NonEmpty(..)) import Data.List.NonEmpty.Singletons (SNonEmpty(..))-import Data.Monoid hiding (First, Last)-import Data.Monoid.Singletons hiding (SFirst, SLast) import Data.Nat import Data.Ord (Down(..)) import Data.Ord.Singletons (SDown(..))-import Data.Semigroup-import Data.Semigroup.Singletons+import Data.Proxy.Singletons (SProxy(..)) import Data.Void (Void)  import Language.Haskell.TH (nameBase) import Language.Haskell.TH.Desugar (tupleNameDegree_maybe) -import Prelude.Singletons hiding-  (All, Any, Const, Last, Min, Max, Product, Sum)+import Prelude.Singletons  {- $eliminators @@ -128,27 +140,15 @@ -}  $(concatMapM (\n -> (++) <$> deriveElim n <*> deriveTypeElim n)-             [ ''All-             , ''Any-             , ''Arg-             , ''Bool-             , ''Const+             [ ''Bool              , ''Down-             , ''Dual              , ''Either-             , ''First-             , ''Identity-             , ''Last-             , ''Max              , ''Maybe-             , ''Min              , ''Nat              , ''NonEmpty              , ''Ordering-             , ''Product-             , ''Sum+             , ''Proxy              , ''Void-             , ''WrappedMonoid              ]) $(deriveElimNamed     "elimList" ''[]) $(deriveTypeElimNamed "ElimList" ''[])
+ src/Data/Eliminator/Functor.hs view
@@ -0,0 +1,51 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneKindSignatures #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-|+Module:      Data.Eliminator.Functor+Copyright:   (C) 2021 Ryan Scott+License:     BSD-style (see the file LICENSE)+Maintainer:  Ryan Scott+Stability:   Experimental+Portability: GHC++Eliminator functions for data types in the @Data.Functor.*@ module namespace.+All of these are re-exported from "Data.Eliminator" with the exceptions of+'Sum' and 'Product', as these clash with eliminators of the same names in+"Data.Eliminator.Semigroup" and "Data.Eliminator.Monoid".+-}+module Data.Eliminator.Functor (+    elimConst+  , ElimConst+  , elimIdentity+  , ElimIdentity+  , elimProduct+  , ElimProduct+  , elimSum+  , ElimSum+  ) where++import Control.Monad.Extra++import Data.Eliminator.TH+import Data.Functor.Const (Const(..))+import Data.Functor.Const.Singletons (SConst(..))+import Data.Functor.Identity (Identity(..))+import Data.Functor.Identity.Singletons (SIdentity(..))+import Data.Functor.Product (Product(..))+import Data.Functor.Product.Singletons (SProduct(..))+import Data.Functor.Sum (Sum(..))+import Data.Functor.Sum.Singletons (SSum(..))++$(concatMapM (\n -> (++) <$> deriveElim n <*> deriveTypeElim n)+             [ ''Const+             , ''Identity+             , ''Product+             , ''Sum+             ])
+ src/Data/Eliminator/Monoid.hs view
@@ -0,0 +1,59 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneKindSignatures #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-|+Module:      Data.Eliminator.Monoid+Copyright:   (C) 2021 Ryan Scott+License:     BSD-style (see the file LICENSE)+Maintainer:  Ryan Scott+Stability:   Experimental+Portability: GHC++Eliminator functions for data types in "Data.Monoid". All of these are+re-exported from "Data.Eliminator" with the following exceptions:++* 'First' and 'Last' are not re-exported from "Data.Eliminator", as they clash+  with eliminators of the same names in "Data.Eliminator.Functor" and+  "Data.Eliminator.Semigroup".++* 'Sum' and 'Product' are not re-exported from "Data.Eliminator", as they clash+  with eliminators of the same names in "Data.Eliminator.Functor".+-}+module Data.Eliminator.Monoid (+    elimAll+  , ElimAll+  , elimAny+  , ElimAny+  , elimDual+  , ElimDual+  , elimFirst+  , ElimFirst+  , elimLast+  , ElimLast+  , elimProduct+  , ElimProduct+  , elimSum+  , ElimSum+  ) where++import Control.Monad.Extra++import Data.Eliminator.TH+import Data.Monoid+import Data.Monoid.Singletons++$(concatMapM (\n -> (++) <$> deriveElim n <*> deriveTypeElim n)+             [ ''All+             , ''Any+             , ''Dual+             , ''First+             , ''Last+             , ''Product+             , ''Sum+             ])
+ src/Data/Eliminator/Semigroup.hs view
@@ -0,0 +1,67 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneKindSignatures #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-|+Module:      Data.Eliminator.Semigroup+Copyright:   (C) 2021 Ryan Scott+License:     BSD-style (see the file LICENSE)+Maintainer:  Ryan Scott+Stability:   Experimental+Portability: GHC++Eliminator functions for data types in "Data.Semigroup". All of these are+re-exported from "Data.Eliminator" with the following exceptions:++* 'First' and 'Last' are not re-exported from "Data.Eliminator", as they clash+  with eliminators of the same names in "Data.Eliminator.Functor" and+  "Data.Eliminator.Monoid".++* 'Sum' and 'Product' are not re-exported from "Data.Eliminator", as they clash+  with eliminators of the same names in "Data.Eliminator.Functor".+-}+module Data.Eliminator.Semigroup (+    elimAll+  , ElimAll+  , elimAny+  , ElimAny+  , elimArg+  , ElimArg+  , elimDual+  , ElimDual+  , elimFirst+  , ElimFirst+  , elimLast+  , ElimLast+  , elimMax+  , ElimMax+  , elimMin+  , ElimMin+  , elimProduct+  , ElimProduct+  , elimSum+  , ElimSum+  , elimWrappedMonoid+  , ElimWrappedMonoid+  ) where++import Control.Monad.Extra++import Data.Eliminator.Monoid hiding (elimFirst, ElimFirst, elimLast, ElimLast)+import Data.Eliminator.TH+import Data.Semigroup+import Data.Semigroup.Singletons++$(concatMapM (\n -> (++) <$> deriveElim n <*> deriveTypeElim n)+             [ ''Arg+             , ''First+             , ''Last+             , ''Max+             , ''Min+             , ''WrappedMonoid+             ])
src/Data/Eliminator/TH.hs view
@@ -275,9 +275,10 @@   -> 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+  info@(DatatypeInfo { datatypeVars      = dataVarBndrs+                     , datatypeInstTypes = instTys+                     , datatypeVariant   = variant+                     , datatypeCons      = cons                      }) <- reifyDatatype dataName   let noDataFamilies =         fail "Eliminators for data family instances are currently not supported"@@ -293,6 +294,8 @@       predVarBndr = kindedTV predVar (InfixT promDataKind ''(~>) (ConT ''Kind.Type))       singVarBndr = kindedTV singVar promDataKind   caseTypes <- traverse (caseType prox dataName predVar) cons+  unless (length (findParams info) == length instTys) $+    fail "Eliminators for polymorphically recursive data types are currently not supported"   let returnType  = predType predVar (VarT singVar)       elimType    = elimTypeSig prox dataVarBndrs predVarBndr singVarBndr                                 caseTypes returnType@@ -328,44 +331,33 @@                      returnType                      (zip vars fieldTypes) --- Generate a single clause for a term-level eliminator.-caseClause ::-     Name            -- The name of the eliminator function+-- Generate a single clause for a term-level eliminator's @go@ function.+goCaseClause ::+     Name            -- The name of the @go@ function   -> Name            -- The name of the data type-  -> [TyVarBndrUnit] -- The type variables bound by the data type-  -> TyVarBndrUnit   -- The predicate type variable-  -> Int             -- The index of this constructor (0-indexed)-  -> Int             -- The total number of data constructors+  -> Name            -- The name of the "case alternative" to apply on the right-hand side   -> ConstructorInfo -- The data constructor   -> Q Clause        -- The generated function clause-caseClause elimName dataName dataVarBndrs predVarBndr conIndex numCons+goCaseClause goName dataName usedCaseVar     (ConstructorInfo { constructorName   = conName                      , constructorFields = fieldTypes })   = do let numFields = length fieldTypes        singVars    <- newNameList "s"   numFields        singVarSigs <- newNameList "sTy" numFields-       usedCaseVar <- newName "useThis"-       caseVars    <- ireplicateA numCons $ \i ->-                        if i == conIndex-                        then pure usedCaseVar-                        else newName ("_p" ++ show i)        let singConName = singledDataConName defaultOptions conName            mkSingVarPat var varSig = SigP (VarP var) (singType varSig)            singVarPats = zipWith mkSingVarPat singVars singVarSigs             mbInductiveArg singVar singVarSig varType =-             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+             let inductiveArg = VarE goName `AppTypeE` VarT singVarSig+                                            `AppE`     VarE singVar+             in mbInductiveCase dataName varType $ const inductiveArg            mkArg f (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)+       pure $ Clause [ConP singConName [] singVarPats]                      (NormalB rhs)                      [] @@ -403,7 +395,7 @@              let inductiveArg = foldAppT prefix $ VarT predVarName                                                 : VarT singVar                                                 : map VarT caseVarNames-             in mbInductiveCase dataName varType inductiveArg+             in mbInductiveCase dataName varType $ const inductiveArg            mkArg f (singVar, varType) =              foldAppDefunT (f `AppT` VarT singVar)                          $ maybeToList (mbInductiveArg singVar varType)@@ -476,16 +468,40 @@     ForallT [kindedTVSpecified 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+  -- A unique characteristic of term-level eliminators is that we manually+  -- apply the static argument transformation, e.g.,+  --+  --   elimT :: forall a (p :: T a ~> Type) (t :: T a).+  --            Sing t+  --         -> (forall (x :: a) (xs :: T a).+  --               Sing x -> Sing xs -> Apply p xs -> Apply p (MkT x xs))+  --         -> Apply p t+  --   elimT st k = go @s k+  --     where+  --       go :: forall (t' :: T a).+  --             Sing t' -> Apply p t'+  --       go (SMkT (sx :: Sing x) (sxs :: Sing xs)) =+  --         k sx sxs (go @xs sxs)+  --+  -- This reduces the likelihood of recursive calls falling afoul of GHC's+  -- ambiguity check.+  qElimEqns _ elimName dataName _dataVarBndrs predVarBndr singVarBndr _caseTypes cons = do+    singTermVar <- newName "s"+    caseVars    <- newNameList "p" $ length cons+    goName      <- newName "go"+    let singTypeVar = tvName singVarBndr+    goSingTypeVar <- newName $ nameBase singTypeVar+    let elimRHS       = VarE goName `AppTypeE` VarT singTypeVar `AppE` VarE singTermVar+        goSingVarBndr = mapTVName (const goSingTypeVar) singVarBndr+        goReturnType  = predType (tvName predVarBndr) (VarT goSingTypeVar)+        goType = ForallT (changeTVFlags SpecifiedSpec [goSingVarBndr]) [] $+                 ArrowT `AppT` singType goSingTypeVar `AppT` goReturnType+    goClauses+      <- if null cons+         then pure [Clause [VarP singTermVar] (NormalB (CaseE (VarE singTermVar) [])) []]+         else zipWithM (goCaseClause goName dataName) caseVars cons+    pure $ FunD elimName [ Clause (map VarP (singTermVar:caseVars)) (NormalB elimRHS)+                                  [SigD goName goType, FunD goName goClauses] ]  instance Eliminator IsType where   elimSigD _ = KiSigD@@ -512,21 +528,20 @@  mbInductiveType :: Name -> Name -> Name -> Kind -> Maybe Type mbInductiveType dataName predVar var varType =-  mbInductiveCase dataName varType $ predType predVar $ VarT var+  mbInductiveCase dataName varType $ const $ predType predVar $ VarT var --- TODO: Rule out polymorphic recursion-mbInductiveCase :: Name -> Type -> a -> Maybe a+mbInductiveCase :: Name -> Type -> ([TypeArg] -> a) -> Maybe a mbInductiveCase dataName varType inductiveArg   = case unfoldType varType of-      (headTy, _)+      (headTy, argTys)           -- Annoying special case for lists         | ListT <- headTy         , dataName == ''[]-       -> Just inductiveArg+       -> Just $ inductiveArg argTys          | ConT n <- headTy         , dataName == n-       -> Just inductiveArg+       -> Just $ inductiveArg argTys          | otherwise        -> Nothing@@ -573,10 +588,6 @@ foldAppE :: Exp -> [Exp] -> Exp foldAppE = foldl' AppE --- 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@@ -602,6 +613,108 @@     loop cnt n         | cnt <= 0  = pure []         | otherwise = liftA2 (:) (f n) (loop (cnt - 1) $! (n + 1))++-- | Find the data type constructor arguments that are parameters.+--+-- Parameters are names which are unchanged across the structure.+-- They appear at least once in every constructor type, always appear+-- in the same argument position(s), and nothing else ever appears in those+-- argument positions.+--+-- This was adapted from a similar algorithm used in Idris+-- (https://github.com/idris-lang/Idris-dev/blob/a13caeb4e50d0c096d34506f2ebf6b9d140a07aa/src/Idris/Elab/Utils.hs#L401-L468),+-- licensed under the BSD-3-Clause license.+findParams :: DatatypeInfo -> [Int]+findParams (DatatypeInfo { datatypeName      = dataName+                         , datatypeInstTypes = instTys+                         , datatypeCons      = cons+                         }) =+  let allapps = map getDataApp cons+        -- do each constructor separately, then merge the results (names+        -- may change between constructors)+      conParams = map paramPos allapps+  in inAll conParams+  where+    inAll :: Eq pos => [[pos]] -> [pos]+    inAll [] = []+    inAll (x : xs) = filter (\p -> all (\ps -> p `elem` ps) xs) x++    paramPos :: Eq name => [[Maybe name]] -> [Int]+    paramPos [] = []+    paramPos (args : rest)+          = dropNothing $ keepSame (zip [0..] args) rest++    dropNothing :: [(pos, Maybe name)] -> [pos]+    dropNothing [] = []+    dropNothing ((_, Nothing) : ts) = dropNothing ts+    dropNothing ((x, _) : ts) = x : dropNothing ts++    keepSame :: Eq name =>+                [(pos, Maybe name)] -> [[Maybe name]] ->+                [(pos, Maybe name)]+    keepSame as [] = as+    keepSame as (args : rest) = keepSame (update as args) rest++    update :: Eq name => [(pos, Maybe name)] -> [Maybe name] -> [(pos, Maybe name)]+    update [] _ = []+    update _ [] = []+    update ((n, Just x) : as) (Just x' : args)+        | x == x' = (n, Just x) : update as args+    update ((n, _) : as) (_ : args) = (n, Nothing) : update as args++    getDataApp :: ConstructorInfo -> [[Maybe Name]]+    getDataApp (ConstructorInfo { constructorFields  = fields }) =+      concatMap getThem $+      fields ++ [ applyType (ConT dataName) $ map TANormal+                                            $ map unSigType instTys+                ]+      where+        getThem :: Type -> [[Maybe Name]]+        getThem ty = maybeToList $ mbInductiveCase dataName ty inductiveArg++        inductiveArg :: [TypeArg] -> [Maybe Name]+        inductiveArg argTys =+          let visArgTys = filterTANormals argTys+          in mParam visArgTys visArgTys++    -- keep the arguments which are single names, which appear+    -- in the return type, counting only the first time they appear in+    -- the return type as the parameter position+    mParam :: [Type] -> [Type] -> [Maybe Name]+    mParam _    [] = []+    mParam args (VarT n:rest)+      | paramIn False n args+      = Just n : mParam (filter (noN n) args) rest+    mParam args (_:rest) = Nothing : mParam args rest++    paramIn :: Bool -> Name -> [Type] -> Bool+    paramIn ok _ []          = ok+    paramIn ok n (VarT t:ts) = paramIn (ok || n == t) n ts+    paramIn ok n (t:ts)+      | n `elem` freeVariables t = False -- not a single name+      | otherwise                = paramIn ok n ts++    -- If the name appears again later, don't count that appearance+    -- as a parameter position+    noN :: Name -> Type -> Bool+    noN n (VarT t) = n /= t+    noN _ _        = False++-----+-- Taken directly from th-desugar+-----++-- | Remove all of the explicit kind signatures from a 'Type'.+unSigType :: Type -> Type+unSigType (SigT t _)            = t+unSigType (AppT f x)            = AppT (unSigType f) (unSigType x)+unSigType (ForallT tvbs ctxt t) = ForallT tvbs (map unSigType ctxt) (unSigType t)+unSigType (InfixT t1 n t2)      = InfixT (unSigType t1) n (unSigType t2)+unSigType (UInfixT t1 n t2)     = UInfixT (unSigType t1) n (unSigType t2)+unSigType (ParensT t)           = ParensT (unSigType t)+unSigType (AppKindT t k)        = AppKindT (unSigType t) (unSigType k)+unSigType (ImplicitParamT n t)  = ImplicitParamT n (unSigType t)+unSigType t                     = t  ----- -- Taken directly from singletons
src/Data/Eliminator/TypeNats.hs view
@@ -21,7 +21,7 @@ import Data.Kind (Type) import Data.Singletons -import GHC.TypeLits.Singletons+import GHC.TypeLits.Singletons () import GHC.TypeNats  import Unsafe.Coerce (unsafeCoerce)
tests/DecideTypes.hs view
@@ -11,6 +11,7 @@ {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -Wno-unused-foralls #-} module DecideTypes where  import Data.Eliminator@@ -18,7 +19,7 @@ import Data.Nat import Data.Singletons.TH hiding (Decision(..)) -import Prelude.Singletons+import Prelude.Singletons (ConstSym1)  -- Due to https://github.com/goldfirere/singletons/issues/82, promoting the -- Decision data type from Data.Singletons.Decide is a tad awkward. To work@@ -33,8 +34,11 @@              -> (forall (yes :: a). Sing yes -> p @@ Proved yes)              -> (forall (no :: a ~> Void). Sing no -> p @@ Disproved no)              -> p @@ d-elimDecision (SProved yes)   pProved _          = pProved yes-elimDecision (SDisproved no) _       pDisproved = pDisproved no+elimDecision sd pProved pDisproved = go @d sd+  where+    go :: forall (d' :: PDecision a). Sing d' -> p @@ d'+    go (SProved yes)   = pProved yes+    go (SDisproved no) = pDisproved no  type ElimDecision :: forall a.                      forall (p :: PDecision a ~> Type)@@ -89,44 +93,71 @@ newtype WhyDecEqList (l1 :: [e]) = WhyDecEqList   { runWhyDecEqList :: forall (l2 :: [e]). Sing l2 -> Decision (l1 :~: l2) } -$(singletons [d|-  type ConstVoidNat :: forall (m :: Nat) -> Const Type m -> Const Type (S m)-  type ConstVoidNat m r = Void+type ConstVoidNat :: Nat -> Type -> Type+type ConstVoidNat m r = Void -  type EqSameNat :: Nat -> forall (m :: Nat) -> Const Type m -> Const Type (S m)-  type EqSameNat n m r = n :~: m+-- ElimNat requires an argument of kind (forall (m :: Nat) -> ...), which is+-- not the same thing as (Nat -> ...). Unfortunately, it's not easy to convince+-- singletons-th to generate defunctionalization symbols for ConstVoidNat that+-- have a dependent kind like this. As a result, we have to define+-- defunctionalization symbols by hand with the appropriate kind.+type ConstVoidNatSym :: forall (m :: Nat) -> (Type ~> Type)+data ConstVoidNatSym m z+type instance Apply (ConstVoidNatSym m) r = ConstVoidNat m r -  type ConstVoidList :: forall e. forall (y :: e) (ys :: [e])-                     -> Const Type ys -> Const Type (y:ys)-  type ConstVoidList y ys r = Void+type EqSameNat :: Nat -> Nat -> Type -> Type+type EqSameNat n m r = n :~: m -  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 EqSameNatSym :: Nat -> forall (m :: Nat) -> (Type ~> Type)+data EqSameNatSym n m z+type instance Apply (EqSameNatSym n m) r = EqSameNat n m r +type ConstVoidList :: e -> [e] -> Type -> Type+type ConstVoidList y ys r = Void++type ConstVoidListSym :: forall e. forall (y :: e) (ys :: [e])+                      -> (Type ~> Type)+data ConstVoidListSym y ys z+type instance Apply (ConstVoidListSym y ys) r = ConstVoidList y ys r++type EqSameList :: e -> [e] -> e -> [e] -> Type -> Type+type EqSameList x xs y ys r = (x :~: y, xs :~: ys)++type EqSameListSym :: forall e. e -> [e] -> forall (y :: e) (ys :: [e])+                   -> (Type ~> Type)+data EqSameListSym x xs y ys z+type instance Apply (EqSameListSym x xs y ys) r = EqSameList x xs y ys r+ $(singletons [d|   type NatEqConsequencesBase :: Nat -> Type-  type NatEqConsequencesBase m = ElimNat (ConstSym1 Type) m () ConstVoidNatSym1+  type NatEqConsequencesBase m = ElimNat (ConstSym1 Type) m () ConstVoidNatSym -  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 NatEqConsequencesStep :: Nat -> (Nat ~> Type) -> Nat -> Type+  type NatEqConsequencesStep m r n = ElimNat (ConstSym1 Type) n Void (EqSameNatSym m)    type ListEqConsequencesBase :: [e] -> Type-  type ListEqConsequencesBase ys = ElimList (ConstSym1 Type) ys () ConstVoidListSym2+  type ListEqConsequencesBase ys = ElimList (ConstSym1 Type) ys () ConstVoidListSym -  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 ListEqConsequencesStep :: e -> [e] -> ([e] ~> Type) -> [e] -> Type+  type ListEqConsequencesStep x xs r ys = ElimList (ConstSym1 Type) ys Void (EqSameListSym x xs)   |]) +type NatEqConsequencesStepSym :: forall (m :: Nat)+                              -> (Nat ~> Type) ~> (Nat ~> Type)+data NatEqConsequencesStepSym m z+type instance Apply (NatEqConsequencesStepSym m) r = NatEqConsequencesStepSym2 m r++type ListEqConsequencesStepSym :: forall e. forall (x :: e) (xs :: [e])+                               -> ([e] ~> Type) ~> ([e] ~> Type)+data ListEqConsequencesStepSym x xs z+type instance Apply (ListEqConsequencesStepSym x xs) r = ListEqConsequencesStepSym3 x xs r+ $(singletons [d|   type NatEqConsequences :: Nat -> Nat -> Type   type NatEqConsequences n m =     ElimNat (ConstSym1 (Nat ~> Type)) n             NatEqConsequencesBaseSym0-            NatEqConsequencesStepSym1 @@ m+            NatEqConsequencesStepSym @@ m    type WhyNatEqConsequencesSame :: Nat -> Type   type WhyNatEqConsequencesSame a = NatEqConsequences a a@@ -141,7 +172,7 @@   type ListEqConsequences (xs :: [e]) (ys :: [e]) =     ElimList (ConstSym1 ([e] ~> Type)) xs              ListEqConsequencesBaseSym0-             ListEqConsequencesStepSym2 @@ ys+             ListEqConsequencesStepSym @@ ys    type WhyListEqConsequencesSame :: [e] -> Type   type WhyListEqConsequencesSame es = ListEqConsequences es es
tests/GADTSpec.hs view
@@ -82,12 +82,16 @@             -> (forall a' b' (x :: a'). Sing x -> p @@ (MkFlarble1 x :: Flarble a' b'))             -> (forall b'. p @@ (MkFlarble2 :: Flarble Bool (Maybe b')))             -> p @@ f-elimFlarble s@(SMkFlarble1 sx) pMkFlarble1 _ =-  case s of-    (_ :: Sing (MkFlarble1 x :: Flarble a' b')) -> pMkFlarble1 @a' @b' @x sx-elimFlarble s@SMkFlarble2 _ pMkFlarble2 =-  case s of-    (_ :: Sing (MkFlarble2 :: Flarble Bool (Maybe b'))) -> pMkFlarble2 @b'+elimFlarble sf pMkFlarble1 pMkFlarble2 = go @a @b @f sf+  where+    go :: forall a' b' (f' :: Flarble a' b').+          Sing f' -> p @@ f'+    go s@(SMkFlarble1 sx) =+      case s of+        (_ :: Sing (MkFlarble1 x :: Flarble a'' b'')) -> pMkFlarble1 @a'' @b'' @x sx+    go s@SMkFlarble2 =+      case s of+        (_ :: Sing (MkFlarble2 :: Flarble Bool (Maybe b''))) -> pMkFlarble2 @b''  type ElimFlarble ::      forall (p :: forall x y. Flarble x y ~> Type)@@ -113,12 +117,15 @@                 -> (forall a' b'. a' -> p @@ a' @@ b')                 -> (forall b'. p @@ Bool @@ Maybe b')                 -> p @@ a @@ b-elimPropFlarble f@(MkFlarble1 x) pMkFlarble1 _ =-  case f of-    (_ :: Flarble a' b') -> pMkFlarble1 @a' @b' x-elimPropFlarble f@MkFlarble2 _ pMkFlarble2 =-  case f of-    (_ :: Flarble Bool (Maybe b')) -> pMkFlarble2 @b'+elimPropFlarble fl pMkFlarble1 pMkFlarble2 = go @a @b fl+  where+    go :: forall a' b'. Flarble a' b' -> p @@ a' @@ b'+    go f@(MkFlarble1 x) =+      case f of+        (_ :: Flarble a'' b'') -> pMkFlarble1 @a'' @b'' x+    go f@MkFlarble2 =+      case f of+        (_ :: Flarble Bool (Maybe b'')) -> pMkFlarble2 @b''  type ElimPropFlarble ::      forall (p :: Type ~> Type ~> Prop)
+ tests/PolyRecTypes.hs view
@@ -0,0 +1,93 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneKindSignatures #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+module PolyRecTypes where++import Data.Kind+import Data.Singletons.Base.TH++import Internal++$(singletons [d|+  type WeirdList :: Type -> Type+  data WeirdList a = WeirdNil | WeirdCons a (WeirdList (WeirdList a))+  |])++elimWeirdList :: forall (p :: forall t. WeirdList t ~> Type)+                        a (wl :: WeirdList a).+                 Sing wl+              -> (forall t. p @t @@ WeirdNil)+              -> (forall t (x :: t) (xs :: WeirdList (WeirdList t)).+                         Sing x -> Sing xs -> p @(WeirdList t) @@ xs -> p @t @@ (WeirdCons x xs))+              -> p @a @@ wl+elimWeirdList swl pWeirdNil pWeirdCons = go @a @wl swl+  where+    go :: forall t (wlt :: WeirdList t). Sing wlt -> p @t @@ wlt+    go SWeirdNil = pWeirdNil @t+    go (SWeirdCons (sx :: Sing x) (sxs :: Sing xs)) =+      pWeirdCons @t @x @xs sx sxs (go @(WeirdList t) @xs sxs)++type ElimWeirdList :: forall (p :: forall t. WeirdList t ~> Type)+                   -> forall a.+                      forall (wl :: WeirdList a)+                   -> (forall t. p @t @@ WeirdNil)+                   -> (forall t.+                       forall (x :: t) (xs :: WeirdList (WeirdList t)) ->+                       p @(WeirdList t) @@ xs ~> p @t @@ (WeirdCons x xs))+                   -> p @a @@ wl+type family ElimWeirdList p wl pWeirdNil pWeirdCons where+  forall (p :: forall t. WeirdList t ~> Type)+         (pWeirdNil :: forall t. p @t @@ WeirdNil)+         (pWeirdCons :: forall t. forall (x :: t) (xs :: WeirdList (WeirdList t)) ->+                        p @(WeirdList t) @@ xs ~> p @t @@ (WeirdCons x xs))+         a.+    ElimWeirdList p (WeirdNil @a) pWeirdNil pWeirdCons = pWeirdNil @a+  forall (p :: forall t. WeirdList t ~> Type)+         (pWeirdNil :: forall t. p @t @@ WeirdNil)+         (pWeirdCons :: forall t. forall (x :: t) (xs :: WeirdList (WeirdList t)) ->+                        p @(WeirdList t) @@ xs ~> p @t @@ (WeirdCons x xs))+         a (x :: a) (xs :: WeirdList (WeirdList a)).+    ElimWeirdList p (WeirdCons @a x xs) pWeirdNil pWeirdCons =+      pWeirdCons @a x xs @@ ElimWeirdList p @(WeirdList a) xs pWeirdNil pWeirdCons++elimPropWeirdList :: forall (p :: Prop ~> Prop)+                            (a :: Prop).+                     WeirdList a+                  -> (forall (t :: Prop). p @@ t)+                  -> (forall (t :: Prop).+                             t -> WeirdList (WeirdList t) -> p @@ WeirdList t -> p @@ t)+                  -> p @@ a+elimPropWeirdList wl pWeirdNil pWeirdCons = go @a wl+  where+    go :: forall (t :: Prop). WeirdList t -> p @@ t+    go WeirdNil = pWeirdNil @t+    go (WeirdCons x xs) = pWeirdCons @t x xs (go @(WeirdList t) xs)++type ElimPropWeirdList :: forall (p :: Prop ~> Prop)+                       -> forall (a :: Prop).+                          WeirdList a+                       -> (forall (t :: Prop). p @@ t)+                       -> (forall (t :: Prop).+                                  t ~> WeirdList (WeirdList t) ~> p @@ WeirdList t ~> p @@ t)+                       -> p @@ a+type family ElimPropWeirdList p wl pWeirdNil pWeirdCons where+  forall (p :: Prop ~> Prop)+         (pWeirdNil :: forall (t :: Prop). p @@ t)+         (pWeirdCons :: forall (t :: Prop). t ~> WeirdList (WeirdList t) ~> p @@ WeirdList t ~> p @@ t)+         a.+    ElimPropWeirdList p (WeirdNil @a) pWeirdNil pWeirdCons = pWeirdNil @a+  forall (p :: Prop ~> Prop)+         (pWeirdNil :: forall (t :: Prop). p @@ t)+         (pWeirdCons :: forall (t :: Prop). t ~> WeirdList (WeirdList t) ~> p @@ WeirdList t ~> p @@ t)+         a (x :: a) (xs :: WeirdList (WeirdList a)).+    ElimPropWeirdList p (WeirdCons x xs) pWeirdNil pWeirdCons =+      pWeirdCons @a @@ x @@ xs @@ ElimPropWeirdList p @(WeirdList a) xs pWeirdNil pWeirdCons
tests/VecTypes.hs view
@@ -53,9 +53,13 @@         -> (forall (k :: Nat) (x :: a) (xs :: Vec a k).                    Sing x -> Sing xs -> p @@ xs -> p @@ (x :# xs))         -> p @@ v-elimVec SVNil pVNil _ = pVNil-elimVec (sx :%# (sxs :: Sing (xs :: Vec a k))) pVNil pVCons =-  pVCons sx sxs (elimVec @a @p @k @xs sxs pVNil pVCons)+elimVec sv pVNil pVCons = go @n @v sv+  where+    go :: forall (n' :: Nat) (v' :: Vec a n').+          Sing v' -> p @@ v'+    go SVNil = pVNil+    go (sx :%# (sxs :: Sing (xs :: Vec a k))) =+      pVCons sx sxs (go @k @xs sxs)  type ElimVec :: forall a.                 forall (p :: forall (k :: Nat). Vec a k ~> Type)@@ -86,9 +90,11 @@             -> p @@ Z             -> (forall (k :: Nat). a -> Vec a k -> p @@ k -> p @@ S k)             -> p @@ n-elimPropVec VNil pZ _ = pZ-elimPropVec (x :# (xs :: Vec a k)) pZ pS =-  pS x xs (elimPropVec @a @p @k xs pZ pS)+elimPropVec v pZ pS = go @n v+  where+    go :: forall (n' :: Nat). Vec a n' -> p @@ n'+    go VNil                   = pZ+    go (x :# (xs :: Vec a k)) = pS x xs (go @k xs)  type ElimPropVec :: forall a.                     forall (p :: Nat ~> Prop)