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

 Replying to [comment:28 jonsterling]:
 > Replying to [comment:26 DerekElkins]:
 >
 > > 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.)

 Yeah, in my reply on Richard Eisenberg's blog
 post,https://typesandkinds.wordpress.com/2015/09/09/what-are-type-
 families/, I explicitly introduce codes.  I don't ''think'' this really
 changes the picture.  (If this does, I'd like to know.  Specifically if
 viewing (closed) type families as functions on codes of types that get
 interpreted into functions on types misses something important due to
 being limited to codes.)

 > 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.

 I agree, in CTT `f(m)` is definitely not canonical and nothing like the
 generative view I suggested.  I mainly mentioned CTT as I think it
 provides an interesting perspective.  Frankly, the behavior Lennart is
 complaining about is the behavior I expected a priori.  My suggestion is
 essentially that codes for * are being quotiented.  The mention of HITs
 was simply because I still really want codes to be "inductive".  I go into
 this further on the above mentioned blog reply where I've also no doubt
 said at best imprecise things about CTT (though not they are not relevant
 to this approach.)

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