[Git][ghc/ghc][wip/T17977] 2 commits: Expect T4267 to pass

[Sebastian Graf]

Sebastian Graf pushed to branch wip/T17977 at Glasgow Haskell Compiler / GHC


Commits:
f024b6e3 by Sylvain Henry at 2020-03-30T12:48:39+02:00
Expect T4267 to pass

Since 54250f2d8de910b094070c1b48f086030df634b1 we expected T4267 to
fail, but it passes on CI.

- - - - -
57342858 by Sebastian Graf at 2020-03-30T17:54:36-04:00
PmCheck: Adjust recursion depth for nonVoid test

In #17977, we ran into the reduction depth limit of the typechecker.
That was only a symptom of a much broader issue: The recursion depth
of the coverage checker for trying to instantiate strict fields in the
`nonVoid` test was far too high (100, the `defaultMaxTcBound`).

As a result, we were performing quite poorly on `T17977`.
Short of a proper termination analysis to prove emptyness of a type,
we just default to a much lower recursion limit of 3.

Fixes #17977.

- - - - -


6 changed files:

- compiler/GHC/HsToCore/PmCheck/Oracle.hs
- testsuite/tests/perf/should_run/all.T
- + testsuite/tests/pmcheck/should_compile/T17977.hs
- + testsuite/tests/pmcheck/should_compile/T17977b.hs
- + testsuite/tests/pmcheck/should_compile/T17977b.stderr
- testsuite/tests/pmcheck/should_compile/all.T


Changes:

=====================================
compiler/GHC/HsToCore/PmCheck/Oracle.hs
=====================================
@@ -1322,7 +1322,7 @@ checkAllNonVoid rec_ts amb_cs strict_arg_tys = do
   let rec_max_bound | tys_to_check `lengthExceeds` 1
                     = 1
                     | otherwise
-                    = defaultRecTcMaxBound
+                    = 3
       rec_ts' = setRecTcMaxBound rec_max_bound rec_ts
   allM (nonVoid rec_ts' amb_cs) tys_to_check
 


=====================================
testsuite/tests/perf/should_run/all.T
=====================================
@@ -233,8 +233,7 @@ test('T5949',
      ['-O'])
 
 test('T4267',
-     [expect_broken(4267),
-      collect_stats('bytes allocated',10),
+     [collect_stats('bytes allocated',10),
       only_ways(['normal'])],
       compile_and_run,
       ['-O'])


=====================================
testsuite/tests/pmcheck/should_compile/T17977.hs
=====================================
@@ -0,0 +1,33 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+module Bug where
+
+import Data.Kind
+import Data.Type.Equality
+
+data Nat = Z | S Nat
+
+data SNat :: Nat -> Type where
+  SZ :: SNat Z
+  SS :: SNat n -> SNat (S n)
+
+type family S' (n :: Nat) :: Nat where
+  S' n = S n
+
+data R :: Nat -> Nat -> Nat -> Type where
+  MkR :: !(R m n o) -> R (S m) n (S o)
+
+type family NatPlus (m :: Nat) (n :: Nat) :: Nat where
+  NatPlus Z     n = n
+  NatPlus (S m) n = S' (NatPlus m n)
+
+f :: forall (m :: Nat) (n :: Nat) (o :: Nat).
+     SNat m -> SNat n -> SNat o
+  -> R m n o -> NatPlus m n :~: o
+f (SS sm) sn (SS so) (MkR r)
+  | Refl <- f sm sn so r
+  = Refl


=====================================
testsuite/tests/pmcheck/should_compile/T17977b.hs
=====================================
@@ -0,0 +1,24 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE EmptyCase #-}
+module Bug where
+
+import Data.Kind
+
+data Nat = Z | S Nat
+
+data Down :: Nat -> Type where
+  Down :: !(Down n) -> Down (S n)
+
+data Up :: Nat -> Type where
+  Up :: !(Up (S n)) -> Up n
+
+f :: Down n -> ()
+f (Down r) = ()
+
+f' :: Down (S (S (S (S Z)))) -> ()
+f' (Down r) = ()
+
+g :: Up n -> ()
+g (Up r) = ()


=====================================
testsuite/tests/pmcheck/should_compile/T17977b.stderr
=====================================
@@ -0,0 +1,4 @@
+
+T17977b.hs:21:1: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match has inaccessible right hand side
+    In an equation for ‘f'’: f' (Down r) = ...


=====================================
testsuite/tests/pmcheck/should_compile/all.T
=====================================
@@ -114,6 +114,10 @@ test('T17703', normal, compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T17783', normal, compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T17977', collect_compiler_stats('bytes allocated',10), compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T17977b', collect_compiler_stats('bytes allocated',10), compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 
 # Other tests
 test('pmc001', [], compile,



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/a2226015e76fed5041aac59433c60e4379f8d73e...5734285808c549ebe505089b0cbf9afe7089e857

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/a2226015e76fed5041aac59433c60e4379f8d73e...5734285808c549ebe505089b0cbf9afe7089e857
You're receiving this email because of your account on gitlab.haskell.org.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20200330/0e1aec95/attachment-0001.html>