Testsuite error message changes
[ghc.git] / testsuite / tests / indexed-types / should_compile / T3826.hs
1 {-# LANGUAGE TypeFamilies #-}
2
3 module T3826 where
4
5 class C a where
6 type E a
7 c :: E a -> a -> a
8
9 data T a = MkT a
10 -- MkT :: a -> T a
11
12 instance C (T b) where
13 type E (T b) = b
14 c x (MkT _) = MkT x
15
16
17 f t@(MkT x) = c x t
18
19 {- c :: E alpha -> alpha -> alpha
20 t :: T beta
21 x :: beta
22 f :: T beta -> gamma
23
24
25 [W] C alpha
26 [W] E alpha ~ beta
27 [W] alpha ~ T beta
28 [W] gamma ~ alpha
29
30 ---> beta = t_aqf alpha = t_aqg
31 alpha := T beta
32 gamma := alpha
33
34 [W] E (T beta) ~ beta
35
36 -->
37 [W] ufsk ~ beta
38 [W] E (T beta) ~ ufsk
39
40 --> (swap and subst)
41 beta := ufsk
42 [W] x : E (T ufsk) ~ ufsk (do not rewrite RHS)
43
44 take a step ax: E (T beta) ~ beta
45
46 -->
47 [W] ufsk
48 --------------------------
49 But what about this?
50 --------------------------
51
52 axiom F [a] = F [a]
53
54 x : F [a] ~ fsk
55 step
56 ax : F [a] ~ F [a]
57 flatten
58 ax ; x : F [a] ~ fsk
59 x = ax ; x Oh dear!
60 -}
61