packages feed

typelevel-rewrite-rules (empty) → 0.1

raw patch · 20 files changed

+1118/−0 lines, 20 filesdep +basedep +ghcdep +ghc-prim

Dependencies added: base, ghc, ghc-prim, ghc-tcplugins-extra, term-rewriting, transformers, typelevel-rewrite-rules, vinyl

Files

+ CHANGELOG.md view
@@ -0,0 +1,2 @@+# 0.1+* initial release
+ README.md view
@@ -0,0 +1,167 @@+# 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)++Solve type equalities using custom type-level rewrite rules like `(n + 'Z) ~ n` and `((m + n) + o) ~ (m + (n + o))`.+++## The problem++Type equalities involving type families sometimes get stuck:++```haskell+{-# LANGUAGE DataKinds, TypeFamilies, TypeOperators #-}+module My.Module where++import Prelude hiding ((++))++import Data.Type.Nat (Nat(Z, S), type (+))+import Data.Vec.Lazy (Vec, (++))++-- Couldn't match type ‘(((m + 'Z) + n) + 'Z) + o’+--                with ‘(m + n) + o’+simplify+  :: 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+```++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.++```haskell+-- ok+simplifyConcrete+  :: Vec ('S 'Z) a+  -> Vec 'Z a+  -> Vec ('S ('S 'Z)) a+  -> Vec 'Z a+  -> Vec ('S ('S ('S 'Z))) a+  -> Vec ('S 'Z + 'S ('S 'Z) + 'S ('S ('S 'Z))) a+simplifyConcrete xsM empty1 xsN empty2 xsO+  = (((xsM ++ empty1) ++ xsN) ++ empty2) ++ xsO+```++The reason this particular type family gets stuck is because it pattern-matches on its left argument. Pattern-matching proceeds as designed when that argument is a known type-level value like `'S 'Z`, but when that argument is the type variable `m`, evaluation cannot proceed until we learn more about `m`.++```haskell+module Data.Type.Nat where++type family (+) (m :: Nat) (n :: Nat) :: Nat where+  'Z   + n = n+  'S m + n = 'S (m + n)+```+++## The solution++First, define some rewrite rules. Each rewrite rule has a name, some variables, a left-hand side, and a right-hand side. The left-hand side gets rewritten to the right-hand side. Syntactically, a rewrite rule is defined via a constraint type synonym expanding to a type equality between the two sides.++For technical reasons, these must be defined in a different module than the one in which the stuck constraints appear, but they could be defined in the same module as the one which defines the type family.++```haskell+{-# LANGUAGE ConstraintKinds, DataKinds, TypeFamilies, TypeOperators #-}+module My.RewriteRules where++import Data.Type.Nat (Nat(Z, S), type (+))++type RightIdentity n+  = (n + 'Z) ~ n+type RightAssociative m n o+  = ((m + n) + o) ~ (m + (n + o))+```++Next, coming back to our original module, point the `TypeLevel.Rewrite` plugin to those rewrite rules. The type error disappears!++```haskell+{-# LANGUAGE DataKinds, TypeFamilies, TypeOperators #-}+{-# OPTIONS_GHC -fplugin TypeLevel.Rewrite+                -fplugin-opt=TypeLevel.Rewrite:My.RewriteRules.RightIdentity+                -fplugin-opt=TypeLevel.Rewrite:My.RewriteRules.RightAssociative #-}+module My.Module where++import Prelude hiding ((++))++import Data.Type.Nat (Nat(Z, S), type (+))+import Data.Vec.Lazy (Vec, (++))++-- the module which contains the rewrite rules must be imported+import My.RewriteRules ()++-- now ok!+simplify+  :: 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+```++For this particular type equality, it just so happens that either of the two rewrite rules would have been sufficient on its own. With only `RightIdentity`, the two `(+ 'Z)`s get removed from `(((m + 'Z) + n) + 'Z) + o`, leaving `(m + n) + o`. With only `RightAssociative`, `(((m + 'Z) + n) + 'Z) + o` gets rewritten to `m + ('Z + (n + ('Z + o)))`, and now `(+)` can pattern-match on the `'Z`s and evaluate to `m + (n + o)`. Meanwhile, the right-hand side `(m + n) + o` also gets rewritten to `m + (n + o)`. With both `RightIdentity` and `RightAssociative`, both sides get rewritten to `m + (n + o)`.+++## Dangers++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:++```haskell+{-# LANGUAGE DataKinds, RankNTypes, TypeFamilies, TypeApplications, TypeOperators #-}+{-# OPTIONS_GHC -fplugin TypeLevel.Rewrite+                -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 My.RewriteRules ()++withNonsense+  :: proxy as+  -> ((as ++ '[]) ~ '[] => r)+  -> r+withNonsense _ r = r++-- |+-- >>> recFromNowhere (Proxy @'[])+-- {}+-- >>> recFromNowhere (Proxy @'[Int, String])+-- error: Impossible case alternative+recFromNowhere+  :: proxy as+  -> Rec Identity (as ++ '[])+recFromNowhere proxy = withNonsense proxy RNil+```++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.+++## Troubleshooting++Most error messages should be self-explanatory, but there are a few circumstances in which the ghc API produces a confusing error message without giving me the opportunity to replace it with a better one. So if you encounter one of those confusing error messages, hopefully google will lead you to this page explaining what they mean.++### `GHC internal error: ‘My.Module.MyRule’ is not in scope during type checking, but it passed the renamer tcl_env of environment: []`++This means you are in `My.Module` and you are trying to use a rewrite rule which is also defined in `My.Module`. This is unfortunately not supported.++Solution: move your rewrite rule to another module and import that module from `My.Module`.++### `attempting to use module ‘My.RewriteRules’ which is not loaded`++This one is annoying because whether it happens or not depends on the order in which ghc chooses to compile your modules. If ghc happens to compile the module which uses your rewrite rules before the module which defines your rewrite rules, you'll get that error message.++Solution: add an `import My.RewriteRules ()` statement to force ghc to compile `My.RewriteRules` first.++### `Can't find interface-file declaration for type constructor or class My.RewriteRules.MyRule`++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?++
+ src/TypeLevel/Append.hs view
@@ -0,0 +1,11 @@+{-# LANGUAGE ConstraintKinds, DataKinds, PolyKinds, TypeFamilies, TypeOperators #-}+module TypeLevel.Append where++type family (++) as bs where+  '[]       ++ bs = bs+  (a ': as) ++ bs = a ': (as ++ bs)++type RightIdentity as+  = (as ++ '[]) ~ as+type RightAssociative as bs cs+  = ((as ++ bs) ++ cs) ~ (as ++ (bs ++ cs))
+ src/TypeLevel/Rewrite.hs view
@@ -0,0 +1,173 @@+{-# LANGUAGE RecordWildCards, ViewPatterns #-}+module TypeLevel.Rewrite (plugin) where++import Control.Monad+import Control.Monad.Trans.Class+import Control.Monad.Trans.Writer+import Data.Foldable+import Data.Traversable+import GHC.TcPluginM.Extra (evByFiat)++-- GHC API+import Plugins (Plugin(pluginRecompile, tcPlugin), CommandLineOption, defaultPlugin, purePlugin)+import TcEvidence (EvTerm)+import TcPluginM (TcPluginM, newCoercionHole)+import TcRnTypes+import TcType (TcPredType)+import TyCon (synTyConDefn_maybe)+import Type (EqRel(NomEq), PredTree(EqPred), Type, classifyPredType, mkPrimEqPred)++import TypeLevel.Rewrite.Internal.Lookup+import TypeLevel.Rewrite.Internal.PrettyPrint+import TypeLevel.Rewrite.Internal.TypeRule+import TypeLevel.Rewrite.Internal.TypeTerm++-- printf-debugging:+--import TcPluginM (tcPluginIO)+--import Outputable+----tcPluginIO $ print ("foo", showSDocUnsafe $ ppr foo)+++data ReplaceCt = ReplaceCt+  { evidenceOfCorrectness  :: EvTerm+  , replacedConstraint     :: Ct+  , replacementConstraints :: [Ct]+  }++combineReplaceCts+  :: [ReplaceCt]+  -> TcPluginResult+combineReplaceCts replaceCts+  = TcPluginOk (fmap solvedConstraint replaceCts)+               (foldMap replacementConstraints replaceCts)+  where+    solvedConstraint :: ReplaceCt -> (EvTerm, Ct)+    solvedConstraint = (,) <$> evidenceOfCorrectness <*> replacedConstraint+++usage+  :: String  -- ^ expected+  -> String  -- ^ actual+  -> TcPluginM a+usage expected actual+  = error $ "usage:\n"+         ++ "  {-# OPTIONS_GHC -fplugin TypeLevel.Rewrite\n"+         ++ "                  -fplugin-opt=TypeLevel.Rewrite:TypeLevel.Append.RightIdentity\n"+         ++ "                  -fplugin-opt=TypeLevel.Rewrite:TypeLevel.Append.RightAssociative #-}\n"+         ++ "Where 'TypeLevel.Append' is a module containing a type synonym named 'RightIdentity':\n"+         ++ "  type RightIdentity as = (as ++ '[]) ~ as\n"+         ++ "Type expressions which match the left of the '~' will get rewritten to the type\n"+         ++ "expression on the right of the '~'. Be careful not to introduce cycles!\n"+         ++ "\n"+         ++ "expected:\n"+         ++ "  " ++ expected ++ "\n"+         ++ "got:\n"+         ++ "  " ++ actual++lookupTypeRules+  :: [CommandLineOption]+  -> TcPluginM [TypeRule]+lookupTypeRules [] = do+  usage (show ["TypeLevel.Append.RightIdentity", "TypeLevel.Append.RightAssociative"])+        "[]"+lookupTypeRules fullyQualifiedTypeSynonyms = do+  -- ["TypeLevel.Append.RightIdentity", "TypeLevel.Append.RightAssociative"]+  for fullyQualifiedTypeSynonyms $ \fullyQualifiedTypeSynonym -> do+    -- "TypeLevel.Append.RightIdentity"+    case splitLastDot fullyQualifiedTypeSynonym of+      Nothing -> do+        usage (show "TypeLevel.Append.RightIdentity")+              (show fullyQualifiedTypeSynonym)+      Just (moduleNameStr, tyConNameStr) -> do+        -- ("TypeLevel.Append", "RightIdentity")+        tyCon <- lookupTyCon moduleNameStr tyConNameStr  -- FIXME: if tyConNameStr is not found in+                                                         -- the module, the error message is poor+        case synTyConDefn_maybe tyCon of+          Nothing -> do+            usage ("type " ++ pprTyCon tyCon ++ " ... = ...")+                  (pprTyCon tyCon ++ " is not a type synonym")+          Just (_tyVars, definition) -> do+            -- ([TyVar "as"], Type "(as ++ '[]) ~ as")+            case toTypeRule_maybe definition of+              Nothing -> do+                usage "... ~ ..."+                      (pprType definition)+              Just typeRule -> do+                -- Rule (TypeTree "(as ++ '[])")+                --      (TypeTree "as")+                pure typeRule+++plugin+  :: Plugin+plugin = defaultPlugin+  { tcPlugin = \args -> Just $ TcPlugin+    { tcPluginInit  = lookupTypeRules args+    , tcPluginSolve = solve+    , tcPluginStop  = \_ -> pure ()+    }+  , pluginRecompile = purePlugin+  }+++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++toEqualityConstraint+  :: Type -> Type -> CtLoc -> TcPluginM Ct+toEqualityConstraint lhs rhs loc = do+  let tcPredType :: TcPredType+      tcPredType = mkPrimEqPred lhs rhs++  hole <- newCoercionHole tcPredType++  pure $ mkNonCanonical+       $ CtWanted tcPredType (HoleDest hole) WDeriv loc+++solve+  :: [TypeRule]+  -> [Ct]  -- ^ Given constraints+  -> [Ct]  -- ^ Derived constraints+  -> [Ct]  -- ^ Wanted constraints+  -> 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 => ...++        let lhsTypeTerm = toTypeTerm lhs+        let rhsTypeTerm = toTypeTerm rhs+        let lhsTypeTerm' = applyRules rules lhsTypeTerm+        let rhsTypeTerm' = applyRules rules rhsTypeTerm++        unless (lhsTypeTerm' == lhsTypeTerm && rhsTypeTerm' == rhsTypeTerm) $ do+          -- lhs' ~ rhs' => ...+          let lhs' = fromTypeTerm lhsTypeTerm'+          let rhs' = fromTypeTerm rhsTypeTerm'++          ct' <- lift $ toEqualityConstraint lhs' rhs' (ctLoc ct)++          let replaceCt :: ReplaceCt+              replaceCt = ReplaceCt+                { evidenceOfCorrectness  = evByFiat "TypeLevel.Rewrite" lhs' rhs'+                , replacedConstraint     = ct+                , replacementConstraints = [ct']+                }+          tell [replaceCt]+  pure $ combineReplaceCts replaceCts
+ src/TypeLevel/Rewrite/Internal/Lookup.hs view
@@ -0,0 +1,95 @@+{-# LANGUAGE LambdaCase, ViewPatterns #-}+module TypeLevel.Rewrite.Internal.Lookup where++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 Module (Module, ModuleName, mkModuleName)+import OccName (mkDataOcc, mkTcOcc)+import Panic (panicDoc)+import TcPluginM+  ( FindResult(Found), TcPluginM, findImportedModule, tcLookupDataCon, tcLookupTyCon+  , unsafeTcPluginTcM+  )+import TyCon (TyCon)+++lookupModule+  :: String  -- ^ module name+  -> TcPluginM Module+lookupModule moduleNameStr = do+  let moduleName :: ModuleName+      moduleName = mkModuleName moduleNameStr+  findImportedModule moduleName Nothing >>= \case+    Found _ module_ -> do+      pure module_+    findResult -> do+      dynFlags <- unsafeTcPluginTcM getDynFlags+      panicDoc ("TypeLevel.Lookup.lookupModule " ++ show moduleNameStr)+             $ cannotFindModule dynFlags moduleName findResult++-- 'TcPluginM.lookupM' unfortunately fails with a very unhelpful error message+-- when we look up a name which doesn't exist:+--+--   Can't find interface-file declaration for type constructor or class ModuleName.TypeName+--   Probable cause: bug in .hi-boot file, or inconsistent .hi file+--   Use -ddump-if-trace to get an idea of which file caused the error+--+-- But the true cause isn't a corrupted file, it's simply that the requested+-- name is not in the given module. I don't know how to fix the error message+-- (I can't use 'try' nor 'tryM' because we're in the wrong monad)++lookupTyCon+  :: String  -- ^ module name+  -> String  -- ^ type constructor/family name+  -> TcPluginM TyCon+lookupTyCon moduleNameStr tyConNameStr = do+  module_ <- lookupModule moduleNameStr+  tyConName <- TcPluginM.lookupName module_ (mkTcOcc tyConNameStr)+  tyCon <- tcLookupTyCon tyConName+  pure tyCon++lookupDataCon+  :: String  -- ^ module name+  -> String  -- ^ data constructor name+  -> TcPluginM DataCon+lookupDataCon moduleNameStr dataConNameStr = do+  module_ <- lookupModule moduleNameStr+  dataConName <- TcPluginM.lookupName module_ (mkDataOcc dataConNameStr)+  dataCon <- tcLookupDataCon dataConName+  pure dataCon+++splitFirstDot+  :: String -> Maybe (String, String)+splitFirstDot ('.' : rhs)+  = Just ("", rhs)+splitFirstDot (x : xs)+  = first (x:) <$> splitFirstDot xs+splitFirstDot _+  = Nothing++splitLastDot+  :: String -> Maybe (String, String)+splitLastDot+  = fmap swap+  . fmap (reverse *** reverse)+  . splitFirstDot+  . reverse++-- lookup a Fully-Qualified Name, such as "'GHC.Types.[]" or "TypeLevel.Append.++"+lookupFQN+  :: String+  -> TcPluginM TyCon+lookupFQN ('\'' : (splitLastDot -> Just (moduleNameStr, dataConNameStr)))+  = promoteDataCon <$> lookupDataCon moduleNameStr dataConNameStr+lookupFQN (splitLastDot -> Just (moduleNameStr, tyConNameStr))+  = lookupTyCon moduleNameStr tyConNameStr+lookupFQN fqn+  = error $ "expected " ++ show "ModuleName.TypeName"+         ++ ", got " ++ show fqn
+ src/TypeLevel/Rewrite/Internal/PrettyPrint.hs view
@@ -0,0 +1,124 @@+{-# LANGUAGE LambdaCase, RecordWildCards #-}+module TypeLevel.Rewrite.Internal.PrettyPrint where++import Data.List (intercalate)++-- GHC API+import Outputable (ppr, showSDocUnsafe)+import TyCon (TyCon)+import Type (TyVar, Type)++-- term-rewriting API+import Data.Rewriting.Rule (Rule(..))+import Data.Rewriting.Rules (Reduct(..))+import Data.Rewriting.Term (Term(Fun, Var))++import TypeLevel.Rewrite.Internal.TypeEq+import TypeLevel.Rewrite.Internal.TypeRule+import TypeLevel.Rewrite.Internal.TypeTemplate+import TypeLevel.Rewrite.Internal.TypeTerm+++pprMaybe+  :: (a -> String)+  -> Maybe a+  -> String+pprMaybe pprA = \case+  Nothing+    -> "Nothing"+  Just a+    -> "Just ("+    ++ pprA a+    ++ ")"++pprList+  :: (a -> String)+  -> [a]+  -> String+pprList pprA+  = ("[" ++)+  . (++ "]")+  . intercalate ", "+  . fmap pprA+++pprTyCon+  :: TyCon -> String+pprTyCon+  = showSDocUnsafe . ppr++pprType+  :: Type -> String+pprType+  = showSDocUnsafe . ppr++pprTyVar+  :: TyVar -> String+pprTyVar+  = showSDocUnsafe . ppr+++pprTypeEq+  :: TypeEq -> String+pprTypeEq+  = pprType . unTypeEq+++pprTerm+  :: (f -> String)+  -> (v -> String)+  -> Term f v+  -> String+pprTerm pprF pprV = \case+  Var v+    -> pprV v+  Fun f args+    -> pprF f+    ++ " "+    ++ pprList (pprTerm pprF pprV) args++pprRule+  :: (f -> String)+  -> (v -> String)+  -> Rule f v+  -> String+pprRule pprF pprV (Rule {..})+  = "Rule "+ ++ "{ lhs = " ++ pprTerm pprF pprV lhs+ ++ ", rhs = " ++ pprTerm pprF pprV rhs+ ++ "}"++pprReduct+  :: (f -> String)+  -> (v -> String)+  -> (v' -> String)+  -> Reduct f v v'+  -> String+pprReduct pprF pprV pprV' (Reduct {..})+  = "Reduct "+ ++ "{ result = " ++ pprTerm pprF pprV result+ ++ ", pos = " ++ show pos+ ++ ", rule = " ++ pprRule pprF pprV' rule+ ++ ", subst = undefined"+ ++ "}"+++pprTypeTemplate+  :: TypeTemplate -> String+pprTypeTemplate+  = pprTerm pprTyCon pprTyVar++pprTypeTerm+  :: TypeTerm -> String+pprTypeTerm+  = pprTerm pprTyCon pprTypeEq++pprTypeRule+  :: TypeRule -> String+pprTypeRule+  = pprRule pprTyCon pprTyVar++pprTypeReduct+  :: Reduct TyCon TypeEq TyVar -> String+pprTypeReduct+  = pprReduct pprTyCon pprTypeEq pprTyVar
+ src/TypeLevel/Rewrite/Internal/Term.hs view
@@ -0,0 +1,16 @@+module TypeLevel.Rewrite.Internal.Term where++import Data.Rewriting.Term (Term(Fun))+++-- |+-- an expression like @(as ++ '[]) ++ bs@ would be represented as+-- @Fun appendTyCon [Var "as", Fun nilTyCon []@+-- or rather+-- @Fun appendTyCon [Fun starTyCon [], Var "as", Fun nilTyCon [Fun starTyCon []]@+-- because those polymorphic TyCons need to be specialized to the '*' kind++atomTerm+  :: f -> Term f v+atomTerm f+  = Fun f []
+ src/TypeLevel/Rewrite/Internal/TypeEq.hs view
@@ -0,0 +1,14 @@+module TypeLevel.Rewrite.Internal.TypeEq where++import Data.Function++import Type (Type, eqType)+++-- | A newtype around 'Type' which has an 'Eq' instance.+newtype TypeEq = TypeEq+  { unTypeEq :: Type+  }++instance Eq TypeEq where+  (==) = eqType `on` unTypeEq
+ src/TypeLevel/Rewrite/Internal/TypeRule.hs view
@@ -0,0 +1,43 @@+{-# LANGUAGE ViewPatterns #-}+module TypeLevel.Rewrite.Internal.TypeRule where++-- GHC API+import Name (getOccString)+import TyCon (TyCon)+import Type (TyVar, Type)++-- term-rewriting API+import Data.Rewriting.Rule (Rule(..))+import Data.Rewriting.Rules (Reduct(result), fullRewrite)+import Data.Rewriting.Term (Term(Fun))++import TypeLevel.Rewrite.Internal.TypeTemplate+import TypeLevel.Rewrite.Internal.TypeTerm+++type TypeRule = Rule TyCon TyVar++toTypeRule_maybe+  :: Type+  -> Maybe TypeRule+toTypeRule_maybe (toTypeTemplate_maybe -> Just (Fun (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
+ src/TypeLevel/Rewrite/Internal/TypeTemplate.hs view
@@ -0,0 +1,22 @@+{-# LANGUAGE LambdaCase, ViewPatterns #-}+module TypeLevel.Rewrite.Internal.TypeTemplate where++-- GHC API+import TyCon (TyCon)+import Type (TyVar, Type, getTyVar_maybe, splitTyConApp_maybe)++-- term-rewriting API+import Data.Rewriting.Term (Term(Fun, Var))+++type TypeTemplate = Term TyCon 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 _+  = Nothing
+ src/TypeLevel/Rewrite/Internal/TypeTerm.hs view
@@ -0,0 +1,29 @@+{-# LANGUAGE LambdaCase, ViewPatterns #-}+module TypeLevel.Rewrite.Internal.TypeTerm where++-- GHC API+import TyCon (TyCon)+import Type (Type, mkTyConApp, splitTyConApp_maybe)++-- term-rewriting API+import Data.Rewriting.Term (Term(Fun, Var))++import TypeLevel.Rewrite.Internal.TypeEq+++type TypeTerm = Term TyCon TypeEq++toTypeTerm+  :: Type -> TypeTerm+toTypeTerm (splitTyConApp_maybe -> Just (tyCon, args))+  = Fun tyCon (fmap toTypeTerm args)+toTypeTerm tp+  = Var (TypeEq tp)++fromTypeTerm+  :: TypeTerm -> Type+fromTypeTerm = \case+  Var x+    -> unTypeEq x+  Fun tyCon args+    -> mkTyConApp tyCon (fmap fromTypeTerm args)
+ test/should-compile/Data/Vinyl/TypeLevel/RewriteRules.hs view
@@ -0,0 +1,10 @@+{-# LANGUAGE ConstraintKinds, DataKinds, PolyKinds, TypeFamilies, TypeOperators #-}+module Data.Vinyl.TypeLevel.RewriteRules where++import Data.Vinyl.TypeLevel+++type RightIdentity as+  = (as ++ '[]) ~ as+type RightAssociative as bs cs+  = ((as ++ bs) ++ cs) ~ (as ++ (bs ++ cs))
+ test/should-compile/Data/Vinyl/TypeLevel/Test.hs view
@@ -0,0 +1,78 @@+{-# LANGUAGE DataKinds, RankNTypes, TypeFamilies, TypeOperators #-}+{-# OPTIONS_GHC -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++import Data.Vinyl.TypeLevel++import Data.Vinyl.TypeLevel.RewriteRules ()+++ex1a :: (((as ++ '[]) ++ (bs ++ '[])) ~ (as ++ bs) => r)+     -> proxy as+     -> proxy bs+     -> r+ex1a r _ _ = r++ex1b :: ((as ++ bs) ~ ((as ++ '[]) ++ (bs ++ '[])) => r)+     -> proxy as+     -> proxy bs+     -> r+ex1b r _ _ = r++ex1c :: ((as ++ (bs ++ cs)) ~ (((as ++ '[]) ++ (bs ++ '[])) ++ (cs ++ '[])) => r)+     -> proxy as+     -> proxy bs+     -> proxy cs+     -> r+ex1c r _ _ _ = r++ex1d :: (proxy (as ++ bs) ~ proxy ((as ++ '[]) ++ (bs ++ '[])) => r)+     -> proxy as+     -> proxy bs+     -> r+ex1d r _ _ = r++ex1e :: proxy as+     -> proxy bs+     -> proxy (as ++ bs)+     -> proxy ((as ++ '[]) ++ (bs ++ '[]))+ex1e _ _ r = r+++ex2a :: (((as ++ bs) ++ cs) ~ (as ++ (bs ++ cs)) => r)+     -> proxy as+     -> proxy bs+     -> proxy cs+     -> r+ex2a r _ _ _ = r++ex2b :: ((as ++ (bs ++ cs)) ~ ((as ++ bs) ++ cs) => r)+     -> proxy as+     -> proxy bs+     -> proxy cs+     -> r+ex2b r _ _ _ = r++ex2c :: ((as ++ (bs ++ (cs ++ ds))) ~ (((as ++ bs) ++ cs) ++ ds) => r)+     -> proxy as+     -> proxy bs+     -> proxy cs+     -> proxy ds+     -> r+ex2c r _ _ _ _ = r++ex2d :: (proxy (as ++ (bs ++ cs)) ~ proxy ((as ++ bs) ++ cs) => r)+     -> proxy as+     -> proxy bs+     -> proxy cs+     -> r+ex2d r _ _ _ = r++ex2e :: proxy as+     -> proxy bs+     -> proxy cs+     -> proxy (as ++ (bs ++ cs))+     -> proxy ((as ++ bs) ++ cs)+ex2e _ _ _ r = r
+ test/should-compile/MonoKinds/Append.hs view
@@ -0,0 +1,16 @@+{-# LANGUAGE ConstraintKinds, DataKinds, KindSignatures, TypeFamilies, TypeOperators #-}+module MonoKinds.Append where++import GHC.TypeLits+++-- unlike "SamePackage.Append", this version of '(++)' only works with+-- type-level lists of strings+type family (++) (as :: [Symbol]) (bs :: [Symbol]) where+  '[]       ++ bs = bs+  (a ': as) ++ bs = a ': (as ++ bs)++type RightIdentity as+  = (as ++ '[]) ~ as+type RightAssociative as bs cs+  = ((as ++ bs) ++ cs) ~ (as ++ (bs ++ cs))
+ test/should-compile/MonoKinds/Test.hs view
@@ -0,0 +1,76 @@+{-# LANGUAGE DataKinds, RankNTypes, TypeFamilies, TypeOperators #-}+{-# OPTIONS_GHC -fplugin TypeLevel.Rewrite+                -fplugin-opt=TypeLevel.Rewrite:MonoKinds.Append.RightIdentity+                -fplugin-opt=TypeLevel.Rewrite:MonoKinds.Append.RightAssociative #-}+module MonoKinds.Test where++import MonoKinds.Append+++ex1a :: (((as ++ '[]) ++ (bs ++ '[])) ~ (as ++ bs) => r)+     -> proxy as+     -> proxy bs+     -> r+ex1a r _ _ = r++ex1b :: ((as ++ bs) ~ ((as ++ '[]) ++ (bs ++ '[])) => r)+     -> proxy as+     -> proxy bs+     -> r+ex1b r _ _ = r++ex1c :: ((as ++ (bs ++ cs)) ~ (((as ++ '[]) ++ (bs ++ '[])) ++ (cs ++ '[])) => r)+     -> proxy as+     -> proxy bs+     -> proxy cs+     -> r+ex1c r _ _ _ = r++ex1d :: (proxy (as ++ bs) ~ proxy ((as ++ '[]) ++ (bs ++ '[])) => r)+     -> proxy as+     -> proxy bs+     -> r+ex1d r _ _ = r++ex1e :: proxy as+     -> proxy bs+     -> proxy (as ++ bs)+     -> proxy ((as ++ '[]) ++ (bs ++ '[]))+ex1e _ _ r = r+++ex2a :: (((as ++ bs) ++ cs) ~ (as ++ (bs ++ cs)) => r)+     -> proxy as+     -> proxy bs+     -> proxy cs+     -> r+ex2a r _ _ _ = r++ex2b :: ((as ++ (bs ++ cs)) ~ ((as ++ bs) ++ cs) => r)+     -> proxy as+     -> proxy bs+     -> proxy cs+     -> r+ex2b r _ _ _ = r++ex2c :: ((as ++ (bs ++ (cs ++ ds))) ~ (((as ++ bs) ++ cs) ++ ds) => r)+     -> proxy as+     -> proxy bs+     -> proxy cs+     -> proxy ds+     -> r+ex2c r _ _ _ _ = r++ex2d :: (proxy (as ++ (bs ++ cs)) ~ proxy ((as ++ bs) ++ cs) => r)+     -> proxy as+     -> proxy bs+     -> proxy cs+     -> r+ex2d r _ _ _ = r++ex2e :: proxy as+     -> proxy bs+     -> proxy cs+     -> proxy (as ++ (bs ++ cs))+     -> proxy ((as ++ bs) ++ cs)+ex2e _ _ _ r = r
+ test/should-compile/SamePackage/Append.hs view
@@ -0,0 +1,11 @@+{-# LANGUAGE ConstraintKinds, DataKinds, PolyKinds, TypeFamilies, TypeOperators #-}+module SamePackage.Append where++type family (++) as bs where+  '[]       ++ bs = bs+  (a ': as) ++ bs = a ': (as ++ bs)++type RightIdentity as+  = (as ++ '[]) ~ as+type RightAssociative as bs cs+  = ((as ++ bs) ++ cs) ~ (as ++ (bs ++ cs))
+ test/should-compile/SamePackage/Test.hs view
@@ -0,0 +1,76 @@+{-# LANGUAGE DataKinds, RankNTypes, TypeFamilies, TypeOperators #-}+{-# OPTIONS_GHC -fplugin TypeLevel.Rewrite+                -fplugin-opt=TypeLevel.Rewrite:SamePackage.Append.RightIdentity+                -fplugin-opt=TypeLevel.Rewrite:SamePackage.Append.RightAssociative #-}+module SamePackage.Test where++import SamePackage.Append+++ex1a :: (((as ++ '[]) ++ (bs ++ '[])) ~ (as ++ bs) => r)+     -> proxy as+     -> proxy bs+     -> r+ex1a r _ _ = r++ex1b :: ((as ++ bs) ~ ((as ++ '[]) ++ (bs ++ '[])) => r)+     -> proxy as+     -> proxy bs+     -> r+ex1b r _ _ = r++ex1c :: ((as ++ (bs ++ cs)) ~ (((as ++ '[]) ++ (bs ++ '[])) ++ (cs ++ '[])) => r)+     -> proxy as+     -> proxy bs+     -> proxy cs+     -> r+ex1c r _ _ _ = r++ex1d :: (proxy (as ++ bs) ~ proxy ((as ++ '[]) ++ (bs ++ '[])) => r)+     -> proxy as+     -> proxy bs+     -> r+ex1d r _ _ = r++ex1e :: proxy as+     -> proxy bs+     -> proxy (as ++ bs)+     -> proxy ((as ++ '[]) ++ (bs ++ '[]))+ex1e _ _ r = r+++ex2a :: (((as ++ bs) ++ cs) ~ (as ++ (bs ++ cs)) => r)+     -> proxy as+     -> proxy bs+     -> proxy cs+     -> r+ex2a r _ _ _ = r++ex2b :: ((as ++ (bs ++ cs)) ~ ((as ++ bs) ++ cs) => r)+     -> proxy as+     -> proxy bs+     -> proxy cs+     -> r+ex2b r _ _ _ = r++ex2c :: ((as ++ (bs ++ (cs ++ ds))) ~ (((as ++ bs) ++ cs) ++ ds) => r)+     -> proxy as+     -> proxy bs+     -> proxy cs+     -> proxy ds+     -> r+ex2c r _ _ _ _ = r++ex2d :: (proxy (as ++ (bs ++ cs)) ~ proxy ((as ++ bs) ++ cs) => r)+     -> proxy as+     -> proxy bs+     -> proxy cs+     -> r+ex2d r _ _ _ = r++ex2e :: proxy as+     -> proxy bs+     -> proxy cs+     -> proxy (as ++ (bs ++ cs))+     -> proxy ((as ++ bs) ++ cs)+ex2e _ _ _ r = r
+ test/should-compile/Test.hs view
@@ -0,0 +1,7 @@+import Data.Vinyl.TypeLevel.Test+import SamePackage.Test+import TypeLevel.Append.Test+++main :: IO ()+main = putStrLn "typechecks."
+ test/should-compile/TypeLevel/Append/Test.hs view
@@ -0,0 +1,76 @@+{-# LANGUAGE DataKinds, RankNTypes, TypeFamilies, TypeOperators #-}+{-# OPTIONS_GHC -fplugin TypeLevel.Rewrite+                -fplugin-opt=TypeLevel.Rewrite:TypeLevel.Append.RightIdentity+                -fplugin-opt=TypeLevel.Rewrite:TypeLevel.Append.RightAssociative #-}+module TypeLevel.Append.Test where++import TypeLevel.Append+++ex1a :: (((as ++ '[]) ++ (bs ++ '[])) ~ (as ++ bs) => r)+     -> proxy as+     -> proxy bs+     -> r+ex1a r _ _ = r++ex1b :: ((as ++ bs) ~ ((as ++ '[]) ++ (bs ++ '[])) => r)+     -> proxy as+     -> proxy bs+     -> r+ex1b r _ _ = r++ex1c :: ((as ++ (bs ++ cs)) ~ (((as ++ '[]) ++ (bs ++ '[])) ++ (cs ++ '[])) => r)+     -> proxy as+     -> proxy bs+     -> proxy cs+     -> r+ex1c r _ _ _ = r++ex1d :: (proxy (as ++ bs) ~ proxy ((as ++ '[]) ++ (bs ++ '[])) => r)+     -> proxy as+     -> proxy bs+     -> r+ex1d r _ _ = r++ex1e :: proxy as+     -> proxy bs+     -> proxy (as ++ bs)+     -> proxy ((as ++ '[]) ++ (bs ++ '[]))+ex1e _ _ r = r+++ex2a :: (((as ++ bs) ++ cs) ~ (as ++ (bs ++ cs)) => r)+     -> proxy as+     -> proxy bs+     -> proxy cs+     -> r+ex2a r _ _ _ = r++ex2b :: ((as ++ (bs ++ cs)) ~ ((as ++ bs) ++ cs) => r)+     -> proxy as+     -> proxy bs+     -> proxy cs+     -> r+ex2b r _ _ _ = r++ex2c :: ((as ++ (bs ++ (cs ++ ds))) ~ (((as ++ bs) ++ cs) ++ ds) => r)+     -> proxy as+     -> proxy bs+     -> proxy cs+     -> proxy ds+     -> r+ex2c r _ _ _ _ = r++ex2d :: (proxy (as ++ (bs ++ cs)) ~ proxy ((as ++ bs) ++ cs) => r)+     -> proxy as+     -> proxy bs+     -> proxy cs+     -> r+ex2d r _ _ _ = r++ex2e :: proxy as+     -> proxy bs+     -> proxy cs+     -> proxy (as ++ (bs ++ cs))+     -> proxy ((as ++ bs) ++ cs)+ex2e _ _ _ r = r
+ typelevel-rewrite-rules.cabal view
@@ -0,0 +1,72 @@+cabal-version: 1.12++-- This file has been generated from package.yaml by hpack version 0.31.2.+--+-- see: https://github.com/sol/hpack+--+-- hash: a0aa0b58de9c55fa77a152d9a3aa0be871bfa33439ebe19185cb1283b97d6350++name:           typelevel-rewrite-rules+version:        0.1+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+homepage:       https://github.com/gelisam/typelevel-rewrite-rules#readme+bug-reports:    https://github.com/gelisam/typelevel-rewrite-rules/issues+author:         Samuel Gélineau+maintainer:     gelisam+github@gmail.com+license:        PublicDomain+build-type:     Simple+extra-source-files:+    README.md+    CHANGELOG.md++source-repository head+  type: git+  location: https://github.com/gelisam/typelevel-rewrite-rules++library+  exposed-modules:+      TypeLevel.Append+      TypeLevel.Rewrite+      TypeLevel.Rewrite.Internal.Lookup+      TypeLevel.Rewrite.Internal.PrettyPrint+      TypeLevel.Rewrite.Internal.Term+      TypeLevel.Rewrite.Internal.TypeEq+      TypeLevel.Rewrite.Internal.TypeRule+      TypeLevel.Rewrite.Internal.TypeTemplate+      TypeLevel.Rewrite.Internal.TypeTerm+  other-modules:+      Paths_typelevel_rewrite_rules+  hs-source-dirs:+      src+  ghc-options: -W -Wall+  build-depends:+      base >=4.12 && <6+    , ghc >=8.6.3+    , ghc-prim >=0.5.3+    , ghc-tcplugins-extra >=0.3+    , term-rewriting >=0.3.0.1+    , transformers >=0.5.5.0+  default-language: Haskell2010++test-suite should-compile+  type: exitcode-stdio-1.0+  main-is: Test.hs+  other-modules:+      Data.Vinyl.TypeLevel.RewriteRules+      Data.Vinyl.TypeLevel.Test+      MonoKinds.Append+      MonoKinds.Test+      SamePackage.Append+      SamePackage.Test+      TypeLevel.Append.Test+      Paths_typelevel_rewrite_rules+  hs-source-dirs:+      test/should-compile+  build-depends:+      base >=4.12 && <6+    , ghc-prim >=0.5.3+    , typelevel-rewrite-rules+    , vinyl+  default-language: Haskell2010