blob: d80f5179237923d65e29ef1c7b78f6ab3a01eff1 (
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
41
|
{-# OPTIONS_GHC -fforce-recomp -Wincomplete-patterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where
import Data.Kind
import Data.Void
type SFalse = SBool 'False
type STrue = SBool 'True
data SBool :: Bool -> Type where
SFalse :: SFalse
STrue :: STrue
type family F (b :: Bool) :: Type where
F 'False = Void
F 'True = ()
data T (b :: Bool)
= MkT1
| MkT2 !(F b)
ex :: SBool b -> T b -> ()
ex sb t =
case t of
MkT1 -> ()
MkT2 f ->
case sb of
STrue -> f
ex2 :: SBool b -> T b -> ()
ex2 sb t =
case t of
MkT2 f ->
case sb of
STrue -> f
MkT1 -> ()
|
