[GHC] #13262: Allow type synonym family application in instance head if it reduces away

[GHC]

#13262: Allow type synonym family application in instance head if it reduces away
-------------------------------------+-------------------------------------
        Reporter:  ezyang            |                Owner:  (none)
            Type:  feature request   |               Status:  new
        Priority:  low               |            Milestone:
       Component:  Compiler (Type    |              Version:  8.0.1
  checker)                           |
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by ezyang):

 * priority:  lowest => low


Comment:

 Actually, I realized that something stronger would be OK here: it's OK for
 a type family synonym to occur in an instance, even if it doesn't reduce
 away, AS LONG AS the expression has no free variables.

 This is pretty useless for normal programmers but actually it is pretty
 useful in Backpack. Consider:

 {{{
 -- there's some type family F a :: * -> *
 data T
 instance Monad (F T) where ...
 }}}

 This is something that I'd really quite like to write in a signature,
 because what I am saying is that there is some existing type family F, and
 whatever it is the abstract type you picked, F T better reduce to a monad.
 Yes I could replace the type family with another abstract type for the
 monad, but if I want Backpack and the type family to coexist, I get better
 backwards compatibility by reusing the type family.

 The analogy is how we handle type families in constraints:

 {{{
 f :: Monad (F a) => ....
 }}}

 This is OK because `a` is a skolem variable, so we aren't ever going to
 instantiate it to some variable while we're typechecking the body of f.
 What would be wrong, and is impossible to write in Haskell's type language
 today, is `f :: (forall a. Monad (F a)) => ...`!

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