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
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:
| 1 | -T26176.hs:18:7: error: [GHC-83865]
|
|
| 2 | - • Couldn't match type ‘FA t’ with ‘5’
|
|
| 3 | - Expected: SNat 5
|
|
| 4 | - Actual: SNat (FA t)
|
|
| 5 | - • In the expression: b
|
|
| 6 | - In an equation for ‘a’: a = b
|
|
| 1 | +T26176.hs:29:7: error: [GHC-64725]
|
|
| 2 | + • Cannot satisfy: FA t <= FB t
|
|
| 3 | + • In the expression: bar @t
|
|
| 4 | + In an equation for ‘x’: x = bar @t
|
|
| 7 | 5 | In an equation for ‘foo’:
|
| 8 | 6 | foo
|
| 9 | 7 | = undefined
|
| ... | ... | @@ -14,30 +12,4 @@ T26176.hs:18:7: error: [GHC-83865] |
| 14 | 12 | b = undefined
|
| 15 | 13 | c :: SNat 3
|
| 16 | 14 | ...
|
| 17 | - • Relevant bindings include
|
|
| 18 | - b :: SNat (FA t) (bound at T26176.hs:21:3)
|
|
| 19 | - d :: SNat (FB t) (bound at T26176.hs:27:3)
|
|
| 20 | - x :: p0 t (bound at T26176.hs:29:3)
|
|
| 21 | - foo :: p t (bound at T26176.hs:15:1)
|
|
| 22 | - |
|
| 23 | -T26176.hs:24:7: error: [GHC-83865]
|
|
| 24 | - • Couldn't match type ‘FB t’ with ‘3’
|
|
| 25 | - Expected: SNat 3
|
|
| 26 | - Actual: SNat (FB t)
|
|
| 27 | - • In the expression: d
|
|
| 28 | - In an equation for ‘c’: c = d
|
|
| 29 | - In an equation for ‘foo’:
|
|
| 30 | - foo
|
|
| 31 | - = undefined
|
|
| 32 | - where
|
|
| 33 | - a :: SNat 5
|
|
| 34 | - a = b
|
|
| 35 | - b :: SNat (FA t)
|
|
| 36 | - b = undefined
|
|
| 37 | - c :: SNat 3
|
|
| 38 | - ...
|
|
| 39 | - • Relevant bindings include
|
|
| 40 | - d :: SNat (FB t) (bound at T26176.hs:27:3)
|
|
| 41 | - x :: p0 t (bound at T26176.hs:29:3)
|
|
| 42 | - foo :: p t (bound at T26176.hs:15:1)
|
|
| 43 | 15 |
| ... | ... | @@ -34,6 +34,22 @@ type family F (u1 :: ()) (u2 :: ()) :: Type where |
| 34 | 34 | type family Case (u :: ()) :: Type where
|
| 35 | 35 | Case '() = Int
|
| 36 | 36 | |
| 37 | +---------------------------------------
|
|
| 38 | +-- The checker can (now, Dec 25) see that (F u1 u2 ~ Char) is
|
|
| 39 | +-- unsatisfiable, so the empty pattern match is fine
|
|
| 40 | +g1a :: F u1 u2 :~: Char -> SUnit u1 -> SUnit u2 -> Void
|
|
| 41 | +g1a r _ _ = case r of {}
|
|
| 42 | + |
|
| 43 | +{- Why [G] F u1 u2 ~ Char is unsatisfiable
|
|
| 44 | + |
|
| 45 | +[G] F u1 u2 ~ Char =>rewrite [G] If (IsUnit u1) (Case u2) Int ~ Char
|
|
| 46 | + =>(fundep) [W] IsUnit u1 ~ True
|
|
| 47 | + [W] Case u2 ~ Char <<-- insoluble: no relevant eqns
|
|
| 48 | +-}
|
|
| 49 | + |
|
| 50 | +---------------------------------------
|
|
| 51 | +-- This older test matches on Refl (which is unsatisfiable)
|
|
| 52 | +-- but we now get complaints from inside
|
|
| 37 | 53 | g1 :: F u1 u2 :~: Char
|
| 38 | 54 | -> SUnit u1 -> SUnit u2
|
| 39 | 55 | -> Void
|
| ... | ... | @@ -41,21 +57,7 @@ g1 Refl su1 su2 |
| 41 | 57 | | STrue <- sIsUnit su1
|
| 42 | 58 | = case su2 of {}
|
| 43 | 59 | |
| 44 | --- g1a :: F u1 u2 :~: Char -> SUnit u1 -> SUnit u2 -> Void
|
|
| 45 | --- g1a r _ _ = case r of {} -- Why does this complain about missing Refl
|
|
| 46 | 60 | |
| 47 | -{- [G] F u1 u2 ~ Char
|
|
| 48 | - [W] SBool (IsUnit u1) ~ SBool True
|
|
| 49 | -==>
|
|
| 50 | - [W] IsUnit u1 ~ True
|
|
| 51 | -==> fundep
|
|
| 52 | - u1 ~ ()
|
|
| 53 | - |
|
| 54 | - |
|
| 55 | -[G] F u1 u2 ~ Char =>(fundep) [W] If (IsUnit u1) (Case u2) Int ~ Char
|
|
| 56 | - =>(fundep) [W] IsUnit u1 ~ True
|
|
| 57 | - [W] Case u2 ~ Char <<-- insoluble: no relevant eqns
|
|
| 58 | --}
|
|
| 59 | 61 | |
| 60 | 62 | g2 :: F u1 u2 :~: Char
|
| 61 | 63 | -> SUnit u1 -> SUnit u2
|
| ... | ... | @@ -64,4 +66,3 @@ g2 Refl su1 su2 |
| 64 | 66 | = case sIsUnit su1 of
|
| 65 | 67 | STrue ->
|
| 66 | 68 | case su2 of {} |
| 67 | - |
| 1 | +{-# LANGUAGE DataKinds, TypeFamilies, GADTs #-}
|
|
| 2 | +{-# OPTIONS_GHC -Wincomplete-patterns -Werror #-}
|
|
| 3 | + |
|
| 4 | +module T22652 where
|
|
| 5 | + |
|
| 6 | +data T = Z | S
|
|
| 7 | + |
|
| 8 | +data ST n where
|
|
| 9 | + SZ :: ST Z
|
|
| 10 | + SS :: ST S
|
|
| 11 | + |
|
| 12 | +type family F n where
|
|
| 13 | + F Z = Z
|
|
| 14 | + F S = Z
|
|
| 15 | + |
|
| 16 | +f :: F m ~ n => ST m -> ST n -> ()
|
|
| 17 | +f _ SZ = () |
| ... | ... | @@ -179,3 +179,4 @@ test('T24824', normal, compile, ['-package ghc -Wincomplete-record-selectors']) |
| 179 | 179 | test('T24891', normal, compile, ['-Wincomplete-record-selectors'])
|
| 180 | 180 | test('T25257', normal, compile, [overlapping_incomplete])
|
| 181 | 181 | test('T24845', [], compile, [overlapping_incomplete])
|
| 182 | +test('T22652', [], compile, [overlapping_incomplete]) |