blob: 5c4d51382ffaa0a8b67240b4f970a9c624455580 (
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
|
{-# LANGUAGE GADTs, TypeOperators, PolyKinds, DataKinds,
TypeFamilyDependencies, RankNTypes, LambdaCase, EmptyCase,
UndecidableInstances #-}
module T13822 where
import Data.Kind
data KIND = STAR | KIND :> KIND
data Ty :: KIND -> Type where
TInt :: Ty STAR
TBool :: Ty STAR
TMaybe :: Ty (STAR :> STAR)
TApp :: Ty (a :> b) -> (Ty a -> Ty b)
type family
IK (k :: KIND) = (res :: Type) | res -> k where
IK STAR = Type
IK (a:>b) = IK a -> IK b
type family
I (t :: Ty k) = (res :: IK k) | res -> t where
I TInt = Int
I TBool = Bool
I TMaybe = Maybe
I (TApp f a) = (I f) (I a)
data TyRep (k :: KIND) (t :: Ty k) where
TyInt :: TyRep STAR TInt
TyBool :: TyRep STAR TBool
TyMaybe :: TyRep (STAR:>STAR) TMaybe
TyApp :: TyRep (a:>b) f -> TyRep a x -> TyRep b (TApp f x)
zero :: TyRep STAR a -> I a
zero = \case
TyInt -> 0
TyBool -> False
TyApp TyMaybe _ -> Nothing
-- Inferred type:
--
-- int :: TyRep STAR TInt -> Int
int rep = zero rep :: Int
-- bool:: TyRep STAR TBool -> Bool
bool rep = zero rep :: Bool
-- Previously failed with:
--
-- v.hs:43:16: error:
-- • Couldn't match kind ‘k’ with ‘'STAR’
-- ‘k’ is a rigid type variable bound by
-- the inferred type of
-- maybeInt :: (I 'TInt ~ Int, I 'TMaybe ~ Maybe) =>
-- TyRep 'STAR ('TApp 'TMaybe 'TInt) -> Maybe Int
-- at v.hs:25:3
-- When matching the kind of ‘'TMaybe’
-- Expected type: Maybe Int
-- Actual type: I ('TApp 'TMaybe 'TInt)
-- • In the expression: zero rep :: Maybe Int
-- In an equation for ‘maybeInt’: maybeInt rep = zero rep :: Maybe Int
-- • Relevant bindings include
-- rep :: TyRep 'STAR ('TApp 'TMaybe 'TInt) (bound at v.hs:43:10)
-- maybeInt :: TyRep 'STAR ('TApp 'TMaybe 'TInt) -> Maybe Int
-- (bound at v.hs:43:1)
-- Failed, modules loaded: none.
maybeInt rep = zero rep :: Maybe Int
|
