[GHC] #8828: allow fully applied type families in instance heads

[GHC]

#8828: allow fully applied type families in instance heads
-------------------------------------+------------------------------------
        Reporter:  aavogt            |            Owner:  goldfire
            Type:  feature request   |           Status:  new
        Priority:  normal            |        Milestone:
       Component:  Compiler          |          Version:  7.6.2
      Resolution:                    |         Keywords:
Operating System:  Unknown/Multiple  |     Architecture:  Unknown/Multiple
 Type of failure:  None/Unknown      |       Difficulty:  Unknown
       Test Case:                    |       Blocked By:
        Blocking:                    |  Related Tickets:
-------------------------------------+------------------------------------

Comment (by goldfire):

 I've thought about this ticket some, and I think implementing this idea is
 a move in the wrong direction.

 Implementing this idea feels quite like allowing function applications in
 patterns. For example, how would we feel about this:

 {{{
 foo :: Bool -> Int
 foo True = 1
 foo (not True) = -1
 }}}

 With some engineering, there is no reason that we couldn't accept a
 definition such as the one above. After all, `not True` is fully applied
 to constants and can be reduced to `False`. We can pretend that there is a
 TH-like stage restriction (somewhat like Simon's quite valid dependency
 concerns in comment:1) to prevent infinite regress. We can even check to
 make sure that the pattern match is complete. Yet, this definition smells
 like rotten eggs to me.

 Should it be different at the type level? I, personally, think not.

 What it seems we really want here are ''type pattern synonyms''. Pattern
 synonyms allow a richer syntax "on the left of an `=`", which is what we
 want here in types. It so happens that, currently, type patterns are
 syntactically just types that don't mention type families, but if we
 separate out a type pattern syntax from a type syntax (which I think is a
 good idea -- they are different!) then the idea of type families "on the
 left" becomes even more suspicious and type pattern synonyms make more
 sense.

 So, instead of implementing the idea proposed here, I would rather think
 about type pattern synonyms. How are these related to term pattern
 synonyms? How would we declare them? Can they be promoted to kinds? etc.

 What do others think here?

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