blob: 5054b43a2c1ba4b5f7231549c69b50870145bbf9 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
|
{-# LANGUAGE TypeApplications, ScopedTypeVariables, GADTs, RankNTypes,
PolyKinds, KindSignatures #-}
{-# OPTIONS_GHC -O2 #-} -- We are provoking a bug in SpecConstr
module T14270a where
import Data.Kind
import Data.Proxy
data T a = T1 (T a) | T2
data K (a :: k) where
K1 :: K (a :: Type)
K2 :: K a
f :: T (a :: Type) -> Bool
f (T1 x) = f x
f T2 = True
g :: forall (a :: k). K a -> T a -> Bool
g kv x = case kv of
K1 -> f @a T2 -- f @a (T1 x) gives a different crash
k2 -> True
-- The point here is that the call to f looks like
-- f @(a |> co) (T2 @(a |> co))
-- where 'co' is bound by the pattern match on K1
-- See Note [SpecConstr and casts] in SpecConstr
|
