Update Trac ticket URLs to point to GitLab
[ghc.git] / testsuite / tests / typecheck / should_compile / T3018.hs
1 {-# OPTIONS_GHC -w #-}
2 {-# LANGUAGE UndecidableInstances, EmptyDataDecls #-}
3 {-# LANGUAGE RankNTypes, KindSignatures, MultiParamTypeClasses, FlexibleInstances #-}
4
5 -- Works with new constraint solver
6
7 module T3018 where
8
9 import Control.Monad
10
11 -- minimal Data/Rep classes
12 data Rep (ctx :: * -> *) a
13
14 class Data (ctx :: * -> *) a where rep :: Rep ctx a
15
16 class Sat a where dict :: a
17
18 --------- Version A: failed in 6.12.3 -----------
19 -- Substitution class
20 -- substitute [a -> t] t'.
21 class Subst_A a t t' where
22 subst_A :: (Monad m) => a -> t -> t' -> m t'
23
24 data SubstD_A a t t' = SubstD_A {substD_A:: forall m. (Monad m) => a -> t -> t' -> m t'}
25
26 -- Allow override dictionary version with implementation of type class Subst
27 instance Subst_A a t t' => Sat (SubstD_A a t t') where
28 dict = SubstD_A {substD_A = subst_A}
29
30 -- Generic instance
31 instance Data (SubstD_A a t) t' => Subst_A a t t' where
32 subst_A = undefined
33
34 --------- Version B: passed in 6.12.3 -----------
35 -- Substitution class
36 -- substitute [a -> t] t'.
37 class Subst_B a t t' where
38 subst_B :: a -> t -> t' -> t'
39
40 data SubstD_B a t t' = SubstD_B {substD_B :: a -> t -> t' -> t'}
41
42 -- allow override dictionary version with implementation of type class Subst
43 instance Subst_B a t t' => Sat (SubstD_B a t t') where
44 dict = SubstD_B {substD_B = subst_B}
45
46 -- generic instance
47 instance Data (SubstD_B a t) t' => Subst_B a t t' where
48 subst_B = undefined
49
50
51 {- Commentary from #3018
52
53 Here are the key lines of code:
54
55 class Subst a t t' where
56 subst :: (Monad m) => a -> t -> t' -> m t'
57
58 data SubstD a t t'
59 = SubstD (forall m. Monad m => a -> t -> t' -> m t')
60
61 instance Data (SubstD a t) t' => Subst a t t' -- (1)
62
63 instance Subst a t t' => Sat (SubstD a t t') where -- (2)
64 dict = SubstD subst
65
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:
68
69 Using the instance declaration for Subst (which matches anything!)
70 Using the context of the Sat (SubstD ..) instance declaration itself
71
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:
75
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
79
80 it should really say
81
82 ...from the context (Subst a t t', Monad m)
83
84 but that's a bit of a separate matter.
85
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:
91
92 f :: Eq [a] => a -> blah
93 f x = let g :: Int -> Int
94 g = ....([x]==[x])...
95 in ...
96
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.
101
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 -}