[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:17 goldfire]:
 > 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.

 I'm saying it's neither equal to itself, nor unequal to itself.  `T Bool`
 is in some sense ill formed, so asking if it's equal to itself is
 nonsensical, because it's not a a type.  Can you use reflexivity to
 conclude `Int Bool ~ Int Bool`?  No, because it's an ill-formed typed.
 The case with `T Bool` is not as severely ill form, though.

 If you want to keep `T Bool` you have to have a different explanation what
 makes a type.  Types a made from `data`, `newtype`, and `type family`.
 But for `type family` certain of the the types are actually equal to other
 existing types.  But if no equation holds then it's a new (empty) type,
 distinct from all other types.  I can go along with that explanation, but
 it's not very satisfactory to me.

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