No title

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
{-# LANGUAGE TypeInType #-}
module Main where

import Prelude
import Data.Kind


type family ValueKind (obj :: k) :: Type

type family Get (key :: k) (obj :: a) :: ValueKind a

data Map k v = Map [(k,v)]

type instance Get (k :: kk) (('Map ('((k::kk), (v::kv)) ': _)) :: Map kk kv) = (v :: kv)

type instance ValueKind (Map k v) = v


ERROR: 
     Occurs check: cannot construct the infinite kind:
        kv ~ ValueKind (Map kk kv)
     In the type (v :: kv)
      In the type instance declaration for Get

No title (annotation)

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
{-# LANGUAGE TypeInType #-}
module Type.Data.Map where

import Prelude
import Data.Kind


type family KeyKind (obj :: Type)
type family ValKind (obj :: Type)

type family Get (key :: KeyKind a) (obj :: a) :: ValKind a

data Map k v = Map [(k,v)]

type instance Get k ('Map ('(k,v) ': _)) = v

type instance KeyKind (Map k v) = k
type instance ValKind (Map k v) = v



ERROR

     Occurs check: cannot construct the infinite kind:
        k0 ~ KeyKind (Map k0 v0)
      The type variables v0, k0 are ambiguous
     In the first argument of Get, namely k
      In the type instance declaration for Get
   |         
15 | type instance Get k ('Map ('(k,v) ': _)) = v
   |                   ^
             
/home/wdanilo/dev/libs/new-core/libs/typelevel/Type/Data/Map.hs:15:44: error:
     Occurs check: cannot construct the infinite kind:
        v0 ~ ValKind (Map k0 v0)
      The type variables k0, v0 are ambiguous
     In the type v
      In the type instance declaration for Get
   |         
15 | type instance Get k ('Map ('(k,v) ': _)) = v
   |                                            ^