Delay Errors Until Runtime

[atnnn]

I would like to add an -XDelayErrors flag to GHC that - changes most type errors into warnings - replaces the faulty expressions with runtime exceptions

This would make haskell development a lot easier. For example, this makes it possible to load buggy code into ghci to be able to execute it and show inferred types.

$ cat hello.lhs 
> main = putStr "Hello World" >> putStr ','

$ inplace/bin/ghc-stage2 --make hello -XDelayErrors
[1 of 1] Compiling Main             ( hello.lhs, hello.o )
Linking hello ...

$ ./hello 
Hello World
hello: hello.lhs:1:41:
    Couldn't match expected type `GHC.Base.String'
                with actual type `GHC.Types.Char'
    In the first argument of `System.IO.putStr', namely ','
    In the second argument of `(GHC.Base.>>)', namely
      System.IO.putStr ','
    In the expression:
      System.IO.putStr "Hello World" GHC.Base.>> System.IO.putStr ','

[atnnn]

proof of concept

[atnnn]

proof of concept (updated)

[atnnn]

It works in ghci too:

Prelude> :set -XDelayErrors
Prelude> head ['a', Nothing] == 'a'
True
Prelude> print "foo" >> print bar
"foo"
*** Exception: <interactive>:16:22: Not in scope: `bar'
Prelude> let f x = if x == 3 then 'a' else Nothing
Prelude> :t f
f :: (Eq a, Num a) => a -> Char
Prelude> f 3
'a'
Prelude> f 4
*** Exception: <interactive>:17:35:
    Couldn't match expected type `Char' with actual type `Maybe a0'
    In the expression: Nothing
    In the expression: if x == 3 then 'a' else Nothing
    In an equation for `f': f x = if x == 3 then 'a' else Nothing

My TODO list is:

• Add a new type of exception and use it instead of calling error

• Identify the compile-time warnings as such (they appear like errors)

• Use original code for pretty printing errors. ([1,2,'a'] gives "No instance for (Num Char) in the expression 1 in the expression [1, error "...", 'a'])

• Add some tests

I have successfully used this feature to develop it. It's great to be able to load code into into ghci and be able to use :t and :i even when errors are present.

[atnnn]

This fixes the problem described in #1896

[simonmar]

Great! We've talked about this idea before:  https://plus.google.com/107890464054636586545/posts/EbSuoRA6FTw

Let's call the flag -Ewarn, by analogy with -Werror. (It's a shame that -E is used for something unrelated, but I'm sure it's hardly ever used and there's no actual clash)

Simon and I will review the patch next week.

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

[simonmar]

I think I agree: the approach here is a clever hack, but will almost certainly lead to problems in the long run as we'll have to introduce special cases to fix the many quirks that will undoubtedly arise. It would be better to do it right, but doing it right means doing something special for every different kind of error (e.g. Simon's plan handles unification errors, but not renamer errors or parse errors).

I have more thoughts about this, but rather than pen a long message it's probably best if Simon and I talk about it next week.

[atnnn]

Thanks for the feedback. Your analysis of my proof of concept is correct.

* I don't really grok the types of findIn etc

findIn

(a -> b) -> a -> SrcSpan? -> Maybe (HsExpr? RdrName?, HsExpr? RdrName? -> b)

findIn is a zipper traversal of a subtree a in a root tree b. It returns when it finds an HsExpr? with the given SrcSpan?.

Most instances implement a more general findIn :: (a -> b) -> a -> Reader c d

* What if the SrcSpan? doesn't match exactly?

The error is left as-is and typechecking isn't retried.

* What happens if you have an error in a type signature, or a type declaration; then there is no obvious expression to replace.

Nothing currently happens, but the type of findIn can be generalised to find something else that HsExprs?.

But I'd like to tell you about my cunning plan.

it generates an equality constraint that looks like g :: ty2 ~ ty1

How is this different than using x itself as evidence that ty2 ~ ty1 and replacing x with bottom if not?

Moreover, the post-typechecked expression looks like (f (x |> g))

This seems to lead to a blowup (((f |> f'ev) (x |> x'ev)) |> f_x'ev), would it have an effect on performace? (If *'ev = id, it might even lead to #5621 :P)

IMHO this is rather elegant: precisely when the runtime execution needs evidence that ty1 = ty2, and no sooner, you'll get the error.

That's what I want.

Like, if f happens not to use its argument, you can run (f x) without getting the error.

This is the current behaviour.

I agree, my approach is a hack. It started as a bash/perl script that parsed the output of ghc.

If you are interested, I can help point you at the right places.

I would love to discuss more about this and other ideas better than mine and implement or adapt one of them.

Etienne Laurin

a Haskell programmer from Montreal

[simonpj@…]

commit 5508ada4b1d90ee54d92f69bbff7f66b3e8eceef

Author: Simon Peyton Jones <simonpj@microsoft.com>
Date:   Thu Jan 12 15:10:54 2012 +0000

    Implememt -fdefer-type-errors (Trac #5624)
    
    This patch implements the idea of deferring (most) type errors to
    runtime, instead emitting only a warning at compile time.  The
    basic idea is very simple:
    
     * The on-the-fly unifier in TcUnify never fails; instead if it
       gets stuck it emits a constraint.
    
     * The constraint solver tries to solve the constraints (and is
       entirely unchanged, hooray).
    
     * The remaining, unsolved constraints (if any) are passed to
       TcErrors.reportUnsolved.  With -fdefer-type-errors, instead of
       emitting an error message, TcErrors emits a warning, AND emits
       a binding for the constraint witness, binding it
       to (error "the error message"), via the new form of evidence
       TcEvidence.EvDelayedError.  So, when the program is run,
       when (and only when) that witness is needed, the program will
       crash with the exact same error message that would have been
       given at compile time.
    
    Simple really.  But, needless to say, the exercise forced me
    into some major refactoring.
    
     * TcErrors is almost entirely rewritten
    
     * EvVarX and WantedEvVar have gone away entirely
    
     * ErrUtils is changed a bit:
         * New Severity field in ErrMsg
         * Renamed the type Message to MsgDoc (this change
           touches a lot of files trivially)
    
     * One minor change is that in the constraint solver we try
       NOT to combine insoluble constraints, like Int~Bool, else
       all such type errors get combined together and result in
       only one error message!
    
     * I moved some definitions from TcSMonad to TcRnTypes,
       where they seem to belong more

 compiler/coreSyn/CoreLint.lhs      |   76 ++--
 compiler/deSugar/DsBinds.lhs       |    7 +-
 compiler/deSugar/DsMonad.lhs       |    5 +-
 compiler/ghci/Linker.lhs           |    4 +-
 compiler/hsSyn/Convert.lhs         |   20 +-
 compiler/iface/LoadIface.lhs       |   10 +-
 compiler/iface/MkIface.lhs         |    2 +-
 compiler/iface/TcIface.lhs         |    2 +-
 compiler/main/CmdLineParser.hs     |    3 +-
 compiler/main/DynFlags.hs          |   16 +-
 compiler/main/ErrUtils.lhs         |  157 ++++----
 compiler/main/ErrUtils.lhs-boot    |    4 +-
 compiler/main/HeaderInfo.hs        |    2 +-
 compiler/main/HscMain.hs           |    8 +-
 compiler/main/HscTypes.lhs         |    4 +-
 compiler/main/Packages.lhs         |    8 +-
 compiler/parser/Lexer.x            |    6 +-
 compiler/rename/RnEnv.lhs          |    4 +-
 compiler/rename/RnNames.lhs        |    6 +-
 compiler/simplCore/CoreMonad.lhs   |    2 +-
 compiler/stgSyn/StgLint.lhs        |   40 +-
 compiler/typecheck/Inst.lhs        |   60 +--
 compiler/typecheck/TcBinds.lhs     |    4 +-
 compiler/typecheck/TcCanonical.lhs |  106 +++--
 compiler/typecheck/TcDeriv.lhs     |   10 +-
 compiler/typecheck/TcErrors.lhs    |  876 +++++++++++++++++++++---------------
 compiler/typecheck/TcEvidence.lhs  |   19 +-
 compiler/typecheck/TcExpr.lhs      |    2 +-
 compiler/typecheck/TcForeign.lhs   |    4 +-
 compiler/typecheck/TcHsSyn.lhs     |    3 +
 compiler/typecheck/TcInteract.lhs  |   77 ++--
 compiler/typecheck/TcMType.lhs     |   13 +-
 compiler/typecheck/TcMatches.lhs   |   18 +
 compiler/typecheck/TcRnDriver.lhs  |    2 +-
 compiler/typecheck/TcRnMonad.lhs   |  149 ++++---
 compiler/typecheck/TcRnTypes.lhs   |  202 +++++----
 compiler/typecheck/TcSMonad.lhs    |   84 +----
 compiler/typecheck/TcSimplify.lhs  |  140 ++++--
 compiler/typecheck/TcSplice.lhs    |    8 +-
 compiler/typecheck/TcType.lhs      |   75 +++-
 compiler/typecheck/TcUnify.lhs     |  162 +++-----
 compiler/types/InstEnv.lhs         |    2 +-
 compiler/types/Unify.lhs           |    6 +-
 docs/users_guide/flags.xml         |   32 +-
 docs/users_guide/using.xml         |   26 ++
 45 files changed, 1340 insertions(+), 1126 deletions(-)

[simonpj]

Thank you for suggesting the idea. It's done!

Simon

[simonmar]

See also #5791.

[guest]

I might be doing something wrong, but does it work in GHCi? The ICFP paper says it does, the bug was fixed 7 months ago, but my month old version gives

$ ghci -fdefer-type-errors
GHCi, version 7.5.20120719: http://www.haskell.org/ghc/  :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
Prelude> fst (True, 'a' && False)

<interactive>:2:12:
    Couldn't match expected type `Bool' with actual type `Char'
    In the first argument of `(&&)', namely 'a'
    In the expression: 'a' && False
    In the first argument of `fst', namely `(True, 'a' && False)'

[simonpj]

This isn't documented (yet -- Paolo is going to add a short section to the user manual), but currently -fdefer-type-errors is switched off for "naked expressions" typed at the command prompt. Why? Because such expressions are typechecked, and then immediately evaluated. So if you said

ghci -fdefer-type-errors
Prelude> True && 'x'

you'd get a warning (from type checking) and an immediately-following error (when evaluating the expression):

Warning: Can't unify Bool and Char
Error: Can't unify Bool and Char

This is a bit stupid, and it's a very common case.

If you use a "statement" rather than an expression, you get deferred type errors, thus

Prelude> let v = True && 'x'
Warning: Can't unify Bool and Char
Prelude> v
Error: Can't unify Bool and Char

Does that make sense? Nothing deep here; it's just a user-interface issue. Yell if you think the behaviour should be different.

I'm re-opening the ticket for Paolo to add a short manual section.

Simon

[simonpj]

commit 3fabf48e0c5be2d7c2f6ea028115fdb9b4045d97
Author: Simon Peyton Jones <simonpj@microsoft.com>
Date:   Tue Aug 14 17:31:18 2012 +0100

    Document -fdefer-type-errors
    
    Thanks to Paolo for most of the work.

[pcapriotti]

Merged as 73057146115870578671ba8e5e50c2448bbbaa9e.