[GHC] #15205: Unnecessary equality superclass

[GHC]

#15205: Unnecessary equality superclass
-------------------------------------+-------------------------------------
           Reporter:  simonpj        |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:  8.6.1
          Component:  Compiler       |           Version:  8.4.3
           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:
-------------------------------------+-------------------------------------
 Consider
 {{{
 {-# LANGUAGE MultiParamTypeClasses, GADTs, TypeOperators #-}
 module Foo where

 class (a ~ b) => C a b where
   op :: a -> a -> b

 f :: C a b => a -> b
 f x = op x x
 }}}
 If you compile this you'll end up with
 {{{
 f = \ (@ a_a1dk)
       (@ b_a1dl)
       ($dC_a1dn :: C a_a1dk b_a1dl)
       (eta_B1 :: a_a1dk) ->
       case GHC.Types.heq_sel
              @ *
              @ *
              @ a_a1dk
              @ b_a1dl
              ((Foo.$p1C @ a_a1dk @ b_a1dl $dC_a1dn)
               `cast` (Data.Type.Equality.N:~[0] <*>_N <a_a1dk>_N
 <b_a1dl>_N
                       :: (a_a1dk ~ b_a1dl) ~R# (a_a1dk ~~ b_a1dl)))
       of co_a1dw
       { __DEFAULT ->
       op @ a_a1dk @ b_a1dl $dC_a1dn eta_B1 eta_B1
       }
 }}}
 What is that unused `heq_sel` doing?

 It happens during solving
 * We have `[G] a ~ b`
 * And, by superclasses we have `[G] a ~# b`
 * We use this to rewrite `a` to `b` in both givens and wanteds
 which is all fine, but we end up with
 {{{
 f = \ (@ a_a1dk) (@ b_a1dl) ($dC_a1dn :: C a_a1dk b_a1dl) ->
       case GHC.Types.heq_sel
              @ *
              @ *
              @ a_a1dk
              @ b_a1dl
              (Data.Type.Equality.$p1~
                 @ * @ a_a1dk @ b_a1dl (Foo.$p1C @ a_a1dk @ b_a1dl
 $dC_a1dn))
       of co_a1dw
       { __DEFAULT ->
       \ (x_axX :: a_a1dk) ->
         op
           @ a_a1dk
           @ b_a1dl
           (($dC_a1dn
             `cast` ((C co_a1dw <b_a1dl>_N)_R
                     :: C a_a1dk b_a1dl ~R# C b_a1dl b_a1dl))
            `cast` ((C (Sym co_a1dw) <b_a1dl>_N)_R
                    :: C b_a1dl b_a1dl ~R# C a_a1dk b_a1dl))
           x_axX
           x_axX
       }
 }}}
 Notice that `co_a1dw` is used.  But we are just casting and casting back,
 so it ends up as Refl and `co_a1dw` is unused.

 Nothing is wrong here, but it seems inelegant

 * Can we discard that `heq_sel`?  Perhaps we can declare that dictionary-
 valued terms are always treated strictly (#2439), so that `(heq_sel ...)`
 is guaranteed non-bottom, and we can discard the case.

 * Or maybe we can expand the given superclasses less aggressively, so that
 the equality isn't exposed until necessary.  But see `Note [Eagerly expand
 given superclasses]` in `TcCanonical`.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15205>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler