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
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
|
{-# LANGUAGE UndecidableInstances, FlexibleInstances,
MultiParamTypeClasses, FunctionalDependencies #-}
module Foo where
data Z = Z
data S a = S a
class MinMax a b c d | a b -> c d, a c d -> b, b c d -> a
instance MinMax Z Z Z Z -- (a)
instance MinMax a Z Z a -- (b) -- L1: wrongly flagged as error src.
instance MinMax Z b Z b -- (c)
instance MinMax a b c d => MinMax (S a) (S b) (S c) (S d)
-- (d)
class Extend a b where extend :: a -> b -> b
instance Extend Z b where Z `extend` b = b
instance MinMax a b _c b => Extend a b where
_a `extend` b = b
t :: MinMax a b _c d => a -> b -> d
t _ _ = (undefined :: d)
n0 = Z
n1 = S n0
t1 = n1 `t` n0 -- L2
t2 = n1 `extend` n0 -- L3: uncommenting just this line produces
-- an error message pointing at L1 and L2
-- with no mention of the real culprit, L3.
-- t1 :: S Z -- L4: uncommenting this and L3 produces an
-- error message rightly pointing at L2 and L3.
{- n0 :: Z; n1 :: S Z
Call of extend gives wanted: Extend (S Z) Z
Use instance => MinMax (S Z) Z gamma Z
FD on (b) => gamma ~ Z, Z ~ S Z
=> MinMax (S Z) Z Z Z
FD on (a), 3rd fundep => Z ~ S Z
(b) again (sadly) Z ~ S Z
-}
{-
Here's what is happening.
Lacking the type signature t1 :: S Z, we get
n0 :: Z
n1 :: S v1
t1 :: d1 with constraint ([L2] MinMax (S v1) Z c1 d1)
t2 :: Z with constraint ([L3] Extend (S v1) Z)
[L2] MinMax (S v1) Z c1 d1, [L3] Extend (S v1) Z
---> <by instance for Extend a b>
[L2] MinMax (S v1) Z c1 d1, [L3] MinMax (S v1) Z c2 Z}
---> <combining these two constraints using (a b -> c d)
[L2] MinMax (S v1) Z c1 Z, [L3] MinMax (S v1) Z c1 Z}
Now there are the two constraints are indistinguishable,
and both give rise to the same error:
---> <combining first with [L1] instance MinMax a Z Z a>
c1=Z, Z=S v1 ERROR
In either case, the error points to L1.
A different sequence leads to a different error:
[L2] MinMax (S v1) Z c1 d1, [L3] Extend (S v1) Z
---> <by instance for Extend a b>
[L2] MinMax (S v1) Z c1 d1, [L3] MinMax (S v1) Z c2 Z}
---> <combining first with [L1] instance MinMax a Z Z a>
[L2] MinMax (S v1) Z Z (S2 v1), [L3] MinMax (S v1) Z c2 Z}
Now combining the two constraints gives rise to the error, but
this time pointing to L2,L3.
I can't explain exactly why adding the type signature for t1
changes the order.
Hmm. Perhaps a good improvement strategy would be:
- first do improvement against the instance declarations
- and only then do pairwise improvement between constraints
I've implemented that, and indeed it improves the result.
Instead of:
Foo.hs:1:0:
Couldn't match `S Z' against `Z'
Expected type: S Z
Inferred type: Z
When using functional dependencies to combine
MinMax a Z Z a, arising from the instance declaration at Foo.hs:10:0
MinMax (S Z) Z _c d, arising from use of `t' at Foo.hs:25:8-10
we get
Foo.hs:1:0:
Couldn't match `S Z' against `Z'
Expected type: S Z
Inferred type: Z
When using functional dependencies to combine
MinMax a Z Z a, arising from the instance declaration at Foo.hs:10:0
MinMax (S Z) Z _c Z, arising from use of `extend' at Foo.hs:27:8-15
And this error in t2 is perfectly correct. You get it even if you comment
out the entire definition of t1.
-}
|
