GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2020-08-19T17:35:02Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/15050ScopedTypeVariables could allow more programs2020-08-19T17:35:02ZJoachim Breitnermail@joachim-breitner.deScopedTypeVariables could allow more programsConsider
```
data P a = P
data T1 a where
MkT1 :: forall a. P a -> T1 a
MkT2 :: forall a. P a -> T1 (a,a)
MkT3 :: forall a b. b ~ Int => P a -> P b -> T1 a
MkT4 :: forall a b. P a -> P b -> T1 a
MkT5 :: forall a b c. b ~ c => P a -> P b -> P c -> T1 a
```
I can write this function
```
foo :: T1 (Int, Int) -> ()
foo (MkT1 (P::P (Int,Int))) = ()
foo (MkT2 (P::P x)) = (() :: x ~ Int => ())
foo (MkT3 P (P::P Int)) = ()
foo (MkT4 P (P::P b)) = ()
foo (MkT5 P (P::P b) (P::P b)) = ()
```
but this these two equations fail
```
foo (MkT1 (P::P (Int,x))) = (() :: x ~ Int => ())
foo (MkT1 (P::P x)) = (() :: x ~ (Int,Int) => ())
```
I am especially surprised by the second one, given that the very similar equation with `MkT2` works.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | -------------- |
| Version | 8.4.1 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"ScopedTypeVariables could allow more programs","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Consider\r\n{{{\r\ndata P a = P\r\ndata T1 a where\r\n MkT1 :: forall a. P a -> T1 a\r\n MkT2 :: forall a. P a -> T1 (a,a)\r\n MkT3 :: forall a b. b ~ Int => P a -> P b -> T1 a\r\n MkT4 :: forall a b. P a -> P b -> T1 a\r\n MkT5 :: forall a b c. b ~ c => P a -> P b -> P c -> T1 a\r\n}}}\r\n\r\nI can write this function\r\n{{{\r\nfoo :: T1 (Int, Int) -> ()\r\nfoo (MkT1 (P::P (Int,Int))) = ()\r\nfoo (MkT2 (P::P x)) = (() :: x ~ Int => ())\r\nfoo (MkT3 P (P::P Int)) = ()\r\nfoo (MkT4 P (P::P b)) = ()\r\nfoo (MkT5 P (P::P b) (P::P b)) = ()\r\n}}}\r\nbut this these two equations fail\r\n{{{\r\nfoo (MkT1 (P::P (Int,x))) = (() :: x ~ Int => ())\r\nfoo (MkT1 (P::P x)) = (() :: x ~ (Int,Int) => ())\r\n}}}\r\n\r\nI am especially surprised by the second one, given that the very similar equation with `MkT2` works.","type_of_failure":"OtherFailure","blocking":[]} -->Consider
```
data P a = P
data T1 a where
MkT1 :: forall a. P a -> T1 a
MkT2 :: forall a. P a -> T1 (a,a)
MkT3 :: forall a b. b ~ Int => P a -> P b -> T1 a
MkT4 :: forall a b. P a -> P b -> T1 a
MkT5 :: forall a b c. b ~ c => P a -> P b -> P c -> T1 a
```
I can write this function
```
foo :: T1 (Int, Int) -> ()
foo (MkT1 (P::P (Int,Int))) = ()
foo (MkT2 (P::P x)) = (() :: x ~ Int => ())
foo (MkT3 P (P::P Int)) = ()
foo (MkT4 P (P::P b)) = ()
foo (MkT5 P (P::P b) (P::P b)) = ()
```
but this these two equations fail
```
foo (MkT1 (P::P (Int,x))) = (() :: x ~ Int => ())
foo (MkT1 (P::P x)) = (() :: x ~ (Int,Int) => ())
```
I am especially surprised by the second one, given that the very similar equation with `MkT2` works.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | -------------- |
| Version | 8.4.1 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"ScopedTypeVariables could allow more programs","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Consider\r\n{{{\r\ndata P a = P\r\ndata T1 a where\r\n MkT1 :: forall a. P a -> T1 a\r\n MkT2 :: forall a. P a -> T1 (a,a)\r\n MkT3 :: forall a b. b ~ Int => P a -> P b -> T1 a\r\n MkT4 :: forall a b. P a -> P b -> T1 a\r\n MkT5 :: forall a b c. b ~ c => P a -> P b -> P c -> T1 a\r\n}}}\r\n\r\nI can write this function\r\n{{{\r\nfoo :: T1 (Int, Int) -> ()\r\nfoo (MkT1 (P::P (Int,Int))) = ()\r\nfoo (MkT2 (P::P x)) = (() :: x ~ Int => ())\r\nfoo (MkT3 P (P::P Int)) = ()\r\nfoo (MkT4 P (P::P b)) = ()\r\nfoo (MkT5 P (P::P b) (P::P b)) = ()\r\n}}}\r\nbut this these two equations fail\r\n{{{\r\nfoo (MkT1 (P::P (Int,x))) = (() :: x ~ Int => ())\r\nfoo (MkT1 (P::P x)) = (() :: x ~ (Int,Int) => ())\r\n}}}\r\n\r\nI am especially surprised by the second one, given that the very similar equation with `MkT2` works.","type_of_failure":"OtherFailure","blocking":[]} -->8.8.1