blob: 5c89ab278d72da396dae1105dd36a51b2d980452 (
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
30
31
32
33
34
35
36
37
38
39
40
|
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE StandaloneKindSignatures #-}
module T21338 where
import Data.Kind ( Type, Constraint )
import Data.Proxy ( Proxy(..) )
newtype K a b = K a
type NP :: (Type -> Type) -> [Type] -> Type
data NP f xs where
data FieldInfo a
type All :: [Type] -> Constraint
type family All xs where {}
data ConstructorInfo :: [Type] -> Type where
Record :: All xs => NP (K String) xs -> ConstructorInfo xs
hmap :: (forall a. f a -> g a) -> h f xs -> h g xs
hmap _ _ = undefined
foo :: forall a flds. ConstructorInfo flds
foo = undefined
fieldNames :: forall (a :: Type) flds. NP (K String) flds
fieldNames = case foo @a {- @flds -} of
Record np -> hmap id np
_ -> hmap undefined @flds
-- The last line caused a "No skolem info" panic on GHC 9.2 and below.
|
