Bump `base` version to 4.9.0.0 (closes #11026)
[ghc.git] / testsuite / tests / typecheck / should_fail / tcfail143.hs
1 {-# LANGUAGE UndecidableInstances, FlexibleInstances,
2 MultiParamTypeClasses, FunctionalDependencies #-}
3
4 module Foo where
5
6 data Z = Z
7 data S a = S a
8
9 class MinMax a b c d | a b -> c d, a c d -> b, b c d -> a
10 instance MinMax Z Z Z Z -- (a)
11 instance MinMax a Z Z a -- (b) -- L1: wrongly flagged as error src.
12 instance MinMax Z b Z b -- (c)
13 instance MinMax a b c d => MinMax (S a) (S b) (S c) (S d)
14 -- (d)
15
16 class Extend a b where extend :: a -> b -> b
17 instance Extend Z b where Z `extend` b = b
18 instance MinMax a b _c b => Extend a b where
19 _a `extend` b = b
20
21 t :: MinMax a b _c d => a -> b -> d
22 t _ _ = (undefined :: d)
23
24 n0 = Z
25 n1 = S n0
26
27 t1 = n1 `t` n0 -- L2
28
29 t2 = n1 `extend` n0 -- L3: uncommenting just this line produces
30 -- an error message pointing at L1 and L2
31 -- with no mention of the real culprit, L3.
32
33 -- t1 :: S Z -- L4: uncommenting this and L3 produces an
34 -- error message rightly pointing at L2 and L3.
35
36
37 {- n0 :: Z; n1 :: S Z
38
39 Call of extend gives wanted: Extend (S Z) Z
40 Use instance => MinMax (S Z) Z gamma Z
41 FD on (b) => gamma ~ Z, Z ~ S Z
42 => MinMax (S Z) Z Z Z
43 FD on (a), 3rd fundep => Z ~ S Z
44 (b) again (sadly) Z ~ S Z
45
46 -}
47 {-
48
49 Here's what is happening.
50
51 Lacking the type signature t1 :: S Z, we get
52
53 n0 :: Z
54 n1 :: S v1
55 t1 :: d1 with constraint ([L2] MinMax (S v1) Z c1 d1)
56 t2 :: Z with constraint ([L3] Extend (S v1) Z)
57
58 [L2] MinMax (S v1) Z c1 d1, [L3] Extend (S v1) Z
59 ---> <by instance for Extend a b>
60 [L2] MinMax (S v1) Z c1 d1, [L3] MinMax (S v1) Z c2 Z}
61 ---> <combining these two constraints using (a b -> c d)
62 [L2] MinMax (S v1) Z c1 Z, [L3] MinMax (S v1) Z c1 Z}
63
64 Now there are the two constraints are indistinguishable,
65 and both give rise to the same error:
66
67 ---> <combining first with [L1] instance MinMax a Z Z a>
68 c1=Z, Z=S v1 ERROR
69
70 In either case, the error points to L1.
71
72
73 A different sequence leads to a different error:
74
75 [L2] MinMax (S v1) Z c1 d1, [L3] Extend (S v1) Z
76 ---> <by instance for Extend a b>
77 [L2] MinMax (S v1) Z c1 d1, [L3] MinMax (S v1) Z c2 Z}
78 ---> <combining first with [L1] instance MinMax a Z Z a>
79 [L2] MinMax (S v1) Z Z (S2 v1), [L3] MinMax (S v1) Z c2 Z}
80
81 Now combining the two constraints gives rise to the error, but
82 this time pointing to L2,L3.
83
84 I can't explain exactly why adding the type signature for t1
85 changes the order.
86
87
88 Hmm. Perhaps a good improvement strategy would be:
89 - first do improvement against the instance declartions
90 - and only then do pairwise improvement between constraints
91
92 I've implemented that, and indeed it improves the result.
93 Instead of:
94
95 Foo.hs:1:0:
96 Couldn't match `S Z' against `Z'
97 Expected type: S Z
98 Inferred type: Z
99 When using functional dependencies to combine
100 MinMax a Z Z a, arising from the instance declaration at Foo.hs:10:0
101 MinMax (S Z) Z _c d, arising from use of `t' at Foo.hs:25:8-10
102
103 we get
104
105 Foo.hs:1:0:
106 Couldn't match `S Z' against `Z'
107 Expected type: S Z
108 Inferred type: Z
109 When using functional dependencies to combine
110 MinMax a Z Z a, arising from the instance declaration at Foo.hs:10:0
111 MinMax (S Z) Z _c Z, arising from use of `extend' at Foo.hs:27:8-15
112
113
114 And this error in t2 is perfectly correct. You get it even if you comment
115 out the entire definition of t1.
116 -}