#13476: Coercion maching in RULES is fragile
-------------------------------------+-------------------------------------
Reporter: simonpj | Owner: (none)
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 8.0.1
Keywords: | Operating System: Unknown/Multiple
Architecture: | Type of failure: None/Unknown
Unknown/Multiple |
Test Case: | Blocked By:
Blocking: | Related Tickets:
Differential Rev(s): | Wiki Page:
-------------------------------------+-------------------------------------
If we have a cast or coercion in the LHS of a rule, matching against is is
very fragile. This came up in #13474.
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.
--
Ticket URL: