blob: 1dcfe756f917ceac597347fe8957466a170c5bb7 (
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
|
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# OPTIONS_GHC -Wall #-}
module T14813 where
import Data.Kind
import Data.Void
data SBool (z :: Bool) where
SFalse :: SBool 'False
STrue :: SBool 'True
type family F (b :: Bool) (a :: Type) :: Type where
F 'True a = a
F 'False _ = Void
dispatch :: forall (b :: Bool) (a :: Type). SBool b -> F b a -> a
dispatch STrue x = x
dispatch SFalse x = case x of {}
type family G a
type instance G Int = Void
fun :: i ~ Int => G i -> a
fun x = case x of {}
|
