#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: GHC The Glasgow Haskell Compiler