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
74
|
{-# LANGUAGE Haskell2010 #-}
{-# LANGUAGE TypeFamilies, FlexibleContexts #-}
module Class4 where
class (Eq (Depend s)) => Bug s where
type Depend s
trans :: Depend s -> Depend s
instance Bug Int where
type Depend Int = ()
trans = (+1)
check :: (Bug s) => Depend s -> Bool
check d = d == trans d
{-
Given: (Bug s, Eq (Depend s))
= (Bug s, Eq fsk, Depend s ~ fsk)
Wanted: (Eq alpha, (invocation of == at alpha)
Depend s ~ alpha (first arg of ==)
Depend sigma ~ alpha (second arg of ==)
Bug sigma, (invocation of trans at sigma)
Depend sigma ~ Depend s (first arg of trans)
{der}Eq (Depend sigma) (superclass of Bug sigma)
==>
Wanted: (Eq alpha, (invocation of == at alpha)
Depend s ~ alpha (first arg of ==)
Depend sigma ~ alpha (second arg of ==)
Bug sigma, (invocation of trans at sigma)
{der}Eq (Depend sigma) (superclass of Bug sigma)
==>
Wanted: (Eq alpha, (invocation of == at alpha)
Depend s ~ alpha (first arg of ==)
Depend sigma ~ alpha (second arg of ==)
Bug sigma, (invocation of trans at sigma)
{der}Eq uf_ahj
Depend sigma ~ uf_ahj
==> uf := alpha
Wanted: (Eq alpha, (invocation of == at alpha)
Depend s ~ alpha (first arg of ==)
Depend sigma ~ alpha (second arg of ==)
Bug sigma, (invocation of trans at sigma)
{der}Eq alpha)
==> discharge Eq alpha from {der}
Wanted: (Depend s ~ alpha (first arg of ==)
Depend sigma ~ alpha (second arg of ==)
Bug sigma, (invocation of trans at sigma)
{der}Eq alpha)
==> use given Depend s ~ fsk
Wanted: (alpha ~ fsk
Depend sigma ~ alpha (second arg of ==)
Bug sigma, (invocation of trans at sigma)
{der}Eq alpha)
==> alpha := fsk
Wanted: ({given}alpha ~ fsk
Depend sigma ~ alpha (second arg of ==)
Bug sigma, (invocation of trans at sigma)
{der}Eq fsk)
==> discharge {der} Eq fsk
Wanted: ({given}uf ~ fsk
Depend sigma ~ uf (second arg of ==)
Bug sigma, (invocation of trans at sigma)
-}
|
