125 | | * Treat equality evidence just like any other sort of evidence. |
126 | | * A coercion variable is an `Id`, not a `TyVar`. |
127 | | * A coercion is an `CoreExpr` whose type is `(s ~ t)` or |
128 | | * A function can reu |
| 127 | * A coercion is an `CoreExpr`, of form `Coercion g`, whose type is `(s ~ t)`, of form `PredTy (EqPred s t)`. |
| 128 | |
| 129 | * Unlike type applications, coercion applications are not required to have a `(Coercion g)` as the argument. For example, suppose we have |
| 130 | {{{ |
| 131 | f :: forall a. (a~Int) => a -> Int |
| 132 | id :: forall b. b->b |
| 133 | c :: x~Int |
| 134 | }}} |
| 135 | Then the term `(f x (id (x~Int) c))` would be fine. Notice that the coercion argument is an appplication of the identity function. (Yes it's a bit contrived.) In `CoreExpr` form it would look like: |
| 136 | {{{ |
| 137 | App (App (Var f) (Type x)) |
| 138 | (App (App (Var id) (Type (PredTy (EqPred x Int)))) |
| 139 | (Var c)) |
| 140 | }}} |
| 141 | |
| 142 | * Similarly a let-binding can bind a coercion |
| 143 | {{{ |
| 144 | Let (NonRec c (...a coercion-valued term..)) (...body...) |
| 145 | }}} |
| 146 | |
| 147 | * Coercion application is call-by value. Ditto let-bindings. You must have the evidence before calling the function. |
| 148 | |
| 149 | * So it doesn't make sense to have recursive coercion bindings. |
| 150 | |
| 151 | * If we see `Let (NonRec c (Coercion g)) e` we can substitute `(Coercion g)` for any term-level occurrences of `c` in the term `e`, and `g` for `c` in any occurrences of `c` in coercions inside `e`. (This seems a bit messy.) |