[GHC] #9636: Function with type error accepted

[GHC]

#9636: Function with type error accepted
-------------------------------------+-------------------------------------
              Reporter:  augustss    |            Owner:
                  Type:  bug         |           Status:  new
              Priority:  normal      |        Milestone:
             Component:  Compiler    |          Version:  7.8.3
            Resolution:              |         Keywords:
      Operating System:              |     Architecture:  Unknown/Multiple
  Unknown/Multiple                   |       Difficulty:  Unknown
       Type of failure:              |       Blocked By:
  None/Unknown                       |  Related Tickets:
             Test Case:              |
              Blocking:              |
Differential Revisions:              |
-------------------------------------+-------------------------------------

Comment (by augustss):

 Replying to [comment:13 rwbarton]:
 > Isn't it analogous to saying that incomplete pattern matches are OK as
 long as they are inaccessible? (Which they are.) After all, like you said,
 a closed type family is like a function on types. The type expression `T
 Bool` has no normal form, for sure, but who says we have to evaluate it?

 Yes, it's a lot like a pattern match failure.  So let us go with that
 analogy for a moment.
 Assume we have these definitions:

 {{{#!hs
 foo :: Int -> Int
 foo 0 = 42

 bar = foo 5 - foo 5
 }}}

 Since we know that `x - x = 0` it is tempting to optimize the definition
 of `bar` to `bar = 0`.  This is, of course, wrong since computing `foo 5`
 will result in bottom.

 Now compare this to what the type checker does in my original example.  It
 happily assumes that `T Bool` is equal to `T Bool`, but that's wrong.  `T
 Bool` is bottom at type checking time and should be reported as such.

 I've decided I'm OK with having `T Bool` just floating around in the same
 way that I'm OK with having `foo 5` floating around in a lazy language.
 Type families introduce partial functions on the type level, and I think
 this has to be dealt with.  Type expressions can now blow up during type
 checking.  So at the points when a (closed) type family expression has to
 be evaluated, e.g., for equality comparison, and it cannot be reduced then
 this should be an error.  IMHO.

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