GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2020-04-26T15:36:54Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/11224Program doesn't preserve semantics after pattern synonym inlining.2020-04-26T15:36:54Zanton.dubovikProgram doesn't preserve semantics after pattern synonym inlining.```hs
{-# language
PatternSynonyms
, ViewPatterns
#-}
import Text.Read
-- pattern PRead :: () => Read a => a -> String
pattern PRead a <- (readMaybe -> Just a)
foo :: String -> Int
foo (PRead x) = (x::Int)
foo (PRead xs) = sum (...```hs
{-# language
PatternSynonyms
, ViewPatterns
#-}
import Text.Read
-- pattern PRead :: () => Read a => a -> String
pattern PRead a <- (readMaybe -> Just a)
foo :: String -> Int
foo (PRead x) = (x::Int)
foo (PRead xs) = sum (xs::[Int])
foo _ = 666
bar :: String -> Int
bar (readMaybe -> Just x) = (x::Int)
bar (readMaybe -> Just xs) = sum (xs::[Int])
bar _ = 666
main :: IO ()
main = do
print $ foo "1" -- 1
print $ foo "[1,2,3]" -- 666 -- ???
print $ foo "xxx" -- 666
print $ bar "1" -- 1
print $ bar "[1,2,3]" -- 6
print $ bar "xxx" -- 666
```
I'm expecting that semantics of the function `foo` would not change if I inline pattern synonym.
However it does. `bar` successfully matches string against list of ints, whereas `foo` apperently skips this pattern and fall back to the catch-all case.
Reproducible both in GHCi and GHC.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 7.10.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":"Program doesn't preserve semantics after pattern synonym inlining.","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{-# language\r\n PatternSynonyms\r\n , ViewPatterns\r\n #-}\r\n\r\nimport Text.Read\r\n\r\n-- pattern PRead :: () => Read a => a -> String\r\npattern PRead a <- (readMaybe -> Just a)\r\n\r\nfoo :: String -> Int\r\nfoo (PRead x) = (x::Int)\r\nfoo (PRead xs) = sum (xs::[Int])\r\nfoo _ = 666\r\n\r\nbar :: String -> Int\r\nbar (readMaybe -> Just x) = (x::Int)\r\nbar (readMaybe -> Just xs) = sum (xs::[Int])\r\nbar _ = 666\r\n\r\nmain :: IO ()\r\nmain = do\r\n print $ foo \"1\" -- 1\r\n print $ foo \"[1,2,3]\" -- 666 -- ???\r\n print $ foo \"xxx\" -- 666\r\n\r\n print $ bar \"1\" -- 1\r\n print $ bar \"[1,2,3]\" -- 6\r\n print $ bar \"xxx\" -- 666\r\n}}}\r\n\r\nI'm expecting that semantics of the function `foo` would not change if I inline pattern synonym.\r\n\r\nHowever it does. `bar` successfully matches string against list of ints, whereas `foo` apperently skips this pattern and fall back to the catch-all case.\r\n\r\nReproducible both in GHCi and GHC.","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1https://gitlab.haskell.org/ghc/ghc/-/issues/11276GHC hangs/takes an exponential amount of time with simple program2020-03-04T08:34:57ZMatthew PickeringGHC hangs/takes an exponential amount of time with simple programThis was discovered when trying to compile xml-conduit. Here is the standalone test case with a few comments indicating how to make it compile.
The program compiles with ghc-7.10.2 but fails with HEAD.
```hs
{-# LANGUAGE RankNTypes #-}...This was discovered when trying to compile xml-conduit. Here is the standalone test case with a few comments indicating how to make it compile.
The program compiles with ghc-7.10.2 but fails with HEAD.
```hs
{-# LANGUAGE RankNTypes #-}
module Hang where
import Control.Monad
import Data.Char
data Event
= EventBeginDocument
| EventEndDocument
| EventBeginDoctype
| EventEndDoctype
| EventInstruction
| EventBeginElement
| EventEndElement
| EventContent Content
| EventComment
| EventCDATA
data Content
= ContentText String
| ContentEntity String
peek :: Monad m => Consumer a m (Maybe a)
peek = undefined
type Consumer i m r = forall o. ConduitM i o m r
tag :: forall m a b c o . Monad m =>
ConduitM Event o m (Maybe c)
tag = do
_ <- dropWS
return undefined
where
-- Add this and it works
-- dropWS :: Monad m => ConduitM Event o m (Maybe Event)
dropWS = do
-- Swap these two lines and it works
-- let x = undefined
x <- peek
let isWS =
case x of
-- Remove some of these and it works
Just EventBeginDocument -> True
Just EventEndDocument -> True
Just EventBeginDoctype{} -> True
Just EventEndDoctype -> True
Just EventInstruction{} -> True
Just EventBeginElement{} -> False
Just EventEndElement{} -> False
Just (EventContent (ContentText t))
| all isSpace t -> True
| otherwise -> False
Just (EventContent ContentEntity{}) -> False
Just EventComment{} -> True
Just EventCDATA{} -> False
Nothing -> False
if isWS then dropWS else return x
-- Inlined Instances
instance Functor (ConduitM i o m) where
fmap f (ConduitM c) = ConduitM $ \rest -> c (rest . f)
instance Applicative (ConduitM i o m) where
pure x = ConduitM ($ x)
{-# INLINE pure #-}
(<*>) = ap
{-# INLINE (<*>) #-}
instance Monad (ConduitM i o m) where
return = pure
ConduitM f >>= g = ConduitM $ \h -> f $ \a -> unConduitM (g a) h
instance Monad m => Functor (Pipe l i o u m) where
fmap = liftM
{-# INLINE fmap #-}
instance Monad m => Applicative (Pipe l i o u m) where
pure = Done
{-# INLINE pure #-}
(<*>) = ap
{-# INLINE (<*>) #-}
instance Monad m => Monad (Pipe l i o u m) where
return = pure
{-# INLINE return #-}
HaveOutput p c o >>= fp = HaveOutput (p >>= fp) c o
NeedInput p c >>= fp = NeedInput (p >=> fp) (c >=> fp)
Done x >>= fp = fp x
PipeM mp >>= fp = PipeM ((>>= fp) `liftM` mp)
Leftover p i >>= fp = Leftover (p >>= fp) i
newtype ConduitM i o m r = ConduitM
{ unConduitM :: forall b.
(r -> Pipe i i o () m b) -> Pipe i i o () m b
}
data Pipe l i o u m r =
HaveOutput (Pipe l i o u m r) (m ()) o
| NeedInput (i -> Pipe l i o u m r) (u -> Pipe l i o u m r)
| Done r
| PipeM (m (Pipe l i o u m r))
| Leftover (Pipe l i o u m r) l
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 7.10.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | high |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC hangs/takes an exponential amount of time with simple program","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This was discovered when trying to compile xml-conduit. Here is the standalone test case with a few comments indicating how to make it compile.\r\n\r\nThe program compiles with ghc-7.10.2 but fails with HEAD. \r\n\r\n{{{#!hs\r\n{-# LANGUAGE RankNTypes #-}\r\nmodule Hang where\r\nimport Control.Monad\r\nimport Data.Char\r\n\r\ndata Event\r\n = EventBeginDocument\r\n | EventEndDocument\r\n | EventBeginDoctype\r\n | EventEndDoctype\r\n | EventInstruction\r\n | EventBeginElement\r\n | EventEndElement\r\n | EventContent Content\r\n | EventComment\r\n | EventCDATA\r\n\r\ndata Content\r\n = ContentText String\r\n | ContentEntity String\r\n\r\n\r\npeek :: Monad m => Consumer a m (Maybe a)\r\npeek = undefined\r\n\r\ntype Consumer i m r = forall o. ConduitM i o m r\r\n\r\ntag :: forall m a b c o . Monad m =>\r\n ConduitM Event o m (Maybe c)\r\ntag = do\r\n _ <- dropWS\r\n return undefined\r\n where\r\n-- Add this and it works\r\n-- dropWS :: Monad m => ConduitM Event o m (Maybe Event)\r\n dropWS = do\r\n-- Swap these two lines and it works\r\n-- let x = undefined\r\n x <- peek\r\n let isWS =\r\n case x of\r\n -- Remove some of these and it works\r\n Just EventBeginDocument -> True\r\n Just EventEndDocument -> True\r\n Just EventBeginDoctype{} -> True\r\n Just EventEndDoctype -> True\r\n Just EventInstruction{} -> True\r\n Just EventBeginElement{} -> False\r\n Just EventEndElement{} -> False\r\n Just (EventContent (ContentText t))\r\n | all isSpace t -> True\r\n | otherwise -> False\r\n Just (EventContent ContentEntity{}) -> False\r\n Just EventComment{} -> True\r\n Just EventCDATA{} -> False\r\n Nothing -> False\r\n if isWS then dropWS else return x\r\n\r\n-- Inlined Instances\r\n\r\ninstance Functor (ConduitM i o m) where\r\n fmap f (ConduitM c) = ConduitM $ \\rest -> c (rest . f)\r\n\r\ninstance Applicative (ConduitM i o m) where\r\n pure x = ConduitM ($ x)\r\n {-# INLINE pure #-}\r\n (<*>) = ap\r\n {-# INLINE (<*>) #-}\r\n\r\ninstance Monad (ConduitM i o m) where\r\n return = pure\r\n ConduitM f >>= g = ConduitM $ \\h -> f $ \\a -> unConduitM (g a) h\r\n\r\ninstance Monad m => Functor (Pipe l i o u m) where\r\n fmap = liftM\r\n {-# INLINE fmap #-}\r\n\r\ninstance Monad m => Applicative (Pipe l i o u m) where\r\n pure = Done\r\n {-# INLINE pure #-}\r\n (<*>) = ap\r\n {-# INLINE (<*>) #-}\r\n\r\ninstance Monad m => Monad (Pipe l i o u m) where\r\n return = pure\r\n {-# INLINE return #-}\r\n\r\n HaveOutput p c o >>= fp = HaveOutput (p >>= fp) c o\r\n NeedInput p c >>= fp = NeedInput (p >=> fp) (c >=> fp)\r\n Done x >>= fp = fp x\r\n PipeM mp >>= fp = PipeM ((>>= fp) `liftM` mp)\r\n Leftover p i >>= fp = Leftover (p >>= fp) i\r\n\r\nnewtype ConduitM i o m r = ConduitM\r\n { unConduitM :: forall b.\r\n (r -> Pipe i i o () m b) -> Pipe i i o () m b\r\n }\r\n\r\ndata Pipe l i o u m r =\r\n HaveOutput (Pipe l i o u m r) (m ()) o\r\n | NeedInput (i -> Pipe l i o u m r) (u -> Pipe l i o u m r)\r\n | Done r\r\n | PipeM (m (Pipe l i o u m r))\r\n | Leftover (Pipe l i o u m r) l\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1Georgios KarachaliasGeorgios Karachaliashttps://gitlab.haskell.org/ghc/ghc/-/issues/6124Spurious non-exhaustive warning with GADT and newtypes2019-09-30T21:37:27ZjoeyadamsSpurious non-exhaustive warning with GADT and newtypesThis may be related to #3927 or similar, but here's another case where the compiler produces a "Pattern match(es) are non-exhaustive" warning for patterns on a GADT that are impossible to implement:
```
newtype A = MkA Int
newtype B = M...This may be related to #3927 or similar, but here's another case where the compiler produces a "Pattern match(es) are non-exhaustive" warning for patterns on a GADT that are impossible to implement:
```
newtype A = MkA Int
newtype B = MkB Char
data T a where
A :: T A
B :: T B
f :: T A -> A
f A = undefined
```
This produces the following warning:
```
Warning: Pattern match(es) are non-exhaustive
In an equation for `f': Patterns not matched: B
```
It is impossible to write a pattern for `B` because `B :: T B` does not match `T A`.
If I replace `newtype` with `data` for both `A` and `B`, the warning goes away. If I replace only one instance of either `newtype`, it will still produce the warning.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.4.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Spurious non-exhaustive warning with GADT and newtypes","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.4.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This may be related to #3927 or similar, but here's another case where the compiler produces a \"Pattern match(es) are non-exhaustive\" warning for patterns on a GADT that are impossible to implement:\r\n\r\n{{{\r\nnewtype A = MkA Int\r\nnewtype B = MkB Char\r\n\r\ndata T a where\r\n A :: T A\r\n B :: T B\r\n\r\nf :: T A -> A\r\nf A = undefined\r\n}}}\r\n\r\nThis produces the following warning:\r\n\r\n{{{\r\n Warning: Pattern match(es) are non-exhaustive\r\n In an equation for `f': Patterns not matched: B\r\n}}}\r\n\r\nIt is impossible to write a pattern for {{{B}}} because {{{B :: T B}}} does not match {{{T A}}}.\r\n\r\nIf I replace {{{newtype}}} with {{{data}}} for both {{{A}}} and {{{B}}}, the warning goes away. If I replace only one instance of either {{{newtype}}}, it will still produce the warning.","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1https://gitlab.haskell.org/ghc/ghc/-/issues/3927Incomplete/overlapped pattern warnings + GADTs = inadequate2019-09-30T21:35:45ZSimon Peyton JonesIncomplete/overlapped pattern warnings + GADTs = inadequateConsider these defintions
```
data T a where
T1 :: T Int
T2 :: T Bool
-- f1 should be exhaustive
f1 :: T a -> T a -> Bool
f1 T1 T1 = True
f1 T2 T2 = False
-- f2 is exhaustive too, even more obviously
f2 :: T a -> T a -> Bool
f2 T1...Consider these defintions
```
data T a where
T1 :: T Int
T2 :: T Bool
-- f1 should be exhaustive
f1 :: T a -> T a -> Bool
f1 T1 T1 = True
f1 T2 T2 = False
-- f2 is exhaustive too, even more obviously
f2 :: T a -> T a -> Bool
f2 T1 (T1 :: T Int) = True
f2 T2 (T2 :: T Bool) = False
-- f3's first equation is unreachable
f3 :: T a -> T a -> Bool
f3 T2 T1 = False
f3 _ _ = True
```
With HEAD (GHC 6.13) we get
```
G1.hs:11:1:
Warning: Pattern match(es) are non-exhaustive
In the definition of `f1':
Patterns not matched:
T1 T2
T2 T1
```
This is wrong.
- `f1` should behave like `f2`, and be accepted without warning.
- `f3` has an inaccessible branch that is not reported.
The type checker accepts just the right programs, but the rather simple-minded approach to overlap warnings isn't doing the right thing.
Note to self: the reason is that `tcPat` does not insert a coercion on the second arg to narrow the type, because there's no *type* reason to do so. So for `f1` we get
```
f1 a (x:T a) (y:T a)
= case x of { T1 (cox:a~Int) ->
case y of { T1 (coy:a~Int) -> ... }
```
In the inner case it's not obvious that T2 is inaccessible. If we refined eagerly we might get
```
f1 a (x:T a) (y:T a)
= case x of { T1 (cox:a~Int) ->
case (y |> T cox) of { T1 (coy:Int~Int) -> ... }
```
and now the scrutinee of the inner case has type `(T Int)` and the `T2` constructor obviously can't occur.
Fix this with the new inference engine.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 6.12.1 |
| 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":"Incomplete/overlapped pattern warnings + GADTs = inadequate","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"6.12.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider these defintions\r\n{{{\r\ndata T a where\r\n T1 :: T Int\r\n T2 :: T Bool\r\n\r\n-- f1 should be exhaustive\r\nf1 :: T a -> T a -> Bool\r\nf1 T1 T1 = True\r\nf1 T2 T2 = False\r\n\r\n-- f2 is exhaustive too, even more obviously\r\nf2 :: T a -> T a -> Bool\r\nf2 T1 (T1 :: T Int) = True\r\nf2 T2 (T2 :: T Bool) = False\r\n\r\n-- f3's first equation is unreachable\r\nf3 :: T a -> T a -> Bool\r\nf3 T2 T1 = False\r\nf3 _ _ = True \r\n}}}\r\nWith HEAD (GHC 6.13) we get\r\n{{{\r\nG1.hs:11:1:\r\n Warning: Pattern match(es) are non-exhaustive\r\n In the definition of `f1':\r\n Patterns not matched:\r\n T1 T2\r\n T2 T1\r\n}}}\r\nThis is wrong. \r\n * `f1` should behave like `f2`, and be accepted without warning.\r\n * `f3` has an inaccessible branch that is not reported.\r\n\r\nThe type checker accepts just the right programs, but the rather simple-minded approach to overlap warnings isn't doing the right thing. \r\n\r\nNote to self: the reason is that `tcPat` does not insert a coercion on the second arg to narrow the type, because there's no ''type'' reason to do so. So for `f1` we get\r\n{{{\r\nf1 a (x:T a) (y:T a)\r\n = case x of { T1 (cox:a~Int) ->\r\n case y of { T1 (coy:a~Int) -> ... }\r\n}}}\r\nIn the inner case it's not obvious that T2 is inaccessible. If we refined eagerly we might get\r\n{{{\r\nf1 a (x:T a) (y:T a)\r\n = case x of { T1 (cox:a~Int) ->\r\n case (y |> T cox) of { T1 (coy:Int~Int) -> ... }\r\n}}}\r\nand now the scrutinee of the inner case has type `(T Int)` and the `T2` constructor obviously can't occur.\r\n\r\nFix this with the new inference engine.","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1Simon Peyton JonesSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc/-/issues/595Overhaul GHC's overlapping/non-exhaustive pattern checking2019-09-30T21:34:22ZSimon MarlowOverhaul GHC's overlapping/non-exhaustive pattern checkingGHC has a module in the desugarer (Check) which checks whether patterns are overlapping and/or exhaustive, to support the flags -fwarn-overlapping-patterns and -fwarn-non-exhaustive-patterns. The code is old and crufty, and has several o...GHC has a module in the desugarer (Check) which checks whether patterns are overlapping and/or exhaustive, to support the flags -fwarn-overlapping-patterns and -fwarn-non-exhaustive-patterns. The code is old and crufty, and has several outstanding bugs. A rewrite is needed.8.0.1