Fix #16188
[ghc.git] / testsuite / tests / typecheck / should_compile / T16204b.hs
1 {-# LANGUAGE DataKinds #-}
2 {-# LANGUAGE FlexibleContexts #-}
3 {-# LANGUAGE GADTs #-}
4 {-# LANGUAGE PolyKinds #-}
5 {-# LANGUAGE RankNTypes #-}
6 {-# LANGUAGE ScopedTypeVariables #-}
7 {-# LANGUAGE TypeApplications #-}
8 {-# LANGUAGE TypeFamilies #-}
9 module T16204b where
10
11 import Data.Kind
12
13 -----
14 -- singletons machinery
15 -----
16
17 data family Sing :: forall k. k -> Type
18 data SomeSing :: Type -> Type where
19 SomeSing :: Sing (a :: k) -> SomeSing k
20
21 -----
22 -- (Simplified) GHC.Generics
23 -----
24
25 class Generic (a :: Type) where
26 type Rep a :: Type
27 from :: a -> Rep a
28 to :: Rep a -> a
29
30 class PGeneric (a :: Type) where
31 -- type PFrom ...
32 type PTo (x :: Rep a) :: a
33
34 class SGeneric k where
35 -- sFrom :: ...
36 sTo :: forall (a :: Rep k). Sing a -> Sing (PTo a :: k)
37
38 -----
39
40 class SingKind k where
41 type Demote k :: Type
42 -- fromSing :: ...
43 toSing :: Demote k -> SomeSing k
44
45 genericToSing :: forall k.
46 ( SingKind k, SGeneric k, SingKind (Rep k)
47 , Generic (Demote k), Rep (Demote k) ~ Demote (Rep k) )
48 => Demote k -> SomeSing k
49 genericToSing d = withSomeSing (from d) $ SomeSing . sTo
50
51 withSomeSing :: forall k r
52 . SingKind k
53 => Demote k
54 -> (forall (a :: k). Sing a -> r)
55 -> r
56 withSomeSing x f =
57 case toSing x of
58 SomeSing x' -> f x'