packages feed

fcf-family (empty) → 0.1.0.0

raw patch · 8 files changed

+805/−0 lines, 8 filesdep +basedep +containersdep +fcf-family

Dependencies added: base, containers, fcf-family, first-class-families, template-haskell

Files

+ CHANGELOG.md view
@@ -0,0 +1,5 @@+# Revision history for fcf-family++## 0.1.0.0 -- 2023-01-23++* First version. Released on an unsuspecting world.
+ LICENSE view
@@ -0,0 +1,20 @@+Copyright (c) 2022 Li-yao Xia++Permission is hereby granted, free of charge, to any person obtaining+a copy of this software and associated documentation files (the+"Software"), to deal in the Software without restriction, including+without limitation the rights to use, copy, modify, merge, publish,+distribute, sublicense, and/or sell copies of the Software, and to+permit persons to whom the Software is furnished to do so, subject to+the following conditions:++The above copyright notice and this permission notice shall be included+in all copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.+IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY+CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,+TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE+SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ README.md view
@@ -0,0 +1,91 @@+# Family of families: featherweight defunctionalization++## Motivation++This package transforms regular type families into+["first-class families"](https://hackage.haskell.org/package/first-class-families).+It does so without declaring dummy data types as defunctionalization symbols,+avoiding namespace pollution.++### Featherweight defunctionalization++The idea is to use strings. There is an unambiguous way to refer to an existing type family:+by its fully qualified name---a triple of a package name, module name, and base name.++```haskell+GHC.TypeNats.++-- as a Name --+MkName "base" "GHC.TypeNats" "+"+```++All type families can be promoted to first-class using a single symbol indexed by+qualified names. That is the `Family` of type families.++- No namespace pollution: Promoting a type family requires no new data type,+  only an `Eval` instance for its name.+- Decentralization: Every type family induces a unique `Eval` instance,+  and multiple packages may declare the same instance without conflicts.++```haskell+type instance Eval (Family_ (MkName "base" "GHC.TypeNats" "+") _ '(x, '(y, '()))) = x + y+```++For more details on this encoding, see the module `Fcf.Family`.++## Usage++### Promote a type family++To promote a type family, the necessary boilerplate+can be generated with Template Haskell, using the function `Fcf.Family.TH.fcfify`.++```haskell+fcfify ''MyTypeFamily++-- Examples+fcfify ''(GHC.TypeNats.+)+fcfify ''Data.Type.Bool.If+```++This generates instances of `Eval` and auxiliary type families for that former+instance to be well-defined.++### Use the promoted type family++This allows using the defunctionalization symbol `Family` indexed by the+type family's name---a tuple of strings constructed with `MkName`.++```haskell+  Eval (Family (MkName "base" "GHC.TypeNats" "+") P0 '(1, '(2, '())))+= 1 + 2+= 3++  Eval (Family (MkName "base" "GHC.Type.Bool" "If") P1 '( 'True, '("yes", '("no", '()))))+= If 'True "yes" "no"+= "yes"+```++The `familyName` function converts the name of an actual family to an *fcf-family* name in Template Haskell.++```haskell+  Eval (Family $(familyName ''+) P0 '(1, '(2, '())))+= 3++  Eval (Family $(familyName ''If) P1 '( 'True, '("yes", '("no", '()))))+= "yes"+```++## Existing instances++- The library [`fcf-base`](https://hackage.haskell.org/package/fcf-base) contains instances for type families defined in *base*.+- The module `Fcf.Family.Meta` contains the instance for `Eval`.++## Limitations++- There is partial support for dependently typed type families.+  The kind of the result may depend on its arguments.+  This package does not yet support type families where the kind of arguments+  depends on other visible arguments.+- Invisible arguments are currently all assumed to be of kind `Type`.+  Lifting this restriction requires either access to more typing information+  from the compiler via TH, or some implementation of kind inference in TH.
+ fcf-family.cabal view
@@ -0,0 +1,46 @@+cabal-version:      3.0+name:               fcf-family+version:            0.1.0.0+synopsis: Family of families: featherweight defunctionalization+description:+  Promote regular type families to first-class,+  without polluting the type namespace.+  .+  See README.+homepage:           https://gitlab.com/lysxia/fcf-family+license:            MIT+license-file:       LICENSE+author:             Li-yao Xia+maintainer:         lysxia@gmail.com+category:           Other+build-type:         Simple+extra-doc-files:    CHANGELOG.md, README.md+tested-with: GHC == { 9.0.2, 9.2.2, 9.4.1 }++common warnings+    ghc-options: -Wall++library+    import:           warnings+    exposed-modules:+      Fcf.Family+      Fcf.Family.Meta+      Fcf.Family.TH+    build-depends:+      first-class-families,+      containers,+      template-haskell,+      base >=4.15 && < 4.20+    hs-source-dirs:   src+    default-language: Haskell2010++test-suite fcf-family-test+    import:           warnings+    default-language: Haskell2010+    type:             exitcode-stdio-1.0+    hs-source-dirs:   test+    main-is:          Main.hs+    build-depends:+        base,+        first-class-families,+        fcf-family
+ src/Fcf/Family.hs view
@@ -0,0 +1,301 @@+{-# LANGUAGE+  AllowAmbiguousTypes,+  DataKinds,+  PolyKinds,+  RankNTypes,+  ScopedTypeVariables,+  StandaloneKindSignatures,+  TypeFamilies,+  TypeOperators,+  UndecidableInstances #-}++-- |+-- Description: The family of type families+--+-- = The family of type families+--+-- /fcf-family/ promotes+-- regular type families to first-class families without+-- defining new symbols (which would either pollute the type namespace+-- or require a centralized organization to decide where the symbol+-- for each family should be defined).+--+-- Every type family is uniquely identified by its qualified 'Name':+-- package, module, and base name.+--+-- Example names:+--+-- @+-- -- GHC.TypeNats.++-- 'MkName' \"base\" \"GHC.TypeNats\" \"+\"+--+-- -- Data.Type.Bool.If+-- 'MkName' \"base\" \"Data.Type.Bool\" \"If\"+-- @+--+-- Hence, a single symbol 'Family' indexed by names+-- is sufficient to promote all regular type families.+--+-- == Promoting a type family to first-class+--+-- For example, the type family @('GHC.TypeNats.+')@ is promoted using the following+-- 'Eval' instance for 'Family':+--+-- @+-- type (::+) = 'MkName' \"base\" \"GHC.TypeNats\" \"+\" -- 'Name' of (+)+-- type instance 'Eval' ('Family_' (::+) _ '(x, '(y, '())))) = x 'GHC.TypeNats.+' y+-- @+--+-- The necessary instances can be generated using 'Fcf.Family.TH.fcfify' from the+-- module "Fcf.Family.TH".+--+-- @+-- 'Fcf.Family.TH.fcfify' \'\'++-- @+--+-- The name of the family can be quoted using 'Fcf.Family.TH.familyName'.+--+-- @+-- type (::+) = $(pure ('Fcf.Family.TH.familyName' \'\'+))+-- @+--+-- Two modules may invoke 'Fcf.Family.TH.fcfify' on the same name without conflict.+-- Identical type family instances will be generated, which is allowed.+--+-- Examples:+--+-- @+-- 2 'GHC.TypeNats.+' 3+-- ~+-- 'Eval' ('Family' ('MkName' \"base\" \"GHC.TypeNats\" \"+\") 'P0' '(2, '(3, '())))+-- @+--+-- @+-- 'Data.Type.Bool.If' a b c+-- ~+-- 'Eval' ('Family' ('MkName' \"base\" \"Data.Type.Bool\" \"If\") 'P1' '(a, '(b, '(c, \()))))+-- @+--+-- == Details+--+-- The type of 'Family' is an uncurried version of the original type family:+--+-- @+-- 'Family' (::+) _ :: (Nat, (Nat, ())) -> Exp Nat+-- ('GHC.TypeNats.+') :: Nat -> Nat -> Nat+-- @+--+-- Tuples @(,)@ and @()@ are used as the cons and nil of heterogeneous lists of arguments.+--+-- The signature of the relevant family is encoded by implementing the following+-- type instances:+--+-- @+-- -- Auxiliary instances.+-- type instance 'Params' (::+) = ()+-- type instance 'Args_' (::+) _ = (Nat, (Nat, ()))+-- type instance 'Res_' (::+) _ _ = Nat+-- @+--+-- 'Args_' and 'Res_' denote the types of arguments and result of the given type family.+-- 'Params' denotes the type of implicit parameters (there are none here+-- since @('GHC.TypeNats.+')@ is monomorphic).+-- The type of explicit arguments ('Args_') may depend on the implicit parameters ('Params').+-- The result type ('Res_') may depend on both 'Params' and 'Args_'.+--+-- === Untyped inside, typed outside  #wrappers#+--+-- These families are intended to be very dependent (the type of 'Family' depends on 'Res' depends on 'Args' depends on 'Params').+-- However, the implementation of this library must work around some technical limitations of GHC.+-- 'Args_' and 'Res_' are actually "untyped" to make GHC more lenient in type+-- checking their instances. \"Typed\" wrappers, 'Family', 'Res', 'Args' are+-- then provided to invoke those families with their intended types,+-- which allows type inference to work.+--+-- To recap: define instances of 'Params', 'Args_', 'Res_', 'Family_',+-- but to invoke the latter three, use 'Args', 'Res', and 'Family' instead.+--+-- == Implicit parameters+--+-- An example using implicit parameters is @'Data.Type.Bool.If' :: forall k. Bool -> k -> k -> k@.+--+-- @+-- type If_ = 'MkName' \"base\" \"Data.Type.Bool\" \"If\"+-- type instance 'Eval' ('Family_' If_ _ '(b, '(x, '(y, '())))) = 'Data.Type.Bool.If' b x y+--+-- type instance 'Params' If_ = ('Data.Kind.Type', ())  -- Type of the implicit parameter+-- type instance 'Args_' If_ k = (Bool, (k, (k, ())      -- Types of the explicit arguments+-- type instance 'Res_' If_ k _ = k                      -- Type of the result+-- @+--+-- The second argument of 'Family_' is a proxy that carries the implicit parameters+-- in its type. For example, the type of @'Family' If_@ is really:+--+-- @+-- 'Family' If_ (_ :: Proxy k) :: (Bool, (k, (k, ()))) -> k+-- @+--+-- When using 'Family', apply it to a proxy encoding the number of implicit parameters+-- in unary using 'P0' and 'PS'.+--+-- For example, use 'P0' for the monomorphic @('GHC.TypeNats.+')@+-- and 'P1' (equal to @'PS' 'P0'@) for 'Data.Type.Bool.If'.++module Fcf.Family+  ( -- * Main definitions++    -- ** First-class families+    -- $reexport+    Exp+  , Eval++    -- ** Family of families+  , Name(..)+  , Family+  , Family_+  , NDFamily+  , NDFamily_++    -- ** Encoding type family signatures+    -- $arity+  , Params+  , Args+  , Args_+  , Res+  , Res_++    -- * Implicit parameters+    -- $tuples+  , ParamsProxy+  , P0, P1, P2, P3, P4, P5, P6, P7+  , PS++    -- * Coercions+    -- $hack+  , Coerce, CoerceTo, CoerceFrom+  , Transp+  ) where++import Data.Kind (Type)+import Data.Proxy (Proxy(..))+import Data.Type.Equality ((:~:)(..))+import GHC.Exts (Any)+import GHC.TypeLits (Symbol)++import Fcf.Core++-- $reexport+-- Reexported from <https://hackage.haskell.org/package/first-class-families first-class-families>.++-- | Qualified name of a type family or type synonym.+data Name = MkName+              Symbol  -- ^ Package name+              Symbol  -- ^ Module name+              Symbol  -- ^ Type name++-- | A general defunctionalization symbol for promoted type families.+-- It encodes saturated applications of type families.+--+-- The second argument (@proxy :: 'ParamsProxy' name ks@) is a gadget+-- carrying implicit parameters (if any). When invoking 'Family', it must be applied to+-- a @proxy@ that corresponds to its number of implicit parameters:+-- 'P0', 'P1', 'P2', ..., 'P7', or a unary encoding using 'P0' and 'PS' for larger implicit arities.+-- (This really matters for arity 2 and more.)+--+-- === __Implementation note__+--+-- This module makes heavy use of dependently typed type families.+-- There is <https://gitlab.haskell.org/ghc/ghc/-/issues/12088 a longstanding issue>+-- which severely limits the usability of such families when done naively.+--+-- The workaround used here is to make the type families themselves "untyped",+-- and wrap them within "typed" synonyms.+--+-- Making the families untyped makes GHC more lenient so that it accepts them.+-- Making the wrappers typed recovers the type inference behavior of the original family.+-- For instance, when using 'Data.Type.Bool.If', one would expect to unify+-- the types of its two branches. That is the case when constructing its+-- defunctionalization symbol using 'Family' and not with 'Family_'.+type Family :: forall (name :: Name) -> forall (ks :: Params name). ParamsProxy name ks -> forall (args :: Args name ks) -> Exp (Res name ks args)+type Family name proxy args = Family_ name proxy args++-- | Non-dependently typed family.+type NDFamily :: forall (name :: Name) -> forall (ks :: Params name). ParamsProxy name ks -> Args name ks -> Exp (Res name ks Any)+type NDFamily name proxy = NDFamily_ name proxy Refl++-- | Untyped internals of 'NDFamily'.+data NDFamily_ :: forall (name :: Name) -> forall (ks :: Params name). ParamsProxy name ks -> Res name ks Any :~: r -> Args name ks -> Exp r+type instance Eval (NDFamily_ name proxy e args) = Transp e (Eval (Coerce (Family name proxy args)))++-- | Untyped internals of 'Family'+data Family_ :: Name -> Proxy ks -> args -> Exp res++-- $arity+-- Parameters should be collected in a heterogeneous list made of @()@ and @(,)@.+--+-- - 0: @()@+-- - 1: @(a, ())@+-- - 2: @(a, (b, ()))@+-- - 3: @(a, (b, (c, ())))@+-- - etc.++-- | Type of implicit parameters of the named family.+type family Params (name :: Name) :: Type++-- | Type of explicit parameters of the named family.+type Args (name :: Name) (ks :: Params name) = Args_ name ks++-- | Untyped internals of 'Args'+type family Args_ (name :: Name) (ks :: ksT) :: Type++-- | Type of result of the named family.+type Res (name :: Name) (ks :: Params name) (args :: Args name ks) = Res_ name ks args++-- | Untyped internals of 'Res'+type family Res_ (name :: Name) (ks :: ksT) (args :: argsT) :: Type++-- * Implicit parameters++-- $tuples+-- We want implicit parameters of polykinded type families to remain implicit+-- in their promotion.+--+-- In 'Family', the parameters are collected in a tuple. To help type inference+-- when using a promoted type family, we instantiate the spine of the tuple+-- using the following proxies.++-- | Synonym to make explicit the dependency of the type of the+-- implicit parameters @ks@ on the @name@ of the family.+type ParamsProxy (name :: Name) (ks :: Params name) = Proxy ks++type P0 = ('Proxy :: Proxy '())+type P1 = PS P0+type P2 = PS P1+type P3 = PS P2+type P4 = PS P3+type P5 = PS P4+type P6 = PS P5+type P7 = PS P6++type PS (p :: Proxy ks) = ('Proxy :: Proxy '(k, ks))++-- * Coercions++-- $hack These coercions are part of hacks to work around some limitations in GHC.++-- | Sometimes GHC doesn't see that two type-level values are equal when they+-- ought to be equal. 'Coerce' lets us postpone the check to another day.+type Coerce :: forall k l. k -> l+type family Coerce (a :: k) :: l where+  Coerce x = x++-- | 'Coerce' with explicit codomain.+type CoerceTo l (a :: k) = (Coerce a :: l)++-- | 'Coerce' with explicit domain.+type CoerceFrom k (a :: k) = Coerce a++-- | Transport: coercion along an equality.+type Transp :: forall k l. k :~: l -> k -> l+type family Transp (e :: k :~: l) (x :: k) :: l where+  Transp (_ :: k :~: k) x = x
+ src/Fcf/Family/Meta.hs view
@@ -0,0 +1,13 @@+{-# LANGUAGE DataKinds, PolyKinds, TemplateHaskell, TypeFamilies #-}+-- {-# OPTIONS_GHC -ddump-splices #-}++-- | 'Eval' and friends as part of the family of families.+module Fcf.Family.Meta () where++import Fcf.Family+import Fcf.Family.TH (fcfify)++fcfify ''Eval+fcfify ''Params+-- fcfify ''Args+-- fcfify ''Res
+ src/Fcf/Family/TH.hs view
@@ -0,0 +1,279 @@+{-# LANGUAGE+  CPP,+  ConstraintKinds,+  ImplicitParams,+  TemplateHaskell #-}++-- | Template Haskell script to promote a type family to first class.+module Fcf.Family.TH+  ( -- * Generate boilerplate+    fcfify++    -- * Using promoted families+  , promoteFamily+  , promoteNDFamily+  , familyName+  , applyFamily+  , consTuple+  , paramsProxy++    -- * Predicates+  , isTypeFamily+  , isTypeSynonym+  , isTypeFamilyOrSynonym+  ) where++import Control.Applicative (liftA2)+import Data.Function (on)+import Data.List (sort)+import Data.Maybe (fromMaybe)+import Data.Foldable (foldl')+import Data.Traversable (for)+import qualified Data.Set as Set+import Language.Haskell.TH++import Fcf.Core+import Fcf.Family hiding (Name)++-- | Generate the boilerplate needed to promote a type family to first class.+--+-- See "Fcf.Family" for details on the encoding.+fcfify :: Name -> Q [Dec]+fcfify name = reifyTyInfo name >>= fcfifyInfo+  where+    ?funName = "fcfify"+    ?name = name++-- | Get the quoted fcf 'Fcf.Core.Family.Name' of an existing type family.+familyName :: Name -> Type+familyName name = PromotedT 'MkName+  `AppT` lit (fromMaybe "" (namePackage name))+  `AppT` lit (fromMaybe "" (nameModule name))+  `AppT` lit (nameBase name)+  where lit = LitT . StrTyLit++-- | Promote a fcfified family, returning its partially applied 'Family' and+-- its arity. The result can be applied to a 'consTuple' of the appropriate size,+promoteFamily :: Name -> Q (Type, Int)+promoteFamily = promoteFamily_ ''Family++-- | Promote a fcfified family, returning its partially applied 'Family' and+-- its arity. The result can be applied to a 'consTuple' of the appropriate size,+promoteNDFamily :: Name -> Q (Type, Int)+promoteNDFamily = promoteFamily_ ''NDFamily++promoteFamily_ :: Name -> Name -> Q (Type, Int)+promoteFamily_ _Family name = do+  info <- reifyTyInfo name+  let arity = length (tiArgs info)+  pure (ConT _Family `AppT` tiNameT info `AppT` paramsProxy' info, arity)+  where+    ?funName = "promoteFamily_"++-- | Apply a promoted family.+--+-- If there are more arguments than the arity of the family (as returned by 'promoteFamily'),+-- they are split and applied properly:+-- the family's main arguments are collected in a 'consTuple' and+-- the rest are applied with 'AppT'.+--+-- If there are fewer arguments than the arity, the result is nonsense.+applyFamily :: Name -> [Q Type] -> Q Type+applyFamily name argsQ = do+  (fam, arity) <- promoteFamily name+  (args1, args2) <- splitAt arity <$> sequenceA argsQ+  pure (fam `AppT` consTuple args1 `appsT` args2)++paramsProxy :: Name -> Q Type+paramsProxy name = paramsProxy' <$> reifyTyInfo name+  where+    ?funName = "paramsProxy"++paramsProxy' :: TyInfo -> Type+paramsProxy' info = go (length (tiParams info))+  where+    go 0 = ConT ''P0+    go n = ConT ''PS `AppT` go (n-1)++reifyTyInfo :: (?funName :: String) => Name -> Q TyInfo+reifyTyInfo name = do+  let ?name = name+  info <- reify name+  case info of+    FamilyI dec _ -> reifyTyInfoDec dec+    TyConI dec -> reifyTyInfoDec dec+    _ -> errorNotType++-- | 'True' if it is a type family (open or closed).+isTypeFamily :: Name -> Q Bool+isTypeFamily name = isTypeFamilyInfo <$> reify name++-- | 'True' if it is a type synonym.+isTypeSynonym :: Name -> Q Bool+isTypeSynonym name = isTypeSynonymInfo <$> reify name++-- | 'True' if it is a type family or synonym.+isTypeFamilyOrSynonym :: Name -> Q Bool+isTypeFamilyOrSynonym name = liftA2 (||) isTypeFamilyInfo isTypeSynonymInfo <$> reify name++isTypeFamilyInfo :: Info -> Bool+isTypeFamilyInfo (FamilyI (OpenTypeFamilyD _) _) = True+isTypeFamilyInfo (FamilyI (ClosedTypeFamilyD _ _) _) = True+isTypeFamilyInfo _ = False++isTypeSynonymInfo :: Info -> Bool+isTypeSynonymInfo (TyConI (TySynD _ _ _)) = True+isTypeSynonymInfo _ = False++--++type ErrCtxt = (?funName :: String, ?name :: Name)++errorNotType :: ErrCtxt => Q a+errorNotType = fail (?funName ++ ": unexpected name, " ++ show ?name ++ " is not a type family or type synonym.")++-- Example:+--+-- @+-- -- Input+-- type F a b c = (...)+--+-- -- Output+-- type instance Params F +-- @++reifyTyInfoDec :: ErrCtxt => Dec -> Q TyInfo+reifyTyInfoDec (TySynD name args _) = mkInfoHead name args StarT -- TODO: don't assume result kind is Type+reifyTyInfoDec (OpenTypeFamilyD t) = reifyTyInfoTFH t+reifyTyInfoDec (ClosedTypeFamilyD t _) = reifyTyInfoTFH t+reifyTyInfoDec _ = errorNotType++reifyTyInfoTFH :: ErrCtxt => TypeFamilyHead -> Q TyInfo+reifyTyInfoTFH (TypeFamilyHead name args resSig _) = do+  res <- getRes resSig+  mkInfoHead name args res++getRes :: ErrCtxt => FamilyResultSig -> Q Type+getRes NoSig = fail (?funName ++ ": implicit result type not supported")+getRes (KindSig k) = pure k+getRes (TyVarSig (KindedTV _ _ k)) = pure k+getRes (TyVarSig PlainTV{}) = fail (?funName ++ ": implicit result type not supported")++--++mkInfoHead :: Name -> [TyVarBndr ()] -> Type -> Q TyInfo+mkInfoHead name args res = do+  args' <- for args (\arg -> case arg of+    PlainTV _ _ -> fail "unexpected unnanotated arguments"  -- as far as I understand, the binders given by reify are always annotated so this shouldn't happen+    KindedTV v _ k -> pure (v, k))+  let params = collectParams args' res+  pure (mkTyInfo name params args' res)++collectParams :: [(Name, Type)] -> Type -> [Name]+collectParams args res = collect Set.empty args where++  collect bound [] = snd (addVars bound [] (getVars res))  -- collect parameters from the result type+  collect bound ((v, k) : vs) =+    let (bound', ws) = addVars bound [] (getVars k) in+    ws ++ collect (Set.insert v bound') vs++  addVars bound ws [] = (bound, reverse ws)+  addVars bound ws (x : xs)+    | Set.member x bound = addVars bound ws xs+    | otherwise = addVars (Set.insert x bound) (x : ws) xs++data TyInfo = TyInfo+  { tiName :: Name+  , tiNameT :: Type     -- ^ Encoding of name as a 'Name'+  , tiParams :: [Name]+  , tiParamsT :: Type   -- ^ Params as a tuple+  , tiArgs :: [(Name, Type)]+  , tiArgsT :: Type+  , tiRes :: Type+  }++appsT :: Type -> [Type] -> Type+appsT = foldl' AppT++mkTyInfo :: Name -> [Name] -> [(Name, Type)] -> Type -> TyInfo+mkTyInfo name params args res = TyInfo+  { tiName = name+  , tiNameT = familyName name+  , tiParams = params+  , tiParamsT = consTuple (VarT <$> params)+  , tiArgs = args+  , tiArgsT = consTuple (uncurry (SigT . VarT) <$> args)+  , tiRes = res+  }++-- | Construct a tuple suitable for a 'Family' argument.+consTuple :: [Type] -> Type+consTuple = consTuple_ (PromotedTupleT 2) (PromotedTupleT 0)++consTupleT :: [Type] -> Type+consTupleT = consTuple_ (TupleT 2) (TupleT 0)++consTuple_ :: Type -> Type -> [Type] -> Type+consTuple_ _ unit [] = unit+consTuple_ tup unit (t : ts) = tup `AppT` t `AppT` consTuple_ tup unit ts++-- ++fcfifyInfo :: ErrCtxt => TyInfo -> Q [Dec]+fcfifyInfo info = do+  paramsD <- declareParams info+  argsD <- declareArgs info+  resD <- declareRes info+  familyD <- declareFamily info+  pure [paramsD, argsD, resD, familyD]++getVars :: Type -> [Name]+getVars (VarT v) = [v]+getVars (AppT t t') = getVars t ++ getVars t'+getVars (AppKindT t t') = getVars t ++ getVars t'+getVars (SigT t k) = getVars t ++ getVars k+getVars (InfixT t _ t') = getVars t ++ getVars t'+getVars (UInfixT t _ t') = getVars t ++ getVars t'+getVars (ParensT t) = getVars t+#if MIN_VERSION_template_haskell(2,19,0)+getVars (PromotedInfixT t _ t') = getVars t ++ getVars t'+getVars (PromotedUInfixT t _ t') = getVars t ++ getVars t'+#endif+getVars _ = []++declareParams :: TyInfo -> Q Dec+declareParams info = do+  let nParams = length (tiParams info)+  pure (TySynInstD (TySynEqn Nothing (ConT ''Params `AppT` tiNameT info) (consTupleT (replicate nParams StarT))))  -- TODO: don't guess Type for all params++declareArgs :: TyInfo -> Q Dec+declareArgs info = do+  pure (TySynInstD (TySynEqn Nothing+    (ConT ''Args_ `AppT` tiNameT info `AppT` tiParamsT info)+    (consTupleT (snd <$> tiArgs info))))+    +declareRes :: TyInfo -> Q Dec+declareRes info = do+  pure (TySynInstD (TySynEqn Nothing+    (ConT ''Res_ `AppT` tiNameT info `AppT` tiParamsT info `AppT` if isDT info then tiArgsT info else WildCardT)+    (tiRes info)))++isDT :: TyInfo -> Bool+isDT info = not (null (intersection (fst <$> tiArgs info) (getVars (tiRes info))))++intersection :: Ord a => [a] -> [a] -> [a]+intersection = intersectionSorted `on` sort++intersectionSorted :: Ord a => [a] -> [a] -> [a]+intersectionSorted [] _  = []+intersectionSorted _  [] = []+intersectionSorted xxs@(x : xs) yys@(y : ys) = case compare x y of+  EQ -> x : intersectionSorted xs ys+  LT -> intersectionSorted xs yys+  GT -> intersectionSorted xxs ys++declareFamily :: TyInfo -> Q Dec+declareFamily info = do+  pure (TySynInstD (TySynEqn Nothing+    (ConT ''Eval `AppT` (ConT ''Family_ `AppT` tiNameT info `AppT` SigT WildCardT (WildCardT `AppT` tiParamsT info) `AppT` tiArgsT info))+    (foldl' AppT (ConT (tiName info)) (VarT . fst <$> tiArgs info))))
+ test/Main.hs view
@@ -0,0 +1,50 @@+{-# LANGUAGE AllowAmbiguousTypes, DataKinds, PolyKinds, ScopedTypeVariables, TemplateHaskell, TypeApplications, TypeFamilies, TypeOperators #-}+-- {-# OPTIONS_GHC -ddump-splices #-}++module Main where++import Data.Type.Bool+import GHC.TypeNats++import Fcf.Core+import Fcf.Family+import Fcf.Family.TH++fcfify ''(||)+fcfify ''(+)+fcfify ''If++type family Fst (xs :: (k, l)) :: k where Fst '(x, _) = x+type family Snd (xs :: (k, l)) :: l where Snd '(_, y) = y++fcfify ''Fst+fcfify ''Snd++type (:+:) = MkName "base" "GHC.TypeNats" "+"+type If_ = MkName "base" "Data.Type.Bool" "If"++equals :: forall a b. (a ~ b) => IO ()+equals = pure ()++main :: IO ()+main = do+  equate @(Eval (Family (:+:) P0 '(1, '(2, '())))) @3+  equate @(Eval (Family If_ P1 '( 'True , '(1, '(2, '()))))) @1+  equate @(Eval (Family If_ P1 '( 'False, '(1, '(2, '()))))) @2++  -- Test applyFamily+  equals @(Eval $(applyFamily ''(+) [ [t|3|] , [t|4|] ])) @7+  equals @(Eval $(applyFamily ''If [ [t|'True|] , [t|Int|] , [t|()|] ])) @Int++  -- Test kind inference: the two Any under If should have the same type.+  equate @(Eval (Family If_ P1 '( 'True, '(Any, '(Any, '()))))) @Any++  -- The following should fail because Family_ is untyped (unlike Family)+  -- equate @(Eval (Family_ If_ P1 '( 'True, '(Any, '(Any, '()))))) @Any++-- Utils++type family Any :: k where {}++equate :: forall a b. (a ~ b) => IO ()+equate = pure ()