GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2019-07-07T19:07:44Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/2600Bind type variables in RULES2019-07-07T19:07:44ZSimon Peyton JonesBind type variables in RULESRoman writes: here's an example I came across while working on the recycling paper
and which I subsequently forgot about. Suppose we have:
```
{-# LANGUAGE Rank2Types #-}
module T where
class T t where
to :: [a] -> t a
from :: t a -> [a]
tmap :: (a -> a) -> t a -> t a
{-# RULES
"myrule" forall f x.
from (tmap f (to x)) = map f (from (to x))
#-}
```
Alas, this fails with:
```
Ambiguous type variable `t' in the constraint:
`T t' arising from a use of `to' at T.hs:12:40-43
Probable fix: add a type signature that fixes these type variable(s)
```
Of course, I'd like the t on the rhs to be the same as on the lhs but
I don't see how to tell this to GHC. Is it actually possible? The only
solution I've found was to add a dummy argument to 'to':
```
to' :: t a -> [a] -> t a
to = to' undefined
{-# RULES
"myrule" forall f t x.
from (tmap f (to' t x)) = map f (from (to' t x))
#-}
```
That's ugly, of course. Am I missing something or is this just
impossible to do with the current system?
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | -------------- |
| Version | 6.8.3 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | Unknown |
| Architecture | Unknown |
</details>
<!-- {"blocked_by":[],"summary":"Bind type variables in RULES","status":"New","operating_system":"Unknown","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"6.8.3","keywords":[],"differentials":[],"test_case":"","architecture":"Unknown","cc":[""],"type":"FeatureRequest","description":"Roman writes: here's an example I came across while working on the recycling paper\r\nand which I subsequently forgot about. Suppose we have:\r\n{{{\r\n{-# LANGUAGE Rank2Types #-}\r\nmodule T where\r\n\r\nclass T t where\r\n to :: [a] -> t a\r\n from :: t a -> [a]\r\n tmap :: (a -> a) -> t a -> t a\r\n\r\n{-# RULES\r\n\r\n\"myrule\" forall f x.\r\n from (tmap f (to x)) = map f (from (to x))\r\n #-}\r\n}}}\r\nAlas, this fails with:\r\n{{{\r\n Ambiguous type variable `t' in the constraint:\r\n `T t' arising from a use of `to' at T.hs:12:40-43\r\n Probable fix: add a type signature that fixes these type variable(s)\r\n}}}\r\nOf course, I'd like the t on the rhs to be the same as on the lhs but\r\nI don't see how to tell this to GHC. Is it actually possible? The only\r\nsolution I've found was to add a dummy argument to 'to':\r\n{{{\r\nto' :: t a -> [a] -> t a\r\n\r\nto = to' undefined\r\n\r\n{-# RULES\r\n\r\n\"myrule\" forall f t x.\r\n from (tmap f (to' t x)) = map f (from (to' t x))\r\n #-}\r\n}}}\r\nThat's ugly, of course. Am I missing something or is this just\r\nimpossible to do with the current system?\r\n","type_of_failure":"OtherFailure","blocking":[]} -->Roman writes: here's an example I came across while working on the recycling paper
and which I subsequently forgot about. Suppose we have:
```
{-# LANGUAGE Rank2Types #-}
module T where
class T t where
to :: [a] -> t a
from :: t a -> [a]
tmap :: (a -> a) -> t a -> t a
{-# RULES
"myrule" forall f x.
from (tmap f (to x)) = map f (from (to x))
#-}
```
Alas, this fails with:
```
Ambiguous type variable `t' in the constraint:
`T t' arising from a use of `to' at T.hs:12:40-43
Probable fix: add a type signature that fixes these type variable(s)
```
Of course, I'd like the t on the rhs to be the same as on the lhs but
I don't see how to tell this to GHC. Is it actually possible? The only
solution I've found was to add a dummy argument to 'to':
```
to' :: t a -> [a] -> t a
to = to' undefined
{-# RULES
"myrule" forall f t x.
from (tmap f (to' t x)) = map f (from (to' t x))
#-}
```
That's ugly, of course. Am I missing something or is this just
impossible to do with the current system?
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | -------------- |
| Version | 6.8.3 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | Unknown |
| Architecture | Unknown |
</details>
<!-- {"blocked_by":[],"summary":"Bind type variables in RULES","status":"New","operating_system":"Unknown","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"6.8.3","keywords":[],"differentials":[],"test_case":"","architecture":"Unknown","cc":[""],"type":"FeatureRequest","description":"Roman writes: here's an example I came across while working on the recycling paper\r\nand which I subsequently forgot about. Suppose we have:\r\n{{{\r\n{-# LANGUAGE Rank2Types #-}\r\nmodule T where\r\n\r\nclass T t where\r\n to :: [a] -> t a\r\n from :: t a -> [a]\r\n tmap :: (a -> a) -> t a -> t a\r\n\r\n{-# RULES\r\n\r\n\"myrule\" forall f x.\r\n from (tmap f (to x)) = map f (from (to x))\r\n #-}\r\n}}}\r\nAlas, this fails with:\r\n{{{\r\n Ambiguous type variable `t' in the constraint:\r\n `T t' arising from a use of `to' at T.hs:12:40-43\r\n Probable fix: add a type signature that fixes these type variable(s)\r\n}}}\r\nOf course, I'd like the t on the rhs to be the same as on the lhs but\r\nI don't see how to tell this to GHC. Is it actually possible? The only\r\nsolution I've found was to add a dummy argument to 'to':\r\n{{{\r\nto' :: t a -> [a] -> t a\r\n\r\nto = to' undefined\r\n\r\n{-# RULES\r\n\r\n\"myrule\" forall f t x.\r\n from (tmap f (to' t x)) = map f (from (to' t x))\r\n #-}\r\n}}}\r\nThat's ugly, of course. Am I missing something or is this just\r\nimpossible to do with the current system?\r\n","type_of_failure":"OtherFailure","blocking":[]} -->8.8.1Simon Peyton JonesSimon Peyton Jones