ci: push perf test metrics even when the testsuite doesn't pass
[ghc.git] / testsuite / tests / polykinds / T14873.hs
1 {-# LANGUAGE RankNTypes #-}
2 {-# LANGUAGE ScopedTypeVariables #-}
3 {-# LANGUAGE TypeApplications #-}
4 {-# LANGUAGE TypeFamilies #-}
5 {-# LANGUAGE TypeOperators #-}
6 {-# LANGUAGE DataKinds #-}
7 {-# LANGUAGE PolyKinds #-}
8 module T14873 where
9
10 import Data.Kind (Type)
11
12 data family Sing (a :: k)
13
14 newtype instance Sing (f :: k1 ~> k2) =
15 SLambda { applySing :: forall t. Sing t -> Sing (Apply f t) }
16
17 data TyFun :: Type -> Type -> Type
18 type a ~> b = TyFun a b -> Type
19 infixr 0 ~>
20 type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
21
22 class SingI (a :: k) where
23 sing :: Sing a
24
25 data ColSym1 :: f a -> a ~> Bool
26 type instance Apply (ColSym1 x) y = Col x y
27
28 class PColumn (f :: Type -> Type) where
29 type Col (x :: f a) (y :: a) :: Bool
30
31 class SColumn (f :: Type -> Type) where
32 sCol :: forall a (x :: f a) (y :: a).
33 Sing x -> Sing y -> Sing (Col x y :: Bool)
34
35 instance (SColumn f, SingI x) => SingI (ColSym1 (x :: f a) :: a ~> Bool) where
36 sing = SLambda (sCol (sing @_ @x))
37
38 {- When the bug was present, this smaller kind-incorrect version also
39 elicited the same piResultTy crash
40
41 But it's kind-incorrect, whereas the main test case should compile file
42
43 class SingI (a :: k) where
44
45 class SColumn (f :: Type -> Type) where
46
47 instance -- forall (f :: Type -> Type) a (x :: f a).
48 SColumn f => SingI (x :: f a)
49 -}
50