| 20 | | 0. To move GADT type checking from refinements to using equalities, proceed as follows (as suggested by SPJ): |
| 21 | | * In `TcPat.tcConPat`: |
| 22 | | * set `eq_spec' = []`, to get an empty refinement |
| 23 | | * add the equalities from `eq_spec` to `theta'` (to propagate them instead of the refinement) |
| 24 | | * Test whether this works (it basically disables the refinement mechanism without deleting it) |
| | 20 | 0. To move GADT type checking from refinements to equalities, proceed as follows (as suggested by SPJ): |
| | 21 | * Implemented this as follows in `TcPat.tcConPat:579:` |
| | 22 | {{{ |
| | 23 | - eq_spec' = substEqSpec tenv eq_spec |
| | 24 | + eq_spec' = [] |
| | 25 | + eq_preds = [mkEqPred (mkTyVarTy tv, ty) | (tv, ty) <- eq_spec] |
| | 26 | + theta' = substTheta tenv (eq_theta ++ dict_theta ++ eq_preds) |
| | 27 | }}} |
| | 28 | * Results: |
| | 29 | * Works in principle. |
| | 30 | * Immediately fixes the tests GADT3, GADT4 & GADT5. |
| | 31 | * Unfortunately, it breaks a whole lot of tests in `gadt/`. |
| | 32 | * The remaining problems are partially due to (1) the splitBoxyXXX function issue mentioned above, (2) the occurs check issue mentioned below, (3) the same problem exhibited by GADT9 (with or without this change), (4) some problems getting hold of the right given class constraints, and (5) some random stuff that I haven't looked at more closely. |
