Version 3 (modified by dreixel, 6 years ago) (diff)


Deferring compilation type errors to runtime

This page describes the -fwarn-type-errors flag, currently implemented in the ghc branch ghc-defer.


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

Implementation details

To do.