blob: bc7cc89201d00aec94385386e0bd1c7bed2fa791 (
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
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
|
{-
This test is inspired by
Practical dependent type checking using twin types
Victor López Juan and Nils Anders Danielsson
TyDe '20
https://dl.acm.org/doi/10.1145/3406089.3409030
The challenge is whether we can unify two types where the only
way to know that the kinds are equal is to unify the types. This
would fail in an algorithm that required kind unification before
type unification.
-}
{-# LANGUAGE TypeOperators, TypeApplications, DataKinds,
StandaloneKindSignatures, PolyKinds, GADTs,
TypeFamilies, NamedWildCards, PartialTypeSignatures #-}
{-# OPTIONS_GHC -Wno-partial-type-signatures #-}
module LopezJuan where
import Data.Type.Equality ( (:~~:)(..) )
import Data.Kind ( Type )
import Data.Proxy ( Proxy )
-- amazingly, this worked without modification
data SBool :: Bool -> Type where
SFalse :: SBool False
STrue :: SBool True
data BoolOp where
None :: Bool -> BoolOp
Some :: Bool -> BoolOp
type F :: Bool -> Type
type family F b
get :: BoolOp -> Bool
get (None _) = True
get (Some x) = x
type Get :: BoolOp -> Bool
type family Get x where
Get (None _) = True
Get (Some x) = x
type TyFun :: Type -> Type -> Type
data TyFun arg res
type (~>) :: Type -> Type -> Type
type arg ~> res = TyFun arg res -> Type
infixr 0 ~>
data Const :: a -> (b ~> a)
f :: SBool x -> (:~~:) @(F (Get (_alpha x)) ~> BoolOp)
@(F True ~> BoolOp)
(Const (None x))
(Const (_alpha x))
f _ = HRefl
-- and something simpler:
type family Idish guard a where
Idish True a = a
Idish False a = Int
g :: (:~~:) @(Idish _alpha Type)
@Type
(Proxy _alpha)
(Proxy True)
g = HRefl
|
