Deferring compilation type errors to runtime

This page describes the -fdefer-type-errors flag that was added in GHC 7.6.1. Ticket #5624 (closed) tracks this feature request.

For more information, see the associated Equality Proofs and Deferred Type Errors (ICFP'12).

Tickets

See the deferred type errors label.

Overview

While developing, sometimes it is desirable to allow compilation to succeed even if there are type errors in the code. Consider the following case:

module Main where

a :: Int
a = 'a'

main = print "b"

Even though a is ill-typed, it is not used in the end, so if all that we're interested in is main it is handy to be able to ignore the problems in a.

Since we treat type equalities as evidence, this is relatively simple. Whenever we run into a type mismatch in TcUnify, we would normally just emit an error. But it is always safe to defer the mismatch to the main constraint solver. If we do that, a will get transformed into

$co :: Int ~# Char
$co = ...

a :: Int
a = 'a' `cast` $co

The constraint solver would realize that co is an insoluble constraint, and emit an error. But we can also replace the right-hand side of co with a runtime error call. This allows the program to compile, and it will run fine unless we evaluate a. Since coercions are unboxed they will be eagerly evaluated if used, so laziness will not "get on the way".

Example

Here's an example of all sorts of errors that can be deferred:

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# OPTIONS_GHC -fdefer-type-errors #-}

module Main where

t5624 :: IO ()
t5624 = putStr "Hello World" >> putStr ','

a :: Int
a = 'p'

data B = B
b :: B -> Bool
b x = x == x

data C a where
  C1 :: C Int
  C2 :: Bool -> C Bool

c :: C Int -> Bool
c (C2 x) = True

d :: a -> a
d = 1

e = 'p'
f = e 'q'

h :: a -> (Char,Char) 
h x = (x,'c')

data T a where 
  K  :: a -> T a

i a = seq (not (K a)) ()

class MyClass a where myOp :: a -> String

j = myOp 23 -- Two errors, should not combine them

k :: (Int ~ Bool) => Int -> Bool
k x = x

l :: IO ()
l = putChar >> putChar 'p'


main :: IO ()
main = print "No errors!"

This module compiles and runs!

Implementation details

The first step is to make sure that TcUnify does not ever fail with a type error; instead, we call uType_defer to defer the unification to the constraint solver.

In the constraint solver, we call reportUnsolved with any remaining unsolved constraints. At this stage, if we are not deferring errors, we simply make the errors for each unsolved constraint and throw them. If we are deferring errors, we make the errors for each constraint and then set the evidence binder of each unsolved constraint to be a runtime error that emits the type error message we just created. This is done by reportTidyWanteds and deferCt in typecheck/TcErrors. Note that reportTidyWanteds has some shuffling to do, because when we are not deferring errors we group certain errors, or we don't report all the errors. But when we are deferring we really want to have (at least) one error for every coercion.

Error messages

For simplicity, we defer errors from TcUnify to the constraint solver even if -fdefer-type-errors is not on; in that case, we will simply fail in the constraint solver, rather than directly in the unifier.

This means that some type error messages change, even without -fdefer-type-errors. In particular, many tests from the testsuite need to have their output adapted.

Kind errors

Currently we cannot defer kind errors because we do not create coercions for kind equalities. This might change in the near future, though, in which case we could use the same strategy to defer kind errors to runtime.