Issues

• Refreshing a telescope crashes when a later payload contains a binder

  fizruk/free-foil#99 · Filter by author fizruk opened on Oct 4, 2026

• The default unifyPatterns ignores the shape of a pattern

  fizruk/free-foil#98 · Filter by author fizruk opened on Oct 4, 2026

• Generic withPattern reorders the binders of a pattern

  fizruk/free-foil#97 · Filter by author fizruk opened on Oct 4, 2026

• alphaEquiv of lambda-pi's Impl.Foil captures a free name when a binder shadows the scope

  fizruk/free-foil#96 · Filter by author fizruk opened on Oct 4, 2026

• alphaEquiv is wrong for patterns with two or more binders

  fizruk/free-foil#95 · Filter by author fizruk opened on Oct 4, 2026

• Generic sinkabilityProof crashes on every binder

  fizruk/free-foil#94 · Filter by author fizruk opened on Oct 4, 2026

• MkFreeFoil: emit single-constructor pattern types as newtypes

  fizruk/free-foil#85 · Filter by author fizruk opened on Aug 28, 2026

• Add generic subsume combinators

  fizruk/free-foil#52 · Filter by author fizruk opened on Jul 25, 2026

• Support split signatures

  fizruk/free-foil#25 · Filter by author fizruk opened on Aug 22, 2024

• Support delayed substitutions

  fizruk/free-foil#24 · Filter by author fizruk opened on Aug 18, 2024

• Derive what is possible via GHC Generics

  fizruk/free-foil#23 · Filter by author fizruk opened on Aug 18, 2024

• Add Church-encoded version of the free foil

  fizruk/free-foil#22 · Filter by author fizruk opened on Aug 18, 2024

• Add strict versions of the foil and free foil

  fizruk/free-foil#21 · Filter by author fizruk opened on Aug 18, 2024

• Support terms in patterns with Template Haskell

  fizruk/free-foil#20 · Filter by author fizruk opened on Aug 18, 2024

• Implement the typechecker for lambda-pi

  fizruk/free-foil#19 · Filter by author fizruk opened on Aug 18, 2024

• Singleton scope types

  fizruk/free-foil#18 · Filter by author fizruk opened on Aug 18, 2024