free-foil 0.2.0 → 0.3.0

raw patch · 15 files changed

+1183/−323 lines, 15 filesdep ~arraydep ~bifunctorsdep ~containersPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: array, bifunctors, containers, deepseq, kind-generics, template-haskell, text

API changes (from Hackage documentation)

Files

• ChangeLog.md +77/−0
• free-foil.cabal +29/−25
• src/Control/Monad/Foil.hs +2/−0
• src/Control/Monad/Foil/Internal.hs +431/−6
• src/Control/Monad/Foil/Internal/ValidNameBinders.hs +180/−0
• src/Control/Monad/Free/Foil.hs +61/−36
• src/Control/Monad/Free/Foil/Generic.hs +0/−196
• src/Control/Monad/Free/Foil/TH.hs +0/−2
• src/Control/Monad/Free/Foil/TH/PatternSynonyms.hs +1/−1
• src/Control/Monad/Free/Foil/TH/ZipMatch.hs +0/−57
• src/Data/ZipMatchK.hs +80/−0
• src/Data/ZipMatchK/Bifunctor.hs +35/−0
• src/Data/ZipMatchK/Functor.hs +34/−0
• src/Data/ZipMatchK/Generic.hs +193/−0
• src/Data/ZipMatchK/Mappings.hs +60/−0

@@ -1,5 +1,82 @@ # CHANGELOG for `free-foil` +# 0.3.0 — 2026-07-14++This release makes generic deriving the default way to instantiate the library:+`Sinkable`, `CoSinkable`, `UnifiablePattern` and `ZipMatchK` can now all be+derived via [`kind-generics`](https://hackage.haskell.org/package/kind-generics),+so a user-defined pattern normally needs no hand-written instances at all.+The cost is one breaking change, described first.++## Breaking changes++- The `ZipMatch` class is **removed** in favour of the kind-polymorphic `ZipMatchK`,+  and the modules are reorganised (see [#30](https://github.com/fizruk/free-foil/pull/30)):++  - `Control.Monad.Free.Foil.Generic` is replaced by `Data.ZipMatchK`+    (with `Data.ZipMatchK.Bifunctor`, `Data.ZipMatchK.Functor`,+    `Data.ZipMatchK.Generic` and `Data.ZipMatchK.Mappings`);+  - `Control.Monad.Free.Foil.TH.ZipMatch` (and its `deriveZipMatch`) is removed,+    and `Control.Monad.Free.Foil.TH` no longer re-exports it.++  To migrate, delete the `ZipMatch` instances and any `deriveZipMatch` splices,+  and keep only the `ZipMatchK` ones. Where you had++  ```haskell+  import Control.Monad.Free.Foil.Generic++  instance ZipMatchK a => ZipMatchK (TermSig a)+  instance ZipMatchK a => ZipMatch  (TermSig a) where zipMatch = genericZipMatch2+  ```++  the second instance simply goes away:++  ```haskell+  import Data.ZipMatchK++  instance ZipMatchK a => ZipMatchK (TermSig a)+  ```++  `ZipMatchK` is derived generically, so the signature needs a `GenericK` instance+  (`deriveGenericK ''TermSig` from `kind-generics-th`). Note that `kind-generics-th`+  is not on Stackage, and is not a dependency of this library: a package using+  `deriveGenericK` must depend on it itself.++- α-equivalence and refreshing now ask for more of the binder: `alphaEquiv`,+  `alphaEquivRefreshed`, `refreshAST` and `refreshScopedAST` require+  `SinkableK binder` (and `ZipMatchK sig` in place of `ZipMatch sig`).+  For binders and patterns generated by our Template Haskell, or derived generically,+  this constraint is already satisfied and no change is needed.++## Generic deriving of patterns (see [#31](https://github.com/fizruk/free-foil/pull/31))++- New `SinkableK` class, generalising both `Sinkable` and `CoSinkable`:+  a type `f n₁ n₂ … nₖ` is treated as a generalised binder with variables and terms+  in scopes `n₁, n₂, …, nₖ`. Generic (kind-polymorphic) implementations are provided+  for `sinkabilityProof` and `coSinkabilityProof`, so `Sinkable` and `CoSinkable`+  instances can be left empty.+- New `HasNameBinders` class, generalising access to the nested `NameBinder`s of a pattern.+  This is what makes a *generic* `withPattern` possible, so user-defined patterns+  no longer need a hand-written traversal.+- `UnifiablePattern` now has a default implementation via `CoSinkable`,+  so `instance UnifiablePattern MyPattern` normally suffices.+- Malformed user-defined patterns are now rejected with a readable type error+  by a separate generic check (`GValidNameBinders`), instead of failing obscurely+  deeper in the machinery. Terms (and other types) are allowed in patterns,+  as long as the binders are threaded correctly.++## New functions (see [#32](https://github.com/fizruk/free-foil/pull/32))++- `unsinkAST` — unsink an `AST` from a larger scope into a smaller one, when possible.+- `freeVarsOf` and `freeVarsOfScopedAST` — collect the free variables of an `AST`.+- `nameMapToScope` — recover a `Scope` from a `NameMap`.+- `NameMap` is now a `Functor`, `Foldable` and `Traversable`.++## Fixes++- `GValidNameBinders` no longer rejects a valid constructor that equates its scopes+  and carries more than one field (substitution now recurses through sums and products).+ # 0.2.0 — 2024-10-27  - Generate [`COMPLETE` pragma](https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/pragmas.html#complete-pragmas) in `mkPatternSynonyms` (see [#26](https://github.com/fizruk/free-foil/pull/26))

@@ -1,11 +1,11 @@ cabal-version: 1.12 --- This file has been generated from package.yaml by hpack version 0.37.0.+-- This file has been generated from package.yaml by hpack version 0.39.1. -- -- see: https://github.com/sol/hpack  name:           free-foil-version:        0.2.0+version:        0.3.0 synopsis:       Efficient Type-Safe Capture-Avoiding Substitution for Free (Scoped Monads) description:    Please see the README on GitHub at <https://github.com/fizruk/free-foil#readme> category:       Parsing@@ -31,6 +31,7 @@       Control.Monad.Foil       Control.Monad.Foil.Example       Control.Monad.Foil.Internal+      Control.Monad.Foil.Internal.ValidNameBinders       Control.Monad.Foil.Relative       Control.Monad.Foil.TH       Control.Monad.Foil.TH.MkFoilData@@ -40,27 +41,30 @@       Control.Monad.Foil.TH.Util       Control.Monad.Free.Foil       Control.Monad.Free.Foil.Example-      Control.Monad.Free.Foil.Generic       Control.Monad.Free.Foil.TH       Control.Monad.Free.Foil.TH.Convert       Control.Monad.Free.Foil.TH.MkFreeFoil       Control.Monad.Free.Foil.TH.PatternSynonyms       Control.Monad.Free.Foil.TH.Signature-      Control.Monad.Free.Foil.TH.ZipMatch+      Data.ZipMatchK+      Data.ZipMatchK.Bifunctor+      Data.ZipMatchK.Functor+      Data.ZipMatchK.Generic+      Data.ZipMatchK.Mappings   other-modules:       Paths_free_foil   hs-source-dirs:       src   ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path   build-depends:-      array >=0.5.3.0+      array >=0.5.3.0 && <0.6     , base >=4.7 && <5-    , bifunctors-    , containers-    , deepseq-    , kind-generics >=0.5.0-    , template-haskell >=2.21.0.0-    , text >=1.2.3.1+    , bifunctors >=5.5 && <5.7+    , containers >=0.6 && <0.9+    , deepseq >=1.4 && <1.6+    , kind-generics >=0.5.0 && <0.6+    , template-haskell >=2.21.0.0 && <2.24+    , text >=1.2.3.1 && <2.2   default-language: Haskell2010  test-suite doctests@@ -71,16 +75,16 @@       test/doctests   ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path   build-depends:-      array >=0.5.3.0+      array >=0.5.3.0 && <0.6     , base >=4.7 && <5-    , bifunctors-    , containers-    , deepseq+    , bifunctors >=5.5 && <5.7+    , containers >=0.6 && <0.9+    , deepseq >=1.4 && <1.6     , doctest-parallel     , free-foil-    , kind-generics >=0.5.0-    , template-haskell >=2.21.0.0-    , text >=1.2.3.1+    , kind-generics >=0.5.0 && <0.6+    , template-haskell >=2.21.0.0 && <2.24+    , text >=1.2.3.1 && <2.2   default-language: Haskell2010  test-suite spec@@ -92,13 +96,13 @@       test   ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path -threaded -rtsopts -with-rtsopts=-N   build-depends:-      array >=0.5.3.0+      array >=0.5.3.0 && <0.6     , base >=4.7 && <5-    , bifunctors-    , containers-    , deepseq+    , bifunctors >=5.5 && <5.7+    , containers >=0.6 && <0.9+    , deepseq >=1.4 && <1.6     , free-foil-    , kind-generics >=0.5.0-    , template-haskell >=2.21.0.0-    , text >=1.2.3.1+    , kind-generics >=0.5.0 && <0.6+    , template-haskell >=2.21.0.0 && <2.24+    , text >=1.2.3.1 && <2.2   default-language: Haskell2010

@@ -35,8 +35,10 @@   unsinkName,   unsinkNamePattern,   -- * Safe (co)sinking and renaming+  SinkableK(..),   Sinkable(..),   CoSinkable(..),+  HasNameBinders(getNameBinders),   sink,   extendRenaming,   extendNameBinderRenaming,

@@ -1,16 +1,25 @@+{-# OPTIONS_GHC -Wno-missing-methods #-}  -- disabled to avoid overlapping type instances+{-# OPTIONS_GHC -Wno-overlapping-patterns -Wno-inaccessible-code #-}  -- disabled because I think GHC is wrong+{-# LANGUAGE AllowAmbiguousTypes        #-} {-# LANGUAGE BlockArguments             #-} {-# LANGUAGE ConstraintKinds            #-} {-# LANGUAGE DataKinds                  #-}+{-# LANGUAGE DeriveTraversable          #-} {-# LANGUAGE EmptyCase                  #-}+{-# LANGUAGE FlexibleContexts           #-} {-# LANGUAGE FlexibleInstances          #-} {-# LANGUAGE GADTs                      #-}+{-# LANGUAGE InstanceSigs               #-} {-# LANGUAGE KindSignatures             #-} {-# LANGUAGE LambdaCase                 #-} {-# LANGUAGE MultiParamTypeClasses      #-}+{-# LANGUAGE PolyKinds                  #-} {-# LANGUAGE QuantifiedConstraints      #-} {-# LANGUAGE RankNTypes                 #-} {-# LANGUAGE ScopedTypeVariables        #-} {-# LANGUAGE TypeApplications           #-}+{-# LANGUAGE TypeFamilies               #-}+{-# LANGUAGE TypeOperators              #-} {-# LANGUAGE UndecidableInstances       #-} {-# OPTIONS_GHC -Wno-incomplete-patterns #-} {-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}@@ -36,15 +45,20 @@ -- — the number of bits in an 'Int' (32 or 64). module Control.Monad.Foil.Internal where -import           Control.DeepSeq (NFData (..))-import           Data.Coerce     (coerce)+import           Control.DeepSeq    (NFData (..))+import           Data.Bifunctor+import           Data.Coerce        (coerce) import           Data.IntMap-import qualified Data.IntMap     as IntMap+import qualified Data.IntMap        as IntMap import           Data.IntSet-import qualified Data.IntSet     as IntSet-import           Data.Kind       (Type)+import qualified Data.IntSet        as IntSet+import           Data.Kind          (Type)+import qualified Data.Type.Equality as Type+import           Generics.Kind import           Unsafe.Coerce +import Control.Monad.Foil.Internal.ValidNameBinders+ -- * Safe types and operations  -- | 'S' is a data kind of scope indices.@@ -563,7 +577,17 @@ class CoSinkable pattern => UnifiablePattern pattern where   -- | Unify two patterns and decide which binders need to be renamed.   unifyPatterns :: Distinct n => pattern n l -> pattern n r -> UnifyNameBinders pattern n l r+  default unifyPatterns+    :: (CoSinkable pattern, Distinct n)+    => pattern n l -> pattern n r -> UnifyNameBinders pattern n l r+  unifyPatterns l r = coerce (unifyPatterns (nameBinderListOf l) (nameBinderListOf r)) +instance UnifiablePattern NameBinderList where+  unifyPatterns NameBinderListEmpty NameBinderListEmpty = SameNameBinders emptyNameBinders+  unifyPatterns (NameBinderListCons x xs) (NameBinderListCons y ys) =+    case (assertDistinct x, assertDistinct y) of+      (Distinct, Distinct) -> unifyNameBinders x y `andThenUnifyPatterns` (xs, ys)+ -- | Unification of values in patterns. -- By default, 'Eq' instance is used, but it may be useful to ignore -- some data in pattens (such as location annotations).@@ -599,6 +623,10 @@     -> e n                  -- ^ Expression with free variables in scope @n@.     -> e l +  default sinkabilityProof+    :: (GenericK e, GSinkableK (RepK e)) => (Name n -> Name l) -> e n -> e l+  sinkabilityProof rename = toK . gsinkabilityProof1 rename . fromK+ -- | Sinking a 'Name' is as simple as applying the renaming. instance Sinkable Name where   sinkabilityProof rename = rename@@ -688,6 +716,14 @@     -- ^ A continuation, accepting an extended renaming from @l@ to @l'@ (which itself extends @n'@)     -- and a (possibly refreshed) pattern that extends @n'@ to @l'@.     -> r+  default coSinkabilityProof+    :: (GenericK pattern, GSinkableK (RepK pattern))+    => (Name n -> Name n')+    -> pattern n l+    -> (forall l'. (Name l -> Name l') -> pattern n' l' -> r)+    -> r+  coSinkabilityProof rename p cont = gsinkabilityProof2 rename (fromK @_ @pattern p) $ \rename' p' ->+    cont rename' (toK @_ @pattern p')    -- | Generalized processing of a pattern.   --@@ -707,6 +743,16 @@     -> (forall o'. DExt o o' => f n l o o' -> pattern o o' -> r)     -- ^ Continuation, accepting result for the entire pattern and a (possibly refreshed) pattern.     -> r+  default withPattern+    :: (Distinct o, GenericK pattern, GValidNameBinders pattern (RepK pattern), GHasNameBinders (RepK pattern))+    => (forall x y z r'. Distinct z => Scope z -> NameBinder x y -> (forall z'. DExt z z' => f x y z z' -> NameBinder z z' -> r') -> r')+    -> (forall x z z'. DExt z z' => f x x z z')+    -> (forall x y y' z z' z''. (DExt z z', DExt z' z'') => f x y z z' -> f y y' z' z'' -> f x y' z z'')+    -> Scope o+    -> pattern n l+    -> (forall o'. DExt o o' => f n l o o' -> pattern o o' -> r)+    -> r+  withPattern = gunsafeWithPatternViaHasNameBinders  -- | Auxiliary data structure for collecting name binders. Used in 'nameBinderListOf'. newtype WithNameBinderList r n l (o :: S) (o' :: S) = WithNameBinderList (NameBinderList l r -> NameBinderList n r)@@ -808,7 +854,7 @@ -- * 'Name' maps  -- | A /total/ map from names in scope @n@ to elements of type @a@.-newtype NameMap (n :: S) a = NameMap { getNameMap :: IntMap a }+newtype NameMap (n :: S) a = NameMap { getNameMap :: IntMap a } deriving (Functor, Foldable, Traversable)  -- | An empty map belongs in the empty scope. emptyNameMap :: NameMap VoidS a@@ -818,6 +864,10 @@ nameMapToSubstitution :: NameMap i (e o) -> Substitution e i o nameMapToSubstitution (NameMap m) = (UnsafeSubstitution m) +-- | Convert a 'NameMap' of expressions into a 'Scope'.+nameMapToScope :: NameMap n a -> Scope n+nameMapToScope (NameMap m) = UnsafeScope (IntMap.keysSet m)+ -- | Extend a map with multiple mappings (by repeatedly applying 'addNameBinder'). -- -- Note that the input list is expected to have __at least__ the same number of elements@@ -907,3 +957,378 @@ class InjectName (e :: S -> Type) where   -- | Inject names into expressions.   injectName :: Name n -> e n++-- * Kind-polymorphic sinkability++data RenamingsK (as :: LoT k) (bs :: LoT k) where+  RNil :: RenamingsK LoT0 LoT0+  RCons :: (Name a -> Name b) -> RenamingsK as bs -> RenamingsK (a :&&: as) (b :&&: bs)+  RSkip :: RenamingsK as bs -> RenamingsK (k :&&: as) (k :&&: bs)++class SinkableK (f :: S -> k) where+  sinkabilityProofK+    :: forall as bs r.+       RenamingsK as bs+    -> f :@@: as+    -> (forall cs. RenamingsK as cs -> f :@@: cs -> r)+    -> r+  default sinkabilityProofK :: forall as bs r.+      (GenericK f, GSinkableK (RepK f))+    => RenamingsK as bs+    -> f :@@: as+    -> (forall cs. RenamingsK as cs -> f :@@: cs -> r)+    -> r+  sinkabilityProofK rename e cont =+    gsinkabilityProofK rename (fromK @_ @f e) $ \rename' e' ->+      cont rename' (toK @_ @f e')++sinkK :: GSinkableK f => RenamingsK xs as -> RenamingsK xs bs -> f :@@: as -> f :@@: bs+sinkK _ _ = unsafeCoerce++instance SinkableK Name where+  sinkabilityProofK renameK@(RCons rename RNil) name cont = cont renameK (rename name)+instance SinkableK NameBinder where+  sinkabilityProofK (RCons _ RNil) (UnsafeNameBinder name) cont =+    cont (RCons unsafeCoerce RNil) (UnsafeNameBinder name)+instance SinkableK NameBinders where+  sinkabilityProofK (RCons _ RNil) (UnsafeNameBinders s) cont =+    cont (RCons unsafeCoerce RNil) (UnsafeNameBinders s)++instance GenericK NameBinderList where+  type RepK NameBinderList = ((Var0 :~~: Var1) :=>: U1) :+: Exists S+    (Field (NameBinder :$: Var1 :@: Var0) :*: Field (NameBinderList :$: Var0 :@: Var2))+  toK (L1 (SuchThat U1))                   = NameBinderListEmpty+  toK (R1 (Exists (Field x :*: Field xs))) = NameBinderListCons x xs+  fromK NameBinderListEmpty       = L1 (SuchThat U1)+  fromK (NameBinderListCons x xs) = R1 (Exists (Field x :*: Field xs))++instance GenericK V2 where+  type RepK V2 = V1+  toK _v1 = error "absurd: Generics.Kind.V1"+  fromK = absurd2++instance GenericK U2 where+  type RepK U2 = ((Var0 :~~: Var1) :=>: U1)+  toK (SuchThat U1) = U2+  fromK U2 = SuchThat U1++instance SinkableK NameBinderList+instance SinkableK V2+instance SinkableK U2++sinkabilityProof1 :: SinkableK f => (Name n -> Name n') -> f n -> f n'+sinkabilityProof1 rename e = sinkabilityProofK (RCons rename RNil) e $ \_ e' -> unsafeCoerce e'++gsinkabilityProof1 :: GSinkableK f => (Name n -> Name n') -> f (n :&&: LoT0) -> f (n' :&&: LoT0)+gsinkabilityProof1 rename e = gsinkabilityProofK (RCons rename RNil) e $ \_ e' -> unsafeCoerce e'++gsinkabilityProof2+  :: forall f n n' l r. GSinkableK f+  => (Name n -> Name n') -> f (n :&&: l :&&: LoT0)+  -> (forall l'. (Name l -> Name l') -> f (n' :&&: l' :&&: LoT0) -> r)+  -> r+gsinkabilityProof2 rename e cont =+  gsinkabilityProofK (RCons rename (RCons id RNil)) e $ \case+    RCons (_ :: Name n -> Name n'') (RCons rename' RNil) -> \e' ->+      case unsafeCoerce (Type.Refl :: n' Type.:~: n') :: n' Type.:~: n'' of+        Type.Refl -> cont rename' e'++gsinkabilityProofK' :: GSinkableK f => RenamingsK as bs -> f as -> f bs+gsinkabilityProofK' renameK e = gsinkabilityProofK renameK e $ \_ e' -> unsafeCoerce e'++class GSinkableK p where+  gsinkabilityProofK+    :: forall as bs r.+       RenamingsK as bs+    -> p as+    -> (forall cs. RenamingsK as cs -> p cs -> r)+    -> r++gsinkK :: GSinkableK f => RenamingsK xs as -> RenamingsK xs bs -> f as -> f bs+gsinkK _ _ = unsafeCoerce++instance GSinkableK V1 where+  gsinkabilityProofK irename _v1 cont =+    cont irename (error "absurd: Generics.Kind.V1")++instance GSinkableK U1 where+  gsinkabilityProofK irename U1 cont =+    cont irename U1++instance GSinkableK f => GSinkableK (M1 i c f) where+  gsinkabilityProofK irename (M1 x) cont =+    gsinkabilityProofK irename x $ \irename' x' ->+      cont irename' (M1 x')++instance (GSinkableK f, GSinkableK g) => GSinkableK (f :+: g) where+  gsinkabilityProofK irename (L1 x) cont =+    gsinkabilityProofK irename x $ \irename' x' ->+      cont irename' (L1 x')+  gsinkabilityProofK irename (R1 x) cont =+    gsinkabilityProofK irename x $ \irename' x' ->+      cont irename' (R1 x')++instance (GSinkableK f, GSinkableK g) => GSinkableK (f :*: g) where+  gsinkabilityProofK irename (x :*: y) cont =+    gsinkabilityProofK irename x $ \irename' x' ->+      gsinkabilityProofK irename' y $ \irename'' y' ->+        cont irename'' (gsinkK irename' irename'' x' :*: y')++instance GSinkableK f => GSinkableK (Exists S f) where+  gsinkabilityProofK irename (Exists x) cont =+    gsinkabilityProofK (RCons id irename) x $ \case+      RCons _ irename' -> \x' ->+        cont irename' (Exists x')++instance {-# OVERLAPPABLE #-} GSinkableK f => GSinkableK (Exists k f) where+  gsinkabilityProofK irename (Exists x) cont =+    gsinkabilityProofK (RSkip irename) x $ \case+      RSkip irename' -> \x' ->+        cont irename' (Exists x')++instance GSinkableK f => GSinkableK ((a :~~: b) :=>: f) where+  gsinkabilityProofK irename (SuchThat x) cont =+    gsinkabilityProofK irename x $ \(irename' :: RenamingsK as cs) x' ->+      -- this is sort of safe...+      case unsafeCoerce (Type.Refl :: Interpret a cs Type.:~: Interpret a cs) :: Interpret a cs Type.:~: Interpret b cs of+        Type.Refl -> cont irename' (SuchThat x')++instance GSinkableK (Field (Kon a)) where+  gsinkabilityProofK irename (Field x) cont =+    cont irename (Field x)++instance GSinkableK (Field (Var a)) where+  gsinkabilityProofK irename (Field x) cont =+    cont irename (Field (unsafeCoerce x)) -- FIXME: unsafeCoerce?++instance (SinkableK f, ExtractRenamingK i) => GSinkableK (Field (Kon f :@: Var i)) where+  gsinkabilityProofK irename (Field x) cont =+    sinkabilityProofK (RCons (extractRenamingK @_ @i irename) RNil) x $ \case+      RCons rename' RNil -> \x' ->+        cont (putBackRenamingK @_ @i rename' irename) (Field (unsafeCoerce x')) -- unsafeCoerce?++instance SinkableK (f a) => GSinkableK (Field (Kon f :@: Kon a :@: Var0)) where+  gsinkabilityProofK irename@(RCons _ RNil) (Field x) cont =+    sinkabilityProofK irename x $ \rename' x' ->+      cont rename' (Field x')++instance SinkableK (f a b) => GSinkableK (Field (Kon f :@: Kon a :@: Kon b :@: Var0)) where+  gsinkabilityProofK irename@(RCons _ RNil) (Field x) cont =+    sinkabilityProofK irename x $ \rename' x' ->+      cont rename' (Field x')++class ExtractRenamingK (i :: TyVar k S) where+  extractRenamingK :: forall (as :: LoT k) (bs :: LoT k).+    RenamingsK as bs -> Name (Interpret (Var i) as) -> Name (Interpret (Var i) bs)+  putBackRenamingK :: forall c (as :: LoT k) (bs :: LoT k).+       (Name (Interpret (Var i) as) -> Name c)+    -> RenamingsK as bs+    -> RenamingsK as (PutBackLoT i c bs)++instance ExtractRenamingK VZ where+  extractRenamingK (RCons f _fs) = f+  putBackRenamingK f (RCons _ gs) = RCons f gs++instance ExtractRenamingK x => ExtractRenamingK (VS x) where+  extractRenamingK (RCons _f fs) = extractRenamingK @_ @x fs+  putBackRenamingK f (RCons g gs) = RCons g (putBackRenamingK @_ @x f gs)++extractTwoRenamingsK :: forall k (i :: TyVar k S) (j :: TyVar k S) (as :: LoT k) (bs :: LoT k).+    (ExtractRenamingK i, ExtractRenamingK j)+  => RenamingsK as bs+  -> RenamingsK+      (Interpret (Var i) as :&&: Interpret (Var j) as :&&: LoT0)+      (Interpret (Var i) bs :&&: Interpret (Var j) bs :&&: LoT0)+extractTwoRenamingsK irename =+  (RCons (extractRenamingK @_ @i irename) (RCons (extractRenamingK @_ @j irename) RNil))++putBackTwoRenamingsK :: forall k (i :: TyVar k S) (j :: TyVar k S) c1 c2 (as :: LoT k) (bs :: LoT k).+    (ExtractRenamingK i, ExtractRenamingK j)+  => RenamingsK+      (Interpret (Var i) as :&&: Interpret (Var j) as :&&: LoT0)+      (c1 :&&: c2 :&&: LoT0)+  -> RenamingsK as bs+  -> RenamingsK as (PutBackLoT j c2 (PutBackLoT i c1 bs))+putBackTwoRenamingsK (RCons f1 (RCons f2 RNil)) rename+  = putBackRenamingK @_ @j f2 (putBackRenamingK @_ @i f1 rename)++instance (SinkableK f, ExtractRenamingK i, ExtractRenamingK j) => GSinkableK (Field (Kon f :@: Var (i :: TyVar k S) :@: Var (j :: TyVar k S))) where+  gsinkabilityProofK irename (Field x) cont =+    sinkabilityProofK (extractTwoRenamingsK @_ @i @j irename) x $ \rename' x' ->+      case rename' of+        RCons _ (RCons _ RNil) ->+          cont (putBackTwoRenamingsK @_ @i @j rename' irename)+              (Field (unsafeCoerce x'))  -- FIXME: can we do better than unsafeCoerce?++instance (Functor f, GSinkableK (Field x)) => GSinkableK (Field (Kon f :@: x)) where+  gsinkabilityProofK irename (Field x) cont =+    cont irename (Field (fmap+      (unField . gsinkabilityProofK' @(Field x) irename . Field)+      x))++instance (Bifunctor f, GSinkableK (Field x), GSinkableK (Field y)) => GSinkableK (Field (Kon f :@: x :@: y)) where+  gsinkabilityProofK irename (Field x) cont =+    cont irename (Field (bimap+      (unField . gsinkabilityProofK' @(Field x) irename . Field)+      (unField . gsinkabilityProofK' @(Field y) irename . Field)+      x))++-- * Kind-polymorphic types with binders++-- ** Generic version of 'withPattern'++-- | Generic generalized processing of a pattern via 'GHasNameBinders'.+--+-- This can be used as a default implementation of 'withPattern'.+gunsafeWithPatternViaHasNameBinders+  :: forall pattern f o n l r.+      (Distinct o, GenericK pattern, GValidNameBinders pattern (RepK pattern), GHasNameBinders (RepK pattern))+  => (forall x y z r'. Distinct z => Scope z -> NameBinder x y -> (forall z'. DExt z z' => f x y z z' -> NameBinder z z' -> r') -> r')+  -- ^ Processing of a single 'NameBinder', this will be applied to each binder in a pattern.+  -> (forall x z z'. DExt z z' => f x x z z')+  -- ^ Result in case no binders are present. This can be seen as scope-indexed 'mempty'.+  -> (forall x y y' z z' z''. (DExt z z', DExt z' z'') => f x y z z' -> f y y' z' z'' -> f x y' z z'')+  -- ^ Composition of results for nested binders/patterns. This can be seen as scope-indexed 'mappend'.+  -> Scope o+  -- ^ Ambient scope.+  -> pattern n l+  -- ^ Pattern to process.+  -> (forall o'. DExt o o' => f n l o o' -> pattern o o' -> r)+  -- ^ Continuation, accepting result for the entire pattern and a (possibly refreshed) pattern.+  -> r+gunsafeWithPatternViaHasNameBinders withBinder id_ comp_ scope pat cont =+  withPattern withBinder id_ comp_ scope (ggetNameBinders pat) $ \result binders ->+    cont result (gunsafeSetNameBinders (unsafeCoerce pat) binders) -- FIXME: safer version++-- ** Manipulating nested 'NameBinder's+-- | If @'HasNameBinders' f@, then @f n l@ is expected to act as a binder,+-- introducing into scope @n@ some local variables, extending it to scope @l@.+-- This class allows to extract and modify the set of binders.+class HasNameBinders f where+  -- | Extract a set of binders from a pattern.+  getNameBinders :: f n l -> NameBinders n l+  getNameBinders = UnsafeNameBinders . IntSet.fromList . getNameBindersRaw++  -- | Replace binders in a pattern.+  --+  -- This function is unsafe, because it does not check if the new set of binders+  -- has the same size. It can therefore crash at runtime.+  --+  -- You should probably not use this.+  -- This is only used for 'gunsafeWithPatternViaHasNameBinders', which is then safe to use.+  unsafeSetNameBinders :: f n l -> NameBinders n l' -> f n l'+  unsafeSetNameBinders e (UnsafeNameBinders m) = fst (reallyUnsafeSetNameBindersRaw e (IntSet.toList m))++  -- | Extract 'RawName's of all binders occurring in a pattern.+  getNameBindersRaw :: f n l -> [RawName]+  default getNameBindersRaw :: forall n l. (GenericK f, GHasNameBinders (RepK f)) => f n l -> [RawName]+  getNameBindersRaw = ggetNameBindersRaw . fromK @_ @f @(n :&&: l :&&: LoT0)++  -- | This is a version of 'unsafeSetNameBinders'+  -- that takes in a list of 'RawName's.+  --+  -- It does not check if the given list has enough elements.+  -- It does not check if the raw names are fresh in the scope @n@.+  -- It does not check if the raw names given are distinct.+  --+  -- You should never use this. This is only used for generic implementation of 'HasNameBinders'.+  reallyUnsafeSetNameBindersRaw :: f n l -> [RawName] -> (f n l', [RawName])+  default reallyUnsafeSetNameBindersRaw :: forall n l l'. (GenericK f, GValidNameBinders f (RepK f), GHasNameBinders (RepK f)) => f n l -> [RawName] -> (f n l', [RawName])+  reallyUnsafeSetNameBindersRaw e names =+    let (e', names') = greallyUnsafeSetNameBindersRaw (fromK @_ @f @(n :&&: l :&&: LoT0) e) names+     in (toK @_ @f @(n :&&: l' :&&: LoT0) e', names')++instance HasNameBinders NameBinder where+  getNameBindersRaw (UnsafeNameBinder (UnsafeName name)) = [name]+  reallyUnsafeSetNameBindersRaw _ (name:names) = (UnsafeNameBinder (UnsafeName name), names)++instance HasNameBinders NameBinderList++-- ** Generic++ggetNameBinders :: forall f n l. (GenericK f, GHasNameBinders (RepK f)) => f n l -> NameBinders n l+ggetNameBinders = UnsafeNameBinders . IntSet.fromList . ggetNameBindersRaw . fromK @_ @f @(n :&&: l :&&: LoT0)++gunsafeSetNameBinders :: forall f n l l'. (GenericK f, GValidNameBinders f (RepK f), GHasNameBinders (RepK f)) => f n l -> NameBinders n l' -> f n l'+gunsafeSetNameBinders e (UnsafeNameBinders m) = toK @_ @f @(n :&&: l' :&&: LoT0) $+  fst (greallyUnsafeSetNameBindersRaw (fromK @_ @f @(n :&&: l :&&: LoT0) e) (IntSet.toList m))++class GHasNameBinders f where+  ggetNameBindersRaw :: f as -> [RawName]+  greallyUnsafeSetNameBindersRaw :: f as -> [RawName] -> (f bs, [RawName])++instance GHasNameBinders V1 where+  ggetNameBindersRaw _ = error "absurd: Generics.Kind.V1"+  greallyUnsafeSetNameBindersRaw _ _ = error "absurd: Generics.Kind.V1"+instance GHasNameBinders U1 where+  ggetNameBindersRaw U1 = []+  greallyUnsafeSetNameBindersRaw U1 names = (U1, names)++instance (GHasNameBinders f, GHasNameBinders g) => GHasNameBinders (f :+: g) where+  ggetNameBindersRaw (L1 x) = ggetNameBindersRaw x+  ggetNameBindersRaw (R1 x) = ggetNameBindersRaw x++  greallyUnsafeSetNameBindersRaw (L1 x) names = first L1 (greallyUnsafeSetNameBindersRaw x names)+  greallyUnsafeSetNameBindersRaw (R1 x) names = first R1 (greallyUnsafeSetNameBindersRaw x names)++-- | FIXME: this is, perhaps, the most "unsafe" place for the user+-- since it does not reject "parallel" binders:+--+--    data BadPattern n l = BadPattern (NameBinder n l) (NameBinder n l)+--+-- This instance will treat both binders in the same way as "nested":+--+--    data GoodPattern n l = forall i. GoodPattern (NameBinder n i) (NameBinder i l)+--+-- However, Template Haskell code at the moment will never generate "parallel" binders,+-- and the very user is unlikely to misuse this instance, since "parallel" binders+-- require extra effort to support it.+--+-- Still, it would be better to detect and reject any "parallel" or otherwise improper binders.+instance (GHasNameBinders f, GHasNameBinders g) => GHasNameBinders (f :*: g) where+  ggetNameBindersRaw (x :*: y) = ggetNameBindersRaw x <> ggetNameBindersRaw y+  greallyUnsafeSetNameBindersRaw (x :*: y) names =+    let (x', names') = greallyUnsafeSetNameBindersRaw x names+        (y', names'') = greallyUnsafeSetNameBindersRaw y names'+     in (x' :*: y', names'')++instance GHasNameBinders f => GHasNameBinders (M1 i c f) where+  ggetNameBindersRaw (M1 x) = ggetNameBindersRaw x+  greallyUnsafeSetNameBindersRaw (M1 x) names =+    let (x', names') = greallyUnsafeSetNameBindersRaw x names+     in (M1 x', names')++instance GHasNameBinders f => GHasNameBinders (Var i :~~: Var j :=>: f) where+  ggetNameBindersRaw (SuchThat x) = ggetNameBindersRaw x++  greallyUnsafeSetNameBindersRaw :: forall as bs. (Var i :~~: Var j :=>: f) as -> [RawName] -> ((Var i :~~: Var j :=>: f) bs, [RawName])+  greallyUnsafeSetNameBindersRaw (SuchThat x) names =+    -- this is sort of safe...+    case unsafeCoerce (Type.Refl :: Interpret (Var i) bs Type.:~: Interpret (Var i) bs) :: Interpret (Var i) bs Type.:~: Interpret (Var j) bs of+      Type.Refl ->+        let (x', names') = greallyUnsafeSetNameBindersRaw x names+         in (SuchThat x', names')++instance GHasNameBinders f => GHasNameBinders (Exists k f) where+  ggetNameBindersRaw (Exists x) = ggetNameBindersRaw x+  greallyUnsafeSetNameBindersRaw (Exists x) names =+    let (x', names') = greallyUnsafeSetNameBindersRaw x names+     in (Exists x', names')++instance GHasNameBinders (Field (Kon a)) where+  ggetNameBindersRaw (Field _x) = []+  greallyUnsafeSetNameBindersRaw (Field x) names = (Field x, names)++instance GHasNameBinders (Field (Var x)) where+  ggetNameBindersRaw (Field _x) = []+  greallyUnsafeSetNameBindersRaw (Field x) names = (Field (unsafeCoerce x), names)  -- FIXME: unsafeCoerce?++instance GHasNameBinders (Field (Kon f :@: Var i)) where+  ggetNameBindersRaw (Field _x) = []+  greallyUnsafeSetNameBindersRaw (Field x) names = (Field (unsafeCoerce x), names) -- FIXME: unsafeCoerce?++instance HasNameBinders f => GHasNameBinders (Field (Kon f :@: Var i :@: Var j)) where+  ggetNameBindersRaw (Field x) = getNameBindersRaw x+  greallyUnsafeSetNameBindersRaw (Field x) names =+    let (x', names') = reallyUnsafeSetNameBindersRaw x names+     in (Field (unsafeCoerce x'), names') -- FIXME: safer version?

@@ -0,0 +1,180 @@+{-# LANGUAGE StandaloneKindSignatures  #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE TypeOperators  #-}+{-# LANGUAGE TypeApplications  #-}+{-# LANGUAGE TypeFamilies  #-}+{-# LANGUAGE PolyKinds  #-}+{-# LANGUAGE DataKinds  #-}+module Control.Monad.Foil.Internal.ValidNameBinders where++import Data.Kind (Type, Constraint)+import GHC.TypeError+import GHC.TypeLits+import Generics.Kind+import qualified GHC.Generics as GHC++type SubstInRepK :: TyVar d k -> Atom d k -> (LoT d -> Type) -> LoT d -> Type+type family SubstInRepK i atom f where+  SubstInRepK i atom V1 = V1+  SubstInRepK i atom U1 = U1+  SubstInRepK i atom (M1 info c f) = M1 info c (SubstInRepK i atom f)+  SubstInRepK i atom (Field field) = Field (SubstInAtom i atom field)+  SubstInRepK i atom (f :+: g) = SubstInRepK i atom f :+: SubstInRepK i atom g+  SubstInRepK i atom (f :*: g) = SubstInRepK i atom f :*: SubstInRepK i atom g+  SubstInRepK i atom f =+    TypeError+      ('Text "cannot substitute variable"+      :$$: 'Text "  " :<>: 'ShowType (Var i)+      :$$: 'Text "with atom"+      :$$: 'Text "  " :<>: 'ShowType atom+      :$$: 'Text "in"+      :$$: 'Text "  " :<>: 'ShowType f)++type SubstInAtom :: TyVar d k -> Atom d k -> Atom d k1 -> Atom d k1+type family SubstInAtom i atom f where+  SubstInAtom i atom (Var i) = atom+  SubstInAtom i atom (Var j) = Var j+  SubstInAtom i atom (Kon a) = Kon a+  SubstInAtom i atom (f :@: x) = SubstInAtom i atom f :@: SubstInAtom i atom x+  -- SubstInAtom i atom atom' = atom'+  SubstInAtom i atom atom' =+    TypeError+      ('Text "cannot substitute variable"+      :$$: 'Text "  " :<>: 'ShowType (Var i)+      :$$: 'Text "with atom"+      :$$: 'Text "  " :<>: 'ShowType atom+      :$$: 'Text "in an atom"+      :$$: 'Text "  " :<>: 'ShowType atom')++type ShowKindedScope oo n ll = ShowScope oo n ll :<>: 'Text " : S"++type ShowScope :: Atom d s -> Atom d s -> Atom d s -> ErrorMessage+type family ShowScope oo n ll where+  ShowScope oo ll ll = 'Text "innerScope"+  ShowScope oo oo ll = 'Text "outerScope"+  ShowScope oo n  ll = ShowScopeN 1 n++type ShowScopeN :: Natural -> Atom d s -> ErrorMessage+type family ShowScopeN i n where+  ShowScopeN i (Var VZ) = 'Text "scope" :<>: 'ShowType i+  ShowScopeN i (Var (VS x)) = ShowScopeN (i + 1) (Var x)++type ShowSaturatedPatternType pattern oo n l ll =+  'ShowType pattern :<>: 'Text " " :<>: ShowScope oo n ll :<>: 'Text " " :<>: ShowScope oo l ll++type GInnerScopeOfAtom :: ErrorMessage -> Nat -> Nat -> (s -> s -> Type) -> Atom d Type -> Atom d s -> Atom d s -> Atom d s -> Atom d s+type family GInnerScopeOfAtom msg icon ifield pattern atom oo n ll where+  GInnerScopeOfAtom msg icon ifield pattern (Kon f :@: n :@: l) oo n ll = l+  GInnerScopeOfAtom msg icon ifield pattern (Kon f :@: o :@: i) oo n ll =+    TypeError+      ('Text "Unexpected Foil scope extension in the binder/pattern"+      :$$: 'Text "  " :<>: ShowSaturatedPatternType f oo o i ll+      :$$: 'Text "the binder/pattern tries to extend scope"+      :$$: 'Text "  " :<>: ShowKindedScope oo o ll+      :$$: 'Text "to scope"+      :$$: 'Text "  " :<>: ShowKindedScope oo i ll+      :$$: 'Text "but it is expected to extend the current (outer) scope"+      :$$: 'Text "  " :<>: ShowKindedScope oo n ll+      :$$: ShowLocalizeError msg icon ifield pattern oo ll+      )+  GInnerScopeOfAtom msg icon ifield pattern atom oo n ll = n++type SameInnerScope :: ErrorMessage -> Nat -> (s -> s -> Type) -> Atom k s -> Atom k s -> Atom k s+type family SameInnerScope msg icon pattern n l where+  SameInnerScope msg icon pattern l l = l+  SameInnerScope msg icon pattern n l =+    TypeError+      ('Text "Unexpected extended (inner) Foil scope in the data type"+      :$$: 'Text "  " :<>: ShowSaturatedPatternType pattern n n l l+      :$$: 'Text "expecting extended (inner) scope to be"+      :$$: 'Text "  " :<>: ShowKindedScope n l l+      :$$: 'Text "but the inferred extended (inner) scope is"+      :$$: 'Text "  " :<>: ShowKindedScope n n l+      :$$: ShowLocalizeError msg icon 0 pattern n l+      )++type GValidNameBinders :: (s -> s -> Type) -> (LoT (s -> s -> Type) -> Type) -> Constraint+type family GValidNameBinders pattern f :: Constraint where+  GValidNameBinders pattern (f :: LoT (s -> s -> Type) -> Type) =+    (GInnerScopeOfRepK ('Text "") 0 0 pattern f Var0 Var0 Var1)+    ~ (Var1 :: Atom (s -> s -> Type) s)++type AtomSucc :: Atom d k1 -> Atom (k -> d) k1+type family AtomSucc atom where+  AtomSucc (Var i) = Var (VS i)++type AtomUnSucc :: ErrorMessage -> Nat -> (s -> s -> Type) -> Atom d s -> Atom d s -> Atom (k -> d) k1 -> Atom d k1+type family AtomUnSucc msg icon pattern oo ll atom where+  AtomUnSucc msg icon pattern oo ll (Var (VS i)) = Var i+  AtomUnSucc msg icon pattern oo ll (Var VZ) = TypeError+    ('Text "Intermediate scope escapes existential quantification for data type"+      :$$: ShowLocalizeError msg icon 0 pattern oo ll+      )++type family First x y where+  First (Var x) (Var y) = Var x++type family AndShowFieldNumber ifield msg where+  AndShowFieldNumber 0 msg = msg+  AndShowFieldNumber n msg =+    'Text "when checking field number " :<>: 'ShowType n+    :$$: msg++type family AndShowConNumber icon msg where+  AndShowConNumber 0 msg = msg+  AndShowConNumber n msg =+    'Text "when checking constructor number " :<>: 'ShowType n+    :$$: msg++type AndShowDataType pattern n l msg =+  'Text "when tracking Foil scopes for the data type"+  :$$: 'Text "  " :<>: ShowSaturatedPatternType pattern n n l l+  :$$: msg++type ShowLocalizeError msg icon ifield pattern o l =+    AndShowFieldNumber ifield+      (AndShowConNumber icon+        (AndShowDataType pattern o l+          msg))++type family CountCons f where+  CountCons (f :+: g) = CountCons f + CountCons g+  CountCons (M1 GHC.C c f) = 1++type family CountFields f where+  CountFields (f :*: g) = CountFields f + CountFields g+  CountFields (M1 GHC.S c f) = 1++type GInnerScopeOfRepK :: ErrorMessage -> Nat -> Nat -> (s -> s -> Type) -> (LoT k -> Type) -> Atom k s -> Atom k s -> Atom k s -> Atom k s+type family GInnerScopeOfRepK msg icon ifield pattern f o n l where+  GInnerScopeOfRepK msg icon ifield pattern V1 o n l = l+  GInnerScopeOfRepK msg icon ifield pattern U1 o n l = n+  GInnerScopeOfRepK msg icon ifield pattern (M1 GHC.C c f) o n l =+    GInnerScopeOfRepK msg icon 1 pattern f o n l+  GInnerScopeOfRepK msg icon ifield pattern (M1 GHC.D c f) o n l =+    GInnerScopeOfRepK msg 1 ifield pattern f o n l+  GInnerScopeOfRepK msg icon ifield pattern (M1 i c f) o n l =+    GInnerScopeOfRepK msg icon ifield pattern f o n l+  GInnerScopeOfRepK msg icon ifield pattern (f :+: g) o n l = First+    (SameInnerScope msg icon pattern (GInnerScopeOfRepK msg icon ifield pattern f o n l) l)+    (SameInnerScope msg icon pattern (GInnerScopeOfRepK msg (icon + CountCons f) ifield pattern g o n l) l)+  GInnerScopeOfRepK msg icon ifield pattern (f :*: g) o n l =+    GInnerScopeOfRepK msg icon (ifield + CountFields f) pattern g o+      (GInnerScopeOfRepK msg icon ifield pattern f o n l) l+  GInnerScopeOfRepK msg icon ifield pattern (Var i :~~: Var j :=>: f) o n l =+    GInnerScopeOfRepK msg icon ifield pattern (SubstInRepK i (Var j) f)+      (SubstInAtom i (Var j) o) (SubstInAtom i (Var j) n) (SubstInAtom i (Var j) l)+  GInnerScopeOfRepK msg icon ifield pattern (Exists k f) o n l =+    AtomUnSucc msg icon pattern o l+      (GInnerScopeOfRepK msg icon ifield pattern f (AtomSucc o) (AtomSucc n) (AtomSucc l))+  GInnerScopeOfRepK msg icon ifield pattern (Field atom) o n l = GInnerScopeOfAtom msg icon ifield pattern atom o n l+  GInnerScopeOfRepK msg icon ifield pattern f o n l =+    TypeError+      ('Text "Unsupported structure in a binder/pattern"+      :$$: 'Text "  " :<>: 'ShowType f+      :$$: ShowLocalizeError msg icon 0 pattern n l)++type PutBackLoT :: TyVar d s -> s -> LoT k -> LoT k+type family PutBackLoT i c bs where+  PutBackLoT VZ c (b :&&: bs) = c :&&: bs+  PutBackLoT (VS x) c (b :&&: bs) = b :&&: PutBackLoT x c bs

@@ -1,4 +1,6 @@ {-# LANGUAGE DataKinds             #-}+{-# LANGUAGE TypeOperators         #-}+{-# LANGUAGE TypeFamilies         #-} {-# LANGUAGE DeriveAnyClass        #-} {-# LANGUAGE DeriveGeneric         #-} {-# LANGUAGE FlexibleContexts      #-}@@ -23,13 +25,18 @@ import qualified Control.Monad.Foil.Internal as Foil import qualified Control.Monad.Foil.Relative as Foil import           Data.Bifoldable+import           Data.Bitraversable import           Data.Bifunctor-import           Data.Bifunctor.Sum+import Data.ZipMatchK+import qualified Generics.Kind as Kind+import Generics.Kind (GenericK(..), Field, Exists, Var0, Var1, (:$:), Atom((:@:), Kon), (:+:), (:*:)) import           Data.Coerce                 (coerce) import           Data.Map                    (Map) import qualified Data.Map                    as Map+import           Data.Maybe                  (mapMaybe) import           Data.Monoid                 (All (..)) import           GHC.Generics                (Generic)+import           Unsafe.Coerce               (unsafeCoerce)  -- | Scoped term under a (single) name binder. data ScopedAST binder sig n where@@ -50,15 +57,26 @@ deriving instance (forall x y. NFData (binder x y), forall scope term. (NFData scope, NFData term) => NFData (sig scope term))   => NFData (AST binder sig n) -instance (Bifunctor sig, Foil.CoSinkable binder) => Foil.Sinkable (AST binder sig) where-  sinkabilityProof rename = \case-    Var name -> Var (rename name)-    Node node -> Node (bimap f (Foil.sinkabilityProof rename) node)-    where-      f (ScopedAST binder body) =-        Foil.extendRenaming rename binder $ \rename' binder' ->-          ScopedAST binder' (Foil.sinkabilityProof rename' body)+instance GenericK (ScopedAST binder sig) where+  type RepK (ScopedAST binder sig) =+    Exists Foil.S+      (Field (Kon binder :@: Var1 :@: Var0) :*: Field (Kon AST :@: Kon binder :@: Kon sig :@: Var0))+  toK (Kind.Exists (Kind.Field binder Kind.:*: Kind.Field ast)) = ScopedAST binder ast+  fromK (ScopedAST binder ast) = Kind.Exists (Kind.Field binder Kind.:*: Kind.Field ast) +instance GenericK (AST binder sig) where+  type RepK (AST binder sig) =+    Field (Foil.Name :$: Var0)+    :+: Field (sig+                :$: (Kon ScopedAST :@: Kon binder :@: Kon sig :@: Var0)+                :@: (Kon AST :@: Kon binder :@: Kon sig :@: Var0))++instance (Bifunctor sig, Foil.CoSinkable binder, Foil.SinkableK binder) => Foil.Sinkable (ScopedAST binder sig)+instance (Bifunctor sig, Foil.CoSinkable binder, Foil.SinkableK binder) => Foil.Sinkable (AST binder sig)++instance (Bifunctor sig, Foil.CoSinkable binder, Foil.SinkableK binder) => Foil.SinkableK (ScopedAST binder sig)+instance (Bifunctor sig, Foil.CoSinkable binder, Foil.SinkableK binder) => Foil.SinkableK (AST binder sig)+ instance Foil.InjectName (AST binder sig) where   injectName = Var @@ -66,7 +84,7 @@  -- | Substitution for free (scoped monads). substitute-  :: (Bifunctor sig, Foil.Distinct o, Foil.CoSinkable binder)+  :: (Bifunctor sig, Foil.Distinct o, Foil.CoSinkable binder, Foil.SinkableK binder)   => Foil.Scope o   -> Foil.Substitution (AST binder sig) i o   -> AST binder sig i@@ -91,7 +109,7 @@ -- -- In general, 'substitute' is more efficient since it does not always refresh binders. substituteRefreshed-  :: (Bifunctor sig, Foil.Distinct o, Foil.CoSinkable binder)+  :: (Bifunctor sig, Foil.Distinct o, Foil.CoSinkable binder, Foil.SinkableK binder)   => Foil.Scope o   -> Foil.Substitution (AST binder sig) i o   -> AST binder sig i@@ -108,7 +126,8 @@         in ScopedAST binder' body'  -- | @'AST' sig@ is a monad relative to 'Foil.Name'.-instance (Bifunctor sig, Foil.CoSinkable binder) => Foil.RelMonad Foil.Name (AST binder sig) where+instance (Bifunctor sig, Foil.CoSinkable binder, Foil.SinkableK binder)+  => Foil.RelMonad Foil.Name (AST binder sig) where   rreturn = Var   rbind scope term subst =     case term of@@ -124,7 +143,7 @@  -- | Substitution for a single generalized pattern. substitutePattern-  :: (Bifunctor sig, Foil.Distinct o, Foil.CoSinkable binder', Foil.CoSinkable binder)+  :: (Bifunctor sig, Foil.Distinct o, Foil.CoSinkable binder', Foil.CoSinkable binder, Foil.SinkableK binder)   => Foil.Scope o                           -- ^ Resulting scope.   -> Foil.Substitution (AST binder sig) n o -- ^ Environment mapping names in scope @n@.   -> binder' n i                            -- ^ Binders that extend scope @n@ to scope @i@.@@ -140,7 +159,7 @@  -- | Refresh (force) all binders in a term, minimizing the used indices. refreshAST-  :: (Bifunctor sig, Foil.Distinct n, Foil.CoSinkable binder)+  :: (Bifunctor sig, Foil.Distinct n, Foil.CoSinkable binder, Foil.SinkableK binder)   => Foil.Scope n   -> AST binder sig n   -> AST binder sig n@@ -149,7 +168,7 @@   Node t -> Node (bimap (refreshScopedAST scope) (refreshAST scope) t)  -- | Similar to `refreshAST`, but for scoped terms.-refreshScopedAST :: (Bifunctor sig, Foil.Distinct n, Foil.CoSinkable binder)+refreshScopedAST :: (Bifunctor sig, Foil.Distinct n, Foil.CoSinkable binder, Foil.SinkableK binder)   => Foil.Scope n   -> ScopedAST binder sig n   -> ScopedAST binder sig n@@ -165,7 +184,7 @@ -- Compared to 'alphaEquiv', this function may perform some unnecessary -- changes of bound variables when the binders are the same on both sides. alphaEquivRefreshed-  :: (Bifunctor sig, Bifoldable sig, ZipMatch sig, Foil.Distinct n, Foil.UnifiablePattern binder)+  :: (Bitraversable sig, ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder, Foil.SinkableK binder)   => Foil.Scope n   -> AST binder sig n   -> AST binder sig n@@ -178,21 +197,21 @@ -- Compared to 'alphaEquivRefreshed', this function might skip unnecessary -- changes of bound variables when both binders in two matching scoped terms coincide. alphaEquiv-  :: (Bifunctor sig, Bifoldable sig, ZipMatch sig, Foil.Distinct n, Foil.UnifiablePattern binder)+  :: (Bitraversable sig, ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder, Foil.SinkableK binder)   => Foil.Scope n   -> AST binder sig n   -> AST binder sig n   -> Bool alphaEquiv _scope (Var x) (Var y) = x == coerce y alphaEquiv scope (Node l) (Node r) =-  case zipMatch l r of+  case zipMatch2 l r of     Nothing -> False     Just tt -> getAll (bifoldMap (All . uncurry (alphaEquivScoped scope)) (All . uncurry (alphaEquiv scope)) tt) alphaEquiv _ _ _ = False  -- | Same as 'alphaEquiv' but for scoped terms. alphaEquivScoped-  :: (Bifunctor sig, Bifoldable sig, ZipMatch sig, Foil.Distinct n, Foil.UnifiablePattern binder)+  :: (Bitraversable sig, ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder, Foil.SinkableK binder)   => Foil.Scope n   -> ScopedAST binder sig n   -> ScopedAST binder sig n@@ -237,20 +256,20 @@ -- scope extensions under binders (which might happen due to substitution -- under a binder in absence of name conflicts). unsafeEqAST-  :: (Bifoldable sig, ZipMatch sig, Foil.UnifiablePattern binder, Foil.Distinct n, Foil.Distinct l)+  :: (Bitraversable sig, ZipMatchK sig, Foil.UnifiablePattern binder, Foil.Distinct n, Foil.Distinct l)   => AST binder sig n   -> AST binder sig l   -> Bool unsafeEqAST (Var x) (Var y) = x == coerce y unsafeEqAST (Node t1) (Node t2) =-  case zipMatch t1 t2 of+  case zipMatch2 t1 t2 of     Nothing -> False     Just tt -> getAll (bifoldMap (All . uncurry unsafeEqScopedAST) (All . uncurry unsafeEqAST) tt) unsafeEqAST _ _ = False  -- | A version of 'unsafeEqAST' for scoped terms. unsafeEqScopedAST-  :: (Bifoldable sig, ZipMatch sig, Foil.UnifiablePattern binder, Foil.Distinct n, Foil.Distinct l)+  :: (Bitraversable sig, ZipMatchK sig, Foil.UnifiablePattern binder, Foil.Distinct n, Foil.Distinct l)   => ScopedAST binder sig n   -> ScopedAST binder sig l   -> Bool@@ -260,20 +279,6 @@       (Foil.Distinct, Foil.Distinct) -> body1 `unsafeEqAST` body2   ] --- ** Syntactic matching (unification)---- | Perform one-level matching for the two (non-variable) terms.-class ZipMatch sig where-  zipMatch-    :: sig scope term     -- ^ Left non-variable term.-    -> sig scope' term'   -- ^ Right non-variable term.-    -> Maybe (sig (scope, scope') (term, term'))--instance (ZipMatch f, ZipMatch g) => ZipMatch (Sum f g) where-  zipMatch (L2 f) (L2 f') = L2 <$> zipMatch f f'-  zipMatch (R2 g) (R2 g') = R2 <$> zipMatch g g'-  zipMatch _ _            = Nothing- -- * Converting to and from free foil  -- ** Convert to free foil@@ -389,3 +394,23 @@   ScopedAST binder body ->     ( makePattern binder     , makeScoped (convertFromAST fromSig fromVar makePattern makeScoped f body))++-- ** Unsinking AST++-- | Unsink an AST from a larger scope to a smaller scope.+unsinkAST :: (Foil.Distinct l, Foil.CoSinkable binder, Bifoldable sig) => Foil.Scope n -> AST binder sig l -> Maybe (AST binder sig n)+unsinkAST scope term+  | all (`Foil.member` scope) (freeVarsOf term) = Just (unsafeCoerce term)+  | otherwise = Nothing++-- | Get the free variables of an AST.+freeVarsOf :: (Foil.Distinct n, Foil.CoSinkable binder, Bifoldable sig) => AST binder sig n -> [Foil.Name n]+freeVarsOf = \case+  Var name -> [name]+  Node node -> bifoldMap freeVarsOfScopedAST freeVarsOf node++-- | Get the free variables of a scoped AST.+freeVarsOfScopedAST :: (Foil.Distinct n, Foil.CoSinkable binder, Bifoldable sig) => ScopedAST binder sig n -> [Foil.Name n]+freeVarsOfScopedAST (ScopedAST binder body) =+  case Foil.assertDistinct binder of+    Foil.Distinct -> mapMaybe (Foil.unsinkNamePattern binder) (freeVarsOf body)

@@ -1,196 +0,0 @@-{-# OPTIONS_GHC -Wno-missing-methods #-}-{-# LANGUAGE AllowAmbiguousTypes      #-}-{-# LANGUAGE ConstraintKinds          #-}-{-# LANGUAGE DataKinds                #-}-{-# LANGUAGE DefaultSignatures        #-}-{-# LANGUAGE FlexibleContexts         #-}-{-# LANGUAGE FlexibleInstances        #-}-{-# LANGUAGE GADTs                    #-}-{-# LANGUAGE InstanceSigs             #-}-{-# LANGUAGE MultiParamTypeClasses    #-}-{-# LANGUAGE PolyKinds                #-}-{-# LANGUAGE RankNTypes               #-}-{-# LANGUAGE ScopedTypeVariables      #-}-{-# LANGUAGE StandaloneKindSignatures #-}-{-# LANGUAGE TypeApplications         #-}-{-# LANGUAGE TypeFamilies             #-}-{-# LANGUAGE TypeOperators            #-}-{-# LANGUAGE UndecidableInstances     #-}-module Control.Monad.Free.Foil.Generic where--import           Data.Kind              (Constraint, Type)-import           Generics.Kind-import           Generics.Kind.Examples ()-import           GHC.TypeError--type ZipLoT :: LoT k -> LoT k -> LoT k-type family ZipLoT as bs where-  ZipLoT LoT0 LoT0 = LoT0-  ZipLoT (a :&&: as) (b :&&: bs) = ((a, b) :&&: ZipLoT as bs)--type Mappings :: LoT k -> LoT k -> LoT k -> Type-data Mappings (as :: LoT k) (bs :: LoT k) (cs :: LoT k) where-  M0 :: Mappings LoT0 LoT0 LoT0-  (:^:) :: (a -> b -> Maybe c) -> Mappings as bs cs -> Mappings (a :&&: as) (b :&&: bs) (c :&&: cs)--class PairMappings (as :: LoT k) (bs :: LoT k) where-  pairMappings :: Mappings as bs (ZipLoT as bs)--instance PairMappings LoT0 LoT0 where-  pairMappings = M0--instance PairMappings as bs => PairMappings ((a :: Type) :&&: as) ((b :: Type) :&&: bs) where-  pairMappings = (\x y -> Just (x, y)) :^: pairMappings--class ApplyMappings (v :: TyVar d Type) where-  applyMappings :: forall (as :: LoT d) (bs :: LoT d) (cs :: LoT d).-    Mappings as bs cs -> Interpret (Var v) as -> Interpret (Var v) bs -> Maybe (Interpret (Var v) cs)--instance ApplyMappings (VZ :: TyVar (Type -> tys) Type) where-  applyMappings (f :^: _) x y = f x y--instance ApplyMappings v => ApplyMappings (VS v :: TyVar (ty -> tys) Type) where-  applyMappings (_ :^: fs) x y = applyMappings @_ @v fs x y--genericZipMatchK :: forall f as bs.-    (GenericK f, GZipMatch (RepK f), ReqsZipMatch (RepK f) as bs, PairMappings as bs)-    => f :@@: as -> f :@@: bs -> Maybe (f :@@: (ZipLoT as bs))-genericZipMatchK = genericZipMatchWithK @f @as @bs pairMappings--genericZipMatchWithK :: forall f as bs cs.-    (GenericK f, GZipMatch (RepK f), ReqsZipMatchWith (RepK f) as bs cs)-    => Mappings as bs cs -> f :@@: as -> f :@@: bs -> Maybe (f :@@: cs)-genericZipMatchWithK mappings x y = toK @_ @f @cs <$> gzipMatchWith mappings-  (fromK @_ @f @as x)-  (fromK @_ @f @bs y)--genericZipMatch2-   :: forall sig scope scope' term term'.-   (GenericK sig, GZipMatch (RepK sig), ReqsZipMatch (RepK sig) (scope :&&: term :&&: 'LoT0) (scope' :&&: term' :&&: 'LoT0))-   => sig scope term -> sig scope' term' -> Maybe (sig (scope, scope') (term, term'))-genericZipMatch2 = genericZipMatchK @sig @(scope :&&: term :&&: 'LoT0) @(scope' :&&: term' :&&: 'LoT0)--zipMatchK :: forall f as bs. (ZipMatchK f, PairMappings as bs) => f :@@: as -> f :@@: bs -> Maybe (f :@@: ZipLoT as bs)-zipMatchK = zipMatchWithK @_ @f @as @bs pairMappings--class ZipMatchK (f :: k) where-  zipMatchWithK :: forall as bs cs. Mappings as bs cs -> f :@@: as -> f :@@: bs -> Maybe (f :@@: cs)-  default zipMatchWithK :: forall as bs cs.-    (GenericK f, GZipMatch (RepK f), ReqsZipMatchWith (RepK f) as bs cs)-    => Mappings as bs cs -> f :@@: as -> f :@@: bs -> Maybe (f :@@: cs)-  zipMatchWithK = genericZipMatchWithK @f @as @bs @cs--zipMatchViaEq :: Eq a => Mappings as bs cs -> a -> a -> Maybe a-zipMatchViaEq _ x y-  | x == y = Just x-  | otherwise = Nothing--zipMatchViaChooseLeft :: Mappings as bs cs -> a -> a -> Maybe a-zipMatchViaChooseLeft _ x _ = Just x---- instance ZipMatchK (,)     -- missing GenericK instance upstream-instance ZipMatchK []-instance ZipMatchK Maybe-instance ZipMatchK Either-instance ZipMatchK a => ZipMatchK (Either a)--type ReqsZipMatch f as bs = ReqsZipMatchWith f as bs (ZipLoT as bs)-class GZipMatch (f :: LoT k -> Type) where-  type ReqsZipMatchWith f (as :: LoT k) (bs :: LoT k) (cs :: LoT k) :: Constraint-  gzipMatchWith :: ReqsZipMatchWith f as bs cs => Mappings as bs cs -> f as -> f bs -> Maybe (f cs)--instance GZipMatch V1 where-  type ReqsZipMatchWith V1 as bs cs = ()-  gzipMatchWith _ _ _ = error "impossible: Generics.Kind.V1 value!" -- FIXME: should be absurd--instance GZipMatch U1 where-  type ReqsZipMatchWith U1 as bs cs = ()-  gzipMatchWith _ U1 U1 = Just U1--instance GZipMatch f => GZipMatch (M1 i c f) where-  type ReqsZipMatchWith (M1 i c f) as bs cs = ReqsZipMatchWith f as bs cs-  gzipMatchWith g (M1 x) (M1 y) = M1 <$> gzipMatchWith g x y--instance (GZipMatch f, GZipMatch g) => GZipMatch (f :+: g) where-  type ReqsZipMatchWith (f :+: g) as bs cs = (ReqsZipMatchWith f as bs cs, ReqsZipMatchWith g as bs cs)-  gzipMatchWith g (L1 x) (L1 y) = L1 <$> gzipMatchWith g x y-  gzipMatchWith g (R1 x) (R1 y) = R1 <$> gzipMatchWith g x y-  gzipMatchWith _ _ _           = Nothing--instance (GZipMatch f, GZipMatch g) => GZipMatch (f :*: g) where-  type ReqsZipMatchWith (f :*: g) as bs cs = (ReqsZipMatchWith f as bs cs, ReqsZipMatchWith g as bs cs)-  gzipMatchWith g (x :*: y) (x' :*: y') =-    liftA2 (:*:) (gzipMatchWith g x x') (gzipMatchWith g y y')--instance ZipMatchFields t => GZipMatch (Field t) where-  type ReqsZipMatchWith (Field t) as bs cs = ReqsZipMatchFieldsWith t as bs cs-  gzipMatchWith f x y = zipMatchFieldsWith f x y--instance GZipMatch f => GZipMatch (c :=>: f) where-  type ReqsZipMatchWith (c :=>: f) as bs cs = (ReqsZipMatchWith f as bs cs, Interpret c cs)-  -- really we want          = (Interpret c as, Interpret c bs) => (ReqsZipMatch f as bs, Interpret c (ZipLoT as bs))-  gzipMatchWith g (SuchThat x) (SuchThat y) = SuchThat <$> gzipMatchWith g x y--instance TypeError ('Text "Existentials are not supported")-         => GZipMatch (Exists k f) where-  type ReqsZipMatchWith (Exists k f) as bs cs = TypeError ('Text "Existentials are not supported")-  gzipMatchWith = undefined--class ZipMatchFields (t :: Atom d Type) where-  type ReqsZipMatchFieldsWith t (as :: LoT d) (bs :: LoT d) (cs :: LoT d) :: Constraint-  zipMatchFieldsWith :: ReqsZipMatchFieldsWith t as bs cs => Mappings as bs cs -> Field t as -> Field t bs -> Maybe (Field t cs)--instance ApplyMappings v => ZipMatchFields (Var v) where-  -- this is always true, but GHC is not smart enough to know that, I think-  type ReqsZipMatchFieldsWith (Var v) as bs cs = () -- InterpretVar v cs ~ (InterpretVar v as, InterpretVar v bs))-  zipMatchFieldsWith g (Field x) (Field y) = Field <$> applyMappings @_ @v g x y--instance ZipMatchK k => ZipMatchFields (Kon k) where-  type ReqsZipMatchFieldsWith (Kon k) as bs cs = ()-  zipMatchFieldsWith _ (Field l) (Field r) = Field <$> zipMatchWithK @_ @k M0 l r--instance (ZipMatchFields t, ZipMatchK k) => ZipMatchFields (Kon k :@: t) where-  type ReqsZipMatchFieldsWith (Kon k :@: t) as bs cs = ReqsZipMatchFieldsWith t as bs cs--  zipMatchFieldsWith :: forall as bs cs. ReqsZipMatchFieldsWith (Kon k :@: t) as bs cs =>-    Mappings as bs cs -> Field (Kon k :@: t) as -> Field (Kon k :@: t) bs -> Maybe (Field (Kon k :@: t) cs)-  zipMatchFieldsWith g (Field l) (Field r) =-    Field <$> zipMatchWithK @_ @k @(Interpret t as :&&: LoT0) @(Interpret t bs :&&: LoT0) @(Interpret t cs :&&: LoT0)-      ((\ll rr -> unField @t <$> zipMatchFieldsWith g (Field ll) (Field rr)) :^: M0) l r--instance (ZipMatchFields t1, ZipMatchFields t2, ZipMatchK k) => ZipMatchFields ((Kon k :@: t1) :@: t2) where-  type ReqsZipMatchFieldsWith ((Kon k :@: t1) :@: t2) as bs cs = (ReqsZipMatchFieldsWith t1 as bs cs, ReqsZipMatchFieldsWith t2 as bs cs)--  zipMatchFieldsWith :: forall as bs cs. ReqsZipMatchFieldsWith ((Kon k :@: t1) :@: t2) as bs cs =>-    Mappings as bs cs -> Field ((Kon k :@: t1) :@: t2) as -> Field ((Kon k :@: t1) :@: t2) bs -> Maybe (Field ((Kon k :@: t1) :@: t2) cs)-  zipMatchFieldsWith g (Field l) (Field r) =-    Field <$> zipMatchWithK @_ @k @(Interpret t1 as :&&: Interpret t2 as :&&: LoT0) @(Interpret t1 bs :&&: Interpret t2 bs :&&: LoT0) @(Interpret t1 cs :&&: Interpret t2 cs :&&: LoT0)-      ((\ll rr -> unField @t1 <$> zipMatchFieldsWith g (Field ll) (Field rr))-        :^: ((\ll rr -> unField @t2 <$> zipMatchFieldsWith g (Field ll) (Field rr))-        :^: M0)) l r--instance {-# OVERLAPPABLE #-} TypeError ('Text "Atom :@: is not supported by ZipMatchFields is a general form") => ZipMatchFields (f :@: t) where-  -- type ReqsZipMatchFieldsWith (f :@: t) as bs cs = TypeError ('Text "Atom :@: is not supported by ZipMatchFields is a general form")-  zipMatchFieldsWith = undefined--instance TypeError ('Text "Atom ForAll is not supported by ZipMatchFields") => ZipMatchFields (ForAll a) where-  type ReqsZipMatchFieldsWith (ForAll a) as bs cs = TypeError ('Text "Atom ForAll is not supported by ZipMatchFields")-  zipMatchFieldsWith = undefined-instance TypeError ('Text "Atom :=>>: is not supported by ZipMatchFields") => ZipMatchFields (c :=>>: a) where-  type ReqsZipMatchFieldsWith (c :=>>: a) as bs cs = TypeError ('Text "Atom :=>>: is not supported by ZipMatchFields")-  zipMatchFieldsWith = undefined-instance TypeError ('Text "Atom Eval is not supported by ZipMatchFields") => ZipMatchFields (Eval a) where-  type ReqsZipMatchFieldsWith (Eval a) as bs cs = TypeError ('Text "Atom Eval is not supported by ZipMatchFields")-  zipMatchFieldsWith = undefined---- instance ZipMatchFields (ForAll f) where---   type ReqsZipMatchFields (ForAll f) as bs = ???---   zipMatchFields = ???---- instance ZipMatchFields (c :=>>: f) where---   type ReqsZipMatchFields (c :=>>: f) as bs = ???---   zipMatchFields = ???---- instance ZipMatchFields (Eval f) where---   type ReqsZipMatchFields (Eval f) as bs = ???---   zipMatchFields = ???

@@ -2,10 +2,8 @@   module Control.Monad.Free.Foil.TH.Signature,   module Control.Monad.Free.Foil.TH.PatternSynonyms,   module Control.Monad.Free.Foil.TH.Convert,-  module Control.Monad.Free.Foil.TH.ZipMatch, ) where  import Control.Monad.Free.Foil.TH.Signature import Control.Monad.Free.Foil.TH.PatternSynonyms import Control.Monad.Free.Foil.TH.Convert-import Control.Monad.Free.Foil.TH.ZipMatch

@@ -83,7 +83,7 @@       where         l = mkName ("l" ++ show i) -    mkPatternName conName = mkName (dropEnd (length "Sig") (nameBase conName))+    mkPatternName conName = mkName (dropEnd (length ("Sig" :: String)) (nameBase conName))     dropEnd k = reverse . drop k . reverse      collapse = \case

@@ -1,57 +0,0 @@-{-# OPTIONS_GHC -fno-warn-type-defaults      #-}-{-# LANGUAGE LambdaCase      #-}-{-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE ViewPatterns    #-}-module Control.Monad.Free.Foil.TH.ZipMatch where--import           Language.Haskell.TH--import           Control.Monad.Foil.TH.Util-import           Control.Monad.Free.Foil---- | Generate 'ZipMatch' instance for a given bifunctor.-deriveZipMatch-  :: Name -- ^ Type name for the signature bifunctor.-  -> Q [Dec]-deriveZipMatch signatureT = do-  TyConI (DataD _ctx _name signatureTVars _kind signatureCons _deriv) <- reify signatureT--  case reverse signatureTVars of-    (tvarName -> term) : (tvarName -> scope) : (reverse -> params) -> do-      let signatureType = PeelConT signatureT (map (VarT . tvarName) params)-      clauses <- concat <$> mapM (toClause scope term) signatureCons-      let defaultClause = Clause [WildP, WildP] (NormalB (ConE 'Nothing)) []-      let instType = AppT (ConT ''ZipMatch) signatureType--      return-        [ InstanceD Nothing [] instType-          [ FunD 'zipMatch (clauses ++ [defaultClause]) ]-        ]-    _ -> fail "cannot generate pattern synonyms"--  where-    toClause :: Name -> Name -> Con -> Q [Clause]-    toClause scope term = go-      where-        go = \case-          NormalC conName types -> mkClause conName types-          RecC conName types -> go (NormalC conName (map removeName types))-          InfixC l conName r -> go (NormalC conName [l, r])-          ForallC _ _ con -> go con-          GadtC conNames types _retType -> concat <$> mapM (\conName -> mkClause conName types) conNames-          RecGadtC conNames types retType -> go (GadtC conNames (map removeName types) retType)--        mkClause :: Name -> [BangType] -> Q [Clause]-        mkClause conName types = return-          [Clause [ConP conName [] lpats, ConP conName [] rpats]-            (NormalB (AppE (ConE 'Just) (foldl AppE (ConE conName) args))) []]-          where-            (lpats, rpats, args) = unzip3-              [ case type_ of-                  VarT typeName-                    | typeName `elem` [scope, term] -> (VarP l, VarP r, TupE [Just (VarE l), Just (VarE r)])-                  _ -> (VarP l, WildP, VarE l)-              | (i, (_bang, type_)) <- zip [0..] types-              , let l = mkName ("l" ++ show i)-              , let r = mkName ("r" ++ show i)-              ]

@@ -0,0 +1,80 @@+{-# OPTIONS_GHC -Wno-redundant-constraints #-}+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeOperators #-}+-- | Kind-polymorphic syntactic (first-order) unification.+module Data.ZipMatchK (+  module Data.ZipMatchK.Mappings,+  ZipMatchK(..),+  zipMatchK,+  -- * Specializations+  -- ** Unification of plain 'Data.Kind.Type's+  zipMatchViaEq,+  zipMatchViaChooseLeft,+  -- ** Unification of 'Data.Functor.Functor's+  zipMatchWith1,+  zipMatch1,+  -- ** Unification of 'Data.Bifunctor.Bifunctor's+  zipMatchWith2,+  zipMatch2,+) where++import           Generics.Kind+import Data.Bitraversable++import Data.ZipMatchK.Generic+import Data.ZipMatchK.Mappings++-- | Perform one level of equality testing for two values and pair up components using @(,)@:+--+-- > zipMatchK = zipMatchWithK (\x y -> Just (,) :^: M0)+zipMatchK :: forall f as bs. (ZipMatchK f, PairMappings as bs) => f :@@: as -> f :@@: bs -> Maybe (f :@@: ZipLoT as bs)+zipMatchK = zipMatchWithK @_ @f @as @bs pairMappings++-- | Unify values via 'Eq'.+-- Can be used as an implementation of 'zipMatchWithK' when @k = 'Data.Kind.Type'@.+zipMatchViaEq :: Eq a => Mappings as bs cs -> a -> a -> Maybe a+zipMatchViaEq _ x y+  | x == y = Just x+  | otherwise = Nothing++-- | Always successfully unify any two values of type @a@ by preferring the left value.+-- Can be used as an implementation of 'zipMatchWithK' when @k = 'Data.Kind.Type'@.+zipMatchViaChooseLeft :: Mappings as bs cs -> a -> a -> Maybe a+zipMatchViaChooseLeft _ x _ = Just x++-- | 'zipMatchWithK' specialised to functors.+--+-- Note: 'Traversable' is a morally correct constraint here.+zipMatchWith1+  :: (Traversable f, ZipMatchK f)+  => (a -> a' -> Maybe a'')+  -> f a -> f a' -> Maybe (f a'')+zipMatchWith1 f = zipMatchWithK (f :^: M0)++-- | 'zipMatchK' specialised to functors.+--+-- Note: 'Traversable' is a morally correct constraint here.+zipMatch1 :: (Traversable f, ZipMatchK f) => f a -> f a' -> Maybe (f (a, a'))+zipMatch1 = zipMatchWith1 pairA+-- | 'zipMatchWithK' specialised to bifunctors.+--+-- Note: 'Bitraversable' is a morally correct constraint here.+zipMatchWith2+  :: (Bitraversable f, ZipMatchK f)+  => (a -> a' -> Maybe a'')+  -> (b -> b' -> Maybe b'')+  -> f a b -> f a' b' -> Maybe (f a'' b'')+zipMatchWith2 f g = zipMatchWithK (f :^: g :^: M0)++-- | 'zipMatchK' specialised to bifunctors.+--+-- Note: 'Bitraversable' is a morally correct constraint here.+zipMatch2 :: (Bitraversable f, ZipMatchK f) => f a b -> f a' b' -> Maybe (f (a, a') (b, b'))+zipMatch2 = zipMatchWith2 pairA pairA

@@ -0,0 +1,35 @@+{-# OPTIONS_GHC -Wno-orphans #-}+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeOperators #-}+-- | This module provides 'GenericK' and 'ZipMatchK' instances for 'Sum' and 'Product',+-- to enable the use of 'ZipMatchK' with the data types à la carte approach.+module Data.ZipMatchK.Bifunctor where++import Data.Kind (Type)+import Generics.Kind+import Data.Bitraversable+import Data.Bifunctor.Sum+import Data.Bifunctor.Product++import Data.ZipMatchK++instance GenericK (Sum f g) where+  type RepK (Sum f g) =+    Field ((Kon f :@: Var0) :@: Var1)+    :+: Field ((Kon g :@: Var0) :@: Var1)+instance GenericK (Product f g) where+  type RepK (Product f g) =+    Field ((Kon f :@: Var0) :@: Var1)+    :*: Field ((Kon g :@: Var0) :@: Var1)++-- | Note: instance is limited to 'Type'-kinded bifunctors @f@ and @g@.+instance (Bitraversable f, Bitraversable g, ZipMatchK f, ZipMatchK g) => ZipMatchK (Sum f (g :: Type -> Type -> Type))+-- | Note: instance is limited to 'Type'-kinded bifunctors @f@ and @g@.+instance (Bitraversable f, Bitraversable g, ZipMatchK f, ZipMatchK g) => ZipMatchK (Product f (g :: Type -> Type -> Type))

@@ -0,0 +1,34 @@+{-# OPTIONS_GHC -Wno-orphans #-}+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeOperators #-}+-- | This module provides 'GenericK' and 'ZipMatchK' instances for 'Sum' and 'Product',+-- to enable the use of 'ZipMatchK' with the data types à la carte approach.+module Data.ZipMatchK.Functor where++import Data.Kind (Type)+import Generics.Kind+import Data.Functor.Sum+import Data.Functor.Product++import Data.ZipMatchK++instance GenericK (Sum f g) where+  type RepK (Sum f g) =+    Field (Kon f :@: Var0)+    :+: Field (Kon g :@: Var0)+instance GenericK (Product f g) where+  type RepK (Product f g) =+    Field (Kon f :@: Var0)+    :*: Field (Kon g :@: Var0)++-- | Note: instance is limited to 'Type'-kinded bifunctors @f@ and @g@.+instance (Traversable f, Traversable g, ZipMatchK f, ZipMatchK g) => ZipMatchK (Sum f (g :: Type -> Type))+-- | Note: instance is limited to 'Type'-kinded bifunctors @f@ and @g@.+instance (Traversable f, Traversable g, ZipMatchK f, ZipMatchK g) => ZipMatchK (Product f (g :: Type -> Type))

@@ -0,0 +1,193 @@+{-# OPTIONS_GHC -Wno-missing-methods -Wno-orphans #-}+{-# LANGUAGE AllowAmbiguousTypes      #-}+{-# LANGUAGE ConstraintKinds          #-}+{-# LANGUAGE DataKinds                #-}+{-# LANGUAGE DefaultSignatures        #-}+{-# LANGUAGE FlexibleContexts         #-}+{-# LANGUAGE FlexibleInstances        #-}+{-# LANGUAGE GADTs                    #-}+{-# LANGUAGE InstanceSigs             #-}+{-# LANGUAGE MultiParamTypeClasses    #-}+{-# LANGUAGE PolyKinds                #-}+{-# LANGUAGE RankNTypes               #-}+{-# LANGUAGE ScopedTypeVariables      #-}+{-# LANGUAGE StandaloneKindSignatures #-}+{-# LANGUAGE TypeApplications         #-}+{-# LANGUAGE TypeFamilies             #-}+{-# LANGUAGE TypeOperators            #-}+{-# LANGUAGE UndecidableInstances     #-}+module Data.ZipMatchK.Generic where++import           Data.Kind              (Constraint, Type)+import           Data.List.NonEmpty+import           Generics.Kind+import           Generics.Kind.Examples ()+import           GHC.TypeError+import           Data.ZipMatchK.Mappings++-- | Kind-polymorphic syntactic (first-order) unification of two values.+--+-- Note: @f@ is expected to be a traversable n-functor,+-- but at the moment we lack a @TraversableK@ constraint.+class ZipMatchK (f :: k) where+  -- | Perform one level of equality testing:+  --+  -- * when @k = 'Type'@, values are compared directly (e.g. via 'Eq');+  -- * when @k = 'Type' -> 'Type'@, we compare term constructors;+  --   if term constructors are unequal, we return 'Nothing';+  --   otherwise, we pair up all components with a given function.+  zipMatchWithK :: forall as bs cs. Mappings as bs cs -> f :@@: as -> f :@@: bs -> Maybe (f :@@: cs)+  default zipMatchWithK :: forall as bs cs.+    (GenericK f, GZipMatch (RepK f), ReqsZipMatchWith (RepK f) as bs cs)+    => Mappings as bs cs -> f :@@: as -> f :@@: bs -> Maybe (f :@@: cs)+  zipMatchWithK = genericZipMatchWithK @f @as @bs @cs++-- | Generic implementation of 'Data.ZipMatch.zipMatchK'.+genericZipMatchK :: forall f as bs.+    (GenericK f, GZipMatch (RepK f), ReqsZipMatch (RepK f) as bs, PairMappings as bs)+    => f :@@: as -> f :@@: bs -> Maybe (f :@@: (ZipLoT as bs))+genericZipMatchK = genericZipMatchWithK @f @as @bs pairMappings++-- | Generic implementation of 'zipMatchWithK'.+genericZipMatchWithK :: forall f as bs cs.+    (GenericK f, GZipMatch (RepK f), ReqsZipMatchWith (RepK f) as bs cs)+    => Mappings as bs cs -> f :@@: as -> f :@@: bs -> Maybe (f :@@: cs)+genericZipMatchWithK mappings x y = toK @_ @f @cs <$> gzipMatchWith mappings+  (fromK @_ @f @as x)+  (fromK @_ @f @bs y)++instance GenericK (,) where+  type RepK (,) = Field Var0 :*: Field Var1+instance GenericK ((,) a) where+  type RepK ((,) a) = Field (Kon a) :*: Field Var0+instance GenericK NonEmpty where+  type RepK NonEmpty = Field Var0 :*: Field ([] :$: Var0)++instance ZipMatchK (,)+instance ZipMatchK a => ZipMatchK ((,) a)+instance ZipMatchK []+instance ZipMatchK Maybe+instance ZipMatchK Either+instance ZipMatchK a => ZipMatchK (Either a)+instance ZipMatchK NonEmpty++type ReqsZipMatch f as bs = ReqsZipMatchWith f as bs (ZipLoT as bs)+class GZipMatch (f :: LoT k -> Type) where+  type ReqsZipMatchWith f (as :: LoT k) (bs :: LoT k) (cs :: LoT k) :: Constraint+  gzipMatchWith :: ReqsZipMatchWith f as bs cs => Mappings as bs cs -> f as -> f bs -> Maybe (f cs)++instance GZipMatch V1 where+  type ReqsZipMatchWith V1 as bs cs = ()+  gzipMatchWith _ _ _ = error "impossible: Generics.Kind.V1 value!" -- FIXME: should be absurd++instance GZipMatch U1 where+  type ReqsZipMatchWith U1 as bs cs = ()+  gzipMatchWith _ U1 U1 = Just U1++instance GZipMatch f => GZipMatch (M1 i c f) where+  type ReqsZipMatchWith (M1 i c f) as bs cs = ReqsZipMatchWith f as bs cs+  gzipMatchWith g (M1 x) (M1 y) = M1 <$> gzipMatchWith g x y++instance (GZipMatch f, GZipMatch g) => GZipMatch (f :+: g) where+  type ReqsZipMatchWith (f :+: g) as bs cs = (ReqsZipMatchWith f as bs cs, ReqsZipMatchWith g as bs cs)+  gzipMatchWith g (L1 x) (L1 y) = L1 <$> gzipMatchWith g x y+  gzipMatchWith g (R1 x) (R1 y) = R1 <$> gzipMatchWith g x y+  gzipMatchWith _ _ _           = Nothing++instance (GZipMatch f, GZipMatch g) => GZipMatch (f :*: g) where+  type ReqsZipMatchWith (f :*: g) as bs cs = (ReqsZipMatchWith f as bs cs, ReqsZipMatchWith g as bs cs)+  gzipMatchWith g (x :*: y) (x' :*: y') =+    liftA2 (:*:) (gzipMatchWith g x x') (gzipMatchWith g y y')++instance ZipMatchFields t => GZipMatch (Field t) where+  type ReqsZipMatchWith (Field t) as bs cs = ReqsZipMatchFieldsWith t as bs cs+  gzipMatchWith f x y = zipMatchFieldsWith f x y++instance GZipMatch f => GZipMatch (c :=>: f) where+  type ReqsZipMatchWith (c :=>: f) as bs cs = (ReqsZipMatchWith f as bs cs, Interpret c cs)+  -- really we want          = (Interpret c as, Interpret c bs) => (ReqsZipMatch f as bs, Interpret c (ZipLoT as bs))+  gzipMatchWith g (SuchThat x) (SuchThat y) = SuchThat <$> gzipMatchWith g x y++instance TypeError ('Text "Existentials are not supported")+         => GZipMatch (Exists k f) where+  type ReqsZipMatchWith (Exists k f) as bs cs = TypeError ('Text "Existentials are not supported")+  gzipMatchWith = undefined++class ZipMatchFields (t :: Atom d Type) where+  type ReqsZipMatchFieldsWith t (as :: LoT d) (bs :: LoT d) (cs :: LoT d) :: Constraint+  zipMatchFieldsWith :: ReqsZipMatchFieldsWith t as bs cs => Mappings as bs cs -> Field t as -> Field t bs -> Maybe (Field t cs)++instance ApplyMappings v => ZipMatchFields (Var v) where+  -- this is always true, but GHC is not smart enough to know that, I think+  type ReqsZipMatchFieldsWith (Var v) as bs cs = () -- InterpretVar v cs ~ (InterpretVar v as, InterpretVar v bs))+  zipMatchFieldsWith g (Field x) (Field y) = Field <$> applyMappings @_ @v g x y++instance ZipMatchK k => ZipMatchFields (Kon k) where+  type ReqsZipMatchFieldsWith (Kon k) as bs cs = ()+  zipMatchFieldsWith _ (Field l) (Field r) = Field <$> zipMatchWithK @_ @k M0 l r++instance {-# OVERLAPPING #-} (ZipMatchFields t, ZipMatchK k) => ZipMatchFields (Kon k :@: t) where+  type ReqsZipMatchFieldsWith (Kon k :@: t) as bs cs = ReqsZipMatchFieldsWith t as bs cs++  zipMatchFieldsWith :: forall as bs cs. ReqsZipMatchFieldsWith (Kon k :@: t) as bs cs =>+    Mappings as bs cs -> Field (Kon k :@: t) as -> Field (Kon k :@: t) bs -> Maybe (Field (Kon (k :: Type -> Type) :@: t) cs)+  zipMatchFieldsWith g (Field l) (Field r) =+    Field <$> zipMatchWithK @_ @k @(Interpret t as :&&: LoT0) @(Interpret t bs :&&: LoT0) @(Interpret t cs :&&: LoT0)+      ((\ll rr -> unField @t <$> zipMatchFieldsWith g (Field ll) (Field rr)) :^: M0) l r++instance {-# OVERLAPPING #-} (ZipMatchFields t1, ZipMatchFields t2, ZipMatchK k) => ZipMatchFields ((Kon (k :: Type -> Type -> Type) :@: t1) :@: t2) where+  type ReqsZipMatchFieldsWith ((Kon k :@: t1) :@: t2) as bs cs = (ReqsZipMatchFieldsWith t1 as bs cs, ReqsZipMatchFieldsWith t2 as bs cs)++  zipMatchFieldsWith :: forall as bs cs. ReqsZipMatchFieldsWith ((Kon k :@: t1) :@: t2) as bs cs =>+    Mappings as bs cs -> Field ((Kon k :@: t1) :@: t2) as -> Field ((Kon k :@: t1) :@: t2) bs -> Maybe (Field ((Kon k :@: t1) :@: t2) cs)+  zipMatchFieldsWith g (Field l) (Field r) =+    Field <$> zipMatchWithK @_ @k @(Interpret t1 as :&&: Interpret t2 as :&&: LoT0) @(Interpret t1 bs :&&: Interpret t2 bs :&&: LoT0) @(Interpret t1 cs :&&: Interpret t2 cs :&&: LoT0)+      ((\ll rr -> unField @t1 <$> zipMatchFieldsWith g (Field ll) (Field rr))+        :^: ((\ll rr -> unField @t2 <$> zipMatchFieldsWith g (Field ll) (Field rr))+        :^: M0)) l r++instance {-# OVERLAPPABLE #-} TypeError+  ('Text "The type constructor is kind-polymorphic:"+  :$$: 'Text "  " :<>: 'ShowType k :<>: 'Text " : " :<>: 'ShowType (kk -> Type)+  :$$: 'Text "Possible fix:"+  :$$: 'Text "  add an explicit kind signature"+  :$$: 'Text "    " :<>: 'ShowType k :<>: 'Text " : " :<>: 'ShowType (Type -> Type))+  => ZipMatchFields (Kon (k :: kk -> Type) :@: t) where+  zipMatchFieldsWith = undefined++instance {-# OVERLAPPABLE #-} TypeError+  ('Text "The type constructor is kind-polymorphic:"+  :$$: 'Text "  " :<>: 'ShowType k :<>: 'Text " : " :<>: 'ShowType (kk1 -> kk2 -> Type)+  :$$: 'Text "Possible fix:"+  :$$: 'Text "  add an explicit kind signature"+  :$$: 'Text "    " :<>: 'ShowType k :<>: 'Text " : " :<>: 'ShowType (Type -> Type -> Type))+  => ZipMatchFields ((Kon (k :: kk1 -> kk2 -> Type) :@: t1) :@: t2) where+  zipMatchFieldsWith = undefined++instance {-# OVERLAPPABLE #-} TypeError+  ('Text "Atom :@: is not supported by ZipMatchFields is a general form:"+  :$$: 'Text "  when attempting to use a generic instance for"+  :$$: 'ShowType (f :@: t)+  :$$: 'ShowType f :<>: 'Text " : " :<>: 'ShowType (Atom d (k1 -> Type)))+  => ZipMatchFields ((f :: Atom d (k1 -> Type)) :@: t) where+  -- type ReqsZipMatchFieldsWith (f :@: t) as bs cs = TypeError ('Text "Atom :@: is not supported by ZipMatchFields is a general form")+  zipMatchFieldsWith = undefined++instance TypeError+  ('Text "Atom ForAll is not supported by ZipMatchFields"+  :$$: 'Text "  when attempting to use a generic instance for"+  :$$: 'ShowType (ForAll a)) => ZipMatchFields (ForAll a) where+  type ReqsZipMatchFieldsWith (ForAll a) as bs cs = TypeError ('Text "Atom ForAll is not supported by ZipMatchFields")+  zipMatchFieldsWith = undefined+instance TypeError+  ('Text "Atom :=>>: is not supported by ZipMatchFields"+  :$$: 'Text "  when attempting to use a generic instance for"+  :$$: 'ShowType (c :=>>: a)) => ZipMatchFields (c :=>>: a) where+  type ReqsZipMatchFieldsWith (c :=>>: a) as bs cs = TypeError ('Text "Atom :=>>: is not supported by ZipMatchFields")+  zipMatchFieldsWith = undefined+instance TypeError+  ('Text "Atom Eval is not supported by ZipMatchFields"+  :$$: 'Text "  when attempting to use a generic instance for"+  :$$: 'ShowType (Eval a)) => ZipMatchFields (Eval a) where+  type ReqsZipMatchFieldsWith (Eval a) as bs cs = TypeError ('Text "Atom Eval is not supported by ZipMatchFields")+  zipMatchFieldsWith = undefined

@@ -0,0 +1,60 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE StandaloneKindSignatures #-}+module Data.ZipMatchK.Mappings where++import           Data.Kind              (Type)+import           Generics.Kind++-- | Zip to lists of types into a single list of pair types.+type ZipLoT :: LoT k -> LoT k -> LoT k+type family ZipLoT as bs where+  ZipLoT LoT0 LoT0 = LoT0+  ZipLoT (a :&&: as) (b :&&: bs) = ((a, b) :&&: ZipLoT as bs)++infixr 5 :^:+type Mappings :: LoT k -> LoT k -> LoT k -> Type+-- | A collection of zipping functions for 'Data.ZipMatchK.zipMatchWithK'.+data Mappings (as :: LoT k) (bs :: LoT k) (cs :: LoT k) where+  -- | An empty collection (when there no (more) type parameters).+  M0 :: Mappings LoT0 LoT0 LoT0+  -- | A non-empty collection (when there is at least one type parameter).+  (:^:) :: (a -> b -> Maybe c)    -- ^ Zipping for the first type parameter.+        -> Mappings as bs cs      -- ^ Zipping for other type parameters.+        -> Mappings (a :&&: as) (b :&&: bs) (c :&&: cs)++class PairMappings (as :: LoT k) (bs :: LoT k) where+  -- | A collection of pairing functions @(\\x y -> Just (x, y))@ for 'Data.ZipMatchK.zipMatchK'.+  pairMappings :: Mappings as bs (ZipLoT as bs)++instance PairMappings LoT0 LoT0 where+  pairMappings = M0++instance PairMappings as bs => PairMappings ((a :: Type) :&&: as) ((b :: Type) :&&: bs) where+  pairMappings = pairA :^: pairMappings++class ApplyMappings (v :: TyVar d Type) where+  -- | Apply a collection of zipping functions to collections of values.+  applyMappings :: forall (as :: LoT d) (bs :: LoT d) (cs :: LoT d).+       Mappings as bs cs      -- ^ A collection of zipping functions.+    -> Interpret (Var v) as   -- ^ First collection of values (one per type parameter).+    -> Interpret (Var v) bs   -- ^ Second collection of values (one per type parameter).+    -> Maybe (Interpret (Var v) cs)++instance ApplyMappings (VZ :: TyVar (Type -> tys) Type) where+  applyMappings (f :^: _) x y = f x y++instance ApplyMappings v => ApplyMappings (VS v :: TyVar (ty -> tys) Type) where+  applyMappings (_ :^: fs) x y = applyMappings @_ @v fs x y++-- | Pair two values in a context.+pairA :: Applicative f => a -> b -> f (a, b)+pairA x y = pure (x, y)