Coercion maching in RULES is fragile

If we have a cast or coercion in the LHS of a rule, matching against is is very fragile. This came up in #13474 (closed).

Consider the map/coerce rule in GHC.Base. (There is a similar one in containers:Data.Map.Internal.) Initially it looks like this:

RULE "map/coerce" forall a b (x::a) (c::a~b) (xs::[a]).
                  map (\x. x |> c) xs = xs |> [c]

In typechecking and desugaring rules we are careful only to use coercion variables in a cast on the LHS, so that matching is more likely to succeed. After all, we never want to match on the way a proof is done, only on the result of the proof.

However, suppose some target expression (to which we would like to apply the rule) looks like

        map (\(y::ty). y |> ec) exs

The simplifier (see Note [Casts and lambdas] in SimplUtils) swizzles the cast outside the lambda, thus

        map ((\ (y::ty). y)  |>  (<ty> -> ec)) exs

Now it's not so easy to match the rule, becuase in one the cast is outside the lambda and in the other it is inside. The casts are making matching fragile.

What to do?

Plan A (current)

Currently, we run the simplifier on the rule LHS, so that the same simplifications apply. But now we get

RULE "map/coerce" forall a b (x::a) (c::a~b) (xs::[a]).
                  map ((\x. x) |> (<a> -> c) xs = xs |> [c]

And now the coercion on the LHS has structure; and we must decompose that structure to bind the c to use it on the RHS.

So Rules.match_co actually matches the structure of coercions (sigh); but is only partially implemented (a) because it is tedious and (b) because it should not be necessary.

Pragmatic but unsatisfactory.

Plan B (possible)

Do not simplify the LHS of rules, so that casts always have a simple coercion variable. But make matching work "modulo casts". Something like this:

match :: PatternExpr -> TargetExpr -> Coercion -> ...result...
-- Invariant:   match pat e c  ==  match pat (e |> c) Refl
-- That is, the coercion wraps the TargetExpr

Now when we find a cast in the target expr we can push it into the coercion

match pat (Cast e c1) c2 = match pat e1 (c1 ; c2)

And a cast in the pattern just binds the variable

match (Cast p v) e c = match p e Refl   +  {v :-> c}

This isn't quite right because we must make sure the types match, but it's close.

The decomposition rules become more interesting:

match (\x.p) (\x.e) c
  = match p e[x -> x |> arg_co] res_co
  where
    (arg_co, res_co) = decomposeFunCo c

or something like that. In effect we do the swizzling on the fly.

This is all similar to the coercion swizzling in Unify when unifying types. I cannot fathom all the details and I'm not sure it's worth the work. But somehow it ought to be possible to make casts NOT impede matching in a systematic way.

Trac metadata

Trac field	Value
Version	8.0.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture