{-# 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
--->
[L2] MinMax (S v1) Z c1 d1, [L3] MinMax (S v1) Z c2 Z}
---> 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:
--->
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
--->
[L2] MinMax (S v1) Z c1 d1, [L3] MinMax (S v1) Z c2 Z}
--->
[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 declartions
- 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.
-}