Overlapping instances error when trying to write fallback instance

Question

I'm trying to do something similar to the advanced overlap trick to define an instance with overlapping behavior. I'm trying to derive an instance for a tuple that will use an instance for the fst field if one exists, otherwise use the instance for the snd field if it exists. This ultimately results in a seemingly incorrect error about overlapping instances.

To begin with, I'm using all of the kitchen sink except for OverlappingInstances.

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}

I'm also using a poly-kinded Proxy and type level or, :||:.

import Data.Proxy

type family (:||:) (a :: Bool) (b :: Bool) :: Bool
type instance (:||:) False a = a
type instance (:||:) True a = True

A is a very simple class to play with. ThingA has an A instance; ThingB doesn't.

class A x where
    traceA :: x -> String

data ThingA = ThingA
data ThingB = ThingB

instance A ThingA where
    traceA = const "ThingA"

The goal of the next parts is to write an A instance for (x, y) which will be defined as long as there's either an A x or A y instance. If there's an A x instance, it will return ("fst " ++) . traceA . fst. If there is not an A x instance but there is a B x instance it will return ("snd " ++) . traceA . fst.

The first step will be to make a functional dependency to test for whether there's an A instance by matching against the instance head. This is the ordinary approach from the advanced overlap article.

class APred (flag :: Bool) x | x -> flag

instance APred 'True ThingA
instance (flag ~ 'False) => APred flag x

If we can determine if x and y both have A instances, we can determine if (x, y) is going to have one.

instance (APred xflag x, APred yflag y, t ~ (xflag :||: yflag)) => APred t (x, y)

Now I'm going to depart from the simple example in advanced overlap and introduce a second functional dependency to select whether to use the A x or A y instance. (We could use a different kind than Bool for Chooses and SwitchA to avoid confusion with APred.)

class Chooses (flag :: Bool) x | x -> flag

If there's an A x instance we'll always choose 'True, otherwise 'False.

instance (APred 'True x) => Chooses 'True (x, y) 
instance (flag ~ 'False) => Chooses flag (x, y)

Then, like the advanced overlap example, I define a class identical to A except with an extra type variable for the choice and a Proxy argument for every member.

class SwitchA (flag :: Bool) x where
    switchA :: Proxy flag -> x -> String

This is easy to define instances for

instance (A x) => SwitchA 'True (x, y) where
    switchA _ = ("fst " ++) . traceA . fst

instance (A y) => SwitchA 'False (x, y) where
    switchA _ = ("snd " ++) . traceA . snd

Finally, if there is a SwitchA instance for the same type that (x, y) Chooses, we can define an A (x, y) instance.

instance (Chooses flag (x, y), SwitchA flag (x, y)) => A (x, y) where
    traceA = switchA (Proxy :: Proxy flag)

Everything up to here compiles beautifully. However, if I try to add

traceA (ThingA, ThingB)

I get the following error.

    Overlapping instances for Chooses 'True (ThingA, ThingB)
      arising from a use of `traceA'
    Matching instances:
      instance APred 'True x => Chooses 'True (x, y)
        -- Defined at defaultOverlap.hs:46:10
      instance flag ~ 'False => Chooses flag (x, y)
        -- Defined at defaultOverlap.hs:47:10
    In the first argument of `print', namely
      `(traceA (ThingA, ThingA))'

What's going on here? Why do these instances overlap when looking for an instance for Chooses 'True ...; shouldn't the instance flag ~ 'False => Chooses flag ... instance fail to match when flag is already known to be 'True?

Conversely, if I try

traceA (ThingB, ThingA)

I get the error

    No instance for (A ThingB) arising from a use of `traceA'
    In the first argument of `print', namely
      `(traceA (ThingB, ThingA))'

Any insight into what is going on when I try to push the compiler into doing what it's designed not to do would be helpful.

Edit - Simplification

Based on an observation from this answer, we can get rid of Chooses completely and write

instance (APred choice x, SwitchA choice (x, y)) => A (x, y) where
    traceA = switchA (Proxy :: Proxy choice)

This solves the problem for traceA (ThingB, ThingA)

Answer 1

To see what is really going on, look at the Chooses class. Specifically, notice that it is not lazy in the False case (ie, when it cannot immediately determine it should have value true):

chooses :: Chooses b x =>  x -> Proxy b 
chooses _ = Proxy

>:t chooses (ThingA, ())
chooses (ThingA, ()) :: Proxy 'True
>:t chooses (ThingB, ())

<interactive>:1:1: Warning:
    Couldn't match type 'True with 'False
    In the expression: chooses (ThingB, ())

The reason why it isn't lazy isn't quite so simple. The most specific instance, which is

instance (APred 'True x) => Chooses 'True (x, y)

is tried first. To verify if this, the compiler must check the APred. Here, instance APred 'True ThingA does not match, because you have ThingB. So it falls through to the 2nd instance and unifies flag (in Chooses) with False. Then the constraint APred 'True x cannot hold! So typechecking fails. The type error you got is sort of strange, but I think that is because you don't have OverlappingInstances enabled. When I turn it on with your code, I get the following:

>traceA (ThingA, ThingA)
"fst ThingA"
>traceA (ThingB, ThingA)

<interactive>:43:1:
    Couldn't match type 'True with 'False
    In the expression: traceA (ThingB, ThingA)
    In an equation for `it': it = traceA (ThingB, ThingA)

Which is as expected - the types True and False cannot be unified.

The fix is quite simple. Convert your classes to type functions. Type functions are essentially equivalent, but "more lazy". This is very hand wavy - sorry I don't have a better explanation why it works.

type family APred' x :: Bool where 
  APred' ThingA = True
  APred' x = False 

type family Chooses' x :: Bool where 
  Chooses' (x, y) = APred' x 

instance (Chooses' (x,y) ~ flag, SwitchA flag (x, y)) => A (x, y) where
    traceA = switchA (Proxy :: Proxy flag)

Now you think "oh no, I have to rewrite all my code to use type families." That is not the case, since you can always "lower" a type family to a Class predicate with a functional dependency:

instance Chooses' x ~ b => Chooses b x 

Now your original instance instance (Chooses flag (x, y), SwitchA flag (x, y)) => A (x, y) where ... will work as expected.

>traceA (ThingA, ThingA)
"fst ThingA"
>traceA (ThingB, ThingA)
"snd ThingA"