| 1 | {-# OPTIONS_GHC -fglasgow-exts -O1 #-} |
|---|
| 2 | |
|---|
| 3 | module Main where |
|---|
| 4 | |
|---|
| 5 | --{-# RULES "rule1" forall x. to (from x) = x #-} |
|---|
| 6 | {-# RULES "rule2" forall x. from (to x) = x #-} |
|---|
| 7 | |
|---|
| 8 | class EP a where |
|---|
| 9 | type Result a |
|---|
| 10 | from :: a -> Result a |
|---|
| 11 | to :: Result a -> a |
|---|
| 12 | |
|---|
| 13 | {- -- Uncommenting rule1 above gives the error: |
|---|
| 14 | Couldn't match expected type `Result a' |
|---|
| 15 | against inferred type `Result a' |
|---|
| 16 | NB: `Result' is a type function, and may not be injective |
|---|
| 17 | In the first argument of `to', namely `(from x)' |
|---|
| 18 | In the expression: to (from x) |
|---|
| 19 | When checking the transformation rule "rule1" |
|---|
| 20 | -} |
|---|
| 21 | |
|---|
| 22 | -- However, this is fine |
|---|
| 23 | {-# RULES "rule3" forall x. to' (from' x) = x #-} |
|---|
| 24 | {-# RULES "rule4" forall x. from' (to' x) = x #-} |
|---|
| 25 | |
|---|
| 26 | class EP' a b | a -> b where |
|---|
| 27 | from' :: a -> b |
|---|
| 28 | to' :: b -> a |
|---|
| 29 | |
|---|
| 30 | main = print "" |
|---|