[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 goldfire):

 Replying to [comment:16 augustss]:
 >  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.

 Unfortunately, this, too, violates the substitution lemma. We probably
 want to be able to solve `(a ~ a)` with reflexivity, for ''any'' `a`. But,
 you're suggesting that a particular value for `a`, namely `T Bool`, will
 ''not'' equal itself.

 The difference between types and terms here is that we need to be able to
 reason about unevaluated types, such as `a`. We never need this ability on
 terms, so the existing term-level semantics works out just fine.

 To be clear, I'm saying that issuing an error/warning in the case of a
 user-written strange beast seems quite easy to implement. Any suggestion
 beyond that made here seems like a stretch, though. Do keep suggesting,
 though -- perhaps we'll find something that works in here.

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