blob: 7d2b8668162c497f69244bad32dee1c255f3c82f (
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
|
:set -XTypeFamilyDependencies
:set -XDataKinds
:set -XUndecidableInstances
:set -XPolyKinds
:set -XMultiParamTypeClasses
-- IA = injectivity annotation `| foo -> bar`
-- use incorrect tyvar in LHS of IA
type family F a = r | a -> a
type family Fc a = r | a -> a where { Fc a = a }
class Fcl a where { type Ft a = r | a -> a }
-- declare result tyvar to be duplicate (without IA)
type family G a = a
type family Gc a = a where { Gc a = a }
-- declare result tyvar to be duplicate (with IA)
type family Gb a = a | a -> a
type family Gcb a = a | a -> a where { Gcb a = a }
class Gclb a where { type Gtb a = a | a -> a } -- here we want two errors
-- not in-scope tyvar in RHS of IA
type family I a b = r | r -> c
type family Ic a b = r | r -> c where { Ic a b = a }
class Icl a b where { type It a b = r | r -> c }
-- repeated tyvar on RHS of IA
type family J a b = r | r -> a a
type family Jc a b = r | r -> a a where { Jc a b = a }
class Jcl a b where { type Jt a b = r | r -> a a }
-- not in-scope tyvar in LHS of IA
type family L a b = r | c -> a
type family Lc a b = r | c -> a where { Lc a b = a }
class Lcl a b where { type Lt a b = r | c -> a }
-- result variable shadows variable in class head
class M a b where { type Mt b = a | a -> b }
-- here b is out-of-scope
class N a b where { type Nt a = r | r -> a b }
|
