free-foil-0.3.0: ChangeLog.md

# 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))
- Polykind `ZipMatchK` class with default generic implementation via [`kind-generics`](https://hackage.haskell.org/package/kind-generics) (see [#27](https://github.com/fizruk/free-foil/pull/27))
- New experimental TH generation for Free Foil with support for rich syntax in `Control.Monad.Free.Foil.TH.MkFreeFoil` (see [#28](https://github.com/fizruk/free-foil/pull/28))

# 0.1.0 — 2024-08-18

- Generalize functions for binders, support general patterns (see [#16](https://github.com/fizruk/free-foil/pull/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](https://github.com/fizruk/free-foil/pull/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](https://github.com/fizruk/free-foil/pull/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](https://github.com/fizruk/free-foil/pull/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](https://github.com/fizruk/free-foil/pull/11))
- Split `lambda-pi` into its own package (see [#10](https://github.com/fizruk/free-foil/pull/10))
- Switch to `template-haskell >= 2.21.0.0` (to support latest Stackage Nightly)
- Fix doctests (see [#9](https://github.com/fizruk/free-foil/pull/9))

# 0.0.1 — 2024-06-08

First release, corresponding to the ICCQ 2024 paper.