#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