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

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

 Obviously NuPRL doesn't loop forever when it encounters T Bool.  It will
 do some computation to see if it can decide the proposition, but if it
 can't it gives up and makes it a proof obligation that the user must
 discharge.  Since CTT is based on partial equivalence relations, T Bool ~
 T Bool presents no problem.  Reflexivity is not given, so that's a
 statement that needs to be proven.  Indeed, typing Lennart's f from the
 bug report, requires, as usual, deriving that T Bool :: * and in CTT this
 is by definition T Bool ~ T Bool.  Clearly GHC has evidence allowing it to
 automatically show the proof obligation is not achievable in this case.
 Thus the analogous situation in CTT would be a type error.

 In comment:19 Lennart mentions that we still have logic programming at the
 type level.  One way of interpreting this is to give (closed) type
 families Curry's semantics, i.e. narrowing, but restricted to functional
 relations, so no (truly) overlapping patterns.  This would be a language
 where a function returns at most one result rather than exactly one result
 as in a functional language.  Still, T Bool would narrow the result set to
 the empty set and thus be a type error.

 Alternatively, Lennart may have just been referring to working with
 uninterpreted functions, something commonly done in logic programming, but
 in no way restricted to logic programming.  Of course, T isn't an
 uninterpreted function, T Int ~ Bool.  We could say it's a quotient of a
 type of uninterpreted functions modulo the relation T Int ~ Bool.  We can
 push this idea a little.  If someone wants to play with the current
 behavior in a more explicit manner all one needs to do is open up Agda and
 type:
 {{{#!hs
 import Level

 data Unit : Set where U : Unit
 data Bool : Set where True : Bool; False : Bool

 data _==_ {l}{A : Set l} (a : A) : A -> Set l where
     refl :  a == a

 subst : {l : Level.Level}{A B : Set l} -> (A == B) -> A -> B
 subst refl x = x

 postulate T : Set -> Set
 postulate T_Bool_is_Unit : T Bool == Unit

 f : T Unit -> Bool
 f _ = True

 g : T Bool -> Unit
 g x = subst T_Bool_is_Unit x

 h : T Bool == T Bool -> Unit
 h refl = U
 }}}
 To handle overlapping, explicit inequality evidence needs to be provided.
 This suggests that like we can view a data declaration as adding a
 constructor to (codes for) *.  A type family could be viewed into making
 that data type a higher inductive type (from Homotopy Type Theory).

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