kind-generics-th (empty) → 0.1.0.0
raw patch · 6 files changed
+911/−0 lines, 6 filesdep +basedep +kind-genericsdep +kind-generics-thsetup-changed
Dependencies added: base, kind-generics, kind-generics-th, template-haskell, th-abstraction
Files
- LICENSE +30/−0
- README.md +157/−0
- Setup.hs +2/−0
- kind-generics-th.cabal +41/−0
- src/Generics/Kind/TH.hs +546/−0
- tests/Main.hs +135/−0
+ LICENSE view
@@ -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.
+ README.md view
@@ -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`.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ kind-generics-th.cabal view
@@ -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
+ src/Generics/Kind/TH.hs view
@@ -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'+ }
+ tests/Main.hs view
@@ -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+ ])