free-foil 0.3.1 → 0.3.2

raw patch · 13 files changed

+1111/−9 lines, 13 filesdep +tasty-benchdep ~basePVP ok

version bump matches the API change (PVP)

Dependencies added: tasty-bench

Dependency ranges changed: base

API changes (from Hackage documentation)

Files

• ChangeLog.md +26/−0
• bench/normalize/Main.hs +56/−0
• bench/zipmatchk/Main.hs +134/−0
• bench/zipmatchk/Signature.hs +59/−0
• free-foil.cabal +52/−4
• src/Control/Monad/Foil.hs +1/−0
• src/Control/Monad/Foil/Internal.hs +36/−0
• src/Control/Monad/Free/Foil.hs +17/−5
• src/Control/Monad/Free/Foil/Annotated.hs +182/−0
• src/Data/ZipMatchK/Generic.hs +10/−0
• src/Data/ZipMatchK/TH.hs +267/−0
• test/Control/Monad/Free/Foil/AnnotatedSpec.hs +139/−0
• test/Data/ZipMatchK/THSpec.hs +132/−0

@@ -1,5 +1,31 @@ # CHANGELOG for `free-foil` +# 0.3.2 — 2026-07-15++An additive release: the annotation layer, the `ZipMatchK` derivers, and a set of performance improvements. Upgrading from 0.3.1 needs no work.++New:++- `Control.Monad.Free.Foil.Annotated`, a layer that annotates every node with an `ann term` built from the node's own term ([#42](https://github.com/fizruk/free-foil/pull/42), [#46](https://github.com/fizruk/free-foil/pull/46)). `Bifoldable` skips the annotation, so `alphaEquiv` is annotation-blind; `freeVarsOfAnnotated` sees the variables inside annotations that `freeVarsOf` skips. `AnnSig`'s `ZipMatchK` is derived rather than generic, since on an annotated signature it sits on a typechecker's hottest path. An annotation-blind instance must return `Just` lazily, and the module documents why a strict one is wrong.++- `Data.ZipMatchK.TH`, Template Haskell derivers for `ZipMatchK` ([#43](https://github.com/fizruk/free-foil/pull/43)). `deriveZipMatchK` zips every type parameter, `deriveZipMatchK2` the last two (for a signature with an annotation parameter), with `deriveZipMatchK1` and `deriveZipMatchKWith` for the rest. The generic instance rebuilds a `Generics.Kind` view of every node on every comparison, at a cost that grows with the number of constructors. The derived instance is flat, and on a 44-constructor signature runs `alphaEquiv` 1.8 times faster for 2.3 times less allocation. It replaces the deriver 0.3.0 dropped along with the old `ZipMatch` class.++- `sinkContainer` sinks a whole container of sinkables (an `IntMap` or `Map` of terms) in O(1) by coercion, instead of `fmap sink` over the spine ([#44](https://github.com/fizruk/free-foil/pull/44)). A `Scope` is not sinkable and a `NameMap` must stay total, both noted with the function.++- `zipmatchk` and `normalize` benchmarks ([#43](https://github.com/fizruk/free-foil/pull/43), [#45](https://github.com/fizruk/free-foil/pull/45)): `alphaEquiv` across signature sizes, and full β-normalisation of untyped λ-terms. CI builds them and does not run them.++Performance:++- `alphaEquiv` and `unsafeEqAST` no longer copy the node into a tuple before folding over it. They recurse inside the zipping functions, allocating nothing and short-circuiting on the first mismatch ([#44](https://github.com/fizruk/free-foil/pull/44)). On the benchmark, 294 µs to 217 µs and 3.1 MB to 2.8 MB with a derived instance. Behaviour is unchanged.++- `substitute`, `alphaEquiv`, `refreshAST` and friends are now `INLINABLE`, so a call site can specialise them for its own signature instead of passing dictionaries ([#44](https://github.com/fizruk/free-foil/pull/44)).++Changed:++- `soas` and `Language.LambdaPi.Impl.FreeFoilTH` derive their `ZipMatchK` instances. `Language.LambdaPi.Impl.FreeFoil` writes them out by hand, so the two implementations show both ways.++- The `base` lower bound is now `>= 4.19` (GHC 9.8). The package has required GHC 9.8 all along through `template-haskell >= 2.21`, so this only makes the bound honest, and lets Hackage's documentation builder pick a compatible GHC ([#15](https://github.com/fizruk/free-foil/issues/15)).+ # 0.3.1 — 2026-07-14  A bug fix and a set of additions, all of them prompted by the projects built on free-foil. Nothing is removed or changed, so upgrading from 0.3.0 needs no work.

@@ -0,0 +1,56 @@+{-# LANGUAGE DataKinds        #-}+{-# LANGUAGE GADTs            #-}+{-# LANGUAGE LambdaCase       #-}+{-# LANGUAGE PatternSynonyms  #-}+{-# LANGUAGE TypeFamilies     #-}++-- | Normalisation benchmark: full β-normalisation of untyped λ-terms over the+-- free foil, which is where the library's 'substitute' is put under pressure.+--+-- The workload is Church-numeral exponentiation. A Church numeral @n@ applied to+-- a Church numeral @m@ normalises to the Church numeral for @m^n@ (see+-- 'Control.Monad.Free.Foil.Example.nf'), so @'power' n m@ forces a number of+-- β-reductions that grows with @m^n@, each one a 'substitute' into a scoped+-- term. This is the same shape of workload as the free-foil module of+-- [lambda-n-ways](https://github.com/sweirich/lambda-n-ways) (Weirich's+-- benchmark suite), from the Free Foil paper.+--+-- There is no substitution or normalisation benchmark elsewhere in the package —+-- the @zipmatchk@ benchmark only exercises 'Control.Monad.Free.Foil.alphaEquiv' —+-- so this is the one that would show a change to term-building (a strict @AST@,+-- a substitution that skips unaffected subterms, and so on).+module Main (main) where++import           Test.Tasty.Bench++import           Control.Monad.Foil            (S (VoidS))+import           Control.Monad.Free.Foil       (pattern Var)+import           Control.Monad.Free.Foil.Example (Expr, churchN, nf', pattern AppE, pattern LamE)++-- | The size of a term, used to force the whole normal form (rather than just+-- its outermost constructor) without a 'Control.DeepSeq.NFData' instance.+sizeOf :: Expr n -> Int+sizeOf = \case+  Var{}       -> 1+  AppE f x    -> 1 + sizeOf f + sizeOf x+  LamE _ body -> 1 + sizeOf body++-- | @'power' n m@ is @m@ raised to the @n@: the Church numeral @n@ applied to+-- the Church numeral @m@, which normalises to the Church numeral for @m^n@.+power :: Int -> Int -> Expr VoidS+power n m = AppE (churchN n) (churchN m)++-- | Normalise, then walk the whole result so the benchmark forces it fully.+normalized :: Expr VoidS -> Int+normalized = sizeOf . nf'++main :: IO ()+main = defaultMain+  [ bgroup "nf of Church m^n"+      [ bench "8^2  = 64"   $ whnf normalized (power 2 8)+      , bench "4^3  = 64"   $ whnf normalized (power 3 4)+      , bench "12^2 = 144"  $ whnf normalized (power 2 12)+      , bench "2^8  = 256"  $ whnf normalized (power 8 2)+      , bench "2^10 = 1024" $ whnf normalized (power 10 2)+      ]+  ]

@@ -0,0 +1,134 @@+{-# LANGUAGE DataKinds             #-}+{-# LANGUAGE DeriveTraversable     #-}+{-# LANGUAGE FlexibleContexts      #-}+{-# LANGUAGE FlexibleInstances     #-}+{-# LANGUAGE GADTs                 #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE RankNTypes            #-}+{-# LANGUAGE ScopedTypeVariables   #-}+{-# LANGUAGE TemplateHaskell       #-}+{-# LANGUAGE TypeFamilies          #-}+{-# LANGUAGE UndecidableInstances  #-}+{-# OPTIONS_GHC -Wno-orphans #-}++-- | What the generic 'ZipMatchK' instance costs, and how that cost scales with+-- the size of the signature.+--+-- For each size, two structurally identical signatures differing only in how+-- their 'ZipMatchK' instance is obtained: @SigNG@ takes the generic default+-- (via "Generics.Kind"), @SigNH@ has the instance derived by+-- 'deriveZipMatchK'. Both are compared on 'alphaEquiv' of a large closed term+-- against itself, which is the worst case (no early exit) and the one a+-- typechecker actually hits.+--+-- The generic representation of a constructor is a chain of @L1@\/@R1@ wrappers+-- as long as the constructor's index, so a term built from constructors spread+-- across the whole signature — as a real language's terms are — should cost the+-- generic instance more the larger the signature is. The derived instance+-- compiles to a single @case@, and should not care.+module Main (main) where++import           Data.Bifunctor.TH+import           Test.Tasty.Bench++import qualified Control.Monad.Foil      as Foil+import           Control.Monad.Free.Foil+import           Data.ZipMatchK+import           Data.ZipMatchK.TH       (deriveZipMatchK)+import           Generics.Kind.TH        (deriveGenericK)++import           Signature               (mkSig)++-- * Signatures of three sizes, twice over++mkSig "Sig2G" 2+mkSig "Sig2H" 2+mkSig "Sig10G" 10+mkSig "Sig10H" 10+mkSig "Sig44G" 44+mkSig "Sig44H" 44++deriveBifunctor ''Sig2G+deriveBifoldable ''Sig2G+deriveBitraversable ''Sig2G+deriveGenericK ''Sig2G+instance ZipMatchK Sig2G++deriveBifunctor ''Sig2H+deriveBifoldable ''Sig2H+deriveBitraversable ''Sig2H+deriveZipMatchK ''Sig2H++deriveBifunctor ''Sig10G+deriveBifoldable ''Sig10G+deriveBitraversable ''Sig10G+deriveGenericK ''Sig10G+instance ZipMatchK Sig10G++deriveBifunctor ''Sig10H+deriveBifoldable ''Sig10H+deriveBitraversable ''Sig10H+deriveZipMatchK ''Sig10H++deriveBifunctor ''Sig44G+deriveBifoldable ''Sig44G+deriveBitraversable ''Sig44G+deriveGenericK ''Sig44G+instance ZipMatchK Sig44G++deriveBifunctor ''Sig44H+deriveBifoldable ''Sig44H+deriveBitraversable ''Sig44H+deriveZipMatchK ''Sig44H++-- * A large closed term++-- | A closed term of the given depth: an application tree with a λ every other+-- level, cycling through the signature's application constructors so that the+-- whole signature is on the hot path.+mkTerm+  :: forall sig+   . (forall scope term. Int -> term -> term -> sig scope term)  -- ^ Application nodes.+  -> (forall scope term. scope -> sig scope term)                -- ^ λ-abstraction node.+  -> Int+  -> AST Foil.NameBinder sig Foil.VoidS+mkTerm app lam maxDepth = Foil.withFresh Foil.emptyScope $ \binder ->+  let scope = Foil.extendScope binder Foil.emptyScope+   in Node (lam (ScopedAST binder (go scope (Foil.nameOf binder) maxDepth)))+  where+    go :: Foil.Distinct n => Foil.Scope n -> Foil.Name n -> Int -> AST Foil.NameBinder sig n+    go _scope x 0 = Var x+    go scope x d+      | even d = Node (app d (go scope x (d - 1)) (go scope x (d - 1)))+      | otherwise = Foil.withFresh scope $ \binder ->+          let scope' = Foil.extendScope binder scope+           in Node (lam (ScopedAST binder (go scope' (Foil.sink x) (d - 1))))++-- | ~4000 leaves.+depth :: Int+depth = 24++main :: IO ()+main = defaultMain+  [ bgroup "alphaEquiv, term against itself"+      [ bgroup "2 constructors"+          [ bench "generic" $ whnf (alphaEquiv Foil.emptyScope t) t+          , bench "derived" $ whnf (alphaEquiv Foil.emptyScope u) u+          ]+      , bgroup "10 constructors"+          [ bench "generic" $ whnf (alphaEquiv Foil.emptyScope t10) t10+          , bench "derived" $ whnf (alphaEquiv Foil.emptyScope u10) u10+          ]+      , bgroup "44 constructors"+          [ bench "generic" $ whnf (alphaEquiv Foil.emptyScope t44) t44+          , bench "derived" $ whnf (alphaEquiv Foil.emptyScope u44) u44+          ]+      ]+  ]+  where+    t = mkTerm appSig2G lamSig2G depth+    u = mkTerm appSig2H lamSig2H depth+    t10 = mkTerm appSig10G lamSig10G depth+    u10 = mkTerm appSig10H lamSig10H depth+    t44 = mkTerm appSig44G lamSig44G depth+    u44 = mkTerm appSig44H lamSig44H depth

@@ -0,0 +1,59 @@+{-# LANGUAGE TemplateHaskell #-}+-- | A generator for signature bifunctors of a given size.+--+-- The cost of the generic 'Data.ZipMatchK.ZipMatchK' instance is expected to+-- grow with the number of constructors — a constructor is represented as a+-- chain of @L1@\/@R1@ wrappers as long as its index — so the benchmark needs+-- signatures of several sizes, and hand-writing them would defeat the purpose.+module Signature (mkSig) where++import           Language.Haskell.TH++-- | @mkSig \"Sig\" n@ declares a signature bifunctor @Sig@ with @n@+-- constructors: @n-1@ application-like nodes (two terms) and one λ-like node+-- (one scoped term), with 'Bifunctor', 'Bifoldable' and 'Bitraversable'+-- instances. It also declares two builders,+--+-- > appSig :: Int -> term -> term -> Sig scope term   -- the i-th application node+-- > lamSig :: scope -> Sig scope term+--+-- named after the type (@appSig@ and @lamSig@ for @Sig@), so that one term+-- builder can serve every signature.+--+-- The 'Data.Bifunctor.Bifunctor' and 'Data.ZipMatchK.ZipMatchK' instances are+-- left to the caller: they need a splice of their own, as Template Haskell+-- cannot reify a type declared in the same declaration group.+mkSig :: String -> Int -> Q [Dec]+mkSig name n = do+  scope <- newName "scope"+  term <- newName "term"+  let typeName = mkName name+      appName i = mkName (name ++ "App" ++ show i)+      lamName = mkName (name ++ "Lam")+      appCon i = NormalC (appName i)+        [ (noBang, VarT term), (noBang, VarT term) ]+      lamCon = NormalC lamName [ (noBang, VarT scope) ]+      noBang = Bang NoSourceUnpackedness NoSourceStrictness+      cons = map appCon [0 .. n - 2] ++ [lamCon]+      dataDec = DataD [] typeName [PlainTV scope BndrReq, PlainTV term BndrReq] Nothing cons+        [DerivClause Nothing [ConT ''Functor, ConT ''Foldable, ConT ''Traversable]]++  -- appSig i = the i-th application constructor, cycling.+  i <- newName "i"+  let sigType t = ForallT [PlainTV scope SpecifiedSpec, PlainTV term SpecifiedSpec] [] t+      appType = sigType (arrows [ConT ''Int, VarT term, VarT term] result)+      lamType = sigType (arrows [VarT scope] result)+      result = AppT (AppT (ConT typeName) (VarT scope)) (VarT term)+      arrows args res = foldr (\a b -> AppT (AppT ArrowT a) b) res args+      appFn = mkName ("app" ++ name)+      appDec = FunD appFn+        [ Clause [VarP i]+            (NormalB (CaseE (InfixE (Just (VarE i)) (VarE 'mod) (Just (LitE (IntegerL (toInteger (n - 1))))))+              ([ Match (LitP (IntegerL (toInteger k))) (NormalB (ConE (appName k))) []+               | k <- [0 .. n - 3] ]+               ++ [ Match WildP (NormalB (ConE (appName (n - 2)))) [] ])))+            [] ]+      lamFn = mkName ("lam" ++ name)+      lamDec = FunD lamFn [ Clause [] (NormalB (ConE lamName)) [] ]++  return [dataDec, SigD appFn appType, appDec, SigD lamFn lamType, lamDec]

@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack  name:           free-foil-version:        0.3.1+version:        0.3.2 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@@ -40,6 +40,7 @@       Control.Monad.Foil.TH.MkToFoil       Control.Monad.Foil.TH.Util       Control.Monad.Free.Foil+      Control.Monad.Free.Foil.Annotated       Control.Monad.Free.Foil.Example       Control.Monad.Free.Foil.TH       Control.Monad.Free.Foil.TH.Convert@@ -51,6 +52,7 @@       Data.ZipMatchK.Functor       Data.ZipMatchK.Generic       Data.ZipMatchK.Mappings+      Data.ZipMatchK.TH   other-modules:       Paths_free_foil   hs-source-dirs:@@ -58,7 +60,7 @@   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 && <0.6-    , base >=4.7 && <5+    , base >=4.19 && <5     , bifunctors >=5.5 && <5.7     , containers >=0.6 && <0.9     , deepseq >=1.4 && <1.6@@ -76,7 +78,7 @@   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 && <0.6-    , base >=4.7 && <5+    , base >=4.19 && <5     , bifunctors >=5.5 && <5.7     , containers >=0.6 && <0.9     , deepseq >=1.4 && <1.6@@ -93,16 +95,18 @@   other-modules:       Control.Monad.Foil.NameMapSpec       Control.Monad.Foil.UnifyNameBindersSpec+      Control.Monad.Free.Foil.AnnotatedSpec       Control.Monad.Free.Foil.TH.MkFreeFoilSpec       Control.Monad.Free.Foil.TH.MkFreeFoilSpec.Config       Control.Monad.Free.Foil.TH.MkFreeFoilSpec.Syntax+      Data.ZipMatchK.THSpec       Paths_free_foil   hs-source-dirs:       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 && <0.6-    , base >=4.7 && <5+    , base >=4.19 && <5     , bifunctors >=5.5 && <5.7     , containers >=0.6 && <0.9     , deepseq >=1.4 && <1.6@@ -111,6 +115,50 @@     , hspec-discover     , kind-generics >=0.5.0 && <0.6     , kind-generics-th+    , template-haskell >=2.21.0.0 && <2.24+    , text >=1.2.3.1 && <2.2+  default-language: Haskell2010++benchmark normalize+  type: exitcode-stdio-1.0+  main-is: Main.hs+  other-modules:+      Paths_free_foil+  hs-source-dirs:+      bench/normalize+  ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path -O2 -rtsopts+  build-depends:+      array >=0.5.3.0 && <0.6+    , base >=4.19 && <5+    , bifunctors >=5.5 && <5.7+    , containers >=0.6 && <0.9+    , deepseq >=1.4 && <1.6+    , free-foil+    , kind-generics >=0.5.0 && <0.6+    , tasty-bench+    , template-haskell >=2.21.0.0 && <2.24+    , text >=1.2.3.1 && <2.2+  default-language: Haskell2010++benchmark zipmatchk+  type: exitcode-stdio-1.0+  main-is: Main.hs+  other-modules:+      Signature+      Paths_free_foil+  hs-source-dirs:+      bench/zipmatchk+  ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path -O2 -rtsopts+  build-depends:+      array >=0.5.3.0 && <0.6+    , base >=4.19 && <5+    , bifunctors >=5.5 && <5.7+    , containers >=0.6 && <0.9+    , deepseq >=1.4 && <1.6+    , free-foil+    , kind-generics >=0.5.0 && <0.6+    , kind-generics-th+    , tasty-bench     , template-haskell >=2.21.0.0 && <2.24     , text >=1.2.3.1 && <2.2   default-language: Haskell2010

@@ -40,6 +40,7 @@   CoSinkable(..),   HasNameBinders(getNameBinders),   sink,+  sinkContainer,   extendRenaming,   extendNameBinderRenaming,   composeNameBinderRenamings,

@@ -48,6 +48,7 @@ import           Control.DeepSeq    (NFData (..)) import           Data.Bifunctor import           Data.Coerce        (coerce)+import           Data.Functor.Compose (Compose (..)) import           Data.IntMap import qualified Data.IntMap        as IntMap import           Data.IntSet@@ -59,6 +60,12 @@  import Control.Monad.Foil.Internal.ValidNameBinders +-- $setup+-- >>> :set -XDataKinds+-- >>> :set -XFlexibleContexts+-- >>> :set -Wno-simplifiable-class-constraints+-- >>> import qualified Data.Map as Map+ -- * Safe types and operations  -- | 'S' is a data kind of scope indices.@@ -662,12 +669,41 @@ instance Sinkable Name where   sinkabilityProof rename = rename +-- | A container of sinkable expressions is sinkable, elementwise.+--+-- The point of this instance is 'sinkContainer': since the proof typechecks,+-- sinking the whole container is a coercion, and does not walk its spine.+instance (Functor f, Sinkable e) => Sinkable (Compose f e) where+  sinkabilityProof rename (Compose xs) = Compose (fmap (sinkabilityProof rename) xs)+ -- | Efficient version of 'sinkabilityProof'. -- In fact, once 'sinkabilityProof' typechecks, -- it is safe to 'sink' by coercion. -- See Section 3.5 in [«The Foil: Capture-Avoiding Substitution With No Sharp Edges»](https://doi.org/10.1145/3587216.3587224) for the details. sink :: (Sinkable e, DExt n l) => e n -> e l sink = unsafeCoerce++-- | Sink an entire container of sinkable expressions, in \(O(1)\).+--+-- The soundness argument for 'sink' extends to a container of sinkables — an+-- 'Data.IntMap.IntMap' of terms, a 'Data.Map.Map' keyed by something else, a+-- list of them — so there is no need to walk the spine with @'fmap' 'sink'@, and+-- entering a binder need not be \(O(size)\).+--+-- >>> :{+-- sinkEnv :: DExt n l => Map.Map String (Name n) -> Map.Map String (Name l)+-- sinkEnv = sinkContainer+-- :}+--+-- Two things this does /not/ cover:+--+-- * A 'Scope' is __not__ sinkable, and must not be sunk: it is the set of names+--   /in/ scope @n@, and it has to grow when a binder is entered (see 'extendScope').+-- * A 'NameMap' must stay __total__ on the names in scope ('lookupName' errors+--   otherwise), so sinking one has to be paired with adding the new binder's+--   entry (see 'addNameBinder').+sinkContainer :: (Functor f, Sinkable e, DExt n l) => f (e n) -> f (e l)+sinkContainer = getCompose . sink . Compose  -- | Extend renaming when going under a 'CoSinkable' pattern (generalized binder). -- Note that the scope under pattern is independent of the codomain of the renaming.

@@ -34,7 +34,6 @@ 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) @@ -83,6 +82,7 @@ -- * Substitution  -- | Substitution for free (scoped monads).+{-# INLINABLE substitute #-} substitute   :: (Bifunctor sig, Foil.Distinct o, Foil.CoSinkable binder, Foil.SinkableK binder)   => Foil.Scope o@@ -108,6 +108,7 @@ -- > substituteRefreshed scope subst = refreshAST scope . subtitute scope subst -- -- In general, 'substitute' is more efficient since it does not always refresh binders.+{-# INLINABLE substituteRefreshed #-} substituteRefreshed   :: (Bifunctor sig, Foil.Distinct o, Foil.CoSinkable binder, Foil.SinkableK binder)   => Foil.Scope o@@ -158,6 +159,7 @@ -- * \(\alpha\)-equivalence  -- | Refresh (force) all binders in a term, minimizing the used indices.+{-# INLINABLE refreshAST #-} refreshAST   :: (Bifunctor sig, Foil.Distinct n, Foil.CoSinkable binder, Foil.SinkableK binder)   => Foil.Scope n@@ -168,6 +170,7 @@   Node t -> Node (bimap (refreshScopedAST scope) (refreshAST scope) t)  -- | Similar to `refreshAST`, but for scoped terms.+{-# INLINABLE refreshScopedAST #-} refreshScopedAST :: (Bifunctor sig, Foil.Distinct n, Foil.CoSinkable binder, Foil.SinkableK binder)   => Foil.Scope n   -> ScopedAST binder sig n@@ -183,6 +186,7 @@ -- -- Compared to 'alphaEquiv', this function may perform some unnecessary -- changes of bound variables when the binders are the same on both sides.+{-# INLINABLE alphaEquivRefreshed #-} alphaEquivRefreshed   :: (Bitraversable sig, ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder, Foil.SinkableK binder)   => Foil.Scope n@@ -196,6 +200,7 @@ -- -- Compared to 'alphaEquivRefreshed', this function might skip unnecessary -- changes of bound variables when both binders in two matching scoped terms coincide.+{-# INLINABLE alphaEquiv #-} alphaEquiv   :: (Bitraversable sig, ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder, Foil.SinkableK binder)   => Foil.Scope n@@ -204,12 +209,15 @@   -> Bool alphaEquiv _scope (Var x) (Var y) = x == coerce y alphaEquiv scope (Node l) (Node r) =-  case zipMatch2 l r of+  case zipMatchWith2 (unit . alphaEquivScoped scope) (unit . alphaEquiv scope) l r of     Nothing -> False-    Just tt -> getAll (bifoldMap (All . uncurry (alphaEquivScoped scope)) (All . uncurry (alphaEquiv scope)) tt)+    Just _  -> True+  where+    unit f x = if f x then Just () else Nothing alphaEquiv _ _ _ = False  -- | Same as 'alphaEquiv' but for scoped terms.+{-# INLINABLE alphaEquivScoped #-} alphaEquivScoped   :: (Bitraversable sig, ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder, Foil.SinkableK binder)   => Foil.Scope n@@ -255,6 +263,7 @@ -- This check ignores the possibility that two terms might have different -- scope extensions under binders (which might happen due to substitution -- under a binder in absence of name conflicts).+{-# INLINABLE unsafeEqAST #-} unsafeEqAST   :: (Bitraversable sig, ZipMatchK sig, Foil.UnifiablePattern binder, Foil.Distinct n, Foil.Distinct l)   => AST binder sig n@@ -262,12 +271,15 @@   -> Bool unsafeEqAST (Var x) (Var y) = x == coerce y unsafeEqAST (Node t1) (Node t2) =-  case zipMatch2 t1 t2 of+  case zipMatchWith2 (unit . unsafeEqScopedAST) (unit . unsafeEqAST) t1 t2 of     Nothing -> False-    Just tt -> getAll (bifoldMap (All . uncurry unsafeEqScopedAST) (All . uncurry unsafeEqAST) tt)+    Just _  -> True+  where+    unit f x = if f x then Just () else Nothing unsafeEqAST _ _ = False  -- | A version of 'unsafeEqAST' for scoped terms.+{-# INLINABLE unsafeEqScopedAST #-} unsafeEqScopedAST   :: (Bitraversable sig, ZipMatchK sig, Foil.UnifiablePattern binder, Foil.Distinct n, Foil.Distinct l)   => ScopedAST binder sig n

@@ -0,0 +1,182 @@+{-# LANGUAGE DataKinds             #-}+{-# LANGUAGE DeriveGeneric         #-}+{-# LANGUAGE DeriveTraversable     #-}+{-# LANGUAGE FlexibleContexts      #-}+{-# LANGUAGE FlexibleInstances     #-}+{-# LANGUAGE LambdaCase            #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PatternSynonyms       #-}+{-# LANGUAGE PolyKinds             #-}+{-# LANGUAGE StandaloneDeriving    #-}+{-# LANGUAGE TemplateHaskell       #-}+{-# LANGUAGE TypeFamilies          #-}+{-# LANGUAGE TypeOperators         #-}+{-# LANGUAGE UndecidableInstances  #-}++-- | Annotating every node of a free foil term.+--+-- A node can be annotated with anything: a source position, a type, a memoised+-- normal form. 'AnnSig' turns a signature into an annotated one, and+-- 'AnnAST' is the annotated syntax it generates.+--+-- The annotation is a /functor of the term/, and that is what lets it depend on+-- the node's scope. In @'AST' binder sig n@ the signature's term parameter /is/+-- the AST at the node's own scope, so an annotation built from it holds terms in+-- that scope — which is what a type annotation in a dependent language needs.+-- An annotation that ignores the term (a source position, say) is @'Const' a@.+--+-- Whether two annotations must agree for their nodes to match is a property of+-- @ann@, not of 'AnnSig'. Two examples, and they are the two you will want:+--+-- An annotation that ignores the term (a source position) and /is/ compared:+--+-- > instance Eq a => ZipMatchK (Const (a :: Type)) where+-- >   zipMatchWithK _ (Const l) (Const r)+-- >     | l == r    = Just (Const l)+-- >     | otherwise = Nothing+--+-- An annotation that holds terms (a type, say) and is /ignored/, so that two+-- terms differing only in their types are α-equivalent. Make the held term+-- optional, so that pairing can fail /without/ failing the match:+--+-- > newtype TypeOf term = TypeOf (Maybe term)+-- >+-- > instance ZipMatchK TypeOf where+-- >   zipMatchWithK (f :^: M0) (TypeOf l) (TypeOf r) =+-- >     Just (TypeOf (do { a <- l; b <- r; f a b }))+--+-- __The instance must return 'Just' unconditionally, and lazily.__ Matching is+-- annotation-blind, so it must succeed whatever the annotations are; the paired+-- annotation is a thunk the (annotation-skipping) 'Bifoldable' never forces. A+-- /strict/ shape — @TypeOf '<$>' f l r@, or anything that yields 'Nothing' when+-- @f@ fails — is a footgun twice over: it breaks blindness (two nodes with+-- different types would fail to match), and it /diverges/ for a finite or+-- lazily-bottomed annotation (a universe tower ending in 'error', say), because+-- forcing the annotation runs off the end. This is why the held term is a 'Maybe':+-- a plain @term@ field would have no value to pair when @f@ fails, forcing a+-- bottom into the result.+--+-- __Do not reach for the generic instance here.__ It compares the annotation's+-- /shape/, so a node carrying a memoised normal form would fail to match the same+-- node without one. (Nor is 'zipMatchViaChooseLeft' available: an annotation+-- holding terms must /construct/ a value at the result index, and cannot simply+-- pick a side.)+--+-- __Note the asymmetry__ in the instances below: 'Bifunctor' and 'Bitraversable'+-- traverse the annotation, but 'Bifoldable' does /not/. This is deliberate — see+-- 'AnnSig'.+module Control.Monad.Free.Foil.Annotated (+  AnnSig(..),+  AnnAST,+  AnnScopedAST,+  pattern AnnNode,+  annotationOf,+  freeVarsOfAnnotated,+) where++import           Data.Bifoldable+import           Data.Bifunctor+import           Data.Bitraversable+import           Data.Kind             (Type)+import           Data.Maybe            (mapMaybe)+import           Data.ZipMatchK.TH     (deriveZipMatchK2)+import           Generics.Kind         (GenericK (..), Field, Var0, Var1, (:$:),+                                        Atom ((:@:)), (:*:))+import qualified GHC.Generics          as GHC++import qualified Control.Monad.Foil    as Foil+import           Control.Monad.Free.Foil++-- | A signature, with every node annotated by an @ann@ built from the node's term.+--+-- The annotation is applied to the /term/ parameter, so in an+-- @'AST' binder ('AnnSig' ann sig) n@ it holds terms in the node's own scope.+--+-- 'Bifoldable' deliberately __skips the annotation__. That is what makes+-- α-equivalence annotation-blind: 'Control.Monad.Free.Foil.alphaEquiv' consumes a+-- zipped node with 'bifoldMap', so a type annotation is never compared, and two+-- terms that differ only in their annotations are α-equivalent. The price is that+-- 'Control.Monad.Free.Foil.freeVarsOf', which is also 'Bifoldable', does not see+-- variables occurring inside annotations. Use 'freeVarsOfAnnotated' when those+-- matter.+data AnnSig (ann :: Type -> Type) (sig :: Type -> Type -> Type) scope term+  = AnnSig (ann term) (sig scope term)+  deriving (GHC.Generic)++deriving instance (Functor ann, Functor (sig scope))+  => Functor (AnnSig ann sig scope)+deriving instance (Foldable ann, Foldable (sig scope))+  => Foldable (AnnSig ann sig scope)+deriving instance (Traversable ann, Traversable (sig scope))+  => Traversable (AnnSig ann sig scope)++instance (Functor ann, Bifunctor sig) => Bifunctor (AnnSig ann sig) where+  bimap f g (AnnSig ann sig) = AnnSig (fmap g ann) (bimap f g sig)++-- | __The annotation is not folded.__ See 'AnnSig'.+instance Bifoldable sig => Bifoldable (AnnSig ann sig) where+  bifoldMap f g (AnnSig _ann sig) = bifoldMap f g sig++instance (Traversable ann, Bitraversable sig) => Bitraversable (AnnSig ann sig) where+  bitraverse f g (AnnSig ann sig) = AnnSig <$> traverse g ann <*> bitraverse f g sig++instance GenericK (AnnSig ann sig) where+  type RepK (AnnSig ann sig) =+    Field (ann :$: Var1) :*: Field ((sig :$: Var0) :@: Var1)++-- | Matching for 'AnnSig' is /derived/, not left to the generic default.+--+-- The generic default would rebuild the "Generics.Kind" view of every node on+-- every comparison, and comparing terms is most of what a typechecker does, so+-- for an annotated signature — where it lands on the hottest path — that is a+-- measurable cost. 'Data.ZipMatchK.TH.deriveZipMatchK2' generates the+-- written-out instance instead: the annotation matched with the term zipper (an+-- annotation is a functor of the term), the inner signature with both. Write+-- @deriveZipMatchK2 ''YourAnnSig@ for a bespoke annotated signature.+deriveZipMatchK2 ''AnnSig++-- | An annotated scope-safe term.+type AnnAST binder ann sig = AST binder (AnnSig ann sig)++-- | An annotated scope-safe term under a binder.+type AnnScopedAST binder ann sig = ScopedAST binder (AnnSig ann sig)++-- | An annotated node.+pattern AnnNode+  :: ann (AnnAST binder ann sig n)+  -> sig (AnnScopedAST binder ann sig n) (AnnAST binder ann sig n)+  -> AnnAST binder ann sig n+pattern AnnNode ann sig = Node (AnnSig ann sig)++{-# COMPLETE Var, AnnNode #-}++-- | The annotation of a term, unless it is a variable (which is not a node, so it+-- carries none).+annotationOf :: AnnAST binder ann sig n -> Maybe (ann (AnnAST binder ann sig n))+annotationOf = \case+  Var _         -> Nothing+  AnnNode ann _ -> Just ann++-- | The free variables of an annotated term, __including__ those occurring inside+-- annotations.+--+-- 'Control.Monad.Free.Foil.freeVarsOf' misses the latter, since 'Bifoldable' skips+-- the annotation (see 'AnnSig').+freeVarsOfAnnotated+  :: (Foil.Distinct n, Foil.CoSinkable binder, Bifoldable sig, Foldable ann)+  => AnnAST binder ann sig n -> [Foil.Name n]+freeVarsOfAnnotated = \case+  Var name -> [name]+  AnnNode ann sig ->+    foldMap freeVarsOfAnnotated ann+      <> bifoldMap freeVarsOfAnnotatedScoped freeVarsOfAnnotated sig++-- | The free variables of an annotated scoped term, including those inside+-- annotations.+freeVarsOfAnnotatedScoped+  :: (Foil.Distinct n, Foil.CoSinkable binder, Bifoldable sig, Foldable ann)+  => AnnScopedAST binder ann sig n -> [Foil.Name n]+freeVarsOfAnnotatedScoped (ScopedAST binder body) =+  case Foil.assertDistinct binder of+    Foil.Distinct ->+      mapMaybe (Foil.unsinkNamePattern binder) (freeVarsOfAnnotated body)

@@ -29,6 +29,16 @@ -- -- Note: @f@ is expected to be a traversable n-functor, -- but at the moment we lack a @TraversableK@ constraint.+--+-- The default implementation is generic, via 'Generics.Kind.RepK'. It is+-- convenient, but it reflects each node into a representation and back on every+-- comparison, and a constructor is represented as a chain of @L1@\/@R1@ wrappers+-- as long as its index, so the cost grows with the size of the signature. On a+-- 44-constructor signature it costs about 1.8 times the time and 2.3 times the+-- allocation of the written-out instance, and comparing terms is most of what a+-- typechecker does. Use 'Data.ZipMatchK.TH.deriveZipMatchK' (or+-- 'Data.ZipMatchK.TH.deriveZipMatchK2', for a signature bifunctor with extra+-- parameters) to generate the written-out instance instead. class ZipMatchK (f :: k) where   -- | Perform one level of equality testing:   --

@@ -0,0 +1,267 @@+{-# LANGUAGE LambdaCase      #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE ViewPatterns    #-}+-- | Template Haskell derivation of 'ZipMatchK' instances.+--+-- The generic instance (the one you get by writing @instance ZipMatchK TermSig@+-- with no body) converts a node into its "Generics.Kind" representation on+-- every comparison, and converts the result back. The representation of a+-- constructor is a chain of @L1@\/@R1@ wrappers as long as that constructor's+-- index, so the cost grows with the number of constructors in the signature,+-- and comparing terms is most of what a typechecker does.+--+-- The derivers here generate the instance that one would otherwise write out by+-- hand: a @case@ over the two nodes, allocating only its result. On a+-- 44-constructor signature that is worth a factor of 1.8 in time and 2.3 in+-- allocation on 'Control.Monad.Free.Foil.alphaEquiv' (see the @zipmatchk@+-- benchmark), and the derived instance does not get slower as the signature+-- grows.+--+-- The module the splice appears in needs at least+--+-- > {-# LANGUAGE GADTs #-}+-- > {-# LANGUAGE TemplateHaskell #-}+-- > {-# LANGUAGE TypeFamilies #-}+--+-- Signatures that refer to one another — as the ones generated by+-- 'Control.Monad.Free.Foil.TH.MkFreeFoil.mkFreeFoil' from a grammar with+-- several syntactic categories do — have to be derived in a __single splice__,+-- since a top-level splice ends a declaration group and an instance from a later+-- group is not visible to an earlier one:+--+-- > concat <$> traverse deriveZipMatchK2 [''Term'Sig, ''OpArg'Sig, ''Type'Sig]+module Data.ZipMatchK.TH (+  deriveZipMatchK,+  deriveZipMatchK1,+  deriveZipMatchK2,+  deriveZipMatchKWith,+) where++import           Data.List             (foldl')+import qualified Data.Set              as Set+import           Language.Haskell.TH++import           Control.Monad.Foil.TH.Util (removeName, tvarName)+import           Data.ZipMatchK.Generic    (ZipMatchK (..))+import           Data.ZipMatchK.Mappings   (Mappings (..))++-- | Derive a 'ZipMatchK' instance, zipping /all/ type parameters.+--+-- For a signature bifunctor+--+-- > data TermSig scope term = AppSig term term | LamSig scope+-- > deriveZipMatchK ''TermSig+--+-- this generates+--+-- > instance ZipMatchK TermSig where+-- >   zipMatchWithK (f :^: g :^: M0) x y = case (x, y) of+-- >     (AppSig l1 l2, AppSig r1 r2) -> AppSig <$> g l1 r1 <*> g l2 r2+-- >     (LamSig l1, LamSig r1)       -> LamSig <$> f l1 r1+-- >     _                            -> Nothing+--+-- Use 'deriveZipMatchK2' when the type has extra parameters that should stay+-- fixed (an annotation, say), as a signature generated by+-- "Control.Monad.Free.Foil.TH.MkFreeFoil" does.+deriveZipMatchK :: Name -> Q [Dec]+deriveZipMatchK = deriveZipMatchKWith Nothing++-- | Derive a 'ZipMatchK' instance for a functor, zipping the last type parameter+-- and fixing the rest.+deriveZipMatchK1 :: Name -> Q [Dec]+deriveZipMatchK1 = deriveZipMatchKWith (Just 1)++-- | Derive a 'ZipMatchK' instance for a signature bifunctor, zipping the last two+-- type parameters (the scoped terms and the terms) and fixing the rest.+--+-- For a signature with an extra parameter (a source position, for instance)+--+-- > data Term'Sig a scope term = AppSig a term term | LamSig a scope+-- > deriveZipMatchK2 ''Term'Sig+--+-- this generates+--+-- > instance ZipMatchK a => ZipMatchK (Term'Sig a) where+-- >   zipMatchWithK (f :^: g :^: M0) x y = case (x, y) of+-- >     (AppSig l1 l2 l3, AppSig r1 r2 r3) ->+-- >       AppSig <$> zipMatchWithK M0 l1 r1 <*> g l2 r2 <*> g l3 r3+-- >     ...+deriveZipMatchK2 :: Name -> Q [Dec]+deriveZipMatchK2 = deriveZipMatchKWith (Just 2)++-- | Derive a 'ZipMatchK' instance, zipping the last @n@ type parameters and+-- fixing the rest. 'Nothing' zips all of them.+--+-- Every fixed parameter that occurs in a field gets a 'ZipMatchK' constraint in+-- the instance context.+deriveZipMatchKWith :: Maybe Int -> Name -> Q [Dec]+deriveZipMatchKWith arity typeName = do+  (tvars, cons) <- reifyDataType typeName+  let params = map tvarName tvars+      n = case arity of+            Nothing -> length params+            Just k  -> k+  if n > length params+    then fail (show typeName ++ " has " ++ show (length params)+                ++ " type parameter(s), cannot zip the last " ++ show n)+    else do+      let (fixed, zipped) = splitAt (length params - n) params+          zippedSet = Set.fromList zipped++      -- One zipping function per zipped parameter, in order.+      mappingVars <- mapM (const (newName "_f")) zipped+      let mappings = zip zipped (map VarE mappingVars)+          mappingsPat = foldr (\v p -> InfixP (VarP v) '(:^:) p) (ConP 'M0 [] []) mappingVars++      fieldsOf <- concat <$> mapM (constructorFields params zippedSet) cons+      clauses <- mapM (conClause zippedSet mappings) fieldsOf+      let fallthrough+            | length fieldsOf > 1 = [Match WildP (NormalB (ConE 'Nothing)) []]+            | otherwise           = []++      x <- newName "x"+      y <- newName "y"+      let body = CaseE (TupE [Just (VarE x), Just (VarE y)]) (clauses ++ fallthrough)+          impl = FunD 'zipMatchWithK+            [Clause [mappingsPat, VarP x, VarP y] (NormalB body) []]++          headType = foldl' AppT (ConT typeName) (map VarT fixed)+          usedVars = foldMap (foldMap freeVarsOfType . snd) fieldsOf+          context = [ AppT (ConT ''ZipMatchK) (VarT v)+                    | v <- fixed, v `Set.member` usedVars ]++      return [InstanceD Nothing context (AppT (ConT ''ZipMatchK) headType) [impl]]++-- | The type parameters and constructors of a @data@ or @newtype@ declaration.+reifyDataType :: Name -> Q ([TyVarBndr BndrVis], [Con])+reifyDataType typeName = reify typeName >>= \case+  TyConI (DataD _ _ tvars _ cons _)      -> return (tvars, cons)+  TyConI (NewtypeD _ _ tvars _ con _)    -> return (tvars, [con])+  _ -> fail (show typeName ++ " is not a data type or a newtype")++-- | A constructor's name and the types of its fields, in terms of the type+-- parameters of the declaration it belongs to.+--+-- 'Control.Monad.Free.Foil.TH.MkFreeFoil.mkFreeFoil' declares its signatures in+-- GADT syntax, and 'reify' returns such a constructor wrapped in a 'ForallC',+-- with variable names of its own. So the fields are renamed through the+-- constructor's return type before anything else looks at them.+constructorFields :: [Name] -> Set.Set Name -> Con -> Q [(Name, [Type])]+constructorFields params zipped = \case+  NormalC conName types      -> return [(conName, map snd types)]+  RecC conName types         -> return [(conName, map (snd . removeName) types)]+  InfixC l conName r         -> return [(conName, [snd l, snd r])]+  RecGadtC conNames types r  -> constructorFields params zipped+                                  (GadtC conNames (map removeName types) r)+  ForallC _ context_ con+    | null context_ -> constructorFields params zipped con+    | otherwise -> fail "constructor contexts are not supported by deriveZipMatchK"+  GadtC conNames types retType -> do+    rename <- renaming retType+    let fields = map (substTypeVars rename . snd) types+        escaping = foldMap freeVarsOfType fields `Set.difference` Set.fromList params+    if Set.null escaping+      then return [ (conName, fields) | conName <- conNames ]+      else fail ("existentials are not supported by deriveZipMatchK: "+                  ++ show (Set.toList escaping))+  where+    -- The constructor's variables, named as the declaration names them.+    renaming retType = do+      let (_, args) = unApply retType+      if length args /= length params+        then fail "the constructor does not return the type being derived for"+        else sequence+          [ case stripType arg of+              VarT v -> return (v, param)+              _ | param `Set.member` zipped ->+                    fail ("the constructor fixes the type parameter "+                           ++ show param ++ ", which is being zipped")+                | otherwise -> return (param, param)  -- a fixed index; no field can mention it+          | (arg, param) <- zip args params ]++-- | One @case@ alternative, zipping a constructor with itself.+conClause :: Set.Set Name -> [(Name, Exp)] -> (Name, [Type]) -> Q Match+conClause zipped mappings (conName, types) = do+  lvars <- mapM (const (newName "l")) types+  rvars <- mapM (const (newName "r")) types+  zippers <- mapM (fieldZipper zipped mappings) types+  -- Con <$> z1 l1 r1 <*> z2 l2 r2 <*> ...+  let zipField z l r = AppE (AppE z (VarE l)) (VarE r)+      apply acc (op, (z, (l, r))) = InfixE (Just acc) op (Just (zipField z l r))+      fields = zip (VarE '(<$>) : repeat (VarE '(<*>)))+                   (zip zippers (zip lvars rvars))+      body+        | null fields = AppE (ConE 'Just) (ConE conName)+        | otherwise   = foldl' apply (ConE conName) fields+  return (Match+            (TupP [ ConP conName [] (map VarP lvars)+                  , ConP conName [] (map VarP rvars) ])+            (NormalB body) [])++-- | Rename type variables.+substTypeVars :: [(Name, Name)] -> Type -> Type+substTypeVars rename = go+  where+    go = \case+      VarT v        -> VarT (maybe v id (lookup v rename))+      AppT f x      -> AppT (go f) (go x)+      AppKindT t k  -> AppKindT (go t) k+      SigT t k      -> SigT (go t) k+      ParensT t     -> ParensT (go t)+      InfixT l n r  -> InfixT (go l) n (go r)+      UInfixT l n r -> UInfixT (go l) n (go r)+      t             -> t++-- | Compile a field type into a zipping function @a -> b -> Maybe c@.+--+-- This mirrors what @ZipMatchFields@ does for the generic instance, but at+-- compile time, so nothing is reflected into a representation type:+--+-- * a zipped type parameter becomes the corresponding zipping function;+-- * any other type is zipped by its own 'ZipMatchK' instance, with the+--   arguments that mention zipped parameters passed as further zipping+--   functions.+--+-- So a field @[term]@ becomes @zipMatchWithK (g :^: M0)@ (asking for+-- @ZipMatchK []@), a field @Either a term@ becomes @zipMatchWithK (g :^: M0)@+-- (asking for @ZipMatchK (Either a)@), and a field @VarIdent@ becomes+-- @zipMatchWithK M0@ (asking for @ZipMatchK VarIdent@).+fieldZipper :: Set.Set Name -> [(Name, Exp)] -> Type -> Q Exp+fieldZipper zipped mappings type_ = case stripType type_ of+  VarT v | Just f <- lookup v mappings -> return f+  t -> do+    let (_headType, args) = unApply t+        zippedArgs = dropWhile (not . mentionsZipped zipped) args+    argZippers <- mapM (fieldZipper zipped mappings) zippedArgs+    let ms = foldr (\z m -> InfixE (Just z) (ConE '(:^:)) (Just m)) (ConE 'M0) argZippers+    return (AppE (VarE 'zipMatchWithK) ms)++-- | Does the type mention any of the zipped type parameters?+mentionsZipped :: Set.Set Name -> Type -> Bool+mentionsZipped zipped t = not (Set.null (Set.intersection zipped (freeVarsOfType t)))++-- | Split a type into its head and its arguments.+unApply :: Type -> (Type, [Type])+unApply = go []+  where+    go args (AppT f x)  = go (x : args) f+    go args (ParensT t) = go args t+    go args (SigT t _)  = go args t+    go args t           = (t, args)++-- | Drop parentheses and kind signatures.+stripType :: Type -> Type+stripType (ParensT t) = stripType t+stripType (SigT t _)  = stripType t+stripType t           = t++freeVarsOfType :: Type -> Set.Set Name+freeVarsOfType = \case+  VarT v      -> Set.singleton v+  AppT f x    -> freeVarsOfType f <> freeVarsOfType x+  AppKindT t _-> freeVarsOfType t+  SigT t _    -> freeVarsOfType t+  ParensT t   -> freeVarsOfType t+  InfixT l _ r-> freeVarsOfType l <> freeVarsOfType r+  UInfixT l _ r -> freeVarsOfType l <> freeVarsOfType r+  _           -> Set.empty

@@ -0,0 +1,139 @@+{-# LANGUAGE DataKinds             #-}+{-# LANGUAGE DeriveGeneric         #-}+{-# LANGUAGE DeriveTraversable     #-}+{-# LANGUAGE FlexibleContexts      #-}+{-# LANGUAGE FlexibleInstances     #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PatternSynonyms       #-}+{-# LANGUAGE TemplateHaskell       #-}+{-# LANGUAGE TypeFamilies          #-}+{-# LANGUAGE UndecidableInstances  #-}+{-# OPTIONS_GHC -Wno-orphans #-}++-- | Annotated syntax: one 'AnnSig' serving two annotations with opposite matching+-- behaviour, and the 'Bifoldable' asymmetry that α-equivalence relies on.+module Control.Monad.Free.Foil.AnnotatedSpec (spec) where++import           Data.Bifunctor.TH+import           Data.Functor.Const                (Const (..))+import           Data.Kind                         (Type)+import           Data.ZipMatchK+import           Generics.Kind.TH                  (deriveGenericK)+import qualified GHC.Generics                      as GHC+import           Test.Hspec++import qualified Control.Monad.Foil                as Foil+import           Control.Monad.Free.Foil+import           Control.Monad.Free.Foil.Annotated++-- | A minimal λ-calculus signature.+data LamSig scope term = AppSig term term | LamSig scope+  deriving (GHC.Generic, Functor, Foldable, Traversable)++deriveBifunctor ''LamSig+deriveBifoldable ''LamSig+deriveBitraversable ''LamSig+deriveGenericK ''LamSig+instance ZipMatchK LamSig++instance ZipMatchK Int where zipMatchWithK = zipMatchViaEq++-- | An annotation that ignores the term — a source position, say — and __is+-- compared__ when matching.+instance Eq a => ZipMatchK (Const (a :: Type)) where+  zipMatchWithK _ (Const l) (Const r)+    | l == r    = Just (Const l)+    | otherwise = Nothing++type Positioned = AnnAST Foil.NameBinder (Const Int) LamSig++-- | An annotation that holds a term at the node's own scope — a type, say.+--+-- It is optional, and it has to be: an annotation holding a term needs a term to+-- hold, so a closed annotated term could not be built at all without either a+-- 'Maybe' or a knot.+newtype TypeOf term = TypeOf (Maybe term)+  deriving (GHC.Generic, Functor, Foldable, Traversable)++deriveGenericK ''TypeOf++-- | Matching __ignores__ the annotation: it always succeeds, pairing the terms it+-- can and dropping what it cannot.+--+-- The /generic/ instance would not do: it compares the annotation's shape, so a+-- node with a memoised type would fail to match the same node without one.+instance ZipMatchK TypeOf where+  zipMatchWithK (f :^: M0) (TypeOf l) (TypeOf r) =+    Just (TypeOf (do { a <- l; b <- r; f a b }))++type Typed = AnnAST Foil.NameBinder TypeOf LamSig++-- | @\\x. x x@, annotated at every node with a source position.+positioned :: Int -> Positioned Foil.VoidS+positioned k = Foil.withFresh Foil.emptyScope $ \binder ->+  case Foil.assertDistinct binder of+    Foil.Distinct ->+      let x = Var (Foil.nameOf binder)+       in AnnNode (Const k)+            (LamSig (ScopedAST binder (AnnNode (Const k) (AppSig x x))))++-- | @\\x. x@, carrying the given type annotation at its root.+typed :: Maybe (Typed Foil.VoidS) -> Typed Foil.VoidS+typed ty = Foil.withFresh Foil.emptyScope $ \binder ->+  case Foil.assertDistinct binder of+    Foil.Distinct ->+      AnnNode (TypeOf ty) (LamSig (ScopedAST binder (Var (Foil.nameOf binder))))++-- | @\\x. x x@, with no type annotations, to have a structurally different term.+selfApp :: Typed Foil.VoidS+selfApp = Foil.withFresh Foil.emptyScope $ \binder ->+  case Foil.assertDistinct binder of+    Foil.Distinct ->+      let x = Var (Foil.nameOf binder)+       in AnnNode (TypeOf Nothing)+            (LamSig (ScopedAST binder (AnnNode (TypeOf Nothing) (AppSig x x))))++spec :: Spec+spec = do+  describe "an annotation that ignores the term (Const)" $ do+    it "matches when the annotations agree" $+      alphaEquiv Foil.emptyScope (positioned 1) (positioned 1) `shouldBe` True++    it "does not match when they differ" $+      alphaEquiv Foil.emptyScope (positioned 1) (positioned 2) `shouldBe` False++  describe "an annotation that holds a term (a type)" $ do+    it "is ignored when matching: terms differing only in their types are alpha-equivalent" $+      -- The property a dependent typechecker needs. It works because Bifoldable+      -- skips the annotation, so alphaEquiv never walks into it.+      alphaEquiv Foil.emptyScope (typed Nothing) (typed (Just (typed Nothing)))+        `shouldBe` True++    it "still distinguishes terms that differ in the term itself" $+      alphaEquiv Foil.emptyScope (typed Nothing) selfApp `shouldBe` False++    it "never forces the annotation: matching is lazy in it" $+      -- The blind instance returns 'Just' unconditionally with a thunked+      -- annotation, so an annotation that is bottom must not break the match.+      -- A strict instance would throw here instead of returning True.+      alphaEquiv Foil.emptyScope+        (typed (Just (error "annotation forced")))+        (typed (Just (error "annotation forced")))+        `shouldBe` True++  describe "freeVarsOfAnnotated" $+    it "sees a variable that freeVarsOf misses, because it occurs in an annotation" $+      Foil.withFresh Foil.emptyScope $ \outer ->+        case Foil.assertDistinct outer of+          Foil.Distinct ->+            let x = Var (Foil.nameOf outer)                      -- free at this scope+                scope = Foil.extendScope outer Foil.emptyScope+             in Foil.withFresh scope $ \inner ->+                  case Foil.assertDistinct inner of+                    Foil.Distinct ->+                      -- \y. y, annotated with a type that mentions x+                      let node = AnnNode (TypeOf (Just x))+                                   (LamSig (ScopedAST inner (Var (Foil.nameOf inner))))+                       in do+                            freeVarsOf node `shouldBe` []+                            length (freeVarsOfAnnotated node) `shouldBe` 1

@@ -0,0 +1,132 @@+{-# LANGUAGE DataKinds             #-}+{-# LANGUAGE DeriveGeneric         #-}+{-# LANGUAGE DeriveTraversable     #-}+{-# LANGUAGE FlexibleContexts      #-}+{-# LANGUAGE FlexibleInstances     #-}+{-# LANGUAGE GADTs                 #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE TemplateHaskell       #-}+{-# LANGUAGE TypeApplications      #-}+{-# LANGUAGE TypeFamilies          #-}+{-# LANGUAGE TypeOperators         #-}+{-# LANGUAGE UndecidableInstances  #-}++-- | The derived 'ZipMatchK' instance must agree with the generic one.+--+-- Both are available for the same type: 'deriveZipMatchK' provides the+-- instance, and 'genericZipMatchWithK' computes the generic answer without+-- needing one. So the test compares the two, on every pair of a set of sample+-- values, over the field shapes a signature actually uses.+module Data.ZipMatchK.THSpec (spec) where++import           Data.List.NonEmpty      (NonEmpty (..))+import           Generics.Kind           (LoT (..))+import qualified GHC.Generics            as GHC+import           Generics.Kind.TH        (deriveGenericK)+import           Test.Hspec++import           Data.ZipMatchK+import           Data.ZipMatchK.Generic  (genericZipMatchWithK)+import           Data.ZipMatchK.TH++-- | An annotation, standing for the extra parameter a generated signature has.+newtype Ann = Ann Int deriving (Eq, Show)+instance ZipMatchK Ann where zipMatchWithK = zipMatchViaEq++-- | A signature exercising every field shape the deriver has to compile: a+-- term, a scoped term, a constant, the extra parameter, a container of terms,+-- a container of scoped terms, and a nest of containers.+data RichSig a scope term+  = AppSig term term+  | LamSig scope+  | LitSig Ann+  | AnnSig a term+  | ManySig [term]+  | SomeSig (Maybe scope)+  | NestSig [Maybe term]+  | NonEmptySig (NonEmpty term)+  | EitherSig (Either Ann term)+  | PairSig (scope, term)+  | NullarySig+  deriving (GHC.Generic, Functor, Foldable, Traversable, Eq, Show)++deriveGenericK ''RichSig+deriveZipMatchK2 ''RichSig++-- | A plain signature bifunctor, with no extra parameters.+data LamSig scope term = App term term | Lam scope+  deriving (GHC.Generic, Functor, Foldable, Traversable, Eq, Show)++deriveGenericK ''LamSig+deriveZipMatchK ''LamSig++-- | A functor, as an annotation would be.+newtype Boxed term = Boxed [term]+  deriving (GHC.Generic, Functor, Foldable, Traversable, Eq, Show)++deriveGenericK ''Boxed+deriveZipMatchK1 ''Boxed++-- | Zip two values by equality, so that a zipped signature has the same type as+-- the signatures it came from, and can be compared with '=='.+zipEq :: Eq a => a -> a -> Maybe a+zipEq x y+  | x == y    = Just x+  | otherwise = Nothing++richSamples :: [RichSig Ann String String]+richSamples =+  [ AppSig "x" "y"+  , AppSig "x" "z"+  , LamSig "s"+  , LamSig "t"+  , LitSig (Ann 1)+  , LitSig (Ann 2)+  , AnnSig (Ann 1) "x"+  , AnnSig (Ann 2) "x"+  , ManySig []+  , ManySig ["x"]+  , ManySig ["x", "y"]+  , SomeSig Nothing+  , SomeSig (Just "s")+  , NestSig [Just "x", Nothing]+  , NestSig [Just "y", Nothing]+  , NonEmptySig ("x" :| [])+  , NonEmptySig ("x" :| ["y"])+  , EitherSig (Left (Ann 1))+  , EitherSig (Right "x")+  , PairSig ("s", "x")+  , NullarySig+  ]++lamSamples :: [LamSig String String]+lamSamples = [App "x" "y", App "x" "x", Lam "s", Lam "t"]++boxedSamples :: [Boxed String]+boxedSamples = [Boxed [], Boxed ["x"], Boxed ["x", "y"]]++spec :: Spec+spec = do+  describe "deriveZipMatchK2" $+    it "agrees with the generic instance on every pair of samples" $+      sequence_+        [ zipMatchWithK @_ @(RichSig Ann) mappings x y+            `shouldBe` genericZipMatchWithK @(RichSig Ann) mappings x y+        | x <- richSamples, y <- richSamples ]++  describe "deriveZipMatchK" $+    it "agrees with the generic instance on every pair of samples" $+      sequence_+        [ zipMatchWithK @_ @LamSig mappings x y+            `shouldBe` genericZipMatchWithK @LamSig mappings x y+        | x <- lamSamples, y <- lamSamples ]++  describe "deriveZipMatchK1" $+    it "agrees with the generic instance on every pair of samples" $+      sequence_+        [ zipMatchWithK @_ @Boxed (zipEq :^: M0) x y+            `shouldBe` genericZipMatchWithK @Boxed (zipEq :^: M0) x y+        | x <- boxedSamples, y <- boxedSamples ]+  where+    mappings :: Mappings (String ':&&: String ':&&: 'LoT0) (String ':&&: String ':&&: 'LoT0) (String ':&&: String ':&&: 'LoT0)+    mappings = zipEq :^: zipEq :^: M0