PmCheck: Add regression test cases for examples in "GADTs and Exhaustiveness: Looking for the Impossible"
Jacques Garrigue showed me https://arxiv.org/abs/1702.02281, which has quite a few tricky examples involving GADTs. We should add them as regression tests.
{-# OPTIONS_GHC -Wincomplete-patterns -fforce-recomp #-}
{-# LANGUAGE GADTs, DataKinds, KindSignatures, EmptyCase #-}
-- | All examples from https://arxiv.org/abs/1702.02281
module GarrigueLeNormand where
data N = Z | S N
data Plus :: N -> N -> N -> * where
PlusO :: Plus Z a a
PlusS :: !(Plus a b c) -> Plus (S a) b (S c)
data SMaybe a = SJust !a | SNothing
trivial :: SMaybe (Plus (S Z) Z Z) -> ()
trivial SNothing = ()
trivial2 :: Plus (S Z) Z Z -> ()
trivial2 x = case x of {}
easy :: SMaybe (Plus Z (S Z) Z) -> ()
easy SNothing = ()
easy2 :: Plus Z (S Z) Z -> ()
easy2 x = case x of {}
harder :: SMaybe (Plus (S Z) (S Z) (S Z)) -> ()
harder SNothing = ()
harder2 :: Plus (S Z) (S Z) (S Z) -> ()
harder2 x = case x of {}
invZero :: Plus a b c -> Plus c d Z -> ()
invZero PlusO PlusO = ()
data T a where
A :: T Int
B :: T Bool
C :: T Char
D :: T Float
data U a b c d where
U :: U Int Int Int Int
f :: T a -> T b -> T c -> T d
-> U a b c d
-> ()
f A A A A U = ()
g :: T a -> T b -> T c -> T d
-> T e -> T f -> T g -> T h
-> U a b c d
-> U e f g h
-> ()
g A A A A A A A A U U = ()
They don't currently warn. We should keep it that way (Edit: Except for f
and g
...)!
But f
and g
show serious performance problems: On my quick
flavoured build, the latter function takes nearly 10 minutes (Edit: 32s and 80GB in validate
) to check and allocates over 800GB of memory. Also they are not exhaustive! As can be seen by calling f A B B B undefined
. Bummer, that's a bug (#18670 (closed)).
I think the morale is that throttling ensures linear scaling in the number of clauses ("vertically"), but can't fix exponential runtime in the number of match variables ("horizontally"). And I argue that's OK, because pattern matches rarely reach this kind of horizontal complexity that it makes difficult to cope with. Awareness of the issue should direct the reader to a refactoring that matches on U
first, in which case the checker terminates pretty much instantly.