Simon Jakobi pushed to branch wip/sjakobi/regression-tests-2 at Glasgow Haskell Compiler / GHC
Commits:
-
f917ac96
by Simon Jakobi at 2026-03-04T23:34:01+01:00
3 changed files:
- + testsuite/tests/dependent/should_fail/T15588.hs
- + testsuite/tests/dependent/should_fail/T15588.stderr
- testsuite/tests/dependent/should_fail/all.T
Changes:
| 1 | +{- This program used to cause a panic (#15588), but it should possibly even be
|
|
| 2 | +accepted. See #15589. -}
|
|
| 3 | +{-# LANGUAGE AllowAmbiguousTypes #-}
|
|
| 4 | +{-# LANGUAGE DataKinds #-}
|
|
| 5 | +{-# LANGUAGE PolyKinds #-}
|
|
| 6 | +{-# LANGUAGE ScopedTypeVariables #-}
|
|
| 7 | +{-# LANGUAGE TypeFamilies #-}
|
|
| 8 | +{-# LANGUAGE TypeOperators #-}
|
|
| 9 | +module T15588 where
|
|
| 10 | + |
|
| 11 | +import Data.Proxy
|
|
| 12 | +import Data.Type.Equality
|
|
| 13 | +import Data.Type.Bool
|
|
| 14 | +import Data.Kind
|
|
| 15 | + |
|
| 16 | +data SameKind :: forall k. k -> k -> Type
|
|
| 17 | +type family IfK (e :: Proxy (j :: Bool)) (f :: m) (g :: n) :: If j m n where
|
|
| 18 | + IfK (_ :: Proxy True) f _ = f
|
|
| 19 | + IfK (_ :: Proxy False) _ g = g
|
|
| 20 | + |
|
| 21 | +y :: forall ck (c :: ck). ck :~: Proxy True -> ()
|
|
| 22 | +y Refl = let x :: forall a b (d :: a). SameKind (IfK c b d) d
|
|
| 23 | + x = undefined
|
|
| 24 | + in ()
|
|
| 25 | + |
| 1 | +T15588.hs:18:9: error: [GHC-25897]
|
|
| 2 | + • Couldn't match kind ‘j’ with ‘True’
|
|
| 3 | + Expected kind ‘Proxy j’,
|
|
| 4 | + but ‘_ :: Proxy True’ has kind ‘Proxy True’
|
|
| 5 | + • In the first argument of ‘IfK’, namely ‘(_ :: Proxy True)’
|
|
| 6 | + In the type family declaration for ‘IfK’
|
|
| 7 | + |
| ... | ... | @@ -34,6 +34,7 @@ test('T15215', normal, compile_fail, ['']) |
| 34 | 34 | test('T15308', normal, compile_fail, ['-fno-print-explicit-kinds'])
|
| 35 | 35 | test('T15343', normal, compile_fail, [''])
|
| 36 | 36 | test('T15380', normal, compile_fail, [''])
|
| 37 | +test('T15588', normal, compile_fail, [''])
|
|
| 37 | 38 | test('T15591b', normal, compile_fail, [''])
|
| 38 | 39 | test('T15591c', normal, compile_fail, [''])
|
| 39 | 40 | test('T15743c', normal, compile_fail, [''])
|