typelevel-rewrite-rules 0.1 → 1.0

raw patch · 23 files changed

+1258/−131 lines, 23 filesdep +containersdep −ghc-tcplugins-extradep ~basedep ~ghcdep ~transformers

Dependencies added: containers

Dependencies removed: ghc-tcplugins-extra

Dependency ranges changed: base, ghc, transformers, vinyl

Files

• CHANGELOG.md +22/−0
• README.md +668/−16
• src/TypeLevel/Rewrite.hs +73/−51
• src/TypeLevel/Rewrite/Internal/ApplyRules.hs +155/−0
• src/TypeLevel/Rewrite/Internal/DecomposedConstraint.hs +59/−0
• src/TypeLevel/Rewrite/Internal/Lookup.hs +6/−8
• src/TypeLevel/Rewrite/Internal/PrettyPrint.hs +34/−3
• src/TypeLevel/Rewrite/Internal/TypeEq.hs +1/−1
• src/TypeLevel/Rewrite/Internal/TypeNode.hs +35/−0
• src/TypeLevel/Rewrite/Internal/TypeRule.hs +31/−24
• src/TypeLevel/Rewrite/Internal/TypeSubst.hs +7/−0
• src/TypeLevel/Rewrite/Internal/TypeTemplate.hs +6/−5
• src/TypeLevel/Rewrite/Internal/TypeTerm.hs +10/−6
• test/should-compile/Data/Vinyl/TypeLevel/Test.hs +2/−1
• test/should-compile/GHC/TypeLits/RewriteRules.hs +12/−0
• test/should-compile/GHC/TypeLits/Test.hs +22/−0
• test/should-compile/InstanceConstraints/Laws.hs +7/−0
• test/should-compile/InstanceConstraints/Test.hs +51/−0
• test/should-compile/MonoKinds/Test.hs +2/−1
• test/should-compile/SamePackage/Test.hs +2/−1
• test/should-compile/Test.hs +5/−3
• test/should-compile/TypeLevel/Append/Test.hs +30/−2
• typelevel-rewrite-rules.cabal +18/−9

@@ -1,2 +1,24 @@+# 1.0+* Now supports ghc-8.10! Unfortunately, ghc-8.6 and ghc-8.8 are no longer+  supported.+* Now using ghc's builtin iteration limit instead of a hardcoded internal+  limit. Since ghc's limit is much smaller than our internal limit was, you may+  need to add something like `{-# OPTIONS_GHC -fconstraint-solver-iterations=100 #-}`+  if ghc recommends you to do so.+* Now making use of givens. That is, you can now call a function expecting+  (xs ~ rewritten-expr) given (xs ~ expr). Previously, you could only call a+  function expecting (xs ~ expr) given (xs ~ rewritten-expr).+* Now supports instance constraints. That is, you can now call a function which+  requires an `Eq (Vec rewritten-expr)` given an `Eq (Vec expr)`. Previously,+  we only supported equality constraints (`expr ~ rewritten-expr`).+* Now works with type variables of kind Nat and Symbol.+* The generated code now passes ghc's core-lint check.+* Error messages involving rewritten constraints now include the relevant+  rewrite rules.+* Bugfix: a spurious "the substitution forms a cycle" message was sometimes+  emitted even when the substitution rules did not form a cycle (see #15).+* Bugfix: rewrite rules were sometimes not firing (see #21).+* Bugfix: error messages were sometimes missing the error location (see #17).+ # 0.1 * initial release

@@ -1,8 +1,21 @@-# Type-Level Rewrite Rules [![Hackage](https://img.shields.io/hackage/v/typelevel-rewrite-rules.svg)](https://hackage.haskell.org/package/typelevel-rewrite-rules) [![Build Status](https://secure.travis-ci.org/gelisam/typelevel-rewrite-rules.png?branch=master)](http://travis-ci.org/gelisam/typelevel-rewrite-rules)+# Type-Level Rewrite Rules [![Hackage](https://img.shields.io/hackage/v/typelevel-rewrite-rules.svg)](https://hackage.haskell.org/package/typelevel-rewrite-rules) [![Build Status](https://github.com/gelisam/typelevel-rewrite-rules/workflows/CI/badge.svg)](https://github.com/gelisam/typelevel-rewrite-rules/actions)  Solve type equalities using custom type-level rewrite rules like `(n + 'Z) ~ n` and `((m + n) + o) ~ (m + (n + o))`. +* [The problem](#the-problem)+* [The solution](#the-solution)+* [Dangers](#dangers)+* [Troubleshooting](#troubleshooting)+* [Alternatives](#alternatives)+  + [Propagate the constraints](#propagate-the-constraints)+  + [Hasochism](#hasochism)+  + [Axiom](#axiom)+  + [ghc-typelits-natnormalise](#ghc-typelits-natnormalise)+  + [Thoralf](#thoralf)+  + [LiquidHaskell](#liquidhaskell)+  + [Ghosts of Departed Proofs](#ghosts-of-departed-proofs) + ## The problem  Type equalities involving type families sometimes get stuck:@@ -29,7 +42,7 @@   = (((xsM ++ empty1) ++ xsN) ++ empty2) ++ xsO ``` -This is unfortunate because the equation is valid; for any three concrete `Nat`s `l`, `m` and `n`, ghc would gladly accept the equation as true, but when `l`, `m` and `n` are abstract, it gets stuck.+This is unfortunate because the equation is valid; for any three concrete `Nat`s `m`, `n` and `o`, ghc would gladly accept the equation as true, but when `m`, `n` and `o` are abstract, it gets stuck.  ```haskell -- ok@@ -109,7 +122,7 @@  Typechecker plugins are used to extend ghc with domain-specific knowledge about particular types. For example, [ghc-typelits-natnormalise](https://hackage.haskell.org/package/ghc-typelits-natnormalise) simplifies type equalities involving natural numbers. It is the plugin's responsibility to ensure its simplifications are valid. -This plugin is both more general and more dangerous: it allows you to specify any rewrite rules you want, including invalid rules like `(n + 'Z) ~ 'Z` which break the type system:+This plugin is both more general and more dangerous: it allows us to specify any rewrite rules we want, including invalid rules like `(n + 'Z) ~ 'Z` which break the type system:  ```haskell {-# LANGUAGE DataKinds, RankNTypes, TypeFamilies, TypeApplications, TypeOperators #-}@@ -117,28 +130,30 @@                 -fplugin-opt=TypeLevel.Rewrite:My.RewriteRules.Nonsense #-} module My.Module where -import Data.Functor.Identity-import Data.Proxy-import Data.Vinyl-import Data.Vinyl.TypeLevel+import Prelude hiding ((++)) +import Data.Proxy (Proxy(Proxy))+import Data.Type.Nat (Nat(Z, S), type (+))+import Data.Vec.Lazy (Vec((:::), VNil), (++))+ import My.RewriteRules ()  withNonsense-  :: proxy as-  -> ((as ++ '[]) ~ '[] => r)+  :: proxy n+  -> ((n + 'Z) ~ 'Z => r)   -> r withNonsense _ r = r  -- |--- >>> recFromNowhere (Proxy @'[])--- {}--- >>> recFromNowhere (Proxy @'[Int, String])--- error: Impossible case alternative+-- >>> recFromNowhere (Proxy @'Z)+-- VNil+-- >>> let (n ::: VNil) = recFromNowhere (Proxy @('S 'Z))+-- >>> n+-- internal error: interpretBCO: hit a CASEFAIL recFromNowhere-  :: proxy as-  -> Rec Identity (as ++ '[])-recFromNowhere proxy = withNonsense proxy RNil+  :: proxy n+  -> Vec (n + 'Z) Int+recFromNowhere proxy = withNonsense proxy VNil ```  A more subtle danger is that even rewrite rules which are valid, such as `(x + y) ~ (y + x)`, can be problematic. The problem with this rule is that the right-hand side matches the left-hand side, and so the rewrite rule can be applied an infinite number of times to switch the arguments back and forth without making any progress. The same problem occurs if both `((m + n) + o) ~ (m + (n + o))` and `(m + (n + o)) ~ ((m + n) + o)` are included, the parentheses can get rearranged back and forth indefinitely.@@ -165,3 +180,640 @@ That error message is misleadingly followed by `Probable cause: bug in .hi-boot file, or inconsistent .hi file`, but the actual cause is that `MyRule` simply isn't defined in `My.RewriteRules`. Maybe it's a typo?  +## Alternatives++Remember, this typechecker plugin is dangerous! Have you considered these other, safer alternatives?++| Approach                                                | Effort                                                         | Limitations             | Safety concerns                         |+|---------------------------------------------------------|----------------------------------------------------------------|-------------------------|-----------------------------------------|+| [typelevel-rewrite-rules](#readme)                      | state rewrite rules                                            | no commutativity        | :construction: invalid rules, loops     |+| [Propagate the constraints](#propagate-the-constraints) |                                                                | no recursion            |                                         |+| [Hasochism](#hasochism)                                 | singletons boilerplate, prove properties, apply properties     |                         |                                         |+| [Axiom](#axiom) (at the call sites)                     | copy-paste equation                                            |                         | :bomb: invalid rules more likely        |+| [Axiom](#axiom) (when defining properties)              | state properties, apply properties                             |                         | :construction: invalid rules            |+| [ghc-typelits-natnormalise](#ghc-typelits-natnormalise) |                                                                | `GHC.TypeLits.Nat` only |                                         |+| [Thoralf](#thoralf)                                     | convert types and functions to Z3                              |                         | :construction: invalid conversion       |+| [LiquidHaskell](#liquidhaskell)                         | state refined types                                            | builtin types only      | :construction: invalid `assume` pragmas |+| [Ghosts of Departed Proofs](#ghosts-of-departed-proofs) | Argument boilerplate, state/prove properties, apply properties |                         | :construction: invalid `axiom` uses     |+++### Propagate the constraints++The easiest alternative is to propagate the constraints. We know that ghc would accept `(m + 'Z + n + 'Z + o) ~ (m + n + o)` if we had concrete `Nat`s for `m`, `n` and `o`; so let's wait until we have a concrete type-level values for them.++```haskell+simplify+  :: (m + 'Z + n + 'Z + o) ~ (m + n + o)+  => Vec  m a+  -> Vec 'Z a+  -> Vec  n a+  -> Vec 'Z a+  -> Vec  o a+  -> Vec (m + n + o) a+simplify xsM empty1 xsN empty2 xsO+  = (((xsM ++ empty1) ++ xsN) ++ empty2) ++ xsO++fooBarBazQuux :: Vec ('S ('S ('S ('S 'Z)))) String+fooBarBazQuux+  -- ('S ('S 'Z) + 'Z + 'S 'Z + 'Z + 'S 'Z) ~ ('S ('S 'Z) + 'S 'Z + 'S 'Z) holds+  -- because both sides evaluate to ('S ('S ('S ('S 'Z))))+  = simplify ("foo" ::: "bar" ::: VNil)+             VNil+             ("baz" ::: VNil)+             VNil+             ("quux" ::: VNil)+```++As you can see, once we call `simplify` with concrete values, the constraint gets discharged. The downside of this approach is that if there are a lot of intermediate calls between `simplify` and `fooBarBazQuux`, we might accumulate a lot of constraints. Also, sometimes this approach doesn't work when recursion is involved, because we would need to accumulate an infinite number of constraints.++```haskell+-- nope!+appendSingletons+  :: ( (m + 'Z) ~ m+     , (m + 'S 'Z + 'Z) ~ (m + 'S 'Z)+     , (m + 'S 'Z + 'S 'Z + 'Z) ~ (m + 'S 'Z + 'S 'Z)+     , ...+     , (m + 'S 'Z + n) ~ (m + 'S n)+     , (m + 'S 'Z + 'S 'Z + n) ~ (m + 'S 'Z + 'S n)+     , ...+     )+  => Vec m a+  -> Vec n (Vec ('S 'Z) a)+  -> Vec (m + n) a+appendSingletons xsM VNil+  -- uses (m + 'Z) ~ m+  = xsM+appendSingletons xsM (singleton1 ::: singletons)+  -- uses (m + 'S 'Z + n) ~ (m + 'S n)+  -- but we're recurring on a larger m, so we need to provide both+  -- (m + 'Z) ~ m and (m + 'S 'Z + n) ~ (m + 'S n) for that larger m;+  -- that is, we need to provide ((m + 'S 'Z) + 'Z) ~ (m + 'S 'Z) and+  -- ((m + 'S 'Z) + 'S 'Z + n) ~ ((m + 'S 'Z) + 'S n). But if we add+  -- those constraints to 'appendSingletons', we'll also need to provide+  -- those constraints for that larger m, etc.+  = appendSingletons (xsM ++ singleton1) singletons+```+++### Hasochism++If you're worried about accidentally breaking the type system by writing an invalid rule like `(n + 'Z) ~ 'Z`, try proving it correct. The [Hasochism](http://homepages.inf.ed.ac.uk/slindley/papers/hasochism.pdf) paper explains how; but as the title implies, writing proofs in Haskell can be a lot more painful than doing it in a language like Agda which was built for writing proofs. Doing it in Agda is not a painless experience either... but in Haskell, we need to write a lot of boilerplate before we can even begin writing the proofs:++```haskell+{-# LANGUAGE DataKinds, GADTs, TypeOperators #-}+++-- called 'SNat' in "Data.Type.Nat"+data Natty n where+  Zy :: Natty 'Z+  Sy :: Natty n -> Natty ('S n)++addy+  :: Natty m+  -> Natty n+  -> Natty (m + n)+addy Zy ny+  = ny+addy (Sy my) ny+  = Sy (addy my ny)+++-- called 'SNatI' in "Data.Type.Nat"+class NATTY n where+  natty :: Natty n++instance NATTY 'Z where+  natty = Zy++instance NATTY n => NATTY ('S n) where+  natty = Sy natty+```++Now that we have defined all of those, we can write the proofs. Here, I am proving `(n + 'Z) ~ n`, `((m + n) + o) ~ (m + (n + o))`, and `(m + n) ~ (n + m)`. The proofs are only a few lines long, but as the abundance of comments shows, careful thought is required in order to figure out what those few lines are.++```haskell+{-# LANGUAGE RankNTypes, ScopedTypeVariables, TypeApplications #-}++withRightIdentity+  :: Natty n+  -> ((n + 'Z) ~ n => r)+  -> r+withRightIdentity Zy r+  = r+    -- ('Z + 'Z) ~ 'Z  holds+    -- because ('Z + 'Z) evaluates to 'Z+withRightIdentity (Sy ny) r+  = withRightIdentity ny+    -- we now have (n + 'Z) ~ n+  $ r+    -- ('S n + 'Z) ~ 'S n  now holds+    -- because ('S n + 'Z) evaluates to ('S (n + 'Z))++withRightAssociative+  :: Natty m+  -> Natty n+  -> Natty o+  -> (((m + n) + o) ~ (m + (n + o)) => r)+  -> r+withRightAssociative Zy _ _ r+  = r+    -- (('Z + n) + o) ~ ('Z + (n + o))  holds+    -- because both sides evaluate to (n + o)+withRightAssociative (Sy my) ny oy r+  = withRightAssociative my ny oy+    -- we now have ((m + n) + o) ~ (m + (n + o))+  $ r+    -- (('S m + n) + o) ~ ('S m + (n + o))  now holds+    -- because (('S m + n) + o) evaluates to 'S ((m + n) + o)+    -- and ('S m + (n + o)) evaluates to 'S (m + (n + o))++withCommutative+  :: Natty m+  -> Natty n+  -> ((m + n) ~ (n + m) => r)+  -> r+withCommutative Zy ny r+  = withRightIdentity ny+    -- we now have (n + 'Z) ~ n+  $ r+    -- ('Z + n) ~ (n + 'Z)  now holds+    -- because both sides are equivalent to n+withCommutative my Zy r+  = withRightIdentity my+    -- we now have (m + 'Z) ~ m+  $ r+    -- (m + 'Z) ~ ('Z + m)  now holds+    -- because both sides are equivalent to m+withCommutative (Sy my) (Sy ny) r+  = withCommutative my (Sy ny)+    -- we now have (m + 'S n) ~ ('S n + m)+  $ withCommutative (Sy my) ny+    -- we now have ('S m + n) ~ (n + 'S m)+  $ withCommutative my ny+    -- we now have (m + n) ~ (n + m)+  $ r+    -- ('S m + 'S n) ~ ('S n + 'S m)  now holds+    -- because ('S m + 'S n) evaluates to 'S (m + 'S n)+    -- which is equivalent to 'S ('S (n + m))+    -- similarly ('S n + 'S m) becomes ('S ('S (m + n)))+    -- and ('S ('S n + m)) is equivalent to ('S ('S m + n))+```++One disadvantage of this approach is that careful thought is also needed when applying the properties we proved.++```+simplify+  :: forall m n o a. (NATTY m, NATTY n)+  => Vec  m a+  -> Vec 'Z a+  -> Vec  n a+  -> Vec 'Z a+  -> Vec  o a+  -> Vec (m + n + o) a+simplify xsM empty1 xsN empty2 xsO+  = withRightIdentity (natty @m)+    -- we now have (m + 'Z) ~ m+  $ withRightIdentity (natty @m `addy` natty @n)+    -- we now have ((m + n) + 'Z) ~ (m + n)+  $ (((xsM ++ empty1) ++ xsN) ++ empty2) ++ xsO+    -- (((m + 'Z) + n) + 'Z) + o+    -- becomes ((m + n) + 'Z) + o+    -- then (m + n) + o+```++As before, `simplify` has some constraints which propagate until we get concrete values for `m` and `n`.++```haskell+fooBarBazQuux :: Vec ('S ('S ('S ('S 'Z)))) String+fooBarBazQuux+  = simplify ("foo" ::: "bar" ::: VNil)+             VNil+             ("baz" ::: VNil)+             VNil+             ("quux" ::: VNil)+```++This time, however, the constraints don't accumulate as much, because we can construct derived `Natty`s from existing ones. In particular, the recursive function which was giving us trouble before no longer requires an infinite number of constraints.++```haskell+appendSingletons+  :: forall m n a. (NATTY m, NATTY n)+  => Vec m a+  -> Vec n (Vec ('S 'Z) a)+  -> Vec (m + n) a+appendSingletons+  = go (natty @m) (natty @n)++go+  :: Natty m+  -> Natty n+  -> Vec m a+  -> Vec n (Vec ('S 'Z) a)+  -> Vec (m + n) a+go my Zy xsM VNil+  = withRightIdentity my+    -- we now have (m + 'Z) ~ m+  $ xsM+    -- m becomes (m + 'Z)+go my (Sy ny) xsM (singleton1 ::: singletons)+  = withCommutative my (natty @('S 'Z))+    -- we now have (m + 'S 'Z) ~ ('S 'Z + m)+  $ withRightAssociative my (natty @('S 'Z)) ny+    -- we now have ((m + 'S 'Z) + n) ~ (m + ('S 'Z + n))+    -- or equivalently ('S m + n) ~ (m + 'S n)+  $ go (Sy my) ny (xsM ++ singleton1) singletons+    -- (xsM ++ singleton1) has type (Vec (m + 'S 'Z) a)+    -- which becomes (Vec ('S 'Z + m) a) and then (Vec ('S m) a)+    -- the recursive call produces a (Vec ('S m + n) a)+    -- which becomes (Vec (m + 'S n) a)+```++Another disadvantage of this approach is that the proofs have a runtime cost, as we recur down the `Natty` in order to construct our type-level constraint. Especially if, like me, you write `withCommutative` using an `O(3^n)` algorithm in order to avoid having to also prove an extra lemma!+++### Axiom++One way to avoid that runtime cost is to write a one-step "trust me" proof. Obviously, this brings us back to the danger zone.++The way to write a one-step "trust me" proof is not obvious, but can be found [in the innards of the `constraints` package](http://hackage.haskell.org/package/constraints-0.11.2/docs/src/Data.Constraint.Nat.html#axiom):++```haskell+{-# LANGUAGE DataKinds, PolyKinds, ScopedTypeVariables, TypeOperators #-}++import Data.Constraint (Dict(Dict), withDict)+import Data.Type.Nat (Nat(Z, S), type (+))+import Data.Vec.Lazy (Vec, (++))+import Unsafe.Coerce (unsafeCoerce)++axiom :: forall a b. Dict (a ~ b)+axiom = unsafeCoerce (Dict :: Dict (a ~ a))++simplify+  :: forall m n o a+   . Vec  m a+  -> Vec 'Z a+  -> Vec  n a+  -> Vec 'Z a+  -> Vec  o a+  -> Vec (m + n + o) a+simplify xsM empty1 xsN empty2 xsO+  = withDict (axiom :: Dict ((m + 'Z + n + 'Z + o) ~ (m + n + o)))+  $ (((xsM ++ empty1) ++ xsN) ++ empty2) ++ xsO+```++Notice that the comments indicating what information we learn from applying each property are gone! That's supposed to illustrate another advantage of this approach, namely that we no longer need to think too hard about which proof to apply in order to get our function to typecheck. Just write the function without using `withDict`, look at the two type-level expressions which ghc says don't match, and if they look to you like they should match, use `axiom` to assert that they do.++The biggest disadvantage of this technique is that if we use `axiom` too often, we're likely to spend less and less time worrying about whether the expressions we're pasting from ghc really are equivalent, and so we're likely to accidentally break the type system.++It's better to restrict `axiom` to a much smaller number of definitions, such as the proofs of a few key properties.++```haskell+rightIdentity+  :: proxy n+  -> Dict ((n + 'Z) ~ n)+rightIdentity _+  = axiom++rightAssociative+  :: proxy m+  -> proxy n+  -> proxy o+  -> Dict (((m + n) + o) ~ (m + (n + o)))+rightAssociative _ _ _+  = axiom+```++Unfortunately, with that variant, we once again need some careful thought when applying the properties.++```haskell+simplify+  :: forall m n o a+   . Vec  m a+  -> Vec 'Z a+  -> Vec  n a+  -> Vec 'Z a+  -> Vec  o a+  -> Vec (m + n + o) a+simplify xsM empty1 xsN empty2 xsO+  = withDict (rightIdentity (Proxy @m))+    -- we now have (m + 'Z) ~ m+  $ withDict (rightIdentity (Proxy @(m + n)))+    -- we now have ((m + n) + 'Z) ~ (m + n)+  $ (((xsM ++ empty1) ++ xsN) ++ empty2) ++ xsO+    -- (((m + 'Z) + n) + 'Z) + o+    -- becomes ((m + n) + 'Z) + o+    -- then (m + n) + o+```++This typechecker plugin, typelevel-rewrite-rules, can be thought as a way to get about the same level of safety as this variant, except that the properties are applied automatically, so we don't need to think hard at the use sites.++The reason it is not exactly the same level of safety is that while both approaches require us to vouch for the validity of a few key properties, typelevel-rewrite-rules has an extra way we can shoot ourselves in the foot: by writing a set of rules which loop indefinitely. This also means that there are properties, like commutativity, which cannot be expressed.+++### ghc-typelits-natnormalise++In order to express properties like commutativity, we need something more sophisticated than rewrite rules: we need a typechecker plugin like [ghc-typelits-natnormalise](https://hackage.haskell.org/package/ghc-typelits-natnormalise), which already knows about commutativity and more.++```haskell+{-# LANGUAGE DataKinds, GADTs, TypeOperators #-}+{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}++import Prelude hiding ((++))++import GHC.TypeLits++data Vec n a where+  VNil  :: Vec 0 a+  (:::) :: a -> Vec n a -> Vec (1 + n) a++(++)+  :: Vec m a+  -> Vec n a+  -> Vec (m + n) a+(++) VNil xsN+  = xsN+(++) (x ::: xsM) xsN+  = x ::: (xsM ++ xsN)++simplify+  :: Vec m a+  -> Vec 0 a+  -> Vec n a+  -> Vec 0 a+  -> Vec o a+  -> Vec (m + n + o) a+simplify xsM empty1 xsN empty2 xsO+  = (((xsM ++ empty1) ++ xsN) ++ empty2) ++ xsO++appendSingletons+  :: Vec m a+  -> Vec n (Vec 1 a)+  -> Vec (m + n) a+appendSingletons xsM VNil+  = xsM+appendSingletons xsM (singleton ::: singletons)+  = appendSingletons (xsM ++ singleton) singletons+```++Like typelevel-rewrite-rules, ghc-typelits-natnormalise automatically solves the constraints it knows about, we don't have to manually apply the properties like we did with the Hasochism and Axiom approaches. Furthermore, since ghc-typelits-natnormalise already knows that `(+)` is associative and commutative, we don't have to state nor prove the properties which we expect to hold.++When ghc-typelits-natnormalise works, it works great! Unfortunately, it only works in one narrow situation: when the type indices are `Nat`s from `GHC.TypeLits`. That's why I had to redefine `Vec` above: I cannot use ghc-typelits-natnormalise with the `Vec`s from `Data.Vec.Lazy`, as they use the `Nat`s from `Data.Type.Nat` instead.+++### Thoralf++The exact same code compiles with `ThoralfPlugin.Plugin` instead of `GHC.TypeLits.Normalise`. That's because [the Thoralf plugin](https://github.com/bgamari/the-thoralf-plugin#readme) also knows about the properties of `Nat`s from `GHC.TypeLits`. However, unlike ghc-typelits-natnormalise, Thoralf is [designed to be extensible](https://github.com/bgamari/the-thoralf-plugin/blob/master/DOCUMENTATION.md), so it's possible to teach Thoralf about the properties of `Nat`s from `Data.Type.Nat`! Here is the code which does so. Note that the `Vec`s in that code are `Thoralf`'s `Vec`s, not the `Vec`s from `Data.Vec.Lazy`. ++```haskell+{-# LANGUAGE GADTs, PackageImports, RankNTypes #-}+module ThoralfPlugin.Encode.Nat (natTheory) where++import "base" Control.Monad (guard)+import "ghc" DataCon (DataCon, promoteDataCon)+import "ghc" FastString (fsLit)+import "ghc" GhcPlugins (getUnique)+import "ghc" Module (Module, mkModuleName)+import "ghc" OccName (mkDataOcc, mkTcOcc)+import "ghc" TcPluginM (FindResult(..), TcPluginM, findImportedModule, lookupOrig, tcLookupDataCon, tcLookupTyCon)+import "ghc" TyCon (TyCon(..))+import "ghc" Type (Type, splitTyConApp_maybe, tyVarKind)+import ThoralfPlugin.Encode.TheoryEncoding++importModule :: String -> String -> TcPluginM Module+importModule packageName moduleName = do+  let package = fsLit packageName+  Found _ module_ <- findImportedModule (mkModuleName moduleName) (Just package)+  pure module_++findTyCon :: Module -> String -> TcPluginM TyCon+findTyCon md strNm = do+    name <- lookupOrig md (mkTcOcc strNm)+    tcLookupTyCon name++findDataCon :: Module -> String -> TcPluginM DataCon+findDataCon md strNm = do+    name <- lookupOrig md (mkDataOcc strNm)+    tcLookupDataCon name++expectTyCon :: TyCon -> Type -> Maybe [Type]+expectTyCon expectedTyCon ty = do+  (actualTyCon, args) <- splitTyConApp_maybe ty+  guard (actualTyCon == expectedTyCon)+  pure args++addZ3Numbers :: Vec n String -> String+addZ3Numbers VNil      = "0"+addZ3Numbers (x :> xs) = "(+ " ++ x ++ " " ++ addZ3Numbers xs ++ ")"++addExtraZ3Numbers :: [Int] -> Vec n String -> String+addExtraZ3Numbers = go addZ3Numbers+  where+    go :: (forall m. Vec m String -> String) -> [Int] -> Vec n String -> String+    go acc []     = acc+    go acc (x:xs) = go (acc . (show x :>)) xs++mkTyConvCont :: [Type] -> [Int] -> TyConvCont+mkTyConvCont args extra = go VNil (reverse args)+  where+    go :: Vec n Type -> [Type] -> TyConvCont+    go acc []     = let toZ3 z3Numbers VNil = addExtraZ3Numbers extra z3Numbers+                    in TyConvCont acc VNil toZ3 []+    go acc (x:xs) = go (x :> acc) xs++convertTyConToZ3 :: TyCon -> Int -> [Int] -> Type -> Maybe TyConvCont+convertTyConToZ3 tyCon argCount extra ty = do+  args <- expectTyCon tyCon ty+  guard (length args == argCount)+  pure $ mkTyConvCont args extra++natTheory :: TcPluginM TheoryEncoding+natTheory = do+  dataDotNat        <- importModule "fin" "Data.Nat"+  dataDotNatDotType <- importModule "fin" "Data.Type.Nat"+  nat <- findTyCon dataDotNat "Nat"+  z <- promoteDataCon <$> findDataCon dataDotNat "Z"+  s <- promoteDataCon <$> findDataCon dataDotNat "S"+  plus <- findTyCon dataDotNatDotType "Plus"+  pure $ emptyTheory+    { kindConvs = [ \ty -> do [] <- expectTyCon nat ty+                              pure $ KdConvCont VNil (\VNil -> "Int")+                  ]+    , tyVarPreds = \tv -> do _ <- expectTyCon nat (tyVarKind tv)+                             pure ["(assert (<= 0 " ++ show (getUnique tv) ++ "))"]+                   +    , typeConvs = [ convertTyConToZ3 z    0 []+                  , convertTyConToZ3 s    1 [1]+                  , convertTyConToZ3 plus 2 []+                  ]+    }+```++That example code illustrates a few disadvantages of this approach. First, the module name `ThoralfPlugin.Encode.Nat`. This hints at the disadvantage that the way in which we extend Thoralf is rather invasive: we don't extend Thoralf by importing a library or by pointing it to some extension code, but by forking the Thoralf repository and adding a new module to its source code. Next, the imports from the "ghc" package. This hints at the disadvantage that we need to be familiar with (a small part of) the ghc API in order to implement the part of the extension which imports modules, types and data constructors, and the part which converts type expressions into Z3 expressions. The final disadvantage is that we also need to be familiar with the Z3 syntax; although as you can see, here I am simply converting `Nat` to `Int` and `'S ('S 'Z)` to `(+ 1 (+ 1 0))`, so it's not that hard.++Once again, we don't have to state the properties which we expect to hold, as Z3 already knows that `(+)` is associative and commutative. Unlike with ghc-typelits-natnormalise, this does not mean we are limited to a single definition of `Nat` and `(+)`. Z3 only knows about one `(+)`, but it doesn't know about any particular Haskell definition of `(+)`; the magic of Thoralf is that it allows us to translate all the Haskell definitions of `(+)` to Z3's definition of `(+)`, which in turn allows Thoralf to solve type-equality constraints for all of those Haskell definitions.++Z3 is an SMT solver, where "SMT" stands for "Satisfiability-Modulo-Theories" and "theories" refers to the set of types and functions like `Int` and `(+)` which the solver knows about. Thankfully, the translation doesn't have to be one-to-one, and so it is possible to combine several Z3 types and functions in order to encode Haskell types and function for which Z3 doesn't have an equivalent. For example, Z3 only knows about integers, not about natural numbers, and so above we used `(assert (<= 0 n))` to encode Haskell's `Nat`s as non-negative Z3 `Int`s. ++The "satisfiability solver" part means that Thoralf is not rewriting the type equalities it encounters to hopefully-simpler type equalities using the properties it knows about, but rather, it searches for a counter-example which would demonstrate that the type equality is invalid. Even though there are infinitely-many `Int`s, Z3 somehow manages to exhaustively search the space in a finite amount of time, and so if Z3 cannot find a counter-example, then Thoralf knows that the type equality holds and discharges the constraint.+++### LiquidHaskell++[LiquidHaskell](https://github.com/ucsd-progsys/liquidhaskell#readme) is in a slightly different category than the other approaches because it doesn't discharge type-equality constraints. Nevertheless, it is very similar to Thoralf in that it also uses an SMT solver to figure out whether to accept or reject the program. Instead of looking at equality constraints, LiquidHaskell looks at `{-@ ... @-}` annotations which specify more precise type signatures for our Haskell functions. Those type signatures use refinement types, which look similar to the GADT-based type signatures we've been using up to now, except they use predicates and support subtyping: if P implies Q, then `{v : T | P}` is a subtype of `{v : T | Q}`.++```haskell+{-@+measure myLen :: [a] -> Int+myLen []     = 0+myLen (x:xs) = 1 + myLen xs+@-}++type Vec a = [a]++{-@ type VecN a N = {v : Vec a | myLen v = N} @-}++{-@ assume (++) :: xs:Vec a -> ys:Vec a -> VecN a {myLen xs + myLen ys} @-}++{-@ simplify+      :: xs:Vec a+      -> VecN a 0+      -> ys:Vec a+      -> VecN a 0+      -> zs:Vec a+      -> VecN a {myLen xs + myLen ys + myLen zs} @-}+simplify :: [a] -> [a] -> [a] -> [a] -> [a] -> [a]+simplify xs empty1 ys empty2 zs+  = (((xs ++ empty1) ++ ys) ++ empty2) ++ zs++{-@ appendSingletons+      :: xs:Vec a+      -> singletons:Vec (VecN a 1)+      -> VecN a {myLen xs + myLen singletons} @-}+appendSingletons :: [a] -> [[a]] -> [a]+appendSingletons xsM []+  = xsM+appendSingletons xsM (singleton : singletons)+  = appendSingletons (xsM ++ singleton) singletons+```++Once again, LiquidHaskell knows that `(+)` is associative and commutative, so we don't have to state the properties which we expect to hold. We don't need to write converters from Haskell types and functions to Z3 types and functions like we did with Thoralf, which means we have to use the types and functions which LiquidHaskell already knows about. Thankfully, these types and functions are the `Int` and `(+)` from Haskell which we are already familiar with, not Z3's `Int` and `(+)`. The way in which we write the `P` and `Q` predicates for our refinement types is also familiar: we write ordinary recursive Haskell functions, such as `myLen` above.++The main disadvantage of this approach is the same as with ghc-typelits-natnormalise: we cannot reuse the existing `Vec` from `Data.Vec.Lazy` nor the existing `Nat` from `Data.Type.Nat`, we have to define a separate type inside LiquidHaskell's framework. There are several reasons for this. First, as I've just explained, we are limited to the types which LiquidHaskell already knows about, and `Nat` is not on that list. Second, `Vec` is a GADT which uses a `Nat` as a type index, but LiquidHaskell uses refinement types, not GADTs. Finally, LiquidHaskell's refinement types are stricter than the Haskell types it refines, and so LiquidHaskell provides more type safety by rejecting more programs. By contrast, our original `Vec`-based program was already rejected by ghc's regular type checker, and so in order to reuse `Vec`, we need an approach which rejects fewer programs, by discharging some constraints.++In the example above, while we were not able to reuse `Vec`, we were able to use lists, a much more ubiquitous type than `Vec` for which many more functions already exist. In fact, `appendSingletons = foldl' (++)`! Unfortunately, we cannot use that simpler definition, because LiquidHaskell needs to observe the recursive call in order to confirm that `appendSingletons` does have the refined type we stated. +++### Ghosts of Departed Proofs++The [Ghosts of Departed Proofs](https://hackage.haskell.org/package/gdp) library supports a variety of styles, including refined types like LiquidHaskell, computer-checked proofs like Hasochism, and using typechecker plugins and "trust me" axioms to avoid having to write those proofs. However, its signature style involves giving names to arguments and functions, like this:++```haskell+{-# LANGUAGE TypeOperators #-}++import GDP++newtype Zero = Zero Defn+newtype Plus m n = Plus Defn++zero :: Int ~~ Zero+zero = defn 0++plus :: (Int ~~ m)+     -> (Int ~~ n)+     -> (Int ~~ Plus m n)+plus m n = defn (the m + the n)+```++The type signature says that given two numbers named `m` and `n`, we can construct a number named `Plus m n`. The only way to obtain a value with that name is to call `plus`.++We can now use those names to express some properties which we assert to be true about those functions:++```haskell+instance Associative Plus+instance Commutative Plus++zeroPlus :: Proof (Plus Zero n == n)+zeroPlus = axiom++plusZero :: Proof (Plus n Zero == n)+plusZero = axiom+```++Using those properties, we can in turn write some proofs showing that some other properties are a consequence of the asserted properties.++```haskell+simplifyZNZ :: Proof (Zero `Plus` n `Plus` Zero == n)+simplifyZNZ+    = -- (Zero `Plus` n) `Plus` Zero+      plusZero+  ==. -- Zero `Plus` n+      zeroPlus+      -- n+```++In the proof above, I was lucky that each equality proof applied to the entire name, so I could simply concatenate a few existing proofs. A more common use case is to apply an equality proof to a portion of the name, in which case we need to specify which portion we have in mind. In order to do that, we need to write a bit of boilerplate in order to identify the various arguments to each function name.++```haskell+{-# LANGUAGE DataKinds, MultiParamTypeClasses, TypeFamilies #-}++instance Argument (Plus m n) 0 where+  type GetArg (Plus m n) 0    = m+  type SetArg (Plus m n) 0 m' = Plus m' n++instance Argument (Plus m n) 1 where+  type GetArg (Plus m n) 1    = n+  type SetArg (Plus m n) 1 n' = Plus m n'+```++We can now use those to `apply` an equality proof to a portion of a name.++```haskell+{-# LANGUAGE TypeApplications #-}++simplifyMZNZO :: Proof ( (m `Plus` Zero `Plus` n `Plus` Zero `Plus` o)+                      == (m `Plus` n `Plus` o)+                       )+simplifyMZNZO+    = -- (((m `Plus` Zero) `Plus` n) `Plus` Zero) `Plus` o+      ( apply (arg @0)+      $ plusZero+      )+  ==. -- ((m `Plus` Zero) `Plus` n) `Plus` o+      ( apply (arg @0)+      $ apply (arg @0)+      $ plusZero+      )+      -- (m `Plus` n) `Plus` o+```++Proofs with GDT can be more tedious than with Hasochism, for two reasons. First, with Hasochism, `(+)` can be a type family, and so we don't need to explicitly simplify `'Z + n` to `n` because the former automatically computes to the latter. Second, Hasochism uses the builtin `~` type equalities, which the typechecker uses when comparing types at any depth, and so it is not necessary to specify where we want to `apply` each equality proof.++On the flip side, the fact that GDP uses its own equality type `Proof (x == y)` instead of the builtin `~` allows GDP to represent properties other than equalities.++```haskell+data Positive xs++positivePlusPositive :: Proof (Positive m)+                     -> Proof (Positive n)+                     -> Proof (Positive (Plus m n))+positivePlusPositive _ _ = axiom+```++A function may ask for a `Proof` value in order to guarantee that some property holds about its arguments.++```haskell+divide1 :: Int+        -> (Int ~~ denominator)+        -> Proof (Positive denominator)+        -> Int+```++But it is more common to associate a proof with the value it describes, like this:++```haskell+divide2 :: Int+        -> (Int ~~ denominator ::: Positive denominator)+        -> Int+```++That type asks for an `Int` named `denominator` such that `Positive denominator` holds. GDP also offers the refinement-type syntax `Int ? Positive` for this common case in which the proof is a proposition applied to the name and that name does not occur anywhere else in the type signature.

@@ -1,4 +1,4 @@-{-# LANGUAGE RecordWildCards, ViewPatterns #-}+{-# LANGUAGE LambdaCase, OverloadedStrings, RecordWildCards, ViewPatterns #-} module TypeLevel.Rewrite (plugin) where  import Control.Monad@@ -6,19 +6,23 @@ import Control.Monad.Trans.Writer import Data.Foldable import Data.Traversable-import GHC.TcPluginM.Extra (evByFiat)  -- GHC API+import Coercion (Role(Representational), mkUnivCo)+import Constraint (CtEvidence(ctev_loc), Ct, ctEvExpr, ctLoc, mkNonCanonical)+import GhcPlugins (PredType, SDoc, eqType, fsep, ppr) import Plugins (Plugin(pluginRecompile, tcPlugin), CommandLineOption, defaultPlugin, purePlugin)-import TcEvidence (EvTerm)-import TcPluginM (TcPluginM, newCoercionHole)+import TcEvidence (EvExpr, EvTerm, evCast)+import TcPluginM (newWanted) import TcRnTypes-import TcType (TcPredType)+import TyCoRep (UnivCoProvenance(PluginProv)) import TyCon (synTyConDefn_maybe)-import Type (EqRel(NomEq), PredTree(EqPred), Type, classifyPredType, mkPrimEqPred) +import TypeLevel.Rewrite.Internal.ApplyRules+import TypeLevel.Rewrite.Internal.DecomposedConstraint import TypeLevel.Rewrite.Internal.Lookup import TypeLevel.Rewrite.Internal.PrettyPrint+import TypeLevel.Rewrite.Internal.TypeEq import TypeLevel.Rewrite.Internal.TypeRule import TypeLevel.Rewrite.Internal.TypeTerm @@ -68,7 +72,9 @@   :: [CommandLineOption]   -> TcPluginM [TypeRule] lookupTypeRules [] = do-  usage (show ["TypeLevel.Append.RightIdentity", "TypeLevel.Append.RightAssociative"])+  usage (show [ "TypeLevel.Append.RightIdentity" :: String+              , "TypeLevel.Append.RightAssociative"+              ])         "[]" lookupTypeRules fullyQualifiedTypeSynonyms = do   -- ["TypeLevel.Append.RightIdentity", "TypeLevel.Append.RightAssociative"]@@ -76,7 +82,7 @@     -- "TypeLevel.Append.RightIdentity"     case splitLastDot fullyQualifiedTypeSynonym of       Nothing -> do-        usage (show "TypeLevel.Append.RightIdentity")+        usage (show ("TypeLevel.Append.RightIdentity" :: String))               (show fullyQualifiedTypeSynonym)       Just (moduleNameStr, tyConNameStr) -> do         -- ("TypeLevel.Append", "RightIdentity")@@ -110,31 +116,30 @@   }  -asEqualityConstraint-  :: Ct-  -> Maybe (Type, Type)-asEqualityConstraint ct = do-  let predTree-        = classifyPredType-        $ ctEvPred-        $ ctEvidence-        $ ct-  case predTree of-    EqPred NomEq lhs rhs-      -> pure (lhs, rhs)-    _ -> Nothing+mkErrCtx+  :: SDoc+  -> ErrCtxt+mkErrCtx errDoc = (True, \env -> pure (env, errDoc)) -toEqualityConstraint-  :: Type -> Type -> CtLoc -> TcPluginM Ct-toEqualityConstraint lhs rhs loc = do-  let tcPredType :: TcPredType-      tcPredType = mkPrimEqPred lhs rhs+newRuleInducedWanted+  :: Ct+  -> TypeRule+  -> PredType+  -> TcPluginM CtEvidence+newRuleInducedWanted oldCt rule newPredType = do+  let loc = ctLoc oldCt -  hole <- newCoercionHole tcPredType+  -- include the rewrite rule in the error message, if any+  let errMsg = fsep [ "From the typelevel rewrite rule:"+                    , ppr (fromTypeRule rule)+                    ]+  let loc' = pushErrCtxtSameOrigin (mkErrCtx errMsg) loc -  pure $ mkNonCanonical-       $ CtWanted tcPredType (HoleDest hole) WDeriv loc+  wanted <- newWanted loc' newPredType +  -- ctLoc only copies the "arising from function X" part but not the location+  -- etc., so we need to copy the rest of it manually+  pure $ wanted { ctev_loc = loc' }  solve   :: [TypeRule]@@ -144,30 +149,47 @@   -> TcPluginM TcPluginResult solve _ _ _ [] = do   pure $ TcPluginOk [] []-solve rules _ _ cts = do-  replaceCts <- execWriterT $ do-    for_ cts $ \ct -> do-      -- ct => ...-      for_ (asEqualityConstraint ct) $ \(lhs, rhs) -> do-        -- lhs ~ rhs => ...+solve rules givens _ wanteds = do+  typeSubst <- execWriterT $ do+    for_ givens $ \given -> do+      for_ (asEqualityConstraint given) $ \(lhs, rhs) -> do+        -- lhs ~ rhs+        -- where lhs is typically an expression and rhs is typically a variable+        let var = TypeEq rhs+        let val = toTypeTerm lhs+        tell [(var, val)] -        let lhsTypeTerm = toTypeTerm lhs-        let rhsTypeTerm = toTypeTerm rhs-        let lhsTypeTerm' = applyRules rules lhsTypeTerm-        let rhsTypeTerm' = applyRules rules rhsTypeTerm+  replaceCts <- execWriterT $ do+    for_ wanteds $ \wanted -> do+      -- wanted => ...+      for_ (asDecomposedConstraint wanted) $ \types -> do+        -- C a b c => ... -        unless (lhsTypeTerm' == lhsTypeTerm && rhsTypeTerm' == rhsTypeTerm) $ do-          -- lhs' ~ rhs' => ...-          let lhs' = fromTypeTerm lhsTypeTerm'-          let rhs' = fromTypeTerm rhsTypeTerm'+        -- C a b c+        let typeTerms = fmap toTypeTerm types+        let predType = fromDecomposeConstraint types -          ct' <- lift $ toEqualityConstraint lhs' rhs' (ctLoc ct)+        for_ (applyRules typeSubst rules typeTerms) $ \(rule, typeTerms') -> do+          -- C a' b' c'+          let types' = fmap fromTypeTerm typeTerms'+          let predType' = fromDecomposeConstraint types' -          let replaceCt :: ReplaceCt-              replaceCt = ReplaceCt-                { evidenceOfCorrectness  = evByFiat "TypeLevel.Rewrite" lhs' rhs'-                , replacedConstraint     = ct-                , replacementConstraints = [ct']-                }-          tell [replaceCt]+          unless (eqType predType' predType) $ do+            -- co :: C a' b' c'  ~R  C a b c+            let co = mkUnivCo+                       (PluginProv "TypeLevel.Rewrite")+                       Representational+                       predType'+                       predType+            evWanted' <- lift $ newRuleInducedWanted wanted rule predType'+            let wanted' = mkNonCanonical evWanted'+            let futureDict :: EvExpr+                futureDict = ctEvExpr evWanted'+            let replaceCt :: ReplaceCt+                replaceCt = ReplaceCt+                  { evidenceOfCorrectness  = evCast futureDict co+                  , replacedConstraint     = wanted+                  , replacementConstraints = [wanted']+                  }+            tell [replaceCt]   pure $ combineReplaceCts replaceCts

@@ -0,0 +1,155 @@+{-# LANGUAGE LambdaCase, TupleSections, ViewPatterns #-}+{-# OPTIONS -Wno-name-shadowing #-}+module TypeLevel.Rewrite.Internal.ApplyRules where++import Control.Applicative+import Control.Monad+import Control.Monad.Trans.Class+import Control.Monad.Trans.State+import Data.Foldable (asum, for_)+import Data.Map (Map)+import Data.Maybe (listToMaybe, maybeToList)+import Data.Traversable+import qualified Data.Map as Map++-- GHC API+import Type (TyVar)++-- term-rewriting API+import Data.Rewriting.Rule (Rule(..))+import Data.Rewriting.Substitution (gApply)+import Data.Rewriting.Term (Term(..))+import qualified Data.Rewriting.Substitution.Type as Substitution++import TypeLevel.Rewrite.Internal.TypeEq+import TypeLevel.Rewrite.Internal.TypeNode+import TypeLevel.Rewrite.Internal.TypeRule+import TypeLevel.Rewrite.Internal.TypeSubst+import TypeLevel.Rewrite.Internal.TypeTerm+++type Subst = Map TyVar (Term TypeNode TypeEq)++applyRules+  :: Traversable t+  => TypeSubst+  -> [TypeRule]+  -> t TypeTerm+  -> Maybe (TypeRule,t TypeTerm)+applyRules typeSubst rules inputs+  = annotatedTraverseFirst (multiRewrite typeSubst rules) inputs++multiRewrite+  :: TypeSubst+  -> [TypeRule]+  -> TypeTerm+  -> Maybe (TypeRule, TypeTerm)+multiRewrite typeSubst rules input+  = asum+    [ (rule,) <$> singleRewrite typeSubst rule input+    | rule <- rules+    ]++-- >>> singleRewrite (F x (F x y) ~ F x y) [F a (F a b)]+-- Just [F a b]+singleRewrite+  :: TypeSubst+  -> TypeRule+  -> TypeTerm+  -> Maybe TypeTerm+singleRewrite typeSubst rule input@(Fun inputF inputXS)+    = topLevelRewrite typeSubst rule input+  <|> (Fun inputF <$> traverseFirst (singleRewrite typeSubst rule) inputXS)+singleRewrite typeSubst rule input+  = topLevelRewrite typeSubst rule input+++-- >>> topLevelRewrite (F x (F x y) ~ F x y) (F a (F a b))+-- Just (F a b)+topLevelRewrite+  :: TypeSubst+  -> TypeRule+  -> TypeTerm+  -> Maybe TypeTerm+topLevelRewrite typeSubst (Rule pattern0 pattern') input0 = do+  subst <- execStateT (go pattern0 input0) Map.empty+  gApply (Substitution.fromMap subst) pattern'+  where+    go+      :: Term TypeNode TyVar+      -> TypeTerm+      -> StateT Subst Maybe ()+    go (Var var) input = do+      subst <- get+      case Map.lookup var subst of+        Nothing -> do+          modify (Map.insert var input)+        Just term -> do+          guard (input == term)+    go (Fun patternF patternXS)+       (Fun inputF inputXS)+       = do+      guard (patternF == inputF)+      guard (length patternXS == length inputXS)+      for_ (zip patternXS inputXS) $ \(pattern, input) -> do+        go pattern input+    go pattern (Var var) = do+      let possibleReplacements = fmap snd+                               . filter ((== var) . fst)+                               $ typeSubst+      asum $ fmap (go pattern) possibleReplacements++-- >>> traverseFirst (\x -> if even x then Just (10 + x) else Nothing) [1,3,5]+-- Nothing+-- >>> traverseFirst (\x -> if even x then Just (10 + x) else Nothing) [1,2,4]+-- Just [1,12,4]+traverseFirst+  :: Traversable t+  => (a -> Maybe a)+  -> t a+  -> Maybe (t a)+traverseFirst f = listToMaybe . traverseAll f++annotatedTraverseFirst+  :: Traversable t+  => (a -> Maybe (annotation, a))+  -> t a+  -> Maybe (annotation, t a)+annotatedTraverseFirst f = listToMaybe . annotatedTraverseAll f++-- >>> traverseAll (\x -> if even x then Just (10 + x) else Nothing) [1,3,5]+-- []+-- >>> traverseAll (\x -> if even x then Just (10 + x) else Nothing) [1,2,4]+-- [[1,12,4], [1,2,14]]+traverseAll+  :: Traversable t+  => (a -> Maybe a)+  -> t a+  -> [t a]+traverseAll f+  = fmap snd+  . annotatedTraverseAll (fmap ((),) . f)++annotatedTraverseAll+  :: Traversable t+  => (a -> Maybe (annotation, a))+  -> t a+  -> [(annotation, t a)]+annotatedTraverseAll f ta = flip evalStateT Nothing $ do+  ta' <- for ta $ \a -> do+    get >>= \case+      Just _ -> do+        -- already picked one+        pure a+      Nothing -> do+        pickIt <- lift [True,False]+        if pickIt+          then do+            (annotation, a) <- lift $ maybeToList $ f a+            put (Just annotation)+            pure a+          else do+            pure a+  maybeAnnotation <- get+  annotation <- lift $ maybeToList maybeAnnotation+  pure (annotation, ta')

@@ -0,0 +1,59 @@+{-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable, LambdaCase, RecordWildCards, ViewPatterns #-}+module TypeLevel.Rewrite.Internal.DecomposedConstraint where++import Control.Applicative++-- GHC API+import GHC (Class, Type)+import Constraint (Ct, ctEvPred, ctEvidence)+import Predicate (EqRel(NomEq), Pred(ClassPred, EqPred), classifyPredType, mkClassPred, mkPrimEqPred)+++data DecomposedConstraint a+  = EqualityConstraint a a        -- lhs ~ rhs+  | InstanceConstraint Class [a]  -- C a b c+  deriving (Functor, Foldable, Traversable)++asEqualityConstraint+  :: Ct+  -> Maybe (Type, Type)+asEqualityConstraint ct = do+  let predTree+        = classifyPredType+        $ ctEvPred+        $ ctEvidence+        $ ct+  case predTree of+    EqPred NomEq lhs rhs+      -> pure (lhs, rhs)+    _ -> Nothing++asInstanceConstraint+  :: Ct+  -> Maybe (Class, [Type])+asInstanceConstraint ct = do+  let predTree+        = classifyPredType+        $ ctEvPred+        $ ctEvidence+        $ ct+  case predTree of+    ClassPred typeclass args+      -> pure (typeclass, args)+    _ -> Nothing++asDecomposedConstraint+  :: Ct+  -> Maybe (DecomposedConstraint Type)+asDecomposedConstraint ct+    = (uncurry EqualityConstraint <$> asEqualityConstraint ct)+  <|> (uncurry InstanceConstraint <$> asInstanceConstraint ct)++fromDecomposeConstraint+  :: DecomposedConstraint Type+  -> Type+fromDecomposeConstraint = \case+  EqualityConstraint t1 t2+    -> mkPrimEqPred t1 t2+  InstanceConstraint cls args+    -> mkClassPred cls args

@@ -3,20 +3,18 @@  import Control.Arrow ((***), first) import Data.Tuple (swap)-import qualified GHC.TcPluginM.Extra as TcPluginM  -- GHC API-import DataCon (DataCon, promoteDataCon)-import DynFlags (getDynFlags) import Finder (cannotFindModule)+import GHC (DataCon, TyCon, dataConTyCon) import Module (Module, ModuleName, mkModuleName) import OccName (mkDataOcc, mkTcOcc) import Panic (panicDoc) import TcPluginM-  ( FindResult(Found), TcPluginM, findImportedModule, tcLookupDataCon, tcLookupTyCon+  ( FindResult(Found), TcPluginM, findImportedModule, lookupOrig, tcLookupDataCon, tcLookupTyCon   , unsafeTcPluginTcM   )-import TyCon (TyCon)+import TcSMonad (getDynFlags)   lookupModule@@ -50,7 +48,7 @@   -> TcPluginM TyCon lookupTyCon moduleNameStr tyConNameStr = do   module_ <- lookupModule moduleNameStr-  tyConName <- TcPluginM.lookupName module_ (mkTcOcc tyConNameStr)+  tyConName <- lookupOrig module_ (mkTcOcc tyConNameStr)   tyCon <- tcLookupTyCon tyConName   pure tyCon @@ -60,7 +58,7 @@   -> TcPluginM DataCon lookupDataCon moduleNameStr dataConNameStr = do   module_ <- lookupModule moduleNameStr-  dataConName <- TcPluginM.lookupName module_ (mkDataOcc dataConNameStr)+  dataConName <- lookupOrig module_ (mkDataOcc dataConNameStr)   dataCon <- tcLookupDataCon dataConName   pure dataCon @@ -87,7 +85,7 @@   :: String   -> TcPluginM TyCon lookupFQN ('\'' : (splitLastDot -> Just (moduleNameStr, dataConNameStr)))-  = promoteDataCon <$> lookupDataCon moduleNameStr dataConNameStr+  = dataConTyCon <$> lookupDataCon moduleNameStr dataConNameStr lookupFQN (splitLastDot -> Just (moduleNameStr, tyConNameStr))   = lookupTyCon moduleNameStr tyConNameStr lookupFQN fqn

@@ -14,7 +14,9 @@ import Data.Rewriting.Term (Term(Fun, Var))  import TypeLevel.Rewrite.Internal.TypeEq+import TypeLevel.Rewrite.Internal.TypeNode import TypeLevel.Rewrite.Internal.TypeRule+import TypeLevel.Rewrite.Internal.TypeSubst import TypeLevel.Rewrite.Internal.TypeTemplate import TypeLevel.Rewrite.Internal.TypeTerm @@ -31,6 +33,18 @@     ++ pprA a     ++ ")" +pprPair+  :: (a -> String)+  -> (b -> String)+  -> (a, b)+  -> String+pprPair pprA pprB (a, b)+  = "("+ ++ pprA a+ ++ ", "+ ++ pprB b+ ++ ")"+ pprList   :: (a -> String)   -> [a]@@ -103,20 +117,37 @@  ++ "}"  +pprTypeNode+  :: TypeNode -> String+pprTypeNode = \case+  TyCon tyCon+    -> "TyCon ("+    ++ pprTyCon tyCon+    ++ ")"+  TyLit tyLit+    -> "TyLit ("+    ++ pprTypeEq tyLit+    ++ ")"++pprTypeSubst+  :: TypeSubst -> String+pprTypeSubst+  = pprList $ pprPair pprTypeEq pprTypeTerm+ pprTypeTemplate   :: TypeTemplate -> String pprTypeTemplate-  = pprTerm pprTyCon pprTyVar+  = pprTerm pprTypeNode pprTyVar  pprTypeTerm   :: TypeTerm -> String pprTypeTerm-  = pprTerm pprTyCon pprTypeEq+  = pprTerm pprTypeNode pprTypeEq  pprTypeRule   :: TypeRule -> String pprTypeRule-  = pprRule pprTyCon pprTyVar+  = pprRule pprTypeNode pprTyVar  pprTypeReduct   :: Reduct TyCon TypeEq TyVar -> String

@@ -2,7 +2,7 @@  import Data.Function -import Type (Type, eqType)+import GhcPlugins (Type, eqType)   -- | A newtype around 'Type' which has an 'Eq' instance.

@@ -0,0 +1,35 @@+{-# LANGUAGE ViewPatterns #-}+module TypeLevel.Rewrite.Internal.TypeNode where++-- GHC API+import TyCon (TyCon)+import Type (Type, isNumLitTy, isStrLitTy, mkTyConApp, splitTyConApp_maybe)++import TypeLevel.Rewrite.Internal.TypeEq+++-- A 'Type' is a tree whose internal nodes are 'TypeNode's and whose leaves are+-- type variables.+data TypeNode+  = TyCon TyCon+  | TyLit TypeEq+  deriving Eq++toTypeNodeApp_maybe+  :: Type+  -> Maybe (TypeNode, [Type])+toTypeNodeApp_maybe (splitTyConApp_maybe -> Just (tyCon, args))+  = pure (TyCon tyCon, args)+toTypeNodeApp_maybe tyLit@(isNumLitTy -> Just _)+  = pure (TyLit (TypeEq tyLit), [])+toTypeNodeApp_maybe tyLit@(isStrLitTy -> Just _)+  = pure (TyLit (TypeEq tyLit), [])+toTypeNodeApp_maybe _+  = Nothing++fromTypeNode+  :: TypeNode+  -> [Type]+  -> Type+fromTypeNode (TyCon tyCon) args = mkTyConApp tyCon args+fromTypeNode (TyLit (TypeEq tyLit)) _ = tyLit

@@ -1,43 +1,50 @@-{-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE LambdaCase, ViewPatterns #-}+{-# OPTIONS -Wno-name-shadowing #-} module TypeLevel.Rewrite.Internal.TypeRule where  -- GHC API import Name (getOccString)-import TyCon (TyCon)-import Type (TyVar, Type)+import Predicate (mkPrimEqPred)+import Type (TyVar, Type, mkTyVarTy)  -- term-rewriting API import Data.Rewriting.Rule (Rule(..))-import Data.Rewriting.Rules (Reduct(result), fullRewrite)-import Data.Rewriting.Term (Term(Fun))+import Data.Rewriting.Term (Term(..)) +import TypeLevel.Rewrite.Internal.TypeNode import TypeLevel.Rewrite.Internal.TypeTemplate-import TypeLevel.Rewrite.Internal.TypeTerm  -type TypeRule = Rule TyCon TyVar+type TypeRule = Rule TypeNode TyVar  toTypeRule_maybe   :: Type   -> Maybe TypeRule-toTypeRule_maybe (toTypeTemplate_maybe -> Just (Fun (getOccString -> "~") [_type, lhs_, rhs_]))+toTypeRule_maybe (toTypeTemplate_maybe -> Just (Fun (TyCon (getOccString -> "~")) [_type, lhs_, rhs_]))   = Just (Rule lhs_ rhs_) toTypeRule_maybe _   = Nothing -applyRules-  :: [TypeRule]-  -> TypeTerm-  -> TypeTerm-applyRules rules-  = go (length rules * 100)-  where-    go :: Int -> TypeTerm -> TypeTerm-    go 0 _-      = error "the rewrite rules form a cycle"-    go fuel typeTerm-      = case fullRewrite rules typeTerm of-          []-            -> typeTerm-          reducts-            -> go (fuel - 1) . result . last $ reducts+fromTyVar+  :: TyVar+  -> Type+fromTyVar+  = mkTyVarTy++fromTerm+  :: (f -> [Type] -> Type)+  -> (v -> Type)+  -> Term f v+  -> Type+fromTerm fromF fromV = \case+  Var v+    -> fromV v+  Fun f args+    -> fromF f (fmap (fromTerm fromF fromV) args)++fromTypeRule+  :: TypeRule+  -> Type+fromTypeRule (Rule lhs rhs)+  = mkPrimEqPred (fromTerm fromTypeNode fromTyVar lhs)+                 (fromTerm fromTypeNode fromTyVar rhs)

@@ -0,0 +1,7 @@+module TypeLevel.Rewrite.Internal.TypeSubst where++import TypeLevel.Rewrite.Internal.TypeEq+import TypeLevel.Rewrite.Internal.TypeTerm+++type TypeSubst = [(TypeEq, TypeTerm)]

@@ -2,21 +2,22 @@ module TypeLevel.Rewrite.Internal.TypeTemplate where  -- GHC API-import TyCon (TyCon)-import Type (TyVar, Type, getTyVar_maybe, splitTyConApp_maybe)+import Type (TyVar, Type, getTyVar_maybe)  -- term-rewriting API import Data.Rewriting.Term (Term(Fun, Var)) +import TypeLevel.Rewrite.Internal.TypeNode -type TypeTemplate = Term TyCon TyVar +type TypeTemplate = Term TypeNode TyVar+ toTypeTemplate_maybe   :: Type   -> Maybe TypeTemplate toTypeTemplate_maybe (getTyVar_maybe -> Just tyVar)   = Just . Var $ tyVar-toTypeTemplate_maybe (splitTyConApp_maybe -> Just (tyCon, args))-  = Fun tyCon <$> traverse toTypeTemplate_maybe args+toTypeTemplate_maybe (toTypeNodeApp_maybe -> Just (tyNode, args))+  = Fun tyNode <$> traverse toTypeTemplate_maybe args toTypeTemplate_maybe _   = Nothing

@@ -2,21 +2,21 @@ module TypeLevel.Rewrite.Internal.TypeTerm where  -- GHC API-import TyCon (TyCon)-import Type (Type, mkTyConApp, splitTyConApp_maybe)+import Type (Type, mkTyConApp)  -- term-rewriting API import Data.Rewriting.Term (Term(Fun, Var))  import TypeLevel.Rewrite.Internal.TypeEq+import TypeLevel.Rewrite.Internal.TypeNode  -type TypeTerm = Term TyCon TypeEq+type TypeTerm = Term TypeNode TypeEq  toTypeTerm   :: Type -> TypeTerm-toTypeTerm (splitTyConApp_maybe -> Just (tyCon, args))-  = Fun tyCon (fmap toTypeTerm args)+toTypeTerm (toTypeNodeApp_maybe -> Just (tyNode, args))+  = Fun tyNode (fmap toTypeTerm args) toTypeTerm tp   = Var (TypeEq tp) @@ -25,5 +25,9 @@ fromTypeTerm = \case   Var x     -> unTypeEq x-  Fun tyCon args+  Fun (TyCon tyCon) args     -> mkTyConApp tyCon (fmap fromTypeTerm args)+  Fun (TyLit (TypeEq tyLit)) []+    -> tyLit+  Fun (TyLit _) _+    -> error "impossible: TyLit doesn't have any arguments"

@@ -1,5 +1,6 @@ {-# LANGUAGE DataKinds, RankNTypes, TypeFamilies, TypeOperators #-}-{-# OPTIONS_GHC -fplugin TypeLevel.Rewrite+{-# OPTIONS_GHC -fconstraint-solver-iterations=10+                -fplugin TypeLevel.Rewrite                 -fplugin-opt=TypeLevel.Rewrite:Data.Vinyl.TypeLevel.RewriteRules.RightIdentity                 -fplugin-opt=TypeLevel.Rewrite:Data.Vinyl.TypeLevel.RewriteRules.RightAssociative #-} module Data.Vinyl.TypeLevel.Test where

@@ -0,0 +1,12 @@+{-# LANGUAGE ConstraintKinds, DataKinds, TypeFamilies, TypeOperators #-}+module GHC.TypeLits.RewriteRules where++import GHC.TypeLits+++type NatRule n+  = (1 + n) ~ (n + 1)++type SymbolRule s1 s2+  = ((s1 `AppendSymbol` "foo") `AppendSymbol` s2)+  ~ (s1 `AppendSymbol` ("foo" `AppendSymbol` s2))

@@ -0,0 +1,22 @@+{-# LANGUAGE DataKinds, RankNTypes, TypeFamilies, TypeOperators #-}+{-# OPTIONS_GHC -fplugin TypeLevel.Rewrite+                -fplugin-opt=TypeLevel.Rewrite:GHC.TypeLits.RewriteRules.NatRule+                -fplugin-opt=TypeLevel.Rewrite:GHC.TypeLits.RewriteRules.SymbolRule #-}+module GHC.TypeLits.Test where++import GHC.TypeLits+import GHC.TypeLits.RewriteRules ()+++ex1 :: ((1 + n) ~ (n + 1) => r)+    -> proxy n+    -> r+ex1 r _ = r++ex2 :: ( ((s1 `AppendSymbol` "foo") `AppendSymbol` s2)+       ~ (s1 `AppendSymbol` ("foo" `AppendSymbol` s2))+      => r+       )+    -> proxy s+    -> r+ex2 r _ = r

@@ -0,0 +1,7 @@+{-# LANGUAGE ConstraintKinds, TypeFamilies #-}+module InstanceConstraints.Laws where++type family F a b+type family G a b++type FLaw a b = F a (F a b) ~ F a b

@@ -0,0 +1,51 @@+{-# LANGUAGE AllowAmbiguousTypes, FlexibleContexts, ScopedTypeVariables, TypeApplications, TypeFamilies #-}+{-# OPTIONS_GHC -fplugin TypeLevel.Rewrite+                -fplugin-opt=TypeLevel.Rewrite:InstanceConstraints.Laws.FLaw #-}+module InstanceConstraints.Test where++import InstanceConstraints.Laws+++class Foo a where+  foo :: ()++f1 :: forall a b. Foo (F a b) => ()+f1 = foo @(F a (F a b))++f2 :: forall a b. Foo [F a b] => ()+f2 = foo @[F a (F a b)]++f3 :: forall a b x y+    . ( F a b ~ y+      , y ~ x+      , Foo (F a b)+      )+   => ()+f3 = foo @(F a x)++f4 :: forall a b x y+    . ( F a b ~ y+      , y ~ x+      , x ~ y+      , Foo (F a b)+      )+   => ()+f4 = foo @(F a x)++f5 :: forall a b x y+    . ( F a b ~ x+      , y ~ x+      , x ~ y+      , Foo (F a b)+      )+   => ()+f5 = foo @(F a x)++f6 :: forall a b x y+    . ( F a b ~ G x y+      , y ~ x+      , x ~ y+      , Foo (F a b)+      )+   => ()+f6 = foo @(F a (G x y))

@@ -1,5 +1,6 @@ {-# LANGUAGE DataKinds, RankNTypes, TypeFamilies, TypeOperators #-}-{-# OPTIONS_GHC -fplugin TypeLevel.Rewrite+{-# OPTIONS_GHC -fconstraint-solver-iterations=10+                -fplugin TypeLevel.Rewrite                 -fplugin-opt=TypeLevel.Rewrite:MonoKinds.Append.RightIdentity                 -fplugin-opt=TypeLevel.Rewrite:MonoKinds.Append.RightAssociative #-} module MonoKinds.Test where

@@ -1,5 +1,6 @@ {-# LANGUAGE DataKinds, RankNTypes, TypeFamilies, TypeOperators #-}-{-# OPTIONS_GHC -fplugin TypeLevel.Rewrite+{-# OPTIONS_GHC -fconstraint-solver-iterations=10+                -fplugin TypeLevel.Rewrite                 -fplugin-opt=TypeLevel.Rewrite:SamePackage.Append.RightIdentity                 -fplugin-opt=TypeLevel.Rewrite:SamePackage.Append.RightAssociative #-} module SamePackage.Test where

@@ -1,6 +1,8 @@-import Data.Vinyl.TypeLevel.Test-import SamePackage.Test-import TypeLevel.Append.Test+import Data.Vinyl.TypeLevel.Test ()+import GHC.TypeLits.Test ()+import InstanceConstraints.Test ()+import SamePackage.Test ()+import TypeLevel.Append.Test ()   main :: IO ()

@@ -1,5 +1,6 @@-{-# LANGUAGE DataKinds, RankNTypes, TypeFamilies, TypeOperators #-}-{-# OPTIONS_GHC -fplugin TypeLevel.Rewrite+{-# LANGUAGE DataKinds, RankNTypes, ScopedTypeVariables, TypeFamilies, TypeOperators #-}+{-# OPTIONS_GHC -fconstraint-solver-iterations=10+                -fplugin TypeLevel.Rewrite                 -fplugin-opt=TypeLevel.Rewrite:TypeLevel.Append.RightIdentity                 -fplugin-opt=TypeLevel.Rewrite:TypeLevel.Append.RightAssociative #-} module TypeLevel.Append.Test where@@ -74,3 +75,30 @@      -> proxy (as ++ (bs ++ cs))      -> proxy ((as ++ bs) ++ cs) ex2e _ _ _ r = r++ex2f :: forall proxy xs as bs cs r. xs ~ ((as ++ bs) ++ cs)+     => (xs ~ (as ++ (bs ++ cs)) => r)+     -> proxy as+     -> proxy bs+     -> proxy cs+     -> r+ex2f r _ _ _ = r++ex2g :: (as ++ (bs ++ cs)) ~ cs+     => (((as ++ bs) ++ cs) ~ cs => r)+     -> proxy as+     -> proxy bs+     -> proxy cs+     -> r+ex2g r _ _ _ = r++ex2h :: forall proxy xs ys as bs cs r+      . ( ys ~ xs+        , xs ~ ((as ++ bs) ++ cs)+        )+     => (xs ~ (as ++ (bs ++ cs)) => r)+     -> proxy as+     -> proxy bs+     -> proxy cs+     -> r+ex2h r _ _ _ = r

@@ -1,13 +1,13 @@ cabal-version: 1.12 --- This file has been generated from package.yaml by hpack version 0.31.2.+-- This file has been generated from package.yaml by hpack version 0.33.0. -- -- see: https://github.com/sol/hpack ----- hash: a0aa0b58de9c55fa77a152d9a3aa0be871bfa33439ebe19185cb1283b97d6350+-- hash: 2673197ba6a9e92128e851017519e221b95a23ca70b1f7b84158feae74eba11b  name:           typelevel-rewrite-rules-version:        0.1+version:        1.0 synopsis:       Solve type equalities using custom type-level rewrite rules description:    A typechecker plugin which allows the user to specify a set of domain-specific rewrite rules. These get applied whenever the compiler is unable to solve a type equality constraint, in the hope that the rewritten equality constraint will be easier to solve. category:       Type System@@ -29,11 +29,15 @@   exposed-modules:       TypeLevel.Append       TypeLevel.Rewrite+      TypeLevel.Rewrite.Internal.ApplyRules+      TypeLevel.Rewrite.Internal.DecomposedConstraint       TypeLevel.Rewrite.Internal.Lookup       TypeLevel.Rewrite.Internal.PrettyPrint       TypeLevel.Rewrite.Internal.Term       TypeLevel.Rewrite.Internal.TypeEq+      TypeLevel.Rewrite.Internal.TypeNode       TypeLevel.Rewrite.Internal.TypeRule+      TypeLevel.Rewrite.Internal.TypeSubst       TypeLevel.Rewrite.Internal.TypeTemplate       TypeLevel.Rewrite.Internal.TypeTerm   other-modules:@@ -42,12 +46,12 @@       src   ghc-options: -W -Wall   build-depends:-      base >=4.12 && <6-    , ghc >=8.6.3+      base >=4.12 && <5+    , containers >=0.6.2.1+    , ghc >=8.10.2 && <9.0     , ghc-prim >=0.5.3-    , ghc-tcplugins-extra >=0.3     , term-rewriting >=0.3.0.1-    , transformers >=0.5.5.0+    , transformers >=0.5.6.2   default-language: Haskell2010  test-suite should-compile@@ -56,6 +60,10 @@   other-modules:       Data.Vinyl.TypeLevel.RewriteRules       Data.Vinyl.TypeLevel.Test+      GHC.TypeLits.RewriteRules+      GHC.TypeLits.Test+      InstanceConstraints.Laws+      InstanceConstraints.Test       MonoKinds.Append       MonoKinds.Test       SamePackage.Append@@ -64,9 +72,10 @@       Paths_typelevel_rewrite_rules   hs-source-dirs:       test/should-compile+  ghc-options: -W -Wall   build-depends:-      base >=4.12 && <6+      base >=4.12 && <5     , ghc-prim >=0.5.3     , typelevel-rewrite-rules-    , vinyl+    , vinyl >=0.13.0   default-language: Haskell2010