Unnecessary equality superclass

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.

Trac metadata

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