Opened 6 weeks ago

Closed 5 weeks ago

Last modified 5 weeks ago

#14228 closed bug (fixed)

PatternSynonyms Non-exhaustive with UnboxedSums

Reported by: guibou Owned by:
Priority: normal Milestone: 8.2.2
Component: Compiler Version: 8.2.1
Keywords: UnboxedSums, PatternSynonyms Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Incorrect result at runtime Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s): Phab:D3951
Wiki Page:

Description

The following implementation of Maybe using UnboxedSums results in Non-exhaustive patterns in case:

(Failure.hs file)

{-# LANGUAGE UnboxedSums #-}
{-# LANGUAGE PatternSynonyms #-}

type Maybe' t = (# t | () #)

pattern Just' :: a -> Maybe' a
pattern Just' x = (# x | #)

pattern Nothing' :: Maybe' a
pattern Nothing' = (# | () #)

foo x = case x of
  Nothing' -> putStrLn "nothing"
  Just' _ -> putStrLn "just"

main = do
  putStrLn "Nothing'"
  foo Nothing'

  putStrLn "Just'"
  foo (Just' "hello")

When executed, it prints:

Nothing'
nothing
Just'
Failure: Failure.hs:10:20-29: Non-exhaustive patterns in case

Compiled with ghc Failure.hs.

Please note that by removing the patterns, and writting foo as following works as expected:

foo x = case x of
  (# | () #) -> putStrLn "nothing"
  (# _ | #) -> putStrLn "just"

Change History (6)

comment:1 Changed 6 weeks ago by RyanGlScott

Keywords: UnboxedSums added; UnboxedSum removed

Wow! Great catch.

Indeed, the ddump-simpl output for that program looks mighty suspicious. I'll post an abridged version below:

-- RHS size: {terms: 14, types: 20, coercions: 0, joins: 0/0}
$mJust'
  :: forall (r :: TYPE rep) a.
     Maybe' a -> (a -> r) -> (Void# -> r) -> r
$mJust'
  = \ (@ (rep :: RuntimeRep))
      (@ (r :: TYPE rep))
      (@ a)
      (scrut :: Maybe' a)
      (cont :: a -> r)
      _ ->
      case scrut of {
        (#_|#) x -> cont x;
        (#|_#) ipv -> patError "Bug.hs:8:19-27|case"#
      }

-- RHS size: {terms: 17, types: 21, coercions: 0, joins: 0/0}
$mNothing'
  :: forall (r :: TYPE rep) a.
     Maybe' a -> (Void# -> r) -> (Void# -> r) -> r
$mNothing'
  = \ (@ (rep :: RuntimeRep))
      (@ (r :: TYPE rep))
      (@ a)
      (scrut :: Maybe' a)
      (cont :: Void# -> r)
      _ ->
      case scrut of {
        (#_|#) ipv -> patError "Bug.hs:11:20-29|case"#;
        (#|_#) ds -> case ds of { () -> cont void# }
      }

Just look at that rubbish! The matchers for Just' and Nothing' each take a failure continuation as an argument, but appear to ignore them completely and just proceed directly to patError in case the expected pattern wasn't matched.

comment:2 Changed 6 weeks ago by RyanGlScott

Differential Rev(s): Phab:D3951
Milestone: 8.2.2
Status: newpatch

comment:3 Changed 5 weeks ago by Ben Gamari <ben@…>

In f4d50a0e/ghc:

Fix #14228 by marking SumPats as non-irrefutable

`isIrrefutableHsPat` should always return `False` for unboxed sum
patterns (`SumPat`s), since they always have at least one other
corresponding pattern of the same arity (since the minimum arity for a
`SumPat` is 2). Failure to do so causes incorrect code to be generated
for pattern synonyms that use unboxed sums, as shown in #14228.

Test Plan: make test TEST=T14228

Reviewers: austin, bgamari, simonpj

Reviewed By: simonpj

Subscribers: simonpj, rwbarton, thomie

GHC Trac Issues: #14228

Differential Revision: https://phabricator.haskell.org/D3951

comment:4 Changed 5 weeks ago by bgamari

Status: patchmerge

comment:5 Changed 5 weeks ago by bgamari

Resolution: fixed
Status: mergeclosed

comment:6 Changed 5 weeks ago by bgamari

Note: See TracTickets for help on using tickets.