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

 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.

 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?

 Anyways, failure of what I have learned is called "the substitution lemma"
 is far more unintuitive to me than GHC allowing `T Bool` even though it is
 "floating" (my made-up word for type family applications that cannot be
 reduced (yet)) and GHC knows that it can never be reduced. But a warning,
 sure.

 > I guess making `T a` behave would require something like kind classes.
 We don't say that the expression `show x` is unconditionally type correct.
 It depends on the type of `x` belonging to the `Show` class.  In the same
 way, `T a` is not unconditionally type correct, it's only type correct if
 `a` is one of the types where `T` is well defined.

 Something like this would be great for other uses, too (imagine
 restricting the kind of the argument to `Set` to only allow types which
 are instances of `Ord`). But it sounds more like a research project than a
 bug report!

 > Until we have something like that I think you'll have to accept that the
 substitution lemma doesn't work.  You can pretend it works by saying `T
 Bool` is a type, if that makes you happier.  I just wonder which type it
 is. :)

 In the System FC translation it's an indeterminate type, sort of like the
 variable "x" in a ring of polynomials. I can do algebra on polynomials
 without ever asking which number "x" is.

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