| | 31 | |
| | 32 | = A proposed design = |
| | 33 | |
| | 34 | Here is a specification of the proposed user-level view of the design. |
| | 35 | |
| | 36 | A hole in a term is written `_?thing`. Example: |
| | 37 | {{{ |
| | 38 | test : List Bool |
| | 39 | test = Cons _?x (Cons _?x Nil) |
| | 40 | }}} |
| | 41 | If {{{-XHoles}}} is set, we want the following: |
| | 42 | 1. The program should be type-checked as if every hole {{{_?h}}} is replaced by {{{undefined}}}, except: |
| | 43 | * If type-checking would fail due to unsolved constraints that could be solved by giving a type to a hole. |
| | 44 | 1. If the program is well-typed, then: |
| | 45 | * The types of all holes should be reported. |
| | 46 | * Reporting the hole types should not cause type-checking (or compiling in general) to stop (in error). |
| | 47 | 1. (optional) If the program is ill-typed, then: |
| | 48 | * The types of all holes should be reported. |
| | 49 | |
| | 50 | The above should hold true with and without the monomorphism restriction. In particular, if an {{{undefined}}} somewhere in a program type-checked with the monomorphism restriction would cause type-checking to fail, then a hole in that same position should also cause type-checking to fail. |
| | 51 | |
| | 52 | The type of a hole should be the resolved type with minimum constraints. That is, the type of a hole should only have constraints that have not be solved but are either inferred from the context (e.g. {{{show _?h}}}) or given in a type annotation/signature (e.g. {{{_?h :: Show a => a}}}. |
| | 53 | --------------------------------- |
| | 54 | '''Stuff below here might be out of date; please edit''' |
