{-# LANGUAGE TypeOperators, TypeFamilies #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
    -- The type of 'empty' is indeed ambiguous

module T2544 where

import Data.Kind

data (:|:) a b = Inl a | Inr b

class Ix i where
   type IxMap i :: Type -> Type
   empty  :: IxMap i [Int]

data BiApp a b c = BiApp (a c) (b c)

instance (Ix l, Ix r) => Ix (l :|: r) where
   type IxMap (l :|: r) = BiApp (IxMap l) (IxMap r)
   empty = BiApp empty empty

-- [W] w1: a c ~ IxMap ii1 [Int]                  (from first 'empty')
-- [W] w2: b c ~ IxMap ii2 [Int]                  (from second 'empty')
-- [W] w3: BiApp a b c ~ IxMap (l :|: r) [Int]    (from call of BiApp
--           ~ BiApp (IxMap l) (IxMap r) [Int]

-- If we process w3 first, we'll rewrite it with w1, w2
-- yielding two constraints (Ix io ~ IxMap l, Ix i1 ~ IxMap r)
-- both with location of w3.  Then we report just one of them,
-- because we suppress multiple errors from the same location
--
-- But if we process w1,w2 first, we'll get the same constraints
-- but this time with different locations.