blob: 7424d821f4922ae846a3bed66fb6e3262cf464ee (
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
29
|
{-# LANGUAGE TypeApplications, ScopedTypeVariables, GADTs, RankNTypes,
PolyKinds, StandaloneKindSignatures #-}
{-# 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
type K :: k -> Type
data K a where
K1 :: K (a :: Type)
K2 :: K a
f :: T (a :: Type) -> Bool
f (T1 x) = f x
f T2 = True
g :: forall k (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
|
