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.