Simon Peyton Jones pushed to branch wip/T23162-part2 at Glasgow Haskell Compiler / GHC Commits: bfff257c by Simon Peyton Jones at 2025-12-12T10:46:55+00:00 Wibbles - - - - - 4 changed files: - testsuite/tests/indexed-types/should_fail/T26176.stderr - testsuite/tests/pmcheck/should_compile/T15753c.hs - + testsuite/tests/pmcheck/should_compile/T22652.hs - testsuite/tests/pmcheck/should_compile/all.T Changes: ===================================== testsuite/tests/indexed-types/should_fail/T26176.stderr ===================================== @@ -1,9 +1,7 @@ -T26176.hs:18:7: error: [GHC-83865] - • Couldn't match type ‘FA t’ with ‘5’ - Expected: SNat 5 - Actual: SNat (FA t) - • In the expression: b - In an equation for ‘a’: a = b +T26176.hs:29:7: error: [GHC-64725] + • Cannot satisfy: FA t <= FB t + • In the expression: bar @t + In an equation for ‘x’: x = bar @t In an equation for ‘foo’: foo = undefined @@ -14,30 +12,4 @@ T26176.hs:18:7: error: [GHC-83865] b = undefined c :: SNat 3 ... - • Relevant bindings include - b :: SNat (FA t) (bound at T26176.hs:21:3) - d :: SNat (FB t) (bound at T26176.hs:27:3) - x :: p0 t (bound at T26176.hs:29:3) - foo :: p t (bound at T26176.hs:15:1) - -T26176.hs:24:7: error: [GHC-83865] - • Couldn't match type ‘FB t’ with ‘3’ - Expected: SNat 3 - Actual: SNat (FB t) - • In the expression: d - In an equation for ‘c’: c = d - In an equation for ‘foo’: - foo - = undefined - where - a :: SNat 5 - a = b - b :: SNat (FA t) - b = undefined - c :: SNat 3 - ... - • Relevant bindings include - d :: SNat (FB t) (bound at T26176.hs:27:3) - x :: p0 t (bound at T26176.hs:29:3) - foo :: p t (bound at T26176.hs:15:1) ===================================== testsuite/tests/pmcheck/should_compile/T15753c.hs ===================================== @@ -34,6 +34,22 @@ type family F (u1 :: ()) (u2 :: ()) :: Type where type family Case (u :: ()) :: Type where Case '() = Int +--------------------------------------- +-- The checker can (now, Dec 25) see that (F u1 u2 ~ Char) is +-- unsatisfiable, so the empty pattern match is fine +g1a :: F u1 u2 :~: Char -> SUnit u1 -> SUnit u2 -> Void +g1a r _ _ = case r of {} + +{- Why [G] F u1 u2 ~ Char is unsatisfiable + +[G] F u1 u2 ~ Char =>rewrite [G] If (IsUnit u1) (Case u2) Int ~ Char + =>(fundep) [W] IsUnit u1 ~ True + [W] Case u2 ~ Char <<-- insoluble: no relevant eqns +-} + +--------------------------------------- +-- This older test matches on Refl (which is unsatisfiable) +-- but we now get complaints from inside g1 :: F u1 u2 :~: Char -> SUnit u1 -> SUnit u2 -> Void @@ -41,21 +57,7 @@ g1 Refl su1 su2 | STrue <- sIsUnit su1 = case su2 of {} --- g1a :: F u1 u2 :~: Char -> SUnit u1 -> SUnit u2 -> Void --- g1a r _ _ = case r of {} -- Why does this complain about missing Refl -{- [G] F u1 u2 ~ Char - [W] SBool (IsUnit u1) ~ SBool True -==> - [W] IsUnit u1 ~ True -==> fundep - u1 ~ () - - -[G] F u1 u2 ~ Char =>(fundep) [W] If (IsUnit u1) (Case u2) Int ~ Char - =>(fundep) [W] IsUnit u1 ~ True - [W] Case u2 ~ Char <<-- insoluble: no relevant eqns --} g2 :: F u1 u2 :~: Char -> SUnit u1 -> SUnit u2 @@ -64,4 +66,3 @@ g2 Refl su1 su2 = case sIsUnit su1 of STrue -> case su2 of {} - ===================================== testsuite/tests/pmcheck/should_compile/T22652.hs ===================================== @@ -0,0 +1,17 @@ +{-# LANGUAGE DataKinds, TypeFamilies, GADTs #-} +{-# OPTIONS_GHC -Wincomplete-patterns -Werror #-} + +module T22652 where + +data T = Z | S + +data ST n where + SZ :: ST Z + SS :: ST S + +type family F n where + F Z = Z + F S = Z + +f :: F m ~ n => ST m -> ST n -> () +f _ SZ = () ===================================== testsuite/tests/pmcheck/should_compile/all.T ===================================== @@ -179,3 +179,4 @@ test('T24824', normal, compile, ['-package ghc -Wincomplete-record-selectors']) test('T24891', normal, compile, ['-Wincomplete-record-selectors']) test('T25257', normal, compile, [overlapping_incomplete]) test('T24845', [], compile, [overlapping_incomplete]) +test('T22652', [], compile, [overlapping_incomplete]) View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/bfff257ca6d35572eec23ae84a8cb872... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/bfff257ca6d35572eec23ae84a8cb872... You're receiving this email because of your account on gitlab.haskell.org.