| 206 | |
| 207 | == Semantics == |
| 208 | |
| 209 | It might seem tempting to just define pattern synonym semantics as 'textual substitution'. On the other hand, just like with any other surface language feature, we don't want to normalize away pattern synonyms before typechecking happens, since we want to report type error occurrences from user-written code. |
| 210 | |
| 211 | |
| 212 | These two goals are incompatible once you start to factor in patterns containing typeclass-polymorphic parts. For example, let's say we have these two GADTs: |
| 213 | |
| 214 | {{{ |
| 215 | data S a where |
| 216 | MkS:: Num a -> a > S a |
| 217 | data T a where |
| 218 | MkT :: Eq a => a -> T a |
| 219 | }}} |
| 220 | |
| 221 | and we define this pattern synonym: |
| 222 | |
| 223 | {{{ |
| 224 | pattern P :: (Eq a, Num a) => a -> a -> (P a, S a) |
| 225 | pattern P x y = (MkT x, MkS y) |
| 226 | }}} |
| 227 | |
| 228 | we can then write a function: |
| 229 | |
| 230 | {{{ |
| 231 | f (P 1 2) = ... |
| 232 | }}} |
| 233 | |
| 234 | which needs to use `fromInteger` from the `Num` instance provided by the `MkS` constructor to be able to pattern-match on the argument of the `MkT` constructor. |
| 235 | |
| 236 | This means when we desugar a pattern synonym occurrence, the whole of the right-hand side needs to be matched before the arguments are matched. So the previous definition of `f` is desugared corresponding to the following Haskell code: |
| 237 | |
| 238 | {{{ |
| 239 | f = \a -> case a of |
| 240 | (MkT x, MkS y) -> case x of |
| 241 | 1 -> case y of |
| 242 | 2 -> ... |
| 243 | }}} |
| 244 | |
| 245 | Of course, we don't actually generate Haskell code for that; instead, the implementation directly emits Core, in the same way Core is emitted for other pattern matchings (in `DsUtils.mkCoAlgCaseMatchResult`) |