diff options
Diffstat (limited to 'testsuite/tests/typecheck/should_compile/T16204a.hs')
-rw-r--r-- | testsuite/tests/typecheck/should_compile/T16204a.hs | 58 |
1 files changed, 58 insertions, 0 deletions
diff --git a/testsuite/tests/typecheck/should_compile/T16204a.hs b/testsuite/tests/typecheck/should_compile/T16204a.hs new file mode 100644 index 0000000000..63cae41d8c --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/T16204a.hs @@ -0,0 +1,58 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +module T16204 where + +import Data.Kind + +----- +-- singletons machinery +----- + +data family Sing :: forall k. k -> Type +data SomeSing :: Type -> Type where + SomeSing :: Sing (a :: k) -> SomeSing k + +----- +-- (Simplified) GHC.Generics +----- + +class Generic (a :: Type) where + type Rep a :: Type + from :: a -> Rep a + to :: Rep a -> a + +class PGeneric (a :: Type) where + -- type PFrom ... + type PTo (x :: Rep a) :: a + +class SGeneric k where + -- sFrom :: ... + sTo :: forall (a :: Rep k). Sing a -> Sing (PTo a :: k) + +----- + +class SingKind k where + type Demote k :: Type + -- fromSing :: ... + toSing :: Demote k -> SomeSing k + +genericToSing :: forall k. + ( SingKind k, SGeneric k, SingKind (Rep k) + , Generic (Demote k), Rep (Demote k) ~ Demote (Rep k) ) + => Demote k -> SomeSing k +genericToSing d = withSomeSing @(Rep k) (from d) $ SomeSing . sTo + +withSomeSing :: forall k r + . SingKind k + => Demote k + -> (forall (a :: k). Sing a -> r) + -> r +withSomeSing x f = + case toSing x of + SomeSing x' -> f x' |