Matching

[augustss]

I suspect that the rewrite rules use exact matching for the RHS instead of matching/unification.
Here's a problem I have:

GHC says:
Could not deduce: Drop (Length sh1 - 1) sh1 ~ '[s0]
where s0 is not a variable I've not quantified over, so I can't mention it.

This rule doesn't match:
type ListLast xs x =
Drop (Length xs - 1) xs ~ '[x]

Nor does this one:
type ListLast xs =
Drop (Length xs - 1) xs ~ '[Last xs]

Any suggestions?

[gelisam]

I suspect that the rewrite rules use exact matching for the RHS instead of matching/unification.

Note that even though the syntax for rules is written lhs ~ rhs and they help resolve equality constraints, which also have the form expr1 ~ expr2, it is not the case that the entire rule is matched against the entire constraint. Instead, it is only lhs which is matched against sub-expressions in both expr1 and expr2, and all matching sub-expressions are replaced with rhs. rhs is not matched against anything.

where s0 is not a variable I've not quantified over, so I can't mention it.

That's probably fine: the goal is not necessarily to discharge the entire constraint, but to rewrite it in a way which makes ghc happy. With the rule Drop (Length xs - 1) xs ~ '[Last xs], the equality constraint Drop (Length sh1 - 1) sh1 ~ '[s0] gets rewritten to '[Last sh1] ~ '[s0], and then ghc takes over from there. If s0 is rigid, then ghc will still be unhappy, but if s0 is a unification variable, ghc should now be able to solve it.

This rule doesn't match:
type ListLast xs x =
Drop (Length xs - 1) xs ~ '[x]

I am happy to hear that this rewrite rule doesn't fire, because it looks extremely unsound! x doesn't appear on the LHS, so the rule is saying that the LHS can be rewritten to anything at all. I delegate the rewriting logic to the term-rewriting library, so I'm not quite sure why it doesn't fire, but I suspect it is because the library cannot figure out from the LHS match what it should replace x with, and it refuses to guess.

Nor does this one:
type ListLast xs =
Drop (Length xs - 1) xs ~ '[Last xs]

I must not quite understand the program you have in mind, because it's working for me. Well, kind of: Length xs - 1 triggers #4 for me, so I had to use unary numbers instead. In any case, here are some concrete definitions for Drop, (-), and Last, and a few functions using them:

{-# LANGUAGE ConstraintKinds, DataKinds, GADTs, TypeApplications, TypeFamilies, TypeOperators #-}
module Lib where

import Data.Vinyl
import Data.Vinyl.TypeLevel


data SingNat n where
  SZ :: SingNat 'Z
  SS :: SingNat n -> SingNat ('S n)

rlength :: Rec f xs -> SingNat (RLength xs)
rlength RNil      = SZ
rlength (_ :& xs) = SS (rlength xs)


type family (-) n m where
  n - 'Z = n
  'Z - m = 'Z
  'S n - 'S m = n - m

rpred :: SingNat n -> SingNat (n - 'S 'Z)
rpred SZ     = SZ
rpred (SS n) = n


fromSingleton :: Rec f '[a] -> f a
fromSingleton (fa :& RNil) = fa


type family Drop n xs where
  Drop 'Z     xs        = xs
  Drop n      '[]       = '[]
  Drop ('S n) (x ': xs) = Drop n xs

rdrop :: SingNat n -> Rec f xs -> Rec f (Drop n xs)
rdrop SZ     xs        = xs
rdrop _      RNil      = RNil
rdrop (SS n) (_ :& xs) = rdrop n xs


type family Last xs where
  Last (x ': '[]) = x
  Last (x ': xs)  = Last xs

type MyRule xs
  = Drop (RLength xs - 'S 'Z) xs ~ '[Last xs]

Without typelevel-rewrite-rules, I don't quite get an error about a missing Drop (Length sh1 - 1) sh1 ~ '[s0] constraint, but I do get an inferred type with that constraint:

{-# LANGUAGE DataKinds, TypeFamilies, TypeOperators #-}
module Main where
import Lib

-- inferred type:
-- rlast :: Drop (RLength xs - 'S 'Z) xs ~ '[a]
--       => Rec f xs -> f a
rlast xs = fromSingleton $ rdrop n xs
  where
    n = rpred (rlength xs)

If I add MyRule, that constraint gets rewritten, ghc is able to solve a, and thus a no longer appears in the inferred type:

{-# LANGUAGE DataKinds, TypeFamilies, TypeOperators #-}
{-# OPTIONS_GHC -fplugin TypeLevel.Rewrite
                -fplugin-opt=TypeLevel.Rewrite:Lib.MyRule #-}
module Main where
import Lib

-- inferred type:
-- rlast :: Rec f xs -> f (Last xs)
rlast xs = fromSingleton $ rdrop n xs
  where
    n = rpred (rlength xs)

[augustss]

Foolishly I didn't save the code that was causing me problems. And noq I can't recreate the exact same problem.
If/when I do, I'll let you knw.

Thanks!

[augustss]

I've recreated the bug. Unzip and compile Flatten.hs. It works. Remove the line with a comment, and it doesn't compile. The removed line corresponds exactly to an equality in the Rules.hs file.

bug.zip

[gelisam]

Wow, thanks for that tricky test case, it manages to exercises a ton of corner cases at once! Many of those corner cases are not supported by version 0.1 or at all, so here is the long list of changes which are required in order to make the file compile with that line removed.

To begin with, a few things which aren't technically a problem with typelevel-rewrite-rules, but probably indicates that the documentation could be improved.

First, Rules is not a plugin; TypeLevel.Rewrite is a plugin, and one of its parameters involves Rules. We thus need to replace

{-# OPTIONS_GHC -fplugin Rules
                -fplugin-opt=Rules:ListLast
  #-}

with

{-# OPTIONS_GHC -fplugin TypeLevel.Rewrite
                -fplugin-opt=TypeLevel.Rewrite:Rules.ListLast
  #-}

I don't know why ghc doesn't complain that the Rules module is not a valid ghc plugin even though it does not export a plugin :: Plugin.

Next, the OPTIONS_GHC block needs to be moved above the module line. Again, no idea why ghc chooses to silently ignore the OPTIONS_GHC block in that case instead of being more helpful.

Okay, now for the changes which are needed because of bugs in typelevel-rewrite-rules.

First, because of #4 , switch from GHC.TypeLits's Nat to a unary representation.

Next, switch to the HEAD version of typelevel-rewrite-rules in order to take the given constraints into account. rerank @(Pred (Rank shx)) wants the constraint Drop (Pred (Rank shx)) sh ~ '[s], while the type signature for flatten gives the constraint shx ~ sh. Or something like that; I haven't quite figured out why some type variables get instantiated inside the wanted constraints while others are specified by given constraints. Anyway, by combining the wanted and the given constraints, we finally get the type Drop (Pred (Rank shx)) shx which matches the LHS, so it gets rewritten to '[Last shx].

At this point, the type error about a missing Drop (Pred (Rank shx)) shx ~ '[s0] disappears, but unfortunately it is replaced by another type error:

Could not deduce (Shape
                   ( Take ...
                  ++ (Last shx : shy)
                   ))
 arising from a use of ‘rerank’
from the context: ( ...
                  , Shape (shx ++ shy)
                  , (shx ++ shy) ~ ( Take ...
                                  ++ (Drop (Pred (Rank shx)) shx ++ shy)
                                   )
                  )

The problem is that the wanted constraint used to be

(Shape
  ( Take ...
 ++ (Drop (Pred (Rank shx)) shx ++ shy)
  ))

That matches the given constraints, but the rewritten version doesn't. Does that mean typelevel-rewrite-rules should also rewrite the given constraints? I'm not sure yet.

Anyway, we can solve the problem by manually replacing the Drop (Pred (Rank shx)) shx with '[Last shx] in flatten's type signature.

Here is the result after all those changes:

{-# LANGUAGE ConstraintKinds, DataKinds, TypeFamilies, TypeOperators, UndecidableInstances #-}
module Rules where
import GHC.TypeLits

data MyNat = Z | S MyNat

class Shape (s :: [Nat])

instance Shape '[]

instance (Shape s, KnownNat n) => Shape (n ': s)

type family Rank (s :: [Nat]) :: MyNat where
  Rank '[] = 'Z
  Rank (n : ns) = 'S (Rank ns)

type family Take (n :: MyNat) (xs :: [Nat]) :: [Nat] where
    Take 'Z xs = '[]
    Take ('S n) (x ': xs) = x ': Take n xs

type family Drop (n :: MyNat) (xs :: [Nat]) :: [Nat] where
    Drop 'Z xs = xs
    Drop ('S n) (x ': xs) = Drop n xs

type family (++) (xs :: [Nat]) (ys :: [Nat]) :: [Nat] where
  (++) '[] ys = ys
  (++) (x ': xs) ys = x ': (xs ++ ys)

type family Last (xs :: [Nat]) where
  Last '[x] = x
  Last (x ': xs) = Last xs

type family Init (xs :: [Nat]) where
  Init '[x] = '[]
  Init (x ': xs) = x ': Init xs

type family Pred (n :: MyNat) :: MyNat where
  Pred ('S n) = n

type ListLast xs =
  Drop (Pred (Rank xs)) xs ~ '[Last xs]

{-# LANGUAGE AllowAmbiguousTypes, DataKinds, FlexibleContexts, RankNTypes, ScopedTypeVariables, TypeApplications, TypeFamilies, TypeOperators #-}

{-# OPTIONS_GHC -fplugin TypeLevel.Rewrite
                -fplugin-opt=TypeLevel.Rewrite:Rules.ListLast
  #-}
module Flatten where
import GHC.TypeLits

import Rules

data Array (sh :: [Nat]) a

rerank :: forall n i o sh a b .
          (Drop n sh ~ i, Shape sh, Shape o, Shape (Take n sh ++ o)) =>
          (Array i a -> Array o b) -> Array sh a -> Array (Take n sh ++ o) b
rerank = undefined

ravel :: forall s sh a .
         (Shape sh, KnownNat s) =>
         Array '[s] (Array sh a) -> Array (s:sh) a
ravel = undefined

flatten :: forall shx shy a .
           (KnownNat (Last shx), Shape shx, Shape shy, Shape (shx ++ shy),
           -- Drop (Pred (Rank shx)) shx ~ '[Last shx],   -- With a lot of effort, this line can be removed :)
           (shx ++ shy) ~ (Take (Pred (Rank shx)) shx ++ ('[Last shx] ++ shy))
           ) =>
           Array shx (Array shy a) -> Array (shx ++ shy) a
flatten = rerank @(Pred (Rank shx)) ravel

[augustss]

Wow, that was a stupid mistake of mine. I'm glad my example uncovered some other problems as well.
I'm afraid using MyNat instead of Nat is not an option for me. The type argument to rerank is mostly something like @1 or @2, and not having numerical literals would ruin the user experience. Is the reason I can't use Nat that it's not implemented, or is it something more fundamental?
BTW, the equality (shx ++ shy) ~ (Take (Pred (Rank shx)) shx ++ ('[Last shx] ++ shy)) should, of course, have a rule too, since it's a valid equality. But I was doing them one at a time.

[gelisam]

Is the reason I can't use Nat that it's not implemented, or is it something more fundamental?

At some point I parse the LHS and the RHS into trees, and I assume that internal nodes are type constructors applied to type arguments, and that leaves are type constructors applied to zero arguments. I am guessing that the problem is that a Nat is a literal, not a type constructor. If so, then I think I just need to be more liberal in what leaves can look like.

[gelisam]

That was indeed the problem, and I have now fixed #4, so numeric literals are now supported!

There is still the tricky business of given vs wanted constraints. You know a lot about Haskell compilers, maybe you can help? I don't have a good story for what typelevel-rewrite-rules should do with the given constraints. Version 0.1 completely ignores them, the HEAD version does a little bit better, but the (shx ++ shy) ~ (Take ... ++ ...) part of your example hints that I'm still not doing enough.

What the HEAD version is currently doing is as follows. I've noticed that most of the given constraints have the form expr ~ var; that is, the given constraints give the definitions of the type variables which have already been solved. Thus, when I encounter such a var in a type expression I am trying to rewrite, I substitute each var with its definition, in the hope that this will cause the type expression to match the LHS. I don't understand why I have to do this, since this note claims that ghc already uses the given constraints to rewrite the wanted constraints by replacing their type variables with their definition, but if I don't do it myself, examples like the Drop (Pred (Rank shx)) sh ~ '[s] part of your example and this test aren't rewritten.

Does it seem sound to apply the rewrite rules to the given constraints? My intuition tells me that I should either leave them alone or apply the rewrite rules in reverse, but that would not have helped in your example. Clearly, I need a better mental model of the relationship between the wanted and the given constraints, beyond "givens are what we already know and wanteds are what we want to prove".

[augustss]

I don't know enough about ghc's constraint solving to have much of an opinion.
Intuitively, it feels like the equalities given by the rules should behave much like given constraints.
An extra complication is that the rules are universally quantified, so they need to be instantiated to be added as givens.