SPECIALISE fails with a cryptic warning

[rl]

Example:

type family T a
type instance T Int = Bool

foo :: Num a => a -> T a
foo = undefined

{-# SPECIALISE foo :: Int -> Bool #-}

GHC produces this warning:

    RULE left-hand side too complicated to desugar
      case cobox of _ { GHC.Types.Eq# cobox ->
      (foo @ Int $dNum)
      `cast` (<Int> -> cobox :: (Int -> T Int) ~# (Int -> Bool))
      }

Given that rewrite rules don't reliably work in the presence of type families, I somewhat suspect that GHC won't be able to generate a sensible specialisation here but it should produce a better diagnostic.

[illissius]

With GHC 7.0 the message was at least a bit less noisy:

             RULE left-hand side too complicated to desugar
               (foo @ Int $dNum)
               `cast` (Int -> co :: (Int -> T Int) ~ (Int -> Bool))

Also, I can work around it by writing

{-# SPECIALIZE foo :: Int -> T Int #-}

that is, leave the type family unexpanded, and then it works.

But if I change the type signature of foo a bit, to introduce a name for T a:

foo :: (Num a, b ~ T a) => a -> b
{-# SPECIALIZE foo :: Int -> T Int #-}

that breaks again, with the 7.0 error message staying much the same (only an @ Bool and an @ co added to the second line), and the 7.4 message getting considerably uglier:

             RULE left-hand side too complicated to desugar
               case cobox of _ { GHC.Types.Eq# cobox ->
               (foo
                  @ Int
                  @ Bool
                  $dNum
                  (case cobox of _ { GHC.Types.Eq# cobox ->
                   GHC.Types.Eq# @ * @ Bool @ (T Int) @~ cobox
                   }))
               `cast` (<Int> -> cobox :: (Int -> Bool) ~# (Int -> T Int))
               }

If I once again change the pragma to match the new "shape" of the signature:

{-# SPECIALISE foo :: b ~ T Int => Int -> b #-}

then with 7.0 it compiles fine!, while 7.4 outputs this perfect monstrosity:

             RULE left-hand side too complicated to desugar
               let {
                 cobox :: T Int ~ b
                 [LclId]
                 cobox =
                   case cobox of _ { GHC.Types.Eq# cobox ->
                   GHC.Types.Eq# @ * @ (T Int) @ b @~ (Sym cobox)
                   } } in
               let {
                 cobox :: b ~ Bool
                 [LclId]
                 cobox =
                   case cobox of _ { GHC.Types.Eq# cobox ->
                   GHC.Types.Eq#
                     @ * @ b @ Asdf.R:TInt @~ (Sym cobox ; Asdf.TFCo:R:TInt)
                   } } in
               foo
                 @ Int
                 @ b
                 GHC.Num.$fNumInt
                 (case case case case cobox of _ { GHC.Types.Eq# cobox ->
                                 case cobox of _ { GHC.Types.Eq# cobox ->
                                 GHC.Types.Eq# @ * @ (T Int) @ Bool @~ (cobox ; cobox)
                                 }
                                 }
                            of _ { GHC.Types.Eq# cobox ->
                            case case cobox of _ { GHC.Types.Eq# cobox ->
                                 GHC.Types.Eq# @ * @ Bool @ b @~ (Sym cobox)
                                 }
                            of _ { GHC.Types.Eq# cobox ->
                            GHC.Types.Eq# @ * @ (T Int) @ b @~ (cobox ; cobox)
                            }
                            }
                       of _ { GHC.Types.Eq# cobox ->
                       GHC.Types.Eq# @ * @ b @ (T Int) @~ (Sym cobox)
                       }
                  of _ { GHC.Types.Eq# cobox ->
                  GHC.Types.Eq# @ * @ b @ (T Int) @~ cobox
                  })

I know this bug is only about the error message, but it seems like that last example might be an actual regression. Should I open a new ticket for it, or is it that "thou shalt not use RULES with type families and expect it to work"?

[illissius]

Just to amuse matters further, these both work, with both 7.0 and 7.4:

foo :: (Num a, b ~ T a) => a -> b
{-# SPECIALISE foo :: b ~ Bool => Int -> b #-}

foo :: (Num a, b ~ T a) => a -> b
{-# SPECIALISE foo :: Int -> Bool #-}

that is, completely the opposite of the original example, now it works if and only if I *do* expand the type family, and it doesn't matter what I do with the equality constraint.

(FTR I'm testing with 7.0 and 7.4 because I don't have a 7.2 on hand.)