Pattern match checking open unions
The combination of type classes, view patterns and pattern synonyms make it possible to encode open unions (see also #11336 (closed), #17112 (closed)). Example:
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
module Bug where
class Member a b where
-- | Try to get an @a@ out of a @b@
prj :: b -> Maybe a
pattern O :: Member a b => a -> b
pattern O a <- (prj -> Just a)
-- Example usage:
data A = A
data B = B
-- | Matches on an open union with members of type 'A' and 'B'.
fun :: (Member B a, Member A a) => a -> ()
fun (O A) = ()
fun (O B) = ()
fun _ = error "some other member of the union we where not prepared for"
-- Concrete function:
data AB = AA A | BB B
instance Member A AB where
prj (AA a) = Just a
prj _ = Nothing
instance Member B AB where
prj (BB b) = Just b
prj _ = Nothing
{-# COMPLETE O :: AB #-}
-- | Same as above, but now we see the COMPLETE set attached to 'AB'.
fun2 :: AB -> ()
fun2 (O A) = ()
fun2 (O B) = ()
If you check this with GHC 8.6.5 or GHC 8.8.1, this reports no warnings, as expected.
With GHC HEAD and the fix we are probably going to backport from !1625 (closed) for 8.8.2, this leads to a crash. I will have to investigate why, but the behavior I would actually expect is the one that !963 (closed) produces, namely this warning:
T17149.hs:43:1: warning: [-Woverlapping-patterns]
Pattern match is redundant
In an equation for ‘fun2’: fun2 (O B) = ...
|
43 | fun2 (O B) = ()
| ^^^^^^^^^^^^^^^
It unsoundly reports the last line as redundant. Here's why:
By the COMPLETE annotation, the pattern match checker regards anything as a complete match over AB
that matches on O a
and also matches all cases of a
exhaustively. Now in the first clause of fun2
, by the fix of !1625 (closed), we give that a
type A
. A
itself has a vanilla COMPLETE set attached to it, meaning that it is enough to match on the A
data constructor to completely overlap a
. And that's in fact what happens here! So by this reasoning, the first line is a COMPLETE match, which is of course wrong considering a call like fun2 (BB B)
.
The point where things went south is when we gave a
type A
, which is true for that particular clause, but doesn't consider the following clauses. The actual type we want to instantiate a
to is forall a. (Member A a, Member B a) => a
, like in the first example.
Sadly, the approach from !1625 (closed) where we lean on the type-checker isn't able to provide us with that amount of polymorphism. Other than looking at required thetas to figure things out, I'm not really sure what to do here. Also this has pervasive effect on the way we regard COMPLETE sets: The most precise approximation to a COMPLETE set for a
would be {A, B}
, the constructors of which aren't even part of the same TyCon. We should probably just discard COMPLETE sets altogether in these cases.
With the knowledge of #17149 (comment 220355), here's a smaller reproduction of the crash:
{-# OPTIONS_GHC -Wincomplete-patterns #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE MultiParamTypeClasses #-}
module Bug where
class Member a b where
prj :: b -> Maybe a
pattern P :: Member a b => a -> b
pattern P a <- (prj -> Just a)
{-# COMPLETE P :: Bool #-}
-- | Trying to instantiate P with 0 type arguments doesn't work, it takes 2.
-- This seemingly unrelated fact, only relevant through the COMPLETE set, may
-- not lead the compiler to crash or do shady stuff.
fun :: Bool -> ()
fun True = ()
fun _ = ()