blob: 3afcd6c24b2e54ca0a438901752369eba3c3efd3 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds, PolyKinds #-}
{-# LANGUAGE StandaloneKindSignatures, ExplicitForAll #-}
module T13780c where
import Data.Kind
import T13780b
type ElimBool ::
forall (p :: Bool -> Type) ->
forall (b :: Bool) ->
Sing b ->
p False ->
p True ->
p b
type family ElimBool p b s pFalse pTrue where
ElimBool _ _ SFalse pFalse _ = pFalse
ElimBool _ _ STrue _ pTrue = pTrue
|
