Ari Fordsham
Ari Fordsham

Reputation: 2515

Constraints and fundep resolution

I have a pair of classes, C1 and C2, with a fundep on C1, as follows:

class C1 a b | a -> b
class C2 a

I declare an instance:

instance (C2 a) => C1 a T1

When I declare another instance, I get an error:

instance  C1 T2 T3
functional dependencies conflict between instance declarations:
  instance C2 a => C1 a T1
  instance C1 T2 T3

Basically, I intended the T1 instance to mean: forall a where a is an instance of C2 b is T1, allowing the other instance so long as T2 is not an instance of C2.

GHC is understanding it as: forall a b is T1, thereby ruling out assigning any other type to b.

I know I can work around this by wrapping a in a newtype, but that is awkward for my application.

Can anyone explain how to get my desired behaviour, if it is indeed possible, or else explain why not?

Upvotes: 0

Views: 151

Answers (1)

AntC
AntC

Reputation: 2806

You have instances overlapping on the 'argument' position of the FunDep. This should work (untested):

{-# LANGUAGE GADTs, UndecidableInstances #-}

instance {-# OVERLAPPABLE #-} (C2 a, b ~ T1) => C1 a b

instance C1 T2 T3

This is exploiting GHC's 'bogus' FunDep consistency check. ('bogus' is a note in the compiler code from SPJ.) It should not work; it is very much 'cheating'; there's every chance one day somebody will fix it and the above code will stop working.

OTOH that's been the threat since 2008; it's still not been addressed; nobody (except me) seems to have a better suggestion.

What the above doesn't implement is your

I intended the T1 instance to mean: forall a where a is an instance of C2 b is T1, allowing the other instance so long as T2 is not an instance of C2.

But you know whether T2 is an instance of C2 -- it's a specific type(?)

If you mean it for any type t2, I think you need to rephrase the question. It might be feasible with fancier overlaps and FunDeps -- and still more bogusness.

Consider a helper class:

{-# LANGUAGE DataKinds #-}
class IsC2 a (t :: Bool) | a -> t

instance IsC2 T2 True

instance (t ~ False) => IsC2 a  t

You need an instance IsC2 t2 True for every specific type t2 that is an instance of C2.

instance (IsC2 a t, C1C2 t a T1 T3 b) => C1 a b

class C1C2 t a bt bf b  | t bt bf -> b
instance (C2 a) => C1C2 True  a bt bf bt   -- constraint as belt and braces
instance C1C2 False a bt bf bf

Upvotes: 1

Related Questions