[GHC] #5624: Delay Errors Until Runtime

[GHC]

#5624: Delay Errors Until Runtime
---------------------------------+------------------------------------------
    Reporter:  atnnn             |        Owner:  atnnn       
        Type:  feature request   |       Status:  new         
    Priority:  high              |    Milestone:  7.6.1       
   Component:  Compiler          |      Version:  7.3         
    Keywords:                    |     Testcase:              
   Blockedby:                    |   Difficulty:              
          Os:  Unknown/Multiple  |     Blocking:              
Architecture:  Unknown/Multiple  |      Failure:  None/Unknown
---------------------------------+------------------------------------------

Comment(by simonpj):

 Good work `atnnn`.  I wonder who you really are?  People have asked me
 about this, and I had a cunning plan, but I never thought of your
 approach.  So far as I can see, your plan is:
  1. Typecheck the program
  2. For each error message,
     * Take the `SrcSpan` of each error
     * Find a sub-expression (of type `HsExpr`) ''in the original input
 program'' that has (exactly?) that `SrcSpan`
     * Replace it with `error "...the message..."`
  3. Repeat from step 1 with the transformed program

 You have a conter to stop an infinite loop in this procedure.

 Assuming I'm right there are lots of details I don't understand.
  * I don't really grok the types of `findIn` etc
  * What if the `SrcSpan` doesn't match exactly?
  * What happens if you have an error in a type signature, or a type
 declaration; then there is no obvious expression to replace.

 What I like about your approach is that it's brutally simple and direct.
 But I'd like to tell you about my cunning plan.  Here's how it goes.

 When the typechecker looks at, say,
 {{{
   (f x)

 where    f :: ty1 -> Int
          x :: ty2
 }}}
 it generate an ''equality constraint'' that looks like
 {{{
   g :: ty2 ~ ty1
 }}}
 Moreover, the post-typechecked expression looks like
 {{{
   (f (x |> g))
 }}}
 That is, the argument `x` is cast by the ''evidence'' `g`, which converts
 a value of type `ty2` to a value of type `ty2`.  Later on, the typechecker
 solves the constraint, and create a binding for `g`, somthing like
 {{{
   g = Refl ty
 }}}
 The point is this.  If `ty1` turns out to be different to `ty2` (say they
 turn out to be `Int` and `Bool`), then today the typecheck emits an error
 message. But it'd be rather easy to make it emit a binding
 {{{
   g = error "...the error message..."
 }}}
 IMHO this is rather elegant: '''precisely when the runtime execution needs
 evidence that `ty1` = `ty2`, and no sooner,  you'll get the error'''.
 Like, if `f` happens not to use its argument, you can run `(f x)` without
 getting the error.

 Moreover, failing type-class constraints work just the same way.

 I think this is the Right Way to solve your problem.  If you are
 interested, I can help point you at the right places.

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