[GHC] #10906: `SPECIALIZE instance` could be better

[GHC]

#10906: `SPECIALIZE instance` could be better
-------------------------------------+-------------------------------------
              Reporter:  goldfire    |             Owner:
                  Type:  feature     |            Status:  new
  request                            |
              Priority:  normal      |         Milestone:
             Component:  Compiler    |           Version:  7.10.2
              Keywords:              |  Operating System:  Unknown/Multiple
          Architecture:              |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
             Test Case:              |        Blocked By:
              Blocking:              |   Related Tickets:
Differential Revisions:              |
-------------------------------------+-------------------------------------
 END GOAL: Use dependent types (or their approximation) to make code run
 faster.
 -----------------------------

 Suppose we have a heterogeneous list type that can only hold a nice,
 limited set of things, as defined by this universe:
 {{{
 data U = INT | BOOL | LIST U

 -- interpret the universe into Haskell types
 type family El u where
   El 'INT = Int
   El 'BOOL = Bool
   El ('LIST u) = [El u]
 }}}

 Here's our list type:
 {{{
 data HList :: [U] -> * where
   Nil  :: HList '[]
   (:>) :: El u -> HList us -> HList (u ': us)
 infixr 5 :>
 }}}

 Now, suppose I want to write a `Show` instance for `HList us`. This should
 certainly be possible -- we can see that such a list can contain only
 things that have instances for `Show`. But I don't really expect GHC to do
 the nested induction to figure that out.

 Through moderate pyrotechnics, I can get something like this to type-
 check, where I'm eliding the pyrotechnics:

 {{{
 -- space separated (terminated, actually), just for ease
 instance {- don't look here -} => Show (HList us) where
   show Nil       = ""
   show (x :> xs) = {- convince GHC that we can `show x` -} $
                    show x ++ " " ++ show xs
 }}}

 (The full file is attached. But it's nothing extraordinary.)

 Now, suppose in client code, I know I'm often dealing with `HList '[INT,
 BOOL, LIST INT]`. Let's call that type `MyList`. When printing a `MyList`,
 the `Show` instance above has to do a runtime lookup to figure how to
 print the elements of `MyList`. It must do this //every time//.

 This is very silly. The whole point of putting the element types in the
 index to `HList` is so that GHC can know, statically, what types the
 elements are. We shouldn't have to check!

 The next step in my thought process was to use `{-# SPECIALIZE instance
 ... #-}` to specialize the `Show` instance. But then I ran into two
 problems:

 1. `{-# SPECIALIZE instance ... #-}` is allowed only in the context of the
 instance declaration. You can't do it in an importing module, even if the
 exporting module is kind enough to say `INLINABLE` in the right spots.

 2. `{-# SPECIALIZE instance ... #-}` doesn't allow one specialization to
 use another.

 3. (For more complicated scenarios) `{-# SPECIALIZE instance ... #-}`
 doesn't allow type families in the `...`.

 About point (1): Is there a good reason for this restriction? Of course,
 the concrete implementations of the methods of the instance to be
 specialized must be available, but the exporting module should be able to
 arrange that with the right pragmas.

 To illustrate (2), I said `{-# SPECIALIZE instance Show (HList '[ 'INT,
 'BOOL, 'LIST 'INT ]) #-}` and GHC specialized only the first layer. OK.
 Reasonable enough. But then I tried

 {{{
   {-# SPECIALIZE instance Show (HList '[ 'LIST 'INT ]) #-}
   {-# SPECIALIZE instance Show (HList '[ 'BOOL, 'LIST 'INT ]) #-}
   {-# SPECIALIZE instance Show (HList '[ 'INT, 'BOOL, 'LIST 'INT]) #-}
 }}}

 and it still only went one layer deep. One specialization didn't call
 another. (Examined with `-ddump-simpl` on `-O2`.) That's frustrating.

 About point (3): While it would be a bad idea to allow type families in
 normal instance heads, it seems sensible to allow them in `SPECIALIZE
 instance`. This is rather like allowing expressions (instead of, say, bare
 variables) on the LHS of rules.

 -------------------

 This ticket posting may be a little overly broad, but I'd love to know
 what others think about all of this. As we pick off the pieces that we
 decide are actually feasible, they should probably become separate
 tickets. But I think these are all of a piece and might benefit from some
 general thought about the whole `SPECIALIZE instance` pragma and how
 improvements here can make a big difference when we have dependent types.

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