PatternSynonyms Non-exhaustive with UnboxedSums

[guibou]

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"

[RyanGlScott]

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.

[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

[bgamari]

comment:3 merged to ghc-8.2 as fb5190185b6819ff4f4b64167d37da85337c524c.