[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:  Unknown/Multiple  |            Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |               Test Case:
      Blocked By:                    |                Blocking:
 Related Tickets:                    |  Differential Revisions:
-------------------------------------+-------------------------------------

Comment (by jonsterling):

 Replying to [comment:26 DerekElkins]:
 > This is a fun one.  We can look at what some other systems do in similar
 situations.
 >
 > comment:17 talks about handling unevaluated terms and the discussion has
 been talking about partial functions.  One system that deals in this realm
 is Computational Type Theory (CTT), the type theory underlying NuPRL (and
 now JonPRL).  In NuPRL you can literally write the equivalent of:
 >
 > {{{#!hs
 > T Int = Bool
 > T   x = fix id
 > }}}

 thanks for the shoutout! I just thought I would clarify that, whilst in
 the past it was considered and perhaps experimented with, Nuprl does not
 currently have the ability to perform case analysis on types. (However,
 one of the principle reasons for types having an intensional equality in
 Nuprl rather than the standard extensional one is to not rule out the
 option of providing an eliminator to the universe in the future.)

 Anyway—with regard to partial operations, you are correct that it is not
 really a problem in Nuprl or JonPRL if a definition is partial; reduction
 is guided by the user in Nuprl. (By the way, contrary to oft-repeated
 mythology, it *is* safe to reduce terms in any context in CTT/ETT—this is
 guaranteed by the fact that computational equivalence is a congruence, a
 well-known result that comes from Howe.)

 It is *not* the case that for some function `f` and value `m`, `f(m)` is
 stuck (or worse, "canonical") if `f` is not defined at `m`; instead, it
 diverges. So viewing Haskell-style type families (whether open or closed)
 as functions or operations doesn't really work, though I believe that in
 many cases where a Haskell programmer reaches for a type family, they are
 really wanting a function/operation. I like your view of type families as
 generative in the same sense as data families, but quotiented by further
 axioms.

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