{-# LANGUAGE Haskell2010 #-}
{-# 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.
-}