testsuite: Assert that testsuite ways are known
[ghc.git] / testsuite / tests / typecheck / should_compile / T16188.hs
1 {-# LANGUAGE DataKinds #-}
2 {-# LANGUAGE GADTs #-}
3 {-# LANGUAGE PolyKinds #-}
4 {-# LANGUAGE ScopedTypeVariables #-}
5 {-# LANGUAGE TypeFamilies #-}
6 {-# LANGUAGE TypeOperators #-}
7 {-# LANGUAGE UndecidableInstances #-}
8 module T16188 where
9
10 import Data.Kind (Type)
11 import Data.Type.Bool (type (&&))
12
13 data TyFun :: Type -> Type -> Type
14 type a ~> b = TyFun a b -> Type
15 infixr 0 ~>
16 type family Apply (f :: a ~> b) (x :: a) :: b
17 data family Sing :: forall k. k -> Type
18
19 data instance Sing :: Bool -> Type where
20 SFalse :: Sing False
21 STrue :: Sing True
22
23 (%&&) :: forall (x :: Bool) (y :: Bool).
24 Sing x -> Sing y -> Sing (x && y)
25 SFalse %&& _ = SFalse
26 STrue %&& a = a
27
28 data RegExp :: Type -> Type where
29 App :: RegExp t -> RegExp t -> RegExp t
30
31 data instance Sing :: forall t. RegExp t -> Type where
32 SApp :: Sing re1 -> Sing re2 -> Sing (App re1 re2)
33
34 data ReNotEmptySym0 :: forall t. RegExp t ~> Bool
35 type instance Apply ReNotEmptySym0 r = ReNotEmpty r
36
37 type family ReNotEmpty (r :: RegExp t) :: Bool where
38 ReNotEmpty (App re1 re2) = ReNotEmpty re1 && ReNotEmpty re2
39
40 sReNotEmpty :: forall t (r :: RegExp t).
41 Sing r -> Sing (Apply ReNotEmptySym0 r :: Bool)
42 sReNotEmpty (SApp sre1 sre2) = sReNotEmpty sre1 %&& sReNotEmpty sre2
43
44 blah :: forall (t :: Type) (re :: RegExp t).
45 Sing re -> ()
46 blah (SApp sre1 sre2)
47 = case (sReNotEmpty sre1, sReNotEmpty sre2) of
48 (STrue, STrue) -> ()