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

 I don't feel strongly how we come down on this one, but I want to note
 that making `T Bool` an error is a breaking change.

 It's easy enough to write a typing rule in Core that handles this:

 {{{
 F is a closed type family
 t is not apart from all equations in F
 F : [a:k1]. k2
 G |- t : k1
 -------------
 G |- F[t] : k2[a |-> t]
 }}}

 BUT, that rule doesn't obey the substitution lemma! Specifically, `T a`
 could be well-typed, but `T Bool` wouldn't be. This is No Good.

 I see this is as somewhat like the error for inaccessible code. Writing
 inaccessible code isn't actually erroneous -- we're just sure that users
 don't want to. Furthermore, with enough type-level trickery, users ''can''
 write provably inaccessible code that GHC isn't smart enough to flag. So,
 we could similarly try to flag and error on "weird beasts" on a best-
 effort basis, but this would probably have to be restricted to user-
 written types, missing Simon's case in comment:8.

 However, having just written that, I recall that, separately, I would love
 a way to disable the "inaccessible code" check. When I'm producing Haskell
 code programmatically (say, from Template Haskell), I sometimes produce
 inaccessible branches and have had to go to some lengths to avoid this. It
 would be nicer just to be able to ask GHC to accept these harmless chunks
 of code. In a similar vein, I can imagine some programatically-written
 Haskell that would contain weird beasts and wouldn't want failure. As I
 said above, though, I don't feel too strongly.

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