| | 5 | |
| | 6 | == Overview == |
| | 7 | While developing, sometimes it is desirable to allow compilation to succeed even |
| | 8 | if there are type errors in the code. Consider the following case: |
| | 9 | {{{ |
| | 10 | module Main where |
| | 11 | |
| | 12 | a :: Int |
| | 13 | a = 'a' |
| | 14 | |
| | 15 | main = print "b" |
| | 16 | }}} |
| | 17 | Even though `a` is ill-typed, it is not used in the end, so if all that we're |
| | 18 | interested in is `main` it is handy to be able to ignore the problems in `a`. |
| | 19 | |
| | 20 | Since we treat type equalities as evidence, this is relatively simple. Whenever |
| | 21 | we run into a type mismatch in TcUnify, we would normally just emit an error. But it |
| | 22 | is always safe to defer the mismatch to the main constraint solver. If we do |
| | 23 | that, `a` will get transformed into |
| | 24 | {{{ |
| | 25 | $co :: Int ~# Char |
| | 26 | $co = ... |
| | 27 | |
| | 28 | a :: Int |
| | 29 | a = 'a' `cast` $co |
| | 30 | }}} |
| | 31 | The constraint solver would realize that `co` is an insoluble constraint, and |
| | 32 | emit an error. But we can also replace the right-hand side |
| | 33 | of `co` with a runtime error call. This allows the program |
| | 34 | to compile, and it will run fine unless we evaluate `a`. Since coercions are |
| | 35 | unboxed they will be eagerly evaluated if used, so laziness will not "get on |
| | 36 | the way". |
| | 37 | |
| | 38 | == Implementation details == |
| | 39 | |
| | 40 | To do. |
