free-foil 0.3.2 → 0.3.3

raw patch · 6 files changed

+207/−3 lines, 6 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• ChangeLog.md +18/−0
• free-foil.cabal +2/−1
• src/Control/Monad/Foil/Internal.hs +65/−1
• src/Control/Monad/Foil/Relative.hs +1/−0
• src/Control/Monad/Foil/TH/MkInstancesFoil.hs +15/−1
• test/Control/Monad/Foil/UnifiablePatternSpec.hs +106/−0

@@ -1,5 +1,23 @@ # CHANGELOG for `free-foil` +# 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](https://github.com/fizruk/free-foil/issues/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.

@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack  name:           free-foil-version:        0.3.2+version:        0.3.3 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@@ -94,6 +94,7 @@   main-is: Spec.hs   other-modules:       Control.Monad.Foil.NameMapSpec+      Control.Monad.Foil.UnifiablePatternSpec       Control.Monad.Foil.UnifyNameBindersSpec       Control.Monad.Free.Foil.AnnotatedSpec       Control.Monad.Free.Foil.TH.MkFreeFoilSpec

@@ -226,6 +226,26 @@ -- does not clash with the scope, it can be used immediately, without renaming. -- -- This is a more general version of 'withRefreshed'.+--+-- Note that there is deliberately no fast path for the case when /every/ binder+-- of the pattern is already fresh in the ambient scope. It is tempting to test+-- all binders at once and, when none clashes, hand the continuation @sink@+-- instead of a renaming composed per binder. That would be unsound.+--+-- Even when a binder is not renamed, the per-binder step is not the identity:+-- 'addRename' /deletes/ the name from the substitution, which is how the binder+-- shadows an outer binding of the same raw name. For skipping that delete to be+-- harmless we would need the substitution's domain to avoid the pattern's binder+-- names, but the substitution's domain lives in the pattern's own scope @n@,+-- while freshness is tested against the unrelated ambient scope @o@.+--+-- The two can indeed disagree, because 'sink' is a coercion and does not rename:+-- a term built in a small scope keeps its binder names when it is placed in a+-- larger one, so a binder can share a raw name with its own enclosing scope. The+-- @whnf@ examples in @Language.LambdaPi.Impl.FreeFoilTH@ show a @λ x1@ nested+-- inside another @λ x1@ arising from ordinary evaluation. Handing such a caller+-- @sink@ would apply its substitution to a name the pattern binds — that is,+-- capture the bound variable. withRefreshedPattern   :: (Distinct o, CoSinkable pattern, Sinkable e, InjectName e)   => Scope o      -- ^ Ambient scope.@@ -245,6 +265,11 @@ -- | Refresh (if needed) bound variables introduced in a pattern. -- -- This is a version of 'withRefreshedPattern' that uses functional renamings instead of 'Substitution'.+--+-- Like 'withRefreshedPattern', this has no all-binders-already-fresh fast path,+-- and for the same reason. Here shadowing is handled by 'unsinkName' rather than+-- by a delete: a name the pattern binds is routed to 'injectName' and never+-- reaches the caller's renaming, whether or not the binder was refreshed. withRefreshedPattern'   :: (CoSinkable pattern, Distinct o, InjectName e, Sinkable e)   => Scope o@@ -612,9 +637,36 @@  -- | A pattern type is unifiable if it is possible to match two -- patterns and decide how to rename binders.+--+-- Note that the default implementation compares patterns only up to their+-- binders; see 'unifyPatterns' for what that does and does not distinguish. class CoSinkable pattern => UnifiablePattern pattern where   -- | Unify two patterns and decide which binders need to be renamed.   unifyPatterns :: Distinct n => pattern n l -> pattern n r -> UnifyNameBinders pattern n l r++  -- | The default implementation flattens both patterns to their binders (via+  -- 'nameBinderListOf') and unifies the resulting 'NameBinderList's. It therefore+  -- compares only the /number and order/ of binders, and ignores+  --+  -- * the constructor, so two patterns built from /different/ constructors with+  --   the same number of binders unify;+  -- * non-binding fields (locations, sorts, literals), whatever their values;+  -- * the nesting of sub-patterns, so @(x, (y, z))@ unifies with @((x, y), z)@.+  --+  -- For most languages this is the intended notion of α-equivalence: what the+  -- body of a binding construct can refer to is precisely the pattern's binders,+  -- in order. Since α-equivalence is defined in terms of 'unifyPatterns', this+  -- also means that terms differing only in such a pattern are α-equivalent.+  --+  -- If your patterns carry data that is semantically relevant, this default is+  -- not what you want and you should write the instance by hand — see the+  -- @UnifiablePattern Pattern@ instance in @Language.LambdaPi.Impl.Foil@ for a+  -- structural one. Use 'UnifiableInPattern' to compare non-binding fields, which+  -- also lets you deliberately ignore some of them (as+  -- @Language.LambdaPi.Impl.FreeFoilTH@ does for BNFC source positions).+  --+  -- The behaviour described here is pinned down in+  -- @Control.Monad.Foil.UnifiablePatternSpec@.   default unifyPatterns     :: (CoSinkable pattern, Distinct n)     => pattern n l -> pattern n r -> UnifyNameBinders pattern n l r@@ -625,6 +677,12 @@   unifyPatterns (NameBinderListCons x xs) (NameBinderListCons y ys) =     case (assertDistinct x, assertDistinct y) of       (Distinct, Distinct) -> unifyNameBinders x y `andThenUnifyPatterns` (xs, ys)+  -- Lists of different lengths are not unifiable. This case is reachable+  -- whenever a language has patterns that bind different numbers of names --+  -- a wildcard and a variable, say -- since the default 'unifyPatterns'+  -- flattens every pattern to a 'NameBinderList'. Note that this module sets+  -- @-Wno-incomplete-patterns@, so its absence was not reported.+  unifyPatterns _ _ = NotUnifiable  -- | Unification of values in patterns. -- By default, 'Eq' instance is used, but it may be useful to ignore@@ -907,7 +965,13 @@ addSubstList _ _ [] = error "cannot add a binder to Substitution since the value list does not have enough elements"  -- | Add variable renaming to a substitution.--- This includes the performance optimization of eliding names mapped to themselves.+--+-- When the binder is mapped to its own name, the name is /deleted/ from the+-- substitution rather than mapped to itself. This is an optimization, but it is+-- not only an optimization: it is also how the binder shadows an outer binding+-- of the same raw name, so the delete cannot be skipped even when nothing is+-- being renamed. See 'withRefreshedPattern' for why that rules out an+-- all-binders-fresh fast path. addRename :: InjectName e => Substitution e i o -> NameBinder i i' -> Name o -> Substitution e i' o addRename s@(UnsafeSubstitution env) b@(UnsafeNameBinder (UnsafeName name1)) n@(UnsafeName name2)     | name1 == name2 = UnsafeSubstitution (IntMap.delete name1 env)

@@ -1,3 +1,4 @@+{-# LANGUAGE DataKinds             #-} {-# LANGUAGE KindSignatures        #-} {-# LANGUAGE MultiParamTypeClasses #-} module Control.Monad.Foil.Relative where

@@ -168,11 +168,25 @@           where             xi = mkName ("x" ++ show i) --- | Generate 'Foil.Sinkable' and 'Foil.CoSinkable' instances.+-- | Generate a structural 'Foil.UnifiablePattern' instance, comparing+-- constructors and non-binding fields rather than only the binders.+--+-- This deriver does not work and has no call sites; see the deprecation note. deriveUnifiablePattern   :: Name -- ^ Type name for raw variable identifiers.   -> Name -- ^ Type name for raw patterns.   -> Q [Dec]+{-# DEPRECATED deriveUnifiablePattern+  "This deriver does not work and has no call sites. It reifies the raw \+  \(BNFC) pattern type and guesses the scope-safe type and constructor names \+  \by prefixing \"Foil\", and it rejects GADT constructors -- so it cannot \+  \handle the pattern types that mkFoilPattern and mkFreeFoil generate, nor a \+  \hand-written pattern GADT. Instead, derive GenericK and take an empty \+  \instance (see Control.Monad.Foil), or write the instance by hand as \+  \Language.LambdaPi.Impl.Foil does. Note that the empty instance compares \+  \only the binders; see UnifiablePattern. Structural derivation is tracked \+  \in https://github.com/fizruk/free-foil/issues/23. To be removed in the \+  \next major release." #-} deriveUnifiablePattern nameT patternT = do   TyConI (DataD _ctx _name patternTVars _kind patternCons _deriv) <- reify patternT 

@@ -0,0 +1,106 @@+{-# LANGUAGE DataKinds         #-}+{-# LANGUAGE GADTs             #-}+{-# LANGUAGE KindSignatures    #-}+{-# LANGUAGE RankNTypes        #-}+{-# LANGUAGE TemplateHaskell   #-}+{-# LANGUAGE TypeFamilies      #-}++-- | The default 'Foil.unifyPatterns' compares two patterns only up to their+-- binders: it flattens both to a 'Foil.NameBinderList' and unifies those. This+-- module pins down what that does /not/ distinguish, because the default is what+-- every client gets from an empty instance, and because two of its consequences+-- are surprising the first time they are met.+--+-- Since α-equivalence is defined in terms of 'Foil.unifyPatterns', these are also+-- statements about which terms the library considers α-equivalent.+--+-- None of this is a defect. What the body of a binding construct can refer to is+-- exactly the pattern's binders, in order, so for most languages the default is+-- the intended notion. It is a defect only for a language whose patterns carry+-- semantically relevant data — a constructor name in a @match@ branch, say — and+-- such a language should write 'Foil.unifyPatterns' by hand.+module Control.Monad.Foil.UnifiablePatternSpec (spec) where++import           Test.Hspec++import qualified Control.Monad.Foil as Foil+import           Generics.Kind.TH   (deriveGenericK)++-- | A pattern type with just enough structure to observe the default:+-- two constructors binding one name each, a nesting constructor, and a+-- constructor carrying a non-binding field.+data DemoPattern (n :: Foil.S) (l :: Foil.S) where+  DemoVar   :: Foil.NameBinder n l -> DemoPattern n l+  DemoBox   :: Foil.NameBinder n l -> DemoPattern n l+  DemoPair  :: DemoPattern n i -> DemoPattern i l -> DemoPattern n l+  DemoLabel :: String -> Foil.NameBinder n l -> DemoPattern n l++-- The configuration every client uses: derive the generic representation, then+-- take all four instances from their defaults.+deriveGenericK ''DemoPattern+instance Foil.SinkableK DemoPattern+instance Foil.HasNameBinders DemoPattern+instance Foil.CoSinkable DemoPattern+instance Foil.UnifiablePattern DemoPattern++-- | Do the two patterns unify with no renaming required? This is the observation+-- α-equivalence makes, phrased in the public API.+unifiesWithoutRenaming+  :: (Foil.UnifiablePattern pattern, Foil.Distinct n)+  => pattern n l -> pattern n r -> Bool+unifiesWithoutRenaming l r =+  case Foil.unifyPatterns l r of+    Foil.SameNameBinders{} -> True+    _                      -> False++-- | Run a continuation with three binders nested in 'Foil.emptyScope'.+withThreeBinders+  :: (forall i1 i2 l.+        Foil.NameBinder Foil.VoidS i1+     -> Foil.NameBinder i1 i2+     -> Foil.NameBinder i2 l+     -> r)+  -> r+withThreeBinders cont =+  Foil.withFresh Foil.emptyScope $ \x ->+    case Foil.assertDistinct x of+      Foil.Distinct ->+        Foil.withFresh (Foil.extendScope x Foil.emptyScope) $ \y ->+          case Foil.assertDistinct y of+            Foil.Distinct ->+              Foil.withFresh (Foil.extendScope y (Foil.extendScope x Foil.emptyScope)) $ \z ->+                cont x y z++spec :: Spec+spec = describe "the default unifyPatterns" $ do+  it "ignores the constructor, so different constructors with equal binders unify" $+    -- The consequence worth knowing: for a pattern type whose constructors mean+    -- different things -- the branches of a @match@, say -- the default calls two+    -- of them equal, and no type error says so.+    Foil.withFresh Foil.emptyScope (\x ->+      unifiesWithoutRenaming (DemoVar x) (DemoBox x))+      `shouldBe` True++  it "ignores non-binding fields, whatever their values" $+    Foil.withFresh Foil.emptyScope (\x ->+      unifiesWithoutRenaming (DemoLabel "left" x) (DemoLabel "right" x))+      `shouldBe` True++  it "ignores nesting, so (x, (y, z)) unifies with ((x, y), z)" $+    -- Both flatten to the same three binders in the same order.+    withThreeBinders (\x y z ->+      unifiesWithoutRenaming+        (DemoPair (DemoVar x) (DemoPair (DemoVar y) (DemoVar z)))+        (DemoPair (DemoPair (DemoVar x) (DemoVar y)) (DemoVar z)))+      `shouldBe` True++  it "still tells apart patterns binding different numbers of names" $+    -- The default is not vacuous: the binders themselves are compared. This case+    -- used to throw 'PatternMatchFail', because the 'NameBinderList' instance had+    -- no case for lists of unequal length and this module disables+    -- @-Wincomplete-patterns@.+    withThreeBinders (\x y _z ->+      unifiesWithoutRenaming+        (DemoVar x)+        (DemoPair (DemoVar x) (DemoVar y)))+      `shouldBe` False