[GHC] #13476: Coercion maching in RULES is fragile

[GHC]

#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: <http://ghc.haskell.org/trac/ghc/ticket/13476>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler