[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:12 augustss]:
 > To me saying that `T Bool` is OK because it's inaccessible is akin to
 saying that type incorrect expressions are OK as long as they are
 inaccessible.  After all, if you don't use them, they can't cause any
 harm.  But for expressions we have decided that this isn't acceptable.

 I actually would say that an inaccessible expression is ''always'' type-
 correct, because inaccessibility means that there is a proof of ''false''
 in the context, and thus anything is possible. But that's perhaps a story
 for another day.

 >
 > I guess making `T a` behave would require something like kind classes.

 It's a little worse than that, I think.

 Say `x :: Z`. In `show x`, we know `Z` must be in the `Show` class, and we
 also know that ''anything'' of type `Z` is a valid parameter to `show`.
 Thus, we have substitution, because substitution preserves types.

 But, in closed type families, we have a stranger situation: `T a` where `a
 :: *` is acceptable, but `T Bool` is not. I think kind classes (which can
 be kludged today) don't solve this problem.

 > But I'm not asking for the moon.  :)  I'd just like the compiler to tell
 me when it finds something that is clearly not going to work, like `T
 Bool`.  Exactly under what conditions and how it tells me, I don't care.

 This is certainly possible. It's just that the behavior around this
 feature won't be complete and might not be predictable in corner cases.

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