CHANGELOG for free-foil

0.6.1 — 2026-10-27

This release lets substitute, alphaEquiv and unsafeEqAST specialise in client code, and fixes problems found by an audit of the documentation. One of the fixes changes the types of unsinkAST and nameSetSubsetOfScope, described first.

Breaking changes:

• unsinkAST requires DExt n l instead of Distinct l, and nameSetSubsetOfScope requires Ext n l: the scope l of the term (or set) must extend the scope n it is restricted to. Both compare raw identifiers, which identify a name only within one chain of scope extensions, so with unrelated scopes the answer was meaningless (see #127).
  • To migrate, bring Ext n l into scope where it is missing, e.g. with assertExt on the binder that leads from n to l, or from withFresh and withThinnedNameBinderList, which provide it.

Changed:

• zipMatchWith1, zipMatch1, zipMatchWith2 and zipMatch2 no longer require Traversable (or Bitraversable). alphaEquiv, unsafeEqAST and the functions behind them no longer require Bitraversable or SinkableK, and alphaEquivRefreshed requires Bifunctor instead of Bitraversable. None of them used these instances (see #125).

Fixes:

• alphaEquivRefreshed compares patterns with unifyPatternsIn, as alphaEquiv does (through the new unsafeEqASTIn). It compared them with unifyPatterns, which compares binders only, so it accepted terms whose binders differ in a payload (such as a type annotation) that alphaEquiv rejects (see #127).

Performance:

• substitute, alphaEquiv, unsafeEqAST and the functions behind them are INLINE wrappers around local loops, which take the instances from the wrapper. Inlined at a known signature, the loops use its instances directly. Before, they looked the instances up at every node, and a SPECIALIZE pragma in a client did not help: GHC split each function into a wrapper and a worker, since some of its dictionaries (such as Distinct) are never used at runtime, and the pragma reached only the wrapper. On the library’s benchmarks, α-equivalence takes 0.54–0.91 of the time and normalisation 0.58–0.85 (see #125).

New:

• unsafeEqASTIn and unsafeEqScopedASTIn compare two terms in one scope, like unsafeEqAST, but compare patterns with unifyPatternsIn, so the payloads of patterns are compared as well (see #127).
• unresolvedNamesWith is unresolvedNames for the arguments of tryConvertToASTWith: it also takes the table of constants, so that the constants no longer count as unresolved (see #127).
• Control.Monad.Free.Foil.Internal holds the implementation of Control.Monad.Free.Foil, which now has an export list. The loops behind α-equivalence, unsafeEqAST and unsafeEqASTIn (AlphaEquivLoops, alphaEquivLoops, EqLoops, unsafeEqLoops, EqInLoops, unsafeEqInLoops) are exported only from the internal module (see #125, #127).

Documentation:

• Doc comments and README passages that the code contradicted are corrected, among them the equation given for substituteRefreshed and the zipMatchK example. Haddock links written through a module alias (such as 'Foil.sink') resolve, where in 0.6.0 they pointed to a nonexistent page (see #126).

0.6.0 — 2026-10-26

This release lets mkFreeFoil generate most instances of a signature, and adds folds that traverse terms without rebuilding them. Several breaking changes come with it, described first.

Breaking changes:

• Scope indices have the nominal role, so coerce can no longer change a scope (see #113, #112). This applies to Name, NameBinder, Scope, NameSet, NameBinders, NameMap, the first index of Substitution, and the types of Control.Monad.Foil.Blocks.
  • To migrate, compare names of different scopes by nameId, and move a term to an extended scope with sink.
• mkFreeFoil generates the Bifunctor, Bifoldable, Bitraversable, ZipMatchK, ZipMatchFoldK and NFData instances of every signature, and NFData of every binding type (see #116, #118, #119).
  • To migrate, delete these instances (or the splices deriving them), or leave them out with mkFreeFoilWith.
  • Instances for the payload types (identifiers, positions) must now be declared before the mkFreeFoil splice.
• deriveCoSinkable takes the scope-safe pattern type, like the other derive* functions (see #122). The old function, which takes the raw identifier and pattern types, is renamed to mkCoSinkableFoilPattern.
• nameBinderListOf is a method of CoSinkable (see #110). A module that imports CoSinkable(..) and defines its own nameBinderListOf must hide one of them.
• deriveZipMatchK needs a ZipMatchFoldK instance for every container type applied to a zipped parameter (see #119). The library provides them for lists, Maybe, Either, pairs, NonEmpty, Sum and Product. Derive others with deriveZipMatchK1.

New:

• ZipMatchFoldK matches two values one level deep, like ZipMatchK, but folds the paired components into a monoid instead of rebuilding the value (see #119). deriveZipMatchK derives it together with ZipMatchK.
• zipMatchAllK and zipMatchAnyK (with 1 and 2 variants) check a relation on all or on any of the paired components (see #121).
• foldAST folds a term bottom-up, and hoistAST changes its signature by a natural transformation (see #115).
• deriveCoSinkable derives CoSinkable for a scope-safe pattern type (see #122).
• mkFreeFoilWith takes FreeFoilOptions to choose which instances to generate (see #116, #118).
• zipMatchKInstance builds a ZipMatchK instance from constructor fields, for Template Haskell code (see #116).
• gnameBinderListOf lists the binders of a pattern generically (see #110).

Performance:

• nameBinderListOf no longer traverses the pattern for the library’s instances and the generated ones (see #110, #123).
• withRefreshedPattern is INLINE, so that it specialises at a known pattern type (see #120).
• rnf of AST specialises at a known signature, and is about four times faster there (see #114).
• The generated signature instances are marked INLINE, since GHC does not inline the derived methods of a large signature (see #116).
• The ZipMatchK instances for Sum and Product are written out instead of generic, and no longer require Bitraversable (or Traversable) of the components (see #109).

0.5.0 — 2026-10-07

A release about binders. The law tests added after 0.4.0 (#100) found bugs in how binders are sunk, ordered, paired and transported, and this release fixes them. The fixes change α-equivalence for patterns of several binders, so the release is major. It also generates single-binder pattern types as newtypes and removes the functions deprecated in 0.3.3 and 0.4.0.

Breaking changes:

• The default unifyPatterns is structural, and it requires GenericK (#101, #98). It is the new gunifyPatterns. Two patterns unify when they consist of the same constructors, nested in the same way, and their binders are then paired in order. The old default compared only the binders, so it unified (x, _) with (_, y), and the conversion check of mltt accepted ill-typed programs. Non-binding fields are still ignored.

  • This changes α-equivalence for every client that takes the default, and reverses the plan in the 0.3.3 entry below to make structural derivation opt-in.
  • A pattern type that takes the default and has no GenericK instance no longer compiles. Derive GenericK for it or write unifyPatterns by hand.
  • mltt, soas and Impl.FreeFoilTH of lambda-pi take the default. For soas, whose binders form a flat list, the result is the same as before.

• transportPayload takes the ambient scope and requires RelMonad Name e instead of Sinkable e, and CoSinkable (Telescope label e) requires RelMonad Name e too (#101, #99). A refreshed binder renames the payloads after it, and renaming a payload with binders needs the scope. For instance, if x0 is refreshed to x1, a later payload λx1. x0 becomes λx2. x1. A hand-written withPattern passes the scope it holds before the payload’s binder (see the recipe in the documentation of transportPayload), and an instance carrying payloads of type e adds RelMonad Name e to its context.

  • The new instance RelMonad Name Name keeps telescopes of names working.
  • RelMonad is now defined in Control.Monad.Foil.Internal. Control.Monad.Foil.Relative re-exports it, so imports need no change.
  • telescopeParams and telescopePayloads keep their constraints.

• mkFreeFoil generates a pattern type as a newtype when its raw type has exactly one constructor with exactly one field, and that field is an identifier or a nested pattern, as in newtype Pattern = PatternVar VarIdent (#106, #85). Such a pattern costs no heap object of its own. Code that matches on the constructor or derives instances needs no change, but Template Haskell that reifys the generated type now sees a NewtypeD and has to accept it.

• The deprecated functions are removed (#104). Use sink1 instead of sinkContainer, and unsafeConvertToAST and unsafeConvertToScopedAST instead of convertToAST and convertToScopedAST (or tryConvertToAST, which reports unresolved identifiers instead of calling error). deriveUnifiablePattern is removed without a replacement: derive GenericK and take an empty UnifiablePattern instance, or write the instance by hand with unsafeUnifyPatternBinders, as Language.LambdaPi.Impl.Foil does.

New:

• unsafeUnifyPatternBinders pairs the binders of two patterns in order, for a hand-written unifyPatterns of a pattern with several binders. It is unsafe: call it only once the two patterns are known to agree on everything except the names of their binders, as gunifyPatterns does after its shape check and as Language.LambdaPi.Impl.Foil does in lambda-pi (#103, #102).

Fixes:

• The generic sinkabilityProof no longer fails with Non-exhaustive patterns in function sinkabilityProofK on a term with a binder (#101, #94). This also fixes the default coSinkabilityProof of every pattern that derives CoSinkable generically, and transportPayload on such a payload.

• alphaEquiv is correct for patterns of two or more binders (#101, #95). It used to pair the binders of the two sides wrongly, with both false negatives and false positives (λ[x0 x1]. x0 and λ[x1 x2]. x2 were α-equivalent). This affected the default unifyPatterns of every pattern type, the conversion check of mltt and isSolutionFor in soas.

  • NameBinderList, Telescope and the default unifyPatterns pair the binders of two patterns by position, all at once, and rename the binders of the right pattern to those of the left one. A single pair of binders keeps the convention of unifyNameBinders.
  • andThenUnifyPatterns and andThenUnifyNameBinders no longer compose renamings. A chain of verdicts that gives two binders the same name now answers NotUnifiable instead of a wrong verdict. With andThenUnifyNameBinders, a chain of two pairs always unifies.

• The generic withPattern, the default for a pattern type that derives HasNameBinders, keeps the binders of a pattern in their order (#101, #97). It used to put them in ascending order of names, which permuted the binders of a pattern whose names do not ascend, such as one that substitute, liftRM or refreshAST produces, and changed the meaning of the term. nameBinderListOf, addSubstPattern, the default unifyPatterns and alphaEquivRefreshed were affected through it. The instances that mkFreeFoil generates were not.

• In lambda-pi, alphaEquiv of Impl.Foil no longer captures a free name when a binder is already in the scope, as for a term built in a smaller scope and sunk (#101, #96). It falls back to alphaEquivRefreshed in that case.

0.4.0 — 2026-08-29

A release about units: checking a module independently of its neighbours, linking the results without renaming, and storing a checked one on disk. Scope restriction, a family of $O(1)$ sinks, and a linear α-equivalence rename path come with it.

Changed:

• Clients of mkFreeFoil must delete their own Foil.CoSinkable instances for the generated binding types, since mkFreeFoil now generates a concrete one (#87, #82). SinkableK, HasNameBinders, and UnifiablePattern remain the client’s.

• withPattern’s continuation now also receives the scope the pattern extends to, and so do those of withRefreshedPattern, withFreshPattern, and withRefreshedPattern' (#88, #84). Add the argument, and drop the extendScopePattern that recomputed it.

• mkFreeFoilConversions now requires Bifoldable on each signature, for the tryToX it generates. deriveBifoldable if a signature lacks it.

• freeVarsOf and freeVarsOfScopedAST no longer repeat a variable, and return names in ascending order of their identifiers rather than in the order the term mentions them.

• rawFreshName allocates 0 over a scope whose maximum is negative, leaving the negative range to explicit policy, and reports a scope holding maxBound as exhausted. Nothing changes on a scope without negative names.

• convertToAST and convertToScopedAST are deprecated in favour of unsafeConvertToAST and unsafeConvertToScopedAST, and sinkContainer in favour of sink1.

• containers >= 0.6.8 is required, for Data.IntSet.fromRange. binary and bytestring are new dependencies, both boot libraries.

New:

• Reserved name ranges, and linking. withFreshIn allocates inside a NameRange, so units drawing from disjoint reservations cannot collide. Control.Monad.Foil.Blocks tracks that as ExtWithin evidence and links two units with withDisjointUnion, one sweep over their range sets. checkExtScope and checkScopeUnion re-mint it for a unit loaded from a cache, and are documented as a trust boundary (#58).

• Deterministic stripes. Control.Monad.Foil.Registry gives each unit its own run of the name line, registerUnit handing out the StripeIndex that every reservation for that unit is derived from. A RegionLayout does the same for the locals of each declaration, so an edit to one file moves no name in another (#78, #80).

• Scope restriction. NameSet, withRestrictedScope, supportOf, withRelevantScope, and withThinnedNameBinderList: a term’s support, the scope it really inhabits, and a chain of binders thinned against a set of names (#56).

• Serialisation. Control.Monad.Free.Foil.Binary has opt-in orphan Binary instances for the syntax, and Control.Monad.Free.Foil.Artifact the checks that loading a stored unit rests on, with relocation of its constants (#68, #69). Decoding mints scope evidence, so both are a trust boundary.

• Patterns carrying scope-indexed payloads. PatternTransport is the sanctioned way to rebuild one, and the generic implementation now refuses such a pattern with a type error rather than mis-refreshing it silently (#71). Control.Monad.Foil.Telescope is the worked example, and unifyPatternsIn with the new AlphaEquiv class lets payloads take part in α-equivalence (#72, #79).

• Conversions that report rather than crash. tryConvertToAST gives the first unresolved identifier together with what was in scope there, in one pass, and unresolvedNames pays a second pass for all of them (#55). tryConvertToASTWith resolves an identifier to a whole term, for constants and abbreviations (#57); convertFromASTWith names free and bound variables separately, which a raw name alone cannot (#59); and toXIn and its siblings allocate within a given range, so the same source elaborates to the same term (#60).

• A family of $O(1)$ sinks. sink1 through a Functor and sink2 through a Bifunctor, with rewrite rules and hlint hints steering the elementwise forms towards them (#66).

• nameBinderListOf, the Id and RawName synonyms, and mapWithName are exported. The restriction and alphaequiv benchmarks are new.

Performance:

• alphaEquiv threads the verdict’s renamings down the recursion instead of applying them, which turns a quadratic rename path linear: 353 ms to 211 µs on two α-equivalent 2000-binder chains (#81).

• substitute short-circuits the empty substitution (#80).

• The binder and substitution operations are INLINABLE, so a downstream SPECIALIZE reaches through them, and the free foil’s Var unpacks its name (#86, #83).

Documentation:

• Every exported entity carries a @since, and CI fails if a new one lacks it.

• The haddocks and the READMEs are proofread. The README’s documentation links pointed at a version of the GitHub Pages haddocks that no longer exists, and point at Hackage now.

0.3.3 — 2026-07-20

A bugfix and documentation release. Upgrading from 0.3.2 needs no work.

Fixes:

• Unifying two patterns that bind different numbers of names no longer throws PatternMatchFail. The UnifiablePattern NameBinderList instance covered only the empty/empty and cons/cons cases, and since the default unifyPatterns flattens every pattern to a NameBinderList, this was reachable from any language with patterns of differing arity: in lambda-pi, alphaEquiv on λ_.x and λy.x crashed. Such patterns are now reported as not unifiable, so the terms are not α-equivalent. The missing case went unnoticed because Control.Monad.Foil.Internal sets -Wno-incomplete-patterns.

Documentation:

• UnifiablePattern states what its class default compares. The default flattens both patterns to their binders, so it ignores the constructor (two patterns built from different constructors with the same number of binders unify), non-binding fields, and the nesting of sub-patterns ((x, (y, z)) unifies with ((x, y), z)). For most languages this is the intended α-equivalence, since what a body can refer to is exactly the pattern’s binders in order, but every client gets it from an empty instance and nothing said so. The new Control.Monad.Foil.UnifiablePatternSpec pins the behaviour down.

• withRefreshedPattern and withRefreshedPattern' explain why they have no fast path for the case when every binder is already fresh in the ambient scope. Testing all binders at once and handing the continuation sink would be unsound: addRename’s delete is how a binder shadows an outer binding of the same raw name, and sink is a coercion that does not rename, so a binder can share a raw name with its own enclosing scope. addRename now says that its delete is not only an optimization.

Changed:

• deriveUnifiablePattern is deprecated. It reifies the raw (BNFC) pattern type and synthesises the scope-safe type and constructor names by prefixing "Foil", and it errors on GADT constructors, so it cannot produce an instance for any pattern type mkFoilPattern or mkFreeFoil generates, nor for a hand-written pattern GADT. It has no call sites and predates the GenericK route clients use. Deprecated rather than removed, since Control.Monad.Foil.TH re-exports the module wholesale; removal is scheduled for the next major. Structural derivation of UnifiablePattern remains tracked in #23, and when it lands it will be opt-in rather than a new default, since changing the default would silently change α-equivalence for every existing client.

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, #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). 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). A Scope is not sinkable and a NameMap must stay total, both noted with the function.

• zipmatchk and normalize benchmarks (#43, #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). 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).

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).

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.

Fixes:

• mkFreeFoil and mkFreeFoilConversions generated ill-typed code for a raw constructor whose shape does not line up with the free foil node it becomes (see #38):

  Let    ::= Pattern Term ScopedTerm        -- a term between the pattern and its scope
  LetRec ::= Pattern ScopedTerm ScopedTerm  -- one pattern binding two scopes
  

  • The pattern synonym’s arguments and its type signature were computed by two traversals that disagreed, and the conversions had the mirror problem.
  • A constructor binding several scopes binds the same raw name in each of them, so raw-to-foil now sends that one binder into every scoped child, and foil-to-raw reads it back from the first.
  • Constructors with at most one scoped child generate exactly what they did before.
  • Reported and diagnosed by @AbsoluteNikola, who had to vendor the generated code by hand in free-foil-refinement-types.

New functions, absorbed from the projects built on free-foil, several of which were importing Control.Monad.Foil.Internal to get at them (see #40):

• popNameBinder — the inverse of addNameBinder, for leaving a binder.
• withFreshNameBinderList — a fresh binder for each element of a list, bound to it in a NameMap.
• snocNameBinderList and concatNameBinderLists.
• nameBindersList, fromNameBindersList and nameMapToScope are now exported (they existed, but were unreachable).
• With thanks to @Probirochniy, @fedor-ivn and @snejugal (free-foil-hou), and to @evermake, @frog-da and @Vikono (free-foil-typecheck), whose copies of these helpers carried the comment “Should be in Control.Monad.Foil”.

Documentation:

• unifyNameBinders renames the binder with the larger name towards the one with the smaller name. That is safe, since the renaming is pushed through a term with liftRM, which refreshes a binder whenever it would capture. The haddock now says so, with a test to match (see #39). Raised by @AbsoluteNikola.

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, 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):

  • 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

  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:

  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)

• 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 NameBinders 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)

• 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 in mkPatternSynonyms (see #26)
• Polykind ZipMatchK class with default generic implementation via kind-generics (see #27)
• New experimental TH generation for Free Foil with support for rich syntax in Control.Monad.Free.Foil.TH.MkFreeFoil (see #28)

0.1.0 — 2024-08-18

• Generalize functions for binders, support general patterns (see #16)

  • Add withPattern method to CoSinkable. It can be seen as a CPS-style traversal over binders in a pattern. Our Template Haskell support covers generation of withPattern, so normally the user does not have to think about it.

  • Generalize many functions to work with arbitrary patterns, not just NameBinder:

    • withFreshPattern — to
    • withRefreshedPattern and withRefreshedPattern'
    • extendScopePattern — extend a given scope with all binders in a given pattern
    • namesOfPattern — collect all names from a pattern
    • unsinkNamePattern — try to unsink names from a scope extended with binders from a given pattern
    • assertDistinctPattern — establish that extended scope is distinct (if outer scope is)
    • assertDistinctExt — establish that extended scope is distinct and indeed an extension

  • Implement unification for patterns in unifyPatterns. This turns out to be one of the most difficult places, especially for compound patterns. Implementing patterns properly on the user side not comfortable at all! Luckily, we provide useful helpers like andThenUnifyPatterns and andThenUnifyNameBinders, as well as Template Haskell support to derive UnifiablePattern.

  • Generalize Free Foil to support arbitrary patterns.

  • The Foil and FreeFoilTH implementations now make use of the generalized pattern support.

0.0.3 — 2024-06-20

• Add α-equivalence checks and α-normalization (see #12):

  • Control.Monad.Foil now offers more helpers to work with binder renaming and binder unification. These helpers can be used to implement (efficient) α-equivalence.
  • In Control.Monad.Free.Foil general implementation of α-equivalence and α-normalization is provided.

• Add general conversion functions for free foil (see #14):

  • Control.Monad.Free.Foil now offers convertToAST and convertFromAST functions enabling easier implementation of conversions raw and scope-safe representations.

• Add Template Haskell functions for free foil (see #14):

  • Control.Monad.Free.Foil.TH contains many useful functions to generate free foil from a raw representation (e.g. generated via BNFC), including generation of the signature, convenient pattern synonyms, ZipMatch instance, and conversion helpers.

0.0.2 — 2024-06-18

• Improve TH to support parametrized data types (see #11)
• Split lambda-pi into its own package (see #10)
• Switch to template-haskell >= 2.21.0.0 (to support latest Stackage Nightly)
• Fix doctests (see #9)

0.0.1 — 2024-06-08

First release, corresponding to the ICCQ 2024 paper.