443d73a17ad9c16efaa915fb47d4cc9d2150ae18
[ghc.git] / testsuite / tests / typecheck / should_compile / T3018.hs
1 {-# LANGUAGE UndecidableInstances, EmptyDataDecls #-}
2 {-# LANGUAGE RankNTypes, KindSignatures, MultiParamTypeClasses, FlexibleInstances #-}
3
4 -- Works with new constraint solver
5
6 module T3018 where
7
8 import Control.Monad
9
10 -- minimal Data/Rep classes
11 data Rep (ctx :: * -> *) a
12
13 class Data (ctx :: * -> *) a where rep :: Rep ctx a
14
15 class Sat a where dict :: a
16
17 --------- Version A: failed in 6.12.3 -----------
18 -- Substitution class
19 -- substitute [a -> t] t'.
20 class Subst_A a t t' where
21 subst_A :: (Monad m) => a -> t -> t' -> m t'
22
23 data SubstD_A a t t' = SubstD_A {substD_A:: (Monad m) => a -> t -> t' -> m t'}
24
25 -- Allow override dictionary verion with implementation of type class Subst
26 instance Subst_A a t t' => Sat (SubstD_A a t t') where
27 dict = SubstD_A {substD_A = subst_A}
28
29 -- Generic instance
30 instance Data (SubstD_A a t) t' => Subst_A a t t' where
31 subst_A = undefined
32
33 --------- Version B: passed in 6.12.3 -----------
34 -- Substitution class
35 -- substitute [a -> t] t'.
36 class Subst_B a t t' where
37 subst_B :: a -> t -> t' -> t'
38
39 data SubstD_B a t t' = SubstD_B {substD_B :: a -> t -> t' -> t'}
40
41 -- allow override dictionary verion with implementation of type class Subst
42 instance Subst_B a t t' => Sat (SubstD_B a t t') where
43 dict = SubstD_B {substD_B = subst_B}
44
45 -- generic instance
46 instance Data (SubstD_B a t) t' => Subst_B a t t' where
47 subst_B = undefined
48
49
50 {- Commentary from Trac #3018
51
52 Here are the key lines of code:
53
54 class Subst a t t' where
55 subst :: (Monad m) => a -> t -> t' -> m t'
56
57 data SubstD a t t'
58 = SubstD (forall m. Monad m => a -> t -> t' -> m t')
59
60 instance Data (SubstD a t) t' => Subst a t t' -- (1)
61
62 instance Subst a t t' => Sat (SubstD a t t') where -- (2)
63 dict = SubstD subst
64
65 The call to 'subst' on the last line gives rise to a constraint (Subst
66 a t t'). But that constraint can be satisfied in two different ways:
67
68 Using the instance declaration for Subst (which matches anything!)
69 Using the context of the Sat (SubstD ..) instance declaration itself
70
71 If GHC uses (1) it gets into a corner it can't get out of, because now
72 it needs (Data (SubstD a t) t'), and that it can't get. The error
73 message is a bit misleading:
74
75 T3018.hs:29:28:
76 Could not deduce (Data (SubstD a t) t') from the context (Monad m)
77 arising from a use of `subst' at T3018.hs:29:28-32
78
79 it should really say
80
81 ...from the context (Subst a t t', Monad m)
82
83 but that's a bit of a separate matter.
84
85 Now, you are hoping that (2) will happen, but I hope you can see that
86 it's delicate. Adding the (Monad m) context just tips things over the
87 edge so that GHC doesn't "see" the (Subst a t t') in the context until
88 too late. But the real problem is that you are asking too much. Here
89 is a simpler example:
90
91 f :: Eq [a] => a -> blah
92 f x = let g :: Int -> Int
93 g = ....([x]==[x])...
94 in ...
95
96 The use of == requires Eq [a], but GHC will probably use the list
97 equality instance to simplify this to Eq a; and then it can't deduce
98 Eq a from Eq [a]. Local constraints that shadow or override global
99 instance declarations are extremely delicate.
100
101 All this is perhaps soluble if GHC were to be lazier about solving
102 constraints, and only makes the attempt when it has all the evidence
103 in hand. I'm thinking quite a bit about constraint solving at the
104 moment and will bear that in mind. But I can't offer you an immediate
105 solution. At least I hope I've explained the problem.
106 -}