[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:13 rwbarton]:
 > Anyways, failure of what I have learned is called "the substitution
 lemma" is far more unintuitive to me

 If the substitution lemma doesn't hold, then (perhaps) FC, and by
 extension Haskell, is no longer type-safe. In other words, I don't believe
 that the type system is capable of ruling out `T Bool`, without major
 surgery. So, maybe we can report errors to the user if we see `T Bool` in
 source code, but if `T Bool` ends up sloshing around internally, GHC will
 respect it as a valid type.

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