[GHC] #8155: Defaulting bug or unfortunate error message with closed type families

[GHC]

#8155: Defaulting bug or unfortunate error message with closed type families
-------------------------------------+------------------------------------
        Reporter:  nh2               |            Owner:
            Type:  bug               |           Status:  closed
        Priority:  normal            |        Milestone:
       Component:  Compiler          |          Version:  7.6.3
      Resolution:  invalid           |         Keywords:
Operating System:  Unknown/Multiple  |     Architecture:  Unknown/Multiple
 Type of failure:  None/Unknown      |       Difficulty:  Unknown
       Test Case:                    |       Blocked By:
        Blocking:                    |  Related Tickets:
-------------------------------------+------------------------------------
Changes (by goldfire):

 * status:  new => closed
 * resolution:   => invalid


Comment:

 This may be an infelicity in defaulting (which I'm not terribly familiar
 with), but the closed-type-family behavior is correct, if rather subtle
 and confusing.

 The original post says "clearly `BoundsOf (a -> a) ~ Integer` (you just
 wrote that down)". I would say that that's not exactly what was written.
 What the closed-type-family definition of `BoundsOf` says is that
 `BoundsOf (a -> a) ~ Integer` as long as `a` is most assuredly '''not'''
 `a -> a`. That is, GHC must be sure that previous equations of a closed
 type family can never apply before using a given equation. Because it is
 quite possible that `a` will be instantiated at a type such that `a`
 '''does''' equal `a -> a` (see below), GHC will not use the second
 equation to simplify `BoundsOf (a -> a)`.

 The dangerous type that `a` might be instantiated with is

 {{{
 type family Looper b
 type instance Looper b = Looper b -> Looper b
 }}}

 So, unless GHC knows that `a` won't be instantiated at a type like
 `Looper`, the second equation will not be used. As a concrete example of
 this, GHC will happily reduce `BoundsOf (Bool -> Bool)`.

 This is all very subtle and can be unexpected, but after lots and lots of
 thinking, Simon PJ, Dimitrios V, and I could not come up with a better way
 here. When I wrote a suggested implementation of `BoundsOf` in my response
 to #8154, I thought a little while about the ordering of the equations to
 avoid exactly this problem.

 I will close this ticket, but do please reopen if you can characterize the
 bug as a specific infelicity in the defaulting mechanism.

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