1 {-# OPTIONS_GHC -w #-}

2 {-# LANGUAGE UndecidableInstances, EmptyDataDecls #-}

3 {-# LANGUAGE RankNTypes, KindSignatures, MultiParamTypeClasses, FlexibleInstances #-}

5 -- Works with new constraint solver

11 -- minimal Data/Rep classes

18 --------- Version A: failed in 6.12.3 -----------

19 -- Substitution class

20 -- substitute [a -> t] t'.

26 -- Allow override dictionary version with implementation of type class Subst

30 -- Generic instance

34 --------- Version B: passed in 6.12.3 -----------

35 -- Substitution class

36 -- substitute [a -> t] t'.

42 -- allow override dictionary version with implementation of type class Subst

46 -- generic instance

51 {- Commentary from #3018

53 Here are the key lines of code:

55 class Subst a t t' where

56 subst :: (Monad m) => a -> t -> t' -> m t'

58 data SubstD a t t'

59 = SubstD (forall m. Monad m => a -> t -> t' -> m t')

61 instance Data (SubstD a t) t' => Subst a t t' -- (1)

63 instance Subst a t t' => Sat (SubstD a t t') where -- (2)

64 dict = SubstD subst

66 The call to 'subst' on the last line gives rise to a constraint (Subst

67 a t t'). But that constraint can be satisfied in two different ways:

69 Using the instance declaration for Subst (which matches anything!)

70 Using the context of the Sat (SubstD ..) instance declaration itself

72 If GHC uses (1) it gets into a corner it can't get out of, because now

73 it needs (Data (SubstD a t) t'), and that it can't get. The error

74 message is a bit misleading:

76 T3018.hs:29:28:

77 Could not deduce (Data (SubstD a t) t') from the context (Monad m)

78 arising from a use of `subst' at T3018.hs:29:28-32

80 it should really say

82 ...from the context (Subst a t t', Monad m)

84 but that's a bit of a separate matter.

86 Now, you are hoping that (2) will happen, but I hope you can see that

87 it's delicate. Adding the (Monad m) context just tips things over the

88 edge so that GHC doesn't "see" the (Subst a t t') in the context until

89 too late. But the real problem is that you are asking too much. Here

90 is a simpler example:

92 f :: Eq [a] => a -> blah

93 f x = let g :: Int -> Int

94 g = ....([x]==[x])...

95 in ...

97 The use of == requires Eq [a], but GHC will probably use the list

98 equality instance to simplify this to Eq a; and then it can't deduce

99 Eq a from Eq [a]. Local constraints that shadow or override global

100 instance declarations are extremely delicate.

102 All this is perhaps soluble if GHC were to be lazier about solving

103 constraints, and only makes the attempt when it has all the evidence

104 in hand. I'm thinking quite a bit about constraint solving at the

105 moment and will bear that in mind. But I can't offer you an immediate

106 solution. At least I hope I've explained the problem.

107 -}