GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2020-09-01T08:32:55Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/15554COMPLETE pragmas make overlapping-patterns warnings behave oddly2020-09-01T08:32:55ZFrank SteffahnCOMPLETE pragmas make overlapping-patterns warnings behave oddlyI can’t really quantify what’s wrong and what’s intended here, here’s a test file comparing different contrasting examples of similar functions which generate no or strange warnings in the cases that use a datatype with COMPLETE pragmas ...I can’t really quantify what’s wrong and what’s intended here, here’s a test file comparing different contrasting examples of similar functions which generate no or strange warnings in the cases that use a datatype with COMPLETE pragmas on pattern synonyms.
```hs
{- 1 -} {-# LANGUAGE PatternSynonyms, ViewPatterns #-}
{- 2 -}
{- 3 -} module M where
{- 4 -}
{- 5 -} data T = A | B | C
{- 6 -}
{- 7 -} isBC :: T -> Bool
{- 8 -} isBC A = False
{- 9 -} isBC B = True
{- 10 -} isBC C = True
{- 11 -}
{- 12 -} pattern BC :: T
{- 13 -} pattern BC <- (isBC -> True)
{- 14 -} {-# COMPLETE A, BC #-}
{- 15 -}
{- 16 -} g1 :: T -> Int
{- 17 -} g1 A = 1
{- 18 -} g1 BC = 2
{- 19 -} g1 _ = 3
{- 20 -}
{- 21 -} -- M.hs:18:1: warning: [-Woverlapping-patterns]
{- 22 -} -- Pattern match is redundant
{- 23 -} -- In an equation for `g1': g1 BC = ...
{- 24 -} -- |
{- 25 -} -- 18 | {- 18 -} g1 BC = 2
{- 26 -} -- | ^^^^^^^^^
{- 27 -}
{- 28 -} g2 :: T -> Int
{- 29 -} g2 BC = 2
{- 30 -} g2 A = 1
{- 31 -} g2 _ = 3
{- 32 -}
{- 33 -} -- g2: no warnings
{- 34 -}
{- 35 -} g3 :: T -> Int
{- 36 -} g3 BC = 2
{- 37 -} g3 _ = 1
{- 38 -} g3 A = 3
{- 39 -} g3 A = 4
{- 40 -} g3 B = 4
{- 41 -} g3 B = 4
{- 42 -} g3 C = 4
{- 43 -} g3 C = 4
{- 44 -} g3 _ = 4
{- 45 -} g3 _ = 4
{- 46 -}
{- 47 -} -- g3: no warnings
{- 48 -}
{- 49 -} data T' = A' | B' | C'
{- 50 -}
{- 51 -} isBC' :: T' -> Bool
{- 52 -} isBC' A' = False
{- 53 -} isBC' B' = True
{- 54 -} isBC' C' = True
{- 55 -}
{- 56 -} pattern BC' :: T'
{- 57 -} pattern BC' <- (isBC' -> True)
{- 58 -} -- no COMPLETE pragma
{- 59 -}
{- 60 -} g3' :: T' -> Int
{- 61 -} g3' BC' = 2
{- 62 -} g3' _ = 1
{- 63 -} g3' A' = 3
{- 64 -} g3' A' = 4
{- 65 -} g3' B' = 4
{- 66 -} g3' B' = 4
{- 67 -} g3' C' = 4
{- 68 -} g3' C' = 4
{- 69 -} g3' _ = 4
{- 70 -} g3' _ = 4
{- 71 -}
{- 72 -} -- M.hs:63:1: warning: [-Woverlapping-patterns]
{- 73 -} -- Pattern match is redundant
{- 74 -} -- In an equation for g3': g3' A' = ...
{- 75 -} -- |
{- 76 -} -- 63 | {- 63 -} g3' A' = 3
{- 77 -} -- | ^^^^^^^^^^
{- 78 -} --
{- 79 -} -- M.hs:64:1: warning: [-Woverlapping-patterns]
{- 80 -} -- Pattern match is redundant
{- 81 -} -- In an equation for g3': g3' A' = ...
{- 82 -} -- |
{- 83 -} -- 64 | {- 64 -} g3' A' = 4
{- 84 -} -- | ^^^^^^^^^^
{- 85 -} --
{- 86 -} -- M.hs:65:1: warning: [-Woverlapping-patterns]
{- 87 -} -- Pattern match is redundant
{- 88 -} -- In an equation for g3': g3' B' = ...
{- 89 -} -- |
{- 90 -} -- 65 | {- 65 -} g3' B' = 4
{- 91 -} -- | ^^^^^^^^^^
{- 92 -} --
{- 93 -} -- M.hs:66:1: warning: [-Woverlapping-patterns]
{- 94 -} -- Pattern match is redundant
{- 95 -} -- In an equation for g3': g3' B' = ...
{- 96 -} -- |
{- 97 -} -- 66 | {- 66 -} g3' B' = 4
{- 98 -} -- | ^^^^^^^^^^
{- 99 -} --
{- 100 -} -- M.hs:67:1: warning: [-Woverlapping-patterns]
{- 101 -} -- Pattern match is redundant
{- 102 -} -- In an equation for g3': g3' C' = ...
{- 103 -} -- |
{- 104 -} -- 67 | {- 67 -} g3' C' = 4
{- 105 -} -- | ^^^^^^^^^^
{- 106 -} --
{- 107 -} -- M.hs:68:1: warning: [-Woverlapping-patterns]
{- 108 -} -- Pattern match is redundant
{- 109 -} -- In an equation for g3': g3' C' = ...
{- 110 -} -- |
{- 111 -} -- 68 | {- 68 -} g3' C' = 4
{- 112 -} -- | ^^^^^^^^^^
{- 113 -} --
{- 114 -} -- M.hs:69:1: warning: [-Woverlapping-patterns]
{- 115 -} -- Pattern match is redundant
{- 116 -} -- In an equation for g3': g3' _ = ...
{- 117 -} -- |
{- 118 -} -- 69 | {- 69 -} g3' _ = 4
{- 119 -} -- | ^^^^^^^^^
{- 120 -} --
{- 121 -} -- M.hs:70:1: warning: [-Woverlapping-patterns]
{- 122 -} -- Pattern match is redundant
{- 123 -} -- In an equation for g3': g3' _ = ...
{- 124 -} -- |
{- 125 -} -- 70 | {- 70 -} g3' _ = 4
{- 126 -} -- | ^^^^^^^^^
{- 127 -}
{- 128 -}
{- 129 -} data S = X
{- 130 -}
{- 131 -} pattern Y :: S
{- 132 -} pattern Y = X
{- 133 -} {-# COMPLETE Y #-}
{- 134 -}
{- 135 -} f1 :: S -> Int
{- 136 -} f1 Y = 1
{- 137 -} f1 _ = 2
{- 138 -}
{- 139 -} -- f1: no warnings
{- 140 -}
{- 141 -} f2 :: S -> Int
{- 142 -} f2 X = 1
{- 143 -} f2 _ = 2
{- 144 -}
{- 145 -} -- M.hs:143:1: warning: [-Woverlapping-patterns]
{- 146 -} -- Pattern match is redundant
{- 147 -} -- In an equation for `f2': f2 _ = ...
{- 148 -} -- |
{- 149 -} -- 143 | {- 143 -} f2 _ = 2
{- 150 -} -- | ^^^^^^^^
{- 151 -}
{- 152 -} f3 :: S -> Int
{- 153 -} f3 Y = 0
{- 154 -} f3 X = 1
{- 155 -} f3 _ = 2
{- 156 -}
{- 157 -} -- f3: no warnings
{- 158 -}
{- 159 -} data S' = X'
{- 160 -}
{- 161 -} pattern Y' :: S'
{- 162 -} pattern Y' = X'
{- 163 -} -- no COMPLETE pragma
{- 164 -}
{- 165 -} f3' :: S' -> Int
{- 166 -} f3' Y' = 1
{- 167 -} f3' X' = 0
{- 168 -} f3' _ = 2
{- 169 -}
{- 170 -} -- M.hs:168:1: warning: [-Woverlapping-patterns]
{- 171 -} -- Pattern match is redundant
{- 172 -} -- In an equation for f3': f3' _ = ...
{- 173 -} -- |
{- 174 -} -- 168 | {- 168 -} f3' _ = 2
{- 175 -} -- | ^^^^^^^^^
```
In particular: the warning for line 18 should probably be a warning for line 19, and there should be a similar warning for line 31. `g3` extends `g2` in a ridiculous way still without generating any warnings. `g3'` demonstrates the warnings one should expect.
The `f` functions are perhaps a bit redundant, but I wanted to include a smaller datatype.
I’m not sure if this is easily fixable, since I’m having doubts, that COMPLETE pragmas give enough information for generating good overlapping-patterns warnings. I didn’t think this matter through in detail, but, well, maybe it’s not that important to have this all that sophisticated anyways, since for example guards won’t give overlapping-patterns warnings either. But at least (IMO) it’d be nice to keep the warnings about the normal constructor’s patterns even when they’re mixed with pattern synonyms that have a COMPLETE pragma.
Even further, I would always expect overlapping-patterns warnings when a pattern is simply duplicated and probably always if any additional pattern follows a complete listing of everything in a COMPLETE group. And there’s probably lots of cases one could consider naturally suggesting a warning; maybe someone can find a good principle/algorithm to use here. Going further, to prevent COMPLETE pragma setting that always give an overlapping-patterns or incomplete-patterns warnings, one could even consider warning directly at a COMPLETE pragma when it’s a strict subset of an existing COMPLETE group.
By the way, my actual goal while finding this bug was to describe another (maybe) bug, which is that the incomplete-patterns warnings can suggest missing pattern synonyms that are not even in scope, which seems not very neat in some cases. In case someone really wants to rework all these warnings, I can make a separate ticket or give details on such a non-neat case that here.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.4.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"COMPLETE pragmas make overlapping-patterns warnings behave oddly","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I can’t really quantify what’s wrong and what’s intended here, here’s a test file comparing different contrasting examples of similar functions which generate no or strange warnings in the cases that use a datatype with COMPLETE pragmas on pattern synonyms.\r\n\r\n{{{#!hs\r\n{- 1 -} {-# LANGUAGE PatternSynonyms, ViewPatterns #-}\r\n{- 2 -} \r\n{- 3 -} module M where\r\n{- 4 -} \r\n{- 5 -} data T = A | B | C\r\n{- 6 -} \r\n{- 7 -} isBC :: T -> Bool\r\n{- 8 -} isBC A = False\r\n{- 9 -} isBC B = True\r\n{- 10 -} isBC C = True\r\n{- 11 -} \r\n{- 12 -} pattern BC :: T\r\n{- 13 -} pattern BC <- (isBC -> True)\r\n{- 14 -} {-# COMPLETE A, BC #-}\r\n{- 15 -} \r\n{- 16 -} g1 :: T -> Int\r\n{- 17 -} g1 A = 1\r\n{- 18 -} g1 BC = 2\r\n{- 19 -} g1 _ = 3\r\n{- 20 -} \r\n{- 21 -} -- M.hs:18:1: warning: [-Woverlapping-patterns]\r\n{- 22 -} -- Pattern match is redundant\r\n{- 23 -} -- In an equation for `g1': g1 BC = ...\r\n{- 24 -} -- |\r\n{- 25 -} -- 18 | {- 18 -} g1 BC = 2\r\n{- 26 -} -- | ^^^^^^^^^\r\n{- 27 -} \r\n{- 28 -} g2 :: T -> Int\r\n{- 29 -} g2 BC = 2\r\n{- 30 -} g2 A = 1\r\n{- 31 -} g2 _ = 3\r\n{- 32 -} \r\n{- 33 -} -- g2: no warnings\r\n{- 34 -} \r\n{- 35 -} g3 :: T -> Int\r\n{- 36 -} g3 BC = 2\r\n{- 37 -} g3 _ = 1\r\n{- 38 -} g3 A = 3\r\n{- 39 -} g3 A = 4\r\n{- 40 -} g3 B = 4\r\n{- 41 -} g3 B = 4\r\n{- 42 -} g3 C = 4\r\n{- 43 -} g3 C = 4\r\n{- 44 -} g3 _ = 4\r\n{- 45 -} g3 _ = 4\r\n{- 46 -} \r\n{- 47 -} -- g3: no warnings\r\n{- 48 -} \r\n{- 49 -} data T' = A' | B' | C'\r\n{- 50 -} \r\n{- 51 -} isBC' :: T' -> Bool\r\n{- 52 -} isBC' A' = False\r\n{- 53 -} isBC' B' = True\r\n{- 54 -} isBC' C' = True\r\n{- 55 -} \r\n{- 56 -} pattern BC' :: T'\r\n{- 57 -} pattern BC' <- (isBC' -> True)\r\n{- 58 -} -- no COMPLETE pragma\r\n{- 59 -} \r\n{- 60 -} g3' :: T' -> Int\r\n{- 61 -} g3' BC' = 2\r\n{- 62 -} g3' _ = 1\r\n{- 63 -} g3' A' = 3\r\n{- 64 -} g3' A' = 4\r\n{- 65 -} g3' B' = 4\r\n{- 66 -} g3' B' = 4\r\n{- 67 -} g3' C' = 4\r\n{- 68 -} g3' C' = 4\r\n{- 69 -} g3' _ = 4\r\n{- 70 -} g3' _ = 4\r\n{- 71 -} \r\n{- 72 -} -- M.hs:63:1: warning: [-Woverlapping-patterns]\r\n{- 73 -} -- Pattern match is redundant\r\n{- 74 -} -- In an equation for g3': g3' A' = ...\r\n{- 75 -} -- |\r\n{- 76 -} -- 63 | {- 63 -} g3' A' = 3\r\n{- 77 -} -- | ^^^^^^^^^^\r\n{- 78 -} -- \r\n{- 79 -} -- M.hs:64:1: warning: [-Woverlapping-patterns]\r\n{- 80 -} -- Pattern match is redundant\r\n{- 81 -} -- In an equation for g3': g3' A' = ...\r\n{- 82 -} -- |\r\n{- 83 -} -- 64 | {- 64 -} g3' A' = 4\r\n{- 84 -} -- | ^^^^^^^^^^\r\n{- 85 -} -- \r\n{- 86 -} -- M.hs:65:1: warning: [-Woverlapping-patterns]\r\n{- 87 -} -- Pattern match is redundant\r\n{- 88 -} -- In an equation for g3': g3' B' = ...\r\n{- 89 -} -- |\r\n{- 90 -} -- 65 | {- 65 -} g3' B' = 4\r\n{- 91 -} -- | ^^^^^^^^^^\r\n{- 92 -} -- \r\n{- 93 -} -- M.hs:66:1: warning: [-Woverlapping-patterns]\r\n{- 94 -} -- Pattern match is redundant\r\n{- 95 -} -- In an equation for g3': g3' B' = ...\r\n{- 96 -} -- |\r\n{- 97 -} -- 66 | {- 66 -} g3' B' = 4\r\n{- 98 -} -- | ^^^^^^^^^^\r\n{- 99 -} -- \r\n{- 100 -} -- M.hs:67:1: warning: [-Woverlapping-patterns]\r\n{- 101 -} -- Pattern match is redundant\r\n{- 102 -} -- In an equation for g3': g3' C' = ...\r\n{- 103 -} -- |\r\n{- 104 -} -- 67 | {- 67 -} g3' C' = 4\r\n{- 105 -} -- | ^^^^^^^^^^\r\n{- 106 -} -- \r\n{- 107 -} -- M.hs:68:1: warning: [-Woverlapping-patterns]\r\n{- 108 -} -- Pattern match is redundant\r\n{- 109 -} -- In an equation for g3': g3' C' = ...\r\n{- 110 -} -- |\r\n{- 111 -} -- 68 | {- 68 -} g3' C' = 4\r\n{- 112 -} -- | ^^^^^^^^^^\r\n{- 113 -} -- \r\n{- 114 -} -- M.hs:69:1: warning: [-Woverlapping-patterns]\r\n{- 115 -} -- Pattern match is redundant\r\n{- 116 -} -- In an equation for g3': g3' _ = ...\r\n{- 117 -} -- |\r\n{- 118 -} -- 69 | {- 69 -} g3' _ = 4\r\n{- 119 -} -- | ^^^^^^^^^\r\n{- 120 -} -- \r\n{- 121 -} -- M.hs:70:1: warning: [-Woverlapping-patterns]\r\n{- 122 -} -- Pattern match is redundant\r\n{- 123 -} -- In an equation for g3': g3' _ = ...\r\n{- 124 -} -- |\r\n{- 125 -} -- 70 | {- 70 -} g3' _ = 4\r\n{- 126 -} -- | ^^^^^^^^^\r\n{- 127 -} \r\n{- 128 -} \r\n{- 129 -} data S = X\r\n{- 130 -} \r\n{- 131 -} pattern Y :: S\r\n{- 132 -} pattern Y = X\r\n{- 133 -} {-# COMPLETE Y #-}\r\n{- 134 -} \r\n{- 135 -} f1 :: S -> Int\r\n{- 136 -} f1 Y = 1\r\n{- 137 -} f1 _ = 2\r\n{- 138 -} \r\n{- 139 -} -- f1: no warnings\r\n{- 140 -} \r\n{- 141 -} f2 :: S -> Int\r\n{- 142 -} f2 X = 1\r\n{- 143 -} f2 _ = 2\r\n{- 144 -} \r\n{- 145 -} -- M.hs:143:1: warning: [-Woverlapping-patterns]\r\n{- 146 -} -- Pattern match is redundant\r\n{- 147 -} -- In an equation for `f2': f2 _ = ...\r\n{- 148 -} -- |\r\n{- 149 -} -- 143 | {- 143 -} f2 _ = 2\r\n{- 150 -} -- | ^^^^^^^^\r\n{- 151 -} \r\n{- 152 -} f3 :: S -> Int\r\n{- 153 -} f3 Y = 0\r\n{- 154 -} f3 X = 1\r\n{- 155 -} f3 _ = 2\r\n{- 156 -} \r\n{- 157 -} -- f3: no warnings\r\n{- 158 -} \r\n{- 159 -} data S' = X'\r\n{- 160 -} \r\n{- 161 -} pattern Y' :: S'\r\n{- 162 -} pattern Y' = X'\r\n{- 163 -} -- no COMPLETE pragma\r\n{- 164 -} \r\n{- 165 -} f3' :: S' -> Int\r\n{- 166 -} f3' Y' = 1\r\n{- 167 -} f3' X' = 0\r\n{- 168 -} f3' _ = 2\r\n{- 169 -} \r\n{- 170 -} -- M.hs:168:1: warning: [-Woverlapping-patterns]\r\n{- 171 -} -- Pattern match is redundant\r\n{- 172 -} -- In an equation for f3': f3' _ = ...\r\n{- 173 -} -- |\r\n{- 174 -} -- 168 | {- 168 -} f3' _ = 2\r\n{- 175 -} -- | ^^^^^^^^^\r\n}}}\r\n\r\nIn particular: the warning for line 18 should probably be a warning for line 19, and there should be a similar warning for line 31. `g3` extends `g2` in a ridiculous way still without generating any warnings. `g3'` demonstrates the warnings one should expect.\r\n\r\nThe `f` functions are perhaps a bit redundant, but I wanted to include a smaller datatype.\r\n\r\nI’m not sure if this is easily fixable, since I’m having doubts, that COMPLETE pragmas give enough information for generating good overlapping-patterns warnings. I didn’t think this matter through in detail, but, well, maybe it’s not that important to have this all that sophisticated anyways, since for example guards won’t give overlapping-patterns warnings either. But at least (IMO) it’d be nice to keep the warnings about the normal constructor’s patterns even when they’re mixed with pattern synonyms that have a COMPLETE pragma.\r\n\r\nEven further, I would always expect overlapping-patterns warnings when a pattern is simply duplicated and probably always if any additional pattern follows a complete listing of everything in a COMPLETE group. And there’s probably lots of cases one could consider naturally suggesting a warning; maybe someone can find a good principle/algorithm to use here. Going further, to prevent COMPLETE pragma setting that always give an overlapping-patterns or incomplete-patterns warnings, one could even consider warning directly at a COMPLETE pragma when it’s a strict subset of an existing COMPLETE group.\r\n\r\nBy the way, my actual goal while finding this bug was to describe another (maybe) bug, which is that the incomplete-patterns warnings can suggest missing pattern synonyms that are not even in scope, which seems not very neat in some cases. In case someone really wants to rework all these warnings, I can make a separate ticket or give details on such a non-neat case that here.","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/15450Inconsistency w.r.t. coverage checking warnings for EmptyCase under unsatisfi...2020-09-30T15:54:07ZRyan ScottInconsistency w.r.t. coverage checking warnings for EmptyCase under unsatisfiable constraintsConsider the following code:
```hs
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE GADTs #-}
{-# OPTIONS_GHC -Wincomplete-patterns #-}
module Bug where
f :: (Int ~ Bool) => Bool -> a
f x = case x of {}
g :: (Int ~ Bool) => Bool -> a
g x = cas...Consider the following code:
```hs
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE GADTs #-}
{-# OPTIONS_GHC -Wincomplete-patterns #-}
module Bug where
f :: (Int ~ Bool) => Bool -> a
f x = case x of {}
g :: (Int ~ Bool) => Bool -> a
g x = case x of True -> undefined
```
```
$ /opt/ghc/8.4.3/bin/ghci Bug.hs
GHCi, version 8.4.3: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:10:7: warning: [-Wincomplete-patterns]
Pattern match(es) are non-exhaustive
In a case alternative: Patterns not matched: False
|
10 | g x = case x of True -> undefined
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
Observe that we get a non-exhaustivity warning for the `case` expression in `g` (thanks to commit adb565aa74582969bbcc3b411d6d518b1c76c3cf), but not for the one in `f`. The difference is that `f` uses `EmptyCase`, whereas `g` does not, and the codepath for `EmptyCase` is unfortunately incongruous with the codepath for other coverage checking.
I know how to fix this. Patch incoming.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.4.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Inconsistency w.r.t. coverage checking warnings for EmptyCase under unsatisfiable constraints","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["PatternMatchWarnings"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider the following code:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE EmptyCase #-}\r\n{-# LANGUAGE GADTs #-}\r\n{-# OPTIONS_GHC -Wincomplete-patterns #-}\r\nmodule Bug where\r\n\r\nf :: (Int ~ Bool) => Bool -> a\r\nf x = case x of {}\r\n\r\ng :: (Int ~ Bool) => Bool -> a\r\ng x = case x of True -> undefined\r\n}}}\r\n{{{\r\n$ /opt/ghc/8.4.3/bin/ghci Bug.hs\r\nGHCi, version 8.4.3: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:10:7: warning: [-Wincomplete-patterns]\r\n Pattern match(es) are non-exhaustive\r\n In a case alternative: Patterns not matched: False\r\n |\r\n10 | g x = case x of True -> undefined\r\n | ^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nObserve that we get a non-exhaustivity warning for the `case` expression in `g` (thanks to commit adb565aa74582969bbcc3b411d6d518b1c76c3cf), but not for the one in `f`. The difference is that `f` uses `EmptyCase`, whereas `g` does not, and the codepath for `EmptyCase` is unfortunately incongruous with the codepath for other coverage checking.\r\n\r\nI know how to fix this. Patch incoming.","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/15385-Wincomplete-patterns gets confused when combining GADTs and pattern guards2019-07-07T18:12:53ZRyan Scott-Wincomplete-patterns gets confused when combining GADTs and pattern guardsConsider the following code:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GH...Consider the following code:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wincomplete-patterns #-}
module Bug where
import Data.Kind
data family Sing :: forall k. k -> Type
newtype Id a = MkId a
data So :: Bool -> Type where
Oh :: So True
data instance Sing :: Bool -> Type where
SFalse :: Sing False
STrue :: Sing True
data instance Sing :: Ordering -> Type where
SLT :: Sing LT
SEQ :: Sing EQ
SGT :: Sing GT
data instance Sing :: forall a. Id a -> Type where
SMkId :: Sing x -> Sing (MkId x)
class POrd a where
type (x :: a) `Compare` (y :: a) :: Ordering
class SOrd a where
sCompare :: forall (x :: a) (y :: a).
Sing x -> Sing y -> Sing (x `Compare` y)
type family (x :: a) <= (y :: a) :: Bool where
x <= y = LeqCase (x `Compare` y)
type family LeqCase (o :: Ordering) :: Bool where
LeqCase LT = True
LeqCase EQ = True
LeqCase GT = False
(%<=) :: forall a (x :: a) (y :: a). SOrd a
=> Sing x -> Sing y -> Sing (x <= y)
sx %<= sy =
case sx `sCompare` sy of
SLT -> STrue
SEQ -> STrue
SGT -> SFalse
class (POrd a, SOrd a) => VOrd a where
leqReflexive :: forall (x :: a). Sing x -> So (x <= x)
instance POrd a => POrd (Id a) where
type MkId x `Compare` MkId y = x `Compare` y
instance SOrd a => SOrd (Id a) where
SMkId sx `sCompare` SMkId sy = sx `sCompare` sy
-----
instance VOrd a => VOrd (Id a) where
leqReflexive (SMkId sa)
| Oh <- leqReflexive sa
= case sa `sCompare` sa of
SLT -> Oh
SEQ -> Oh
-- SGT -> undefined
```
What exactly this code does isn't terribly important. The important bit is that last instance (`VOrd (Id a)`). That //should// be total, but GHC disagrees:
```
GHCi, version 8.6.0.20180627: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:63:7: warning: [-Wincomplete-patterns]
Pattern match(es) are non-exhaustive
In a case alternative: Patterns not matched: SGT
|
63 | = case sa `sCompare` sa of
| ^^^^^^^^^^^^^^^^^^^^^^^^...
```
As evidence that this warning is bogus, if you uncomment the last line, then GHC correctly observes that that line is inaccessible:
```
GHCi, version 8.6.0.20180627: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:66:9: warning: [-Winaccessible-code]
• Couldn't match type ‘'True’ with ‘'False’
Inaccessible code in
a pattern with constructor: SGT :: Sing 'GT, in a case alternative
• In the pattern: SGT
In a case alternative: SGT -> undefined
In the expression:
case sa `sCompare` sa of
SLT -> Oh
SEQ -> Oh
SGT -> undefined
|
66 | SGT -> undefined
| ^^^
```
Clearly, something is afoot in the coverage checker.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.5 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"-Wincomplete-patterns gets confused when combining GADTs and pattern guards","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["PatternMatchWarnings"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider the following code:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE TypeOperators #-}\r\n{-# LANGUAGE UndecidableInstances #-}\r\n{-# OPTIONS_GHC -Wincomplete-patterns #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ndata family Sing :: forall k. k -> Type\r\nnewtype Id a = MkId a\r\ndata So :: Bool -> Type where\r\n Oh :: So True\r\n\r\ndata instance Sing :: Bool -> Type where\r\n SFalse :: Sing False\r\n STrue :: Sing True\r\ndata instance Sing :: Ordering -> Type where\r\n SLT :: Sing LT\r\n SEQ :: Sing EQ\r\n SGT :: Sing GT\r\ndata instance Sing :: forall a. Id a -> Type where\r\n SMkId :: Sing x -> Sing (MkId x)\r\n\r\nclass POrd a where\r\n type (x :: a) `Compare` (y :: a) :: Ordering\r\n\r\nclass SOrd a where\r\n sCompare :: forall (x :: a) (y :: a).\r\n Sing x -> Sing y -> Sing (x `Compare` y)\r\n\r\ntype family (x :: a) <= (y :: a) :: Bool where\r\n x <= y = LeqCase (x `Compare` y)\r\ntype family LeqCase (o :: Ordering) :: Bool where\r\n LeqCase LT = True\r\n LeqCase EQ = True\r\n LeqCase GT = False\r\n\r\n(%<=) :: forall a (x :: a) (y :: a). SOrd a\r\n => Sing x -> Sing y -> Sing (x <= y)\r\nsx %<= sy =\r\n case sx `sCompare` sy of\r\n SLT -> STrue\r\n SEQ -> STrue\r\n SGT -> SFalse\r\n\r\nclass (POrd a, SOrd a) => VOrd a where\r\n leqReflexive :: forall (x :: a). Sing x -> So (x <= x)\r\n\r\ninstance POrd a => POrd (Id a) where\r\n type MkId x `Compare` MkId y = x `Compare` y\r\n\r\ninstance SOrd a => SOrd (Id a) where\r\n SMkId sx `sCompare` SMkId sy = sx `sCompare` sy\r\n\r\n-----\r\n\r\ninstance VOrd a => VOrd (Id a) where\r\n leqReflexive (SMkId sa)\r\n | Oh <- leqReflexive sa\r\n = case sa `sCompare` sa of\r\n SLT -> Oh\r\n SEQ -> Oh\r\n -- SGT -> undefined\r\n}}}\r\n\r\nWhat exactly this code does isn't terribly important. The important bit is that last instance (`VOrd (Id a)`). That //should// be total, but GHC disagrees:\r\n\r\n{{{\r\nGHCi, version 8.6.0.20180627: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:63:7: warning: [-Wincomplete-patterns]\r\n Pattern match(es) are non-exhaustive\r\n In a case alternative: Patterns not matched: SGT\r\n |\r\n63 | = case sa `sCompare` sa of\r\n | ^^^^^^^^^^^^^^^^^^^^^^^^...\r\n}}}\r\n\r\nAs evidence that this warning is bogus, if you uncomment the last line, then GHC correctly observes that that line is inaccessible:\r\n\r\n{{{\r\nGHCi, version 8.6.0.20180627: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:66:9: warning: [-Winaccessible-code]\r\n • Couldn't match type ‘'True’ with ‘'False’\r\n Inaccessible code in\r\n a pattern with constructor: SGT :: Sing 'GT, in a case alternative\r\n • In the pattern: SGT\r\n In a case alternative: SGT -> undefined\r\n In the expression:\r\n case sa `sCompare` sa of\r\n SLT -> Oh\r\n SEQ -> Oh\r\n SGT -> undefined\r\n |\r\n66 | SGT -> undefined\r\n | ^^^\r\n}}}\r\n\r\nClearly, something is afoot in the coverage checker.","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/14773MultiWayIf makes it easy to write partial programs that are not catched by -Wall2019-08-08T12:58:27ZSimon Hengelsol@typeful.netMultiWayIf makes it easy to write partial programs that are not catched by -WallThe following partial function will pass `-Wall`
```haskell
-- program 1
{-# LANGUAGE MultiWayIf #-}
foo :: Bool -> Int
foo b = if | b -> 23
```
While the following two alternatives will not:
```haskell
-- program 2
foo :: Bool -> Int...The following partial function will pass `-Wall`
```haskell
-- program 1
{-# LANGUAGE MultiWayIf #-}
foo :: Bool -> Int
foo b = if | b -> 23
```
While the following two alternatives will not:
```haskell
-- program 2
foo :: Bool -> Int
foo b | b = 23
```
```haskell
-- program 3
foo :: Bool -> Int
foo b = case () of
() | b -> 23
```
Note that the GHC User's Guide states that "program 1" and "program 3" are equivalent.
1. Is this a bug or by design?
1. I guess at the very least we would want to update the User's Guide
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.2.2 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"MultiWayIf makes it easy to write partial programs that are not catched by -Wall","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following partial function will pass {{{-Wall}}}\r\n\r\n{{{#!haskell\r\n-- program 1\r\n{-# LANGUAGE MultiWayIf #-}\r\nfoo :: Bool -> Int\r\nfoo b = if | b -> 23\r\n}}}\r\n\r\nWhile the following two alternatives will not:\r\n\r\n{{{#!haskell\r\n-- program 2\r\nfoo :: Bool -> Int \r\nfoo b | b = 23\r\n}}}\r\n\r\n{{{#!haskell\r\n-- program 3\r\nfoo :: Bool -> Int\r\nfoo b = case () of\r\n () | b -> 23\r\n}}}\r\n\r\nNote that the GHC User's Guide states that \"program 1\" and \"program 3\" are equivalent.\r\n\r\n1. Is this a bug or by design?\r\n2. I guess at the very least we would want to update the User's Guide","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1Tao Hesighingnow@gmail.comTao Hesighingnow@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/14667Compiling a function with a lot of alternatives bottlenecks on insertIntHeap2019-07-07T18:16:05ZniteriaCompiling a function with a lot of alternatives bottlenecks on insertIntHeapI have a module that looks like this:
```
module A10000 where
data A = A
| A00001
| A00002
...
| A10000
f :: A -> Int
f A00001 = 19900001
f A00002 = 19900002
...
f A10000 = 19910000
```
Compiling with `-s` gives:
```
[1 of 1] ...I have a module that looks like this:
```
module A10000 where
data A = A
| A00001
| A00002
...
| A10000
f :: A -> Int
f A00001 = 19900001
f A00002 = 19900002
...
f A10000 = 19910000
```
Compiling with `-s` gives:
```
[1 of 1] Compiling A10000 ( A10000.hs, A10000.o )
A10000.hs:10004:1: warning:
Pattern match checker exceeded (2000000) iterations in
an equation for ‘f’. (Use -fmax-pmcheck-iterations=n
to set the maximun number of iterations to n)
|
10004 | f A00001 = 19900001
| ^^^^^^^^^^^^^^^^^^^...
95,068,628,968 bytes allocated in the heap
14,166,421,680 bytes copied during GC
312,247,488 bytes maximum residency (19 sample(s))
3,267,024 bytes maximum slop
857 MB total memory in use (0 MB lost due to fragmentation)
Tot time (elapsed) Avg pause Max pause
Gen 0 35163 colls, 0 par 5.191s 5.170s 0.0001s 0.0724s
Gen 1 19 colls, 0 par 1.240s 1.236s 0.0650s 0.1872s
TASKS: 4 (1 bound, 3 peak workers (3 total), using -N1)
SPARKS: 0 (0 converted, 0 overflowed, 0 dud, 0 GC'd, 0 fizzled)
INIT time 0.000s ( 0.000s elapsed)
MUT time 23.100s ( 23.341s elapsed)
GC time 6.431s ( 6.405s elapsed)
RP time 0.000s ( 0.000s elapsed)
PROF time 0.000s ( 0.000s elapsed)
EXIT time 0.000s ( 0.001s elapsed)
Total time 29.532s ( 29.748s elapsed)
```
With profiling enabled I get:
```
total time = 22.67 secs (22673 ticks @ 1000 us, 1 processor)
total alloc = 36,143,653,320 bytes (excludes profiling overheads)
COST CENTRE MODULE SRC %time %alloc ticks bytes
insertIntHeap Hoopl.Dataflow compiler/cmm/Hoopl/Dataflow.hs:(450,1)-(454,38) 73.9 77.5 16746 28001680176
SimplTopBinds SimplCore compiler/simplCore/SimplCore.hs:770:39-74 9.4 1.8 2136 647116224
deSugar HscMain compiler/main/HscMain.hs:511:7-44 2.6 4.2 599 1530056552
pprNativeCode AsmCodeGen compiler/nativeGen/AsmCodeGen.hs:(529,37)-(530,65) 2.3 2.9 524 1030493864
StgCmm HscMain compiler/main/HscMain.hs:(1426,13)-(1427,62) 1.3 1.4 288 497401376
RegAlloc-linear AsmCodeGen compiler/nativeGen/AsmCodeGen.hs:(658,27)-(660,55) 0.9 1.1 201 383789200
tc_rn_src_decls TcRnDriver compiler/typecheck/TcRnDriver.hs:(494,4)-(556,7) 0.8 1.2 176 441973152
Parser HscMain compiler/main/HscMain.hs:(316,5)-(384,20) 0.5 1.1 113 411448880
```
After a local patch that basically reverts https://phabricator.haskell.org/rGHC5a1a2633553 I get:
```
[1 of 1] Compiling A10000 ( A10000.hs, A10000.o )
A10000.hs:10004:1: warning:
Pattern match checker exceeded (2000000) iterations in
an equation for ‘f’. (Use -fmax-pmcheck-iterations=n
to set the maximun number of iterations to n)
|
10004 | f A00001 = 19900001
| ^^^^^^^^^^^^^^^^^^^...
15,162,268,144 bytes allocated in the heap
4,870,184,600 bytes copied during GC
323,794,936 bytes maximum residency (19 sample(s))
3,074,056 bytes maximum slop
886 MB total memory in use (0 MB lost due to fragmentation)
Tot time (elapsed) Avg pause Max pause
Gen 0 811 colls, 0 par 1.828s 1.821s 0.0022s 0.0770s
Gen 1 19 colls, 0 par 1.217s 1.213s 0.0638s 0.1820s
TASKS: 4 (1 bound, 3 peak workers (3 total), using -N1)
SPARKS: 0 (0 converted, 0 overflowed, 0 dud, 0 GC'd, 0 fizzled)
INIT time 0.000s ( 0.000s elapsed)
MUT time 5.842s ( 6.144s elapsed)
GC time 3.046s ( 3.034s elapsed)
RP time 0.000s ( 0.000s elapsed)
PROF time 0.000s ( 0.000s elapsed)
EXIT time 0.000s ( 0.001s elapsed)
Total time 8.888s ( 9.179s elapsed)
```
For a file of smaller size with 1000 constructors, it still gives a 10% win.
This example is artificial, but it looks like something that someone could write for a sparse enum that looks like this in C++:
```
enum access_t { read = 1, write = 2, exec = 4 };
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Compiling a function with a lot of alternatives bottlenecks on insertIntHeap","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I have a module that looks like this:\r\n{{{\r\nmodule A10000 where\r\n\r\ndata A = A\r\n | A00001\r\n | A00002\r\n...\r\n | A10000\r\n\r\nf :: A -> Int\r\nf A00001 = 19900001\r\nf A00002 = 19900002\r\n...\r\nf A10000 = 19910000\r\n}}}\r\n\r\nCompiling with `-s` gives:\r\n{{{\r\n[1 of 1] Compiling A10000 ( A10000.hs, A10000.o ) \r\n \r\nA10000.hs:10004:1: warning: \r\n Pattern match checker exceeded (2000000) iterations in \r\n an equation for ‘f’. (Use -fmax-pmcheck-iterations=n \r\n to set the maximun number of iterations to n) \r\n |\r\n10004 | f A00001 = 19900001\r\n | ^^^^^^^^^^^^^^^^^^^...\r\n 95,068,628,968 bytes allocated in the heap\r\n 14,166,421,680 bytes copied during GC\r\n 312,247,488 bytes maximum residency (19 sample(s))\r\n 3,267,024 bytes maximum slop\r\n 857 MB total memory in use (0 MB lost due to fragmentation)\r\n\r\n Tot time (elapsed) Avg pause Max pause\r\n Gen 0 35163 colls, 0 par 5.191s 5.170s 0.0001s 0.0724s\r\n Gen 1 19 colls, 0 par 1.240s 1.236s 0.0650s 0.1872s\r\n\r\n TASKS: 4 (1 bound, 3 peak workers (3 total), using -N1)\r\n\r\n SPARKS: 0 (0 converted, 0 overflowed, 0 dud, 0 GC'd, 0 fizzled)\r\n\r\n INIT time 0.000s ( 0.000s elapsed)\r\n MUT time 23.100s ( 23.341s elapsed)\r\n GC time 6.431s ( 6.405s elapsed)\r\n RP time 0.000s ( 0.000s elapsed)\r\n PROF time 0.000s ( 0.000s elapsed)\r\n EXIT time 0.000s ( 0.001s elapsed)\r\n Total time 29.532s ( 29.748s elapsed)\r\n}}}\r\n\r\nWith profiling enabled I get:\r\n{{{\r\n total time = 22.67 secs (22673 ticks @ 1000 us, 1 processor) \r\n total alloc = 36,143,653,320 bytes (excludes profiling overheads) \r\n \r\nCOST CENTRE MODULE SRC %time %alloc ticks bytes \r\n \r\ninsertIntHeap Hoopl.Dataflow compiler/cmm/Hoopl/Dataflow.hs:(450,1)-(454,38) 73.9 77.5 16746 28001680176 \r\nSimplTopBinds SimplCore compiler/simplCore/SimplCore.hs:770:39-74 9.4 1.8 2136 647116224 \r\ndeSugar HscMain compiler/main/HscMain.hs:511:7-44 2.6 4.2 599 1530056552 \r\npprNativeCode AsmCodeGen compiler/nativeGen/AsmCodeGen.hs:(529,37)-(530,65) 2.3 2.9 524 1030493864 \r\nStgCmm HscMain compiler/main/HscMain.hs:(1426,13)-(1427,62) 1.3 1.4 288 497401376 \r\nRegAlloc-linear AsmCodeGen compiler/nativeGen/AsmCodeGen.hs:(658,27)-(660,55) 0.9 1.1 201 383789200 \r\ntc_rn_src_decls TcRnDriver compiler/typecheck/TcRnDriver.hs:(494,4)-(556,7) 0.8 1.2 176 441973152 \r\nParser HscMain compiler/main/HscMain.hs:(316,5)-(384,20) 0.5 1.1 113 411448880 \r\n}}}\r\n\r\n\r\nAfter a local patch that basically reverts https://phabricator.haskell.org/rGHC5a1a2633553 I get:\r\n{{{\r\n[1 of 1] Compiling A10000 ( A10000.hs, A10000.o ) \r\n \r\nA10000.hs:10004:1: warning: \r\n Pattern match checker exceeded (2000000) iterations in \r\n an equation for ‘f’. (Use -fmax-pmcheck-iterations=n\r\n to set the maximun number of iterations to n)\r\n |\r\n10004 | f A00001 = 19900001\r\n | ^^^^^^^^^^^^^^^^^^^...\r\n 15,162,268,144 bytes allocated in the heap\r\n 4,870,184,600 bytes copied during GC\r\n 323,794,936 bytes maximum residency (19 sample(s))\r\n 3,074,056 bytes maximum slop\r\n 886 MB total memory in use (0 MB lost due to fragmentation)\r\n\r\n Tot time (elapsed) Avg pause Max pause\r\n Gen 0 811 colls, 0 par 1.828s 1.821s 0.0022s 0.0770s\r\n Gen 1 19 colls, 0 par 1.217s 1.213s 0.0638s 0.1820s\r\n\r\n TASKS: 4 (1 bound, 3 peak workers (3 total), using -N1)\r\n\r\n SPARKS: 0 (0 converted, 0 overflowed, 0 dud, 0 GC'd, 0 fizzled)\r\n\r\n INIT time 0.000s ( 0.000s elapsed)\r\n MUT time 5.842s ( 6.144s elapsed)\r\n GC time 3.046s ( 3.034s elapsed)\r\n RP time 0.000s ( 0.000s elapsed)\r\n PROF time 0.000s ( 0.000s elapsed)\r\n EXIT time 0.000s ( 0.001s elapsed)\r\n Total time 8.888s ( 9.179s elapsed)\r\n}}}\r\n\r\nFor a file of smaller size with 1000 constructors, it still gives a 10% win.\r\n\r\nThis example is artificial, but it looks like something that someone could write for a sparse enum that looks like this in C++:\r\n{{{\r\nenum access_t { read = 1, write = 2, exec = 4 };\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1niterianiteriahttps://gitlab.haskell.org/ghc/ghc/-/issues/14098Incorrect pattern match warning on nested GADTs2022-09-30T18:20:38ZjmgrosenIncorrect pattern match warning on nested GADTs```hs
{-# Language GADTs #-}
data App f a where
App :: f a -> App f (Maybe a)
data Ty a where
TBool :: Ty Bool
TInt :: Ty Int
data T f a where
C :: T Ty (Maybe Bool)
-- Warning
f :: T f a -> App f a -> ()
f C (App TBool) = (...```hs
{-# Language GADTs #-}
data App f a where
App :: f a -> App f (Maybe a)
data Ty a where
TBool :: Ty Bool
TInt :: Ty Int
data T f a where
C :: T Ty (Maybe Bool)
-- Warning
f :: T f a -> App f a -> ()
f C (App TBool) = ()
-- No warning
g :: T f a -> App f a -> ()
g C (App x) = case x of
TBool -> ()
```
When compiling, with `-Wincomplete-patterns`:
```
Foo.hs:15:1: warning: [-Wincomplete-patterns]
Pattern match(es) are non-exhaustive
In an equation for ‘f’: Patterns not matched: C (App TInt)
|
15 | f C (App TBool) = ()
| ^^^^^^^^^^^^^^^^^^^^
```
I'm sorry for such a complicated example, but I wasn't able to reduce it any further than this.
The gist of the problem is that this code gives a pattern matching non-exhaustiveness warning when matching a nested pattern, when pulling out a value then matching on it produces no warning (correctly). It also seems to have to do with using a type constructor (`Maybe`) within the constructor definition of `App`, as changing it to
```hs
data App f a where
App :: f a -> App f a
...
data T f a where
C :: T Ty Bool
```
does not give a warning, even when `App` is modified further to force it to be a proper GADT.
This might be a known limitation of the checker, but given that it works fine when the nesting is removed, I would think it would be more of a bug.
Thanks to Iavor for helping me minimize the test case.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.2.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | diatchki |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Incorrect pattern match warning on nested GADTs","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["PatternMatchWarnings"],"differentials":[],"test_case":"","architecture":"","cc":["diatchki"],"type":"Bug","description":"{{{#!hs\r\n{-# Language GADTs #-}\r\n\r\ndata App f a where\r\n App :: f a -> App f (Maybe a)\r\n\r\ndata Ty a where\r\n TBool :: Ty Bool\r\n TInt :: Ty Int\r\n\r\ndata T f a where\r\n C :: T Ty (Maybe Bool)\r\n\r\n-- Warning\r\nf :: T f a -> App f a -> ()\r\nf C (App TBool) = ()\r\n\r\n-- No warning\r\ng :: T f a -> App f a -> ()\r\ng C (App x) = case x of\r\n TBool -> ()\r\n}}}\r\n\r\nWhen compiling, with `-Wincomplete-patterns`:\r\n{{{\r\nFoo.hs:15:1: warning: [-Wincomplete-patterns]\r\n Pattern match(es) are non-exhaustive\r\n In an equation for ‘f’: Patterns not matched: C (App TInt)\r\n |\r\n15 | f C (App TBool) = ()\r\n | ^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nI'm sorry for such a complicated example, but I wasn't able to reduce it any further than this.\r\n\r\nThe gist of the problem is that this code gives a pattern matching non-exhaustiveness warning when matching a nested pattern, when pulling out a value then matching on it produces no warning (correctly). It also seems to have to do with using a type constructor (`Maybe`) within the constructor definition of `App`, as changing it to\r\n{{{#!hs\r\ndata App f a where\r\n App :: f a -> App f a\r\n\r\n...\r\n\r\ndata T f a where\r\n C :: T Ty Bool\r\n}}}\r\ndoes not give a warning, even when `App` is modified further to force it to be a proper GADT.\r\n\r\nThis might be a known limitation of the checker, but given that it works fine when the nesting is removed, I would think it would be more of a bug.\r\n\r\nThanks to Iavor for helping me minimize the test case.","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/11984Pattern match incompleteness / inaccessibility discrepancy2020-02-14T15:48:17ZRichard Eisenbergrae@richarde.devPattern match incompleteness / inaccessibility discrepancyConsider this module:
```hs
{-# LANGUAGE PolyKinds, TypeOperators, DataKinds, TypeFamilies, GADTs #-}
module Bug where
data family Sing (a :: k)
data Schema = Sch [Bool]
data instance Sing (x :: Schema) where
SSch :: Sing x -> Sin...Consider this module:
```hs
{-# LANGUAGE PolyKinds, TypeOperators, DataKinds, TypeFamilies, GADTs #-}
module Bug where
data family Sing (a :: k)
data Schema = Sch [Bool]
data instance Sing (x :: Schema) where
SSch :: Sing x -> Sing ('Sch x)
data instance Sing (x :: [k]) where
SNil :: Sing '[]
SCons :: Sing a -> Sing b -> Sing (a ': b)
data G a where
GCons :: G ('Sch (a ': b))
eval :: G s -> Sing s -> ()
eval GCons s =
case s of
-- SSch SNil -> undefined
SSch (SCons _ _) -> undefined
```
Upon seeing this, GHC says
```
Bug.hs:21:9: warning: [-Wincomplete-patterns]
Pattern match(es) are non-exhaustive
In a case alternative: Patterns not matched: (SSch SNil)
```
So I uncomment the second-to-last line, inducing GHC to say
```
Bug.hs:22:16: error:
• Couldn't match type ‘a : b’ with ‘'[]’
Inaccessible code in
a pattern with constructor: SNil :: forall k. Sing '[],
in a case alternative
• In the pattern: SNil
In the pattern: SSch SNil
In a case alternative: SSch SNil -> undefined
```
Thankfully, this pattern is much rarer than it once was, but it's a bit sad that it's still possible.8.6.1