Error overlapping instances when trying to write a backup instance

Question

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

First, I use the entire kitchen sink except OverlappingInstances .

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

I also use the poly-like Proxy and level type, 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 instance A ; ThingB no.

 class A x where traceA :: x -> String data ThingA = ThingA data ThingB = ThingB instance A ThingA where traceA = const "ThingA" 

The purpose of the following parts is to record an instance of A for (x, y) , which will be determined until there is an instance of A x or A y . If there is an instance of A x , it will return ("fst " ++) . traceA . fst ("fst " ++) . traceA . fst ("fst " ++) . traceA . fst . If there is not an instance of A x , but there is an instance of B x , it will return ("snd " ++) . traceA . fst ("snd " ++) . traceA . fst ("snd " ++) . traceA . fst .

The first step is to create a functional dependency to check for the presence of instance A by matching it with the instance header. This is a common approach from an extended 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 instances of A , we can determine if (x, y) have it.

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

Now I'm going to get away from a simple example in extended overlap and introduce a second functional dependency to choose whether to use an instance of A x or A y . (We could use a different type than Bool for Chooses and SwitchA to avoid confusion with APred .)

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

If there is an instance of A x , we will always select 'True , otherwise 'False .

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

Then, like the extended overlap example, I define a class that is identical to A , with the exception of an additional type variable for selection and a Proxy argument for each member.

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

It is easy to identify 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 an instance of SwitchA for the same type as (x, y) Chooses , we can define an instance of A (x, y) .

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

Everything here is beautifully compiled. 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 searching for an instance for Chooses 'True ... ; should an instance instance flag ~ 'False => Chooses flag ... not match when the flag already known as 'True ?

And vice versa, if I try

 traceA (ThingB, ThingA) 

I get an error

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

Any understanding of what happens when I try to get the compiler to do what it designed to not do would be helpful.

Edit - Simplify

Based on the observation of this answer , we can completely get rid of Chooses 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 find out what's really going on, check out the Chooses class. In particular, note that it is not lazy in the case of False (i.e. when it cannot immediately determine that it must be true):

 chooses :: Chooses bx => 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 this is not laziness is not so simple. The most specific instance that

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

checked first. To check this, the compiler must check APred . Here, instance APred 'True ThingA does not match because you have ThingB . Thus, it falls into the second instance and combines flag (in modes) with False. Then the APred 'True x constraint cannot be met! So typechecking fails. The type error you received looks strange, but I think this is because you do not have OverlappingInstances. When I turn it on with 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) 

As expected, the types True and False cannot be unified.

The fix is ​​pretty simple. Convert your classes to function types. Type functions are essentially equivalent, but "more lazy." This is a very wavy hand - sorry, I have no 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 are thinking, "Oh no, I need to rewrite all my code in order to use type families." This is not so, since you can always “omit” a type family in a class predicate with a functional dependency:

 instance Chooses' x ~ b => Chooses bx 

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"