diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,30 @@ +Copyright (c) 2018, Alejandro Serrano + +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * Redistributions in binary form must reproduce the above + copyright notice, this list of conditions and the following + disclaimer in the documentation and/or other materials provided + with the distribution. + + * Neither the name of Alejandro Serrano nor the names of other + contributors may be used to endorse or promote products derived + from this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,157 @@ +# `kind-generics-th`: Template Haskell support for generating `GenericK` instances + +This package provides Template Haskell functionality to automatically derive +`GenericK` instances. Currently, this only supports the version of `GenericK` +as found in the `kind-generics` library. (The `GenericK` class found in +`kind-generics-sop` is not supported at the moment.) + +## How to use this library + +To derive instances of `GenericK` for a data type, simply pass the Template +Haskell–quoted `Name` of the type to the `deriveGenericK` function, as in the +following example: + +```haskell +$(deriveGenericK ''Either) +``` + +If you wish to pass a data family instance, one can pass the name of a +constructor belonging to the particular family instance, such as in the +following example: + +```haskell +data family Foo a b +data instance Foo Int b = MkFooInt b + +$(deriveGenericK 'MkFooInt) +``` + +You will likely need to enable most of these language extensions in order for +GHC to accept the generated code: + +* `DataKinds` +* `EmptyCase` (if using an empty data type) +* `FlexibleInstances` +* `MultiParamTypeClasses` +* `PolyKinds` (if using a poly-kinded data type) +* `TemplateHaskell` +* `TypeFamilies` + +## How many `GenericK` instances are generated + +`deriveGenericK` typically generates multiple `GenericK` instances per data +type, as there is one `GenericK` instance per partial application of a data +type constructor. For instance, `$(deriveGenericK ''Either)` will generate +three `GenericK` instances: + +```haskell +instance GenericK (Either a b) LoT0 where ... +instance GenericK (Either a) (b :&&: LoT0) where ... +instance GenericK Either (a :&&: b :&&: LoT0) where ... +``` + +Not every data type can be partially applied all the way in this fashion, +however. Some notable counterexamples are: + +1. Data family instances. In the following example: + + ```haskell + data family Bar a b + data instance Bar a a = MkBar a + ``` + + One cannot partially apply to `Bar a a` to simply `Bar a`, so + `$(deriveGenericK 'MkBar)` will only generate a single instance for + `GenericK (Bar a a) LoT0`. +2. Dependent kinds. `kind-generics` is not currently capable of representing + data types such as the following in their full generality: + + ```haskell + data Baz k (a :: k) + ``` + + Because the `k` type variable is used in the kind of `a` (i.e., it is used + in a visible, dependent fashion). As a consequence, + `$(deriveGenericK ''Baz)` will only generate the following instances: + + * `instance GenericK (Baz k a) LoT0` + * `instance GenericK (Baz k) (a :&&: LoT0)` +3. Data types with type family applications. In the following example: + + ```haskell + type family Fam a + newtype WrappedFam a = WrapFam (Fam a) + ``` + + It is impossible to write a `GenericK` instance for a partial application + of `WrappedFam`, since the representation type would necessarily need to + partially apply `Fam`, which GHC does not permit. Therefore, + `$(deriveGenericK ''WrappedFam)` will only generate a single instance for + `GenericK (WrappedFam a) LoT0`. + + There are some uses of type families that are not supported altogether. + For instance, if a type family is applied to an _existentially_ quantified + type variable, as in the following example: + + ```haskell + data ExFam where + MkExFam :: forall a. Fam a -> ExFam + ``` + + Representing `ExFam` would fundamentally require a partial application of + `Fam`, as `type RepK ExFam = Exists * (Field (Fam :$: Var0))`. As a result, + it is impossible to give `ExFam` a `GenericK` instance. + + Note that not all type families are problematic. For instance: + + ```haskell + type family Fam2 :: * -> * + newtype WrappedFam2 a = WrapFam2 (Fam2 a) + ``` + + In this example, `Fam2` is perfectly fine to partially apply, so + `$(deriveGenericK ''WrappedFam2)` will generate two instances (as opposed + to just one, as was the case for `WrappedFam`). + +## Limitations + +`kind-generics` is capable of representing a wide variety of data types. The +Template Haskell machinery in this library makes a best-effort attempt to +automate the creation of most of these instances, but there are a handful of +corner cases that it does not handle well. This section documents all of the +known limitations of `deriveGenericK`: + +1. Data constructors with rank-_n_ field types (e.g., `(forall a. a -> a)`) + are currently not supported. +2. Data constructors with unlifted field types (e.g., `Int#` or `(# Bool #)`) + are unlikely to work. +3. GADTs that make use of certain forms of kind equalities are currently not + supported. For example: + + ```haskell + data Quux (a :: k) where + MkQuux :: forall (a :: *). Maybe a -> Quux a + ``` + + If one were to rewrite `Quux` to make the existential quantification + explicit, it would look like this: + + ```haskell + data Quux (a :: k) = + forall (a' :: *). (k ~ Type, a' ~~ a) => MkQuux (Maybe a') + ``` + + Therefore, we ought to get a `GenericK` instance like this: + + ```haskell + instance GenericK (Quux :: k -> *) (a :&&: LoT0) where + type RepK (Quux :: k -> *) = + Exists * + ((Kon (k ~ Type) :&: (Var0 :~~: Var1)) :=>: Field (Maybe :$: Var0)) + ... + ``` + + Devising an algorithm that converts the original GADT definition of `Quux` + into the explicitly existential form is not straightforward, however. In + particular, `deriveGenericK` only detects the `k ~ *` part correctly at the + moment, so it will generate an ill kinded instance for `Quux`. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/kind-generics-th.cabal b/kind-generics-th.cabal new file mode 100644 --- /dev/null +++ b/kind-generics-th.cabal @@ -0,0 +1,41 @@ +cabal-version: >=1.10 +name: kind-generics-th +version: 0.1.0.0 +synopsis: Template Haskell support for generating `GenericK` instances +description: This package provides Template Haskell functionality to + automatically derive @GenericK@ instances (from the + @kind-generics@ library). +-- bug-reports: +license: BSD3 +license-file: LICENSE +author: Alejandro Serrano +maintainer: trupill@gmail.com +-- copyright: +category: Data +build-type: Simple +extra-source-files: README.md + +source-repository head + type: git + location: https://gitlab.com/trupill/kind-generics.git + subdir: kind-generics-th + +library + exposed-modules: Generics.Kind.TH + build-depends: base >=4.12 && <5 + , kind-generics >=0.3 + , template-haskell >=2.14 && <2.15 + , th-abstraction >=0.2.8 && <0.3 + hs-source-dirs: src + default-language: Haskell2010 + ghc-options: -Wall + +test-suite tests + type: exitcode-stdio-1.0 + main-is: Main.hs + build-depends: base >=4.12 && <5 + , kind-generics >=0.2.1 + , kind-generics-th + hs-source-dirs: tests + default-language: Haskell2010 + ghc-options: -Wall diff --git a/src/Generics/Kind/TH.hs b/src/Generics/Kind/TH.hs new file mode 100644 --- /dev/null +++ b/src/Generics/Kind/TH.hs @@ -0,0 +1,546 @@ +{-# language ExplicitNamespaces #-} +{-# language MultiWayIf #-} +{-# language TemplateHaskellQuotes #-} + +-- | Main module of @kind-generics-th@. +-- Please refer to the @README@ file for documentation on how to use this package. +module Generics.Kind.TH (deriveGenericK) where + +import Control.Applicative +import Control.Monad +import qualified Data.Kind as Kind +import Data.List +import Data.Maybe +import Data.Type.Equality (type (~~)) +import Generics.Kind +import GHC.Generics as Generics hiding (conIsRecord, conName, datatypeName) +import Language.Haskell.TH as TH +import Language.Haskell.TH.Datatype as THAbs + +-- | Given the 'Name' of a data type (or, the 'Name' of a constructor belonging +-- to a data type), generate 'GenericK' instances for that data type. You will +-- likely need to enable most of these language extensions in order for GHC to +-- accept the generated code: +-- +-- * @DataKinds@ +-- +-- * @EmptyCase@ (if using an empty data type) +-- +-- * @FlexibleInstances@ +-- +-- * @MultiParamTypeClasses@ +-- +-- * @PolyKinds@ (if using a poly-kinded data type) +-- +-- * @TemplateHaskell@ +-- +-- * @TypeFamilies@ +deriveGenericK :: Name -> Q [Dec] +deriveGenericK n = do + DatatypeInfo{ datatypeName = dataName + , datatypeVars = univVars + , datatypeVariant = variant + , datatypeCons = cons + } <- reifyDatatype n + cons' <- traverse resolveConSynonyms cons + let deriveInsts :: [Type] -> [Type] -> Q [Dec] + deriveInsts argsToKeep argsToDrop = do + inst <- deriveGenericKFor argsToKeep argsToDrop + case argsToKeep of + [] -> pure [inst] + (argToDrop:argsToKeep') -> do + argToDrop' <- resolveTypeSynonyms argToDrop + if | -- Can the argument to drop be eta-reduced? + Just argNameToDrop <- distinctTyVarType (freeVariables argsToKeep') + argToDrop' + -- Check for dependent quantification, which we currently can't handle. + , argNameToDrop `notElem` + freeVariables (map typeKind argsToDrop + ++ map tvKind (gatherExistentials cons')) + -> do let allInnerTypes = gatherConstraints cons' ++ gatherFields cons' + -- Check if the argument appears in a type family application. + inTyFamApp <- or <$> traverse (isInTypeFamilyApp argNameToDrop) + allInnerTypes + if inTyFamApp + then pure [inst] + else (inst:) <$> deriveInsts argsToKeep' (argToDrop':argsToDrop) + | otherwise + -> pure [inst] + + -- Generate a single GenericK instance for a given set of data type + -- arguments and indexed arguments. + deriveGenericKFor :: [Type] -> [Type] -> Q Dec + deriveGenericKFor argsToKeep argsToDrop = do + let argNamesToDrop = map varTToName argsToDrop + kind = foldr (\x y -> ArrowT `AppT` x `AppT` y) + (ConT ''Kind.Type) (map typeKind argsToDrop) + dataApp = pure $ SigT (foldr (flip AppT) (ConT dataName) argsToKeep) kind + instanceD (pure []) + (conT ''GenericK `appT` dataApp `appT` + foldr (\x y -> infixT x '(:&&:) y) + (promotedT 'LoT0) (map varT argNamesToDrop)) + [ tySynInstD ''RepK $ tySynEqn [dataApp] $ + deriveRepK dataName argNamesToDrop variant cons' + , deriveFromK cons' + , deriveToK cons' + ] + + deriveInsts (reverse univVars) [] + +-- | @'distinctTyVarType' tvSet ty@ returns @'Just' tvTy@ if @ty@: +-- +-- a. Is a type variable named @tvTy@, and +-- b. @tvTy@ is not an element of @tvSet@. +-- +-- Otherwise, returns 'Nothing'. +distinctTyVarType :: [Name] -> Type -> Maybe Name +distinctTyVarType tvSet ty = do + tvTy <- varTToName_maybe ty + guard $ tvTy `notElem` tvSet + pure tvTy + +deriveRepK :: Name -> [Name] + -> DatatypeVariant -> [ConstructorInfo] -> Q Type +deriveRepK dataName univVarNames dataVariant cons = do + cons' <- traverse constructor cons + metaData $ foldBal (\x y -> InfixT x ''(:+:) y) (ConT ''V1) cons' + where + metaData :: Type -> Q Type + metaData t = do + m <- maybe (fail "Cannot fetch module name!") pure (nameModule dataName) + pkg <- maybe (fail "Cannot fetch package name!") pure (namePackage dataName) + conT ''D1 + `appT` (promotedT 'MetaData `appT` + litT (strTyLit (nameBase dataName)) `appT` + litT (strTyLit m) `appT` + litT (strTyLit pkg) `appT` + promoteBool (isNewtypeVariant dataVariant)) + `appT` pure t + + constructor :: ConstructorInfo -> Q Type + constructor ConstructorInfo{ constructorName = conName + , constructorVars = exTvbs + , constructorContext = conCtxt + , constructorFields = fields + , constructorStrictness = fieldStricts + , constructorVariant = conVariant + } = do + mbFi <- reifyFixity conName + conT ''C1 + `appT` (promotedT 'MetaCons `appT` + litT (strTyLit (nameBase conName)) `appT` + fixityIPromotedType mbFi conIsInfix `appT` + promoteBool conIsRecord) + `appT` do prod <- foldBal (\x y -> InfixT x ''(:*:) y) (ConT ''U1) <$> selectors + ctxtProd <- context prod + existentials ctxtProd + where + conIsRecord :: Bool + conIsRecord = + case conVariant of + NormalConstructor -> False + InfixConstructor -> False + RecordConstructor{} -> True + + conIsInfix :: Bool + conIsInfix = + case conVariant of + NormalConstructor -> False + InfixConstructor -> True + RecordConstructor{} -> False + + context :: Type -> Q Type + context ty = + case conCtxt of + [] -> pure ty -- Don't use (:=>:) if there are no constraints + _ -> infixT (atomizeContext conCtxt) ''(:=>:) (pure ty) + + existentials :: Type -> Q Type + existentials ty = + foldl' (\x tvb -> conT ''Exists `appT` pure (tvKind tvb) `appT` x) + (pure ty) exTvbs + + selectors :: Q [Type] + selectors = + case conVariant of + NormalConstructor -> nonRecordCase + InfixConstructor -> nonRecordCase + RecordConstructor records -> recordCase records + where + nonRecordCase :: Q [Type] + nonRecordCase = mkCase (map (const Nothing) fields) + + recordCase :: [Name] -> Q [Type] + recordCase records = mkCase (map Just records) + + mkCase :: [Maybe Name] -> Q [Type] + mkCase mbRecords = do + dcdStricts <- reifyConStrictness conName + zipWith4M selector mbRecords fieldStricts dcdStricts fields + + selector :: Maybe Name -> FieldStrictness -> TH.DecidedStrictness -> Type -> Q Type + selector mbRecord (FieldStrictness fu fs) ds field = do + let mbSelNameT = + case mbRecord of + Just record -> promotedT 'Just `appT` litT (strTyLit (nameBase record)) + Nothing -> promotedT 'Nothing + conT ''S1 + `appT` (promotedT 'MetaSel `appT` + mbSelNameT `appT` + promoteSourceUnpackedness (generifyUnpackedness fu) `appT` + promoteSourceStrictness (generifyStrictness fs) `appT` + promoteDecidedStrictness (generifyDecidedStrictness ds)) + `appT` (conT ''Field `appT` atomize field) + + atomizeContext :: Cxt -> Q Type + atomizeContext = foldBal (\x y -> infixT x '(:&:) y) + (promotedT 'Kon `appT` tupleT 0) + . map atomize + + atomize :: Type -> Q Type + atomize = go + where + go :: Type -> Q Type + -- Var case + go ty@(VarT n) = + case elemIndex n allTvbNames of + Just idx -> pure $ enumerateTyVar idx + Nothing -> kon ty + + -- Kon cases + go ty@ConT{} = kon ty + go ty@PromotedT{} = kon ty + go ty@TupleT{} = kon ty + go ty@ArrowT = kon ty + go ty@ListT = kon ty + go ty@PromotedTupleT{} = kon ty + go ty@PromotedNilT = kon ty + go ty@PromotedConsT = kon ty + go ty@StarT = kon ty + go ty@ConstraintT = kon ty + go ty@LitT{} = kon ty + go ty@WildCardT = kon ty + go ty@UnboxedTupleT{} = kon ty + go ty@UnboxedSumT{} = kon ty + go EqualityT = kon (ConT ''(~~)) + -- EqualityT can refer to both homogeneous + -- and heterogeneous equality, but TH always + -- splices EqualityT back in as if it were + -- homogeneous. To be on the safe side, always + -- conservatively assume that the equality it + -- heterogeneous, since it is more permissive. + + -- Recursive cases + go (AppT ty1 ty2) = do ty1' <- go ty1 + ty2' <- go ty2 + case (ty1', ty2') of + (PromotedT kon1 `AppT` tyArg1, + PromotedT kon2 `AppT` tyArg2) + | kon1 == 'Kon, kon2 == 'Kon + -> kon (AppT tyArg1 tyArg2) + (_, _) -> pure $ InfixT ty1' '(:@:) ty2' + go (InfixT ty1 n ty2) = go (ConT n `AppT` ty1 `AppT` ty2) + go (UInfixT ty1 n ty2) = go (ConT n `AppT` ty1 `AppT` ty2) + go (SigT ty _) = go ty + go (ParensT ty) = ParensT <$> go ty + + -- Failure case + go ty@ForallT{} = can'tRepresent "rank-n type" ty + + kon :: Type -> Q Type + kon ty = promotedT 'Kon `appT` pure ty + + can'tRepresent :: String -> Type -> Q a + can'tRepresent thing ty = fail $ "Unsupported " ++ thing ++ ": " ++ pprint ty + + allTvbNames :: [Name] + allTvbNames = map tvName exTvbs ++ univVarNames + + fixityIPromotedType :: Maybe TH.Fixity -> Bool -> Q Type + fixityIPromotedType mbFi True = + promotedT 'InfixI + `appT` promoteAssociativity (fdToAssociativity fd) + `appT` litT (numTyLit (toInteger n)) + where + Fixity n fd = fromMaybe defaultFixity mbFi + fixityIPromotedType _ False = promotedT 'PrefixI + +deriveFromK :: [ConstructorInfo] -> Q Dec +deriveFromK cons = do + x <- newName "x" + funD 'fromK + [clause [varP x] + (normalB $ conE 'M1 `appE` caseE (varE x) cases) + []] + where + cases :: [Q Match] + cases = zipWith (fromCon (length cons)) [1..] cons + + fromCon :: Int -- Total number of constructors + -> Int -- Constructor index + -> ConstructorInfo -> Q Match + fromCon n i (ConstructorInfo{ constructorName = conName + , constructorVars = exTvbs + , constructorContext = conCtxt + , constructorFields = fields + }) = do + fNames <- newNameList "f" $ length fields + match (conP conName (map varP fNames)) + (normalB $ lrE i n $ conE 'M1 `appE` + do prod <- foldBal (\x y -> infixE (Just x) (conE '(:*:)) (Just y)) + (conE 'U1) + (map fromField fNames) + ctxtProd <- context prod + existentials ctxtProd) + [] + where + fromField :: Name -> Q Exp + fromField fName = conE 'M1 `appE` (conE 'Field `appE` varE fName) + + context :: Exp -> Q Exp + context e = + case conCtxt of + [] -> pure e + _ -> conE 'SuchThat `appE` pure e + + existentials :: Exp -> Q Exp + existentials e = foldl' (\x _ -> conE 'Exists `appE` x) (pure e) exTvbs + +deriveToK :: [ConstructorInfo] -> Q Dec +deriveToK cons = do + x <- newName "x" + funD 'toK + [clause [conP 'M1 [varP x]] + (normalB $ caseE (varE x) cases) + []] + where + cases :: [Q Match] + cases = zipWith (toCon (length cons)) [1..] cons + + toCon :: Int -- Total number of constructors + -> Int -- Constructor index + -> ConstructorInfo -> Q Match + toCon n i (ConstructorInfo{ constructorName = conName + , constructorVars = exTvbs + , constructorContext = conCtxt + , constructorFields = fields + }) = do + fNames <- newNameList "f" $ length fields + match (lrP i n $ conP 'M1 + [ do prod <- foldBal (\x y -> infixP x '(:*:) y) + (conP 'U1 []) + (map toField fNames) + ctxtProd <- context prod + existentials ctxtProd + ] ) + (normalB $ foldl' appE (conE conName) (map varE fNames)) + [] + where + toField :: Name -> Q Pat + toField fName = conP 'M1 [conP 'Field [varP fName]] + + context :: Pat -> Q Pat + context p = + case conCtxt of + [] -> pure p + _ -> conP 'SuchThat [pure p] + + existentials :: Pat -> Q Pat + existentials p = foldl' (\x _ -> conP 'Exists [x]) (pure p) exTvbs + +-- | If a Type is a SigT, returns its kind signature. Otherwise, return Type. +typeKind :: Type -> Kind +typeKind (SigT _ k) = k +typeKind _ = ConT ''Kind.Type + +fdToAssociativity :: FixityDirection -> Associativity +fdToAssociativity InfixL = LeftAssociative +fdToAssociativity InfixR = RightAssociative +fdToAssociativity InfixN = NotAssociative + +generifyUnpackedness :: Unpackedness -> Generics.SourceUnpackedness +generifyUnpackedness UnspecifiedUnpackedness = Generics.NoSourceUnpackedness +generifyUnpackedness NoUnpack = Generics.SourceNoUnpack +generifyUnpackedness Unpack = Generics.SourceUnpack + +generifyStrictness :: Strictness -> Generics.SourceStrictness +generifyStrictness UnspecifiedStrictness = Generics.NoSourceStrictness +generifyStrictness Lazy = Generics.SourceLazy +generifyStrictness THAbs.Strict = Generics.SourceStrict + +generifyDecidedStrictness :: TH.DecidedStrictness -> Generics.DecidedStrictness +generifyDecidedStrictness TH.DecidedLazy = Generics.DecidedLazy +generifyDecidedStrictness TH.DecidedStrict = Generics.DecidedStrict +generifyDecidedStrictness TH.DecidedUnpack = Generics.DecidedUnpack + +promoteSourceUnpackedness :: Generics.SourceUnpackedness -> Q Type +promoteSourceUnpackedness Generics.NoSourceUnpackedness = promotedT 'Generics.NoSourceUnpackedness +promoteSourceUnpackedness Generics.SourceNoUnpack = promotedT 'Generics.SourceNoUnpack +promoteSourceUnpackedness Generics.SourceUnpack = promotedT 'Generics.SourceUnpack + +promoteSourceStrictness :: Generics.SourceStrictness -> Q Type +promoteSourceStrictness Generics.NoSourceStrictness = promotedT 'Generics.NoSourceStrictness +promoteSourceStrictness Generics.SourceLazy = promotedT 'Generics.SourceLazy +promoteSourceStrictness Generics.SourceStrict = promotedT 'Generics.SourceStrict + +promoteDecidedStrictness :: Generics.DecidedStrictness -> Q Type +promoteDecidedStrictness Generics.DecidedLazy = promotedT 'Generics.DecidedLazy +promoteDecidedStrictness Generics.DecidedStrict = promotedT 'Generics.DecidedStrict +promoteDecidedStrictness Generics.DecidedUnpack = promotedT 'Generics.DecidedUnpack + +promoteAssociativity :: Associativity -> Q Type +promoteAssociativity LeftAssociative = promotedT 'LeftAssociative +promoteAssociativity RightAssociative = promotedT 'RightAssociative +promoteAssociativity NotAssociative = promotedT 'NotAssociative + +promoteBool :: Bool -> Q Type +promoteBool True = promotedT 'True +promoteBool False = promotedT 'False + +enumerateTyVar :: Int -> Type +-- Special-case the first 10, if only to generate more compact code +enumerateTyVar 0 = ConT ''Var0 +enumerateTyVar 1 = ConT ''Var1 +enumerateTyVar 2 = ConT ''Var2 +enumerateTyVar 3 = ConT ''Var3 +enumerateTyVar 4 = ConT ''Var4 +enumerateTyVar 5 = ConT ''Var5 +enumerateTyVar 6 = ConT ''Var6 +enumerateTyVar 7 = ConT ''Var7 +enumerateTyVar 8 = ConT ''Var8 +enumerateTyVar 9 = ConT ''Var9 +enumerateTyVar n = PromotedT 'Var `AppT` nTimes n (AppT (PromotedT 'VS)) (PromotedT 'VZ) + +-- | Variant of foldr for producing balanced lists +foldBal :: (a -> a -> a) -> a -> [a] -> a +foldBal _ x [] = x +foldBal _ _ [y] = y +foldBal op x l = let (a,b) = splitAt (length l `div` 2) l + in foldBal op x a `op` foldBal op x b + +lrP :: Int -- Constructor index + -> Int -- Total number of constructors + -> Q Pat -> Q Pat +lrP i n p + | n == 0 = fail "lrP: impossible" + | n == 1 = p + | i <= div n 2 = conP 'L1 [lrP i (div n 2) p] + | otherwise = conP 'R1 [lrP (i-m) (n-m) p] + where m = div n 2 + +lrE :: Int -- Constructor index + -> Int -- Total number of constructors + -> Q Exp -> Q Exp +lrE i n e + | n == 0 = fail "lrE: impossible" + | n == 1 = e + | i <= div n 2 = conE 'L1 `appE` lrE i (div n 2) e + | otherwise = conE 'R1 `appE` lrE (i-m) (n-m) e + where m = div n 2 + +isNewtypeVariant :: DatatypeVariant -> Bool +isNewtypeVariant Datatype = False +isNewtypeVariant Newtype = True +isNewtypeVariant DataInstance = False +isNewtypeVariant NewtypeInstance = True + +-- | Extract 'Just' the 'Name' from a type variable. If the argument 'Type' is +-- not a type variable, return 'Nothing'. +varTToName_maybe :: Type -> Maybe Name +varTToName_maybe (VarT n) = Just n +varTToName_maybe (SigT t _) = varTToName_maybe t +varTToName_maybe _ = Nothing + +-- | Extract the 'Name' from a type variable. If the argument 'Type' is not a +-- type variable, throw an error. +varTToName :: Type -> Name +varTToName = fromMaybe (error "Not a type variable!") . varTToName_maybe + +zipWith4M :: Monad m => (a -> b -> c -> d -> m e) + -> [a] -> [b] -> [c] -> [d] -> m [e] +zipWith4M _ [] _ _ _ = pure [] +zipWith4M _ _ [] _ _ = pure [] +zipWith4M _ _ _ [] _ = pure [] +zipWith4M _ _ _ _ [] = pure [] +zipWith4M f (x:xs) (y:ys) (z:zs) (a:as) + = do r <- f x y z a + rs <- zipWith4M f xs ys zs as + pure $ r:rs + +-- | Compose a function with itself n times. (nth rather than twice) +nTimes :: Int -> (a -> a) -> (a -> a) +nTimes 0 _ = id +nTimes 1 f = f +nTimes n f = f . nTimes (n-1) f + +-- | Generate a list of fresh names with a common prefix, and numbered suffixes. +newNameList :: String -> Int -> Q [Name] +newNameList prefix n = traverse (newName . (prefix ++) . show) [1..n] + +gatherExistentials :: [ConstructorInfo] -> [TyVarBndr] +gatherExistentials = concatMap constructorVars + +gatherConstraints :: [ConstructorInfo] -> [Pred] +gatherConstraints = concatMap constructorContext + +gatherFields :: [ConstructorInfo] -> [Type] +gatherFields = concatMap constructorFields + +-- | Detect if a name occurs as an argument to some type family. +isInTypeFamilyApp :: Name -> Type -> Q Bool +isInTypeFamilyApp name = go + where + go :: Type -> Q Bool + go ty@AppT{} = case splitAppTs ty of + (tyFun, tyArgs) + | ConT tcName <- tyFun + -> goTyConApp tcName tyArgs + | otherwise + -> or <$> traverse go (tyFun:tyArgs) + go (InfixT ty1 n ty2) = go (ConT n `AppT` ty1 `AppT` ty2) + go (SigT ty ki) = liftA2 (||) (go ty) (go ki) + go (ParensT ty) = go ty + go _ = pure False + + goTyConApp :: Name -> [Type] -> Q Bool + goTyConApp tcName tcArgs = do + info <- reify tcName + case info of + FamilyI (OpenTypeFamilyD (TypeFamilyHead _ bndrs _ _)) _ + -> withinFirstArgs bndrs + FamilyI (ClosedTypeFamilyD (TypeFamilyHead _ bndrs _ _) _) _ + -> withinFirstArgs bndrs + _ -> pure False + where + withinFirstArgs :: [a] -> Q Bool + withinFirstArgs bndrs = + let firstArgs = take (length bndrs) tcArgs + in pure $ name `elem` freeVariables firstArgs + +-- | Split a chain of 'AppT's to a linear chain of arguments. +splitAppTs :: Type -> (Type, [Type]) +splitAppTs ty = split ty ty [] + where + split :: Type -> Type -> [Type] -> (Type, [Type]) + split _ (AppT ty1 ty2) args = split ty1 ty1 (ty2:args) + split origTy (InfixT ty1 n ty2) args = split origTy (ConT n `AppT` ty1 `AppT` ty2) args + split origTy (SigT ty' _) args = split origTy ty' args + split origTy (ParensT ty') args = split origTy ty' args + split origTy _ args = (origTy, args) + +-- | Resolve all of the type synonyms in a 'ConstructorInfo'. +resolveConSynonyms :: ConstructorInfo -> Q ConstructorInfo +resolveConSynonyms con@(ConstructorInfo{ constructorVars = vars + , constructorContext = context + , constructorFields = fields + }) = do + vars' <- traverse (\tvb -> + case tvb of + PlainTV{} -> pure tvb + KindedTV n k -> KindedTV n <$> resolveTypeSynonyms k) vars + context' <- traverse resolveTypeSynonyms context + fields' <- traverse resolveTypeSynonyms fields + pure $ con{ constructorVars = vars' + , constructorContext = context' + , constructorFields = fields' + } diff --git a/tests/Main.hs b/tests/Main.hs new file mode 100644 --- /dev/null +++ b/tests/Main.hs @@ -0,0 +1,135 @@ +{-# language AllowAmbiguousTypes #-} +{-# language DataKinds #-} +{-# language EmptyCase #-} +{-# language FlexibleInstances #-} +{-# language GADTs #-} +{-# language MultiParamTypeClasses #-} +{-# language PolyKinds #-} +{-# language ScopedTypeVariables #-} +{-# language TemplateHaskell #-} +{-# language TypeApplications #-} +{-# language TypeFamilies #-} +{-# language TypeOperators #-} +{-# options_ghc -Wno-orphans #-} +module Main (main) where + +import Data.Kind +import Data.Proxy +import Generics.Kind +import Generics.Kind.TH + +main :: IO () +main = + let insts = [ -- Representation types + isGenericK @_ @(V1 _) @'LoT0 + , isGenericK @_ @V1 @(_ ':&&: 'LoT0) + + , isGenericK @_ @((:+:) _ _ _) @'LoT0 + , isGenericK @_ @((:+:) _ _) @(_ ':&&: 'LoT0) + , isGenericK @_ @((:+:) _) @(_ ':&&: _ ':&&: 'LoT0) + , isGenericK @_ @(:+:) @(_ ':&&: _ ':&&: _ ':&&: 'LoT0) + + , isGenericK @_ @((:*:) _ _ _) @'LoT0 + , isGenericK @_ @((:*:) _ _) @(_ ':&&: 'LoT0) + , isGenericK @_ @((:*:) _) @(_ ':&&: _ ':&&: 'LoT0) + , isGenericK @_ @(:*:) @(_ ':&&: _ ':&&: _ ':&&: 'LoT0) + + , isGenericK @_ @(U1 _) @'LoT0 + , isGenericK @_ @U1 @(_ ':&&: 'LoT0) + + , isGenericK @_ @(M1 _ _ _ _) @'LoT0 + , isGenericK @_ @(M1 _ _ _) @(_ ':&&: 'LoT0) + , isGenericK @_ @(M1 _ _) @(_ ':&&: _ ':&&: 'LoT0) + , isGenericK @_ @(M1 _) @(_ ':&&: _ ':&&: _ ':&&: 'LoT0) + , isGenericK @_ @M1 @(_ ':&&: _ ':&&: _ ':&&: _ ':&&: 'LoT0) + + , isGenericK @_ @(Field _ _) @'LoT0 + + , isGenericK @_ @((:=>:) _ _ _) @'LoT0 + + , isGenericK @_ @(Exists _ _ _) @'LoT0 + , isGenericK @_ @(Exists _ _) @(_ ':&&: 'LoT0) + , isGenericK @_ @(Exists _) @(_ ':&&: _ ':&&: 'LoT0) + + -- Other data types + , isGenericK @_ @(LoT _) @'LoT0 + , isGenericK @_ @LoT @(_ ':&&: 'LoT0) + + , isGenericK @_ @TyEnv @'LoT0 + + -- Data families + , isGenericK @_ @(DF Char Int _) @'LoT0 + , isGenericK @_ @(DF Char Int) @(_ ':&&: 'LoT0) + + , isGenericK @_ @(DF () () _) @'LoT0 + , isGenericK @_ @(DF () ()) @(_ ':&&: 'LoT0) + + , isGenericK @_ @(DF Bool () (Maybe _)) @'LoT0 + + -- Tricky cases + , isGenericK @_ @(TC1 _) @'LoT0 + , isGenericK @_ @TC1 @(_ ':&&: 'LoT0) + + , isGenericK @_ @(TC2 _) @'LoT0 + , isGenericK @_ @TC2 @(_ ':&&: 'LoT0) + + , isGenericK @_ @(TC3 _ _) @'LoT0 + , isGenericK @_ @(TC3 _) @(_ ':&&: 'LoT0) + + , isGenericK @_ @(TC4 _) @'LoT0 + , isGenericK @_ @TC4 @(_ ':&&: 'LoT0) + + , isGenericK @_ @(TC5 _) @'LoT0 + ] + in insts `seq` pure () + +isGenericK :: forall k (f :: k) (x :: LoT k). GenericK f x => () +isGenericK = fromK @k @f @x `seq` () + +---------------- +-- Data families +---------------- + +data family DF a b c +data instance DF Char Int c = DF1 c +data instance DF a a c = DF2 a c +data instance DF Bool () (Maybe c) = DF3 c + +--------------- +-- Tricky cases +--------------- + +-- An existential context with multiple constraints +data TC1 :: Type -> Type where + MkTC1 :: forall a. (Eq a, Read a, Show a) => TC1 a + +-- A kind variable being used as a type variable +data TC2 :: forall k. k -> Type where + MkTC2 :: forall k (a :: k). k -> Proxy a -> TC2 a + +-- Visible dependent quantification +data TC3 k :: k -> Type where + MkTC3 :: forall k (a :: k). k -> Proxy a -> TC3 k a + +-- This sort of type family is OK to partially apply +type family UnsaturateMe :: Type -> Type +newtype TC4 :: Type -> Type where + MkTC4 :: forall a. UnsaturateMe a -> TC4 a + +-- Tricky kind inference involving Proxy +data TC5 :: Type -> Type where + MkTC5 :: forall k (a :: k). k -> Proxy a -> TC5 k + +$(concat <$> traverse deriveGenericK + [ -- Representation types + ''V1, ''(:+:), ''(:*:), ''U1, ''M1, ''Field, ''(:=>:), ''Exists + + -- Other data types + , ''LoT, ''TyEnv + + -- Data families + , 'DF1, 'DF2, 'DF3 + + -- Tricky cases + , ''TC1, ''TC2, ''TC3, ''TC4, ''TC5 + ])